Point src to fips-2022-11-02

SAW/proof/AES/AESNI-GCM.saw

@@ -61,14 +61,14 @@ add_x86_preserved_reg "rax";
 enable_what4_hash_consing;
 
 aesni_gcm_encrypt_ov <- llvm_verify_x86 m "../../build/x86/crypto/crypto_test" "aesni_gcm_encrypt"
-  [ ("byte64_len_to_mask_table", 640) // We need .Lbswap_mask. Its location is <byte64_len_to_mask_table+0x240>. 640 bytes is an offset that would be large enough to contain the right bytes after alignment.
+[ ("aesni_gcm_encrypt", 1200) // we need .Lbswap_mask, which lives in .text after aesni_gcm_encrypt (1081 bytes itself). 1200 bytes is an arbitrary size that I guessed would be large enough to contain the right bytes after alignment.
   ]
   true
   (aesni_gcm_cipher_spec {{ 1 : [32] }} aesni_gcm_cipher_gcm_len aesni_gcm_cipher_len)
   aesni_gcm_cipher_tactic;
 
 aesni_gcm_decrypt_ov <- llvm_verify_x86 m "../../build/x86/crypto/crypto_test" "aesni_gcm_decrypt"
-  [ ("byte64_len_to_mask_table", 640)
+[ ("aesni_gcm_encrypt", 1200) // we need .Lbswap_mask, which lives in .text after aesni_gcm_encrypt (1081 bytes itself). 1200 bytes is an arbitrary size that I guessed would be large enough to contain the right bytes after alignment.
   ]
   true
   (aesni_gcm_cipher_spec {{ 0 : [32] }} aesni_gcm_cipher_gcm_len aesni_gcm_cipher_len)

SAW/proof/AES/GHASH.saw

@@ -48,17 +48,7 @@ let gcm_ghash_avx_spec len = do {
 
 enable_what4_hash_consing;
 gcm_init_avx_ov <- llvm_verify_x86 m "../../build/x86/crypto/crypto_test" "gcm_init_avx"
-  // How to find clues for constructing the global symbol pair?
-  // 1. Find the location of the function "gcm_init_avx" in the assembly
-  //    using "nm crypto_test | grep gcm_init_avx"
-  // 2. Find the instruction that uses the constant L0x1c2_polynomial
-  //    using "objdump -S --start-address=... --stop-address=... crypto_test"
-  // 3. If there is a comment, then the comment tells us where that constant is;
-  //    else the address should be
-  //      %rip ( which is current_instruction_addr + current_instruction_size ) + the displacement offset
-  // 4. If one wants to confirm the location, try
-  //      objdump -s -j .rodata crypto_test
-  [ ("shufb_15_7", 384) // We need .L0x1c2_polynomial. Its location is <shufb_15_7+0x160>. 384 bytes is an offset that would be large enough to contain the right bytes after alignment.
+  [ ("gcm_ghash_avx", 1800) // similar hack to the one in AESNI-GCM.saw to grab .L0x1c2_polynomial, we need a better way to handle this
   ]
   true
   gcm_init_avx_spec
@@ -70,7 +60,7 @@ gcm_init_avx_ov <- llvm_verify_x86 m "../../build/x86/crypto/crypto_test" "gcm_i
 disable_what4_hash_consing;
 
 gcm_gmult_avx_ov <- llvm_verify_x86 m "../../build/x86/crypto/crypto_test" "gcm_gmult_avx"
-  [ ("shufb_15_7", 384)
+  [ ("gcm_ghash_avx", 1800)
   ]
   true
   gcm_gmult_avx_spec
@@ -92,14 +82,14 @@ let gcm_ghash_avx_tactic = do {
 };
 
 gcm_ghash_avx_encrypt_ov <- llvm_verify_x86 m "../../build/x86/crypto/crypto_test" "gcm_ghash_avx"
-  [ ("shufb_15_7", 384)
+  [ ("gcm_ghash_avx", 1800)
   ]
   true
   (gcm_ghash_avx_spec GHASH_length_blocks_encrypt)
   gcm_ghash_avx_tactic;
 
 gcm_ghash_avx_decrypt_ov <- llvm_verify_x86 m "../../build/x86/crypto/crypto_test" "gcm_ghash_avx"
-  [ ("shufb_15_7", 384)
+  [ ("gcm_ghash_avx", 1800)
   ]
   true
   (gcm_ghash_avx_spec GHASH_length_blocks_decrypt)