Merge pull request #7 from pennyannn/yppe/addsub

Add ADD, SUB, ADDS, SUBS (shifted register) and SUB (vector)

Arm/Decode.lean

@@ -71,6 +71,8 @@ def decode_data_proc_reg (i : BitVec 32) : Option ArmInst :=
   match_bv i with
   | [sf:1, op:1, S:1, 11010000, Rm:5, 000000, Rn:5, Rd:5] =>
     DPR (Add_sub_carry {sf, op, S, Rm, Rn, Rd})
+  | [sf:1, op:1, S:1, 01011, shift:2, 0, Rm:5, imm6:6 , Rn:5, Rd:5] =>
+    DPR (Add_sub_shifted_reg {sf, op, S, shift, Rm, imm6, Rn, Rd})
   | [sf:1, op:1, S:1, 11010100, Rm:5, cond:4, op2:2, Rn:5, Rd:5] =>
     DPR (Conditional_select {sf, op, S, Rm, cond, op2, Rn, Rd})
   | [sf:1, opc:2, 01010, shift:2, N:1, Rm:5, imm6:6, Rn:5, Rd:5] =>
@@ -373,6 +375,21 @@ example : decode_raw_inst 0xd2524b8f#32 =
             Rd := 0x0f#5 })) := by
         rfl
 
+-- sub x9, x27, x15, lsl #55
+example : decode_raw_inst 0xcb0fdf69 =
+          (ArmInst.DPR (DataProcRegInst.Add_sub_shifted_reg
+          { sf := 0x1#1,
+            op := 0x1#1,
+            S := 0x0#1,
+            _fixed1 := 0x0b#5,
+            shift := 0x0#2,
+            _fixed2 := 0x0#1,
+            Rm := 0x0f#5,
+            imm6 := 0x37#6,
+            Rn := 0x1b#5,
+            Rd := 0x09#5 })) := by
+        rfl
+
 -- Unimplemented
 example : decode_raw_inst 0x00000000#32 = none := by rfl
 

Arm/Decode/DPR.lean

@@ -1,6 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Author(s): Shilpi Goel
+Author(s): Shilpi Goel, Yan Peng
 -/
 import Arm.BitVec
 
@@ -28,6 +28,24 @@ instance : ToString Add_sub_carry_cls where toString a := toString (repr a)
 def Add_sub_carry_cls.toBitVec32 (x : Add_sub_carry_cls) : BitVec 32 :=
   x.sf ++ x.op ++ x.S ++ x._fixed1 ++ x.Rm ++ x._fixed2 ++ x.Rn ++ x.Rd
 
+structure Add_sub_shifted_reg_cls where
+  sf      : BitVec 1                 -- [31:31]
+  op      : BitVec 1                 -- [30:30]
+  S       : BitVec 1                 -- [29:29]
+  _fixed1 : BitVec 5 := 0b01011#5    -- [28:24]
+  shift   : BitVec 2                 -- [23:22]
+  _fixed2 : BitVec 1 := 0            -- [21:21]
+  Rm      : BitVec 5                 -- [20:16]
+  imm6    : BitVec 6                 -- [15:10]
+  Rn      : BitVec 5                 --   [9:5]
+  Rd      : BitVec 5                 --   [4:0]
+deriving DecidableEq, Repr
+
+instance : ToString Add_sub_shifted_reg_cls where toString a := toString (repr a)
+
+def Add_sub_shifted_reg_cls.toBitVec32 (x : Add_sub_shifted_reg_cls) : BitVec 32 :=
+  x.sf ++ x.op ++ x.S ++ x._fixed1 ++ x.shift ++ x._fixed2 ++ x.Rm ++ x.imm6 ++ x.Rn ++ x.Rd
+
 structure Conditional_select_cls where
   sf     : BitVec 1                 -- [31:31]
   op     : BitVec 1                 -- [30:30]
@@ -65,6 +83,8 @@ def Logical_shifted_reg_cls.toBitVec32 (x : Logical_shifted_reg_cls) : BitVec 32
 inductive DataProcRegInst where
   | Add_sub_carry :
     Add_sub_carry_cls → DataProcRegInst
+  | Add_sub_shifted_reg :
+    Add_sub_shifted_reg_cls → DataProcRegInst
   | Conditional_select :
     Conditional_select_cls → DataProcRegInst
   | Logical_shifted_reg :

Arm/Exec.lean

@@ -28,6 +28,8 @@ def exec_inst (ai : ArmInst) (s : ArmState) : ArmState :=
 
   | DPR (DataProcRegInst.Add_sub_carry i) =>
     DPR.exec_add_sub_carry i s
+  | DPR (DataProcRegInst.Add_sub_shifted_reg i) =>
+    DPR.exec_add_sub_shifted_reg i s
   | DPR (DataProcRegInst.Conditional_select i) =>
     DPR.exec_conditional_select i s
   | DPR (DataProcRegInst.Logical_shifted_reg i) =>

Arm/Insts/DPR/Add_sub_shifted_reg.lean

@@ -0,0 +1,62 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Author(s): Yan Peng
+-/
+-- ADD, ADDS, SUB, SUBS (shifted registers): 32- and 64-bit versions
+
+import Arm.Decode
+import Arm.Insts.Common
+
+namespace DPR
+
+open Std.BitVec
+
+@[simp]
+def exec_add_sub_shifted_reg (inst : Add_sub_shifted_reg_cls) (s : ArmState) : ArmState :=
+  let datasize := 32 <<< inst.sf.toNat
+  if inst.shift == 0b11#2 then
+    write_err (StateError.Illegal s!"Illegal {inst} encountered!") s
+  else if inst.sf == 0 && extractLsb 5 5 inst.imm6 == 1 then
+    write_err (StateError.Illegal s!"Illegal {inst} encountered!") s
+  else
+    let sub_op := inst.op == 1#1
+    let setflags := inst.S == 1#1
+    let shift_type := decode_shift inst.shift
+    let operand1 := read_gpr_zr datasize inst.Rn s
+    let operand2_unshifted := read_gpr_zr datasize inst.Rm s
+    let operand2 := shift_reg operand2_unshifted shift_type inst.imm6
+    let operand2 := if sub_op then ~~~operand2 else operand2
+    let carry := if sub_op then 1 else 0
+    let (result, pstate) := AddWithCarry operand1 operand2 carry
+    -- State Updates
+    let s'            := write_pc ((read_pc s) + 4#64) s
+    let s'            := if setflags then write_pstate pstate s' else s'
+    let s'            := write_gpr_zr datasize inst.Rd result s'
+    s'
+
+----------------------------------------------------------------------
+
+/-- Generate random instructions of the DPR.Add_sub_shifted_reg class. -/
+partial def Add_sub_shifted_reg_cls.rand : IO (Option (BitVec 32)) := do
+  let shift := ← BitVec.rand 2
+  let sf := ← BitVec.rand 1
+  let imm6 := ← BitVec.rand 6
+  if shift == 0b11#2 then
+    Add_sub_shifted_reg_cls.rand
+  else if sf == 0 && extractLsb 5 5 imm6 == 1 then
+    Add_sub_shifted_reg_cls.rand
+  else
+    let (inst : Add_sub_shifted_reg_cls) :=
+      { sf    := sf,
+        op    := ← BitVec.rand 1,
+        S     := ← BitVec.rand 1,
+        shift := shift,
+        Rm    := ← BitVec.rand 5,
+        imm6  := imm6,
+        Rn    := ← BitVec.rand 5,
+        Rd    := ← BitVec.rand 5 }
+    pure (some (inst.toBitVec32))
+
+----------------------------------------------------------------------
+
+end DPR

Arm/Insts/DPR/Insts.lean

@@ -3,12 +3,14 @@ Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
 Author(s): Shilpi Goel
 -/
 import Arm.Insts.DPR.Add_sub_carry
+import Arm.Insts.DPR.Add_sub_shifted_reg
 import Arm.Insts.DPR.Conditional_select
 import Arm.Insts.DPR.Logical_shifted_reg
 
 /-- List of functions to generate random instructions of the
 DPR class. -/
 def DPR.rand : List (IO (Option (BitVec 32))) :=
   [DPR.Add_sub_carry_cls.rand,
+   DPR.Add_sub_shifted_reg_cls.rand,
    DPR.Conditional_select_cls.rand,
    DPR.Logical_shifted_reg_cls.rand]

Arm/Insts/DPSFP/Advanced_simd_three_same.lean

@@ -15,10 +15,10 @@ namespace DPSFP
 
 open Std.BitVec
 
-theorem add_vector_op_helper_lemma (x y : Nat) (h : 0 < y) :
+theorem binary_vector_op_aux_helper_lemma (x y : Nat) (h : 0 < y) :
   x + y - 1 - x + 1 = y := by omega
 
-def add_vector_op (e : Nat) (elems : Nat) (esize : Nat)
+def binary_vector_op_aux (e : Nat) (elems : Nat) (esize : Nat)
   (op : BitVec esize → BitVec esize → BitVec esize)
   (x : BitVec n) (y : BitVec n) (result : BitVec n)
   (H : esize > 0) : BitVec n :=
@@ -31,17 +31,23 @@ def add_vector_op (e : Nat) (elems : Nat) (esize : Nat)
     let element1 := extractLsb hi lo x
     let element2 := extractLsb hi lo y
     have h : hi - lo + 1 = esize := by
-      simp; apply add_vector_op_helper_lemma; simp [*] at *
+      simp; apply binary_vector_op_aux_helper_lemma; simp [*] at *
     let elem_result := op (h ▸ element1) (h ▸ element2)
     let result := BitVec.partInstall hi lo (h.symm ▸ elem_result) result
     have ht1 : elems - (e + 1) < elems - e := by omega
-    add_vector_op (e + 1) elems esize op x y result H
-  termination_by add_vector_op e elems esize op x y result H => (elems - e)
+    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)
 
--- #eval add_vector_op 0 2 4 Std.BitVec.add 0xAB 0x12 (Std.BitVec.zero 8)
+/--
+  Perform pairwise op on esize-bit slices of x and y
+-/
+@[simp]
+def binary_vector_op (esize : Nat) (op : BitVec esize → BitVec esize → BitVec esize)
+  (x : BitVec n) (y : BitVec n) (H : esize > 0) : BitVec n :=
+  binary_vector_op_aux 0 (n / esize) esize op x y (Std.BitVec.zero n) H
 
 @[simp]
-def exec_add_vector (inst : Advanced_simd_three_same_cls) (s : ArmState) : ArmState :=
+def exec_binary_vector (inst : Advanced_simd_three_same_cls) (s : ArmState) : ArmState :=
   if inst.size == 0b11#2 && inst.Q == 0b0#1 then
     write_err (StateError.Illegal s!"Illegal {inst} encountered!") s
   else
@@ -51,10 +57,11 @@ def exec_add_vector (inst : Advanced_simd_three_same_cls) (s : ArmState) : ArmSt
       simp_all only [Nat.shiftLeft_eq, gt_iff_lt, 
                      Nat.zero_lt_succ, mul_pos_iff_of_pos_left, 
                      zero_lt_two, pow_pos]
-    let elements := datasize / esize
+    let sub_op := inst.U == 1
     let operand1 := read_sfp datasize inst.Rn s
     let operand2 := read_sfp datasize inst.Rm s
-    let result := add_vector_op 0 elements esize Std.BitVec.add operand1 operand2 (Std.BitVec.zero datasize) h_esize
+    let op := if sub_op then Std.BitVec.sub else Std.BitVec.add
+    let result := binary_vector_op esize op operand1 operand2 h_esize
     let s := write_sfp datasize inst.Rd result s
     s
 
@@ -98,10 +105,10 @@ def exec_advanced_simd_three_same
   (inst : Advanced_simd_three_same_cls) (s : ArmState) : ArmState :=
   open Std.BitVec in
   let s :=
-    match inst.U, inst.size, inst.opcode with
-    | 0#1, _, 0b10000#5 => exec_add_vector inst s
-    | _, _, 0b00011#5 => exec_logic_vector inst s
-    | _, _, _ =>
+    match inst.opcode with
+    | 0b10000#5 => exec_binary_vector inst s
+    | 0b00011#5 => exec_logic_vector inst s
+    | _ =>
       write_err (StateError.Unimplemented s!"Unsupported instruction {inst} encountered!") s
   write_pc ((read_pc s) + 4#64) s
 
@@ -112,20 +119,20 @@ theorem pc_of_exec_advanced_simd_three_same
   -- (r StateField.PC s) + 4#64 -- TODO: How do I use + here?
   (Std.BitVec.add (r StateField.PC s) 4#64) := by
   simp_all!
-  simp [exec_advanced_simd_three_same, exec_add_vector, exec_logic_vector]
+  simp [exec_advanced_simd_three_same, exec_binary_vector, exec_logic_vector]
   split
   · split <;> simp
   · simp
   · simp
 
 ----------------------------------------------------------------------
 
-def Advanced_simd_three_same_cls.add.rand : IO (Option (BitVec 32)) := do
+def Advanced_simd_three_same_cls.binary.rand : IO (Option (BitVec 32)) := do
   let Q := ← BitVec.rand 1
   let size := ← if Q = 0#1 then BitVec.rand 2 (lo := 0) (hi := 2) else BitVec.rand 2
   let (inst : Advanced_simd_three_same_cls) :=
     { Q := Q,
-      U := ← pure 0b0#1,
+      U := ← BitVec.rand 1,
       size := size,
       Rm := ← BitVec.rand 5,
       opcode := ← pure 0b10000#5,
@@ -146,7 +153,7 @@ def Advanced_simd_three_same_cls.logic.rand : IO (Option (BitVec 32)) := do
 
 /-- Generate random instructions of Advanced_simd_three_same class. -/
 def Advanced_simd_three_same_cls.rand : List (IO (Option (BitVec 32))) :=
-  [ Advanced_simd_three_same_cls.add.rand,
+  [ Advanced_simd_three_same_cls.binary.rand,
     Advanced_simd_three_same_cls.logic.rand ]
 
 end DPSFP

Proofs/Sha512_block_armv8_rules.lean

@@ -70,8 +70,8 @@ set_option auto.smt.savepath "/tmp/sha512h_rule_1.smt2" in
 theorem sha512h_rule_1 (a b c d e : BitVec 128) :
   let elements := 2
   let esize := 64
-  let inner_sum := (add_vector_op 0 elements esize Std.BitVec.add c d (Std.BitVec.zero 128) H)
-  let outer_sum := (add_vector_op 0 elements esize Std.BitVec.add inner_sum e (Std.BitVec.zero 128) H)
+  let inner_sum := (binary_vector_op_aux 0 elements esize Std.BitVec.add c d (Std.BitVec.zero 128) H)
+  let outer_sum := (binary_vector_op_aux 0 elements esize Std.BitVec.add inner_sum e (Std.BitVec.zero 128) H)
   let a0 := extractLsb 63 0   a
   let a1 := extractLsb 127 64 a
   let b0 := extractLsb 63 0   b
@@ -86,7 +86,7 @@ theorem sha512h_rule_1 (a b c d e : BitVec 128) :
   let lo64_spec := compression_update_t1 (b0 + hi64_spec) b1 a0 c0 d0 e0
   sha512h a b outer_sum = hi64_spec ++ lo64_spec := by
   simp_all! only [Nat.sub_zero];
-  repeat (unfold add_vector_op; simp)
+  repeat (unfold binary_vector_op_aux; simp)
   unfold BitVec.partInstall
   unfold sha512h compression_update_t1 sigma_big_1 ch allOnes
   auto
@@ -157,14 +157,14 @@ theorem sha512h_rule_2 (a b c d e : BitVec 128) :
   let d1 := extractLsb 127 64 d
   let e0 := extractLsb 63 0   e
   let e1 := extractLsb 127 64 e
-  let inner_sum := add_vector_op 0 2 64 Std.BitVec.add d e (Std.BitVec.zero 128) h1
+  let inner_sum := binary_vector_op_aux 0 2 64 Std.BitVec.add d e (Std.BitVec.zero 128) h1
   let concat := inner_sum ++ inner_sum
   let operand := extractLsb 191 64 concat
   let hi64_spec := compression_update_t1 b1 a0 a1 c1 d0 e0
   let lo64_spec := compression_update_t1 (b0 + hi64_spec) b1 a0 c0 d1 e1
-  sha512h a b (add_vector_op 0 2 64 Std.BitVec.add c operand (Std.BitVec.zero 128) h2) =
+  sha512h a b (binary_vector_op_aux 0 2 64 Std.BitVec.add c operand (Std.BitVec.zero 128) h2) =
   hi64_spec ++ lo64_spec := by
-  repeat (unfold add_vector_op; simp)
+  repeat (unfold binary_vector_op_aux; simp)
   repeat (unfold BitVec.partInstall; simp)
   unfold sha512h compression_update_t1 sigma_big_1 ch allOnes
   auto