aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments
Commit message (Expand)AuthorAge
* Generalize add_coordinatesGravatar Jason Gross2016-11-17
* Support for 128-bit wordsGravatar Jason Gross2016-11-14
* extraction: inline field operations into group operationsGravatar Andres Erbsen2016-11-14
* Add mulW_noinlineGravatar Jason Gross2016-11-14
* Proper_sqrtGravatar Andres Erbsen2016-11-13
* Remove extra admitted lemmas in 8.4Gravatar Jason Gross2016-11-12
* GF25519: add ErepAddGravatar Andres Erbsen2016-11-11
* [cbn] is 8.5 onlyGravatar Jason Gross2016-11-11
* Fix proofs broken by stronger preconditionsGravatar Jason Gross2016-11-11
* Most of the admits in Ed25519.vGravatar Rob Sloan2016-11-11
* extraction less slowGravatar Andres Erbsen2016-11-11
* Work around looping in 8.4Gravatar Jason Gross2016-11-10
* Rewrite cast_word so that it's extracted betterGravatar Jason Gross2016-11-09
* implement X25519Gravatar Andres Erbsen2016-11-06
* move B_order_l and prime_qGravatar Andres Erbsen2016-11-06
* Connect [is_bounded] to [bounded_by]Gravatar Jason Gross2016-11-06
* Work around a bug in 8.4 vm_computeGravatar Jason Gross2016-11-05
* put EdDSA encoding sign bit at the MSBGravatar Andres Erbsen2016-11-04
* fix extraction directives -- tested enc((l+1)B)=enc(B)Gravatar Andres Erbsen2016-11-03
* separate Ed25519Extraction.v, add extraction to MakefileGravatar Andres Erbsen2016-11-03
* fix Word64 constants for extraction, check in more extraction directivesGravatar Andres Erbsen2016-11-03
* Make [freeze] proofs consider machine integer width and hard input bounds sep...Gravatar jadep2016-11-03
* fix and prove ERepDec_correctGravatar Andres Erbsen2016-11-02
* Fix diverging Qed in 8.5{,pl1} ([f_equal] is broken)Gravatar Jason Gross2016-11-02
* Fix broken proofGravatar Jason Gross2016-11-02
* Fix a possibly-diverging Qed in 8.4 (feEnc_correct)Gravatar Jason Gross2016-11-02
* Ed25519: use fully qualified names for [a] and [d]Gravatar Andres Erbsen2016-11-02
* almost fix Ed25519 for 8.4Gravatar Andres Erbsen2016-11-02
* even less fragile proofsGravatar Andres Erbsen2016-11-02
* improve some fragile proofs (built on 8.4)Gravatar Andres Erbsen2016-11-02
* Proved feDec_correct modulo a few admits about ZGravatar jadep2016-11-02
* feDec_correct in progress, fully converted to Z operationsGravatar jadep2016-11-02
* use correct version of WToZ_ZToW lemmaGravatar jadep2016-11-02
* sqrt_correct reduced to a few admitsGravatar jadep2016-11-02
* Progress proving ERepDec_correct (included tweaking preconditions for Modular...Gravatar jadep2016-11-02
* Fixed reversed tuple in feDecGravatar jadep2016-11-02
* Parameterize bounded things over the limb lengthGravatar Jason Gross2016-11-01
* Add some interpretations things, speed up proofs in Ed25519Gravatar Jason Gross2016-10-31
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-16 16:32:02 +0000