aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/GF25519BoundedCommon.v
Commit message (Expand)AuthorAge
* Revert "Add apply10"Gravatar Jason Gross2017-01-07
* Add i10top_correct_and_boundedGravatar Jason Gross2017-01-07
* Add appify10Gravatar Jason Gross2017-01-07
* Minor change to inm_op_correct_and_bounded_prefixGravatar Jason Gross2016-11-25
* Fix a typoGravatar Jason Gross2016-11-25
* Add inm_op_correct_and_bounded_iff_prefixGravatar Jason Gross2016-11-25
* Add inm_op_correct_and_boundedGravatar Jason Gross2016-11-25
* Update AddCoordinatesGravatar Jason Gross2016-11-17
* Fix postfreezeW_correct_and_boundedGravatar Jason Gross2016-11-14
* Speed up some GF25519 tacticsGravatar Jason Gross2016-11-14
* Begin filling in @JasonGross's stubsGravatar jadep2016-11-11
* Remove 8.6 only syntaxGravatar Jason Gross2016-11-11
* Freeze stubsGravatar Jason Gross2016-11-11
* Connect [is_bounded] to [bounded_by]Gravatar Jason Gross2016-11-06
* Add eta-expansion in GF25519BoundedCommon.vGravatar Jason Gross2016-11-05
* Add unfold_is_boundedGravatar Jason Gross2016-11-05
* 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-06-06 07:02:49 +0000