| Commit message (Expand) | Author | Age |
* | More improved structure for EdDSA and PointFormats. | Jade Philipoom | 2015-12-10 |
* | Rewrote PointFormats to be parameterized by modulus; reformatting of EdDSA. | Jade Philipoom | 2015-12-09 |
* | EdDSA: Added PointFormatsSpec module type (possibly temporary). Transcribed p... | Jade Philipoom | 2015-12-07 |
* | Transcribed EdDSA parameters from [https://eprint.iacr.org/2015/677.pdf]. | Jade Philipoom | 2015-12-07 |
* | GaloisTheory: prove 4 trivial admits. GF25519 only assumption is now that 2^2... | Andres Erbsen | 2015-12-05 |
* | Specific/GF25519: explicit formula for multiplication | Andres Erbsen | 2015-12-05 |
* | reorganized lemmas; moved several to ListUtil and ZUtil. | Jade Philipoom | 2015-11-24 |
* | ModularBaseSystem: added definition to perform a specific sequence of carries... | Jade Philipoom | 2015-11-24 |
* | ModularBaseSystem: relocated base_succ to PsuedoMersenneBaseParams, proved ca... | Jade Philipoom | 2015-11-20 |
* | Added base_succ precondition to BaseSystem to help prove carrying. | Jade Philipoom | 2015-11-19 |
* | ModularBaseSystem: proving reduce case of carry_rep. | Jade Philipoom | 2015-11-18 |
* | ModularBaseSystem: carry_rep has boring modular arithmetic proofs | Andres Erbsen | 2015-11-17 |
* | ModularBaseSystem: introduced lemmas about breaking lists; working on carry_r... | Jade Philipoom | 2015-11-17 |
* | ModularBaseSystem.carry: implement, state lemmas, some progress on proofs | Andres Erbsen | 2015-11-17 |
* | BaseSystem: finish first pass of prettifying proofs | Andres Erbsen | 2015-11-11 |
* | BaseSystem: more prettyfication | Andres Erbsen | 2015-11-10 |
* | ModularBaseSystem: Implemented and proved subtraction, completing implementat... | Jade Philipoom | 2015-11-10 |
* | BaseSystem: implemented and proved subtraction. | Jade Philipoom | 2015-11-10 |
* | ModularBaseSystem: implemented fromGF and proved correct, moved inline admits... | Jade Philipoom | 2015-11-10 |
* | Merge of local changes and most recent changes in mit-plv master | Jade Philipoom | 2015-11-10 |
|\ |
|
* | | BaseSystem: added encode definition, included b0_1 precondition in BaseCoefs ... | Jade Philipoom | 2015-11-10 |
| * | BaseSystem: more boring | Andres Erbsen | 2015-11-10 |
| * | BaseSystem: more hints, more boring | Andres Erbsen | 2015-11-10 |
|/ |
|
* | ModularBaseSystem: finished most admits for addition and multiplication, move... | Jade Philipoom | 2015-11-09 |
* | ModularBaseSystem: proved addition and multiplication. | Jade Philipoom | 2015-11-07 |
* | BaseSystem: removed confusing notations and added mul_length lemma (currently... | Jade Philipoom | 2015-11-07 |
* | ModularBaseSystem: finish base_good | Andres Erbsen | 2015-11-07 |
* | ModularBaseSystem: prove some admits in mase system extension | Andres Erbsen | 2015-11-07 |
* | ModularBaseSystem: continuing to prove base_good. | Jade Philipoom | 2015-11-07 |
* | Merge branch 'master' of github.mit.edu:plv/fiat-crypto | Jade Philipoom | 2015-11-06 |
|\ |
|
* | | Starting to prove base_good in ModularBaseSystem | Jade Philipoom | 2015-11-06 |
| * | Specific: PseudoMersenneBaseParams for GF25519Base25Point5. | Andres Erbsen | 2015-11-06 |
| * | Merge remote-tracking branch 'jadep/master' | Andres Erbsen | 2015-11-06 |
| |\
| |/
|/| |
|
* | | ModularBaseSystem: finished proving all admits for reduce_rep; proved base_po... | Jade Philipoom | 2015-11-05 |
* | | Added lemmas to ListUtil and BaseSystem to help in ModularBaseSystem. | Jade Philipoom | 2015-11-05 |
* | | ModularBaseSystem: Implemented reduce and proved reduce_rep, currently workin... | Jade Philipoom | 2015-11-05 |
* | | ModularBaseSystem: defined an extended base system to represent unreduced pro... | Jade Philipoom | 2015-11-04 |
* | | Relocated boring tactic to ListUtil and added combine_truncate lemma. | Jade Philipoom | 2015-11-04 |
* | | Merge branch 'master' of github.mit.edu:plv/fiat-crypto | Jade Philipoom | 2015-11-03 |
|\| |
|
* | | ModularBaseSystem skeleton | Andres Erbsen | 2015-10-30 |
| * | BaseSystem to Util.ListUtil: separate out generic list lemmas | Andres Erbsen | 2015-10-29 |
| * | Merge branch 'master' of github.mit.edu:rsloan/fiat-crypto | Andres Erbsen | 2015-10-29 |
| |\ |
|
| * | | remove SearchAbouts | Andres Erbsen | 2015-10-28 |
* | | | BaseSystem: removed axiom b0_1. | Jade Philipoom | 2015-10-28 |
* | | | Merge branch 'master' into jade | Jade Philipoom | 2015-10-28 |
|\| | |
|
* | | | BaseSystem: proved all admits. | Jade Philipoom | 2015-10-28 |
| * | | Proof improvements in BaseSystem | Adam Chlipala | 2015-10-28 |
* | | | Proved add_same_length lemma. | Jade Philipoom | 2015-10-27 |
* | | | Multiply rep mostly proven, working on admits. | Jade Philipoom | 2015-10-27 |
| | * | patches for galois | Robert Sloan | 2015-10-27 |