| Commit message (Expand) | Author | Age |
|---|
| * | PointFOrmats,EdDSA: remove redundant axioms |  Andres Erbsen | 2016-01-16 |
| * | simple tactic rule |  Rob Sloan | 2016-01-11 |
| * | assumption lemmas in PointFormats | Rob Sloan | 2016-01-11 |
| * | simple refactor of makefile; comments |  varomodt | 2016-01-09 |
| * | PointFormats: factor out admits | Andres Erbsen | 2016-01-08 |
| * | fix field for division by constant (by dmz@mit.edu) | Andres Erbsen | 2016-01-07 |
| * | PointFormats/EdDSA: scoping tweaks in PointFormats, small changes of phrasing... |  Jade Philipoom | 2016-01-05 |
| * | Code-reviewing EdDSA |  Adam Chlipala | 2015-12-29 |
| * | PointFormats: wrote and proved equivalent a double-and-add implementation of ... | Jade Philipoom | 2015-12-20 |
| * | EdDSA: prettification of proofs; parameter l is now a nat instead of a Prime. | Jade Philipoom | 2015-12-17 |
| * | EdDSA: Proved verify_valid_passes and rewrote spec in terms of encoding typec... | Jade Philipoom | 2015-12-17 |
| * | rename fields for encodings | Andres Erbsen | 2015-12-15 |
| * | EdDSA: point encoding is a parameter | Andres Erbsen | 2015-12-15 |
| * | PointFormats: all Edwards25519 points are onCurve | Andres Erbsen | 2015-12-15 |
| * | another pass over the eddsa spec | Andres Erbsen | 2015-12-15 |
| * | EdDSA: mostly-complete spec and preliminary structure. | Jade Philipoom | 2015-12-12 |
| * | 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 |
Andres Erbsen
Rob Sloan
varomodt
Jade Philipoom
Adam Chlipala