Updated the proof of gcm_init_avx to reflect the location change of g…

…lobal constant L0x1c2_polynomial. (#106)
awslabs · Jun 7, 2023 · 4af55bb · 4af55bb
1 parent e3287aa
commit 4af55bb
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 7 deletions.
diff --git a/.gitmodules b/.gitmodules
@@ -1,7 +1,7 @@
 [submodule "src"]
 	path = src
 	branch = main
-	url = https://github.com/aws/aws-lc.git
+	url = https://github.com/shirsing0712/aws-lc.git
 [submodule "cryptol-specs"]
 	path = cryptol-specs
 	branch = sha-imperative

diff --git a/SAW/proof/AES/GHASH.saw b/SAW/proof/AES/GHASH.saw
@@ -55,8 +55,10 @@ gcm_init_avx_ov <- llvm_verify_x86 m "../../build/x86/crypto/crypto_test" "gcm_i
   //    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 (8 bytes) ) + the displacement offset
-  [ ("byte64_len_to_mask_table", 1152) // We need .L0x1c2_polynomial. Its location is <byte64_len_to_mask_table+0x450>. 1152 bytes is an offset that would be large enough to contain the right bytes after alignment.
+  //      %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.
   ]
   true
   gcm_init_avx_spec
@@ -68,7 +70,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"
-  [ ("byte64_len_to_mask_table", 1152)
+  [ ("shufb_15_7", 384)
   ]
   true
   gcm_gmult_avx_spec
@@ -90,14 +92,14 @@ let gcm_ghash_avx_tactic = do {
 };
 
 gcm_ghash_avx_encrypt_ov <- llvm_verify_x86 m "../../build/x86/crypto/crypto_test" "gcm_ghash_avx"
-  [ ("byte64_len_to_mask_table", 1152)
+  [ ("shufb_15_7", 384)
   ]
   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"
-  [ ("byte64_len_to_mask_table", 1152)
+  [ ("shufb_15_7", 384)
   ]
   true
   (gcm_ghash_avx_spec GHASH_length_blocks_decrypt)

diff --git a/src b/src