From 80e8c0d0687aa9504799a734689937a5996c6f77 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Mon, 30 Sep 2024 12:42:25 -0500 Subject: [PATCH] chore: bump up toolchian --- Arm/BitVec.lean | 45 +++++-------------------------------------- Arm/Cfg/Cfg.lean | 6 +++--- Arm/Insts/Common.lean | 3 --- lean-toolchain | 2 +- 4 files changed, 9 insertions(+), 47 deletions(-) diff --git a/Arm/BitVec.lean b/Arm/BitVec.lean index ead22987..f17e1799 100644 --- a/Arm/BitVec.lean +++ b/Arm/BitVec.lean @@ -14,6 +14,9 @@ namespace BitVec open BitVec +@[deprecated setWidth_setWidth_of_le (since := "2024-09-18")] +abbrev truncate_truncate_of_le := @setWidth_setWidth_of_le + -- Adding some useful simp lemmas to `bitvec_rules`: we do not include -- `bv_toNat` lemmas here. -- See Init.Data.BitVec.Lemmas. @@ -213,7 +216,7 @@ attribute [bitvec_rules] BitVec.reduceULT attribute [bitvec_rules] BitVec.reduceULE attribute [bitvec_rules] BitVec.reduceSLT attribute [bitvec_rules] BitVec.reduceSLE -attribute [bitvec_rules] BitVec.reduceZeroExtend' +attribute [bitvec_rules] BitVec.reduceSetWidth' attribute [bitvec_rules] BitVec.reduceShiftLeftZeroExtend attribute [bitvec_rules] BitVec.reduceExtracLsb' attribute [bitvec_rules] BitVec.reduceReplicate @@ -457,9 +460,6 @@ theorem toNat_ofNat_lt {n w₁ : Nat} (hn : n < 2^w₁) : ---------------------------- Comparison Lemmas ----------------------- -@[simp] protected theorem not_lt {n : Nat} {a b : BitVec n} : ¬ a < b ↔ b ≤ a := by - exact Fin.not_lt .. - theorem ge_of_not_lt (x y : BitVec w₁) (h : ¬ (x < y)) : x ≥ y := by simp_all only [BitVec.le_def, BitVec.lt_def] omega @@ -501,32 +501,12 @@ protected theorem zero_le_sub (x y : BitVec n) : ----------------------------- Logical Lemmas ------------------------ -@[bitvec_rules] -protected theorem zero_or (x : BitVec n) : 0#n ||| x = x := by - unfold HOr.hOr instHOrOfOrOp OrOp.or instOrOp BitVec.or - simp only [toNat_ofNat, Nat.zero_mod, Nat.zero_or] - congr - -@[bitvec_rules] -protected theorem or_zero (x : BitVec n) : x ||| 0#n = x := by - rw [BitVec.or_comm] - rw [BitVec.zero_or] - done - -@[bitvec_rules] -protected theorem or_self (x : BitVec n) : - x ||| x = x := by - refine eq_of_toNat_eq ?_ - rw [BitVec.toNat_or] - apply Nat.eq_of_testBit_eq - simp only [Nat.testBit_or, Bool.or_self, implies_true] - done --------------------- ZeroExtend/Append/Extract Lemmas ---------------- @[bitvec_rules] theorem zeroExtend_zero_width : (zeroExtend 0 x) = 0#0 := by - unfold zeroExtend + unfold zeroExtend setWidth split <;> simp [bitvec_zero_is_unique] -- During symbolic simulation, we often encounter an `if` in the first argument @@ -1088,21 +1068,6 @@ theorem BitVec.ofBool_getLsbD (a : BitVec w) (i : Nat) : intro ⟨0, _⟩ simp -/-- If multiplication does not overflow, -then `(x * y).toNat` equals `x.toNat * y.toNat` -/ -theorem toNat_mul_of_lt {w} {x y : BitVec w} (h : x.toNat * y.toNat < 2^w) : - (x * y).toNat = x.toNat * y.toNat := by - rw [BitVec.toNat_mul, Nat.mod_eq_of_lt h] - -/-- If subtraction does not overflow, -then `(x - y).toNat` equals `x.toNat - y.toNat` -/ -theorem toNat_sub_of_lt {w} {x y : BitVec w} (h : x.toNat < y.toNat) : - (y - x).toNat = y.toNat - x.toNat := by - rw [BitVec.toNat_sub, - show (2^w - x.toNat + y.toNat) = 2^w + (y.toNat - x.toNat) by omega, - Nat.add_mod, Nat.mod_self, Nat.zero_add, Nat.mod_mod, - Nat.mod_eq_of_lt (by omega)] - /-- `x.toNat * z.toNat ≤ k` if `z ≤ y` and `x.toNat * y.toNat ≤ k` -/ theorem toNat_mul_toNat_le_of_le_of_le {w} (x y z : BitVec w) (hxy : x.toNat * y.toNat ≤ k) diff --git a/Arm/Cfg/Cfg.lean b/Arm/Cfg/Cfg.lean index 9400882e..63bc19ad 100644 --- a/Arm/Cfg/Cfg.lean +++ b/Arm/Cfg/Cfg.lean @@ -216,8 +216,8 @@ protected def addToCfg (address : BitVec 64) (program : Program) (cfg : Cfg) -- is in terms of Fin so that we can take advantage of Fin lemmas. We -- will map this theorem to BitVecs (using lemmas like -- BitVec.fin_bitvec_lt) in create'. -private theorem termination_lemma (i j max : Fin n) (h : n > 0) - (h0 : i < max) (h1 : j <= max - i) (h2 : ((Fin.ofNat' 0 h) : Fin n) < j) : +private theorem termination_lemma (i j max : Fin n) (h : NeZero n) + (h0 : i < max) (h1 : j <= max - i) (h2 : ((Fin.ofNat' n 0)) < j) : (max - (i + j)) < (max - i) := by -- Our strategy is to convert this proof obligation in terms of Nat, -- which is made possible by h0 and h1 hypotheses above. @@ -270,7 +270,7 @@ private def create' (address : BitVec 64) (max_address : BitVec 64) else if h₂ : 4#64 <= max_address - address then have ?term_lemma : (max_address - (address + 4#64)).toNat < (max_address - address).toNat := by have := termination_lemma address.toFin (4#64).toFin max_address.toFin - (by decide) + (by exact inferInstance) (by simp_all! only [BitVec.not_lt, BitVec.fin_bitvec_lt, not_false_eq_true, BitVec.lt_of_le_ne, h₁]) (by rw [← BitVec.toFin_sub]; exact h₂) (by simp_arith) diff --git a/Arm/Insts/Common.lean b/Arm/Insts/Common.lean index 1bee0cf8..aba98c78 100644 --- a/Arm/Insts/Common.lean +++ b/Arm/Insts/Common.lean @@ -389,9 +389,6 @@ dsimproc [state_simp_rules] reduceInvalidBitMasks (invalid_bit_masks _ _ _ _) := imm.expr.isTrue M) -theorem Nat.lt_one_iff {n : Nat} : n < 1 ↔ n = 0 := by - omega - theorem M_divisible_by_esize_of_valid_bit_masks (immN : BitVec 1) (imms : BitVec 6) (immediate : Bool) (M : Nat): ¬ invalid_bit_masks immN imms immediate M → diff --git a/lean-toolchain b/lean-toolchain index 018f6702..dfd7fc65 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-09-10 \ No newline at end of file +leanprover/lean4:nightly-2024-09-29