aboutsummaryrefslogtreecommitdiff
path: root/src/Util/WordUtil.v
Commit message (Expand)AuthorAge
* Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtilGravatar Jason Gross2018-08-23
* git submodule update --remote --recursiveGravatar Andres Erbsen2018-02-24
* minor updates needed to make it compile with bbvGravatar Samuel Gruetter2018-02-05
* Don't rely on autogenerated namesGravatar Jason Gross2017-06-05
* Split off notation and defs in ZUtilGravatar Jason Gross2017-05-12
* s/appcontext/context/Gravatar Jason Gross2017-05-11
* Add wordToZ_ZToWord_modGravatar Jason Gross2017-04-08
* Add ZToWord_wordToZ_ZToWord_smallGravatar Jason Gross2017-04-08
* More fine-grained tactic importsGravatar Jason Gross2017-04-03
* move lemmas from Ed25519 to WordUtilGravatar jadep2017-02-22
* Move things from WordUtil to ZUtil, add word lemmaGravatar Jason Gross2017-02-06
* More zutilGravatar Jason Gross2017-02-03
* Add wordToZ_ZToWord_wordToZGravatar Jason Gross2017-02-01
* Add NToWord_wordToN_NToWordGravatar Jason Gross2017-02-01
* Add transparent equality proofs for fixed wordTGravatar Jason Gross2017-01-21
* Revert "Fix a missing qualification"Gravatar Jason Gross2017-01-21
* Fix a missing qualificationGravatar Jason Gross2017-01-21
* Move weqb_hetero to Bedrock.WordGravatar Jason Gross2017-01-21
* Add weqb_heteroGravatar Jason Gross2017-01-21
* Lemmas about winit, wlastGravatar Rob Sloan2016-11-11
* Fix for Coq 8.4Gravatar Jason Gross2016-11-11
* Most of the admits in Ed25519.vGravatar Rob Sloan2016-11-11
* Fix for 8.4Gravatar Jason Gross2016-11-10
* Hint Rewrite is section-local; move to top-levelGravatar Jason Gross2016-11-10
* Remove WordizeUtil dependency from WordUtilGravatar Rob Sloan2016-11-09
* Rebase + remove WordizeUtil dependency from Z/InterpretationsGravatar Rob Sloan2016-11-09
|\
| * Rewrite cast_word so that it's extracted betterGravatar Jason Gross2016-11-09
* | Finished WordUtil, word operations in Z/InterpretationGravatar Rob Sloan2016-11-09
* | Not quite done with WordUtil lemmas.Gravatar Robert Sloan2016-11-08
|\|
| * put EdDSA encoding sign bit at the MSBGravatar Andres Erbsen2016-11-04
* | More of jgross admits, less neg and the cmovsGravatar Rob Sloan2016-11-01
* | most of jgross' admitsGravatar Rob Sloan2016-10-31
|/
* Some work on proofs in src/Reflection/Z/Interpretations.vGravatar Jason Gross2016-10-27
* Add some rewrites and admitted lemmasGravatar Jason Gross2016-10-27
* Add beginnings of various interpretations of expression treesGravatar Jason Gross2016-10-27
* More 8.4 fixesGravatar Jason Gross2016-10-23
* Prove more things in WordUtilGravatar Jason Gross2016-10-23
* Fill in some word util admitted lemmasGravatar Jason Gross2016-10-23
* Add word64eqb_ZeqbGravatar Jason Gross2016-10-21
* integrate bitwise operationsGravatar Andres Erbsen2016-10-12
* Generalize and simplify cast_word_reflGravatar Jason Gross2016-10-12
* word manipulation functions for secret key formatting (#74)Gravatar Andres Erbsen2016-10-12
* Derive EdDSA.verify from equational specificationGravatar Andres Erbsen2016-09-16
* Proved decode_point_eq in Ed25519 (comparing encodings is equivalent toGravatar jadep2016-04-29
* Cleanup: mostly moving lemmas to Util files, some moving lemmas to more gener...Gravatar jadep2016-04-28
* Finish absolutizing importsGravatar Jason Gross2016-03-10
* Factor out some bedrock dependencies into WordUtilGravatar Jason Gross2016-02-25
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-01 12:26:24 +0000