Skip to content

Commit

Permalink
wip
Browse files Browse the repository at this point in the history
  • Loading branch information
@andreistefanescu
andreistefanescu committed Dec 18, 2023
1 parent 93cba5c commit cdb6a1b
Show file tree
Hide file tree
Showing 2 changed files with 95 additions and 80 deletions.
3 changes: 2 additions & 1 deletion SAW/proof/Loop.cry
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
172 changes: 93 additions & 79 deletions SAW/proof/loop_test.saw
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"])
Expand Down Expand Up @@ -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))
Expand All @@ -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))
Expand All @@ -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
Expand Down Expand Up @@ -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 {
Expand All @@ -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;

Expand Down Expand Up @@ -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);
Expand All @@ -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;
Expand Down

0 comments on commit cdb6a1b

Please sign in to comment.