aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* 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
* Initial stab at id_with_altGravatar Jason Gross2017-06-11
* Add dummy version of IdWithAlt to compilersGravatar Jason Gross2017-06-11
* Factor karatsuba through IdfunWithAlt, add testGravatar Jason Gross2017-06-11
* Add unfold lemmas for id_with_altGravatar Jason Gross2017-06-11
* Add IdfunWithAltGravatar Jason Gross2017-06-11
* Be more forceful about clearing before abstract in glue codeGravatar Jason Gross2017-06-11
* Add script to remake Tactics.v fileGravatar Jason Gross2017-06-11
* Add clearbody_allGravatar Jason Gross2017-06-11
* Fix loop notations, add for loopsGravatar Jason Gross2017-06-11
* Reserve some more notationsGravatar Jason Gross2017-06-11
* cps notations WIP...Gravatar Andres Erbsen2017-06-11
* cps and loop notations WIPGravatar Andres Erbsen2017-06-11
* Finish admits in WordByWord/Proofs.vGravatar Jason Gross2017-06-10
* Add mod_pull_div{,_full}Gravatar Jason Gross2017-06-10
* More powerful replace_neg_with_posGravatar Jason Gross2017-06-10
* Fix a typoGravatar Jason Gross2017-06-10
* Rename power_mod_full to mod_pow_full for similarity with std libGravatar Jason Gross2017-06-10
* Add Z.pow_mod_ProperGravatar 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
* Fix broken implicitsGravatar Jason Gross2017-06-08
* 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
* Allow loop notation to printGravatar 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 22:12:10 +0000