From 83a63f477db84ff6c00137744e4506df62188e22 Mon Sep 17 00:00:00 2001
From: Yan Peng <yppe@amazon.com>
Date: Mon, 30 Sep 2024 23:03:46 +0000
Subject: [PATCH] More addressing review

---
 Arm/BitVec.lean              | 14 +++++++++-----
 Arm/Memory/MemoryProofs.lean |  5 ++---
 2 files changed, 11 insertions(+), 8 deletions(-)

diff --git a/Arm/BitVec.lean b/Arm/BitVec.lean
index 501b51f2..76370336 100644
--- a/Arm/BitVec.lean
+++ b/Arm/BitVec.lean
@@ -539,6 +539,12 @@ theorem zeroExtend_if_false [Decidable p] (x : BitVec n)
   (zeroExtend (if p then a else b) x) = BitVec.cast h_eq (zeroExtend b x) := by
   simp only [toNat_eq, toNat_truncate, ← h_eq, toNat_cast]
 
+theorem extractLsb_eq (x : BitVec n) (h : n = n - 1 + 1) :
+  BitVec.extractLsb (n - 1) 0 x = BitVec.cast h x := by
+  unfold extractLsb extractLsb'
+  ext1
+  simp [←h]
+
 theorem extractLsb'_eq (x : BitVec n) :
   BitVec.extractLsb' 0 n x = x := by
   unfold extractLsb'
@@ -626,17 +632,15 @@ theorem append_of_extract_general_nat (high low n vn : Nat) (h : vn < 2 ^ n) :
 
 theorem append_of_extract (n : Nat) (v : BitVec n)
   (high0 : high = n - low) (h : high + low = n) :
-  zeroExtend high (v >>> low) ++ extractLsb' 0 low v = BitVec.cast h.symm v := by
+  BitVec.cast h (zeroExtend high (v >>> low) ++ extractLsb' 0 low v) = v := by
   ext
   subst high
   have vlt := v.isLt
   have := append_of_extract_general_nat (n - low) low n (BitVec.toNat v) vlt
   have low_le : low ≤ n := by omega
-  simp only [toNat_append, toNat_truncate, toNat_ushiftRight, extractLsb'_toNat,
-    Nat.shiftRight_zero, toNat_cast]
-  -- simp_all [toNat_zeroExtend, Nat.sub_add_cancel, low_le]
+  simp_all [toNat_zeroExtend, Nat.sub_add_cancel, low_le]
   rw [Nat.mod_eq_of_lt (b := 2 ^ n)] at this
-  · sorry -- rw [this]
+  · rw [this]
   · rw [Nat.shiftRight_eq_div_pow]
     exact Nat.lt_of_le_of_lt (Nat.div_le_self _ _) vlt
   done
diff --git a/Arm/Memory/MemoryProofs.lean b/Arm/Memory/MemoryProofs.lean
index 98c3bbe9..34a2d63b 100644
--- a/Arm/Memory/MemoryProofs.lean
+++ b/Arm/Memory/MemoryProofs.lean
@@ -65,10 +65,9 @@ theorem append_byte_of_extract_rest_same_cast (n : Nat) (v : BitVec ((n + 1) * 8
   (hn0 : Nat.succ 0 ≤ n)
   (h : (n * 8 + 8) = (n + 1) * 8) :
   BitVec.cast h (zeroExtend (n * 8) (v >>> 8) ++ extractLsb' 0 8 v) = v := by
-  rw [BitVec.append_of_extract]
-  · simp only [BitVec.cast_cast, BitVec.cast_eq]
-  · omega
+  apply BitVec.append_of_extract
   · omega
+  done
 
 @[state_simp_rules]
 theorem read_mem_bytes_of_write_mem_bytes_same (hn1 : n <= 2^64) :