blob: 8d8e3701eeedde1fcf55e92c82748a77772e3a4c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
#+title: BitEQ
#+author: Yann Herklotz
#+options: toc:nil
* 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.
|
