aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* 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
* eddsa spec fixGravatar Andres Erbsen2017-06-14
* typofixGravatar Andres Erbsen2017-06-14
* fix goldilocks karatsuba; TODO implement reduceGravatar Andres Erbsen2017-06-14
* Loop changes, ScalarMultBase_correct with admitsGravatar Andres Erbsen2017-06-14
* loops WIPGravatar Andres Erbsen2017-06-14
* ScalarMult: Z -> G -> G (closes #193)Gravatar Andres Erbsen2017-06-14
* Add constant-pushing IdWithAlt optimizationGravatar Jason Gross2017-06-14
* Rework and speed up arithmetic simplifier proofsGravatar Jason Gross2017-06-14
* Make rewrite_eta_match_base_type_impl a bit fasterGravatar Jason Gross2017-06-13
* Fix a typoGravatar Jason Gross2017-06-13
* Add rewrite_eta_match_base_type_implGravatar Jason Gross2017-06-13