aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments/Ed25519.v
Commit message (Expand)AuthorAge
* framework for l_order_BGravatar Andres Erbsen2016-10-30
* proved feSign_correctGravatar jadep2016-10-29
* proved Proper_feSignGravatar jadep2016-10-29
* prove Proper_SRepERepMulGravatar Andres Erbsen2016-10-29
* proved last admit (Proper_feEnc) in Experiments/Ed25519Gravatar jadep2016-10-27
* proved an admit (eq_enc_S_iff) in Ed25519.vGravatar jadep2016-10-27
* removed now irrelevant commented-out codeGravatar jadep2016-10-27
* convert feEnc correctness proof to bounded typeGravatar jadep2016-10-27
* finished feEnc correctnessGravatar jadep2016-10-27
* most of feEnc correctness proofGravatar jadep2016-10-27
* removed lingering TODOGravatar jadep2016-10-27
* Fix for Coq 8.4 (f_equiv changed behavior)Gravatar Jason Gross2016-10-26
* Initial work on filling ed25519 with bounded thingsGravatar Jason Gross2016-10-25
* prove SRepMul admitGravatar Andres Erbsen2016-10-25
* Proved homomorphism between curve groups (Twisted Edwards Curve representatio...Gravatar jadep2016-10-24
* Freeze before packing to get canonical encodingsGravatar jadep2016-10-24
* ed25519: prove some admitsGravatar Andres Erbsen2016-10-24
* Modify point_phi (from PointEncodings) to use ref_phiGravatar jadep2016-10-23
* Fix a typoGravatar Jason Gross2016-10-23
* Prove onCurve_ERepBGravatar Jason Gross2016-10-23
* Finish twedprm_ERep proofGravatar Jason Gross2016-10-23
* Made field-element encodings canonicalize elements before encoding themGravatar jadep2016-10-22
* Fix src/Experiments/Ed25519.v for Coq 8.4Gravatar Jason Gross2016-10-22
* final touches/fixes for freeze restructuringGravatar jadep2016-10-22
* extraction: use more Haskell functionsGravatar Andres Erbsen2016-10-21
* fiddle with [rewrite <-!(field_div_definition)], maybe fix buildGravatar Andres Erbsen2016-10-21
* Edwards.Extended.to_twisted: only one inversion, improve extractionGravatar Andres Erbsen2016-10-21
* Fix build failureGravatar Jason Gross2016-10-21
* extraction of [sign] using Haskell [Integer]s for limbsGravatar Andres Erbsen2016-10-21
* Fill in some things in Ed25519 from SC25519Gravatar Jason Gross2016-10-19
* Fix for change in precedence of <-> vs -> in 8.4/8.5Gravatar Jason Gross2016-10-19
* Work around out of memory error in 8.5, 8.5pl1Gravatar Jason Gross2016-10-18
* Fix for 8.4 unification being unhappy in Ed25519 (nats are terrible)Gravatar Jason Gross2016-10-17
* Various Ed25519 8.4 fixesGravatar Jason Gross2016-10-17
* refactor scalar multiplication thoery, implement SRepERepMulGravatar Andres Erbsen2016-10-12
* Fixed naming issueGravatar jadep2016-10-12
* defined sign operation on field elementsGravatar jadep2016-10-12
* Fixing merge conflictGravatar jadep2016-10-12
* integrate bitwise operationsGravatar Andres Erbsen2016-10-12
* Add Ed25519 to _CoqProjectGravatar Jason Gross2016-10-12
* Starting to fill in Ed25519 context variablesGravatar jadep2016-10-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 11:27:34 +0000