aboutsummaryrefslogtreecommitdiff
path: root/src/Arithmetic
Commit message (Expand)AuthorAge
...
* Remove duplicate [small p] hypothesis from small_conditional_subGravatar Jason Gross2017-06-20
* Add conditional_sub_id to uncps globallyGravatar Jason Gross2017-06-20
* defined conditional_sub (see #207) -- small_conditional_sub admitted, eval_co...Gravatar jadep2017-06-20
* rename Columns.sub_cps to make it clear that no balance is addedGravatar jadep2017-06-20
* Don't depend on classical axioms for small_addGravatar Jason Gross2017-06-20
* Make use of new small_addGravatar Jason Gross2017-06-20
* Weaken preconditions on small_addGravatar Jason Gross2017-06-20
* Strip trailing whitespaceGravatar Jason Gross2017-06-20
* Fix build errorGravatar Jason Gross2017-06-19
* fixed precondition on small_addGravatar jadep2017-06-19
* mulmod: sig type in terms of equivalence modulo pGravatar Jason Gross2017-06-18
* Make use of new small_scmulGravatar Jason Gross2017-06-18
* proved small_scmulGravatar jadep2017-06-18
* Update wbw to work with new apiGravatar Jason Gross2017-06-18
* proved eval_scmulGravatar jadep2017-06-18
* proved small_zeroGravatar jadep2017-06-18
* proved small_drop_highGravatar jadep2017-06-18
* proved eval_drop_highGravatar jadep2017-06-18
* define strong small and re-prove small_add and small_compact with that defini...Gravatar jadep2017-06-18
* make scmul discard its carry in a saner way; rather than concatenating it in ...Gravatar jadep2017-06-18
* Drop the 0-carry bit before bounds analysisGravatar Jason Gross2017-06-17
* Fix scmul bounds issueGravatar jadep2017-06-17
* More eye-catching naming scheme for nm in saturatedGravatar Jason Gross2017-06-17
* Make use of non-uniform tuple-based addGravatar Jason Gross2017-06-17
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-08 14:15:10 +0000