aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* 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
* Fix a typo in the previous commitGravatar Jason Gross2016-11-01
* Generalize hlistGravatar Jason Gross2016-11-01
* Add hlist to tupleGravatar Jason Gross2016-11-01
* Make it easier to extract word64Gravatar Jason Gross2016-10-31
* Add version of [Apply] for [Interp] thingsGravatar Jason Gross2016-10-31
* Add bounds type in Specific/GF25519Reflective/Common.vGravatar Jason Gross2016-10-31
* Add Reflection.ApplicationGravatar Jason Gross2016-10-31
* Add SmartVarMap_heteroGravatar Jason Gross2016-10-31
* Add some interpretations things, speed up proofs in Ed25519Gravatar Jason Gross2016-10-31
* Add [f] to things that use [exprf] or [flat_type]Gravatar Jason Gross2016-10-31
* Implicits for SmartVarMapTGravatar Jason Gross2016-10-31
* Make it so that changing the list of wire bounds doesn't break the buildGravatar Jason Gross2016-10-31
* Add SmartVarMapTGravatar Jason Gross2016-10-31
* Revert "Switch from word to Z"Gravatar Jason Gross2016-10-31
* Switch from word to ZGravatar Jason Gross2016-10-31
* Switch to reflective bounded word in Ed25519Gravatar Jason Gross2016-10-31
* Safer definitions of shl, shrGravatar Jason Gross2016-10-31
* Fix a typo making word calculations wrongGravatar Jason Gross2016-10-31
* Use sigma types to fix extractionGravatar Jason Gross2016-10-31
* Silence a warningGravatar Jason Gross2016-10-31
* Significantly faster wordToN, I hopeGravatar Jason Gross2016-10-31
* Add src/Specific/GF25519Reflective.vGravatar Jason Gross2016-10-31
* Interpret syntax with Let_InGravatar Jason Gross2016-10-31
* Also construct relatedness proofs in reifiedGravatar Jason Gross2016-10-30
* Fix tactic notation scope in the 8.5 buildGravatar Jason Gross2016-10-30
* Fix for 8.5 build?Gravatar Jason Gross2016-10-30
* Proved eq_enc_E_iffGravatar jadep2016-10-30
* Fix some subtleties with equalities in point encodingsGravatar jadep2016-10-30
* Added new algebra lemmaGravatar jadep2016-10-30
* Remove an [About]Gravatar Jason Gross2016-10-30
* Renaming in Reflection/Z/Interpretations.v, admitted rel lemmasGravatar Jason Gross2016-10-30
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 20:06:33 +0000