aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/GF25519Bounded.v
Commit message (Expand)AuthorAge
* Handle both kinds of sqrtGravatar Jason Gross2016-11-14
* More generic sqrtGravatar Jason Gross2016-11-14
* Fix postfreezeW_correct_and_boundedGravatar Jason Gross2016-11-14
* Support for 128-bit wordsGravatar Jason Gross2016-11-14
* Fix some sqrt thingsGravatar Jason Gross2016-11-14
* Fix a missing unfoldGravatar Jason Gross2016-11-14
* Update bounds things with prefreezeGravatar Jason Gross2016-11-14
* Add mulW_noinlineGravatar Jason Gross2016-11-14
* More 8.4pl2 fixesGravatar Jason Gross2016-11-12
* Fix for Coq 8.2Gravatar Jason Gross2016-11-12
* Fixes for 8.4 (instantiate)Gravatar Jason Gross2016-11-12
* Proved postfreezeW_correct_and_boundedGravatar jadep2016-11-11
* Begin filling in @JasonGross's stubsGravatar jadep2016-11-11
* Freeze stubsGravatar Jason Gross2016-11-11
* separate Ed25519Extraction.v, add extraction to MakefileGravatar Andres Erbsen2016-11-03
* fix lingering reference to old name of renamed lemmaGravatar jadep2016-11-02
* Fix GF25519Bounded in a different wayGravatar Jason Gross2016-11-02
* Fix [sqrtW_sig]Gravatar Jason Gross2016-11-02
* Changes to sqrt for easier bounds proofs; currently blocked on broken proof i...Gravatar jadep2016-11-02
* Parameterize bounded things over the limb lengthGravatar Jason Gross2016-11-01
* Make it easier to extract word64Gravatar Jason Gross2016-10-31
* Switch to reflective bounded word in Ed25519Gravatar Jason Gross2016-10-31
* Switch to bounded ZGravatar Jason Gross2016-10-25
* Add pack, unpack, ge_modulus to axioms to be reifiedGravatar Jason Gross2016-10-24
* Finish twedprm_ERep proofGravatar Jason Gross2016-10-23
* Make some things instancesGravatar Jason Gross2016-10-23
* Generalize field_from_redundant_representationGravatar Jason Gross2016-10-23
* Add decode to GF25519BoundedCommonGravatar Jason Gross2016-10-22
* Fix divergence in src/Specific/GF25519Bounded.vGravatar Jason Gross2016-10-22
* Unfold interp stuff in Assembly/GF25519BoundedInstantiationGravatar Jason Gross2016-10-22
* Add bounded sqrtGravatar Jason Gross2016-10-22
* Remove axioms from src/Specific/GF25519Bounded.v, plug assemblyGravatar Jason Gross2016-10-21
* Remove code that should have been removedGravatar Jason Gross2016-10-20
* Split up GF25519Bounded to avoid circular dependenciesGravatar Jason Gross2016-10-20
* Add todoGravatar Jason Gross2016-10-20
* Switch from bounded Z to bounded wordGravatar Jason Gross2016-10-20
* More specific bounded requirements, implement invGravatar Jason Gross2016-10-19
* First pass at bounded version of GF25519Gravatar Jason Gross2016-10-19
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 05:44:00 +0000