Update BIKE R2 proofs to the latest SAW.

GaloisInc · Mar 27, 2020 · caa6bea · caa6bea
1 parent ce419d3
commit caa6bea
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 0 deletions.
diff --git 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
@@ -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;
+