aboutsummaryrefslogtreecommitdiff
path: root/src/ModularArithmetic/ModularBaseSystemProofs.v
Commit message (Expand)AuthorAge
* remove trailing whitespace from src/Gravatar Andres Erbsen2016-06-20
* PseudoMersenneBaseRep.mul now carries by default (made possible by strictly b...Gravatar jadep2016-06-15
* changed representation definition to require digits vector to be the exact le...Gravatar jadep2016-06-15
* Added canonicalization to ModularBaseSystemOpt.Gravatar jadep2016-06-15
* MergeGravatar jadep2016-06-14
|\
* | Finished admits for canonicalization proofs.Gravatar jadep2016-06-14
* | reversed modulus_digits and proved a few admitsGravatar jadep2016-06-13
* | progress on second stage (conditional constant-time subtraction) of canonical...Gravatar jadep2016-06-13
| * More Coq 8.4pl2 fixesGravatar Jason Gross2016-06-11
* | starting rewrite using different definition of mapGravatar jadep2016-06-11
|/
* First stage of canonicalization proofs complete; proved 3 carry loops reduce ...Gravatar jadep2016-05-20
* Implemented subtraction mod q as as (sub a b = sub (add a (2*q)) b) to avoid ...Gravatar jadep2016-05-09
* Cleanup: mostly moving lemmas to Util files, some moving lemmas to more gener...Gravatar jadep2016-04-28
* moved lemmas from ModularBaseSystemProofs to various Util filesGravatar jadep2016-04-20
* Merge and refactor of GF25519Gravatar jadep2016-04-11
* made BaseVector instance globalGravatar Jade Philipoom2016-03-20
* refactor of Basesystem and ModularBaseSystem; includes general code organizat...Gravatar Jade Philipoom2016-03-20