Module contracts

Kani implementation of function contracts.

Function contracts are still under development. Using the APIs therefore requires the unstable -Zfunction-contracts flag to be passed. You can join the discussion on contract design by reading our RFC and commenting on the tracking issue.

The function contract API is expressed as proc-macro attributes, and there are two parts to it.

1. Contract specification attributes: requires and ensures.
2. Contract use attributes: proof_for_contract and stub_verified.

Step-by-step Guide

Let us explore using a workflow involving contracts on the example of a simple division function my_div:

fn my_div(dividend: usize, divisor: usize) -> usize {
  dividend / divisor
}

With the contract specification attributes we can specify the behavior of this function declaratively. The requires attribute allows us to declare constraints on what constitutes valid inputs to our function. In this case we would want to disallow a divisor that is 0.

#[requires(divisor != 0)]

This is called a precondition, because it is enforced before (pre-) the function call. As you can see attribute has access to the functions arguments. The condition itself is just regular Rust code. You can use any Rust code, including calling functions and methods. However you may not perform I/O (like println!) or mutate memory (like Vec::push).

The ensures attribute on the other hand lets us describe the output value in terms of the inputs. You may be as (im)precise as you like in the ensures clause, depending on your needs. One approximation of the result of division for instance could be this:

#[ensures(|result : &usize| *result <= dividend)]

This is called a postcondition and it also has access to the arguments and is expressed in regular Rust code. The same restrictions apply as did for requires. In addition to the postcondition is expressed as a closure where the value returned from the function is passed to this closure by reference.

You may combine as many requires and ensures attributes on a single function as you please. They all get enforced (as if their conditions were &&ed together) and the order does not matter. In our example putting them together looks like this:

use kani::{requires, ensures};

#[requires(divisor != 0)]
#[ensures(|result : &usize| *result <= dividend)]
fn my_div(dividend: usize, divisor: usize) -> usize {
  dividend / divisor
}

Once we are finished specifying our contract we can ask Kani to check it’s validity. For this we need to provide a proof harness that exercises the function. The harness is created like any other, e.g. as a test-like function with inputs and using kani::any to create arbitrary values. However we do not need to add any assertions or assumptions about the inputs, Kani will use the pre- and postconditions we have specified for that and we use the proof_for_contract attribute instead of proof and provide it with the path to the function we want to check.

#[kani::proof_for_contract(my_div)]
fn my_div_harness() {
    my_div(kani::any(), kani::any());
}

The harness is checked like any other by running cargo kani and can be specifically selected with --harness my_div_harness.

Once we have verified that our contract holds, we can use perhaps it’s coolest feature: verified stubbing. This allows us to use the conditions of the contract instead of it’s implementation. This can be very powerful for expensive implementations (involving loops for instance).

Verified stubbing is available to any harness via the stub_verified harness attribute. We must provide the attribute with the path to the function to stub, but unlike with stub we do not need to provide a function to replace with, the contract will be used automatically.

#[kani::proof]
#[kani::stub_verified(my_div)]
fn use_div() {
  let v = kani::vec::any_vec::<char, 5>();
  let some_idx = my_div(v.len() - 1, 3);
  v[some_idx];
}

In this example the contract is sufficient to prove that the element access in the last line cannot be out-of-bounds.

Specification Attributes Overview

The basic two specification attributes available for describing function behavior are requires for preconditions and ensures for postconditions. Both admit arbitrary Rust expressions as their bodies which may also reference the function arguments but must not mutate memory or perform I/O. The postcondition may additionally reference the return value of the function as the variable result.

In addition Kani provides the modifies attribute. This works a bit different in that it does not contain conditions but a comma separated sequence of expressions that evaluate to pointers. This attribute constrains to which memory locations the function is allowed to write. Each expression can contain arbitrary Rust syntax, though it may not perform side effects and it is also currently unsound if the expression can panic. For more information see the write sets section.

During verified stubbing the return value of a function with a contract is replaced by a call to kani::any. As such the return value must implement the kani::Arbitrary trait.

In Kani, function contracts are optional. As such a function with at least one specification attribute is considered to “have a contract” and any absent specification type defaults to its most general interpretation (true). All functions with not a single specification attribute are considered “not to have a contract” and are ineligible for use as the target of a proof_for_contract of stub_verified attribute.

Contract Use Attributes Overview

Contract are used both to verify function behavior and to leverage the verification result as a sound abstraction.

Verifying function behavior currently requires the designation of at least one checking harness with the proof_for_contract attribute. A harness may only have one proof_for_contract attribute and it may not also have a proof attribute.

The checking harness is expected to set up the arguments that foo should be called with and initialized any static mut globals that are reachable. All of these should be initialized to as general value as possible, usually achieved using kani::any. The harness must call e.g. foo at least once and if foo has type parameters, only one instantiation of those parameters is admissible. Violating either results in a compile error.

If any inputs have special invariants you can use kani::assume to enforce them but this may introduce unsoundness. In general all restrictions on input parameters should be part of the requires clause of the function contract.

Once the contract has been verified it may be used as a verified stub. For this the stub_verified attribute is used. stub_verified is a harness attribute, like unwind, meaning it is used on functions that are annotated with proof. It may also be used on a proof_for_contract proof.

Unlike proof_for_contract multiple stub_verified attributes are allowed on the same proof harness though they must target different functions.

Inductive Verification

Function contracts by default use inductive verification to efficiently verify recursive functions. In inductive verification a recursive function is executed once and every recursive call instead uses the contract replacement. In this way many recursive calls can be checked with a single verification pass.

The downside of inductive verification is that the return value of a contracted function must implement kani::Arbitrary. Due to restrictions to code generation in proc macros, the contract macros cannot determine reliably in all cases whether a given function with a contract is recursive. As a result it conservatively sets up inductive verification for every function and requires the kani::Arbitrary constraint for contract checks.

If you feel strongly about this issue you can join the discussion on issue #2823 to enable opt-out of inductive verification.

Write Sets

The modifies attribute is used to describe which locations in memory a function may assign to. The attribute contains a comma separated series of expressions that reference the function arguments. Syntactically any expression is permissible, though it may not perform side effects (I/O, mutation) or panic. As an example consider this super simple function:

#[kani::modifies(ptr, my_box.as_ref())]
fn a_function(ptr: &mut u32, my_box: &mut Box<u32>) {
    *ptr = 80;
    *my_box.as_mut() = 90;
}

Because the function performs an observable side-effect (setting both the value behind the pointer and the value pointed-to by the box) we need to provide a modifies attribute. Otherwise Kani will reject a contract on this function.

An expression used in a modifies clause must return a pointer to the location that you would like to allow to be modified. This can be any basic Rust pointer type (&T, &mut T, *const T or *mut T). In addition T must implement Arbitrary. This is used to assign kani::any() to the location when the function is used in a stub_verified.

History Expressions

Additionally, an ensures clause is allowed to refer to the state of the function arguments before function execution and perform simple computations on them via an old monad. Any instance of old(computation) will evaluate the computation before the function is called. It is required that this computation is effect free and closed with respect to the function arguments.

For example, the following code passes kani tests:

#[kani::modifies(a)]
#[kani::ensures(|result| old(*a).wrapping_add(1) == *a)]
#[kani::ensures(|result : &u32| old(*a).wrapping_add(1) == *result)]
fn add1(a : &mut u32) -> u32 {
    *a=a.wrapping_add(1);
    *a
}

Here, the value stored in a is precomputed and remembered after the function is called, even though the contents of a changed during the function execution.

Attribute Macros

ensures

Add a postcondition to this function.

modifies

Declaration of an explicit write-set for the annotated function.

proof_for_contract

Designates this function as a harness to check a function contract.

requires

Add a precondition to this function.

stub_verified

stub_verified(TARGET) is a harness attribute (to be used on proof or proof_for_contract function) that replaces all occurrences of TARGET reachable from this harness with a stub generated from the contract on TARGET.