aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* 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
* Add eta_match_base_type_implGravatar Jason Gross2017-06-13
* Stronger invert_op tacticGravatar Jason Gross2017-06-13
* Fix a major bug in C-notation printingGravatar Jason Gross2017-06-13
* Don't unfold id_with_altGravatar Jason Gross2017-06-13
* Move temporary CNotations importGravatar Jason Gross2017-06-13
* Reify Z.mul_with_split_at_bitwidthGravatar Jason Gross2017-06-13
* Add mul_split_at_bitwidth, define things in terms of thatGravatar Jason Gross2017-06-13
* Update WBW montgomery commentsGravatar Jason Gross2017-06-13
* Add Z.peano_rect_strongGravatar Jason Gross2017-06-13
* Add dec_eq_comparisonGravatar Jason Gross2017-06-13
* Add Z.peano_rectGravatar Jason Gross2017-06-13
* Fill in mul_split to wbw montgomeryGravatar Jason Gross2017-06-13
* Add Z.mul_splitGravatar Jason Gross2017-06-13
* WBW-montgomery: Fill in most context variablesGravatar Jason Gross2017-06-13
* finish computational portions of operations needed for Montgomery, and sketch...Gravatar jadep2017-06-12
* Remove use of id_tuple_with_alt_proofGravatar Jason Gross2017-06-12
* Add a Show to keep track of where we are in karatsubaGravatar Jason Gross2017-06-12
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 16:05:51 +0000