aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Fix shiftr_spec_fullGravatar Jason Gross2016-10-09
* Add more to Ztestbit_fullGravatar Jason Gross2016-10-09
* Add a Ztestbit_full databaseGravatar Jason Gross2016-10-09
* Some work on x86 and bounded repeated thingsGravatar Jason Gross2016-10-09
* Add some bounded decode/and thingsGravatar Jason Gross2016-10-09
* Split up DoubleBoundedProofs, add proofsGravatar Jason Gross2016-10-07
* Stronger Ztestbit, convert_to_ztestbitGravatar Jason Gross2016-10-07
* More zsimplify lemmas, stronger ZtestbitGravatar Jason Gross2016-10-07
* Add eta_expand to Prod.vGravatar Jason Gross2016-10-07
* Add a variant of [map] on reflective things that changes the interp functionGravatar Jason Gross2016-10-07
* Weaken hyps of lor_range, add it to zarithGravatar Jason Gross2016-10-07
* Moved lemma to ZUtil and added an extra lemma jgross neededGravatar jadep2016-10-06
* Add testbit_add_shiftl_fullGravatar Jason Gross2016-10-06
* Use zutil_arith for side-conditions in testbitGravatar Jason Gross2016-10-06
* Add Z.pow_le_mono_{r,l} to zarithGravatar Jason Gross2016-10-06
* Add a lemma to Ztestbit about large indicesGravatar Jason Gross2016-10-06
* Do shl, shr doubling in terms of orGravatar Jason Gross2016-10-06
* Add more bounded assembly lemmasGravatar Jason Gross2016-10-06
* Moved PointEncoding out of SpecGravatar jadep2016-10-06
* Fixed a lingering inappropriate use of Logic.eqGravatar jadep2016-10-06
* Moved conversion logic out of Pow2BaseProofs into its own fileGravatar jadep2016-10-06
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-30 17:43:16 +0000