aboutsummaryrefslogtreecommitdiff
path: root/src/Spec/EdDSA.v
Commit message (Expand)AuthorAge
* Remove EdDSAGravatar Benjamin Barenblat2019-04-26
* Import prim token notations before using themGravatar Jason Gross2018-08-24
* minor updates needed to make it compile with bbvGravatar Samuel Gruetter2018-02-05
* ScalarMult: Z -> G -> G (closes #193)Gravatar Andres Erbsen2017-06-14
* rename-everythingGravatar Andres Erbsen2017-04-06
* use [positive] for [F] modulus, char_ge_C instead of char_gt_CGravatar Andres Erbsen2017-03-02
* alternative signing derivationGravatar Andres Erbsen2016-09-22
* Derive EdDSA.verify from equational specificationGravatar Andres Erbsen2016-09-16
* Fully qualify [Require]sGravatar Jason Gross2016-09-08
* added proofs about addition chain exponentiation for later use in ModularBase...Gravatar jadep2016-07-10
* scalarmult support; EdDSA.sign produces valid signaturesGravatar Andres Erbsen2016-06-27
* EdDSA: prove things about specGravatar Andres Erbsen2016-06-25
* EdDSA.Notations: indentationGravatar Andres Erbsen2016-06-22
* Handle renaming of NPeano.pow to Nat.pow (#3)Gravatar Jason Gross2016-06-22
* EdDSA.v: resolve ambiguity based on ed25519.pyGravatar Andres Erbsen2016-06-21
* Whitespace changeGravatar Jason Gross2016-06-21
* remove trailing whitespace from src/Gravatar Andres Erbsen2016-06-20
* port EdDSA specGravatar Andres Erbsen2016-06-20
* before changing SRep from N to F lGravatar Andres Erbsen2016-05-27
* Changed name of Encoding to CanonicalEncoding, and changed notation to match.Gravatar jadep2016-04-29
* consolidate and rename Edwards curve lemmasGravatar Andres Erbsen2016-04-25
* point_eq_decGravatar Andres Erbsen2016-04-22
* ed25519 derivation: pair programming with jgross... slow progressGravatar Andres Erbsen2016-03-24
* nicer verify() derivation starterGravatar Andres Erbsen2016-03-21
* Finish absolutizing importsGravatar Jason Gross2016-03-10
* Factor out some bedrock dependencies into WordUtilGravatar Jason Gross2016-02-25
* instantiated FqEncoding and FlEncoding (also fixed indentation, which is why ...Gravatar Jade Philipoom2016-02-15
* Spec/EdDSA: comments, remove prehashingGravatar Andres Erbsen2016-02-13
* Spec/EdDSA: cleanup; refactor lemmas to src/EdDSAProofs.vGravatar Andres Erbsen2016-02-13
* EdDSA spec ported over to new field implementationGravatar Jade Philipoom2016-02-13
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-07 11:12:00 +0000