From caa6beabaac31cf61d48ac84d520c2f058fced5e Mon Sep 17 00:00:00 2001 From: Andrei Stefanescu Date: Thu, 26 Mar 2020 17:51:16 -0700 Subject: [PATCH] Update BIKE R2 proofs to the latest SAW. --- tests/saw/bike_r2/proof/decode.saw | 2 ++ tests/saw/bike_r2/proof/sampling.saw | 4 ++++ 2 files changed, 6 insertions(+) diff --git a/tests/saw/bike_r2/proof/decode.saw b/tests/saw/bike_r2/proof/decode.saw index a7d0af13ef0..803d202cfb6 100644 --- a/tests/saw/bike_r2/proof/decode.saw +++ b/tests/saw/bike_r2/proof/decode.saw @@ -107,8 +107,10 @@ compute_syndrome_ov <- verify compute_syndrome_fun_name ] compute_syndrome_spec; +enable_crucible_assert_then_assume; bit_sliced_adder_ov <- verify_pathsat "bit_sliced_adder" [] bit_sliced_adder_spec; +disable_crucible_assert_then_assume; bit_slice_full_subtract_ov <- verify "bit_slice_full_subtract" [] bit_slice_full_subtract_spec; diff --git a/tests/saw/bike_r2/proof/sampling.saw b/tests/saw/bike_r2/proof/sampling.saw index 46888bdcf88..2a8f6e675fb 100644 --- a/tests/saw/bike_r2/proof/sampling.saw +++ b/tests/saw/bike_r2/proof/sampling.saw @@ -250,6 +250,8 @@ secure_set_bits_DV_R_ov <- verify secure_set_bits_fun_name [secure_set_bits_DV_R_loop_ov] (secure_set_bits_spec R_PADDED_QW DV); +enable_crucible_assert_then_assume; + generate_sparse_rep_T1_N_loop_ov <- admit breakpoint__generate_sparse_rep_loop [] (generate_sparse_rep_loop_spec T1 N_BITS N_PADDED_SIZE); verify_pathsat breakpoint__generate_sparse_rep_loop @@ -274,3 +276,5 @@ generate_sparse_rep_DV_R_ov <- verify_pathsat generate_sparse_rep_fun_name [generate_sparse_rep_DV_R_loop_ov] (generate_sparse_rep_spec DV R_BITS R_PADDED_SIZE); +disable_crucible_assert_then_assume; +