Nondeterministic variables

Kani is able to reason about programs and their execution paths by allowing users to create nondeterministic (also called symbolic) values using kani::any(). Kani is a "bit-precise" model checker, which means that Kani considers all the possible bit-value combinations that would be valid if assigned to a variable's memory contents. In other words, kani::any() should not produce values that are invalid for the type (which would lead to Rust undefined behavior).

Out of the box, Kani includes kani::any() implementations for most primitive and some std types. In this tutorial, we will show how to use kani::any() to create symbolic values for other types.

Safe nondeterministic variables

Let's say you're developing an inventory management tool, and you would like to start verifying properties about your API. Here is a simple example (available here):

use std::num::NonZeroU32;
use vector_map::VecMap;

pub type ProductId = u32;

pub struct Inventory {
    /// Every product in inventory must have a non-zero quantity
    pub inner: VecMap<ProductId, NonZeroU32>,
}

impl Inventory {
    pub fn update(&mut self, id: ProductId, new_quantity: NonZeroU32) {
        self.inner.insert(id, new_quantity);
    }

    pub fn get(&self, id: &ProductId) -> Option<NonZeroU32> {
        self.inner.get(id).cloned()
    }
}

Let's write a fairly simple proof harness, one that just ensures we successfully get the value we inserted with update:

    #[kani::proof]
    #[kani::unwind(3)]
    pub fn safe_update() {
        // Empty to start
        let mut inventory = Inventory { inner: VecMap::new() };

        // Create non-deterministic variables for id and quantity.
        let id: ProductId = kani::any();
        let quantity: NonZeroU32 = kani::any();
        assert!(quantity.get() != 0, "NonZeroU32 is internally a u32 but it should never be 0.");

        // Update the inventory and check the result.
        inventory.update(id, quantity);
        assert!(inventory.get(&id).unwrap() == quantity);
    }

We use kani::any() twice here:

  1. id has type ProductId which was actually just a u32, and so any value is fine.
  2. quantity, however, has type NonZeroU32. In Rust, it would be undefined behavior to have a value of 0 for this type.

We included an extra assertion that the value returned by kani::any() here was actually non-zero. If we run this, you'll notice that verification succeeds.

cargo kani --harness safe_update

kani::any() is safe Rust, and so Kani only implements it for types where type invariants are enforced. For NonZeroU32, this means we never return a 0 value. The assertion we wrote in this harness was just an extra check we added to demonstrate this fact, not an essential part of the proof.

Custom nondeterministic types

While kani::any() is the only method Kani provides to inject non-determinism into a proof harness, Kani only ships with implementations for a few std types where we can guarantee safety. When you need nondeterministic variables of types that don't have a kani::any() implementation available, you have the following options:

  1. Implement the kani::Arbitrary trait for your type, so you and downstream crates can use kani::any() with your type.
  2. Implement the bolero_generator::TypeGenerator trait. This will enable you and downstream crates to use Kani via Bolero.
  3. Write a function that builds an object from non-deterministic variables.

We recommend the first approach for most cases. The first approach is simple and conventional. This option will also enable you to use it with parameterized types, such as Option<MyType> and arrays. Kani includes a derive macro that allows you to automatically derive kani::Arbitrary for structures and enumerations as long as all its fields also implement the kani::Arbitrary trait. One downside of this approach today is that the kani crate ships with Kani, but it's not yet available on crates.io. So you need to annotate the Arbitrary implementation with a #[cfg(kani)] attribute. For the derive macro, use #[cfg_attr(kani, derive(kani::Arbitrary))].

The second approach is recommended for cases where you would also like to be able to apply fuzzing or property testing. The benefits of doing so were described in this blog post. Like kani::Arbitrary, this trait can also be used with a derive macro. One thing to be aware of is that this type allow users to generate arbitrary values that include pointers. In those cases, only the values pointed to are arbitrary, not the pointers themselves.

Finally, the last approach is recommended when you need to pass in parameters, like bounds on the size of the data structure. (Which we'll discuss more in the next section.) This approach is also necessary when you need to generate a nondeterministic variable of a type that you're importing from another crate, since Rust doesn't allow you to implement a trait defined in an external crate for a type that you don't own.

Either way, inside this function you would simply return an arbitrary value by generating arbitrary values for its components. To generate a nondeterministic struct, you would just generate nondeterministic values for each of its fields. For complex data structures like vectors or other containers, you can start with an empty one and add a (bounded) nondeterministic number of entries.

For example, for a simple enum you can just annotate it with the Arbitrary derive attribute:

#[derive(Copy, Clone)]
#[cfg_attr(kani, derive(kani::Arbitrary))]
pub enum Rating {
    One,
    Two,
    Three,
}

But if the same enum is defined in an external crate, you can use a simple trick:

    pub fn any_rating() -> Rating {
        match kani::any() {
            0 => Rating::One,
            1 => Rating::Two,
            _ => Rating::Three,
        }
    }

All we're doing here is making use of a nondeterministic integer to decide which variant of Rating to return.

NOTE: If we thought of this code as generating a random value, this function looks heavily biased. We'd overwhelmingly generate a Three because it's matching "all other integers besides 1 and 2." But Kani just see 3 meaningful possibilities, each of which is not treated any differently from each other. The "proportion" of integers does not matter.

Bounding nondeterministic variables

You can use kani::any() for [T; N] (if implemented for T) because this array type has an exact and constant size. But if you wanted a slice ([T]) up to size N, you can no longer use kani::any() for that. Likewise, there is no implementation of kani::any() for more complex data structures like Vec.

The trouble with a nondeterministic vector is that you usually need to bound the size of the vector, for the reasons we investigated in the last chapter. The kani::any() function does not have any arguments, and so cannot be given an upper bound.

This does not mean you cannot have a nondeterministic vector. It just means you have to construct one. Our example proof harness above constructs a nondeterministic Inventory of size 1, simply by starting with the empty Inventory and inserting a nondeterministic entry.

Exercise

Try writing a function to generate a (bounded) nondeterministic inventory (from the first example:)

fn any_inventory(bound: u32) -> Inventory {
   // fill in here
}

One thing you'll quickly find is that the bounds must be very small. Kani does not (yet!) scale well to nondeterministic-size data structures involving heap allocations. A proof harness like safe_update above, but starting with any_inventory(2) will probably take a couple of minutes to prove.

A hint for this exercise: you might choose two different behaviors, "size of exactly bound" or "size up to bound". Try both!

A solution can be found in exercise_solution.rs.

Summary

In this section:

  1. We saw how kani::any() will return "safe" values for each of the types Kani implements it for.
  2. We saw how to implement kani::Arbitrary or just write a function to create nondeterministic values for other types.
  3. We noted that some types cannot implement kani::any() as they need a bound on their size.
  4. We did an exercise to generate nondeterministic values of bounded size for Inventory.