chore: bump up toolchain 29/9/2024

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.
@@ -161,6 +164,8 @@ attribute [bitvec_rules] BitVec.ofBool_false
 attribute [bitvec_rules] BitVec.ofNat_eq_ofNat
 attribute [bitvec_rules] BitVec.zero_eq
 attribute [bitvec_rules] BitVec.truncate_eq_zeroExtend
+attribute [bitvec_rules] BitVec.or_self
+attribute [minimal_theory] BitVec.zero_or
 
 attribute [bitvec_rules] BitVec.add_sub_cancel
 attribute [bitvec_rules] BitVec.sub_add_cancel
@@ -213,7 +218,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
@@ -456,9 +461,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
@@ -500,32 +502,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
@@ -1087,21 +1069,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)

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)

Arm/Insts/Common.lean

@@ -401,9 +401,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 →

Arm/Memory/MemoryProofs.lean

@@ -158,7 +158,7 @@ theorem write_mem_of_write_mem_commute
   (h : mem_separate addr2 addr2 addr1 addr1) :
   write_mem addr2 val2 (write_mem addr1 val1 s) =
   write_mem addr1 val1 (write_mem addr2 val2 s) := by
-  simp_all only [write_mem, ArmState.mk.injEq, and_self, and_true, true_and]
+  simp_all only [write_mem, ArmState.mk.injEq, BitVec.and_self, and_true, true_and]
   unfold write_store
   have := @mem_separate_starting_addresses_neq addr2 addr2 addr1 addr1
   simp [h] at this
@@ -317,7 +317,7 @@ private theorem mem_subset_neq_first_addr_small_second_region
   cases h2
   · rename_i h
     simp only [BitVec.add_sub_self_left_64] at h
-    have l1 : n' = 18446744073709551615 := by      
+    have l1 : n' = 18446744073709551615 := by
       rw [BitVec.toNat_eq] at h
       simp only [toNat_ofNat, Nat.reducePow, Nat.reduceMod] at h
       omega

Arm/Memory/SeparateProofs.lean

@@ -75,56 +75,58 @@ theorem addr_add_one_add_m_sub_one  (n : Nat) (addr : BitVec 64)
 
 theorem mem_subset_refl : mem_subset a1 a2 a1 a2 := by
   simp [mem_subset]
-  bv_check "lrat_files/SeparateProofs.lean-mem_subset_refl-77-2.lrat"
+  bv_check "lrat_files/SeparateProofs.lean-mem_subset_refl-78-2.lrat"
 
 theorem mem_subsets_overlap (h : mem_subset a1 a2 b1 b2) :
   mem_overlap a1 a2 b1 b2 := by
   revert h
   simp [mem_subset, mem_overlap]
-  bv_check "lrat_files/SeparateProofs.lean-mem_subsets_overlap-83-2.lrat"
+  bv_check "lrat_files/SeparateProofs.lean-mem_subsets_overlap-84-2.lrat"
 
 theorem mem_subset_eq : mem_subset a a b b = (a = b)  := by
   simp [mem_subset]
-  bv_check "lrat_files/SeparateProofs.lean-mem_subset_eq-87-2.lrat"
+  bv_check "lrat_files/SeparateProofs.lean-mem_subset_eq-88-2.lrat"
 
 theorem mem_subset_first_address (h : mem_subset a b c d) :
   mem_subset a a c d := by
   revert h
   simp_all [mem_subset]
-  bv_check "lrat_files/SeparateProofs.lean-mem_subset_first_address-93-2.lrat"
+  bv_check "lrat_files/SeparateProofs.lean-mem_subset_first_address-94-2.lrat"
 
 theorem mem_subset_one_addr_neq (h1 : a ≠ b1)
   (h : mem_subset a a b1 b2) :
   mem_subset a a (b1 + 1#64) b2 := by
   revert h
   simp_all [mem_subset]
-  bv_check "lrat_files/SeparateProofs.lean-mem_subset_one_addr_neq-100-2.lrat"
+  bv_check "lrat_files/SeparateProofs.lean-mem_subset_one_addr_neq-101-2.lrat"
 
 theorem mem_subset_same_address_different_sizes
   (h : mem_subset addr (addr + n1) addr (addr + n2)) :
   n1 <= n2 := by
   revert h
   simp [mem_subset]
-  bv_check "lrat_files/SeparateProofs.lean-mem_subset_same_address_different_sizes-107-2.lrat"
+  bv_check "lrat_files/SeparateProofs.lean-mem_subset_same_address_different_sizes-108-2.lrat" -- wow, crazy.
+
 
 theorem first_address_is_subset_of_region :
   mem_subset a a a (a + n) := by
   simp [mem_subset]
-  bv_check "lrat_files/SeparateProofs.lean-first_address_is_subset_of_region-112-2.lrat"
+  bv_check "lrat_files/SeparateProofs.lean-first_address_is_subset_of_region-114-2.lrat"
 
 private theorem first_address_add_one_is_subset_of_region_helper (n addr : BitVec 64)
   (_h_lb : 0#64 < n) :
   addr + n - addr = 18446744073709551615#64 ∨
   addr + n - addr ≤ addr + n - addr ∧ addr + 1#64 - addr ≤ addr + n - addr := by
   bv_check
-    "lrat_files/SeparateProofs.lean-_private.Arm.SeparateProofs.0.first_address_add_one_is_subset_of_region_helper-118-2.lrat"
+    "lrat_files/SeparateProofs.lean-_private.Arm.Memory.SeparateProofs.0.first_address_add_one_is_subset_of_region_helper-120-2.lrat"
 
 theorem first_address_add_one_is_subset_of_region (n : Nat) (addr : BitVec 64)
   (_h_lb : 0 < n) (h_ub : n < 2 ^ 64) :
   mem_subset (addr + 1#64) (addr + (BitVec.ofNat 64 n)) addr (addr + (BitVec.ofNat 64 n)) := by
-  simp [mem_subset]
-  apply first_address_add_one_is_subset_of_region_helper
-  bv_omega
+  simp only [mem_subset]
+  have : 0#64 < (BitVec.ofNat 64 n) := by
+    bv_omega
+  bv_check "lrat_files/SeparateProofs.lean-first_address_add_one_is_subset_of_region-129-2.lrat"
 
 private theorem first_addresses_add_one_is_subset_of_region_general_helper
   (n m addr1 addr2 : BitVec 64) (h0 : 0#64 < m) :
@@ -133,7 +135,7 @@ private theorem first_addresses_add_one_is_subset_of_region_general_helper
   addr2 + n - addr2 = 18446744073709551615#64 ∨
     addr1 + m - addr2 ≤ addr2 + n - addr2 ∧ addr1 + 1#64 - addr2 ≤ addr1 + m - addr2 := by
     bv_check
-      "lrat_files/SeparateProofs.lean-_private.Arm.SeparateProofs.0.first_addresses_add_one_is_subset_of_region_general_helper-134-4.lrat"
+      "lrat_files/SeparateProofs.lean-_private.Arm.Memory.SeparateProofs.0.first_addresses_add_one_is_subset_of_region_general_helper-137-4.lrat"
 
 theorem first_addresses_add_one_is_subset_of_region_general
   (h0 : 0 < m) (h1 : m < 2 ^ 64) (h2 : n < 2 ^ 64)
@@ -152,7 +154,7 @@ private theorem first_addresses_add_one_preserves_subset_same_addr_helper (h1l :
   m - 1#64 ≤ (BitVec.ofNat 64 (2^64 - 1)) - 1#64 := by
   revert h1l
   bv_check
-    "lrat_files/SeparateProofs.lean-_private.Arm.SeparateProofs.0.first_addresses_add_one_preserves_subset_same_addr_helper-153-2.lrat"
+    "lrat_files/SeparateProofs.lean-_private.Arm.Memory.SeparateProofs.0.first_addresses_add_one_preserves_subset_same_addr_helper-156-2.lrat"
 
 theorem first_addresses_add_one_preserves_subset_same_addr
   (h1l : 0 < m) (h1u : m < 2 ^ 64)
@@ -202,7 +204,7 @@ private theorem mem_subset_one_addr_region_lemma_helper (n1 addr1 addr2 : BitVec
   addr1 + n1 - 1#64 - addr2 ≤ 0#64 ∧ addr1 - addr2 ≤ addr1 + n1 - 1#64 - addr2 →
   n1 = 1 ∧ addr1 = addr2 := by
   bv_check
-    "lrat_files/SeparateProofs.lean-_private.Arm.SeparateProofs.0.mem_subset_one_addr_region_lemma_helper-203-2.lrat"
+    "lrat_files/SeparateProofs.lean-_private.Arm.Memory.SeparateProofs.0.mem_subset_one_addr_region_lemma_helper-206-2.lrat"
 
 theorem mem_subset_one_addr_region_lemma (addr1 addr2 : BitVec 64) (h : n1 <= 2 ^ 64) :
   mem_subset addr1 (addr1 + (BitVec.ofNat 64 n1) - 1#64) addr2 addr2 → (n1 = 1) ∧ (addr1 = addr2) := by
@@ -212,7 +214,8 @@ theorem mem_subset_one_addr_region_lemma (addr1 addr2 : BitVec 64) (h : n1 <= 2
   simp_all only [ofNat_eq_ofNat, and_imp, ne_eq, false_or]
   have h2 : (BitVec.ofNat 64 n1) = 1#64 → n1 = 1 := by bv_omega
   intro h₀ h₁
-  simp_all only [true_implies, BitVec.sub_self, and_self]
+  simp_all only [true_implies, BitVec.sub_self, BitVec.and_self]
+  bv_normalize
 
 theorem mem_subset_one_addr_region_lemma_alt (addr1 addr2 : BitVec 64)
   (h : n1 < 2 ^ 64) :
@@ -230,70 +233,71 @@ theorem mem_subset_same_region_lemma
   bv_omega
   done
 
+/-- slow proof. -/
 theorem mem_subset_trans
   (h1 : mem_subset a1 a2 b1 b2)
   (h2 : mem_subset b1 b2 c1 c2) :
   mem_subset a1 a2 c1 c2 := by
   revert h1 h2
   simp [mem_subset]
-  bv_check "lrat_files/SeparateProofs.lean-mem_subset_trans-239-2.lrat"
-
+  bv_check "lrat_files/SeparateProofs.lean-mem_subset_trans-243-2.lrat"
 ----------------------------------------------------------------------
 ---- mem_separate ----
 
 theorem mem_separate_commutative :
   mem_separate a1 a2 b1 b2 = mem_separate b1 b2 a1 a2 := by
   simp [mem_separate, mem_overlap]
-  bv_check "lrat_files/SeparateProofs.lean-mem_separate_commutative-247-2.lrat"
+  bv_check "lrat_files/SeparateProofs.lean-mem_separate_commutative-250-2.lrat"
 
 theorem mem_separate_starting_addresses_neq :
   mem_separate a1 a2 b1 b2 → a1 ≠ b1 := by
   simp [mem_separate, mem_overlap]
-  bv_check "lrat_files/SeparateProofs.lean-mem_separate_starting_addresses_neq-252-2.lrat"
+  bv_check "lrat_files/SeparateProofs.lean-mem_separate_starting_addresses_neq-255-2.lrat"
 
 theorem mem_separate_neq :
   a ≠ b ↔ mem_separate a a b b := by
   simp [mem_separate, mem_overlap]
-  bv_check "lrat_files/SeparateProofs.lean-mem_separate_neq-257-2.lrat"
+  bv_check "lrat_files/SeparateProofs.lean-mem_separate_neq-260-2.lrat"
 
 theorem mem_separate_first_address_separate (h : mem_separate a b c d) :
   mem_separate a a c d := by
   revert h
   simp [mem_separate, mem_overlap]
-  bv_check "lrat_files/SeparateProofs.lean-mem_separate_first_address_separate-263-2.lrat"
+  bv_check "lrat_files/SeparateProofs.lean-mem_separate_first_address_separate-266-2.lrat"
 
+/-- Slow proof. -/
 theorem mem_separate_contiguous_regions (a k n : BitVec 64)
   (hn : n < ((BitVec.ofNat 64 (2^64 - 1)) - k)) :
   mem_separate a (a + k) (a + k + 1#64) (a + k + 1#64 + n) := by
   revert hn
   simp [mem_separate, mem_overlap]
-  bv_check "lrat_files/SeparateProofs.lean-mem_separate_contiguous_regions-270-2.lrat"
+  bv_check "lrat_files/SeparateProofs.lean-mem_separate_contiguous_regions-274-2.lrat"
 
 private theorem mem_separate_contiguous_regions_one_address_helper (n' addr : BitVec 64)
   (h : n' < 0xffffffffffffffff) :
 (¬addr + 1#64 - addr ≤ 0#64 ∧ ¬addr + 1#64 + n' - addr ≤ 0#64) ∧
     ¬addr - (addr + 1#64) ≤ addr + 1#64 + n' - (addr + 1#64) := by
   bv_check
-    "lrat_files/SeparateProofs.lean-_private.Arm.SeparateProofs.0.mem_separate_contiguous_regions_one_address_helper-276-2.lrat"
+    "lrat_files/SeparateProofs.lean-_private.Arm.Memory.SeparateProofs.0.mem_separate_contiguous_regions_one_address_helper-280-2.lrat"
 
 -- TODO: Perhaps use/modify mem_separate_contiguous_regions instead?
 theorem mem_separate_contiguous_regions_one_address (addr : BitVec 64) (h : n' < 2 ^ 64) :
   mem_separate addr addr (addr + 1#64) (addr + 1#64 + (BitVec.ofNat 64 (n' - 1))) := by
   simp [mem_separate, mem_overlap]
   have h' : (BitVec.ofNat 64 (n' - 1)) < 0xffffffffffffffff#64 := by
     bv_omega
-  apply mem_separate_contiguous_regions_one_address_helper
-  assumption
+  bv_check "lrat_files/SeparateProofs.lean-mem_separate_contiguous_regions_one_address-289-2.lrat"
 
 ----------------------------------------------------------------------
 ---- mem_subset and mem_separate -----
 
+/-- Slow proof, bv_decide just times out, bv_omega solves this instantly. -/
 theorem mem_separate_for_subset2
   (h1 : mem_separate a1 a2 b1 b2) (h2 : mem_subset c1 c2 b1 b2) :
   mem_separate a1 a2 c1 c2 := by
   revert h1 h2
   simp [mem_subset, mem_separate, mem_overlap]
-  bv_check "lrat_files/SeparateProofs.lean-mem_separate_for_subset2-296-2.lrat"
+  bv_omega
 
 theorem mem_separate_for_subset1
   (h1 : mem_separate a1 a2 b1 b2) (h2 : mem_subset c1 c2 a1 a2) :