diff options
| author | James Pollard <james@pollard.dev> | 2020-06-28 17:15:14 +0100 |
|---|---|---|
| committer | James Pollard <james@pollard.dev> | 2020-06-28 17:15:14 +0100 |
| commit | accf4b273525412801dc21c893d41c890c9fed6d (patch) | |
| tree | 1e866f98be07db46a446161a07ff1dbcf2ea5945 /src/common/Coquplib.v | |
| parent | 8fda19cb580bda72f374bc2176d7e2efa5cd613b (diff) | |
| download | vericert-kvx-accf4b273525412801dc21c893d41c890c9fed6d.tar.gz vericert-kvx-accf4b273525412801dc21c893d41c890c9fed6d.zip | |
Fix unsigned/signed issues.
Diffstat (limited to 'src/common/Coquplib.v')
| -rw-r--r-- | src/common/Coquplib.v | 23 |
1 files changed, 15 insertions, 8 deletions
diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v index b8a02d2..5de1e7c 100644 --- a/src/common/Coquplib.v +++ b/src/common/Coquplib.v @@ -69,45 +69,52 @@ Ltac kill_bools := Ltac unfold_constants := repeat match goal with - | [ _ : _ |- context[Integers.Ptrofs.modulus] ] => + | [ |- context[Integers.Ptrofs.modulus] ] => replace Integers.Ptrofs.modulus with 4294967296 by reflexivity | [ H : context[Integers.Ptrofs.modulus] |- _ ] => replace Integers.Ptrofs.modulus with 4294967296 in H by reflexivity - | [ _ : _ |- context[Integers.Ptrofs.min_signed] ] => + | [ |- context[Integers.Ptrofs.min_signed] ] => replace Integers.Ptrofs.min_signed with (-2147483648) by reflexivity | [ H : context[Integers.Ptrofs.min_signed] |- _ ] => replace Integers.Ptrofs.min_signed with (-2147483648) in H by reflexivity - | [ _ : _ |- context[Integers.Ptrofs.max_signed] ] => + | [ |- context[Integers.Ptrofs.max_signed] ] => replace Integers.Ptrofs.max_signed with 2147483647 by reflexivity | [ H : context[Integers.Ptrofs.max_signed] |- _ ] => replace Integers.Ptrofs.max_signed with 2147483647 in H by reflexivity - | [ _ : _ |- context[Integers.Ptrofs.max_unsigned] ] => + | [ |- context[Integers.Ptrofs.max_unsigned] ] => replace Integers.Ptrofs.max_unsigned with 4294967295 by reflexivity | [ H : context[Integers.Ptrofs.max_unsigned] |- _ ] => replace Integers.Ptrofs.max_unsigned with 4294967295 in H by reflexivity - | [ _ : _ |- context[Integers.Int.modulus] ] => + | [ |- context[Integers.Int.modulus] ] => replace Integers.Int.modulus with 4294967296 by reflexivity | [ H : context[Integers.Int.modulus] |- _ ] => replace Integers.Int.modulus with 4294967296 in H by reflexivity - | [ _ : _ |- context[Integers.Int.min_signed] ] => + | [ |- context[Integers.Int.min_signed] ] => replace Integers.Int.min_signed with (-2147483648) by reflexivity | [ H : context[Integers.Int.min_signed] |- _ ] => replace Integers.Int.min_signed with (-2147483648) in H by reflexivity - | [ _ : _ |- context[Integers.Int.max_signed] ] => + | [ |- context[Integers.Int.max_signed] ] => replace Integers.Int.max_signed with 2147483647 by reflexivity | [ H : context[Integers.Int.max_signed] |- _ ] => replace Integers.Int.max_signed with 2147483647 in H by reflexivity - | [ _ : _ |- context[Integers.Int.max_unsigned] ] => + | [ |- context[Integers.Int.max_unsigned] ] => replace Integers.Int.max_unsigned with 4294967295 by reflexivity | [ H : context[Integers.Int.max_unsigned] |- _ ] => replace Integers.Int.max_unsigned with 4294967295 in H by reflexivity + + | [ |- context[Integers.Ptrofs.unsigned (Integers.Ptrofs.repr ?x) ] ] => + match (eval compute in (0 <=? x)) with + | true => replace (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr x)) + with x by reflexivity + | false => idtac + end end. Ltac simplify := unfold_constants; simpl in *; |