aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/Ed25519.v
Commit message (Expand)AuthorAge
* unifiedAddM1Rep_sig: almost thereGravatar Andres Erbsen2016-05-18
* Moved sign_bit definition to Spec.Gravatar jadep2016-04-29
* Proved decode_point_eq in Ed25519 (comparing encodings is equivalent toGravatar jadep2016-04-29
* Completed encoding reorganization; factored sign_bit out of PointEncodings an...Gravatar jadep2016-04-28
* ed25519: solve elliptic curve math admitsGravatar Andres Erbsen2016-04-25
* consolidate and rename Edwards curve lemmasGravatar Andres Erbsen2016-04-25
* Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar jadep2016-04-25
|\
* | Reorganization and revision of Encoding code and redefinition of sign_bit fun...Gravatar jadep2016-04-25
| * refactor field lemmas out of ed25519Gravatar Andres Erbsen2016-04-25
| * reduce admits related to point negationGravatar Andres Erbsen2016-04-25
|/
* point_eq_decGravatar Andres Erbsen2016-04-22
* ed25519 derivation: down to final encodingGravatar Andres Erbsen2016-04-17
* ed25519 derivation: use representation of FGravatar Andres Erbsen2016-04-17
* ed25519 derivation: wrangle non-unique representationsGravatar Andres Erbsen2016-04-16
* ed25519 derivation: stuck at main loopGravatar Andres Erbsen2016-04-16
* ed25519 derivation down to word until main equationGravatar Andres Erbsen2016-04-16
* Retrieved updated version of Util/IterAssocOp and modified ExtendedCoordinate...Gravatar jadep2016-04-14
* Fixed syntax error (missing bracket) in Ed25519 to make merge buildGravatar jadep2016-04-12
* ed25519: continue derivationGravatar Andres Erbsen2016-04-08
* Drop second projections in Ed25519Gravatar Jason Gross2016-03-29
* ed25519 derivation: pair programming with jgross... slow progressGravatar Andres Erbsen2016-03-24
* nicer verify() derivation starterGravatar Andres Erbsen2016-03-21
* state top-level derivation for Ed25519.verifyGravatar Andres Erbsen2016-03-20