aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* More 8.4 fixesGravatar Jason Gross2016-10-23
* Fix 8.4 build issueGravatar Jason Gross2016-10-23
* Prove an admitted NatUtil lemmaGravatar Jason Gross2016-10-23
* Prove more things in WordUtilGravatar Jason Gross2016-10-23
* Fill in some word util admitted lemmasGravatar Jason Gross2016-10-23
* Fix a typoGravatar Jason Gross2016-10-23
* Prove onCurve_ERepBGravatar Jason Gross2016-10-23
* 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 for weaker pattern matching in < 8.4pl4Gravatar Jason Gross2016-10-22
* Fix for weaker pattern matching in < 8.4pl4Gravatar Jason Gross2016-10-22
* Made field-element encodings canonicalize elements before encoding themGravatar jadep2016-10-22
* Make [vm_compute] on Bounded word reasonableGravatar Jason Gross2016-10-22
* Fix divergence in src/Specific/GF25519Bounded.vGravatar Jason Gross2016-10-22
* Fix src/Experiments/Ed25519.v for Coq 8.4Gravatar Jason Gross2016-10-22
* Unfold interp stuff in Assembly/GF25519BoundedInstantiationGravatar Jason Gross2016-10-22
* Interpret LetIn to Let_In for better control of interpGravatar Jason Gross2016-10-22
* Add bounded sqrtGravatar Jason Gross2016-10-22
* Add more specific form of Proper_Let_In_nd_changebodyGravatar Jason Gross2016-10-22
* final touches/fixes for freeze restructuringGravatar jadep2016-10-22
* add arguments that I forgotGravatar jadep2016-10-22
* Modified [freeze] to be more reifyableGravatar jadep2016-10-22
* extraction: use more Haskell functionsGravatar Andres Erbsen2016-10-21
* fiddle with [rewrite <-!(field_div_definition)], maybe fix buildGravatar Andres Erbsen2016-10-21
* Add Bool lemmas about if statementsGravatar Jason Gross2016-10-21
* pow, not pow_opt, in Specific/GF25519Gravatar Jason Gross2016-10-21
* Add word64eqb_ZeqbGravatar Jason Gross2016-10-21
* Sane fieldwisebGravatar Jason Gross2016-10-21
* Make eqb sane (help from Jade)Gravatar Jason Gross2016-10-21
* Edwards.Extended.to_twisted: only one inversion, improve extractionGravatar Andres Erbsen2016-10-21
* Remove axioms from src/Specific/GF25519Bounded.v, plug assemblyGravatar Jason Gross2016-10-21
* Instantiate some things with bounded thingsGravatar Jason Gross2016-10-21
* Fix build failureGravatar Jason Gross2016-10-21
* extraction of [sign] using Haskell [Integer]s for limbsGravatar Andres Erbsen2016-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
* Remove code that should have been removedGravatar Jason Gross2016-10-20
* Adjust bounds in assemblyGravatar Jason Gross2016-10-20
* Split up GF25519Bounded to avoid circular dependenciesGravatar Jason Gross2016-10-20
* Various fixes for Coq 8.4Gravatar Jason Gross2016-10-20
* Merge remote-tracking branch 'jgross/instantiation-rsloan-phoas' into merge-r...Gravatar Jason Gross2016-10-20
|\
* | Add todoGravatar Jason Gross2016-10-20
* | Switch from bounded Z to bounded wordGravatar Jason Gross2016-10-20
| * Use carry versions of operationsGravatar Jason Gross2016-10-20
| * Merge branch 'master' into instantiation-rsloan-phoasGravatar Jason Gross2016-10-20
| |\ | |/ |/|
| * rfreeze, not rinv; update to saner boundedness requirementsGravatar 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-11-19 20:07:46 +0000