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

NSym/proof/proofs/SHA512/sha512_program.ml

@@ -42,15 +42,15 @@ let print_hex (intstr : string) : unit =
   Format.fprintf Format.std_formatter "@[<1>%s@]@." hexstr;;
 
 let (sha512_block_armv8_start_address, sha512_block_armv8_dump) =
-  Elf.symbol_contents ~section_name:".symtab" "sha512_block_armv8" elf;;
+  Elf.symbol_contents ~section_name:".symtab" "sha512_block_data_order_hw" elf;;
 let sha512_block_armv8_bytes =
   (Elf.uint32_list_of_data sha512_block_armv8_dump);;
 
 (* Print, in hex, the list of sha512_block_armv8 instructions. *)
 let _ = List.iter (fun i -> print_hex (Int.to_string i)) sha512_block_armv8_bytes;;
 
 let (sha512_block_data_order_start_address, sha512_block_data_order_dump) =
-  Elf.symbol_contents ~section_name:".symtab" "sha512_block_data_order" elf;;
+  Elf.symbol_contents ~section_name:".symtab" "sha512_block_data_order_nohw" elf;;
 let sha512_block_data_order_bytes =
   (Elf.uint32_list_of_data sha512_block_data_order_dump);;
 

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_avx"
+           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/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";

SAW/proof/common/asm_helpers.saw

@@ -16,10 +16,14 @@ let load_module = if asm_switch
 
 let llvm_verify_or_assume_asm m bin func globals pathsat spec tactic =
 if asm_switch
-  then llvm_verify_x86 m bin func globals pathsat spec tactic
+  then if do_prove
+       then llvm_verify_x86 m bin func globals pathsat spec tactic
+       else crucible_llvm_unsafe_assume_spec m func spec
   else crucible_llvm_unsafe_assume_spec m func spec;
 
 let llvm_verify_or_assume_fixpoint_asm m bin func globals pathsat loop spec tactic =
 if asm_switch
-  then llvm_verify_fixpoint_x86 m bin func globals pathsat loop spec tactic
+  then if do_prove
+       then llvm_verify_fixpoint_x86 m bin func globals pathsat loop spec tactic
+       else crucible_llvm_unsafe_assume_spec m func spec
   else crucible_llvm_unsafe_assume_spec m func spec;