From 0af0e6847753ab8f20a13ab8aaf9e83357f3774c Mon Sep 17 00:00:00 2001 From: Hongyu Ouyang <96765450+casavaca@users.noreply.github.com> Date: Tue, 19 Mar 2024 14:54:27 -0700 Subject: [PATCH 1/2] Add proof for theorem add_x1_x1_1_sym --- Proofs/Test.lean | 46 +++++++++++++++++++++++++++++----------------- 1 file changed, 29 insertions(+), 17 deletions(-) diff --git a/Proofs/Test.lean b/Proofs/Test.lean index a5c54d75..51d2fac7 100644 --- a/Proofs/Test.lean +++ b/Proofs/Test.lean @@ -56,7 +56,7 @@ theorem zeroExtend_irrelevant (x : BitVec 64) : theorem add_x1_x1_1_sym_helper (x1_var : BitVec 64) : (BitVec.toNat x1_var + 1)#64 = x1_var + 1#64 := by - sorry + rfl theorem add_x1_x1_1_sym (h_pc : read_pc s = 0#64) @@ -66,22 +66,34 @@ theorem add_x1_x1_1_sym (h_s' : s' = run 1 s) (h_x1': x1' = read_gpr 64 1#5 s') : x1' = x1 + 1#64 ∧ read_err s' = StateError.None := by - sorry - -- simp [*] at * - -- unfold run stepi; simp [h_pc, h_inst, h_s_ok] - -- unfold exec_inst - -- simp (config := { ground := true }) only [h_inst] - -- -- This proof is still broken in `simp (config := { ground := true })` - -- sorry - -- unfold DPI.exec_add_sub_imm; simp (config := { ground := true }) - -- unfold AddWithCarry - -- simp (config := { ground := true }) only [zeroExtend_twice, zeroExtend_of_Nat_64] - -- generalize (r (StateField.GPR 1#5) s) = x1_var - -- unfold state_value at x1_var; - -- simp at x1_var - -- simp [zeroExtend_irrelevant] - -- rw [add_x1_x1_1_sym_helper] - -- trivial + -- the following can be removed once we add builtin_simproc for HShift for Nat. + -- https://github.com/leanprover/lean4/blob/master/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean + have : (2432697377 >>> 25)#4 = 8#4 := by decide + have : (2432697377 >>> 23)#6 = 34#6 := by decide + have : (2432697377 >>> 31)#1 = 1#1 := by decide + have : (2432697377 >>> 30)#1 = 0#1 := by decide + have : (2432697377 >>> 29)#1 = 0#1 := by decide + have : (2432697377 >>> 22)#1 = 0#1 := by decide + have : (2432697377 >>> 10)#12 = 1#12 := by decide + have : (2432697377 >>> 5)#5 = 1#5 := by decide + conv at h_s' => { + rhs + unfold run run stepi + simp only [h_s_ok, h_pc, h_inst] + unfold decode_raw_inst + simp [decode_data_proc_imm, *] -- * for unnamed have ... = ... above + simp [exec_inst, DPI.exec_add_sub_imm] + -- similarly, the following can be removed once we add builtin_simproc for BEq for BitVec. + -- https://github.com/leanprover/lean4/blob/master/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean + rw [if_pos ((by decide) : 1#1 == 1#1), if_neg ((by decide) : 0#1 ≠ 1#1)] + rw [←h_x1, h_pc] + } + rw [h_x1', h_s', ←h_s_ok] + simp [state_simp_rules] + unfold AddWithCarry + simp only [bv_toNat] + rw [Nat.add_assoc, Nat.add_mod, Nat.add_mod (BitVec.toNat x1) _] + congr -- This version of the theorem opens up run only once. See the -- revert...intro block below. From 5f0ed8a9296a9fb21779775de78acc946f0463e0 Mon Sep 17 00:00:00 2001 From: Hongyu Ouyang <96765450+casavaca@users.noreply.github.com> Date: Tue, 19 Mar 2024 18:07:40 -0700 Subject: [PATCH 2/2] simp --> simp only --- Proofs/Test.lean | 41 ++++++++++++++++++++++++----------------- 1 file changed, 24 insertions(+), 17 deletions(-) diff --git a/Proofs/Test.lean b/Proofs/Test.lean index 51d2fac7..2d3d6e60 100644 --- a/Proofs/Test.lean +++ b/Proofs/Test.lean @@ -67,33 +67,40 @@ theorem add_x1_x1_1_sym (h_x1': x1' = read_gpr 64 1#5 s') : x1' = x1 + 1#64 ∧ read_err s' = StateError.None := by -- the following can be removed once we add builtin_simproc for HShift for Nat. - -- https://github.com/leanprover/lean4/blob/master/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean - have : (2432697377 >>> 25)#4 = 8#4 := by decide - have : (2432697377 >>> 23)#6 = 34#6 := by decide - have : (2432697377 >>> 31)#1 = 1#1 := by decide - have : (2432697377 >>> 30)#1 = 0#1 := by decide - have : (2432697377 >>> 29)#1 = 0#1 := by decide - have : (2432697377 >>> 22)#1 = 0#1 := by decide - have : (2432697377 >>> 10)#12 = 1#12 := by decide - have : (2432697377 >>> 5)#5 = 1#5 := by decide + have tmp1 : (2432697377 >>> 25)#4 = 8#4 := by decide + have tmp2 : (2432697377 >>> 23)#6 = 34#6 := by decide + have tmp3 : (2432697377 >>> 31)#1 = 1#1 := by decide + have tmp4 : (2432697377 >>> 30)#1 = 0#1 := by decide + have tmp5 : (2432697377 >>> 29)#1 = 0#1 := by decide + have tmp6 : (2432697377 >>> 22)#1 = 0#1 := by decide + have tmp7 : (2432697377 >>> 10)#12 = 1#12 := by decide + have tmp8 : (2432697377 >>> 5)#5 = 1#5 := by decide conv at h_s' => { rhs unfold run run stepi simp only [h_s_ok, h_pc, h_inst] unfold decode_raw_inst - simp [decode_data_proc_imm, *] -- * for unnamed have ... = ... above - simp [exec_inst, DPI.exec_add_sub_imm] + -- apply hints provided by `simp? [decode_data_proc_imm]` + simp only [decode_data_proc_imm, BitVec.extractLsb_ofNat, Nat.reduceAdd, Nat.reduceSub, Nat.reducePow, + Nat.reduceMod, Bool.true_and, beq_iff_eq, Nat.sub_zero, Nat.shiftRight_zero, reduceOfNat] + -- guide lean to do the calculation. In the future, this should be done automatically by Lean, + -- by adding builtin_simproc for HShift for Nat. + -- https://github.com/leanprover/lean4/blob/master/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean + simp only [tmp1, tmp2, tmp3, tmp4, tmp5, tmp6, tmp7, tmp8] + -- apply hints provided by `simp? [exec_inst, DPI.exec_add_sub_imm]` + simp only [exec_inst, DPI.exec_add_sub_imm, Nat.reduceAdd, beq_self_eq_true, ↓reduceIte, reduceAppend, + reduceNot, beq_iff_eq] + -- guide lean to do the calculation. -- similarly, the following can be removed once we add builtin_simproc for BEq for BitVec. -- https://github.com/leanprover/lean4/blob/master/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean rw [if_pos ((by decide) : 1#1 == 1#1), if_neg ((by decide) : 0#1 ≠ 1#1)] - rw [←h_x1, h_pc] + rw [←h_x1, h_pc, ofNat_add_ofNat, Nat.zero_add] + rw [instDecidableEqBool, Bool.decEq, AddWithCarry] + rw [((by decide) : (0#1 == 1#1) = false)] + dsimp only } rw [h_x1', h_s', ←h_s_ok] - simp [state_simp_rules] - unfold AddWithCarry - simp only [bv_toNat] - rw [Nat.add_assoc, Nat.add_mod, Nat.add_mod (BitVec.toNat x1) _] - congr + simp [state_simp_rules, ←ofNat_add_ofNat] -- This version of the theorem opens up run only once. See the -- revert...intro block below.