aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* simple refactor of makefile; commentsGravatar varomodt2016-01-09
* PointFormats: factor out admitsGravatar Andres Erbsen2016-01-08
* PointFormats: no zero denominators in Edwards additionGravatar Andres Erbsen2016-01-08
* PointFormats: addition produces points on curveGravatar Andres Erbsen2016-01-07
* fix field for division by constant (by dmz@mit.edu)Gravatar Andres Erbsen2016-01-07
* fix unverified typo in fermat proofGravatar Andres Erbsen2016-01-07
* Start writing PointFormats field proofsGravatar Andres Erbsen2016-01-07
* Merge branch 'specific-rewrite'Gravatar Andres Erbsen2016-01-06
|\
| * fix letify to only insert a term onceGravatar Andres Erbsen2016-01-06
* | Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar Jade Philipoom2016-01-05
|\ \
* | | Specific/EdDSA25519: created most of specific instantiation of EdDSA; still m...Gravatar Jade Philipoom2016-01-05
* | | PointFormats/EdDSA: scoping tweaks in PointFormats, small changes of phrasing...Gravatar Jade Philipoom2016-01-05
* | | Util: added util lemmas needed to instantiate EdDSA25519.Gravatar Jade Philipoom2016-01-05
| * | remove commentGravatar Andres Erbsen2016-01-04
| | * prettier GF25519 derivation that runs out of memoryGravatar Andres Erbsen2016-01-04
| | * UNTESTED simplification of specific GF25519 derivationGravatar Andres Erbsen2016-01-02
| |/
| * draft of Fermat's Little TheoremGravatar Andres Erbsen2015-12-31
|/
* 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
* 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 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 16:23:28 +0000