Add proof for the other version of secure_set_bits.
@@ -147,8 +147,6 @@ let is_new_spec = do {
// Must have weight < max (T1, FAKE_DV), or an assertion fails.
// a_len_64 is the length of a `a` array, and is 1/8 times `a_len_bytes
-let MAX_WEIGHT = eval_int {{ max (`T1:[64]) (`FAKE_DV:[64]) }};
-
let secure_set_bits_loop_spec a_len_64 weight = do {
(a ,a_ptr) <- inout_ref (plain_type (llvm_array a_len_64 i64)) "a";
a_ptr_ptr <- crucible_alloc i64;
@@ -160,8 +158,8 @@ let secure_set_bits_loop_spec a_len_64 weight = do {
crucible_points_to a_len_8_ptr (crucible_term {{ 8 * (`a_len_64:[32]) }});
weight_ptr <- crucible_alloc i32;
crucible_points_to weight_ptr (crucible_term {{ `weight:[32] }});
- (qw_pos, qw_pos_ptr) <- inout_ref (make_i64_T MAX_WEIGHT) "qw_pos";
- (bit_pos, bit_pos_ptr) <- inout_ref (make_i64_T MAX_WEIGHT) "bit_pos";
+ (qw_pos, qw_pos_ptr) <- in_ref (make_i64_T weight) "qw_pos";
+ (bit_pos, bit_pos_ptr) <- in_ref (make_i64_T weight) "bit_pos";
(tmp, tmp_ptr) <- ptr_to_fresh "tmp" i64;
(qw, qw_ptr) <- ptr_to_fresh "qw" i32;
(j, j_ptr) <- ptr_to_fresh "j" i32;
@@ -513,7 +511,7 @@ secure_set_bits_GSFR_loop_ov <- admit "__breakpoint__secure_set_bits_loop#secure
verify "__breakpoint__secure_set_bits_loop#secure_set_bits"
[secure_set_bits_GSFR_loop_ov, secure_cmp32_ov]
(secure_set_bits_loop_spec (eval_int {{( `R_PADDED_SIZE:[32])/8 }}) FAKE_DV);
-secure_set_bits_GSFR_ov <- admit "secure_set_bits"
+secure_set_bits_GSFR_ov <- verify "secure_set_bits"
[secure_set_bits_GSFR_loop_ov, secure_cmp32_ov]
(secure_set_bits_spec (eval_int {{( `R_PADDED_SIZE:[32])/8 }}) FAKE_DV);
