Add to the README

1 files changed, 19 insertions, 0 deletions

diff --git a/README.org b/README.org
index cba18aa..9730dd9 100644
--- a/README.org
+++ b/README.org
@@ -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.