The order of requires clauses is not respected

[zhassan-aws]

I tried this code:

#[kani::requires(x == 0)]
#[kani::requires(x * y < 10)]
fn foo(x: u8, y: u8) {}

#[kani::proof_for_contract(foo)]
fn check_foo() {
    foo(kani::any(), kani::any());
}

using the following command line invocation:

cargo kani -Zfunction-contracts

with Kani version: d2f5dbe

I expected to see this happen: Verification successful

Instead, this happened: the multiplication overflow check failed:

SUMMARY:
 ** 1 of 49 failed
Failed Checks: attempt to multiply with overflow
 File: "src/lib.rs", line 2, in foo::{closure#2}

VERIFICATION:- FAILED

I would expect it to succeed because of the previous requires clause.

Interestingly, if I flip the order of the requires clauses, verification succeeds:

#[kani::requires(x * y < 10)]
#[kani::requires(x == 0)]
fn foo(x: u8, y: u8) {}

#[kani::proof_for_contract(foo)]
fn check_foo() {
    foo(kani::any(), kani::any());
}

SUMMARY:
 ** 0 of 49 failed

VERIFICATION:- SUCCESSFUL

[celinval]

I don't think we have established the evaluation order of contract predicates though.

[zhassan-aws]

I understand. It seems intuitive to expect that the order is respected though. This was the source of confusion in model-checking/verify-rust-std#99.

[carolynzech]

We decided not to fix this issue. If a user writes this:

#[requires(a)]
#[requires(b)]
fn foo() {...}

it's not obvious that b has a control flow dependency on a (i.e., that we should not evaluate b unless a is true). If the user wants to introduce such a dependency, they should do so explicitly, e.g.:

#[requires(a && b)]
fn foo() {...}