diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-08-04 13:12:22 +0200 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-08-04 13:12:22 +0200 |
| commit | b9d02cd15c0ea7250b83e5b333327dfc024c783c (patch) | |
| tree | 65d540791a97730647d0c40b7c14f1a14223a96f /src/verilog | |
| parent | c303debfd22030e0d4f8c0fdb8f1938e10e9675c (diff) | |
| download | vericert-kvx-b9d02cd15c0ea7250b83e5b333327dfc024c783c.tar.gz vericert-kvx-b9d02cd15c0ea7250b83e5b333327dfc024c783c.zip | |
Fix iload proof
Diffstat (limited to 'src/verilog')
| -rw-r--r-- | src/verilog/ValueInt.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/verilog/ValueInt.v b/src/verilog/ValueInt.v index c7f69a1..4e34c06 100644 --- a/src/verilog/ValueInt.v +++ b/src/verilog/ValueInt.v @@ -161,3 +161,7 @@ Proof. unfold valueToInt. unfold intToValue in H1. auto. inv H. symmetry. unfold valueToPtr, ptrToValue. apply Ptrofs.of_int_to_int. trivial. Qed. + +Ltac simplify_val := repeat (simplify; unfold uvalueToZ, valueToPtr, Ptrofs.of_int in *). + +Ltac crush_val := simplify_val; try discriminate; try congruence; try lia; liapp; try assumption. |