aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/GF25519BoundedCommon.v
Commit message (Expand)AuthorAge
* Clean up fe25519_word64ize, give examplesGravatar Jason Gross2016-11-02
* GF25519BoundedCommon.v: require less higher order unification (8.4)Gravatar Andres Erbsen2016-11-02
* Prove fe25519WToZ_ZToW, rename FooToBarToFoo to BarToFoo_FooToBarGravatar Jason Gross2016-11-01
* Parameterize bounded things over the limb lengthGravatar Jason Gross2016-11-01
* Add fe25519WToZToWGravatar Jason Gross2016-11-01
* Make it easier to extract word64Gravatar Jason Gross2016-10-31
* Make it so that changing the list of wire bounds doesn't break the buildGravatar Jason Gross2016-10-31
* Revert "Switch from word to Z"Gravatar Jason Gross2016-10-31
* Switch from word to ZGravatar Jason Gross2016-10-31
* Switch to reflective bounded word in Ed25519Gravatar Jason Gross2016-10-31
* Use sigma types to fix extractionGravatar Jason Gross2016-10-31
* Simplify proof of proj1_fe25519_encodeGravatar Jason Gross2016-10-27
* Add lemmas about GF25519BoundedCommon.{encode,decode}Gravatar Jason Gross2016-10-27
* Switch to bounded ZGravatar Jason Gross2016-10-25
* Adjust bound on final word in wire_digits to 31Gravatar Jason Gross2016-10-24
* Fix bounds on wire_digitsGravatar Jason Gross2016-10-24
* Add pack, unpack, ge_modulus to axioms to be reifiedGravatar Jason Gross2016-10-24
* Add decode to GF25519BoundedCommonGravatar Jason Gross2016-10-22
* Make [vm_compute] on Bounded word reasonableGravatar Jason Gross2016-10-22
* Add word64eqb_ZeqbGravatar Jason Gross2016-10-21
* A bit of initial setup on correct_and_bounded proofs in GF25519BoundedInstant...Gravatar Jason Gross2016-10-20
* Plug bounded into assembly stuffGravatar Jason Gross2016-10-20
* Split up GF25519Bounded to avoid circular dependenciesGravatar Jason Gross2016-10-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 06:40:54 +0000