Fail verification if contract is vacuous

[carolynzech]

Fail verification if a contract's preconditions empty the search space. This solution introduces a new Kani intrinsic, kani::internal::assume_unless_vacuous, which codegens to this:

 Stmt::block(
    vec![
       gcx.codegen_assume(cond, loc),
       // This `assert(false)` is new
       Stmt::assert_false(PropertyClass::AssumeUnlessVacuous.as_str(), &msg, loc),
       Stmt::goto(bb_label(target), loc),
     ],
     loc,
  )

The CBMC property renderer updates the results of these checks like so:

} else if prop.is_assume_unless_vacuous_property() {
   // if the assert(false) didn't fail, then something is wrong, so we fail verification
    if prop.status == CheckStatus::Success {
        prop.status = CheckStatus::Failure;
    // we expect the assert(false) to fail, so the check succeeds
    } else if prop.status == CheckStatus::Failure {
        prop.status = CheckStatus::Success;
    }
}

This solution is inspired by how we implement kani::cover.

Creating as a draft for now for feedback.

Resolves #2793

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[carolynzech]

Note that this fails the standard library job because a number of the unchecked_mul harnesses are restricted to ranges such that the precondition empties the search space. For example, verify::unchecked_mul_usize_edge performs lhs.unchecked_mul(rhs) on usizes between [u32::MAX / 2, u32::MAX], with a precondition that the product must not overflow. However, this product will always overflow, so the contract is vacuous and verification fails. If we decide we're happy with this behavior, I can create a PR to update those harnesses before merging this PR (or ping the CMU team who authored them).

[celinval]

May I suggest a different approach? I think we should add 2 special cover statements to harnesses. One before we invoke the function and one after we leave the function. This would help us understand whether the pre-conditions are ever satisfied, and if the post-condition is ever checked.

Note that this fails the standard library job because a number of the unchecked_mul harnesses are restricted to ranges such that the precondition empties the search space. For example, verify::unchecked_mul_usize_edge performs lhs.unchecked_mul(rhs) on usizes between [u32::MAX / 2, u32::MAX], with a precondition that the product must not overflow. However, this product will always overflow, so the contract is vacuous and verification fails. If we decide we're happy with this behavior, I can create a PR to update those harnesses before merging this PR (or ping the CMU team who authored them).

hummm... that's an interesting point. I don't think the harness is incorrect though. I am not sure what the best approach is here to combine problem partitioning and the vacuous contract check. Maybe what we want is to combine harnesses that verify the same contract.

[celinval]

* I'm changing the result of undetermined checks to failure if there's unwinding failures. My rationale is that in the case of code like this:

I would prefer if we don't do that. We can discuss this further but I think it's out of scope of this PR.

[carolynzech]

Moving to draft for now -- we need to decide whether we want verification failure for these properties to be the default behavior, or a characteristic of the harness. This implementation has failure as the default behavior, but one could imagine that in the unchecked_mul case I mentioned above, you may want something like this:

#[requires(!self.overflowing_mul(rhs).1)]
pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self {
  ...
}

#[kani::proof_for_contract(unchecked_mul)]
// without this attribute, verification would fail because of a vacuous proof,
// but maybe you want to sanity check your precondition
// by having a separate harness with just invalid inputs
#[kani::allow_vacuity]
fn unchecked_mul_usize_edge() {
  let lhs: u32 = kani::any_where(|num| num >= u32::MAX / 2);
  let rhs: u32 = kani::any_where(|num| num >= u32::MAX / 2);
  lhs.unchecked_mul(rhs);
}

// This harness will fail for a vacuous proof by default
#[kani::proof_for_contract(unchecked_mul)]
fn unchecked_mul_middle() { ... }

Partitioning harnesses like this is a reasonable thing to do (and in fact, an approach we recommend and would like to implement as a feature) so failing by default could produce a bad experience for users. Introducing a harness-level attribute requires further discussion, however.

[carolynzech]

Closing this PR, since we don't have an answer for the UX questions and we have other features that are higher priority right now.