Contracts

Consider the following example:

fn gcd(mut max: u8, mut min: u8) -> u8 {
    if min > max {
        std::mem::swap(&mut max, &mut min);
    }

    let rest = max % min;
    if rest == 0 { min } else { gcd(min, rest) }
}

Let's assume we want to verify some code that calls gcd. In the worst case, the number of steps (recursions) in gcd approaches 1.5 times the number of bits needed to represent the input numbers. So, for two large 64-bit numbers, a single call to gcd can take almost 96 iterations. It would be very expensive for Kani to unroll each of these iterations and then perform symbolic execution.

Instead, we can write contracts with guarantees about gcd's behavior. Once Kani verifies that gcd's contracts are correct, it can replace each invocation of gcd with its contracts, which reduces verification time for gcd's callers. For example, perhaps we want to ensure that the returned result does indeed divide both max and min. In that case, we could write contracts like these:

#[kani::requires(min != 0 && max != 0)]
#[kani::ensures(|result| *result != 0 && max % *result == 0 && min % *result == 0)]
#[kani::recursion]
fn gcd(mut max: u8, mut min: u8) -> u8 { ... }

Since gcd performs max % min (and perhaps swaps those values), passing zero as an argument could cause a division by zero. The requires contract tells Kani to restrict the range of nondeterministic inputs to nonzero ones so that we don't run into this error. The ensures contract is what actually checks that the result is a correct divisor for the inputs. (The recursion attribute is required when using contracts on recursive functions).

Then, we would write a harness to verify those contracts, like so:

#[kani::proof_for_contract(gcd)]
fn check_gcd() {
    let max: u8 = kani::any();
    let min: u8 = kani::any();
    gcd(max, min);
}

and verify it by running kani -Z function-contracts.

Once Kani verifies the contracts, we can use Kani's stubbing feature to replace all invocations to gcd with its contracts, for instance:

// Assume foo() invokes gcd().
// By using stub_verified, we tell Kani to replace 
// invocations of gcd() with its verified contracts.
#[kani::proof]
#[kani::stub_verified(gcd)]
fn check_foo() {
    let x: u8 = kani::any();
    foo(x);
}

By leveraging the stubbing feature, we can replace the (expensive) gcd call with a verified abstraction of its behavior, greatly reducing verification time for foo.

There is far more to learn about contracts. We highly recommend reading our blog post about contracts (from which this gcd example is taken). We also recommend looking at the contracts module in our documentation.