From b1aff2a1a6d45a253d87c01b4c967376491597dc Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 4 Aug 2020 19:59:30 +0200 Subject: Finish istore and iload without any admits --- src/verilog/ValueInt.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src/verilog/ValueInt.v') 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. -- cgit