From b7d1a1679e6ff98f0050831f5f15bceccab376f2 Mon Sep 17 00:00:00 2001 From: Yan Peng 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 ++-- NSym/proof/proofs/SHA512/sha512_program.ml | 4 ++-- SAW/proof/SHA512/SHA512-common.saw | 10 ++++++++-- SAW/proof/SHA512/aarch64-neoverse-n1.saw | 3 ++- SAW/proof/SHA512/aarch64-neoverse-v1.saw | 1 + SAW/proof/common/asm_helpers.saw | 10 ++++++++-- src | 2 +- 7 files changed, 24 insertions(+), 10 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/NSym/proof/proofs/SHA512/sha512_program.ml b/NSym/proof/proofs/SHA512/sha512_program.ml index ca3f5298..b335422e 100644 --- a/NSym/proof/proofs/SHA512/sha512_program.ml +++ b/NSym/proof/proofs/SHA512/sha512_program.ml @@ -42,7 +42,7 @@ 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);; @@ -50,7 +50,7 @@ let sha512_block_armv8_bytes = 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);; diff --git a/SAW/proof/SHA512/SHA512-common.saw b/SAW/proof/SHA512/SHA512-common.saw index 9b1dd6b2..56d34c21 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_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 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/SAW/proof/common/asm_helpers.saw b/SAW/proof/common/asm_helpers.saw index 91a82256..e00e8d15 100644 --- a/SAW/proof/common/asm_helpers.saw +++ b/SAW/proof/common/asm_helpers.saw @@ -5,6 +5,8 @@ enable_experimental; +include "../common/helpers.saw"; + // ARCH is either "X86_64":[6] or "AARCH64":[7], note they are of different types // We will get a type error if we directly compare ARCH with "X86_64" // when ARCH is set to be "AARCH64". @@ -16,10 +18,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; diff --git a/src b/src index 37ba0e2e..5baec02f 160000 --- a/src +++ b/src @@ -1 +1 @@ -Subproject commit 37ba0e2efc68407e7b20c71a7f4332846a76a7fb +Subproject commit 5baec02f0ac71e30959014c2ee523ec17a4545b1