aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Add more interpretation thingsGravatar Jason Gross2016-11-03
* Fix buildGravatar Jason Gross2016-11-03
* More relatednessGravatar Jason Gross2016-11-03
* Make apply things go through interp_flat_typeGravatar Jason Gross2016-11-03
* Make apply things go through interp_flat_typeGravatar Jason Gross2016-11-03
* Versions of [Apply] that guarantee flat thingsGravatar Jason Gross2016-11-03
* Add more relatedness thingsGravatar Jason Gross2016-11-03
* Make [freeze] proofs consider machine integer width and hard input bounds sep...Gravatar jadep2016-11-03
* Fix bounds that were reversedGravatar Jason Gross2016-11-03
* Fix Not_found exception in 8.4Gravatar Jason Gross2016-11-03
* Clean up fe25519_word64ize, give examplesGravatar Jason Gross2016-11-02
* fix and prove ERepDec_correctGravatar Andres Erbsen2016-11-02
* add type-compatible SHA512 wrapperGravatar Andres Erbsen2016-11-02
* Fix divergence of Ltac match in 8.4Gravatar Jason Gross2016-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
* Work around divergence of unification in Coq 8.5{,pl1}Gravatar Jason Gross2016-11-02
* Write code to lift option types over tuplesGravatar 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
* GF25519BoundedCommon.v: require less higher order unification (8.4)Gravatar 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
* Fix bounds on neg in interpretationsGravatar Jason Gross2016-11-02
* Add ZUtil.Z.log2_ones_lt_nonnegGravatar Jason Gross2016-11-02
* Add more ZUtilGravatar Jason Gross2016-11-02
* Add ZUtil lemmaGravatar Jason Gross2016-11-02
* Add ZUtil lemmaGravatar Jason Gross2016-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
* Lift conversion correctness proofs to ModularBaseSystem by providing [pack_re...Gravatar jadep2016-11-02
* use correct version of WToZ_ZToW lemmaGravatar jadep2016-11-02
* fix lingering reference to old name of renamed lemmaGravatar jadep2016-11-02
* sqrt_correct reduced to a few admitsGravatar jadep2016-11-02
* Fix GF25519Bounded in a different wayGravatar Jason Gross2016-11-02
* Fix [sqrtW_sig]Gravatar Jason Gross2016-11-02
* Changes to sqrt for easier bounds proofs; currently blocked on broken proof i...Gravatar jadep2016-11-02
* Progress proving ERepDec_correct (included tweaking preconditions for Modular...Gravatar jadep2016-11-02
* Fixed reversed tuple in feDecGravatar jadep2016-11-02
* Add a ZUtil lemmaGravatar Jason Gross2016-11-02
* Prove fe25519WToZ_ZToW, rename FooToBarToFoo to BarToFoo_FooToBarGravatar Jason Gross2016-11-01
* Export strings in GF25519Reflective/CommonGravatar Jason Gross2016-11-01
* Fix and prove bounds for cmovne, cmovle; note a problem with the neg boundGravatar Jason Gross2016-11-01
* Print out the computed bounds on the various opsGravatar Jason Gross2016-11-01
* Parameterize bounded things over the limb lengthGravatar Jason Gross2016-11-01
* Add fe25519WToZToWGravatar Jason Gross2016-11-01
* Change hlist implicit statusGravatar Jason Gross2016-11-01
* Work around bug #5175 in 8.6Gravatar Jason Gross2016-11-01
* Move hlist to new fileGravatar Jason Gross2016-11-01
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 04:36:46 +0000