Update SHA proof for moving AArch64/X86_64 dispatching to C changes

.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

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

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;

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";

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";