diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-08-10 12:09:03 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-08-10 12:09:03 +0100 |
| commit | 86e64fd05cea7b1da996701cd3653db5f471f8d1 (patch) | |
| tree | 5cee338b89c4b1b2906cbf8e62d8f8dffdff0abb /src/common | |
| parent | 4d62c7f35533ebd36ae4a0bdef6cd64fcc0be375 (diff) | |
| download | vericert-86e64fd05cea7b1da996701cd3653db5f471f8d1.tar.gz vericert-86e64fd05cea7b1da996701cd3653db5f471f8d1.zip | |
Finish final forward simulation correctness
Diffstat (limited to 'src/common')
| -rw-r--r-- | src/common/IntegerExtra.v | 20 |
1 files changed, 0 insertions, 20 deletions
diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v index 2b6cded..e56bda0 100644 --- a/src/common/IntegerExtra.v +++ b/src/common/IntegerExtra.v @@ -361,26 +361,6 @@ Module IntExtra. apply zlt_true. lia. lia. Qed. - Lemma bits_ofwords: - forall b4 b3 b2 b1 i, 0 <= i < zwordsize -> - testbit (ofbytes b4 b3 b2 b1) i = - if zlt i Byte.zwordsize - then Byte.testbit b1 i - else (if zlt i (2 * Byte.zwordsize) - then Byte.testbit b2 (i - Byte.zwordsize) - else (if zlt i (3 * Byte.zwordsize) - then Byte.testbit b2 (i - 2 * Byte.zwordsize) - else Byte.testbit b2 (i - 3 * Byte.zwordsize))). - Proof. - intros. unfold ofbytes. repeat (rewrite bits_or; auto). repeat (rewrite bits_shl; auto). - change (unsigned (repr Byte.zwordsize)) with Byte.zwordsize. - change (unsigned (repr (2 * Byte.zwordsize))) with (2 * Byte.zwordsize). - change (unsigned (repr (3 * Byte.zwordsize))) with (3 * Byte.zwordsize). - assert (zwordsize = 4 * Byte.zwordsize) by reflexivity. - destruct (zlt i Byte.zwordsize). - rewrite testbit_repr; auto. - Abort. - Lemma div_divs_equiv : forall x y, signed x >= 0 -> |