aboutsummaryrefslogtreecommitdiff
path: root/src/Arithmetic/MontgomeryReduction
Commit message (Expand)AuthorAge
* remove old pipelineGravatar Andres Erbsen2019-01-09
* Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtilGravatar Jason Gross2018-08-23
* add equivalence proof for Montgomery reduce_via_partial_altGravatar Jade Philipoom2018-02-23
* Switch arithmetic to cps for Z * Z under the hoodGravatar Jason Gross2017-10-19
* Fix a typo that ends up not matteringGravatar Jason Gross2017-07-06
* fix [small_div] argumentsGravatar Andres Erbsen2017-07-02
* Prove saturated carrying-addition-chain correctGravatar jadep2017-06-30
* Reorganization of saturated arithmeticGravatar jadep2017-06-29
* Adapt to new arguments of saturated thingsGravatar Jason Gross2017-06-29
* proved eval_mod and eval_div (last remaining eval_ admits in Saturated)Gravatar jadep2017-06-27
* Fix a broken proofGravatar Jason Gross2017-06-26
* Add nonzero synthesisGravatar Jason Gross2017-06-26
* indentationGravatar Jason Gross2017-06-25
* Fixes #219Gravatar jadep2017-06-25
* Clean up some montgomery wbw instantiation, make displayGravatar Jason Gross2017-06-24
* Fill in axioms for sub_then_maybe_add; this required fiddling with updated ar...Gravatar jadep2017-06-24
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 22:04:03 +0000