diff --git a/Arm/Decode.lean b/Arm/Decode.lean index a2b22325..4a956d9f 100644 --- a/Arm/Decode.lean +++ b/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 diff --git a/Arm/Decode/DPR.lean b/Arm/Decode/DPR.lean index 65791ed6..4ca7f2f3 100644 --- a/Arm/Decode/DPR.lean +++ b/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 : diff --git a/Arm/Exec.lean b/Arm/Exec.lean index d374366d..9ad033ef 100644 --- a/Arm/Exec.lean +++ b/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) => diff --git a/Arm/Insts/DPR/Add_sub_shifted_reg.lean b/Arm/Insts/DPR/Add_sub_shifted_reg.lean new file mode 100644 index 00000000..9c97b3c8 --- /dev/null +++ b/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 diff --git a/Arm/Insts/DPR/Insts.lean b/Arm/Insts/DPR/Insts.lean index dcc71c03..d505ddd7 100644 --- a/Arm/Insts/DPR/Insts.lean +++ b/Arm/Insts/DPR/Insts.lean @@ -3,6 +3,7 @@ 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 @@ -10,5 +11,6 @@ import Arm.Insts.DPR.Logical_shifted_reg 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] diff --git a/Arm/Insts/DPSFP/Advanced_simd_three_same.lean b/Arm/Insts/DPSFP/Advanced_simd_three_same.lean index 087349fe..09d15262 100644 --- a/Arm/Insts/DPSFP/Advanced_simd_three_same.lean +++ b/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,7 +119,7 @@ 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 @@ -120,12 +127,12 @@ theorem pc_of_exec_advanced_simd_three_same ---------------------------------------------------------------------- -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 diff --git a/Proofs/Sha512_block_armv8_rules.lean b/Proofs/Sha512_block_armv8_rules.lean index ff032d34..0ca2d6fa 100644 --- a/Proofs/Sha512_block_armv8_rules.lean +++ b/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