diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-03-05 14:30:32 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-03-05 14:30:32 +0000 |
| commit | ad56f236ad65585da1d895b3754ad751bec1aade (patch) | |
| tree | 8021af15a76c084a6469155e6ee5de31df37ca78 | |
| parent | 2c73988a36d94b81c8b49b283f50ff463fc63342 (diff) | |
| download | biteq-main.tar.gz biteq-main.zip | |
| -rw-r--r-- | README.md | 9 | ||||
| -rw-r--r-- | README.org | 1 |
2 files changed, 1 insertions, 9 deletions
@@ -1,17 +1,8 @@ -- [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. @@ -1,5 +1,6 @@ #+title: BitEQ #+author: Yann Herklotz +#+options: toc:nil * BitEQ |