diff options
author | Yann Herklotz <git@yannherklotz.com> | 2022-03-05 14:21:42 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2022-03-05 14:21:42 +0000 |
commit | 2c73988a36d94b81c8b49b283f50ff463fc63342 (patch) | |
tree | 74faa26970439b3738f492376911e9f5da20ef6a /README.md | |
parent | b591b0eeebf449f09421de20ca8aae24effad336 (diff) | |
download | biteq-2c73988a36d94b81c8b49b283f50ff463fc63342.tar.gz biteq-2c73988a36d94b81c8b49b283f50ff463fc63342.zip |
Add to the README
Diffstat (limited to 'README.md')
-rw-r--r-- | README.md | 28 |
1 files changed, 27 insertions, 1 deletions
@@ -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 |