aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/Ed25519.v
Commit message (Expand)AuthorAge
* Merge branch 'field-experiment'Gravatar Andres Erbsen2016-06-20
|\
* | Another fix for an anomaly in 8.4pl2Gravatar Jason Gross2016-06-11
| * ed25519: refactor some ProperGravatar Andres Erbsen2016-06-06
| * rewrite in Let_In binder by tacticGravatar Andres Erbsen2016-06-04
| * Let_In rewritingGravatar Andres Erbsen2016-06-03
| * leibniz equal version of topdown rewriting of sigma types: nicerGravatar Andres Erbsen2016-06-01
| * leibniz equal version of topdown rewriting of sigma typesGravatar Andres Erbsen2016-06-01
| * E impl: proper morphisms are hard to dow without setoidsGravatar Andres Erbsen2016-05-30
| * ERep addGravatar Andres Erbsen2016-05-29
| * --amendGravatar Andres Erbsen2016-05-28
| * verify derivation, EdDSA layer: allow arbitrary equivalence relation for ERep...Gravatar Andres Erbsen2016-05-28
| * verify derivation, EdDSA layer: remove unused context variablesGravatar Andres Erbsen2016-05-28
| * verify derivation: EdDSA layerGravatar Andres Erbsen2016-05-28
| * right after scalars to F lGravatar Andres Erbsen2016-05-27
| * before changing SRep from N to F lGravatar Andres Erbsen2016-05-27
|/
* ed25519: indentation fixGravatar Andres Erbsen2016-05-24
* ed25519: integrate FRepPow and FRepInvGravatar Andres Erbsen2016-05-24
* ed25519: continue refactorGravatar Andres Erbsen2016-05-24
* Factor some rewrites into a single [autorewrite]Gravatar Jason Gross2016-05-24
* Remove unfolding, rewrite -> setoid_rewriteGravatar Jason Gross2016-05-24
* Fix some issues in Ed25519 tacticsGravatar Jason Gross2016-05-24
* F,Ed25519: integrate F representation for mul,add,sub. Ed25519 even more brok...Gravatar Andres Erbsen2016-05-24
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 16:46:44 +0000