Fixing extractLsb to be extractLsb'

Arm/Insts/BR/Cond_branch_imm.lean

@@ -29,7 +29,7 @@ def Cond_branch_imm_inst.condition_holds
   let N := read_flag PFlag.N s
   let V := read_flag PFlag.V s
   let result :=
-    match (extractLsb 3 1 inst.cond) with
+    match (extractLsb' 1 3 inst.cond) with
     | 0b000#3 => Z = 1#1
     | 0b001#3 => C = 1#1
     | 0b010#3 => N = 1#1

Arm/Insts/DPI/Logical_imm.lean

@@ -63,7 +63,7 @@ def MoveWidePreferred (sf immN : BitVec 1) (imms immr : BitVec 6) : Bool :=
       false
     -- NOTE: the second conjunct below is semantically equivalent to the ASL code
     -- !((immN:imms) IN {'00xxxxx'})
-    else if sf = 0#1 ∧ ¬(immN = 0#1 ∧ imms.extractLsb 5 5 = 0#1) then
+    else if sf = 0#1 ∧ ¬(immN = 0#1 ∧ imms.extractLsb' 5 1 = 0#1) then
       false
 
     -- for MOVZ must contain no more than 16 ones

Arm/Insts/DPR/Data_processing_one_source.lean

@@ -55,7 +55,7 @@ private theorem opc_and_sf_constraint (x : BitVec 2) (y : BitVec 1)
 @[state_simp_rules]
 def exec_data_processing_rev
   (inst : Data_processing_one_source_cls) (s : ArmState) : ArmState :=
-  let opc : BitVec 2 := extractLsb 1 0 inst.opcode
+  let opc : BitVec 2 := extractLsb' 0 2 inst.opcode
   if H₁ : opc = 0b11#2 ∧ inst.sf = 0b0#1 then
     write_err (StateError.Illegal s!"Illegal {inst} encountered!") s
   else
@@ -65,16 +65,16 @@ def exec_data_processing_rev
     let esize := 8
     have opc_h₁ : opc.toNat ≥ 0 := by simp only [ge_iff_le, Nat.zero_le]
     have opc_h₂ : opc.toNat < 4 := by
-      refine BitVec.isLt (extractLsb 1 0 inst.opcode)
+      refine BitVec.isLt (extractLsb' 0 2 inst.opcode)
     have opc_sf_h : ¬(opc.toNat = 3 ∧ inst.sf.toNat = 0) := by
-      apply opc_and_sf_constraint (extractLsb 1 0 inst.opcode) inst.sf H₁
+      apply opc_and_sf_constraint (extractLsb' 0 2 inst.opcode) inst.sf H₁
     have h₀ : 0 < esize := by decide
     have h₁ : esize ≤ container_size := by apply shiftLeft_ge
     have h₂ : container_size ≤ datasize := by
       apply container_size_le_datasize opc.toNat inst.sf.toNat opc_h₁ opc_h₂ opc_sf_h
     have h₃ : esize ∣ container_size := by
       simp only [esize, container_size]
-      generalize BitVec.toNat (extractLsb 1 0 inst.opcode) = x
+      generalize BitVec.toNat (extractLsb' 0 2 inst.opcode) = x
       simp only [Nat.shiftLeft_eq]
       generalize 2 ^ x = n
       simp only [Nat.dvd_mul_right]

Arm/Insts/DPR/Data_processing_two_source.lean

@@ -19,7 +19,7 @@ open BitVec
 def exec_data_processing_shift
   (inst : Data_processing_two_source_cls) (s : ArmState) : ArmState :=
   let datasize := 32 <<< inst.sf.toNat
-  let shift_type := decode_shift $ extractLsb 1 0 inst.opcode
+  let shift_type := decode_shift $ extractLsb' 0 2 inst.opcode
   let operand2 := read_gpr_zr datasize inst.Rm s
   let amount := BitVec.ofInt 6 (operand2.toInt % datasize)
   let operand := read_gpr_zr datasize inst.Rn s

Arm/Insts/DPSFP/Advanced_simd_copy.lean

@@ -32,7 +32,7 @@ def exec_dup_element (inst : Advanced_simd_copy_cls) (s : ArmState) : ArmState :
   if size > 3 ∨ (size = 3 ∧ inst.Q = 0) then
     write_err (StateError.Illegal s!"Illegal {inst} encountered!") s
   else
-    let index := (extractLsb 4 (size + 1) inst.imm5).toNat
+    let index := (extractLsb' (size + 1) (4 - size) inst.imm5).toNat
     let idxdsize := 64 <<< (lsb inst.imm5 4).toNat
     let esize := 8 <<< size
     let datasize := 64 <<< inst.Q.toNat
@@ -69,8 +69,8 @@ def exec_ins_element (inst : Advanced_simd_copy_cls) (s : ArmState) : ArmState :
   if size > 3 then
     write_err (StateError.Illegal s!"Illegal {inst} encountered!") s
   else
-    let dst_index := (extractLsb 4 (size + 1) inst.imm5).toNat
-    let src_index := (extractLsb 3 size inst.imm4).toNat
+    let dst_index := (extractLsb' (size + 1) (4 - size) inst.imm5).toNat
+    let src_index := (extractLsb' size (4 - size) inst.imm4).toNat
     let idxdsize := 64 <<< (lsb inst.imm4 3).toNat
     let esize := 8 <<< size
     let operand := read_sfp idxdsize inst.Rn s
@@ -89,7 +89,7 @@ def exec_ins_general (inst : Advanced_simd_copy_cls) (s : ArmState) : ArmState :
   if size > 3 then
     write_err (StateError.Illegal s!"Illegal {inst} encountered!") s
   else
-    let index := (extractLsb 4 (size + 1) inst.imm5).toNat
+    let index := (extractLsb' (size + 1) (4 - size) inst.imm5).toNat
     let esize := 8 <<< size
     let element := read_gpr esize inst.Rn s
     let result := read_sfp 128 inst.Rd s
@@ -113,7 +113,7 @@ def exec_smov_umov (inst : Advanced_simd_copy_cls) (s : ArmState) (signed : Bool
            (datasize = 32 ∧ esize >= 64)) then
      write_err (StateError.Illegal s!"Illegal {inst} encountered!") s
   else
-    let index := (extractLsb 4 (size + 1) inst.imm5).toNat
+    let index := (extractLsb' (size + 1) (4 - size) inst.imm5).toNat
     let idxdsize := 64 <<< (lsb inst.imm5 4).toNat
     -- if index == 0 then CheckFPEnabled64 else CheckFPAdvSIMDEnabled64
     let operand := read_sfp idxdsize inst.Rn s

Arm/Insts/DPSFP/Advanced_simd_extract.lean

@@ -31,12 +31,12 @@ def exec_advanced_simd_extract
     let hi := read_sfp datasize inst.Rm s
     let lo := read_sfp datasize inst.Rn s
     let concat := hi ++ lo
-    let result := extractLsb (position + datasize - 1) position concat
+    let result := extractLsb' position datasize concat
     have h_datasize : 1 <= datasize := by simp_all! [datasize]; split <;> decide
     have h : (position + datasize - 1 - position + 1) = datasize := by
       rw [Nat.add_sub_assoc, Nat.add_sub_self_left]
       exact Nat.sub_add_cancel h_datasize; trivial
-    let s := write_sfp datasize inst.Rd (BitVec.cast h result) s
+    let s := write_sfp datasize inst.Rd result s
     let s := write_pc ((read_pc s) + 4#64) s
     s
 

Arm/Insts/DPSFP/Advanced_simd_modified_immediate.lean

@@ -52,7 +52,7 @@ def decode_immediate_op (inst : Advanced_simd_modified_immediate_cls)
            else (some ImmediateOp.MOVI, s)
 
 def AdvSIMDExpandImm (op : BitVec 1) (cmode : BitVec 4) (imm8 : BitVec 8) : BitVec 64 :=
-  let cmode_high3 := extractLsb 3 1 cmode
+  let cmode_high3 := extractLsb' 1 3 cmode
   let cmode_low1 := lsb cmode 0
   match cmode_high3 with
   | 0b000#3 => replicate 2 $ BitVec.zero 24 ++ imm8
@@ -82,13 +82,13 @@ def AdvSIMDExpandImm (op : BitVec 1) (cmode : BitVec 4) (imm8 : BitVec 8) : BitV
     else if cmode_low1 = 1 ∧ op = 0 then
       let imm32 := lsb imm8 7 ++ ~~~(lsb imm8 6) ++
                    (replicate 5 $ lsb imm8 6) ++
-                   extractLsb 5 0 imm8 ++ BitVec.zero 19
+                   extractLsb' 0 6 imm8 ++ BitVec.zero 19
       replicate 2 imm32
     else
       -- Assume not UsingAArch32()
       -- if UsingAArch32() then ReservedEncoding();
       lsb imm8 7 ++ ~~~(lsb imm8 6) ++
-        (replicate 8 $ lsb imm8 6) ++ extractLsb 5 0 imm8 ++ BitVec.zero 48
+        (replicate 8 $ lsb imm8 6) ++ extractLsb' 0 6 imm8 ++ BitVec.zero 48
 
 
 private theorem mul_div_norm_form_lemma  (n m : Nat) (_h1 : 0 < m) (h2 : n ∣ m) :
@@ -107,9 +107,9 @@ def exec_advanced_simd_modified_immediate
     let datasize := 64 <<< inst.Q.toNat
     let imm8 := inst.a ++ inst.b ++ inst.c ++ inst.d ++ inst.e ++ inst.f ++ inst.g ++ inst.h
     let imm16 : BitVec 16 :=
-                 extractLsb 7 7 imm8 ++ ~~~ (extractLsb 6 6 imm8) ++
-                 (replicate 2 $ extractLsb 6 6 imm8) ++ extractLsb 5 0 imm8 ++
-                 BitVec.zero 6
+                 extractLsb' 7 1 imm8 ++ ~~~ (extractLsb' 6 1 imm8) ++
+                 (replicate 2 $ extractLsb' 6 1 imm8) ++
+                 extractLsb' 0 6 imm8 ++ BitVec.zero 6
     let imm64 := AdvSIMDExpandImm inst.op inst.cmode imm8
     have h₁ : 16 * (datasize / 16) = datasize := by omega
     have h₂ : 64 * (datasize / 64) = datasize := by omega

Arm/Insts/DPSFP/Advanced_simd_scalar_copy.lean

@@ -23,7 +23,7 @@ def exec_advanced_simd_scalar_copy
   if size > 3 ∨ inst.imm4 ≠ 0b0000#4 ∨ inst.op ≠ 0 then
     write_err (StateError.Illegal s!"Illegal {inst} encountered!") s
   else
-    let index := extractLsb 4 (size + 1) inst.imm5
+    let index := extractLsb' (size + 1) (4 - size) inst.imm5
     let idxdsize := 64 <<< (lsb inst.imm5 4).toNat
     let esize := 8 <<< size
     let operand := read_sfp idxdsize inst.Rn s

Arm/Insts/DPSFP/Conversion_between_FP_and_Int.lean

@@ -32,10 +32,9 @@ def fmov_general_aux (intsize : Nat) (fltsize : Nat) (op : FPConvOp)
     s
   | FPConvOp.FPConvOp_MOV_ItoF =>
     let intval := read_gpr intsize inst.Rn s
-    let fltval := extractLsb (fltsize - 1) 0 intval
+    let fltval := extractLsb' 0 fltsize intval
     -- State Update
-    have h₀ : fltsize - 1 - 0 + 1 = fltsize := by omega
-    let s := Vpart_write inst.Rd part fltsize (BitVec.cast h₀ fltval) s
+    let s := Vpart_write inst.Rd part fltsize fltval s
     let s := write_pc ((read_pc s) + 4#64) s
     s
   | _ => write_err (StateError.Other s!"fmov_general_aux called with non-FMOV op!") s
@@ -51,7 +50,7 @@ def exec_fmov_general
     · decide
     · generalize BitVec.toNat (inst.ftype ^^^ 2#2) = x
       apply zero_lt_shift_left_pos (by decide)
-  match (extractLsb 2 1 inst.opcode) ++ inst.rmode with
+  match (extractLsb' 1 2 inst.opcode) ++ inst.rmode with
   | 1100 =>  -- FMOV
     if decode_fltsize ≠ 16 ∧ decode_fltsize ≠ intsize then
       write_err (StateError.Illegal s!"Illegal {inst} encountered!") s
@@ -75,7 +74,7 @@ def exec_fmov_general
 @[state_simp_rules]
 def exec_conversion_between_FP_and_Int
   (inst : Conversion_between_FP_and_Int_cls) (s : ArmState) : ArmState :=
-  if inst.ftype = 0b10#2 ∧ (extractLsb 2 1 inst.opcode) ++ inst.rmode ≠ 0b1101#4 then
+  if inst.ftype = 0b10#2 ∧ (extractLsb' 1 2 inst.opcode) ++ inst.rmode ≠ 0b1101#4 then
     write_err (StateError.Illegal s!"Illegal {inst} encountered!") s
     -- Assume IsFeatureImplemented(FEAT_FP16) is true
   else
@@ -92,7 +91,7 @@ partial def Conversion_between_FP_and_Int_cls.fmov_general.rand : Cosim.CosimM (
   let sf := ← BitVec.rand 1
   let intsize := 32 <<< sf.toNat
   let decode_fltsize := if ftype == 0b10#2 then 64 else (8 <<< (ftype ^^^ 0b10#2).toNat)
-  if ftype == 0b10#2 && ((extractLsb 2 1 opcode) ++ rmode) != 0b1101#4 ||
+  if ftype == 0b10#2 && ((extractLsb' 1 2 opcode) ++ rmode) != 0b1101#4 ||
      decode_fltsize != 16 && decode_fltsize != intsize ||
      intsize != 64 || ftype != 0b10#2 then
     Conversion_between_FP_and_Int_cls.fmov_general.rand

Arm/Insts/DPSFP/Crypto_aes.lean

@@ -53,7 +53,7 @@ def FFmul02 (b : BitVec 8) : BitVec 8 :=
     ]
   let lo := b.toNat * 8
   let hi := lo + 7
-  BitVec.cast (by omega) $ extractLsb hi lo $ BitVec.flatten FFmul_02
+  extractLsb' lo 8 $ BitVec.flatten FFmul_02
 
 def FFmul03 (b : BitVec 8) : BitVec 8 :=
   let FFmul_03 :=
@@ -76,8 +76,7 @@ def FFmul03 (b : BitVec 8) : BitVec 8 :=
       0x111217141D1E1B18090A0F0C05060300#128  -- 0
     ]
   let lo := b.toNat * 8
-  let hi := lo + 7
-  BitVec.cast (by omega) $ extractLsb hi lo $ BitVec.flatten FFmul_03
+  extractLsb' lo 8 $ BitVec.flatten FFmul_03
 
 def AESMixColumns (op : BitVec 128) : BitVec 128 :=
   AESCommon.MixColumns op FFmul02 FFmul03

Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean

@@ -21,14 +21,14 @@ open BitVec
 def sha512h (x : BitVec 128) (y : BitVec 128) (w : BitVec 128)
   : BitVec 128 :=
   open sha512_helpers in
-  let y_127_64    := extractLsb 127 64 y
-  let y_63_0      := extractLsb 63 0 y
+  let y_127_64    := extractLsb' 64 64 y
+  let y_63_0      := extractLsb' 0 64 y
   let msigma1     := sigma_big_1 y_127_64
-  let x_63_0      := extractLsb 63 0 x
-  let x_127_64    := extractLsb 127 64 x
+  let x_63_0      := extractLsb' 0 64 x
+  let x_127_64    := extractLsb' 64 64 x
   let vtmp_127_64 := ch y_127_64 x_63_0 x_127_64
-  let w_127_64    := extractLsb 127 64 w
-  let w_63_0      := extractLsb 63 0 w
+  let w_127_64    := extractLsb' 64 64 w
+  let w_63_0      := extractLsb' 0 64 w
   let vtmp_127_64 := vtmp_127_64 + msigma1 + w_127_64
   let tmp         := vtmp_127_64 + y_63_0
   let msigma1     := sigma_big_1 tmp
@@ -40,32 +40,32 @@ def sha512h (x : BitVec 128) (y : BitVec 128) (w : BitVec 128)
 def sha512h2 (x : BitVec 128) (y : BitVec 128) (w : BitVec 128) :
     BitVec 128 :=
     open sha512_helpers in
-    let y_63_0      := extractLsb 63 0 y
-    let y_127_64    := extractLsb 127 64 y
+    let y_63_0      := extractLsb' 0 64 y
+    let y_127_64    := extractLsb' 64 64 y
     let nsigma0     := sigma_big_0 y_63_0
-    let x_63_0      := extractLsb 63 0 x
+    let x_63_0      := extractLsb' 0 64 x
     let vtmp_127_64 := maj x_63_0 y_127_64 y_63_0
-    let w_127_64    := extractLsb 127 64 w
+    let w_127_64    := extractLsb' 64 64 w
     let vtmp_127_64 := vtmp_127_64 + nsigma0 + w_127_64
     let nsigma0     := sigma_big_0 vtmp_127_64
     let vtmp_63_0   := maj vtmp_127_64 y_63_0 y_127_64
-    let w_63_0      := extractLsb 63 0 w
+    let w_63_0      := extractLsb' 0 64 w
     let vtmp_63_0   := vtmp_63_0 + nsigma0 + w_63_0
     let result      := vtmp_127_64 ++ vtmp_63_0
     result
 
 def sha512su1 (x : BitVec 128) (y : BitVec 128) (w : BitVec 128)
   : BitVec 128 :=
   open sha512_helpers in
-  let x_127_64    := extractLsb 127 64 x
+  let x_127_64    := extractLsb' 64 64 x
   let sig1        := sigma_1 x_127_64
-  let w_127_64    := extractLsb 127 64 w
-  let y_127_64    := extractLsb 127 64 y
+  let w_127_64    := extractLsb' 64 64 w
+  let y_127_64    := extractLsb' 64 64 y
   let vtmp_127_64 := w_127_64 + sig1 + y_127_64
-  let x_63_0      := extractLsb 63 0 x
+  let x_63_0      := extractLsb' 0 64 x
   let sig1        := sigma_1 x_63_0
-  let w_63_0      := extractLsb 63 0 w
-  let y_63_0      := extractLsb 63 0 y
+  let w_63_0      := extractLsb' 0 64 w
+  let y_63_0      := extractLsb' 0 64 y
   let vtmp_63_0   := w_63_0 + sig1 + y_63_0
   let result      := vtmp_127_64 ++ vtmp_63_0
   result

Arm/Insts/DPSFP/Crypto_two_reg_sha512.lean

@@ -19,10 +19,10 @@ open BitVec
 def sha512su0 (x : BitVec 128) (w : BitVec 128)
   : BitVec 128 :=
   open sha512_helpers in
-  let w_127_64    := extractLsb 127 64 w
-  let w_63_0      := extractLsb 63 0 w
+  let w_127_64    := extractLsb' 64 64 w
+  let w_63_0      := extractLsb' 0 64 w
   let sig0        := sigma_0 w_127_64
-  let x_63_0      := extractLsb 63 0 x
+  let x_63_0      := extractLsb' 0 64 x
   let vtmp_63_0   := w_63_0 + sig0
   let sig0        := sigma_0 x_63_0
   let vtmp_127_64 := w_127_64 + sig0

Arm/Insts/LDST/Reg_pair.lean

@@ -64,18 +64,15 @@ def reg_pair_operation (inst : Reg_pair_cls) (inst_str : String) (signed : Bool)
         let full_data := data2 ++ data1
         write_mem_bytes (2 * (datasize / 8)) address (BitVec.cast h3 full_data) s
       | _ => -- LOAD
-        have h4 : datasize - 1 - 0 + 1 = datasize := by
-          simp; apply Nat.sub_add_cancel H2
-        have h5 : 2 * datasize - 1 - datasize + 1 = datasize := by omega
         let full_data := read_mem_bytes (2 * (datasize / 8)) address s
-        let data1 := extractLsb (datasize - 1) 0 full_data
-        let data2 := extractLsb ((2 * datasize) - 1) datasize full_data
+        let data1 := extractLsb' 0 datasize full_data
+        let data2 := extractLsb' datasize datasize full_data
         if not inst.SIMD? ∧ signed then
           let s := write_gpr 64 inst.Rt (signExtend 64 data1) s
           write_gpr 64 inst.Rt2 (signExtend 64 data2) s
         else
-          let s:= ldst_write inst.SIMD? datasize inst.Rt (BitVec.cast h4 data1) s
-          ldst_write inst.SIMD? datasize inst.Rt2 (BitVec.cast h5 data2) s
+          let s:= ldst_write inst.SIMD? datasize inst.Rt data1 s
+          ldst_write inst.SIMD? datasize inst.Rt2 data2 s
     if inst.wback then
       let address := if inst.postindex then address + offset else address
       write_gpr 64 inst.Rn address s

Arm/Insts/LDST/Reg_unscaled_imm.lean

@@ -17,7 +17,7 @@ open BitVec
 @[state_simp_rules]
 def exec_ldstur
   (inst : Reg_unscaled_imm_cls) (s : ArmState) : ArmState :=
-  let scale := (extractLsb 1 1 inst.opc ++ inst.size).toNat
+  let scale := (extractLsb' 1 1 inst.opc ++ inst.size).toNat
   if scale > 4 then
     write_err (StateError.Illegal s!"Illegal {inst} encountered!") s
   else
@@ -44,9 +44,9 @@ def exec_ldstur
 @[state_simp_rules]
 def exec_reg_unscaled_imm
   (inst : Reg_unscaled_imm_cls) (s : ArmState) : ArmState :=
-  if inst.VR = 0b1#1 then 
+  if inst.VR = 0b1#1 then
     exec_ldstur inst s
-  else 
+  else
     write_err (StateError.Unimplemented s!"Unsupported instruction {inst} encountered!") s
 
 end LDST

Arm/Memory/MemoryProofs.lean

@@ -317,7 +317,7 @@ private theorem mem_subset_neq_first_addr_small_second_region
   cases h2
   · rename_i h
     simp only [BitVec.add_sub_self_left_64] at h
-    have l1 : n' = 18446744073709551615 := by      
+    have l1 : n' = 18446744073709551615 := by
       rw [BitVec.toNat_eq] at h
       simp only [toNat_ofNat, Nat.reducePow, Nat.reduceMod] at h
       omega

Specs/AESArm.lean

@@ -112,9 +112,7 @@ protected def InitKey {Param : KBR} (i : Nat) (key : BitVec Param.key_len)
   (acc : KeySchedule) : KeySchedule :=
   if h₀ : Param.Nk ≤ i then acc
   else
-    have h₁ : i * 32 + 32 - 1 - i * 32 + 1 = WordSize := by
-      simp only [WordSize]; omega
-    let wd := BitVec.cast h₁ $ extractLsb (i * 32 + 32 - 1) (i * 32) key
+    let wd := extractLsb' (i * 32) 32 key
     let (x:KeySchedule) := [wd]
     have _ : Param.Nk - (i + 1) < Param.Nk - i := by omega
     AESArm.InitKey (Param := Param) (i + 1) key (acc ++ x)