aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* More zsimplify lemmasGravatar Jason Gross2016-10-04
* Add Zplus_minus to zsimplifyGravatar Jason Gross2016-10-04
* Weaken hyps of zutil lemmaGravatar Jason Gross2016-10-04
* Add a variant of add_shift_modGravatar Jason Gross2016-10-04
* Add some doubling constructions to bounded arithGravatar Jason Gross2016-10-04
* Add ZUtil lemmaGravatar Jason Gross2016-10-04
* Add ZUtil lemmaGravatar Jason Gross2016-10-04
* Add Zmult_lt_compat_r to zarithGravatar Jason Gross2016-10-04
* Prevent infinite loops by not dealing with 0 mod _Gravatar Jason Gross2016-10-04
* Handle 0 mod _ in push_ZmodGravatar Jason Gross2016-10-04
* Handle ?x mod ?x in push_ZmodGravatar Jason Gross2016-10-04
* Add some more instructionsGravatar Jason Gross2016-10-04
* Z.ltb_to_lt now also handles eqbGravatar Jason Gross2016-10-04
* Add instructions with carry flagsGravatar Jason Gross2016-10-04
* Add spec for x86 (#72)Gravatar Jason Gross2016-10-04
* fix 8.4 buildGravatar jadep2016-10-03
* A couple hotfixes; recent commits somehow broke thingsGravatar jadep2016-10-03
* Wrote proofs necessary to fill in all point-encoding related context variable...Gravatar jadep2016-10-03
* Add bitwise and, remove mkl from fancyGravatar Jason Gross2016-10-03
* Work around bug 5107 (broken return inference)Gravatar Jason Gross2016-10-03
* Work around bug #5112 ([Arguments id /] broken)Gravatar Jason Gross2016-10-03
* Ed25519: use Global InstanceGravatar Andres Erbsen2016-10-03
* Spec: add ed25519Gravatar Andres Erbsen2016-10-03
* Fix a spelling typoGravatar Jason Gross2016-10-02
* Add homomorphism compositionGravatar Jason Gross2016-09-30
* Add group and homomorphism lemmasGravatar Jason Gross2016-09-30
* Weaken surjective_homomorphism_from_groupGravatar Jason Gross2016-09-30
* Work around bug #5112 ([Arguments id /] broken)Gravatar Jason Gross2016-09-30
* Silence warnings about Require in GenericFieldPowGravatar Jason Gross2016-09-30
* More map -> List.mapGravatar Jason Gross2016-09-29
* map -> List.map (not Tuple.map)Gravatar Jason Gross2016-09-29
* Add Tuple.mapGravatar Jason Gross2016-09-29
* Small example of bounds-calculation with dependent types (#61)Gravatar Jason Gross2016-09-29
* montgomery-curveGravatar Andres Erbsen2016-09-28
* Merge pull request #69 from JasonGross/scalable-scalarsGravatar Jason Gross2016-09-26
|\
| * Add a comment with an exampleGravatar Jason Gross2016-09-26
* | MxDH: do not depend on implicit import of list notationsGravatar Andres Erbsen2016-09-26
* | add Montgomery x-coordinate Diffie-Hellman and Curve25519Gravatar Andres Erbsen2016-09-26
* | Finished remaining admits in [freeze] proofsGravatar jadep2016-09-23
| * Drop CSE from Fancy MachineGravatar Jason Gross2016-09-22
| * Use dlet, not lletGravatar Jason Gross2016-09-22
| * Fix for Coq < 8.6Gravatar Jason Gross2016-09-22
| * Don't inline everything in Montgomery and BarrettGravatar Jason Gross2016-09-22
| * Make use of named syntax, do reg assign for fancyGravatar Jason Gross2016-09-22
| * Add dead code eliminationGravatar Jason Gross2016-09-22
| * Add a non-higher-order syntax, and reg assignmentGravatar Jason Gross2016-09-22
|/
* Revert "Add a locked version of [let] with fewer reductions"Gravatar Jason Gross2016-09-22
* Revert "Update _CoqProject"Gravatar Jason Gross2016-09-22
* Revert "Fix LockedLet"Gravatar Jason Gross2016-09-22
* Fix a typoGravatar Jason Gross2016-09-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 15:55:04 +0000