From 9f6e2129a748cd8edf0f6bbe9dd38e33aeb7176a Mon Sep 17 00:00:00 2001
From: Yan Peng <yppe@amazon.com>
Date: Fri, 14 Jun 2024 22:50:59 +0000
Subject: [PATCH] Update SHA proof for moving AArch64/X86_64 dispatching to C
 changes

---
 .gitmodules                              |  4 ++--
 SAW/proof/SHA512/SHA512-common.saw       | 10 ++++++++--
 SAW/proof/SHA512/SHA512.saw              |  3 +++
 SAW/proof/SHA512/aarch64-neoverse-n1.saw |  3 ++-
 SAW/proof/SHA512/aarch64-neoverse-v1.saw |  1 +
 src                                      |  2 +-
 6 files changed, 17 insertions(+), 6 deletions(-)

diff --git a/.gitmodules b/.gitmodules
index 772e2da7..fe35603d 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -1,7 +1,7 @@
 [submodule "src"]
 	path = src
-	branch = main
-	url = https://github.com/aws/aws-lc.git
+	branch = upstream-sha-asm
+	url = https://github.com/justsmth/aws-lc.git
 [submodule "cryptol-specs"]
 	path = cryptol-specs
 	branch = sha-imperative
diff --git a/SAW/proof/SHA512/SHA512-common.saw b/SAW/proof/SHA512/SHA512-common.saw
index 9b1dd6b2..84cd473f 100644
--- a/SAW/proof/SHA512/SHA512-common.saw
+++ b/SAW/proof/SHA512/SHA512-common.saw
@@ -32,7 +32,13 @@ EVP_MD_pctx_ops_ov <- llvm_unsafe_assume_spec
 
 enable_what4_hash_consing;
 
-sha512_block_data_order_ov <- llvm_verify_or_assume_asm m "../../build/x86/crypto/crypto_test" "sha512_block_data_order"
+let func = if eval_bool {{ARCH@@[0..2] == "X86"}}
+           then "sha512_block_data_order_nohw"
+           else if eval_bool {{MicroARCH == "neoverse_n1"}}
+                then "sha512_block_data_order_nohw"
+                else "sha512_block_data_order_hw";
+
+sha512_block_data_order_ov <- llvm_verify_or_assume_asm m "../../build/x86/crypto/crypto_test" func
   [ ("K512", 5120) // Initializes the global for round constants, called K, at a size of 5120 bytes
   ]
   true
@@ -52,7 +58,7 @@ sha512_block_data_order_ov <- llvm_verify_or_assume_asm m "../../build/x86/crypt
 enable_what4_eval;
 enable_x86_what4_hash_consing;
 
-sha512_block_data_order_array_ov <- llvm_verify_or_assume_fixpoint_asm m "../../build/x86/crypto/crypto_test" "sha512_block_data_order"
+sha512_block_data_order_array_ov <- llvm_verify_or_assume_fixpoint_asm m "../../build/x86/crypto/crypto_test" func
   [ ("K512", 5120) // Initializes the global for round constants, called K, at a size of 5120 bytes
   ]
   true
diff --git a/SAW/proof/SHA512/SHA512.saw b/SAW/proof/SHA512/SHA512.saw
index 4403957b..0dbfef04 100644
--- a/SAW/proof/SHA512/SHA512.saw
+++ b/SAW/proof/SHA512/SHA512.saw
@@ -52,6 +52,9 @@ EVP_DigestUpdate_array_ov <- llvm_verify m "EVP_DigestUpdate"
 // overlapping = end(sha->h) > begin(out) && end(out) > begin(sha->h)
 // This comparison compares pointers from different locations,
 // triggers an undefined behaviour and therefore SAW errors.
+
+let do_prove = false;
+
 let verify_final_with_length withLength = do {
   print (str_concat "Verifying EVP_DigestFinal withLength=" (show withLength));
   enable_what4_eval;
diff --git a/SAW/proof/SHA512/aarch64-neoverse-n1.saw b/SAW/proof/SHA512/aarch64-neoverse-n1.saw
index a775c6c4..dafd82ee 100644
--- a/SAW/proof/SHA512/aarch64-neoverse-n1.saw
+++ b/SAW/proof/SHA512/aarch64-neoverse-n1.saw
@@ -10,7 +10,8 @@
 // Name of the OPENSSL machine cap variable
 let cap_sym = "OPENSSL_armcap_P";
 // Set machine cap value
-// The value is acquired by printing OPENSSL_armcap_P in AWS-LC on Graviton3
+// The value is acquired by printing OPENSSL_armcap_P in AWS-LC on Graviton2
 let {{ machine_cap = 0x0000003D : [32] }};
 // Set the architecture variable for controlling proof settings
 let ARCH = "AARCH64";
+let MicroARCH = "neoverse_n1";
diff --git a/SAW/proof/SHA512/aarch64-neoverse-v1.saw b/SAW/proof/SHA512/aarch64-neoverse-v1.saw
index 6607f531..cf3b93f9 100644
--- a/SAW/proof/SHA512/aarch64-neoverse-v1.saw
+++ b/SAW/proof/SHA512/aarch64-neoverse-v1.saw
@@ -14,3 +14,4 @@ let cap_sym = "OPENSSL_armcap_P";
 let {{ machine_cap = 0x0000187D : [32] }};
 // Set the architecture variable for controlling proof settings
 let ARCH = "AARCH64";
+let MicroARCH = "neoverse_v1";
diff --git a/src b/src
index 37ba0e2e..5baec02f 160000
--- a/src
+++ b/src
@@ -1 +1 @@
-Subproject commit 37ba0e2efc68407e7b20c71a7f4332846a76a7fb
+Subproject commit 5baec02f0ac71e30959014c2ee523ec17a4545b1