Add to the README

2 files changed, 46 insertions, 1 deletions

diff --git a/README.md b/README.md
index f73dbfa..5595e45 100644
--- a/README.md
+++ b/README.md
@@ -1 +1,27 @@
-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.
\ No newline at end of file
+- [BitEQ](#orged8a59e)
+  - [Difficulties of using Coq for bitvector proofs](#orga4f0f39)
+
+
+
+<a id="orged8a59e"></a>
+
+# 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.
+
+
+<a id="orga4f0f39"></a>
+
+## 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.
\ No newline at end of file
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.