Verification results of `#[proof]` and #[proof_for_contract] are different

[zjp-CN]

I'm writing some basic tests, and find verification results of standard proof and proof_for_contract are different :

#[kani::requires(a > 0)]
fn contract(a: u8) {}

#[kani::proof] // VERIFICATION:- FAILED
fn proof() {
    contract(0);
}

#[kani::proof_for_contract(contract)] // VERIFICATION:- SUCCESSFUL
fn proof() {
    contract(0);
}

using the following command line invocation:

kani file.rs # for #[kani::proof] - VERIFICATION:- FAILED
kani -Zfunction-contracts file.rs # for #[kani::proof_for_contract(contract)] - VERIFICATION:- SUCCESSFUL

with Kani version: c87c7d0

I expected to see this happen: #[kani::proof_for_contract(contract)] proof fails as #[kani::proof] proof does

Instead, this happened: #[kani::proof_for_contract(contract)] proof succeeds

---

Maybe relate to #3864 and #3905

[carolynzech]

Hi, this is expected behavior. The goal of #[kani::proof_for_contract] is to provide a proof that if the precondition holds, then the postcondition holds (and we don't encounter any UB, panics, etc. along the way). So Kani will assume the precondition, meaning that when it encounters

#[kani::requires(a > 0)]
fn contract(a: u8) {}

it will assume that a > 0. When you provide an input that is incompatible with that assumption, you empty the search space, making your proof vacuously succeed. You can see that behavior if you change contract to be this:

#[kani::requires(a > 0)]
#[kani::ensures(|_| a > 0)]
fn contract(a: u8) {}

and run the #[proof_for_contract], getting this:

Check 4: contract::{closure#2}.assertion.1
         - Status: UNREACHABLE
         - Description: "|_| a > 0"
         - Location: src/lib.rs:2:1 in function contract::{closure#2}

This postcondition should fail, but since the unsatisfiable assumption emptied the search space, we don't reach it.

As for why the #[kani::proof] fails--#3802 made it so that we generate contracts of dependencies/callees as assertions. What this means is that if you have a #[kani::proof] that encounters a function with a contract somewhere in its call graph, it will assert that the caller respects the precondition of that contract. Thus, the #[kani::proof] fails because your input doesn't satisfy the precondition. If you want to disable this behavior, you can pass the --no-assert-contracts flag.

So while this is expected behavior, there are definitely things we can do on our end to make this behavior less surprising. We had some work in #3623 toward making proofs like this fail--if I run your original #[proof_for_contract] example on the code from that branch, I get:

SUMMARY:
 ** 1 of 90 failed
Failed Checks: The contract's precondition is satisfiable.

We closed this PR because of some unresolved UX questions, but I'd be happy to see this work picked back up again if you think that would improve the user experience. Do you have any suggestions for documentation, printed messages in the terminal, changes in proof behavior, etc. that you think would have made these results clearer for you?

[zjp-CN]

Thank you for explaining why the proof_for_contract example fails to catch verififaction failure and how to make it do so.

These links are also helpful.

As a user, I may expect kani to be correct as the top priority with regard to usage and functionality. So I think it's totally fine for me to see errors in strict mode if proofs or contracts go wrong, and when I'm sure about what I'm doing, then will look up the documentation to find how to solve or mitigate the problems.

It's not ok for me to run kani in silent mode if bugs could be caught in the first place.

These are my two cents.