| 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 |