aboutsummaryrefslogtreecommitdiff
path: root/src/Util/WordUtil.v
Commit message (Expand)AuthorAge
* 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-15 09:45:21 +0000