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 types where we can guarantee safety. When you need nondeterministic variables of types that kani::any() cannot construct, you have two options:

  1. Implement the kani::Arbitrary trait for your type, so you can use kani::any().
  2. Just write a function.

The advantage of the first approach is that it's simple and conventional. It also means that in addition to being able to use kani::any() with your type, you can also use it with Option<MyType> (for example).

The advantage of the second approach is that you're able 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 are unable to implement a trait (like Arbitrary) on a type you're importing from another crate.

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 an enum, you can make use of a simple trick:

    impl kani::Arbitrary for Rating {
        fn any() -> Self {
            match kani::any::<u8>() {
                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.