aboutsummaryrefslogtreecommitdiff
path: root/src/Specific
Commit message (Expand)AuthorAge
...
* Fixes for 8.4 (instantiate)Gravatar Jason Gross2016-11-12
* GF25519: add ErepAddGravatar Andres Erbsen2016-11-11
* GF25519: add optimized addition chainGravatar Andres Erbsen2016-11-11
* Proved postfreezeW_correct_and_boundedGravatar jadep2016-11-11
* Remove dead code in rebuild-reified.pyGravatar Jason Gross2016-11-11
* Begin filling in @JasonGross's stubsGravatar jadep2016-11-11
* separate freeze into two partsGravatar jadep2016-11-11
* 8.4-compatible universe handlingGravatar Jason Gross2016-11-11
* Remove 8.6 only syntaxGravatar Jason Gross2016-11-11
* Freeze stubsGravatar Jason Gross2016-11-11
* Fix bug in 8.4 buildGravatar Jason Gross2016-11-09
* Split up GF25519Reflective.Common: faster+parallelGravatar Jason Gross2016-11-09
* move B_order_l and prime_qGravatar Andres Erbsen2016-11-06
* Refactor various reflective thingsGravatar Jason Gross2016-11-06
* Connect [is_bounded] to [bounded_by]Gravatar Jason Gross2016-11-06
* The fix in 8.4 broke 8.5/8.6, so we fix thatGravatar Jason Gross2016-11-06
* Add syntactic tuplesGravatar Jason Gross2016-11-06
* Add support for dependent reificationGravatar Jason Gross2016-11-06
* Work around broken evars in 8.4Gravatar Jason Gross2016-11-06
* Plug in boundedness proofsGravatar Jason Gross2016-11-05
* Add better bounded lemmas to reified thingsGravatar Jason Gross2016-11-05
* Add eta-expansion in GF25519BoundedCommon.vGravatar Jason Gross2016-11-05
* Add proofs about boundedness to GF25519Reflective/Common.vGravatar Jason Gross2016-11-05
* Add unfold_is_boundedGravatar Jason Gross2016-11-05
* Add code for overflow check (disabled bc freeze)Gravatar Jason Gross2016-11-05
* Split off some things from InterpretationsGravatar Jason Gross2016-11-05
* separate Ed25519Extraction.v, add extraction to MakefileGravatar Andres Erbsen2016-11-03
* Shove Z.Interpretations into closer alignmentGravatar Jason Gross2016-11-03
* Fix buildGravatar Jason Gross2016-11-03
* Make [freeze] proofs consider machine integer width and hard input bounds sep...Gravatar jadep2016-11-03
* Fix bounds that were reversedGravatar Jason Gross2016-11-03
* Clean up fe25519_word64ize, give examplesGravatar Jason Gross2016-11-02
* GF25519BoundedCommon.v: require less higher order unification (8.4)Gravatar Andres Erbsen2016-11-02
* 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
* Prove fe25519WToZ_ZToW, rename FooToBarToFoo to BarToFoo_FooToBarGravatar Jason Gross2016-11-01
* Export strings in GF25519Reflective/CommonGravatar Jason Gross2016-11-01
* Print out the computed bounds on the various opsGravatar 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
* Add bounds type in Specific/GF25519Reflective/Common.vGravatar 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
* Add src/Specific/GF25519Reflective.vGravatar Jason Gross2016-10-31
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 00:13:00 +0000