aboutsummaryrefslogtreecommitdiff
path: root/src/Specific
Commit message (Expand)AuthorAge
...
| * UNTESTED simplification of specific GF25519 derivationGravatar Andres Erbsen2016-01-02
|/
* Remove redundancy in lemma statementGravatar Adam Chlipala2015-12-09
* Specific/GF25519: explicit formula for multiplicationGravatar Andres Erbsen2015-12-05
* GF25519: synthesize explicit formula for multiplication (no reduction yet)Gravatar Andres Erbsen2015-12-05
* Specific/GF25519: Updated to match new PseudoMersenneBaseParams spec.Gravatar Jade Philipoom2015-11-24
* ModularBaseSystem: relocated base_succ to PsuedoMersenneBaseParams, proved ca...Gravatar Jade Philipoom2015-11-20
* BaseSystem: added encode definition, included b0_1 precondition in BaseCoefs ...Gravatar Jade Philipoom2015-11-10
* ModularBaseSystem: finish base_goodGravatar Andres Erbsen2015-11-07
* ModularBaseSystem: prove some admits in mase system extensionGravatar Andres Erbsen2015-11-07
* Specific: PseudoMersenneBaseParams for GF25519Base25Point5.Gravatar Andres Erbsen2015-11-06
* instantiate BaseSystem using base 2^ceil(25.5i) representation of GF(2^255-19)Gravatar Andres Erbsen2015-11-06
* src/Specific/GF25519.v: more complicated example for BaseSystemGravatar Andres Erbsen2015-11-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 08:08:35 +0000