From d440d9f7a056510ba266178e9dd00a5e32f9630b Mon Sep 17 00:00:00 2001
From: Nevine Ebeid <nebeid@amazon.com>
Date: Wed, 21 Feb 2024 17:51:16 -0500
Subject: [PATCH] EOR3, part of Cryptographic four-register group.

Also place the shabang line at the top of the shell script.
---
 Arm/Decode.lean                      |  2 +
 Arm/Decode/DPSFP.lean                | 18 +++++++++
 Arm/Exec.lean                        |  2 +
 Arm/Insts/Cosim/platform_check.sh    |  4 +-
 Arm/Insts/DPSFP/Crypto_four_reg.lean | 57 ++++++++++++++++++++++++++++
 Arm/Insts/DPSFP/Insts.lean           |  6 ++-
 6 files changed, 85 insertions(+), 4 deletions(-)
 create mode 100644 Arm/Insts/DPSFP/Crypto_four_reg.lean

diff --git a/Arm/Decode.lean b/Arm/Decode.lean
index a438c360..6db16fa2 100644
--- a/Arm/Decode.lean
+++ b/Arm/Decode.lean
@@ -90,6 +90,8 @@ def decode_data_proc_sfp (i : BitVec 32) : Option ArmInst :=
     DPSFP (Crypto_three_reg_sha512 {Rm, O, opcode, Rn, Rd})
   | [11001110110000001000, opcode:2, Rn:5, Rd:5] =>
     DPSFP (Crypto_two_reg_sha512 {opcode, Rn, Rd})
+  | [110011100, Op0:2, Rm:5, 0, Ra:5, Rn:5, Rd:5] =>
+    DPSFP (Crypto_four_reg {Op0, Rm, Ra, Rn, Rd})
   | [0, Q:1, U:1, 01110, size:2, 10000, opcode:5, 10, Rn:5, Rd:5] =>
     DPSFP (Advanced_simd_two_reg_misc {Q, U, size, opcode, Rn, Rd})
   | [0, Q:1, op:1, 01110000, imm5:5, 0, imm4:4, 1, Rn:5, Rd:5] =>
diff --git a/Arm/Decode/DPSFP.lean b/Arm/Decode/DPSFP.lean
index 5b12859c..7adcd735 100644
--- a/Arm/Decode/DPSFP.lean
+++ b/Arm/Decode/DPSFP.lean
@@ -53,6 +53,22 @@ instance : ToString Crypto_two_reg_sha512_cls where toString a := toString (repr
 def Crypto_two_reg_sha512_cls.toBitVec32 (x : Crypto_two_reg_sha512_cls) : BitVec 32 :=
   x._fixed ++ x.opcode ++ x.Rn ++ x.Rd
 
+structure Crypto_four_reg_cls where
+  _fixed1 : BitVec 9 := 0b110011100#9     -- [31:23]
+  Op0     : BitVec 2                      -- [22:21]
+  Rm      : BitVec 5                      -- [20:16]
+  _fixed2 : BitVec 1 := 0b0#1             -- [15:15]
+  Ra      : BitVec 5                      -- [14:10]
+  Rn      : BitVec 5                      --   [9:5]
+  Rd      : BitVec 5                      --   [4:0]
+deriving DecidableEq, Repr
+
+instance : ToString Crypto_four_reg_cls where
+toString a := toString (repr a)
+
+def Crypto_four_reg_cls.toBitVec32 (x : Crypto_four_reg_cls) : BitVec 32 :=
+  x._fixed1 ++ x.Op0 ++ x.Rm ++ x._fixed2 ++ x.Ra ++ x.Rn ++ x.Rd
+
 structure Advanced_simd_two_reg_misc_cls where
   _fixed1 : BitVec 1 := 0b0#1      -- [31:31]
   Q       : BitVec 1               -- [30:30]
@@ -150,6 +166,8 @@ inductive DataProcSFPInst where
     Crypto_two_reg_sha512_cls → DataProcSFPInst
   | Crypto_three_reg_sha512 :
     Crypto_three_reg_sha512_cls → DataProcSFPInst
+  | Crypto_four_reg :
+    Crypto_four_reg_cls → DataProcSFPInst
   | Advanced_simd_two_reg_misc :
     Advanced_simd_two_reg_misc_cls → DataProcSFPInst
   | Advanced_simd_copy :
diff --git a/Arm/Exec.lean b/Arm/Exec.lean
index bea31af6..90731b1e 100644
--- a/Arm/Exec.lean
+++ b/Arm/Exec.lean
@@ -40,6 +40,8 @@ def exec_inst (ai : ArmInst) (s : ArmState) : ArmState :=
     DPSFP.exec_crypto_two_reg_sha512 i s
   | DPSFP (DataProcSFPInst.Crypto_three_reg_sha512 i) =>
     DPSFP.exec_crypto_three_reg_sha512 i s
+  | DPSFP (DataProcSFPInst.Crypto_four_reg i) =>
+    DPSFP.exec_crypto_four_reg i s
   | DPSFP (DataProcSFPInst.Advanced_simd_two_reg_misc i) =>
     DPSFP.exec_advanced_simd_two_reg_misc i s
   | DPSFP (DataProcSFPInst.Advanced_simd_extract i) =>
diff --git a/Arm/Insts/Cosim/platform_check.sh b/Arm/Insts/Cosim/platform_check.sh
index d56a2707..a622dbc3 100755
--- a/Arm/Insts/Cosim/platform_check.sh
+++ b/Arm/Insts/Cosim/platform_check.sh
@@ -1,9 +1,9 @@
+#!/bin/bash
+
 # 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
 
-#!/bin/bash
-
 machine_check () {
     machine=$(uname -m)
     if [[ $machine == *aarch64* ]]; then
diff --git a/Arm/Insts/DPSFP/Crypto_four_reg.lean b/Arm/Insts/DPSFP/Crypto_four_reg.lean
new file mode 100644
index 00000000..d685c395
--- /dev/null
+++ b/Arm/Insts/DPSFP/Crypto_four_reg.lean
@@ -0,0 +1,57 @@
+/-
+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): Shilpi Goel, Nevine Ebeid
+-/
+-- EOR3
+
+import Arm.Decode
+import Arm.Memory
+import Arm.Insts.Common
+import Arm.BitVec
+
+----------------------------------------------------------------------
+
+namespace DPSFP
+
+open Std.BitVec
+
+def exec_crypto_four_reg (inst : Crypto_four_reg_cls) (s : ArmState) : ArmState :=
+  -- This function assumes IsFeatureImplemented(FEAT_SHA3) is true
+  -- and that AArch64.CheckFPAdvSIMDEnabled() returns successfully
+  if inst.Op0 != 0b00#2 then
+    write_err (StateError.Illegal s!"Illegal {inst} encountered!") s
+  else
+    let datasize := 128
+    let opdm := read_sfp datasize inst.Rm s
+    let opdn := read_sfp datasize inst.Rn s
+    let opda := read_sfp datasize inst.Ra s
+    let result := opdm ^^^ opdn ^^^ opda
+    let s := write_sfp datasize inst.Rd result s
+    let s := write_pc ((read_pc s) + 4#64) s
+    s
+
+----------------------------------------------------------------------
+
+def Crypto_four_reg_cls.eor3.rand : IO (Option (BitVec 32)) := do
+  let feat_check ←
+      IO.Process.output
+      { cmd  := "../Cosim/platform_check.sh",
+        args := #["-f", "sha3"] }
+  if feat_check.exitCode == 0 then
+    let (inst : Crypto_four_reg_cls) :=
+      { Op0    := ← pure 0b00#2,
+        Rm     := ← BitVec.rand 5,
+        Rn     := ← BitVec.rand 5,
+        Ra     := ← BitVec.rand 5,
+        Rd     := ← BitVec.rand 5 }
+    pure (some inst.toBitVec32)
+  else
+    pure none
+
+/-- Generate random instructions of Crypto_four_reg_cls class. -/
+def Crypto_four_reg_cls.rand : List (IO (Option (BitVec 32))) :=
+  [Crypto_four_reg_cls.eor3.rand]
+
+
+end DPSFP
diff --git a/Arm/Insts/DPSFP/Insts.lean b/Arm/Insts/DPSFP/Insts.lean
index 0009361a..d2d51f20 100644
--- a/Arm/Insts/DPSFP/Insts.lean
+++ b/Arm/Insts/DPSFP/Insts.lean
@@ -10,7 +10,8 @@ import Arm.Insts.DPSFP.Advanced_simd_three_different
 import Arm.Insts.DPSFP.Crypto_aes
 import Arm.Insts.DPSFP.Crypto_two_reg_sha512
 import Arm.Insts.DPSFP.Crypto_three_reg_sha512
-        
+import Arm.Insts.DPSFP.Crypto_four_reg
+
 /-- List of functions to generate random instructions of the
 DPSFP class. -/
 def DPSFP.rand : List (IO (Option (BitVec 32))) :=
@@ -19,4 +20,5 @@ def DPSFP.rand : List (IO (Option (BitVec 32))) :=
   DPSFP.Advanced_simd_three_different_cls.rand ++
   DPSFP.Advanced_simd_two_reg_misc_cls.rand ++
   DPSFP.Crypto_three_reg_sha512_cls.rand ++
-  DPSFP.Crypto_two_reg_sha512_cls.rand
+  DPSFP.Crypto_two_reg_sha512_cls.rand ++
+  DPSFP.Crypto_four_reg_cls.rand