aboutsummaryrefslogtreecommitdiff
path: root/src/BoundedArithmetic
Commit message (Expand)AuthorAge
* Actually fix the exponential blowup (hopefully)Gravatar Jason Gross2016-10-14
* Fix a typo in the previous commitGravatar Jason Gross2016-10-14
* Fix exponential blowup in some doubling opsGravatar Jason Gross2016-10-14
* Work around bug 5401 (bad let '(x, y))Gravatar Jason Gross2016-10-13
* Revert "Eta-expand pairs in Eta.v"Gravatar Jason Gross2016-10-13
* Eta-expand pairs in Eta.vGravatar Jason Gross2016-10-13
* Unfold more things in etaGravatar Jason Gross2016-10-13
* Add src/BoundedArithmetic/Eta.vGravatar Jason Gross2016-10-13
* Fix for missing Nat.log2 in 8.4Gravatar Jason Gross2016-10-11
* Fix for missing Nat.log2 in 8.4Gravatar Jason Gross2016-10-11
* Add some admitted x86->ZLike proofsGravatar Jason Gross2016-10-10
* Work around bug 5003 (broken omega on projections)Gravatar Jason Gross2016-10-10
* Add definitions for x86Gravatar Jason Gross2016-10-10
* Add repeated multipleGravatar Jason Gross2016-10-10
* Add shl,shr,shrd to repeated doublingGravatar Jason Gross2016-10-09
* Add proofs for doubling shl,shr,shrdGravatar 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
* Add testbit_add_shiftl_fullGravatar 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
* Add some doubling constructions to bounded arithGravatar Jason Gross2016-10-04
* Add some more instructionsGravatar Jason Gross2016-10-04
* Add instructions with carry flagsGravatar Jason Gross2016-10-04
* Add spec for x86 (#72)Gravatar Jason Gross2016-10-04
* 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
* Work around bug #5112 ([Arguments id /] broken)Gravatar Jason Gross2016-09-30
* More map -> List.mapGravatar Jason Gross2016-09-29
* Add a comment with an exampleGravatar Jason Gross2016-09-26
* Drop CSE from Fancy MachineGravatar Jason Gross2016-09-22
* Use dlet, not lletGravatar Jason Gross2016-09-22
* Don't inline everything in Montgomery and BarrettGravatar Jason Gross2016-09-22
* Integrate suggestions from AndresGravatar Jason Gross2016-08-25
* Rework bounded proofsGravatar Jason Gross2016-08-24
* More slight cleanupsGravatar Jason Gross2016-08-24
* Clean up DoubleBoundedGravatar Jason Gross2016-08-24
* Coq 8.4 fixesGravatar Jason Gross2016-08-24
* Weaken the condition on smaller_boundGravatar Jason Gross2016-08-23
* Hook up the bounded interface, finish proofsGravatar Jason Gross2016-08-23
* Revert "Add _valid properties"Gravatar Jason Gross2016-08-23
* Add _valid propertiesGravatar Jason Gross2016-08-23
* Fix some thingsGravatar Jason Gross2016-08-23
* Add TODOGravatar Jason Gross2016-08-23
* Rework interface to support rewriting databaseGravatar Jason Gross2016-08-23
* alternative machine interface specification proposalGravatar Andres Erbsen2016-08-23
* Initial work on an architecture interface for ℤ/nℤGravatar Jason Gross2016-08-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-10 07:49:22 +0000