From 857ed826aa65008f3dcb79a0631643bb703b644e Mon Sep 17 00:00:00 2001 From: Shilpi Goel Date: Mon, 25 Mar 2024 13:39:08 -0500 Subject: [PATCH] Bump Lean toolchain --- Arm/BitVec.lean | 10 +++++----- Arm/MemoryProofs.lean | 3 +-- Tactics/Sym.lean | 2 +- lean-toolchain | 2 +- 4 files changed, 8 insertions(+), 9 deletions(-) diff --git a/Arm/BitVec.lean b/Arm/BitVec.lean index 84ad9ec3..2f59c63e 100644 --- a/Arm/BitVec.lean +++ b/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 diff --git a/Arm/MemoryProofs.lean b/Arm/MemoryProofs.lean index 2a0bf7b0..accd8a6b 100644 --- a/Arm/MemoryProofs.lean +++ b/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 = diff --git a/Tactics/Sym.lean b/Tactics/Sym.lean index 6266228b..7c24a636 100644 --- a/Tactics/Sym.lean +++ b/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")) diff --git a/lean-toolchain b/lean-toolchain index 60d4af99..f55067a5 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-03-08 +leanprover/lean4:nightly-2024-03-25