Kani doesn't check that stub_verified contracts are verified

[carolynzech]

I tried this code:

#[kani::ensures(|res| *res == 7)]
fn foo() -> u8 {
    8
}

#[kani::proof]
#[kani::stub_verified(foo)]
fn harness() {
    let x: u8 = foo();
    assert!(x == 7);
}

using the following command line invocation:

cargo kani -Zfunction-contracts

with Kani version: 0.65.0

I expected to see this happen: verification failure since the ensures clause condition is incorrect, so the contract is an unsound abstraction for foo's body.

Instead, this happened: verification succeeded.

The contracts RFC says that Kani errors if there isn't a contract harness for a verified stub:

Each contract (from the local crate7) that is used in a stub_verified is required to have at least one associated contract harness. Kani reports any missing contract harnesses as errors.

But it looks like this never got implemented. This is a soundness hole; the name of the attribute implies that Kani checks the contract before doing the stubbing, but it doesn't.

(Also, we should probably require passing -Z stubbing to use stub_verified).

[zhassan-aws]

I'm pretty sure the error was there at some point.

[zhassan-aws]

Or maybe the error message we had was only for the case where #[stub_verified] is specified, but there's no contract.

[carolynzech]

Or maybe the error message we had was only for the case where #[stub_verified] is specified, but there's no contract.

Yes, that error exists:

kani/kani-compiler/src/kani_middle/attributes.rs

Lines 602 to 607 in 100857e

	dcx.struct_span_err(
	attr.span(),
	format!(
	"Target function in stub_verified, `{}`, has no contract.",
	stub_target.trimmed_name()
	),