aboutsummaryrefslogtreecommitdiff
path: root/src/BoundedArithmetic/Interface.v
Commit message (Expand)AuthorAge
* 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 #5112 ([Arguments id /] broken)Gravatar Jason Gross2016-09-30
* 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