Addressing comments from Alex

pennyannn · Oct 2, 2024 · 3f87b51 · 3f87b51
1 parent 9fc97da
commit 3f87b51
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 14 deletions.
diff --git a/Arm/BitVec.lean b/Arm/BitVec.lean
@@ -955,7 +955,7 @@ theorem extractLsb'_or (x y : BitVec w₁) (n : Nat) :
 
 -- TODO: upstream
 protected theorem extractLsb'_ofNat (x n : Nat) (l lo : Nat) :
-  extractLsb' lo l (BitVec.ofNat n x) = .ofNat l ((x % 2^n) >>> lo) := by
+    extractLsb' lo l (BitVec.ofNat n x) = .ofNat l ((x % 2^n) >>> lo) := by
   apply eq_of_getLsbD_eq
   intro ⟨i, _lt⟩
   simp [BitVec.ofNat]

diff --git a/Arm/Memory/MemoryProofs.lean b/Arm/Memory/MemoryProofs.lean
@@ -862,14 +862,6 @@ theorem entire_memory_subset_legal_regions_eq_addr
   simp_all [mem_subset, mem_legal]
   bv_omega
 
-private theorem read_mem_bytes_of_write_mem_bytes_subset_n2_eq_alt_helper (val : BitVec (x * 8)):
-  val =
-    extractLsb' ((BitVec.toNat (addr2 - addr2)) * 8) (x * 8) val := by
-  ext
-  simp only [BitVec.sub_self, toNat_ofNat, Nat.zero_mod,
-    Nat.zero_mul, extractLsb'_toNat,
-    Nat.shiftRight_zero, toNat_mod_cancel]
-
 private theorem read_mem_bytes_of_write_mem_bytes_subset_n2_eq_alt
   (h0 : 0 < n1) (h1 : n1 <= my_pow 2 64) (h2 : 0 < n2) (h3 : n2 = my_pow 2 64)
   (h4 : mem_subset addr2 (addr2 + (BitVec.ofNat 64 (n2 - 1))) addr1 (addr1 + (BitVec.ofNat 64 (n1 - 1))))
@@ -883,7 +875,8 @@ private theorem read_mem_bytes_of_write_mem_bytes_subset_n2_eq_alt
     have l1 := @entire_memory_subset_legal_regions_eq_addr addr2 addr1 h4 h6 h5
     subst addr1
     rw [read_mem_bytes_of_write_mem_bytes_same]
-    · apply read_mem_bytes_of_write_mem_bytes_subset_n2_eq_alt_helper
+    · simp only [BitVec.sub_self, toNat_ofNat, Nat.reducePow, Nat.zero_mod, Nat.zero_mul]
+      exact Eq.symm (extractLsb'_eq val)
     · unfold my_pow; decide
 
 @[state_simp_rules]

diff --git a/Specs/AESArm.lean b/Specs/AESArm.lean
@@ -113,10 +113,8 @@ protected def InitKey {Param : KBR} (i : Nat) (key : BitVec Param.key_len)
   match i with
   | 0 => acc
   | i' + 1 =>
-    let i := Param.Nk - i
-    let wd := extractLsb' (i * 32) 32 key
-    let (x:KeySchedule) := [wd]
-    AESArm.InitKey (Param := Param) i' key (acc ++ x)
+    let wd := extractLsb' ((i - 1) * 32) 32 key
+    AESArm.InitKey (Param := Param) i' key (wd :: acc)
 
 protected def KeyExpansion_helper {Param : KBR} (i : Nat) (ks : KeySchedule)
   : KeySchedule :=