From 2c73988a36d94b81c8b49b283f50ff463fc63342 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 5 Mar 2022 14:21:42 +0000 Subject: Add to the README --- README.md | 28 +++++++++++++++++++++++++++- README.org | 19 +++++++++++++++++++ 2 files changed, 46 insertions(+), 1 deletion(-) 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) + + + + + +# 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. \ 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. -- cgit