From b9d02cd15c0ea7250b83e5b333327dfc024c783c Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 4 Aug 2020 13:12:22 +0200 Subject: Fix iload proof --- src/verilog/ValueInt.v | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'src/verilog') 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. -- cgit