diff --git a/SAW/proof/Loop.cry b/SAW/proof/Loop.cry index 97466464..06eb0f8b 100644 --- a/SAW/proof/Loop.cry +++ b/SAW/proof/Loop.cry @@ -333,7 +333,8 @@ aesni_gcm_decrypt_impl_loop_step len in out key ivec ctr Xi , loop_index + 1 ) where - next_prefetch_offset = prefetch_offset + (if prefetch_offset + 192 <= len then 96 else 0) + //next_prefetch_offset = prefetch_offset + (if prefetch_offset + 192 <= len then 96 else 0) + next_prefetch_offset = prefetch_offset + (if prefetch_offset + 4096 <= len + 3904 then 96 else 0) [in_block0, in_block1, in_block2, in_block3, in_block4, in_block5] = split (join (arrayRangeLookup in (loop_index * 96))) (next_T1, [out_block0, out_block1, out_block2, out_block3, out_block4, out_block5]) = aes_encrypt_blocks_6_impl key ctr_least_byte T1 inout0 inout1 inout2 inout3 inout4 inout5 [in_block0, in_block1, in_block2, in_block3, in_block4, in_block5] diff --git a/SAW/proof/loop_test.saw b/SAW/proof/loop_test.saw index ac9fad9b..c153dcc3 100644 --- a/SAW/proof/loop_test.saw +++ b/SAW/proof/loop_test.saw @@ -713,19 +713,19 @@ aes_encrypt_blocks_6_impl_thm <- prove_theorem goal_normalize ["aesEncryptWithKeySchedule", "ExpandKey"]; w4_unint_z3 ["aesEncryptWithKeySchedule", "ExpandKey"]; }) - (rewrite (cryptol_ss ()) {{ \key (iv : [12][8]) (ctr : [4][8]) (loop_index : [64]) blocks -> + (rewrite (cryptol_ss ()) {{ \key (iv : [12][8]) (ctr : [4][8]) (block_index : [64]) blocks -> aes_encrypt_blocks_6_impl key - (0 # ((swap8 (join ctr)) + (((drop (6 * loop_index + 12)) : [8]) # 0))) - (0 # (swap8 ((join iv) # ((join ctr) + (drop (6 * loop_index + 12)))))) - (0 # ((swap8 ((join iv) # ((join ctr) + (drop (6 * loop_index + 12))))) ^ (join (reverse (take key))))) - (0 # ((swap8 ((join iv) # ((join ctr) + (drop (6 * loop_index + 12))))) + ((1 : [8]) # 0))) - (0 # ((swap8 ((join iv) # ((join ctr) + (drop (6 * loop_index + 12))))) + ((2 : [8]) # 0))) - (0 # ((swap8 ((join iv) # ((join ctr) + (drop (6 * loop_index + 12))))) + ((3 : [8]) # 0))) - (0 # ((swap8 ((join iv) # ((join ctr) + (drop (6 * loop_index + 12))))) + ((4 : [8]) # 0))) - (0 # ((swap8 ((join iv) # ((join ctr) + (drop (6 * loop_index + 12))))) + ((5 : [8]) # 0))) + (0 # ((swap8 (join ctr)) + (((drop block_index) : [8]) # 0))) + (0 # (swap8 ((join iv) # ((join ctr) + (drop block_index))))) + (0 # ((swap8 ((join iv) # ((join ctr) + (drop block_index)))) ^ (join (reverse (take key))))) + (0 # ((swap8 ((join iv) # ((join ctr) + (drop block_index)))) + ((1 : [8]) # 0))) + (0 # ((swap8 ((join iv) # ((join ctr) + (drop block_index)))) + ((2 : [8]) # 0))) + (0 # ((swap8 ((join iv) # ((join ctr) + (drop block_index)))) + ((3 : [8]) # 0))) + (0 # ((swap8 ((join iv) # ((join ctr) + (drop block_index)))) + ((4 : [8]) # 0))) + (0 # ((swap8 ((join iv) # ((join ctr) + (drop block_index)))) + ((5 : [8]) # 0))) blocks - == ((swap8 ((join iv) # ((join ctr) + (drop (6 * (loop_index + 1) + 12))))), aes_ctr32_encrypt_blocks (join key) (join iv) ((join ctr) + (drop (6 * loop_index + 12))) blocks) }}); + == ((swap8 ((join iv) # ((join ctr) + (drop (block_index + 6))))), aes_ctr32_encrypt_blocks (join key) (join iv) ((join ctr) + (drop block_index)) blocks) }}); gcm_polyval_red_half_pmult_thm <- prove_theorem (w4_unint_yices ["gcm_polyval_red_half_pmult"]) @@ -773,7 +773,6 @@ let {{ (aesni_gcm_encrypt_impl_loop_step' len in out key iv ctr Xi (aesni_gcm_encrypt_impl_loop len in out key iv ctr Xi ( impl_out - // stack values , join (arrayRangeLookup`{n=8} impl_out (96 * loop_index + 72)) , join (arrayRangeLookup`{n=8} impl_out (96 * loop_index + 64)) , join (arrayRangeLookup`{n=8} impl_out (96 * loop_index + 56)) @@ -785,7 +784,6 @@ let {{ , 0 , join (arrayRangeLookup`{n=8} impl_out (96 * loop_index + 8)) , join (arrayRangeLookup`{n=8} impl_out (96 * loop_index)) - // XMM registers , 0 # ((swap8 ((join iv) # ((join ctr) + (drop (6 * loop_index + 12))))) + ((5 : [8]) # 0)) , 0 # ((swap8 ((join iv) # ((join ctr) + (drop (6 * loop_index + 12))))) + ((4 : [8]) # 0)) , 0 # ((swap8 ((join iv) # ((join ctr) + (drop (6 * loop_index + 12))))) + ((3 : [8]) # 0)) @@ -796,7 +794,6 @@ let {{ , 0 # (join (arrayRangeLookup`{n=16} impl_out (96 * loop_index + 80))) , 0 , 0 # (swap8 ((join iv) # ((join ctr) + (drop (6 * loop_index + 12))))) - // GP registers , 96 * loop_index , 0 # ((swap8 (join ctr)) + (((drop (6 * loop_index + 12)) : [8]) # 0)) , loop_index @@ -862,29 +859,22 @@ aesni_gcm_encrypt_impl_loop_thm <- prove_theorem split_ite (do { goal_eval_unint ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl"]; - print_goal; w4_unint_z3 ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl"]; }) (do { goal_eval_unint ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl"]; - print_goal; w4_unint_z3 ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl"]; }); }); }) (do { - w4_unint_z3 ["aesni_gcm_encrypt", "aesni_gcm_encrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_encrypt_output_and_tag", "aesni_gcm_encrypt_impl_loop_step'"]; + w4_unint_z3 ["aesni_gcm_encrypt"]; }); }) (rewrite (cryptol_ss ()) (unfold_term ["aesni_gcm_encrypt_impl_loop_stmt"] {{ aesni_gcm_encrypt_impl_loop_stmt }})); -ite_decrypt_out_and_tag_thm <- prove_theorem - (do { - w4_unint_yices ["aesni_gcm_decrypt_impl_loop_step", "get_decrypt_output_and_tag"]; - }) - (rewrite (cryptol_ss ()) ({{ \len in out key iv ctr Xi c x y-> - pairEq - (get_decrypt_output_and_tag (aesni_gcm_decrypt_impl_loop_step len in out key iv ctr Xi (if c then x else y))) - (if c then (get_decrypt_output_and_tag (aesni_gcm_decrypt_impl_loop_step len in out key iv ctr Xi x)) else (get_decrypt_output_and_tag (aesni_gcm_decrypt_impl_loop_step len in out key iv ctr Xi y))) }})); +let {{ + aesni_gcm_decrypt_impl_loop_step' = aesni_gcm_decrypt_impl_loop_step +}}; out_and_tag_aesni_gcm_decrypt_impl_loop_thm <- prove_theorem (do { @@ -893,66 +883,87 @@ out_and_tag_aesni_gcm_decrypt_impl_loop_thm <- prove_theorem }) (rewrite (cryptol_ss ()) {{ \len in out key iv ctr Xi loop_tuple -> pairEq - (get_decrypt_output_and_tag (aesni_gcm_decrypt_impl_loop_step len in out key iv ctr Xi (aesni_gcm_decrypt_impl_loop len in out key iv ctr Xi (aesni_gcm_decrypt_impl_loop_step len in out key iv ctr Xi loop_tuple)))) - (get_decrypt_output_and_tag (aesni_gcm_decrypt_impl_loop_step len in out key iv ctr Xi (aesni_gcm_decrypt_impl_loop len in out key iv ctr Xi (combine_Xi_parts (aesni_gcm_decrypt_impl_loop_step len in out key iv ctr Xi loop_tuple))))) + (get_decrypt_output_and_tag (aesni_gcm_decrypt_impl_loop_step' len in out key iv ctr Xi (aesni_gcm_decrypt_impl_loop len in out key iv ctr Xi (aesni_gcm_decrypt_impl_loop_step len in out key iv ctr Xi loop_tuple)))) + (get_decrypt_output_and_tag (aesni_gcm_decrypt_impl_loop_step' len in out key iv ctr Xi (aesni_gcm_decrypt_impl_loop len in out key iv ctr Xi (combine_Xi_parts (aesni_gcm_decrypt_impl_loop_step len in out key iv ctr Xi loop_tuple))))) }}); let aesni_gcm_decrypt_impl_loop_stmt = rewrite (cryptol_ss ()) {{ \len in out key iv ctr Xi loop_index current_out current_Xi -> pairEq (aesni_gcm_decrypt len in out key iv ctr Xi loop_index current_out current_Xi) - (get_decrypt_output_and_tag (aesni_gcm_decrypt_impl_loop_step len in out key iv ctr Xi (aesni_gcm_decrypt_impl_loop len in out key iv ctr Xi - ( current_out - // stack values - , join (arrayRangeLookup`{n=8} in (96 * loop_index + 72)) - , join (arrayRangeLookup`{n=8} in (96 * loop_index + 64)) - , join (arrayRangeLookup`{n=8} in (96 * loop_index + 56)) - , join (arrayRangeLookup`{n=8} in (96 * loop_index + 48)) - , join (arrayRangeLookup`{n=8} in (96 * loop_index + 40)) - , join (arrayRangeLookup`{n=8} in (96 * loop_index + 32)) - , join (arrayRangeLookup`{n=8} in (96 * loop_index + 24)) - , join (arrayRangeLookup`{n=8} in (96 * loop_index + 16)) - , 0 - , join (arrayRangeLookup`{n=8} in (96 * loop_index + 8)) - , join (arrayRangeLookup`{n=8} in (96 * loop_index)) - // XMM registers - , 0 # ((swap8 ((join iv) # ((join ctr) + (drop (6 * loop_index))))) + (5 << 120)) - , 0 # ((swap8 ((join iv) # ((join ctr) + (drop (6 * loop_index))))) + (4 << 120)) - , 0 # ((swap8 ((join iv) # ((join ctr) + (drop (6 * loop_index))))) + (3 << 120)) - , 0 # ((swap8 ((join iv) # ((join ctr) + (drop (6 * loop_index))))) + (2 << 120)) - , 0 # ((swap8 ((join iv) # ((join ctr) + (drop (6 * loop_index))))) + (1 << 120)) - , 0 # ((swap8 ((join iv) # ((join ctr) + (drop (6 * loop_index))))) ^ (join (reverse (take key)))) - , 0 # current_Xi - , 0 # (join (arrayRangeLookup`{n=16} in (96 * loop_index + 80))) - , 0 - , 0 # (swap8 ((join iv) # ((join ctr) + (drop (6 * loop_index))))) - // GP registers - , 96 * loop_index - , 0 # ((swap8 (join ctr)) + ((drop (6 * loop_index)) << 24)) - , loop_index - )))) + (if (6 * loop_index <= (len / 16) - 6) && (96 <= len) && (len < 68719476736) && (loop_index <= ((len / 16) / 6) - 1) then + (get_decrypt_output_and_tag + (aesni_gcm_decrypt_impl_loop_step' len in out key iv ctr Xi + (aesni_gcm_decrypt_impl_loop len in out key iv ctr Xi + ( current_out + , join (arrayRangeLookup`{n=8} in (96 * loop_index + 72)) + , join (arrayRangeLookup`{n=8} in (96 * loop_index + 64)) + , join (arrayRangeLookup`{n=8} in (96 * loop_index + 56)) + , join (arrayRangeLookup`{n=8} in (96 * loop_index + 48)) + , join (arrayRangeLookup`{n=8} in (96 * loop_index + 40)) + , join (arrayRangeLookup`{n=8} in (96 * loop_index + 32)) + , join (arrayRangeLookup`{n=8} in (96 * loop_index + 24)) + , join (arrayRangeLookup`{n=8} in (96 * loop_index + 16)) + , 0 + , join (arrayRangeLookup`{n=8} in (96 * loop_index + 8)) + , join (arrayRangeLookup`{n=8} in (96 * loop_index)) + , 0 # ((swap8 ((join iv) # ((join ctr) + (drop (6 * loop_index))))) + ((5 : [8]) # 0)) + , 0 # ((swap8 ((join iv) # ((join ctr) + (drop (6 * loop_index))))) + ((4 : [8]) # 0)) + , 0 # ((swap8 ((join iv) # ((join ctr) + (drop (6 * loop_index))))) + ((3 : [8]) # 0)) + , 0 # ((swap8 ((join iv) # ((join ctr) + (drop (6 * loop_index))))) + ((2 : [8]) # 0)) + , 0 # ((swap8 ((join iv) # ((join ctr) + (drop (6 * loop_index))))) + ((1 : [8]) # 0)) + , 0 # ((swap8 ((join iv) # ((join ctr) + (drop (6 * loop_index))))) ^ (join (reverse (take key)))) + , 0 # current_Xi + , 0 # (join (arrayRangeLookup`{n=16} in (96 * loop_index + 80))) + , 0 + , 0 # (swap8 ((join iv) # ((join ctr) + (drop (6 * loop_index))))) + , 96 * loop_index + , 0 # ((swap8 (join ctr)) + (((drop (6 * loop_index)) : [8]) # 0)) + , loop_index + )))) + else + (aesni_gcm_decrypt len in out key iv ctr Xi loop_index current_out current_Xi)) }}; aesni_gcm_decrypt_impl_loop_hyp <- prove_theorem assume_unsat aesni_gcm_decrypt_impl_loop_stmt; aesni_gcm_decrypt_impl_loop_thm <- prove_theorem (do { - unfolding_fix_once ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop"]; - simplify (cryptol_ss ()); - simplify (addsimps [aesni_gcm_decrypt_impl_loop_hyp] empty_ss); - simplify (addsimps [ite_decrypt_out_and_tag_thm, out_and_tag_aesni_gcm_decrypt_impl_loop_thm] empty_ss); - simplify (addsimps [gcm_ghash_blocks_6_pmult4_thm] empty_ss); - print_goal; - goal_eval_unint ["aesEncryptWithKeySchedule", "ExpandKey", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "aesni_gcm_decrypt_impl_loop"]; - simplify (addsimps [append_assoc_0_thm] empty_ss); - simplify (addsimps concat_assoc_0_thms empty_ss); - simplify (addsimps concat_assoc_1_thms empty_ss); - simplify (addsimps concat_assoc_2_thms empty_ss); - simplify (addsimps [foo_append_slice_thm, foo_append_slice_thm] empty_ss); - simplify (addsimps [append_assoc_0_thm] empty_ss); - goal_eval_unint ["aesEncryptWithKeySchedule", "ExpandKey", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "aesni_gcm_decrypt_impl_loop"]; - print_goal; - w4_unint_yices ["aesEncryptWithKeySchedule", "ExpandKey", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "aesni_gcm_decrypt_impl_loop"]; - //offline_w4_unint_z3 ["pmult", "pmod", "gcm_polyval", "aesEncryptWithKeySchedule", "ExpandKey", "aesni_gcm_decrypt_impl_loop", "get_Htable", "gcm_polyval_mul_pmult4", "gcm_polyval_red_half_pmult"] "lalala"; + split_ite (do { + unfolding_fix_once ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop"]; + unfolding ["get_loop_index"]; + + split_ite (do { + simplify (addsimp_shallow aesni_gcm_decrypt_impl_loop_hyp (cryptol_ss ())); + + split_ite (do { + simplify (addsimps [out_and_tag_aesni_gcm_decrypt_impl_loop_thm] (cryptol_ss ())); + unfolding ["aesni_gcm_decrypt_impl_loop_step"]; + simplify (addsimps [aes_encrypt_blocks_6_impl_thm] (cryptol_ss ())); + goal_normalize ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop", "aes_ctr32_encrypt_blocks", "aes_encrypt_blocks_6_impl", "gcm_ghash_blocks", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_decrypt_output_and_tag", "aesni_gcm_decrypt_impl_loop_step'"]; + simplify (addsimps [gcm_ghash_blocks_6_pmult4_thm] empty_ss); + goal_eval_unint ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop", "aes_ctr32_encrypt_block", "aes_encrypt_blocks_6_impl", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_decrypt_output_and_tag", "aesni_gcm_decrypt_impl_loop_step'"]; + + split_ite (do { + goal_eval_unint ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop", "aes_ctr32_encrypt_block", "aes_encrypt_blocks_6_impl", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_decrypt_output_and_tag", "aesni_gcm_decrypt_impl_loop_step'"]; + w4_unint_z3 ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop", "aes_ctr32_encrypt_block", "aes_encrypt_blocks_6_impl", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_decrypt_output_and_tag", "aesni_gcm_decrypt_impl_loop_step'"]; + }) (do { + w4_unint_z3 ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop", "aes_ctr32_encrypt_block", "aes_encrypt_blocks_6_impl", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_decrypt_output_and_tag", "aesni_gcm_decrypt_impl_loop_step'"]; + }); + }) (do { + goal_eval_unint ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_ghash_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_decrypt_output_and_tag", "aesni_gcm_decrypt_impl_loop_step", "aesni_gcm_decrypt_impl_loop_step'"]; + w4_unint_z3 ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_ghash_block", "gcm_polyval_pmult4_impl", "gcm_polyval_pmult3_impl", "get_decrypt_output_and_tag", "aesni_gcm_decrypt_impl_loop_step", "aesni_gcm_decrypt_impl_loop_step'"]; + }); + }) (do { + unfolding ["aesni_gcm_decrypt_impl_loop_step", "aesni_gcm_decrypt_impl_loop_step'"]; + simplify (addsimps [aes_encrypt_blocks_6_impl_thm] (cryptol_ss ())); + goal_normalize ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop", "aes_ctr32_encrypt_blocks", "gcm_ghash_blocks", "gcm_polyval_pmult4_impl"]; + simplify (addsimps [gcm_ghash_blocks_6_pmult4_thm] empty_ss); + goal_eval_unint ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_polyval_pmult4_impl"]; + w4_unint_z3 ["aesni_gcm_decrypt", "aesni_gcm_decrypt_impl_loop", "aes_ctr32_encrypt_block", "gcm_polyval_pmult4_impl"]; + }); + }) (do { + w4_unint_z3 ["aesni_gcm_decrypt"]; + }); }) aesni_gcm_decrypt_impl_loop_stmt; @@ -1026,20 +1037,23 @@ aesni_gcm_decrypt_array_ov <- llvm_verify_fixpoint_x86' m "../../../aws-lc-verif {{ aesni_gcm_decrypt_impl_loop }} (aesni_gcm_cipher_array_spec false) (do { - simplify (addsimps [aesni_gcm_decrypt_impl_loop_thm] empty_ss); + print_goal; + simplify (addsimp_shallow aesni_gcm_decrypt_impl_loop_thm empty_ss); simplify (addsimps [aesenc_key0_0_thm, aesenc_key0_1_thm, aesenclast_thm] empty_ss); simplify (addsimps [aesenc_aesenclast_thm, aesenc_aesenclast_1_thm] empty_ss); simplify (addsimps [aesEncryptWithKeySchedule_swap8_0_thm, aesEncryptWithKeySchedule_swap8_1_thm] empty_ss); //simplify (addsimps [aesenc_key0_0_thm, aesenc_key0_1_thm] empty_ss); //simplify (addsimps aesenclast_thms empty_ss); //simplify (addsimps [aesenc_aesenclast_thm] empty_ss); + print_goal; simplify (cryptol_ss ()); simplify (addsimps concat_assoc_0_thms empty_ss); simplify (addsimps concat_assoc_1_thms empty_ss); simplify (addsimps concat_assoc_2_thms empty_ss); simplify (addsimps [foo_append_slice_thm, bar_append_slice_thm] empty_ss); - goal_eval_unint ["pmult", "pmod", "gcm_polyval", "aesEncryptWithKeySchedule", "ExpandKey", "aesni_gcm_decrypt_impl_loop", "get_H'", "get_Htable"]; - goal_eval_unint ["pmult", "pmod", "gcm_polyval", "aesEncryptWithKeySchedule", "ExpandKey", "aesni_gcm_decrypt_impl_loop", "get_H'", "get_Htable"]; + print_goal; + goal_eval_unint ["aesni_gcm_decrypt", "pmult", "pmod", "gcm_polyval", "aesEncryptWithKeySchedule", "ExpandKey", "aesni_gcm_decrypt_impl_loop", "get_H'", "get_Htable"]; + goal_eval_unint ["aesni_gcm_decrypt", "pmult", "pmod", "gcm_polyval", "aesEncryptWithKeySchedule", "ExpandKey", "aesni_gcm_decrypt_impl_loop", "get_H'", "get_Htable"]; simplify (addsimps [aesEncryptWithKeySchedule_ExpandKey_thm] empty_ss); simplify (addsimps xor_slice_append_thms basic_ss); simplify (addsimps slice_slice_thms empty_ss); @@ -1048,11 +1062,11 @@ aesni_gcm_decrypt_array_ov <- llvm_verify_fixpoint_x86' m "../../../aws-lc-verif simplify (addsimps concat_assoc_1_thms empty_ss); simplify (addsimps concat_assoc_2_thms empty_ss); simplify (addsimps [append_0_xor_thm, append_xor_0_thm, append_add_thm] empty_ss); - goal_eval_unint ["pmult", "pmod", "gcm_polyval", "aesEncryptWithKeySchedule", "aesni_gcm_decrypt_impl_loop", "get_H'", "get_Htable"]; + goal_eval_unint ["aesni_gcm_decrypt", "pmult", "pmod", "gcm_polyval", "aesEncryptWithKeySchedule", "aesni_gcm_decrypt_impl_loop", "get_H'", "get_Htable"]; //goal_normalize ["pmult", "pmod", "gcm_polyval", "aesEncryptWithKeySchedule", "aes_key_to_schedule", "aes_key_from_schedule", "ExpandKey", "aesni_gcm_decrypt_impl_loop"]; print_goal; - w4_unint_yices ["pmult", "pmod", "gcm_polyval", "aesEncryptWithKeySchedule", "ExpandKey", "aesni_gcm_decrypt_impl_loop", "get_H'", "get_Htable"]; - //w4_unint_z3 ["pmult", "pmod", "gcm_polyval", "aesEncryptWithKeySchedule", "ExpandKey", "aesni_gcm_decrypt_impl_loop", "get_H'", "get_Htable"]; + w4_unint_yices ["aesni_gcm_decrypt", "pmult", "pmod", "gcm_polyval", "aesEncryptWithKeySchedule", "ExpandKey", "aesni_gcm_decrypt_impl_loop", "get_H'", "get_Htable"]; + //w4_unint_z3 ["aesni_gcm_decrypt", "pmult", "pmod", "gcm_polyval", "aesEncryptWithKeySchedule", "ExpandKey", "aesni_gcm_decrypt_impl_loop", "get_H'", "get_Htable"]; }); default_x86_preserved_reg;