# 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.


## 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.