aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Collapse)AuthorAge
* NumTheoryUtil: proved Fermat's Little Theorem.Gravatar Jade Philipoom2016-01-23
|
* NumTheoryUtil : code cleanup; moved some lemmas to ZUtil.Gravatar Jade Philipoom2016-01-23
|
* Import coqprime; use it to prove Euler's criterion.Gravatar Jade Philipoom2016-01-20
|
* PointFOrmats,EdDSA: remove redundant axiomsGravatar Andres Erbsen2016-01-16
|
* remove duplicate axiomGravatar Andres Erbsen2016-01-16
|
* PointFormats: extended coordinates equivalence proofsGravatar Andres Erbsen2016-01-16
|
* fix merge conflicts + PointFormats proofsGravatar Robert Sloan2016-01-14
|\
| * Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar Jade Philipoom2016-01-13
| |\
| * | euler's criterion reduced to fermat's little theorem and two lemmas about ↵Gravatar Jade Philipoom2016-01-13
| | | | | | | | | | | | primitive roots.
* | | simple tactic ruleGravatar Rob Sloan2016-01-11
| | |
* | | assumption lemmas in PointFormatsGravatar Rob Sloan2016-01-11
| | |
* | | simple refactor of makefile; commentsGravatar varomodt2016-01-09
| | |
| | * cleanupGravatar Andres Erbsen2016-01-08
| |/ |/|
* | 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 ↵Gravatar Jade Philipoom2016-01-05
| | | | | | | | | | | | missing parameters d, H, l, B, and PointEncoding.
* | | PointFormats/EdDSA: scoping tweaks in PointFormats, small changes of ↵Gravatar Jade Philipoom2016-01-05
| | | | | | | | | | | | phrasing in EdDSA to make proofs more convenient.
* | | 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 ↵Gravatar Jade Philipoom2015-12-28
| | | | argument that serves as an upper bound on bit length.
* 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
| | | | 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
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-24 20:57:31 +0000