Add symbolic simulation for aes_gcm_enc_kernel

Proofs/AES-GCM/AESGCMEncKernelPre.lean

@@ -0,0 +1,16 @@
+/-
+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
+-/
+import Tests.«AES-GCM».AESGCMEncKernelProgram
+import Tactics.Sym
+import Tactics.StepThms
+import Correctness.ArmSpec
+
+namespace AESGCMEncKernelProgram
+
+set_option maxHeartbeats 2000000 in
+#genStepEqTheorems aes_gcm_enc_kernel_program
+
+end AESGCMEncKernelProgram

Proofs/AES-GCM/AESGCMEncKernelSym.lean

@@ -0,0 +1,33 @@
+/-
+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
+-/
+import Proofs.«AES-GCM».AESGCMEncKernelPre
+import Tactics.Sym
+import Tactics.StepThms
+import Correctness.ArmSpec
+
+namespace AESGCMEncKernelProgram
+
+set_option maxRecDepth 1000000 in
+theorem aes_gcm_enc_kernel_program_run_xx (s0 sf : ArmState)
+    (h_s0_program : s0.program = aes_gcm_enc_kernel_program)
+    (h_s0_err : read_err s0 = .None)
+    (h_s0_pc : read_pc s0 = aes_gcm_enc_kernel_program.min)
+    (h_s0_sp_aligned : CheckSPAlignment s0)
+    (h_run : sf = run 1 s0)
+    -- -- AES256 rounds = 14, the address of rounds is stored in x2
+    -- (h_rounds : 14 = read_mem_bytes 4 (round_addr s0) s0)
+    -- -- memory separation
+    -- (h_s0_in_key_separate :
+    --   mem_separate' (in_addr s0) 128 (key_addr s0) 304)
+    -- (h_s0_out_key_separate :
+    --   mem_separate' (out_addr s0) 128 (key_addr s0) 304)
+    -- (h_s0_in_out_separate :
+    --   mem_separate' (in_addr s0) 128 (out_addr s0) 128)
+     :
+    read_err sf = .None := by
+    sorry
+
+end AESGCMEncKernelProgram

Proofs/AES-GCM/GCM.lean

@@ -6,3 +6,4 @@ Author(s): Alex Keizer
 import Proofs.«AES-GCM».GCMGmultV8Sym
 import Proofs.«AES-GCM».GCMInitV8Sym
 import Proofs.«AES-GCM».AESHWEncryptSym
+import Proofs.«AES-GCM».AESGCMEncKernelSym