aboutsummaryrefslogtreecommitdiff
path: root/src/BoundedArithmetic/ArchitectureToZLike.v
Commit message (Expand)AuthorAge
* Split up DoubleBoundedProofs, add proofsGravatar Jason Gross2016-10-07
* 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
* Rework bounded proofsGravatar 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
* 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