aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/GF25519Reflective
Commit message (Collapse)AuthorAge
* 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
| | | | Now the _correct_and_bounded lemma goes through
* 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
| | | | | This is https://coq.inria.fr/bugs/show_bug.cgi?id=5205, Bogus "Error: Wrong argument name: n." error message in 8.4, 8.5
* Split fixedpoint in interpfGravatar Jason Gross2016-11-16
|
* Add more things to Reflective/CommonGravatar Jason Gross2016-11-16
| | | | Preparation for reflective add_coordinates
* 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
| | | | | I haven't found a good way to genericize the proofs of relatedness things, mostly because Modules and functors are annoying.
* 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
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change -------------------------------------------------------------------------------- 2m53.12s | Total | 2m52.26s || +0m00.85s -------------------------------------------------------------------------------- 0m01.38s | Specific/GF25519Reflective/Common | 0m43.51s || -0m42.12s 0m14.82s | Specific/GF25519Reflective/CommonBinOp | N/A || +0m14.82s 0m10.91s | Specific/GF25519Reflective/CommonUnOp | N/A || +0m10.91s 0m10.44s | Specific/GF25519Reflective/CommonUnOpWireToFE | N/A || +0m10.43s 0m06.42s | Specific/GF25519Reflective/CommonUnOpFEToWire | N/A || +0m06.41s 1m18.24s | Experiments/Ed25519 | 1m18.57s || -0m00.32s 0m07.97s | Specific/GF25519Reflective/Reified/Mul | 0m08.45s || -0m00.47s 0m07.89s | Specific/GF25519Reflective/Reified/Freeze | 0m07.84s || +0m00.04s 0m06.87s | Specific/GF25519Reflective | 0m06.92s || -0m00.04s 0m03.53s | Specific/GF25519Reflective/Reified/CarrySub | 0m03.63s || -0m00.10s 0m03.27s | Specific/GF25519Reflective/Reified/CarryAdd | 0m03.28s || -0m00.00s 0m03.18s | Specific/GF25519Reflective/Reified/CarryOpp | 0m03.15s || +0m00.03s 0m02.24s | Specific/GF25519Reflective/Reified/Unpack | 0m02.21s || +0m00.03s 0m02.19s | Specific/GF25519Reflective/Reified/Pack | 0m02.28s || -0m00.08s 0m02.16s | Specific/GF25519Reflective/Reified/Sub | 0m02.15s || +0m00.01s 0m02.14s | Specific/GF25519Bounded | 0m02.07s || +0m00.07s 0m02.07s | Experiments/Ed25519Extraction | 0m02.16s || -0m00.09s 0m01.99s | Specific/GF25519Reflective/Reified/Add | 0m01.81s || +0m00.17s 0m01.82s | Specific/GF25519Reflective/Reified/Opp | 0m01.78s || +0m00.04s 0m01.76s | Specific/GF25519Reflective/Reified/GeModulus | 0m01.71s || +0m00.05s 0m00.97s | Specific/GF25519Reflective/CommonUnOpFEToZ | N/A || +0m00.97s 0m00.86s | Specific/GF25519Reflective/Reified | 0m00.75s || +0m00.10s
* Refactor various reflective thingsGravatar Jason Gross2016-11-06
| | | | | We now have a more principled approach in many places, and some of the tuple-specific reasoning has been filled in.
* The fix in 8.4 broke 8.5/8.6, so we fix thatGravatar Jason Gross2016-11-06
| | | | Grrrr, evars
* Work around broken evars in 8.4Gravatar Jason Gross2016-11-06
|
* Plug in boundedness proofsGravatar Jason Gross2016-11-05
| | | | | We no longer admit the boundedness proofs (other than freeze); a significant chunk of the boundedness proofs now line up nicely.
* 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
| | | | | | | Currently freeze overflows; Jade says this is because the carry chain got reversed, and that she'll work on fixing this. We should enable the sanity checks at some point after this is fixed, to fail early if things overflow.
* Split off some things from InterpretationsGravatar Jason Gross2016-11-05
|
* Shove Z.Interpretations into closer alignmentGravatar Jason Gross2016-11-03
| | | | There's some really terrible code taking advantage of the fact that we only interpret a single type
* Fix buildGravatar Jason Gross2016-11-03
|
* Fix bounds that were reversedGravatar Jason Gross2016-11-03
|
* Export strings in GF25519Reflective/CommonGravatar Jason Gross2016-11-01
| | | | This makes pretty-printing of bounds easier
* Print out the computed bounds on the various opsGravatar Jason Gross2016-11-01
| | | | | | | | | Apparently some of them overflow (carry_opp, opp, sub, carry_sub) Also the bounds on ge_modulus are probably wrong, given that it's claiming that the function always returns 0. cc @andres-erbsen @jadep
* Parameterize bounded things over the limb lengthGravatar Jason Gross2016-11-01
| | | | | | | | | | It should now be possible to use sed to change to other limbs. Alas, there are a lot of files that need to be copied over (including about 5-10 in src/Specific/GF25519Reflective/Refied/) cc @jadep cc @andres-erbsen @jadep about my change to feDec
* Add bounds type in Specific/GF25519Reflective/Common.vGravatar Jason Gross2016-10-31
|
* Revert "Switch from word to Z"Gravatar Jason Gross2016-10-31
| | | | This reverts commit ac46ff22a9f6a279068ebdb897498e8dd14b1916.
* Switch from word to ZGravatar Jason Gross2016-10-31
|
* Switch to reflective bounded word in Ed25519Gravatar Jason Gross2016-10-31
| | | | (cc @andres-erbsen)
* Also construct relatedness proofs in reifiedGravatar Jason Gross2016-10-30
|
* Minor changes to GF25519 reflectiveGravatar Jason Gross2016-10-30
|
* Add reification of various operationsGravatar Jason Gross2016-10-30
| | | | | We split the reification up into separate files, one operation per file, so that we can run all the reification in parallel when building.
* Add initial work on reifying GF25519 stuffGravatar Jason Gross2016-10-30
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 09:36:57 +0000