diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-08-04 19:59:30 +0200 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-08-04 19:59:30 +0200 |
| commit | b1aff2a1a6d45a253d87c01b4c967376491597dc (patch) | |
| tree | 671ec341d6610a1ddb2ffeae66391905643499a5 /src/verilog/ValueInt.v | |
| parent | bb2b5199a63521b83d26c97c3eee7afdd4e88437 (diff) | |
| download | vericert-kvx-b1aff2a1a6d45a253d87c01b4c967376491597dc.tar.gz vericert-kvx-b1aff2a1a6d45a253d87c01b4c967376491597dc.zip | |
Finish istore and iload without any admits
Diffstat (limited to 'src/verilog/ValueInt.v')
| -rw-r--r-- | src/verilog/ValueInt.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/verilog/ValueInt.v b/src/verilog/ValueInt.v index 4e34c06..2220998 100644 --- a/src/verilog/ValueInt.v +++ b/src/verilog/ValueInt.v @@ -162,6 +162,7 @@ Proof. 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 simplify_val := repeat (simplify; unfold uvalueToZ, valueToPtr, Ptrofs.of_int, valueToInt, intToValue, + ptrToValue in *). Ltac crush_val := simplify_val; try discriminate; try congruence; try lia; liapp; try assumption. |