Fixing a couple more foundamental files

pennyannn · Sep 30, 2024 · 86ae42e · 86ae42e
1 parent 4ed62f4
commit 86ae42e
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 6 deletions.
diff --git a/Arm/BitVec.lean b/Arm/BitVec.lean
@@ -289,7 +289,7 @@ abbrev lsb (x : BitVec n) (i : Nat) : BitVec 1 :=
   --   BitVec.extractLsb' i 1 x
   -- and avoid the cast here, but unfortunately, extractLsb' isn't supported
   -- by LeanSAT.
-  (BitVec.extractLsb i i x).cast (by omega)
+  (BitVec.extractLsb' i 1 x).cast (by omega)
 
 abbrev partInstall (hi lo : Nat) (val : BitVec (hi - lo + 1)) (x : BitVec n): BitVec n :=
   let mask := allOnes (hi - lo + 1)
@@ -554,14 +554,12 @@ theorem extractLsb_eq (x : BitVec n) (h : n = n - 1 + 1) :
 
 @[bitvec_rules]
 protected theorem extract_lsb_of_zeroExtend (x : BitVec n) (h : j < i) :
-    extractLsb j 0 (zeroExtend i x) = zeroExtend (j + 1) x := by
+    extractLsb' 0 (j + 1) (zeroExtend i x) = zeroExtend (j + 1) x := by
   apply BitVec.eq_of_getLsbD_eq
   simp
   intro k
   have q : k < i := by omega
   by_cases h : decide (k ≤ j) <;> simp [q, h]
-  simp_all
-  omega
 
 @[bitvec_rules, simp]
 theorem zero_append {w} (x : BitVec 0) (y : BitVec w) :

diff --git a/Arm/State.lean b/Arm/State.lean
@@ -675,7 +675,7 @@ def write_mem_bytes (n : Nat) (addr : BitVec 64) (val : BitVec (n * 8)) (s : Arm
   match n with
   | 0 => s
   | n' + 1 =>
-    let byte := BitVec.extractLsb 7 0 val
+    let byte := BitVec.extractLsb' 0 8 val
     let s := write_mem addr byte s
     let val_rest := BitVec.zeroExtend (n' * 8) (val >>> 8)
     write_mem_bytes n' (addr + 1#64) val_rest s

diff --git a/Proofs/Bit_twiddling.lean b/Proofs/Bit_twiddling.lean
@@ -216,7 +216,7 @@ def popcount32_spec_rec (i : Nat) (x : BitVec 32) : (BitVec 32) :=
   match i with
   | 0 => BitVec.zero 32
   | i' + 1 =>
-    let bit_idx := BitVec.extractLsb i' i' x
+    let bit_idx := BitVec.extractLsb' i' 1 x
     let bv_idx := (BitVec.zeroExtend 32 bit_idx)
     (bv_idx + (popcount32_spec_rec i' x))