Default behaviour for pre and postconditions

[AlexLB99]

Hi,

We were wondering about Kani's default behaviour with respect to pre and postconditions.

In modular verification, when we encounter a function call, we would normally want to guarantee (assert) its precondition and assume its postcondition (e.g., if a function f1() that we're verifying calls another function f2() that has a contract, we would want to guarantee f2()'s preconditions just prior to the call, and assume its postconditions right after the call). This is currently possible in Kani via stubbing (#[kani::stub_verified(f2)]).

What we were wondering in particular is whether, in the situation where we are calling f2() from f1() (where f1() would be a #[kani::proof] for instance), it would be better for Kani to assert the preconditions and assume the postconditions of f2(), as it currently would if we were stubbing f2(). It seems that the current default behaviour in the absence of a #[kani::stub_verified] is to symbolically execute f2() (via inlining). We suspect that stubbing could be a better default behaviour (to leverage assume/guarantee reasoning and to support recursion), but are wondering what the thought process here is.

Thanks!

[SebTardif]

@AlexLB99

It seems that the current default behaviour in the absence of a #[kani::stub_verified] is to symbolically execute f2() (via inlining). We suspect that stubbing could be a better default behaviour (to leverage assume/guarantee reasoning and to support recursion)

Inlining is the right default for Kani. Making stubbing the default would be unsound for the way this repo uses proofs.

Kani is a bounded model checker. A #[kani::proof] harness is a closed program. Every callee body is part of what CBMC explores. Inlining f2 checks the actual implementation, including cases a contract forgot. That is what you want for "this core/alloc function has no UB" and for challenge harnesses in verify-rust-std.

#[kani::stub_verified(f2)] is assume/guarantee reasoning: assert f2's requires at the call, replace the body with the ensures. That is only sound if:

1. someone verified f2 against that contract (or you are willing to trust it),
2. the contract over-approximates every behavior the body can have,
3. you are not trying to catch bugs inside f2 itself.

If stubbing were the default, a missing or weak contract on f2 would silently assume a postcondition the body does not satisfy, and the harness would go green. Recursion is the one place where inlining hurts (unwinding). That is exactly why stub_verified exists as an opt-in.

A split that works here:

• Default: inline, so challenge harnesses keep checking real std bodies.
• Modular: stub_verified at crate boundaries and for recursive helpers, once those callees have their own harnesses.

Contract-first tools flip this default because their unit of proof is the contract, not a bounded unrolling of the body. I maintain Assura, which treats requires/ensures as assume/guarantee (Z3 and CVC5) and can also encode some Rust bodies with assura check-rust when you want a body proof instead of a stub. That is a different workflow. It does not change Kani's default, which should stay "execute the body."