aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* Util: added util lemmas needed to instantiate EdDSA25519.Gravatar Jade Philipoom2016-01-05
* Code-reviewing EdDSAGravatar Adam Chlipala2015-12-29
* PointFormats : removed reliance on Pos.size_nat; doubleAndAdd now takes an ar...Gravatar Jade Philipoom2015-12-28
* PointFormats : changed iter_op to allow overestimating bitlength of argument.Gravatar Jade Philipoom2015-12-26
* Removed OpWithZero typeclass in favor of explicit arguments.Gravatar Jade Philipoom2015-12-25
* 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
* PointFormats: wrote and proved equivalent a double-and-add implementation of ...Gravatar Jade Philipoom2015-12-20
* 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 typec...Gravatar Jade Philipoom2015-12-17
* 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 p...Gravatar Jade Philipoom2015-12-07
* 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 2^2...Gravatar Andres Erbsen2015-12-05
* Specific/GF25519: explicit formula for multiplicationGravatar Andres Erbsen2015-12-05
* GF25519: synthesize explicit formula for multiplication (no reduction yet)Gravatar Andres Erbsen2015-12-05
* 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 carries...Gravatar Jade Philipoom2015-11-24
* 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
* 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 carry_r...Gravatar Jade Philipoom2015-11-17
* 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 implementat...Gravatar Jade Philipoom2015-11-10
* BaseSystem: implemented and proved subtraction.Gravatar Jade Philipoom2015-11-10
* ModularBaseSystem: implemented fromGF and proved correct, moved inline admits...Gravatar Jade Philipoom2015-11-10
* 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
| * BaseSystem: more boringGravatar Andres Erbsen2015-11-10
| * BaseSystem: more hints, more boringGravatar Andres Erbsen2015-11-10
|/
* ModularBaseSystem: finished most admits for addition and multiplication, move...Gravatar Jade Philipoom2015-11-09
* ModularBaseSystem: proved addition and multiplication.Gravatar Jade Philipoom2015-11-07
* BaseSystem: removed confusing notations and added mul_length lemma (currently...Gravatar Jade Philipoom2015-11-07
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 07:55:37 +0000