Is it possible to cause unsoundness with an incorrect function contract?

[joshlf]

In the original blog post introducing function contracts, it is suggested that an incomplete proof harness can allow an unsound function contract to slip through.

I wrote the following:

#[kani::ensures(|&r| r != 0)]
fn foo() -> usize {
    #[kani::proof_for_contract(foo)]
    fn proof() {
        if 0 == 1 {
            foo();
        }
    }

    0
}

#[kani::proof]
fn prove_foo() {
    foo();
}

I expected prove_foo to succeed. In particular, proof should be taken as a proof of the soundness of foo's function contract. It is an incomplete proof, but as suggested in the blog post, Kani isn't smart enough to realize that. Thus, I would expect the proof of prove_foo to take the post-condition as an axiom. Instead, I get this error:

Checking harness prove_foo...

VERIFICATION RESULT:
 ** 1 of 10 failed
Failed Checks: |&r| r != 0
 File: "src/lib.rs", line 1, in util::foo::{closure#1}

I have two questions:

• Is it still true that an unsound function contract can cause unsoundness in proofs?
• If function contracts are not taken as axioms in proofs, then is there any performance benefit in using them, as suggested in the post?

[zhassan-aws]

Is it still true that an unsound function contract can cause unsoundness in proofs?

One common issue with function contracts is the usage of an overly-constrained pre-condition (similar to your example). While this can lead to a vacuous proof for the contract, the overconstrained pre-condition is typically caught when the function is stubbed with its contract. So to guarantee soundness, it is not sufficient to verify a function's contract; one must also verify that the function's callers satisfy its precondition.

If function contracts are not taken as axioms in proofs, then is there any performance benefit in using them, as suggested in the post?

Currently, using function contracts as axioms in proofs requires explicitly using the #[kani::stub_verified] attribute on a harness (see the Contracts section of the documentation. Without this attribute, Kani asserts the function's pre and post conditions, which is why verification fails in your example.

[remi-delmas-3000]

Adding to @zhassan-aws remark,

There's something strange in your example: foo itself contains a #[kani::proof_for_contract(foo)] harness for foo. This is not the intended use at all and I'm not sure we even try to catch that type of mistakes.

Coming back to contracts and how they are used:

Starting from this:

#[kani::requires(R)]
#[kani::modifies(M)]
#[kani::ensures(E)]
fn foo(x: Tx, Y: Tx) -> R {
  body(); 
}

You can check foo against its contract, in the context of some #[kani::proof_for_contract(foo)] harness function. The harness function is meant to allocate the symbolic inputs under which the function is going to be exercised:

#[kani::proof_for_contract(foo)]`
fn harness() {

    // preamble : allocate some nondeterministic inputs for `foo`
    let x = kani::any(); 
    let y = kani::any();

    // invoke foo with nondet inputs
    foo(x, y);
}

Under the hood, Kani generates a contract-checking wrapper for foo that looks like that:

 fn foo_wrapper(x: Tx, Y: Tx) -> R {
   kani::assume(R);
   let r = foo(x, y);
   assert!(E);
   r
}

and rewrites the call to foo in the proof harness with a call to foo_wrapper.

Ideally:

• the harness should allocate "maximally nondeterministic" input values for the function's inputs x: Tx and y: Ty, and the wrapper additionally constrains them via an assume to satisfy the requires clause R. The function would then be exercised under any possible value in R.
• Kani should be able to generate these maximally nondet inputs for you when input types are simple enough, e.g. when they only contain owned values, are not inductively defined, and are essentially bounded (@carolynzech is actively working on this with something called auto-harness).
• However, for anything more complex that that (raw pointers, Rc, etc.) you would need to specify explicitly how aliasing happens within the inputs using some language like separation logic or something similar.

Since we cannot yet do that in general in Kani, for now we let users write their own nondeterministic input generation code in these kani::proof_for_contract(foo) harnesses, and we apply preconditions as "assumes" in the wrapper function that we generate.

This means that if your manually written harness allocates anything less than the maximally nondeterministic values allowed by the input types, the function is potentially exercised under a subset of all possible values satisfying R, and some bad behaviors of the function may remain hidden in this analysis because they would only be reachable under these missing inputs.

For instance, foo requires x in [0,10] and panics when x == 10, but the harness generates x in [0, 9] so the analysis concludes that foo cannot panic. But the problem here is that the harness allocates inputs in a strict subset of the preconditions.

#[kani:requires(x <= 10)]
fn foo(x: u32) -> u32 {
   if x == 10 {
     panic!();
   }
}

#[kani::proof_for_contract(foo)]`
fn harness() {
   let x = kani::any_where(|x| *x < 10); //  over constrained !
   foo(x);
}

If that function is invoked in the program at some call site where these missing inputs can actually occur, even if the requires clause holds at this call site, the bad behaviors of the function can trigger :

fn bar() {
   let r = foo(10); // requires clause holds
                            // but `foo` still panics for x == 10
}

As to what happens when a function call is stubbed out by its contract and how it improves proof performance:

The stub generated for foo based on its contract looks roughly like this,

fn foo_stub() -> R {
  assert!(R);
  havoc(M);
  let r: R = kani::any();
  kani::assume(E);
}

It checks that the requires clause R holds, havocs all locations M from the modifies clause, and further constrains that havoced state with the ensures clause E.

This abstracts away the complexity of foos body instructions with three instructions assert/havoc/assume, which reduces the amount of code that Kani has to symbolically execute, reduces SAT/SMT formula size, and can ultimately improve solving time.

This works well in particular if the function behavior summary provided via the ensures clause E is smaller/simpler than the actual body of the function.

However, it does not always improve performance:

• For very short functions where the body and the postcondition say exactly the same thing, it is likely that this makes no difference, or even makes performance slightly worse (there is still some overhead to stubbing like extra wrapper calls, etc.).
• In other cases, replacing the imperative code of the function body with a declarative havoc/assume can prevent symbolic execution from propagating constants through the stubbed function call , which may negatively impact performance.

Hope this helps