Bump Lean toolchain

Arm/BitVec.lean

@@ -32,6 +32,7 @@ protected def flatten {n : Nat} (xs : List (BitVec n)) : BitVec (n * xs.length)
   | x :: rest =>
     have h : n + n * List.length rest = n * List.length (x :: rest) := by
       simp [List.length_cons, Nat.mul_one, Nat.mul_add, Nat.succ_eq_one_add]
+      omega
     BitVec.cast h (x ++ (BitVec.flatten rest))
 
 /-- Generate a random bitvector of width n. The range of the values
@@ -271,9 +272,6 @@ protected theorem extract_lsb_of_zeroExtend (x : BitVec n) (h : j < i) :
 theorem empty_bitvector_append_left
   (x : BitVec n) (h : 0 + n = n) :
   BitVec.cast h (0#0 ++ x) = x := by
-  simp [HAppend.hAppend, BitVec.append, shiftLeftZeroExtend, zeroExtend']
-  simp [HOr.hOr, OrOp.or, BitVec.or, Nat.lor]
-  unfold Nat.bitwise
   simp [BitVec.cast]
   rfl
 
@@ -337,7 +335,7 @@ theorem append_of_extract_general_nat (high low n vn : Nat) (h : vn < 2 ^ n) :
   done
 
 theorem append_of_extract (n : Nat) (v : BitVec n)
-  (hn0 : 0 < n) (high0 : high = n - low) (low0 : 1 <= low)
+  (high0 : high = n - low) (low0 : 1 <= low)
   (h : high + (low - 1 - 0 + 1) = n) :
   BitVec.cast h (zeroExtend high (v >>> low) ++ extractLsb (low - 1) 0 v) = v := by
   ext
@@ -350,9 +348,10 @@ theorem append_of_extract (n : Nat) (v : BitVec n)
   · rw [this]
   · rw [Nat.shiftRight_eq_div_pow]
     exact Nat.lt_of_le_of_lt (Nat.div_le_self _ _) vlt
+  done
 
 theorem append_of_extract_general (v : BitVec n)
-  (hn0 : 0 < n) (low0 : 1 <= low)
+  (low0 : 1 <= low)
   (h1 : high = width)
   (h2 : (high + low - 1 - 0 + 1) = (width + (low - 1 - 0 + 1))) :
   BitVec.cast h1 (zeroExtend high (v >>> low)) ++ extractLsb (low - 1) 0 v =
@@ -367,6 +366,7 @@ theorem append_of_extract_general (v : BitVec n)
   · rw [this]
   · rw [Nat.shiftRight_eq_div_pow]
     exact Nat.lt_of_le_of_lt (Nat.div_le_self _ _) h_vlt
+  done
 
 theorem leftshift_n_or_mod_2n :
   (x <<< n ||| y) % 2 ^ n = y % 2 ^ n := by

Arm/MemoryProofs.lean

@@ -78,7 +78,6 @@ theorem append_byte_of_extract_rest_same_cast (n : Nat) (v : BitVec ((n + 1) * 8
   apply BitVec.append_of_extract
   · omega
   · omega
-  · decide
   · omega
   done
 
@@ -720,7 +719,7 @@ theorem read_mem_bytes_of_write_mem_bytes_subset_helper1 (a i : Nat)
 
 theorem read_mem_bytes_of_write_mem_bytes_subset_helper2
   (addr2 addr1 : BitVec 64) (val : BitVec (n1 * 8))
-  (h0 : 0 < n1) (h1 : n1 <= 2 ^ 64) (h2 : 0 < n)
+  (_h0 : 0 < n1) (_h1 : n1 <= 2 ^ 64) (h2 : 0 < n)
   (h4 : addr1 ≠ addr2) (h5 : addr2 - addr1 < (2 ^ 64 - 1)#64) :
   (BitVec.toNat val >>> ((BitVec.toNat (addr2 - addr1) + 1) % 2 ^ 64 * 8) % 2 ^ (n * 8)) <<< 8 |||
       BitVec.toNat val >>> (BitVec.toNat (addr2 - addr1) * 8) % 2 ^ 8 =

Tactics/Sym.lean

@@ -141,7 +141,7 @@ def sym_one (curr_state_number : Nat) (prog : Lean.Ident) :
     --                            pcexpr).toSyntax
     -- Question: how can I convert this pcbv into Syntax?
     let mk_name (s : String) : Lean.Name :=
-      Lean.Name.append Lean.Name.anonymous s
+      Lean.Name.mkStr Lean.Name.anonymous s
     -- st': name of the next state
     let st' := Lean.mkIdent (mk_name ("s_" ++ n'_str))
     -- let h_st_ok := Lean.mkIdent (mk_name ("h_s" ++ n_str ++ "_ok"))

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2024-03-08
+leanprover/lean4:nightly-2024-03-25