aboutsummaryrefslogtreecommitdiff
path: root/src/Arithmetic/MontgomeryReduction
Commit message (Expand)AuthorAge
* Add (partially admitted) integration tests for add, sub, oppGravatar Jason Gross2017-06-22
* P256: Partial work on add, sub, oppGravatar Jason Gross2017-06-22
* Account for future changes of #219Gravatar Jason Gross2017-06-22
* Prove In_to_list_left_tl, In_left_hd, to_list_left_appendGravatar Jason Gross2017-06-21
* Prove some admitted lemmas about uweightGravatar Jason Gross2017-06-21
* Make use of new conditional_subtractGravatar Jason Gross2017-06-20
* Make use of new small_addGravatar Jason Gross2017-06-20
* Fix build errorGravatar Jason Gross2017-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
* Update wbw to work with new apiGravatar Jason Gross2017-06-18
* Drop the 0-carry bit before bounds analysisGravatar Jason Gross2017-06-17
* Make use of non-uniform tuple-based addGravatar Jason Gross2017-06-17
* fix WWMM partial evaluationGravatar Andres Erbsen2017-06-16
* Switch to using tuples for word-by-word montgomeryGravatar Jason Gross2017-06-16
* CPSify montgomery wbw reductionGravatar Jason Gross2017-06-15
* 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
* 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
* 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
* Clean up implementationGravatar Jason Gross2017-05-01
* Use columns rather than positionalGravatar Jason Gross2017-05-01
* Use mod (weight (S i) / weight i), not mod (weight i)Gravatar Jason Gross2017-05-01
* Initial stab at word-by-word montgomeryGravatar Jason Gross2017-05-01
* rename-everythingGravatar Andres Erbsen2017-04-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 15:37:18 +0000