diff --git a/Arm/Decode.lean b/Arm/Decode.lean index f82bbedb..76534c8d 100644 --- a/Arm/Decode.lean +++ b/Arm/Decode.lean @@ -86,8 +86,8 @@ def decode_data_proc_sfp (i : BitVec 32) : Option ArmInst := open ArmInst in open DataProcSFPInst in match_bv i with - | [01001110, esize:2, 10100, opcode:5, 10, Rn:5, Rd:5] => - DPSFP (Crypto_aes {esize, opcode, Rn, Rd}) + | [01001110, size:2, 10100, opcode:5, 10, Rn:5, Rd:5] => + DPSFP (Crypto_aes {size, opcode, Rn, Rd}) | [11001110011, Rm:5, 1, O:1, 00, opcode:2, Rn:5, Rd:5] => DPSFP (Crypto_three_reg_sha512 {Rm, O, opcode, Rn, Rd}) | [11001110110000001000, opcode:2, Rn:5, Rd:5] => @@ -325,14 +325,14 @@ example : decode_raw_inst 0x4e200800#32 = -- aese v0.16b, v16.16b example : decode_raw_inst 0x4e284a00#32 = (ArmInst.DPSFP (DataProcSFPInst.Crypto_aes - { esize := 0x0#2, opcode := 0x04#5, + { size := 0x0#2, opcode := 0x04#5, Rn := 0x10#5, Rd := 0x00#5 })) := by rfl -- aesmc v0.16b, v0.16b example : decode_raw_inst 0x4e286800#32 = (ArmInst.DPSFP (DataProcSFPInst.Crypto_aes - { esize := 0x0#2, opcode := 0x06#5, + { size := 0x0#2, opcode := 0x06#5, Rn := 0x00#5, Rd := 0x00#5 })) := by rfl diff --git a/Arm/Decode/DPSFP.lean b/Arm/Decode/DPSFP.lean index 60299431..eceb57bb 100644 --- a/Arm/Decode/DPSFP.lean +++ b/Arm/Decode/DPSFP.lean @@ -14,8 +14,8 @@ open BitVec -- Data Processing (SIMD and FP) Instructions -- structure Crypto_aes_cls where - _fixed1 : BitVec 7 := 0b01001110#7 -- [31:24] - esize : BitVec 2 -- [23:22] + _fixed1 : BitVec 8 := 0b01001110#8 -- [31:24] + size : BitVec 2 -- [23:22] _fixed2 : BitVec 5 := 0b10100#5 -- [21:17] opcode : BitVec 5 -- [16:12] _fixed3 : BitVec 2 := 0b10#2 -- [11:10] @@ -25,6 +25,9 @@ deriving DecidableEq, Repr instance : ToString Crypto_aes_cls where toString a := toString (repr a) +def Crypto_aes_cls.toBitVec32 (x : Crypto_aes_cls) : BitVec 32 := + x._fixed1 ++ x.size ++ x._fixed2 ++ x.opcode ++ x._fixed3 ++ x.Rn ++ x.Rd + structure Crypto_three_reg_sha512_cls where _fixed1 : BitVec 11 := 0b11001110011#11 -- [31:21] Rm : BitVec 5 -- [20:16] diff --git a/Arm/Exec.lean b/Arm/Exec.lean index bd01b9f8..86b92c34 100644 --- a/Arm/Exec.lean +++ b/Arm/Exec.lean @@ -42,6 +42,8 @@ def exec_inst (ai : ArmInst) (s : ArmState) : ArmState := | DPSFP (DataProcSFPInst.Advanced_simd_copy i) => DPSFP.exec_advanced_simd_copy i s + | DPSFP (DataProcSFPInst.Crypto_aes i) => + DPSFP.exec_crypto_aes i s | DPSFP (DataProcSFPInst.Crypto_two_reg_sha512 i) => DPSFP.exec_crypto_two_reg_sha512 i s | DPSFP (DataProcSFPInst.Crypto_three_reg_sha512 i) => @@ -82,10 +84,6 @@ def exec_inst (ai : ArmInst) (s : ArmState) : ArmState := | LDST (LDSTInst.Advanced_simd_multiple_struct_post_indexed i) => LDST.exec_advanced_simd_multiple_struct_post_indexed i s - | _ => - write_err - (StateError.Unimplemented s!"Unsupported ArmInst {ai} encountered in exec_inst!") s - def stepi (s : ArmState) : ArmState := -- This function should be simulated away automatically because the diff --git a/Arm/Insts/DPSFP/Advanced_simd_scalar_copy.lean b/Arm/Insts/DPSFP/Advanced_simd_scalar_copy.lean index 298a2ae2..a5136b9e 100644 --- a/Arm/Insts/DPSFP/Advanced_simd_scalar_copy.lean +++ b/Arm/Insts/DPSFP/Advanced_simd_scalar_copy.lean @@ -26,8 +26,8 @@ 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 - have h₁ : esize > 0 := by apply zero_lt_shift_left_pos (by decide) - let result := elem_get operand index.toNat esize h₁ + have h : esize > 0 := by apply zero_lt_shift_left_pos (by decide) + 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 diff --git a/Arm/Insts/DPSFP/Crypto_aes.lean b/Arm/Insts/DPSFP/Crypto_aes.lean index a24410dd..32a8d09b 100644 --- a/Arm/Insts/DPSFP/Crypto_aes.lean +++ b/Arm/Insts/DPSFP/Crypto_aes.lean @@ -1,12 +1,13 @@ /- Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author(s): Shilpi Goel +Author(s): Shilpi Goel, Yan Peng -/ -- AESE, AESMC import Arm.Decode import Arm.Insts.Common +import Arm.BitVec ---------------------------------------------------------------------- @@ -14,32 +15,213 @@ namespace DPSFP open BitVec --- def aese (x : BitVec 128) : BitVec 128 := --- open aes_helpers in --- let w_127_64 := extractLsb 127 64 w --- let w_127_71 := extractLsb 127 71 w --- let w_63_0 := extractLsb 63 0 w --- let sig0 := sigma_0 w_127_64 w_127_71 --- let x_63_0 := extractLsb 63 0 x --- let x_63_7 := extractLsb 63 7 x --- let vtmp_63_0 := w_63_0 + sig0 --- let sig0 := sigma_0 x_63_0 x_63_7 --- let vtmp_127_64 := w_127_64 + sig0 --- let result := vtmp_127_64 ++ vtmp_63_0 --- result - --- def exec_crypto_aes --- (inst : Crypto_aes_cls) (s : ArmState) : ArmState := --- open BitVec in --- let operand1 := read_sfp 128 inst.Rd s --- let operand2 := read_sfp 128 inst.Rn s --- let result := --- match inst.opcode with --- | 00#2 => sha512su0 x w --- | _ => 0#128 -- Throw an "unimplemented instruction" exception --- -- State Updates --- let s' := write_pc ((read_pc s) + 4#64) s --- let s' := write_sfp 128 inst.Rd result s' --- s' +def SBox := + -- F E D C B A 9 8 7 6 5 4 3 2 1 0 + [ 0x16bb54b00f2d99416842e6bf0d89a18c#128, -- F + 0xdf2855cee9871e9b948ed9691198f8e1#128, -- E + 0x9e1dc186b95735610ef6034866b53e70#128, -- D + 0x8a8bbd4b1f74dde8c6b4a61c2e2578ba#128, -- C + 0x08ae7a65eaf4566ca94ed58d6d37c8e7#128, -- B + 0x79e4959162acd3c25c2406490a3a32e0#128, -- A + 0xdb0b5ede14b8ee4688902a22dc4f8160#128, -- 9 + 0x73195d643d7ea7c41744975fec130ccd#128, -- 8 + 0xd2f3ff1021dab6bcf5389d928f40a351#128, -- 7 + 0xa89f3c507f02f94585334d43fbaaefd0#128, -- 6 + 0xcf584c4a39becb6a5bb1fc20ed00d153#128, -- 5 + 0x842fe329b3d63b52a05a6e1b1a2c8309#128, -- 4 + 0x75b227ebe28012079a059618c323c704#128, -- 3 + 0x1531d871f1e5a534ccf73f362693fdb7#128, -- 2 + 0xc072a49cafa2d4adf04759fa7dc982ca#128, -- 1 + 0x76abd7fe2b670130c56f6bf27b777c63#128 -- 0 + ] + +def AESShiftRows (op : BitVec 128) : BitVec 128 := + extractLsb 95 88 op ++ extractLsb 55 48 op ++ + extractLsb 15 8 op ++ extractLsb 103 96 op ++ + extractLsb 63 56 op ++ extractLsb 23 16 op ++ + extractLsb 111 104 op ++ extractLsb 71 64 op ++ + extractLsb 31 24 op ++ extractLsb 119 112 op ++ + extractLsb 79 72 op ++ extractLsb 39 32 op ++ + extractLsb 127 120 op ++ extractLsb 87 80 op ++ + extractLsb 47 40 op ++ extractLsb 7 0 op + +def AESSubBytes_aux (i : Nat) (op : BitVec 128) (out : BitVec 128) + : BitVec 128 := + if h₀ : 16 <= i then + out + else + let idx := (extractLsb (i * 8 + 7) (i * 8) op).toNat + let val := extractLsb (idx * 8 + 7) (idx * 8) $ BitVec.flatten SBox + have h₁ : idx * 8 + 7 - idx * 8 = i * 8 + 7 - i * 8 := by omega + let out := BitVec.partInstall (i * 8 + 7) (i * 8) (h₁ ▸ val) out + have _ : 15 - i < 16 - i := by omega + AESSubBytes_aux (i + 1) op out + termination_by (16 - i) + +def AESSubBytes (op : BitVec 128) : BitVec 128 := + AESSubBytes_aux 0 op (BitVec.zero 128) + +@[state_simp_rules] +def exec_aese + (inst : Crypto_aes_cls) (s : ArmState) : ArmState := + -- Assumes IsFeatureImplemented(FEAT_AES) + -- AArch64.CheckFPAdvSIMDEnabled(); + let operand1 := read_sfp 128 inst.Rd s + let operand2 := read_sfp 128 inst.Rn s + let result := operand1 ^^^ operand2 + let result := AESSubBytes $ AESShiftRows result + -- State Updates + let s := write_sfp 128 inst.Rd result s + let s := write_pc ((read_pc s) + 4#64) s + s + +def FFmul02 (b : BitVec 8) : BitVec 8 := + let FFmul_02 := + -- F E D C B A 9 8 7 6 5 4 3 2 1 0 + [ 0xE5E7E1E3EDEFE9EBF5F7F1F3FDFFF9FB#128, -- F + 0xC5C7C1C3CDCFC9CBD5D7D1D3DDDFD9DB#128, -- E + 0xA5A7A1A3ADAFA9ABB5B7B1B3BDBFB9BB#128, -- D + 0x858781838D8F898B959791939D9F999B#128, -- C + 0x656761636D6F696B757771737D7F797B#128, -- B + 0x454741434D4F494B555751535D5F595B#128, -- A + 0x252721232D2F292B353731333D3F393B#128, -- 9 + 0x050701030D0F090B151711131D1F191B#128, -- 8 + 0xFEFCFAF8F6F4F2F0EEECEAE8E6E4E2E0#128, -- 7 + 0xDEDCDAD8D6D4D2D0CECCCAC8C6C4C2C0#128, -- 6 + 0xBEBCBAB8B6B4B2B0AEACAAA8A6A4A2A0#128, -- 5 + 0x9E9C9A98969492908E8C8A8886848280#128, -- 4 + 0x7E7C7A78767472706E6C6A6866646260#128, -- 3 + 0x5E5C5A58565452504E4C4A4846444240#128, -- 2 + 0x3E3C3A38363432302E2C2A2826242220#128, -- 1 + 0x1E1C1A18161412100E0C0A0806040200#128 -- 0 + ] + let lo := b.toNat * 8 + let hi := lo + 7 + have h : hi - lo + 1 = 8 := by omega + h ▸ extractLsb hi lo $ BitVec.flatten FFmul_02 + +def FFmul03 (b : BitVec 8) : BitVec 8 := + let FFmul_03 := + -- F E D C B A 9 8 7 6 5 4 3 2 1 0 + [ 0x1A191C1F16151013020104070E0D080B#128, -- F + 0x2A292C2F26252023323134373E3D383B#128, -- E + 0x7A797C7F76757073626164676E6D686B#128, -- D + 0x4A494C4F46454043525154575E5D585B#128, -- C + 0xDAD9DCDFD6D5D0D3C2C1C4C7CECDC8CB#128, -- B + 0xEAE9ECEFE6E5E0E3F2F1F4F7FEFDF8FB#128, -- A + 0xBAB9BCBFB6B5B0B3A2A1A4A7AEADA8AB#128, -- 9 + 0x8A898C8F86858083929194979E9D989B#128, -- 8 + 0x818287848D8E8B88999A9F9C95969390#128, -- 7 + 0xB1B2B7B4BDBEBBB8A9AAAFACA5A6A3A0#128, -- 6 + 0xE1E2E7E4EDEEEBE8F9FAFFFCF5F6F3F0#128, -- 5 + 0xD1D2D7D4DDDEDBD8C9CACFCCC5C6C3C0#128, -- 4 + 0x414247444D4E4B48595A5F5C55565350#128, -- 3 + 0x717277747D7E7B78696A6F6C65666360#128, -- 2 + 0x212227242D2E2B28393A3F3C35363330#128, -- 1 + 0x111217141D1E1B18090A0F0C05060300#128 -- 0 + ] + let lo := b.toNat * 8 + let hi := lo + 7 + have h : hi - lo + 1 = 8 := by omega + h ▸ extractLsb hi lo $ BitVec.flatten FFmul_03 + +def AESMixColumns_aux (c : Nat) + (in0 : BitVec 32) (in1 : BitVec 32) (in2 : BitVec 32) (in3 : BitVec 32) + (out0 : BitVec 32) (out1 : BitVec 32) (out2 : BitVec 32) (out3 : BitVec 32) + : BitVec 32 × BitVec 32 × BitVec 32 × BitVec 32 := + if h₀ : 4 <= c then + (out0, out1, out2, out3) + else + let lo := c * 8 + let hi := lo + 7 + have h₁ : hi - lo + 1 = 8 := by omega + let in0_byte := h₁ ▸ extractLsb hi lo in0 + let in1_byte := h₁ ▸ extractLsb hi lo in1 + let in2_byte := h₁ ▸ extractLsb hi lo in2 + let in3_byte := h₁ ▸ extractLsb hi lo in3 + let val0 := h₁.symm ▸ (FFmul02 in0_byte ^^^ FFmul03 in1_byte ^^^ in2_byte ^^^ in3_byte) + let out0 := BitVec.partInstall hi lo val0 out0 + let val1 := h₁.symm ▸ (FFmul02 in1_byte ^^^ FFmul03 in2_byte ^^^ in3_byte ^^^ in0_byte) + let out1 := BitVec.partInstall hi lo val1 out1 + let val2 := h₁.symm ▸ (FFmul02 in2_byte ^^^ FFmul03 in3_byte ^^^ in0_byte ^^^ in1_byte) + let out2 := BitVec.partInstall hi lo val2 out2 + let val3 := h₁.symm ▸ (FFmul02 in3_byte ^^^ FFmul03 in0_byte ^^^ in1_byte ^^^ in2_byte) + let out3 := BitVec.partInstall hi lo val3 out3 + have _ : 3 - c < 4 - c := by omega + AESMixColumns_aux (c + 1) in0 in1 in2 in3 out0 out1 out2 out3 + termination_by (4 - c) + +def AESMixColumns (op : BitVec 128) : BitVec 128 := + let in0 := + extractLsb 103 96 op ++ extractLsb 71 64 op ++ + extractLsb 39 32 op ++ extractLsb 7 0 op + let in1 := + extractLsb 111 104 op ++ extractLsb 79 72 op ++ + extractLsb 47 40 op ++ extractLsb 15 8 op + let in2 := + extractLsb 119 112 op ++ extractLsb 87 80 op ++ + extractLsb 55 48 op ++ extractLsb 23 16 op + let in3 := + extractLsb 127 120 op ++ extractLsb 95 88 op ++ + extractLsb 63 56 op ++ extractLsb 31 24 op + let (out0, out1, out2, out3) := + (BitVec.zero 32, BitVec.zero 32, + BitVec.zero 32, BitVec.zero 32) + let (out0, out1, out2, out3) := + AESMixColumns_aux 0 in0 in1 in2 in3 out0 out1 out2 out3 + extractLsb 31 24 out3 ++ extractLsb 31 24 out2 ++ + extractLsb 31 24 out1 ++ extractLsb 31 24 out0 ++ + extractLsb 23 16 out3 ++ extractLsb 23 16 out2 ++ + extractLsb 23 16 out1 ++ extractLsb 23 16 out0 ++ + extractLsb 15 8 out3 ++ extractLsb 15 8 out2 ++ + extractLsb 15 8 out1 ++ extractLsb 15 8 out0 ++ + extractLsb 7 0 out3 ++ extractLsb 7 0 out2 ++ + extractLsb 7 0 out1 ++ extractLsb 7 0 out0 + +@[state_simp_rules] +def exec_aesmc + (inst : Crypto_aes_cls) (s : ArmState) : ArmState := + -- Assumes IsFeatureImplemented(FEAT_AES) + -- AArch64.CheckFPAdvSIMDEnabled(); + let operand := read_sfp 128 inst.Rn s + let result := AESMixColumns operand + -- State Updates + let s := write_sfp 128 inst.Rd result s + let s := write_pc ((read_pc s) + 4#64) s + s + +@[state_simp_rules] +def exec_crypto_aes + (inst : Crypto_aes_cls) (s : ArmState) : ArmState := + match inst.size, inst.opcode with + | 0b00#2, 0b00100#5 => exec_aese inst s + | 0b00#2, 0b00110#5 => exec_aesmc inst s + | _, _ => write_err + (StateError.Unimplemented s!"Unsupported instruction {inst} encountered!") s + +---------------------------------------------------------------------- + +def Crypto_aes_cls.aese.rand : IO (Option (BitVec 32)) := do + let (inst : Crypto_aes_cls) := + { size := 0b00#2, + opcode := 0b00100#5, + Rn := ← BitVec.rand 5, + Rd := ← BitVec.rand 5 + } + pure (some inst.toBitVec32) + +def Crypto_aes_cls.aesmc.rand : IO (Option (BitVec 32)) := do + let (inst : Crypto_aes_cls) := + { size := 0b00#2, + opcode := 0b00110#5, + Rn := ← BitVec.rand 5, + Rd := ← BitVec.rand 5 + } + pure (some inst.toBitVec32) + +/-- Generate random instructions of Crypto_aes_cls class. -/ +def Crypto_aes_cls.rand : List (IO (Option (BitVec 32))) := + [ Crypto_aes_cls.aese.rand, + Crypto_aes_cls.aesmc.rand ] end DPSFP diff --git a/Arm/Insts/DPSFP/Insts.lean b/Arm/Insts/DPSFP/Insts.lean index 1e1c9d07..6bef855f 100644 --- a/Arm/Insts/DPSFP/Insts.lean +++ b/Arm/Insts/DPSFP/Insts.lean @@ -30,6 +30,7 @@ def DPSFP.rand : List (IO (Option (BitVec 32))) := DPSFP.Advanced_simd_three_same_cls.rand ++ DPSFP.Advanced_simd_three_different_cls.rand ++ DPSFP.Advanced_simd_two_reg_misc_cls.rand ++ + DPSFP.Crypto_aes_cls.rand ++ DPSFP.Crypto_three_reg_sha512_cls.rand ++ DPSFP.Crypto_two_reg_sha512_cls.rand ++ DPSFP.Crypto_four_reg_cls.rand ++