Creusot is a tool to help you prove that your Rust program is correct: it is free from errors and does what you specified it should do.

In this devlog we highlight Creusot's newest features, now version 0.12.0.

What's new in Creusot?

Prove by default

The main command cargo creusot now runs the whole verification pipeline:

1. compile Rust to Coma;

2. verify the Coma code.

Previously, cargo creusot only ran step 1, and there was a separate command cargo creusot prove to run step 2. This made sense in earlier days when the verification process used to be more fiddly, but now we are finding "prove by default" to be more and more workable in our recent experience.

It is still convenient to only run these steps individually, especially step 1 which gives you the reasonably fast feedback of type checking. Hence cargo creusot also provides the options --only=coma (step 1) and --only=prove (step 2, with the risk that the verified Coma is out of date).

Improved termination checking

Many holes in the termination checker have been fixed, notably by detecting recursive trait implementations and by adding restrictions on recursive types. This section provides is a brief simplified overview; for more details, see the Creusot User Guide: Termination.

Recursive trait implementations

To determine whether a function is recursive, a good starting point is to build a call graph: a graph whose vertices are functions, and there is an edge from f to g if f contains calls to g in its body. A cycle in this graph then means that a function may call itself.

Traits complicate this story, because method calls no longer correspond to concrete functions. If a generic function f<T: Tr> calls a method <T as Tr>::method, the definition of f alone is not enough to tell us whether f might call itself, since this depends on how the method is instantiated via the resolution of the bound T: Tr.

To address this, we track additional dependencies at the call sites of generic functions. The call graph now also includes trait implementations (impl Trait for Type blocks). In the body of a function caller, when the generic function f<T: Tr> is instantiated with some type A, we add not only an edge from the caller to f, but also an edge from the caller to the trait implementation impl Tr for A, which itself depends on all of the method implementations that it contains. Hence, instantiating f<T: Tr> with A is interpreted as potentially calling any of the methods of the trait Tr for A.

This may seem like a quite coarse-grained analysis, but it is also more predictable in that the resulting edges out of caller in the call graph don't depend on the bodies of the functions it calls.

Recursive types

In Rust, the definition of recursive types must follow some rules to ensure that they have a well-defined size. In Creusot, it is crucial to impose additional restrictions on recursive types for the sake of soundness.

The classical counterexample is a type T which is defined recursively as the type of functions from itself into booleans, commonly denoted as T -> bool. In Creusot, it is written as Mapping<T, bool>, where Mapping is a built-in type provided by Creusot:

// This type spells trouble
struct T(Mapping<T, bool>);

Indeed, the mere existence of such a type leads to a contradiction. Suppose T = (T -> bool). We define the function n : T -> bool of negated self-application: take an argument x : T, apply it (as a function x : T -> bool) to itself, and negate the result, yielding !x(x). (As a lambda: n = λ(x : T). !x(x).) By evaluating the application of n to itself, we reach a contradiction:

n(n) = !n(n)  // after one reduction step

The boolean n(n) equals its own negation, which is impossible!

This is precisely Cantor's diagonal argument that no set S is in one-to-one correspondence with its powerset 2^S, aka. S -> bool.

For the curious, here is the diagonal argument written in Creusot: we define the negated self-application n, and prove false using it.

use creusot_std::prelude::*;

struct T(Mapping<T, bool>);

/// Negated self-application
/// Instead of directly writing `x(x)` as in the proof above,
/// we must write `x.0(x)` here, explicitly projecting `x` to the function it contains.
#[logic]
fn n() -> Mapping<T, bool> {
    pearlite! {
        |x: T| !x.0(x)
    }
}

#[logic]
#[ensures(false)]  // should not be provable
fn contradiction() {
    // trivially provable by definition of n
    proof_assert! { n()(T(n())) == !n()(T(n())) }
}

To fix this soundness issue, Creusot follows the lead of other proof languages with recursive types (Why3, Rocq, etc.) in imposing restrictions upon the definition of recursive types: all recursive occurrences must appear in strictly positive positions. Strictly positive roughly means "under sums and products (enum, struct) and to the right of arrows (that is the second argument of Mapping)".

In the above example, Creusot will emit an error on the definition struct T(Mapping<T, bool>) because the type T occurs as the first argument of Mapping, which is not a strictly positive position.

Allow overriding collect

Creusot provides a specification of many standard traits, including the Iterator trait, that you must prove when implementing this trait. However, the previous specification did not allow you to redefine collect, forcing you to reuse the default implementation. Redefining collect can enable better performance, for example in IndexMap.

This limitation results from Creusot's way of specifying pre-existing traits. The collect function has a FromIterator bound, but our specification of collect also expects a FromIteratorSpec bound, which as its name implies, is a trait that provides a specification for FromIterator, in the form of a postcondition for the from_iter method. What happens when you try to re-implement collect is that, while it only has a FromIterator bound from its original declaration in the Iterator trait, the specification of collect—that Creusot introduces to verify your implementation—fails to type check because of the missing FromIteratorSpec.

As long as you omit collect, you inherit from the default implementation which is axiomatized as satisfying the specification, and we don't even try to type check it.

The root of the problem is actually quite deep, and we'll spare you the details, but basically we plan to redesign how Creusot retrofits specifications onto pre-existing traits.

In the meantime, there is a shortcut that we took to deal with FromIterator and enable users to redefine collect. We now refer to the postcondition of from_iter directly in the definition of collect—as a logic method from_iter.postcondition, avoiding the need for a separate trait such as FromIteratorSpec to define that postcondition. That solution can probably be adapted to other similar cases in the standard library where specs only need to refer to pre- and postconditions of trait methods.

Lifetime logic

The concept of lifetimes is core to Rust's ownership system, combining both flexibility and memory-safety. Checking the validity of lifetimes when sharing or mutating memory is the notorious role of the borrow-checker in the Rust compiler. The borrow-checker works completely automatically, which makes it overly strict in some situations: it may reject programs that are actually safe. Rust programmers can bypass those limitations by writing unsafe code, ideally with some argument that memory safety is preserved.

We are interested in ways to turn safety arguments into formal proofs. One approach is to reason about lifetimes using more fine-grained rules than those implemented by the borrow-checker. Such rules can be found in the lifetime logic originally introduced by RustBelt to model types with interior mutability such as Cell and Mutex.

The present release includes a new API that adapts RustBelt's lifetime logic to Creusot. Lifetimes, rather than being type variables of a special kind tracked by the borrow-checker, become tokens (LifetimeToken) which are regular Rust values to be tracked by Creusot. The API then provides methods to split and join tokens, and to use borrows (FullBorrow) alongside matching lifetime tokens.

This is a complementary feature to ghost permissions—a feature previously introduced by Verus, whose adaptation to Creusot was presented earlier this year. Ghost permissions make the "ownership metadata" of raw pointers visible to the borrow-checker, and the lifetime logic provides manual but fine-grained control over the sharing of that metadata. As a starting application of the lifetime logic, we are working on a verified implementation of a spinlock.