aboutsummaryrefslogtreecommitdiff
path: root/src/Assembly/GF25519.v
Commit message (Expand)AuthorAge
* Silence a warningGravatar Jason Gross2016-10-31
* Disable extraction in src/Assembly/GF25519.vGravatar Jason Gross2016-10-29
* Strip function extensionality, enable printing of sub, mul, opp, freezeGravatar Jason Gross2016-10-27
* Tactics to manually remove Z.to/of_N and suchGravatar Robert Sloan2016-10-26
* Refactors to remove intermediate conversionsGravatar Robert Sloan2016-10-26
* Refactors to remove intermediate conversions in HLConversionsGravatar Robert Sloan2016-10-25
* Use HL conversions for all data types + Pipeline.v refactorsGravatar Robert Sloan2016-10-24
* Make lower bounds work by using HL conversionsGravatar Robert Sloan2016-10-21
* merge rsloan-phoas refactors into masterGravatar Robert Sloan2016-10-21
|\
* \ merge rsloan-phoas refactors into masterGravatar Robert Sloan2016-10-21
|\ \
* | | committing unstable refactors to patch masterGravatar Robert Sloan2016-10-21
| | * committing unstable refactors to patch masterGravatar Robert Sloan2016-10-21
| |/ |/|
| * Adjust bounds in assemblyGravatar Jason Gross2016-10-20
| * Use carry versions of operationsGravatar Jason Gross2016-10-20
|/
* Fast bounds-checking machinery but lower-bounds are brokenGravatar Robert Sloan2016-10-18
* Converting to bounded machineryGravatar Robert Sloan2016-10-17
* More of the Conversions.v correctness proofsGravatar Robert Sloan2016-10-14
* Use 64-bit limbs in PipelinesGravatar Robert Sloan2016-10-14
* Making sub bounds actually tightGravatar Robert Sloan2016-10-14
* Moved to non-extended operations + Extraction + Bounds-checkingGravatar Robert Sloan2016-10-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 16:36:55 +0000