diff options
Diffstat (limited to 'README.org')
-rw-r--r-- | README.org | 19 |
1 files changed, 19 insertions, 0 deletions
@@ -1,5 +1,24 @@ #+title: BitEQ #+author: Yann Herklotz +* BitEQ + Reasoning about bit equality for various rewrites. This is based on [[file:resources/samc.lisp][proofs]] done in ACL2, and uses the =bbv= library to convert the proofs into Coq. + +** 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. + +#+begin_src coq +Lemma mod_mod_pow_2 : + forall a p q, + 0 <= p <= q -> (a mod 2 ^ q) mod (2 ^ p) = a mod (2 ^ p). +#+end_src + +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. |