aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments
Commit message (Expand)AuthorAge
...
* Switch to reflective bounded word in Ed25519Gravatar Jason Gross2016-10-31
* Use sigma types to fix extractionGravatar Jason Gross2016-10-31
* Proved eq_enc_E_iffGravatar jadep2016-10-30
* 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
* Merge branch 'master' into instantiation-rsloan-phoasGravatar Jason Gross2016-10-20
|\
| * 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
| * remove Experiments.EncodingLemmas (superseded by Jade's recent work)Gravatar Andres Erbsen2016-10-12
| * Add Ed25519 to _CoqProjectGravatar Jason Gross2016-10-12
| * Starting to fill in Ed25519 context variablesGravatar jadep2016-10-10
* | Merge _CoqProjectGravatar Rob Sloan2016-10-06
|\ \ | |/ |/|
* | Silence warnings about Require in GenericFieldPowGravatar Jason Gross2016-09-30
* | montgomery-curveGravatar Andres Erbsen2016-09-28
| * Fix merge with masterGravatar Robert Sloan2016-09-24
| |\ | |/ |/|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 19:38:26 +0000