aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* Make displayGravatar Jason Gross2017-06-17
* Add some more display constantsGravatar Jason Gross2017-06-17
* Add bool into P256Gravatar Jason Gross2017-06-17
* make displayGravatar Jason Gross2017-06-17
* Finish MontgomeryP256 (less conditional subtract)Gravatar Jason Gross2017-06-17
* Remove fails; if we fail too strongly, we miss debugging informationGravatar Jason Gross2017-06-17
* Try to fail a bit faster in bad reificationGravatar Jason Gross2017-06-17
* Add back failure at level 100Gravatar Jason Gross2017-06-17
* Better error messages in reificationGravatar Jason Gross2017-06-17
* Add initial IntegrationTestMontgomeryP256.vGravatar Jason Gross2017-06-17
* Better reification tactic debuggingGravatar Jason Gross2017-06-17
* Fix a typoGravatar Jason Gross2017-06-17
* Define m in p256Gravatar Jason Gross2017-06-17
* Fix spellingGravatar Jason Gross2017-06-17
* fix WWMM partial evaluationGravatar Andres Erbsen2017-06-16
* Unfold more things in src/Specific/MontgomreyP256Gravatar Jason Gross2017-06-16
* finish tuple-ifying Montgomery APIGravatar jadep2017-06-16
* Switch to using tuples for word-by-word montgomeryGravatar Jason Gross2017-06-16
* Fix buildGravatar Jason Gross2017-06-16
* Revert PR #203Gravatar Jason Gross2017-06-16
* update ocq2C sed scriptGravatar Andres Erbsen2017-06-16
* make displayGravatar Jason Gross2017-06-16
* Make use of CArrayNotationsGravatar Jason Gross2017-06-16
* Fix CArrayNotationsGravatar Jason Gross2017-06-16
* Revert "Revert "Add CArrayNotations""Gravatar Jason Gross2017-06-16
* montgomery p256 in Specific WIPGravatar Andres Erbsen2017-06-16
* make displayGravatar Jason Gross2017-06-15
* Revert "Add CArrayNotations"Gravatar Jason Gross2017-06-15
* Finish karatsuba mul, add display file (#199)Gravatar Jason Gross2017-06-15
* ed448 mul: use two carry chains to fix bounds (still silly otherwise)Gravatar Andres Erbsen2017-06-15
* Add CArrayNotationsGravatar Jason Gross2017-06-15
* CPSify montgomery wbw reductionGravatar Jason Gross2017-06-15
* CPSify Saturated API in preparation for CPSifying Montgomery (see #194)Gravatar jadep2017-06-15
* Show the bounds going wrong in karatsubaGravatar Jason Gross2017-06-15
* Display Z operations with ℤ attachedGravatar Jason Gross2017-06-15
* Eliminate well-bounded IdWithAlt from final outputGravatar Jason Gross2017-06-15
* Improve replace_match_with_destructuring_matchGravatar Jason Gross2017-06-15
* Fix debugging codeGravatar Jason Gross2017-06-15
* Don't force [Require Import String] for debug msgsGravatar Jason Gross2017-06-15
* Fix a changed case in the proof in loop.vGravatar Jason Gross2017-06-15
* Better for_loop induction principleGravatar Jason Gross2017-06-15
* Export ZUtil.Z2Nat in ZUtilGravatar Jason Gross2017-06-15
* Add ZUtil.Z2NatGravatar Jason Gross2017-06-15
* Add for_cps_unroll1Gravatar Jason Gross2017-06-15
* Add eq_loop_cps_large_nGravatar Jason Gross2017-06-15
* Edwards coordinates precomputed addition formulaGravatar Andres Erbsen2017-06-15
* move CPS notations to Util.CPSNotationsGravatar Andres Erbsen2017-06-15
* fix wrong number of limbs for square as wellGravatar jadep2017-06-15
* fix wrong number of limbsGravatar jadep2017-06-15
* Added reduce to karatsuba synthesisGravatar jadep2017-06-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 19:22:22 +0000