aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
...
* 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
* pulled in a CPS version of Karatsuba from another branchGravatar jadep2017-06-02
* Add an only-parsing loop notationGravatar Jason Gross2017-06-02
* Add experimental loopsGravatar Jason Gross2017-06-02
* Strip trailing whitespaceGravatar Jason Gross2017-06-02
* Only use bool in freezeGravatar Jason Gross2017-05-21
* fix last wide mul in curve25519-51Gravatar Andres Erbsen2017-05-20
* src/Specific/x25519_c64.c.sh: use exact donna skeletonGravatar Andres Erbsen2017-05-20
* make displayGravatar Jason Gross2017-05-20
* Fix extra opp in freezeGravatar Jason Gross2017-05-20
* make display (freeze, fully notationified)Gravatar Jason Gross2017-05-20
* Add compiler optimization for [Zselect (-x) _ _]Gravatar Jason Gross2017-05-20
* make displayGravatar Jason Gross2017-05-20
* Get sbb conversion working in the pipelineGravatar Jason Gross2017-05-20
* make displayGravatar Jason Gross2017-05-20
* Add adc -> sbb to arithmetic simpliferGravatar Jason Gross2017-05-20
* Add sbb notations to CNotationsGravatar Jason Gross2017-05-20
* Also reify Z.sub_with_get_borrowGravatar Jason Gross2017-05-20