Rename Elem_nassign to elem_get and Elem_assign to elem_set and add c…

…omments

Arm/Insts/Common.lean

@@ -321,17 +321,21 @@ example : rev_vector 32 16 8 0xaabbccdd#32 (by decide)
 
 ----------------------------------------------------------------------
 
+/-- Divide bv `vector` into elements, each of size `size`. This function gets
+the `e`'th element from the `vector`. -/
 @[simp]
-def Elem_nassign (vector : BitVec n) (e : Nat) (size : Nat)
+def elem_get (vector : BitVec n) (e : Nat) (size : Nat)
   (h: size > 0): BitVec size :=
   -- assert (e+1)*size <= n
   let lo := e * size
   let hi := lo + size - 1
   have h : hi - lo + 1 = size := by simp only []; omega
   h ▸ extractLsb hi lo vector
 
+/-- Divide bv `vector` into elements, each of size `size`. This function sets
+the `e`'th element in the `vector`. -/
 @[simp]
-def Elem_assign (vector : BitVec n) (e : Nat) (size : Nat) 
+def elem_set (vector : BitVec n) (e : Nat) (size : Nat) 
   (value : BitVec size) (h: size > 0): BitVec n :=
   -- assert (e+1)*size <= n
   let lo := e * size

Arm/Insts/DPSFP/Advanced_simd_copy.lean

@@ -20,7 +20,7 @@ def dup_aux (e : Nat) (elements : Nat) (esize : Nat)
   if h₀ : e ≥ elements then
     result
   else
-    let result := Elem_assign result e esize element H
+    let result := elem_set result e esize element H
     have h : elements - (e + 1) < elements - e := by omega
     dup_aux (e + 1) elements esize element result H
   termination_by dup_aux e elements esize element result H => (elements - e)
@@ -37,7 +37,7 @@ def exec_dup_element (inst : Advanced_simd_copy_cls) (s : ArmState) : ArmState :
     let elements := datasize / esize
     let operand := read_sfp idxdsize inst.Rn s
     have h₀ : esize > 0 := by apply esize_gt_zero
-    let element := Elem_nassign operand index esize h₀
+    let element := elem_get operand index esize h₀
     let result := dup_aux 0 elements esize element (Std.BitVec.zero datasize) h₀
     -- State Updates
     let s := write_pc ((read_pc s) + 4#64) s
@@ -72,8 +72,8 @@ def exec_ins_element (inst : Advanced_simd_copy_cls) (s : ArmState) : ArmState :
     let operand := read_sfp idxdsize inst.Rn s
     let result := read_sfp 128 inst.Rd s
     have h₀ : esize > 0 := by apply esize_gt_zero
-    let elem := Elem_nassign operand src_index esize h₀
-    let result := Elem_assign result dst_index esize elem h₀
+    let elem := elem_get operand src_index esize h₀
+    let result := elem_set result dst_index esize elem h₀
     -- State Updates
     let s := write_pc ((read_pc s) + 4#64) s
     let s := write_sfp 128 inst.Rd result s
@@ -89,7 +89,7 @@ def exec_ins_general (inst : Advanced_simd_copy_cls) (s : ArmState) : ArmState :
     let element := read_gpr esize inst.Rn s
     let result := read_sfp 128 inst.Rd s
     have h₀ : esize > 0 := by apply esize_gt_zero
-    let result := Elem_assign result index esize element h₀
+    let result := elem_set result index esize element h₀
     -- State Updates
     let s := write_pc ((read_pc s) + 4#64) s
     let s := write_sfp 128 inst.Rd result s
@@ -110,7 +110,7 @@ def exec_smov_umov (inst : Advanced_simd_copy_cls) (s : ArmState) (signed : Bool
     -- if index == 0 then CheckFPEnabled64 else CheckFPAdvSIMDEnabled64
     let operand := read_sfp idxdsize inst.Rn s
     have h₀ : esize > 0 := by apply esize_gt_zero
-    let element := Elem_nassign operand index esize h₀
+    let element := elem_get operand index esize h₀
     let result := if signed then signExtend datasize element else zeroExtend datasize element
     -- State Updates
     let s := write_pc ((read_pc s) + 4#64) s

Arm/Insts/DPSFP/Advanced_simd_permute.lean

@@ -21,10 +21,10 @@ def trn_aux (p : Nat) (pairs : Nat) (esize : Nat) (part : Nat)
     result
   else
     let idx_from := 2 * p + part
-    let op1_part := Elem_nassign operand1 idx_from esize h
-    let op2_part := Elem_nassign operand2 idx_from esize h
-    let result := Elem_assign result (2 * p) esize op1_part h
-    let result := Elem_assign result (2 * p + 1) esize op2_part h
+    let op1_part := elem_get operand1 idx_from esize h
+    let op2_part := elem_get operand2 idx_from esize h
+    let result := elem_set result (2 * p) esize op1_part h
+    let result := elem_set result (2 * p + 1) esize op2_part h
     have h₁ : pairs - (p + 1) < pairs - p := by omega
     trn_aux (p + 1) pairs esize part operand1 operand2 result h
   termination_by trn_aux p pairs esize part operand1 operand2 result h => (pairs - p)

Arm/Insts/DPSFP/Advanced_simd_scalar_copy.lean

@@ -27,7 +27,7 @@ def exec_advanced_simd_scalar_copy
     let esize := 8 <<< size
     let operand := read_sfp idxdsize inst.Rn s
     have h₁ : esize > 0 := by apply esize_gt_zero
-    let result := Elem_nassign operand index.toNat esize h₁
+    let result := elem_get operand index.toNat esize h₁
     -- State Updates
     let s := write_pc ((read_pc s) + 4#64) s
     let s := write_sfp esize inst.Rd result s

Arm/Insts/DPSFP/Advanced_simd_three_different.lean

@@ -36,12 +36,12 @@ def pmull_op (e : Nat) (esize : Nat) (elements : Nat) (x : BitVec n)
   if h₀ : e ≥ elements then
     result
   else
-    let element1 := Elem_nassign x e esize H
-    let element2 := Elem_nassign y e esize H
+    let element1 := elem_get x e esize H
+    let element2 := elem_get y e esize H
     let elem_result := polynomial_mult element1 element2
     have h₁ : esize + esize = 2 * esize := by omega
     have h₂ : 2 * esize > 0 := by omega
-    let result := Elem_assign result e (2 * esize) (h₁ ▸ elem_result) h₂
+    let result := elem_set result e (2 * esize) (h₁ ▸ elem_result) h₂
     have _ : elements - (e + 1) < elements - e := by omega
     pmull_op (e + 1) esize elements x y result H
   termination_by pmull_op e esize elements op x y result => (elements - e)

Arm/Insts/DPSFP/Advanced_simd_three_same.lean

@@ -24,10 +24,10 @@ def binary_vector_op_aux (e : Nat) (elems : Nat) (esize : Nat)
     result
   else
     have h₁ : e < elems := by omega
-    let element1 := Elem_nassign x e esize H
-    let element2 := Elem_nassign y e esize H
+    let element1 := elem_get x e esize H
+    let element2 := elem_get y e esize H
     let elem_result := op element1 element2
-    let result := Elem_assign result e esize elem_result H
+    let result := elem_set result e esize elem_result H
     have ht1 : elems - (e + 1) < elems - e := by omega
     binary_vector_op_aux (e + 1) elems esize op x y result H
   termination_by binary_vector_op_aux e elems esize op x y result H => (elems - e)