diff options
Diffstat (limited to 'README.md')
-rw-r--r-- | README.md | 28 |
1 files changed, 27 insertions, 1 deletions
@@ -1 +1,27 @@ -Reasoning about bit equality for various rewrites. This is based on [proofs](resources/samc.lisp) done in ACL2, and uses the `bbv` library to convert the proofs into Coq.
\ No newline at end of file +- [BitEQ](#orged8a59e) + - [Difficulties of using Coq for bitvector proofs](#orga4f0f39) + + + +<a id="orged8a59e"></a> + +# BitEQ + +Reasoning about bit equality for various rewrites. This is based on [proofs](resources/samc.lisp) done in ACL2, and uses the `bbv` library to convert the proofs into Coq. + + +<a id="orga4f0f39"></a> + +## Difficulties of using Coq for bitvector proofs + +The main difficulty of using Coq for bitvector proofs is that the standard library is missing many proofs about numbers that have the form `x mod 2 ^ y`. These are crucial for bitvector arithmetic, but have to all be manually proven. One example of such a proof is the following Lemma. + +```coq +Lemma mod_mod_pow_2 : + forall a p q, + 0 <= p <= q -> (a mod 2 ^ q) mod (2 ^ p) = a mod (2 ^ p). +``` + +This is true, but has to be proven manually in Coq. + +In addition to that, the automatic arithmetic solvers, such as `lia` or `nia` provided by Coq cannot deal with bitvector arithmetic either, so the proofs are quite manual in general.
\ No newline at end of file |