aboutsummaryrefslogtreecommitdiff
path: root/src/Arithmetic
Commit message (Expand)AuthorAge
* fix WWMM partial evaluationGravatar Andres Erbsen2017-06-16
* finish tuple-ifying Montgomery APIGravatar jadep2017-06-16
* Switch to using tuples for word-by-word montgomeryGravatar Jason Gross2017-06-16
* CPSify montgomery wbw reductionGravatar Jason Gross2017-06-15
* CPSify Saturated API in preparation for CPSifying Montgomery (see #194)Gravatar jadep2017-06-15
* Improve replace_match_with_destructuring_matchGravatar Jason Gross2017-06-15
* Added reduce to karatsuba synthesisGravatar jadep2017-06-15
* fix goldilocks karatsuba; TODO implement reduceGravatar Andres Erbsen2017-06-14
* ScalarMult: Z -> G -> G (closes #193)Gravatar Andres Erbsen2017-06-14
* Update WBW montgomery commentsGravatar Jason Gross2017-06-13
* Fill in mul_split to wbw montgomeryGravatar 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
* Drop unused [bn] notationGravatar Jason Gross2017-06-12
* Drop some small hyps in light of small_add changeGravatar Jason Gross2017-06-12
* Remove eval_small_bounded_numlimbsGravatar Jason Gross2017-06-12
* Factor karatsuba through IdfunWithAlt, add testGravatar Jason Gross2017-06-11
* Finish admits in WordByWord/Proofs.vGravatar Jason Gross2017-06-10
* Minor changes to a proof in progressGravatar Jason Gross2017-06-10
* Remove useless small_from_bound; drop R_bigGravatar Jason Gross2017-06-10
* Add proofs about numlimbsGravatar Jason Gross2017-06-10
* Add constraint on scmul scalarGravatar Jason Gross2017-06-10
* Update context to not need eval_nonnegGravatar Jason Gross2017-06-10
* Add redc_boundGravatar Jason Gross2017-06-10
* Remove temporary fileGravatar Jason Gross2017-06-10
* More work in progress on montgomery proofsGravatar Jason Gross2017-06-10
* More work on redc correctness proofsGravatar Jason Gross2017-06-10
* Add initial proofs for word-by-wordGravatar Jason Gross2017-06-10
* Switch from t to T to match #157Gravatar Jason Gross2017-06-10
* Update redc algorithmGravatar Jason Gross2017-06-10
* Update word-by-word montgomery with ctx varsGravatar Jason Gross2017-06-10
* Finish proving loop invariant for wbw redcGravatar Jason Gross2017-06-09
* Make it clear that the combined definition/proof file is a work in progressGravatar Jason Gross2017-06-09
* Admit-free proof of cS3_mod_NGravatar Jason Gross2017-06-09
* Fix open sections errorGravatar Jason Gross2017-06-09
* More WIP on bounds for redcGravatar Jason Gross2017-06-09
* Minor progress on boundsGravatar Jason Gross2017-06-09
* Add pair-programmed wbw montgomeryGravatar Jason Gross2017-06-09
* add zero (as per #157)Gravatar jadep2017-06-08
* start saturated-arithmetic API for use in Montgomery (see discussion in #157)Gravatar jadep2017-06-08
* first stage of synthesis for karatsuba with alt-bounds hack, contains several...Gravatar jadep2017-06-07
* Don't rely on autogenerated namesGravatar Jason Gross2017-06-05
* Make Karatsuba depend on Arithmetic/Core to make calling it less of a painGravatar jadep2017-06-02
* export a few more wrapper definitions in PositionalGravatar jadep2017-06-02
* first successful stage of karatsuba synthesisGravatar jadep2017-06-02
* Strip trailing whitespaceGravatar Jason Gross2017-06-02
* force carry intermediates to be bound earlyGravatar Andres Erbsen2017-05-14
* remove redundant definitionGravatar jadep2017-05-14
* make freeze use the correct versions of add_get_carry and zselectGravatar jadep2017-05-14