aboutsummaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* PointFormats: completed remaining admits for non-destruction doubleAndAdd.Gravatar Jade Philipoom2015-12-24
|
* PointFormats: implemented doubleAndAdd without destructing scalar and proved ↵Gravatar Jade Philipoom2015-12-24
| | | | equivalence with scalarMult; several small admits remain.
* PointFormats: wrote and proved equivalent a double-and-add implementation of ↵Gravatar Jade Philipoom2015-12-20
| | | | scalar-point multiplication; standardized EdDSA to use nat instead of Z.
* EdDSA: prettification of proofs; parameter l is now a nat instead of a Prime.Gravatar Jade Philipoom2015-12-17
|
* EdDSA: Proved verify_valid_passes and rewrote spec in terms of encoding ↵Gravatar Jade Philipoom2015-12-17
| | | | typeclasses.
* rename fields for encodingsGravatar Andres Erbsen2015-12-15
|
* EdDSA: point encoding is a parameterGravatar Andres Erbsen2015-12-15
|
* PointFormats: all Edwards25519 points are onCurveGravatar Andres Erbsen2015-12-15
|
* another pass over the eddsa specGravatar Andres Erbsen2015-12-15
|
* EdDSA: mostly-complete spec and preliminary structure.Gravatar Jade Philipoom2015-12-12
|
* Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar Jade Philipoom2015-12-10
|\
* | More improved structure for EdDSA and PointFormats.Gravatar Jade Philipoom2015-12-10
| |
* | More refacoring PointFormats.Gravatar Jade Philipoom2015-12-09
| |
* | Rewrote PointFormats to be parameterized by modulus; reformatting of EdDSA.Gravatar Jade Philipoom2015-12-09
| |
| * Remove redundancy in lemma statementGravatar Adam Chlipala2015-12-09
|/
* EdDSA: Added PointFormatsSpec module type (possibly temporary). Transcribed ↵Gravatar Jade Philipoom2015-12-07
| | | | public key generation.
* Transcribed EdDSA parameters from [https://eprint.iacr.org/2015/677.pdf].Gravatar Jade Philipoom2015-12-07
|
* GaloisTheory: prove 4 trivial admits. GF25519 only assumption is now that ↵Gravatar Andres Erbsen2015-12-05
| | | | 2^255-19 is prime.
* Specific/GF25519: explicit formula for multiplicationGravatar Andres Erbsen2015-12-05
|
* GF25519: synthesize explicit formula for multiplication (no reduction yet)Gravatar Andres Erbsen2015-12-05
|
* Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar Jade Philipoom2015-11-29
|\
* | Added roadmap of long term goals and current subtasks.Gravatar Jade Philipoom2015-11-29
| |
| * scalar multiplicationGravatar Andres Erbsen2015-11-25
|/
* reorganized lemmas; moved several to ListUtil and ZUtil.Gravatar Jade Philipoom2015-11-24
|
* ModularBaseSystem: added definition to perform a specific sequence of ↵Gravatar Jade Philipoom2015-11-24
| | | | carries and proved that it preserves GF representation.
* Specific/GF25519: Updated to match new PseudoMersenneBaseParams spec.Gravatar Jade Philipoom2015-11-24
|
* ModularBaseSystem: relocated base_succ to PsuedoMersenneBaseParams, proved ↵Gravatar Jade Philipoom2015-11-20
| | | | carry_rep.
* Added base_succ precondition to BaseSystem to help prove carrying.Gravatar Jade Philipoom2015-11-19
|
* ModularBaseSystem: proving reduce case of carry_rep.Gravatar Jade Philipoom2015-11-18
|
* ModularBaseSystem: carry_rep has boring modular arithmetic proofsGravatar Andres Erbsen2015-11-17
|
* ModularBaseSystem: introduced lemmas about breaking lists; working on ↵Gravatar Jade Philipoom2015-11-17
| | | | carry_rep_reduce.
* ModularBaseSystem.carry: implement, state lemmas, some progress on proofsGravatar Andres Erbsen2015-11-17
|
* BaseSystem: finish first pass of prettifying proofsGravatar Andres Erbsen2015-11-11
|
* BaseSystem: more prettyficationGravatar Andres Erbsen2015-11-10
|
* ModularBaseSystem: Implemented and proved subtraction, completing ↵Gravatar Jade Philipoom2015-11-10
| | | | implementation of GFrep interface.
* BaseSystem: implemented and proved subtraction.Gravatar Jade Philipoom2015-11-10
|
* ModularBaseSystem: implemented fromGF and proved correct, moved inline ↵Gravatar Jade Philipoom2015-11-10
| | | | admits about inject to GaloisTheory.
* Merge of local changes and most recent changes in mit-plv masterGravatar Jade Philipoom2015-11-10
|\
* | BaseSystem: added encode definition, included b0_1 precondition in BaseCoefs ↵Gravatar Jade Philipoom2015-11-10
| | | | | | | | (first element of base is 1).
| * BaseSystem: more boringGravatar Andres Erbsen2015-11-10
| |
| * BaseSystem: more hints, more boringGravatar Andres Erbsen2015-11-10
|/
* ModularBaseSystem: finished most admits for addition and multiplication, ↵Gravatar Jade Philipoom2015-11-09
| | | | moved some lemmas to ListUtil.
* ModularBaseSystem: proved addition and multiplication.Gravatar Jade Philipoom2015-11-07
|
* BaseSystem: removed confusing notations and added mul_length lemma ↵Gravatar Jade Philipoom2015-11-07
| | | | (currently admitted).
* ModularBaseSystem: finish base_goodGravatar Andres Erbsen2015-11-07
|
* ModularBaseSystem: prove some admits in mase system extensionGravatar Andres Erbsen2015-11-07
|
* ModularBaseSystem: continuing to prove base_good.Gravatar Jade Philipoom2015-11-07
|
* Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar Jade Philipoom2015-11-06
|\
* | Starting to prove base_good in ModularBaseSystemGravatar Jade Philipoom2015-11-06
| |
| * Specific: PseudoMersenneBaseParams for GF25519Base25Point5.Gravatar Andres Erbsen2015-11-06
| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 05:52:13 +0000