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?