aboutsummaryrefslogtreecommitdiff
path: root/src/ModularArithmetic/PseudoMersenneBaseParams.v
Commit message (Collapse)AuthorAge
* Factored out some proofs that rely only on base being powers of two, and ↵Gravatar jadep2016-07-06
| | | | defined conversion between two such bases. This will allow conversion between the pseudomersenne base representation and the wire format. Also relocated some lemmas to Util.
* BaseSystem encode function is no longer naive; it does a mod/div loop rather ↵Gravatar jadep2016-06-28
| | | | than sticking the value of the Z input in the first digit. The condition that c is positive has been added to PseudoMersenneBaseParams--it is necessary for this encode and for canonicalization, for which it was previously a section variable.
* starting rewrite using different definition of mapGravatar jadep2016-06-11
|
* Merge and refactor of GF25519Gravatar jadep2016-04-11
|
* made BaseVector instance globalGravatar Jade Philipoom2016-03-20
|
* refactor of Basesystem and ModularBaseSystem; includes general code ↵Gravatar Jade Philipoom2016-03-20
organization and changes to pseudomersenne base parameters that require bases to be expressed as powers of 2, which reduces the burden of proof on the caller and allows carry functions to use bitwise operations rather than mod and division