Add TRN1 and TRN2 from Advanced SIMD permute

Arm/Decode.lean

@@ -100,6 +100,8 @@ def decode_data_proc_sfp (i : BitVec 32) : Option ArmInst :=
     DPSFP (Advanced_simd_copy {Q, op, imm5, imm4, Rn, Rd})
   | [0, Q:1, 101110, op2:2, 0, Rm:5, 0, imm4:4, 0, Rn:5, Rd:5] =>
     DPSFP (Advanced_simd_extract {Q, op2, Rm, imm4, Rn, Rd})
+  | [0, Q:1, 001110, size:2, 0, Rm:5, 0, opcode:3, 10, Rn:5, Rd:5] =>
+    DPSFP (Advanced_simd_permute {Q, size, Rm, opcode, Rn, Rd})
   | [0, Q:1, op:1, 0111100000, a:1, b:1, c:1, cmode:4, o2:1, 1, d:1, e:1, f:1, g:1, h:1, Rd:5] =>
     DPSFP (Advanced_simd_modified_immediate {Q, op, a, b, c, cmode, o2, d, e, f, g, h, Rd})
   | [01, op:1, 11110000, imm5:5, 0, imm4:4, 1, Rn:5, Rd:5] =>

Arm/Decode/DPSFP.lean

@@ -141,6 +141,25 @@ instance : ToString Advanced_simd_extract_cls where toString a := toString (repr
 def Advanced_simd_extract_cls.toBitVec32 (x : Advanced_simd_extract_cls) : BitVec 32 :=
   x._fixed1 ++ x.Q ++ x._fixed2 ++ x.op2 ++ x._fixed3 ++ x.Rm ++ x._fixed4 ++ x.imm4 ++ x._fixed5 ++ x.Rn ++ x.Rd
 
+structure Advanced_simd_permute_cls where
+  _fixed1 : BitVec 1 := 0b0#1      -- [31:31]
+  Q       : BitVec 1               -- [30:30]
+  _fixed2 : BitVec 6 := 0b001110#6 -- [29:24]
+  size    : BitVec 2               -- [23:22]
+  _fixed3 : BitVec 1 := 0b0#1      -- [21:21]
+  Rm      : BitVec 5               -- [20:16]
+  _fixed4 : BitVec 1 := 0b0#1      -- [15:15]
+  opcode  : BitVec 3               -- [14:12]
+  _fixed5 : BitVec 2 := 0b10#2     -- [11:10]
+  Rn      : BitVec 5               --   [9:5]
+  Rd      : BitVec 5               --   [4:0]
+deriving DecidableEq, Repr
+
+instance : ToString Advanced_simd_permute_cls where toString a := toString (repr a)
+
+def Advanced_simd_permute_cls.toBitVec32 (x : Advanced_simd_permute_cls) : BitVec 32 :=
+  x._fixed1 ++ x.Q ++ x._fixed2 ++ x.size ++ x._fixed3 ++ x.Rm ++ x._fixed4 ++ x.opcode ++ x._fixed5 ++ x.Rn ++ x.Rd
+
 structure Advanced_simd_modified_immediate_cls where
   _fixed1 : BitVec 1 := 0b0#1            -- [31:31]
   Q       : BitVec 1                     -- [30:30]
@@ -237,6 +256,8 @@ inductive DataProcSFPInst where
     Advanced_simd_copy_cls → DataProcSFPInst
   | Advanced_simd_extract :
     Advanced_simd_extract_cls → DataProcSFPInst
+  | Advanced_simd_permute :
+    Advanced_simd_permute_cls → DataProcSFPInst
   | Advanced_simd_modified_immediate :
     Advanced_simd_modified_immediate_cls → DataProcSFPInst
   | Advanced_simd_scalar_copy :

Arm/Exec.lean

@@ -52,6 +52,8 @@ def exec_inst (ai : ArmInst) (s : ArmState) : ArmState :=
     DPSFP.exec_advanced_simd_two_reg_misc i s
   | DPSFP (DataProcSFPInst.Advanced_simd_extract i) =>
     DPSFP.exec_advanced_simd_extract i s
+  | DPSFP (DataProcSFPInst.Advanced_simd_permute i) =>
+    DPSFP.exec_advanced_simd_permute i s
   | DPSFP (DataProcSFPInst.Advanced_simd_modified_immediate i) =>
     DPSFP.exec_advanced_simd_modified_immediate i s
   | DPSFP (DataProcSFPInst.Advanced_simd_scalar_copy i) =>

Arm/Insts/Common.lean

@@ -238,10 +238,6 @@ def ldst_write (SIMD? : Bool) (width : Nat) (idx : BitVec 5) (val : BitVec width
 
 ----------------------------------------------------------------------
 
-theorem hi_lo_diff_equal_esize (esize : Nat) (lo : Nat) (hi : Nat) 
-  (h₀ : esize > 0) (h₁ : hi = lo + esize - 1):
-  hi - lo + 1 = esize := by omega
-
 theorem esize_gt_zero (size : Nat):
   8 <<< size > 0 := by
   simp_all only [ Nat.shiftLeft_eq, gt_iff_lt, Nat.zero_lt_succ
@@ -323,4 +319,24 @@ example : rev_vector 32 16 8 0xaabbccdd#32 (by decide)
           0xbbaaddcc#32 := by
           native_decide
 
+----------------------------------------------------------------------
+
+@[simp]
+def Elem_nassign (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
+
+@[simp]
+def Elem_assign (vector : BitVec n) (e : Nat) (size : Nat) 
+  (value : BitVec size) (h: size > 0): BitVec n :=
+  -- assert (e+1)*size <= n
+  let lo := e * size
+  let hi := lo + size - 1
+  have h : hi - lo + 1 = size := by simp only []; omega
+  BitVec.partInstall hi lo (h ▸ value) vector
+
 end Common

Arm/Insts/DPSFP/Advanced_simd_copy.lean

@@ -20,10 +20,7 @@ def dup_aux (e : Nat) (elements : Nat) (esize : Nat)
   if h₀ : e ≥ elements then
     result
   else
-    let lo := e * esize
-    let hi := lo + esize -1
-    have h₁ : hi - lo + 1 = esize := by simp; omega
-    let result := BitVec.partInstall hi lo (h₁ ▸ element) result
+    let result := Elem_assign 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)
@@ -39,12 +36,9 @@ def exec_dup_element (inst : Advanced_simd_copy_cls) (s : ArmState) : ArmState :
     let datasize := 64 <<< inst.Q.toNat
     let elements := datasize / esize
     let operand := read_sfp idxdsize inst.Rn s
-    let lo := index * esize
-    let hi := lo + esize - 1
-    let element := extractLsb hi lo operand
     have h₀ : esize > 0 := by apply esize_gt_zero
-    have h₁ : hi - lo + 1 = esize := by simp; omega
-    let result := dup_aux 0 elements esize (h₁ ▸ element) (Std.BitVec.zero datasize) h₀
+    let element := Elem_nassign 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
     let s := write_sfp datasize inst.Rd result s
@@ -77,17 +71,9 @@ def exec_ins_element (inst : Advanced_simd_copy_cls) (s : ArmState) : ArmState :
     let esize := 8 <<< size
     let operand := read_sfp idxdsize inst.Rn s
     let result := read_sfp 128 inst.Rd s
-    let lo_src := src_index * esize
-    let hi_src := lo_src + esize - 1
-    let elem := extractLsb hi_src lo_src operand
-    let lo_dst := dst_index * esize
-    let hi_dst := lo_dst + esize - 1
     have h₀ : esize > 0 := by apply esize_gt_zero
-    have h : hi_dst - lo_dst + 1 = hi_src - lo_src + 1 := by
-      -- rewrite the LHS and RHS to esize
-      rw [hi_lo_diff_equal_esize _ _ _ h₀ (by simp)]
-      rw [hi_lo_diff_equal_esize _ _ _ h₀ (by simp)]
-    let result := BitVec.partInstall hi_dst lo_dst (h ▸ elem) result
+    let elem := Elem_nassign operand src_index esize h₀
+    let result := Elem_assign 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
@@ -102,11 +88,8 @@ def exec_ins_general (inst : Advanced_simd_copy_cls) (s : ArmState) : ArmState :
     let esize := 8 <<< size
     let element := read_gpr esize inst.Rn s
     let result := read_sfp 128 inst.Rd s
-    let lo := index * esize
-    let hi := lo + esize -1
     have h₀ : esize > 0 := by apply esize_gt_zero
-    have h : hi - lo + 1 = esize := by simp; omega
-    let result := BitVec.partInstall hi lo (h ▸ element) result
+    let result := Elem_assign 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
@@ -126,9 +109,8 @@ def exec_smov_umov (inst : Advanced_simd_copy_cls) (s : ArmState) (signed : Bool
     let idxdsize := 64 <<< (extractLsb 4 4 inst.imm5).toNat
     -- if index == 0 then CheckFPEnabled64 else CheckFPAdvSIMDEnabled64
     let operand := read_sfp idxdsize inst.Rn s
-    let lo := index * esize
-    let hi := lo + esize - 1
-    let element := extractLsb hi lo operand
+    have h₀ : esize > 0 := by apply esize_gt_zero
+    let element := Elem_nassign 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

@@ -0,0 +1,99 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Yan Peng
+-/
+-- TRN1, TRN2
+
+import Arm.Decode
+import Arm.Insts.Common
+
+----------------------------------------------------------------------
+
+namespace DPSFP
+
+open Std.BitVec
+
+def trn_aux (p : Nat) (pairs : Nat) (esize : Nat) (part : Nat)
+  (operand1 : BitVec datasize) (operand2 : BitVec datasize)
+  (result : BitVec datasize) (h : esize > 0) : BitVec datasize :=
+  if h₀ : pairs <= p then
+    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
+    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)
+
+@[simp]
+def exec_trn (inst : Advanced_simd_permute_cls) (s : ArmState) : ArmState :=
+  if inst.size ++ inst.Q == 0b110#3 then
+    write_err (StateError.Illegal s!"Illegal {inst} encountered!") s
+  else
+    let esize := 8 <<< inst.size.toNat
+    let datasize := 64 <<< inst.Q.toNat
+    let elements := datasize / esize
+    let op := extractLsb 2 2 inst.opcode
+    let part := op.toNat
+    let pairs := elements / 2
+    let operand1 := read_sfp datasize inst.Rn s
+    let operand2 := read_sfp datasize inst.Rm s
+    have h : esize > 0 := by apply esize_gt_zero
+    let result := trn_aux 0 pairs esize part operand1 operand2 (Std.BitVec.zero datasize) h
+    -- Update States
+    let s := write_sfp datasize inst.Rd result s
+    let s := write_pc ((read_pc s) + 4#64) s
+    s
+
+@[simp]
+def exec_advanced_simd_permute
+  (inst : Advanced_simd_permute_cls) (s : ArmState) : ArmState :=
+  match inst.opcode with
+  | 0b010#3
+  | 0b110#3 => exec_trn inst s
+  | _ => write_err (StateError.Unimplemented s!"Unsupported {inst} encountered!") s
+
+----------------------------------------------------------------------
+
+partial def Advanced_simd_permute_cls.trn1.rand : IO (Option (BitVec 32)) := do
+  let size := ← BitVec.rand 2
+  let Q := ← BitVec.rand 1
+  if size ++ Q == 0b110#3 then
+    Advanced_simd_permute_cls.trn1.rand
+  else
+    let (inst : Advanced_simd_permute_cls) :=
+      { Q := Q,
+        size := size,
+        Rm := ← BitVec.rand 5,
+        opcode := 0b010#3,
+        Rn := ← BitVec.rand 5,
+        Rd := ← BitVec.rand 5
+      }
+    pure (some (inst.toBitVec32))
+
+partial def Advanced_simd_permute_cls.trn2.rand : IO (Option (BitVec 32)) := do
+  let size := ← BitVec.rand 2
+  let Q := ← BitVec.rand 1
+  if size ++ Q == 0b110#3 then
+    Advanced_simd_permute_cls.trn2.rand
+  else
+    let (inst : Advanced_simd_permute_cls) :=
+      { Q := Q,
+        size := size,
+        Rm := ← BitVec.rand 5,
+        opcode := 0b110#3,
+        Rn := ← BitVec.rand 5,
+        Rd := ← BitVec.rand 5
+      }
+    pure (some (inst.toBitVec32))
+
+/-- Generate random instructions of Advanced_simd_permute class. -/
+def Advanced_simd_permute_cls.rand : List (IO (Option (BitVec 32))) :=
+  [ Advanced_simd_permute_cls.trn1.rand,
+    Advanced_simd_permute_cls.trn2.rand ]
+
+end DPSFP

Arm/Insts/DPSFP/Advanced_simd_scalar_copy.lean

@@ -26,14 +26,11 @@ def exec_advanced_simd_scalar_copy
     let idxdsize := 64 <<< (extractLsb 4 4 inst.imm5).toNat
     let esize := 8 <<< size
     let operand := read_sfp idxdsize inst.Rn s
-    let lo := index.toNat * esize
-    let hi := lo + esize - 1
-    let result := extractLsb hi lo operand
     have h₁ : esize > 0 := by apply esize_gt_zero
-    have h : hi - lo + 1 = esize := by simp; omega
+    let result := Elem_nassign operand index.toNat esize h₁
     -- State Updates
     let s := write_pc ((read_pc s) + 4#64) s
-    let s := write_sfp esize inst.Rd (h ▸ result) s
+    let s := write_sfp esize inst.Rd result s
     s
 
 ----------------------------------------------------------------------

Arm/Insts/DPSFP/Advanced_simd_three_different.lean

@@ -36,16 +36,13 @@ def pmull_op (e : Nat) (esize : Nat) (elements : Nat) (x : BitVec n)
   if h₀ : e ≥ elements then
     result
   else
-    let lo := e * esize
-    let hi := lo + esize - 1
-    let element1 := extractLsb hi lo x
-    let element2 := extractLsb hi lo y
+    let element1 := Elem_nassign x e esize H
+    let element2 := Elem_nassign y e esize H
     let elem_result := polynomial_mult element1 element2
-    let lo2 := 2 * (e * esize)
-    let hi2 := lo2 + 2 * esize - 1
-    have h₁ : hi - lo + 1 + (hi - lo + 1) = hi2 - lo2 + 1 := by simp; omega
-    let result := BitVec.partInstall hi2 lo2 (h₁ ▸ elem_result) result
-    have h₂ : elements - (e + 1) < elements - e := by omega
+    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₂
+    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,13 +24,10 @@ def binary_vector_op_aux (e : Nat) (elems : Nat) (esize : Nat)
     result
   else
     have h₁ : e < elems := by omega
-    let lo := e * esize
-    let hi := lo + esize - 1
-    let element1 := extractLsb hi lo x
-    let element2 := extractLsb hi lo y
-    have h : hi - lo + 1 = esize := by simp; omega
-    let elem_result := op (h ▸ element1) (h ▸ element2)
-    let result := BitVec.partInstall hi lo (h.symm ▸ elem_result) result
+    let element1 := Elem_nassign x e esize H
+    let element2 := Elem_nassign y e esize H
+    let elem_result := op element1 element2
+    let result := Elem_assign 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)

Arm/Insts/DPSFP/Insts.lean

@@ -6,6 +6,7 @@ Author(s): Shilpi Goel
 import Arm.Insts.DPSFP.Advanced_simd_copy
 import Arm.Insts.DPSFP.Advanced_simd_two_reg_misc
 import Arm.Insts.DPSFP.Advanced_simd_extract
+import Arm.Insts.DPSFP.Advanced_simd_permute
 import Arm.Insts.DPSFP.Advanced_simd_modified_immediate
 import Arm.Insts.DPSFP.Advanced_simd_scalar_copy
 import Arm.Insts.DPSFP.Advanced_simd_three_same
@@ -21,6 +22,7 @@ DPSFP class. -/
 def DPSFP.rand : List (IO (Option (BitVec 32))) :=
   DPSFP.Advanced_simd_copy_cls.rand ++
   DPSFP.Advanced_simd_extract_cls.rand ++
+  DPSFP.Advanced_simd_permute_cls.rand ++
   DPSFP.Advanced_simd_modified_immediate_cls.rand ++
   DPSFP.Advanced_simd_scalar_copy_cls.rand ++
   DPSFP.Advanced_simd_three_same_cls.rand ++