BitEQ

Reasoning about bit equality for various rewrites. This is based on 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.

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.