aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/GF25519Reflective
Commit message (Expand)AuthorAge
* Remove the Const constructor of exprfGravatar Jason Gross2017-01-19
* Split out Reflection.Equality, change Tflat implicit argumentGravatar Jason Gross2017-01-19
* Add reified LadderStep without carriesGravatar Jason Gross2017-01-07
* Revert "Add apply10"Gravatar Jason Gross2017-01-07
* Add Common10_4OpGravatar Jason Gross2017-01-07
* Add Expr10_4OpGravatar Jason Gross2017-01-07
* Admit Common9_4Op.vGravatar Jason Gross2016-12-08
* Various application lemmasGravatar Jason Gross2016-11-23
* More GF25519ReflectiveCommon generalizationGravatar Jason Gross2016-11-22
* Copy bounds, fix a typoGravatar Jason Gross2016-11-22
* Start work on a faster version of GF*Reflective/Common*Gravatar Jason Gross2016-11-21
* Fix missing import for List.repeat in 8.4Gravatar Jason Gross2016-11-21
* Fix some problems with previous commitGravatar Jason Gross2016-11-17
* Remove admits, fill templates, copy boundsGravatar Jason Gross2016-11-17
* Update AddCoordinatesGravatar Jason Gross2016-11-17
* Minor change in AddCoordinatesGravatar Jason Gross2016-11-17
* Move util definitions to util folderGravatar Jason Gross2016-11-17
* Add reified mostly-bounds-checked add_coordinatesGravatar Jason Gross2016-11-17
* Work around bug #5205 (arguments naming weirdness)Gravatar Jason Gross2016-11-16
* Split fixedpoint in interpfGravatar Jason Gross2016-11-16
* Add more things to Reflective/CommonGravatar Jason Gross2016-11-16
* Fix for Coq 8.5 (more unfolding)Gravatar Jason Gross2016-11-15
* Speed up some GF25519 tacticsGravatar Jason Gross2016-11-14
* Support for 128-bit wordsGravatar Jason Gross2016-11-14
* Remove dead code in rebuild-reified.pyGravatar Jason Gross2016-11-11
* Begin filling in @JasonGross's stubsGravatar jadep2016-11-11
* 8.4-compatible universe handlingGravatar 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
* Refactor various reflective thingsGravatar Jason Gross2016-11-06
* The fix in 8.4 broke 8.5/8.6, so we fix thatGravatar 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 proofs about boundedness to GF25519Reflective/Common.vGravatar 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
* Shove Z.Interpretations into closer alignmentGravatar Jason Gross2016-11-03
* Fix buildGravatar Jason Gross2016-11-03
* Fix bounds that were reversedGravatar Jason Gross2016-11-03
* 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 bounds type in Specific/GF25519Reflective/Common.vGravatar 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
* Also construct relatedness proofs in reifiedGravatar Jason Gross2016-10-30
* Minor changes to GF25519 reflectiveGravatar Jason Gross2016-10-30
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-05 23:59:55 +0000