aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments/Ed25519.v
Commit message (Expand)AuthorAge
* Remove everything after the individual reified opsGravatar Jason Gross2017-04-03
* move large non-building chunks of Ed25519.vGravatar Andres Erbsen2017-03-02
* Switch to fully uncurried form for reflectionGravatar Jason Gross2017-03-01
* Removed code that will be completely replaced in the future; replaced some po...Gravatar jadep2017-02-22
* move lemmas from Ed25519 to WordUtilGravatar jadep2017-02-22
* move some lemmas from Ed25519 to ZUtilGravatar jadep2017-02-22
* moved more stuff to NUtilGravatar jadep2017-02-22
* Moved N lemmas from Ed25519 and IterAssocOp into new NUtil fileGravatar jadep2017-02-22
* categorize the rest of the stuff in Ed25519Gravatar jadep2017-02-22
* categorize some of the stuff in Ed25519Gravatar jadep2017-02-22
* Fix changed namesGravatar Jason Gross2017-02-03
* Generalize add_coordinatesGravatar Jason Gross2016-11-17
* 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
* Work around looping in 8.4Gravatar Jason Gross2016-11-10
* 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
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-20 05:27:28 +0000