From 1b3901f60e736580a55bf635cb2f57143168a825 Mon Sep 17 00:00:00 2001
From: Shilpi Goel <shigoel@gmail.com>
Date: Mon, 7 Oct 2024 20:18:23 -0500
Subject: [PATCH 1/2] Bump toolchain

---
 ELFSage/Util/ByteArray.lean | 11 +++++------
 lean-toolchain              |  2 +-
 2 files changed, 6 insertions(+), 7 deletions(-)

diff --git a/ELFSage/Util/ByteArray.lean b/ELFSage/Util/ByteArray.lean
index c7c3364..b136e61 100644
--- a/ELFSage/Util/ByteArray.lean
+++ b/ELFSage/Util/ByteArray.lean
@@ -1,3 +1,5 @@
+import Std.Tactic.BVDecide
+
 def ByteArray.getUInt64BEfrom (bs : ByteArray) (offset : Nat) (h: bs.size - offset ≥ 8) : UInt64 :=
   (bs.get ⟨offset + 0, by omega⟩).toUInt64 <<< 0x38 |||
   (bs.get ⟨offset + 1, by omega⟩).toUInt64 <<< 0x30 |||
@@ -175,7 +177,7 @@ theorem Array.extract_len_aux {src: Array α} :
      intro lt
      simp; split
      · have : n + l + 1 ≤ size src := by omega
-       simp only [Array.toList_length] at ih
+       simp only [length_toList] at ih
        rw [ih (l + 1) (push dst src[l]) this]
        simp_arith
      · omega
@@ -202,9 +204,6 @@ def NByteArray.extract (bs : ByteArray) (n : Nat) (h : bs.size ≥ n) : NByteArr
         unfold Array.extract.loop
         split; simp; contradiction
       rw [this, this]
-      have : ∀α, ∀a b : Array α, (a ++ b).size = a.size + b.size := by
-        simp only [Array.append_toList, Array.size, List.length_append, implies_true]
-      rw [this, this]
       simp
       have : bs.data.size = bs.size := by
         simp [ByteArray.size]
@@ -213,7 +212,7 @@ def NByteArray.extract (bs : ByteArray) (n : Nat) (h : bs.size ≥ n) : NByteArr
         split <;> omega
       rw [Array.extract_loop_len (min n bs.data.size) 0 #[]]
       simp only [ByteArray.size, Array.size,
-                 ge_iff_le, Array.append_toList,
+                 ge_iff_le, Array.size_append,
                  List.length_append, implies_true,
                  Nat.min_def, Nat.zero_add,
                  Array.toList_toArray, List.length_nil,
@@ -223,7 +222,7 @@ def NByteArray.extract (bs : ByteArray) (n : Nat) (h : bs.size ≥ n) : NByteArr
       · simp [Nat.min_def]; split
         · assumption
         · simp only [ByteArray.size, Array.size,
-                     ge_iff_le, Array.append_toList,
+                     ge_iff_le, Array.size_append,
                      List.length_append, implies_true,
                      Nat.min_def, Nat.zero_add,
                      Nat.not_le, Nat.le_refl]
diff --git a/lean-toolchain b/lean-toolchain
index 018f670..8e380e1 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-10-07
\ No newline at end of file

From 243d8b07356fe1e488bbd03f23787c752cf61f7e Mon Sep 17 00:00:00 2001
From: Shilpi Goel <shigoel@gmail.com>
Date: Mon, 7 Oct 2024 20:22:24 -0500
Subject: [PATCH 2/2] Remove unnecessary import

---
 ELFSage/Util/ByteArray.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/ELFSage/Util/ByteArray.lean b/ELFSage/Util/ByteArray.lean
index b136e61..ade4f25 100644
--- a/ELFSage/Util/ByteArray.lean
+++ b/ELFSage/Util/ByteArray.lean
@@ -1,5 +1,3 @@
-import Std.Tactic.BVDecide
-
 def ByteArray.getUInt64BEfrom (bs : ByteArray) (offset : Nat) (h: bs.size - offset ≥ 8) : UInt64 :=
   (bs.get ⟨offset + 0, by omega⟩).toUInt64 <<< 0x38 |||
   (bs.get ⟨offset + 1, by omega⟩).toUInt64 <<< 0x30 |||