Quickstart

Installation

Install Creusot and why3 as described in the README.

Create a project

Create a new project with this command:

cargo creusot new project-name

That command creates a directory package-name containing the basic elements of a Rust project verified with Creusot. The file src/lib.rs is initialized with an example function annotated with a contract:

// src/lib.rs
use creusot_contracts::*;

#[requires(x@ < i64::MAX@)]
#[ensures(result@ == x@ + 1)]
pub fn add_one(x: i64) -> i64 {
    x + 1
}

Compile and prove

To verify this project, run this command:

cargo creusot prove

A successful run gives us the certainty that functions defined in this package satisfy their contracts: for all arguments satisfying the preconditions (requires clauses), the result of the function will satisfy the postconditions (ensures clauses).

Prove with Why3

Finally, launch the why3 ide:

cargo creusot why3 ide

The documentation for the why3 ide can be found here.

We also recommend section 2.3 of this thesis for a brief overview of Why3 and Creusot proofs.

We plan to improve this part of the user experience, but that will have to wait until Creusot gets more stable and complete. If you'd like to help, a prototype VSCode plugin for Why3 is in development, it should make the experience much smoother when complete.

Prove with Why3find

Configure

$ cargo creusot config

The configuration is stored in why3find.json.

Prove

  1. Run the Creusot translation.

    $ cargo creusot

  2. Run the Why3find prover.

    $ cargo creusot prove

    Run the Why3find prover on specific files:

    $ cargo creusot prove verif/[COMA_FILES]

  3. Launch Why3 IDE on unproved goals (this will only open one file even if there are many listed with unproved goals).

    $ cargo creusot prove -i
$ cargo creusot prove -i verif/[COMA_FILES]

Tutorial

This tutorial is an introduction to deductive verification with Creusot. After introducing basic concepts, we will walk through the steps to verify a function with Creusot.

No prior knowledge about formal methods is required to follow this tutorial. Basic familiarity with Rust should be enough to get started with Creusot.

Creusot

Follow the README to install Why3 and Creusot.

Setup

Create a new project with this command:

cargo creusot new creusot-tutorial

This generates a directory creusot-tutorial containing the following files:

Cargo.toml
rust-toolchain
why3find.json
src/lib.rs

The first three files contain package-level configuration settings. You may already be familiar with Cargo.toml and rust-toolchain, generic files for Rust projects. The file why3find.json is used by a verification tool invoked by Creusot. We will leave these files alone for this tutorial.

The last file, src/lib.rs, is what we will be editing in this tutorial.

My first contract

Open src/lib.rs. It contains an example function with a contract:

use creusot_contracts::*;

#[requires(x@ < i64::MAX@)]
#[ensures(result@ == x@ + 1)]
pub fn add_one(x: i64) -> i64 {
    x + 1
}

In Creusot, contracts are how we specify the expected behavior of functions. A contract contains two kinds of assertions: preconditions, or "required clauses", describe the values of arguments that the function accepts; postconditions, or "ensured clauses", describe the result value that the function returns.

In this first example, there is one precondition (requires) and one postcondition (ensures). This contract can be read as follows: if the argument x is smaller than i64::MAX, then the value of add_one(x) will be equal to x@ + 1.

More generally, a function satisfies its contract when, for any input arguments that satisfy the preconditions (requires), the result of the function satisfies the postcondition (ensures).

It is not a very exciting contract, since it just replicates the body of the function x + 1. But note that x@ + 1 is not exactly the same expression. The @ suffix is Creusot's view operator, which maps a Rust value to a mathematical value. If x has type i64, then x@ has type Int, as the type of mathematical integers (..., -2, -1, 0, 1, 2, ...). The key difference is that mathematical integers are unbounded: their arithmetic operations do not overflow. They are more intuitive and better behaved than operations on machine integer. For example, all x: Int satisfy x < x + 1 whereas this cannot be true for Rust's machine integers because they are finite.

The type Int is one of several built-in types of common mathematical objects defined by Creusot; others include sequences and mappings (mathematical functions). On the one hand, mathematical objects like Int cannot be manipulated by Rust programs, they can only be used in contracts. On the other hand, values that exist in Rust programs such as machine integers (i64, etc.) are not as easy to manipulate in the logical world of contracts, so we use the view operator @ to transform them into something more intuitive.

The contract of add_one specifies the result slightly indirectly: its view as an unbounded integer, denoted by result@, must be equal to x@ + 1. Note that arithmetic operations are only defined on Int in the logical world of contracts.

Verifying the contract

cargo creusot prove

First, the Rust code is compiled to Coma, an intermediate verification language in the Why3 platform. Second, Why3 verifies the compiled program by generating verification conditions and sending them as queries to SMT solvers. When all verification conditions have been proved, that amounts to proving that functions defined in our crate satisfy their contracts.

My second contract

Here is a more involved example: given a non-negative integer n, compute the sum of all integers between 0 and n included. We can do this simply by iterating through each integer up to n. This is the function to verify.

pub fn sum_up_to(n: u64) -> u64 {
    let mut sum = 0;
    let mut i = 0;
    while i < n {
        i += 1;
        sum += i;
    }
    sum
}

Although a for loop would be idiomatic, that also adds some complications to the verification process. For the sake of simplicity, we start with a while loop, and switch to a for loop at the end.

As a sanity check, we can write unit tests:

#[test]
pub fn test_sum_up_to() {
    // 1 + 2 + 3 + 4 = 10
    assert_eq!(sum_up_to(4), 10);
}

Run with

cargo test

Whereas unit tests let us check the output associated with specific inputs of a function, contracts let us specify the output for all possible inputs. Naturally, we can't exhaustively list input-output pairs. Instead, we describe the relation between inputs and outputs as properties, logical formulas that are true about the inputs and outputs of a function.

Contract

The result of this sum is also known as the triangular numbers, with a well-known formula: n * (n + 1) / 2. This provides a nice and concise specification for sum_up_to.

Write an #[ensures(...)] clause to give a postcondition to sum_up_to using the formula for triangular numbers.

Added postcondition 
#[ensures(result@ == n@ * (n@ + 1) / 2)]
pub fn sum_up_to(n: u64) -> u64 {
    // ...
}

Run cargo creusot to make sure that the postcondition is well-formed. Of course, cargo creusot prove will fail. The contract is still too naive at this point.

What if the sum overflows? Feel free to try different approaches to handle this problem. Here is a non-exhaustive list of possibilities.

Add a simple bound on the input as a precondition 
#[requires(n@ < 1000)]
#[ensures(result@ == n@ * (n@ + 1) / 2)]
pub fn sum_up_to(n: u64) -> u64 {
    // ...
}
Add a more precise upper bound as a precondition 
#[requires(n@ * (n@ + 1) / 2 <= u64::MAX@)]
#[ensures(result@ == n@ * (n@ + 1) / 2)]
pub fn sum_up_to(n: u64) -> u64 {
    // ...
}
Allow overflows and adjust the postcondition accordingly 
#[ensures(result@ == (n@ * (n@ + 1) / 2) % (u64::MAX + 1))]
pub fn sum_up_to(n: u64) -> u64 {
    // ...
}
Change the result type to be big enough 
#[ensures(result@ == n@ * (n@ + 1) / 2)]
pub fn sum_up_to(n: u64) -> u128 {
    // ...
}

At this point, you may have a contract that is satisfied by the function, but cargo creusot prove still can't verify it. This function contains a loop, and loops must be annotated with loop invariants: assertions which must be true at every iteration of the loop.

Loop invariants

A loop invariant looks like this:

    #[invariant(i@ <= n@)]
    while i < n {
        i += 1;
        sum += i;
    }

At every step, i is less than or equal to n. In particular, it is true when we enter the loop (when i = 0), inside the loop body it must have been that i < n, which gives us i+1 <= n, with i+1 as the next value of i, and when we exit, the loop condition i < n is false, which combined with the invariant i@ <= n@ tells us that i = n when the function returns. We could have written this invariant as i <= n, without the @.

Inspecting proofs with Why3 IDE

The invariant is still incomplete. To investigate what's missing, we can inspect proofs in progress with Why3 IDE. The command cargo creusot prove with the -i option launches Why3 IDE, showing the proof state for an as yet unverified function.

cargo creusot prove -i

If there are many functions to verify, we can pick a specific one on the command line by naming the Coma file it was compiled to. Coma files are generated in the verif/ directory, and their path consists of the crate name (creusot_tutorial_rlib for the library creusot-tutorial) followed by the fully qualified function name (creusot_tutorial::sum_up_to becomes creusot_tutorial/M_sum_up_to.coma).

cargo creusot prove -i verif/creusot_tutorial_rlib/creusot_tutorial/M_sum_up_to.coma

Why3 IDE is a GUI that looks like this:

Screenshot of Why3 IDE window

It's a three-pane window. The left panel displays the tree of goals to prove. The top right panel displays the proof context, which consists of relevant source files and a special Task tab listing available hypotheses and the goal formula. The bottom right panel contains error messages and other logs.

In the left panel, the status of every tree node is shown as an icon in the leftmost column. Goals with complete proofs have green checkmarks, unproved goals have blue question marks. Currently, the bottom of the tree consists of five subgoals labeled [loop invariant], [sum_up_to ensures], [integer overflow] twice, and [loop invariant] again.

To verify that a function satisfies its contract, Why3 generates verification conditions which represent properties that must hold at certain points in the program:

  1. Starting from the top of the function sum_up_to, we must check that the loop invariant holds when we enter the loop, that corresponds to the first [loop invariant] goal.

  2. Inside the loop, we show that any iteration of the loop body preserves the loop invariant: we start with arbitrary values of i and sum assuming that the loop invariant holds and that the condition i < n is true. Checking that i += 1 does not overflow corresponds to the first [integer overflow] goal. Checking that sum += i does not overflow corresponds to the second [integer overflow] goal.

  3. At the end of the loop body the invariant must hold again, corresponding to the last [loop invariant] goal.

Finally, at the loop exit, we assume that the loop invariant holds and that the condition i < n is false, and prove that the returned value satisfies the postcondition (ensures clause), which corresponds to the [sum_up_to ensures] goal. It may seem surprising that the goal [sum_up_to ensures] appears first even though it corresponds to the end of the function; this is due to internal details of compiling the program to a control-flow graph and generating verification conditions by traversing the control-flow graph in a somewhat arbitrary order.

One way to make sense of the goals is to look at the source spans they contain. In the left panel, click on the goal labeled [sum_up_to ensures]. That opens a tab lib.rs on the top right panel; click on it.

Screenshot of Why3 IDE window, focused on ensures goal

We see a view of the Rust code we are trying to verify, with highlighted spans relevant to the goal we selected. What we are trying to prove is highlighted in yellow: the goal [sum_up_to ensures], as its name indicates, is trying to prove that the ensures clause holds when the function returns. Hypotheses and various bits of code that the goal depends on are highlighted in green: the requires clause and the loop invariant are hypotheses.

Similarly, you can inspect the two [loop invariant] goals. Both will highlight the invariant i <= n in yellow, but there will be a difference in the surrounding spans: one goal will highlight the 0 from the initialization of i, indicating that the goal comes from entering the loop, whereas the other goal will highlight the 1 in the increment i += 1, indicating that the goal comes from checking that the loop body maintains the loop invariant.

It is easy to prove that the addition in i += 1 will not overflow, because the loop condition i < n is true. However we cannot deduce that the addition in sum += i will not overflow yet, because we know nothing about sum in the loop invariant. For that same reason, there is also no way to prove the postcondition ([sum_up_to ensures]).

Complete the loop invariant

Complete the invariant. Below we extended the invariant with a placeholder for your solution. Intuitively, the invariant should reflect the idea that at every step, sum is the sum of numbers from 0 to i included.

    #[invariant(i@ <= n@)]
    #[invariant(true /* YOUR INVARIANT HERE */)]
    while i < n {
        i += 1;
        sum += i;
    }
Completed invariant 
    #[invariant(i@ <= n@)]
    #[invariant(sum@ == i@ * (i@ + 1) / 2)]
    while i < n {
        i += 1;
        sum += i;
    }

With that, cargo creusot prove succeeds. We have proved that the function sum_up_to satisfies its contract.

Complete sum_up_to function with all annotations 
#[requires(n@ * (n@ + 1) / 2 <= u64::MAX@)]
#[ensures(result@ == n@ * (n@ + 1) / 2)]
pub fn sum_up_to(n: u64) -> u64 {
    let mut sum = 0;
    let mut i = 0;
    #[invariant(i@ <= n@)]
    #[invariant(sum@ == i@ * (i@ + 1) / 2)]
    while i < n {
        i += 1;
        sum += i;
    }
    sum
}

Use a for loop

The while loop above can be replaced with a more idiomatic for loop.

    for i in 1..=n {
        sum += i;
    }

Verifying a for loop is more complicated because we must reason about iterators. Another challenge is that the invariant cannot talk about the next value (i): there might not be a next value.

Creusot defines a special variable, produced, which contains the sequence of elements previously produced by the iterator of a for loop. Using that variable, we can restate the invariant about sum:

    #[invariant(sum@ == produced.len() * (produced.len() + 1) / 2)]
    for i in 1..=n {
        sum += i;
    }

Indeed, produced.len() is exactly the number of past iterations.

We no longer need the other clause of the invariant, i <= n, first because i isn't even in scope in the invariant, and also because that fact will be deduced automatically from the postcondition of next for the iterator 1..=n, which is where i comes from.

We are almost done. In principle, that invariant should be all we need to complete the proof. But the solvers can't figure it out for some reason. It may be that solvers have trouble with division. We can tweak the invariant to avoid relying on division, and the proof goes through.

    #[invariant(sum@ * 2 == produced.len() * (produced.len() + 1))]
    for i in 1..=n {
        sum += i;
    }

This kind of wrinkle is par for the course in SMT-based tools such as Creusot.

Complete sum_up_to function with all annotations (for loop version) 
#[requires(n@ * (n@ + 1) / 2 <= u64::MAX@)]
#[ensures(result@ == n@ * (n@ + 1) / 2)]
pub fn sum_up_to(n: u64) -> u64 {
    let mut sum = 0;
    #[invariant(sum@ * 2 == produced.len() * (produced.len() + 1))]
    for i in 1..=n {
        sum += i;
    }
    sum
}

Conclusion

In this tutorial, we've got a glimpse of the workflow of verifying a Rust program in Creusot.

We have only scratched the surface. Creusot offers many more features for verifying Rust code at large. You can read about them in the rest of this user guide.

Basic concepts

Every Creusot macro will erase themselves when compiled normally: they only exist when using cargo creusot.

If you need to have Creusot-only code, you can use the #[cfg(creusot)] attribute.

Note that you must explicitly use the creusot_contracts crate in your code (which should be the case once you actually prove things, but not necessarily when you initially set up a project), such as with the line:

use creusot_contracts::*;

or you will get a compilation error complaining that the creusot_contracts crate is not loaded.

requires and ensure

Most of what you will be writing with creusot will be requires and ensures clauses. That is: preconditions and postconditions.

Together, those form the contract of a function. This is in essence the "logical signature" of your function: when analyzing a function, only the contract of other functions is visible.

Preconditions with requires

A precondition is an assertion that must hold when entering the function. For example, the following function accesses a slice at index 0:

fn head(v: &[i32]) -> i32 {
    v[0]
}

So we must require that the slice has at least one element:

#[requires(v@.len() >= 1)]
fn head(v: &[i32]) -> i32 {
    v[0]
}

Note the view (@) operator: it is needed to convert the Rust type &[i32] to a logical type Seq<i32>. Else, we could not call [T]::len, which is a program function (and not a logical one).

To learn more, see the chapter on Pearlite and Views.

Postconditions with ensures

A postcondition is an assertions that is proven true at the end of the function. The return value of the function can be accessed via the result keyword.

In the case of the example above, we want to assert that the returned integer is the first of the slice:

#[requires(v@.len() >= 1)]
#[ensures(v@[0] == result)]
fn head(v: &[i32]) -> i32 {
    v[0]
}

Note that we:

  • use the @ operator on the slice to get a Seq<i32>
  • we can then index this Seq<i32> to get a i32.

Invariants

When writing a loop (be it for, while or loop), you will generally need to specify an invariant, that is an assertion that stays true for the duration of the loop. For example, the following program:

#[ensures(result == n)]
fn loop_add(n: u64) -> u64 {
    let mut total = 0;
    while total < n {
        total += 1;
    }
    total
}

Needs an invariant: even though its proof seems obvious to us, it is not for Creusot. What Creusot knows is:

  • Any variable not referenced in the loop is unchanged at the end (here this is obvious because n is immutable, but it might be relevant in a more complicated program).
  • At the end of the loop, the loop condition is false: here total >= n.

We still need to know that total <= n to get result == n:

#[ensures(result == n)]
fn loop_add(n: u64) -> u64 {
    let mut total = 0;
    #[invariant(total <= n)]
    while total < n {
        total += 1;
    }
    total
}

This is now provable !

Like requires and ensures, invariant must contain a pearlite expression returning a boolean.

Verification conditions

An invariant generates two verification conditions in Why3:

  • First, that the invariants holds before the loop (initialization).
  • Second, that if the invariant holds at the beginning of a loop iteration, then it holds at the end of it.

Compiling with rustc

Make sure that functions that contain #[invariant(...)] attributes also have an #[ensures(...)] or #[requires(...)] attribute. You can always add #[ensures(true)] as a trivial contract.

That enables compilation (cargo build) with a stable Rust compiler, preventing the following error:

error[E0658]: attributes on expressions are experimental

Indeed, the #[invariant(...)] attribute on loops is only allowed by unstable features (stmt_expr_attributes, proc_macro_hygiene). For compatibility with stable Rust, the requires and ensures macros remove #[invariant(...)] attributes during normal compilation.

Variants

A variant clause can be attached either to a function like ensures, or requires or to a loop like invariant, it should contain a strictly decreasing expression which can prove the termination of the item it is attached to.

proof_assert!

At any point in the code, you may want to insert an arbitrary verification condition. This can be useful:

  • For debugging, to ensure that a property indeed holds at a certain point of the program.
  • To help the provers in specific cases.

To do this, Creusot gives you the proof_assert! macro:

fn f() {
    // ...
    let x = 1;
    let y = 2;
    proof_assert!(x@ + y@ == 3);
    // ...
}

proof_assert must contain a pearlite expression returning a boolean.

Trusted

The trusted marker lets Creusot trust the implementation and specs. More specifically, you can put #[trusted] on a function like the following:

#[trusted]
#[ensures(result == 42u32)]
fn the_answer() -> u32 {
    trusted_super_oracle("the answer to life, the universe and everything")
}

TODO: trusted traits

Representation of types

Creusot translates Rust code to Why3. But Rust types don't always exists in Why3, and would not have the same semantics: thus we need to map each Rust type to a Why3 type.

Base types

Most type have a very simple interpretation in Why3:

  • The interpretation for a scalar type (i32, bool, f64, ...) is itself.

  • The interpretation of [T] is Seq<T>, the type of sequences.

  • The interpretation of &T is the interpretation of T.

    Creusot is able to assume that T and &T behave the same, because of the "shared xor mutable" rule of Rust: we won't be able to change the value (interior mutability is handled by defining a special model for e.g. Cell<T>), so we may as well be manipulating an exact copy of the value.

  • The interpretation of Box<T> is the interpretation of T.

    This is because a Box uniquely own its content: it really acts exactly the same as T.

  • Structures and enums are interpreted by products and sum types.

  • The interpretation of &mut T is a bit more complicated: see the next section.

Mutable borrows

In Creusot, mutable borrows are handled via prophecies. A mutable borrow &mut T contains:

  • The current value (of type T) written in the borrow.
  • The last value written in the borrow, called the prophecy.

This works in the underlying logic by performing two key steps:

  • When the borrow is created, the prophecy is given a special any value. We don't know it yet, we will trust the logic solvers to find its actual value based on later operations.
  • When dropping the borrow, Creusot adds the assumption current == prophecy. We call that resolving the prophecy.

Final reborrows

The above model is incomplete: in order to preserve soundness (see the Why is this needed ? section), we need to add a third field to the model of mutable borrows, which we call the id.

Each new mutable borrow gets a unique id, including reborrows. However, this is too restrictive: with this, the identity function cannot have its obvious spec (#[ensures(result == input)]), because a reborrow happens right before returning.

To fix this, we introduce final reborrows:

A reborrow is considered final if the prophecy of the original borrow depends only on the reborrow. In that case, the reborrow id can be inherited:

  • If this is a reborrow of the same place (e.g. let y = &mut *x), the new id is the same.
  • Else (e.g. let y = &mut x.field), the new id is deterministically derived from the old.

Examples

In most simple cases, the reborrow is final:

let mut i = 0;
let borrow = &mut i;
let reborrow = &mut *borrow;
// Don't use `borrow` afterward
proof_assert!(reborrow == borrow);

#[ensures(result == x)]
fn identity<T>(x: &mut T) -> &mut T {
    x
}

It even handles reborrowing of fields:

let mut pair = (1, 2);
let mut borrow = &mut pair;
let borrow_0 = &mut borrow.0;
proof_assert!(borrow_0 == &mut borrow.0);

However, this is not the case if the original borrow is used after the reborrow:

let mut i = 0;
let borrow = &mut i;
let reborrow = &mut *borrow;
*borrow = 1;
proof_assert!(borrow == reborrow); // unprovable
                                   // Here the prophecy of `borrow` is `1`,
                                   // which is a value completely unrelated to the reborrow.

Or if there is an indirection based on a runtime value:

let mut list = creusot_contracts::vec![1, 2];
let borrow: &mut [i32] = &mut list;
let borrow_0 = &mut borrow[0];
proof_assert!(borrow_0 == &mut borrow[0]); // unprovable

Why is this needed ?

In essence, to prevent the following unsound code:

pub fn unsound() {
    let mut x: Snapshot<bool> = snapshot! { true };
    let xm: &mut Snapshot<bool> = &mut x;
    let b: &mut Snapshot<bool> = &mut *xm;
    let bg: Snapshot<&mut Snapshot<bool>> = snapshot! { b };
    proof_assert! { ***bg == true && *^*bg == true };
    let evil: &mut Snapshot<bool> = &mut *xm;
    proof_assert! { (evil == *bg) == (*^evil == true) };
    *evil = snapshot! { if evil == *bg { false } else { true } };
    proof_assert! { **evil == !*^evil };
    proof_assert! { **evil == !**evil };
}

If borrows are only a pair of current value/prophecy, the above code can be proven, and in particular it proves **evil == !**evil, a false assertion.

Pearlite

Pearlite is the language used in:

  • contracts (ensures, requires, invariant, variant)
  • proof_assert!
  • the pearlite! macro

It can be seen as a pure, immutable fragment of Rust which has access to a few additional logical operations and connectives. In practice you have:

  • Base Rust expressions: matching, function calls, let bindings, binary and unary operators, tuples, structs and enums, projections, primitive casts, and dereferencing
  • Logical Expressions: quantifiers (forall and exists), logical implication ==>, logical equality a == b, labels
  • Rust specific logical expressions: access to the final value of a mutable reference ^, access to the view of an object @

Logical implication

Since => is already a used token in Rust, we use ==> to mean implication:

proof_assert!(true ==> true);
proof_assert!(false ==> true);
proof_assert!(false ==> false);
// proof_assert!(true ==> false); // incorrect

Quantifiers

The logical quantifiers ∀ and ∃ are written forall and exists in Pearlite:

#[requires(forall<i: Int> i >= 0 && i < list@.len() ==> list@[i] == 0)]
fn requires_all_zeros(list: &[i32]) {
    // ...
}

Logic functions

We provide two new attributes on Rust functions: logic and predicate.

Marked #[logic] or #[predicate], a function can be used in specs and other logical conditions (requires/ensures and invariant). They can use ghost functions. The two attributes have the following difference:

  • A logic function can freely have logical, non-executable operations, such as quantifiers, logic equalities, etc. Instead, this function can't be called in normal Rust code (the function body of a logic function is replaced with a panic). You can use pearlite syntax for any part in the logic function by marking that part with the pearlite! { ... } macro.
  • A predicate is a logical function which returns a proposition (in practice, returns a boolean value).

Recursion

When you write recursive ghost, logic or predicate functions, you have to show that the function terminates. For that, you can add #[variant(EXPR)] attribute, which says that the value of the expression EXPR strictly decreases (in a known well-founded order) at each recursive call. The type of EXPR should implement the WellFounded trait.

Prophetic functions

As seen in the chapter on mutable borrow, a mutable borrow contains a prophetic value, whose value depends on future execution. In order to preserve the soundness of the logic, #[logic] functions are not allowed to observe that value: that is, they cannot call the prophetic ^ operator.

If you really need a logic function to use that operator, you need to mark it with #[logic(prophetic)]/#[predicate(prophetic)] instead. In exchange, this function cannot be called from ghost code (unimplemented right now).

A normal #[logic] function cannot call a #[logic(prophetic)] function.

Examples

Basic example:

#[logic]
fn logic_add(x: Int, y: Int) -> Int {
    x + y
}

#[requires(x < i32::MAX)]
#[ensures(result@ == logic_add(x@, 1))]
pub fn add_one(x: i32) -> i32 {
    x + 1
}

Pearlite block:

#[predicate]
fn all_ones(s: Seq<i32>) -> bool {
    pearlite! {
        forall<i: Int> i >= 0 && i < s.len() ==> s[i]@ == 1
    }
}

#[ensures(all_ones(result@))]
#[ensures(result@.len() == n@)]
pub fn make_ones(n: usize) -> Vec<i32> {
    creusot_contracts::vec![1; n]
}

Recursion:

TODO

Prophetic:

TODO

Views as models of types

It is generally convenient to map a Rust type to its logical model. This logical model is the type that specifications and clients then use to describe values of this type in the logic.

In Creusot, this is provide using the creusot_contracts::View trait, providing a view method mapping the type to a ViewTy associated type for the model.

Specifications can then use the @ operator as a syntactic sugar for .view() on a type that implements View.

For example, the following gives a spooky data type MyPair<T, U> a nice pair model.

struct MyPair<T, U> {
  fst: T, 
  snd: U,
}

impl<T, U> View for MyPair<T, U> {
    type ViewTy = (T, U);

    #[logic]
    #[open]
    fn view(self) -> Self::ViewTy {
        (self.fst, self.snd)
    }
}

#[ensures(result@ == (a, b))]
fn my_pair<T, U>(a: T, b: U) -> MyPair<T, U> {
    MyPair(a, b)
}

Termination

By default, Creusot does not require that program functions terminate, which may lead to surprising situations:

#[ensures(result@ == 42)]
fn nonsense() -> u64 {
    while true {}
    1
}

This can be avoided at the cost of more complicated verification, by adding the terminates attribute to a function:

#[terminates]
#[ensures(result@ == 42)]
fn nonsense() -> u64 { // Fails to compile now !
    while true {}
    1
}

A function with the terminates attribute cannot:

  • Call a non-terminates function.

  • Use a loop construct (for, while, loop). This restriction may be lifted in the future.

  • Use simple recursion without the variant attribute.

    This means that this function will not be accepted:

    #[terminates]
fn f(x: u32) -> bool {
    if x == 0 { false } else { f(x - 1) }
}

    But this one will (the variant will be checked by why3):

    #[terminates]
#[variant(x)]
fn f(x: u32) -> bool {
    if x == 0 { false } else { f(x - 1) }
}

  • Use mutual recursion, like in the following example:

    #[terminates]
fn f() { g() } // Error: mutually recursive functions

#[terminates]
fn g() { f() }

Mutual recursion through traits

Traits complicate the recursion analysis. Indeed, if we have a function like

trait Tr {
    fn f();
}
fn g<T: Tr>() {
    <T as Tr>::f();
}

It isn't possible to know ahead of time which instance of f will be called.

Thus, Creusot makes the decision to check recursion at instantiation time: the above example compiles, but

trait Tr {
    fn f();
}
fn g<T: Tr>() {
    <T as Tr>::f();
}

impl Tr for i32 {
    fn f() {
        g::<i32>();
    }
}

does not, because we know that g::<i32> calls <i32 as Tr>::f(), causing a cycle.

Dependencies

The recursion check explores the body of the functions in the current crate, but it cannot do so with the dependencies, whose function bodies are not visible.

Thus, it assumes two things:

  1. The recursion check passed on the dependencies of the current crate.
  2. If a function in a dependency has a trait bound, the recursion check pessimistically assumes that all the functions of the trait are called.

Example:

// dependency/src/lib.rs
trait Tr {
    fn f();
}
fn g<T: Tr>() {
    // It does not matter if `<T as Tr>::f` is called or not, since we cannot see it
}

// lib.rs
impl Tr for i32 {
    fn f() {
        g::<i32>(); // Error !
    }
}

Snapshots

A useful tool to have in proofs is the Snapshot<T> type (creusot_contracts::Snapshot). Snapshot<T> is:

  • a zero-sized-type
  • created with the snapshot! macro
  • whose model is the model of T
  • that can be dereferenced in a logic context.

Example

They can be useful if you need a way to remember a previous value, but only for the proof:

#[ensures(array@.permutation_of((^array)@))]
#[ensures(sorted((^array)@))]
pub fn insertion_sort(array: &mut [i32]) {
    let original = snapshot!(*array); // remember the original value
    let n = array.len();
    #[invariant(original@.permutation_of(array@))]
    #[invariant(...)]
    for i in 1..n {
        let mut j = i;
        #[invariant(original@.permutation_of(array@))]
        #[invariant(...)]
        while j > 0 {
            if array[j - 1] > array[j] {
                array.swap(j - 1, j);
            } else {
                break;
            }
            j -= 1;
        }
    }

    proof_assert!(sorted_range(array@, 0, array@.len()));
}

#[logic]
fn permutation_of(s1: Seq<i32>, s2: Seq<i32>) -> bool {
    // ...
}
#[logic]
fn is_sorted(s: Seq<i32>) -> bool {
    // ...
}

Ghost code

Sometimes, you may need code that will be used only in the proofs/specification, that yet still obeys the typing rules of Rust. In this case, snapshots are not enough, since they don't have lifetimes or ownership.

This is why there exists a separate mechanism: ghost code.

ghost! and Ghost<T> are the counterparts of snapshot! and Snapshot<T>.

ghost! blocks

At any point in the code, you may open a ghost! block:

ghost! {
    // code here
}

In ghost! block, you may write any kind of Rust code, with the following restrictions :

  • ghost code must terminate (see termination for details)
  • all functions called must have the #[pure] attribute
  • When reading an outer variable, the variable must be of type Ghost<T>, or implement Copy
  • When writing an outer variable, the variable must be of type Ghost<T> or Snapshot<T>
  • The output of the ghost! block will automatically be wrapped in Ghost::new

Those restriction exists to ensure that ghost code is erasable: its presence or absence does not affect the semantics of the actual running program, only the proofs.

Ghost<T>

The Ghost<T> type is the type of "ghost data". In Creusot, it acts like a Box<T>, while in normal running code, it is an empty type. It has the same View as the underlying type, meaning you can use the @ operator directly.

The only restriction of Ghost<T> is that it may not be dereferenced nor created in non-ghost code.

Examples

  • Creating and modifying a ghost variable:
let mut g = ghost!(50);
ghost! {
    *g *= 2;
};
proof_assert!(g@ == 100);
  • Calling a function in ghost code:
#[pure]
#[requires(*g < i32::MAX)]
#[ensures((^g)@ == (*g)@ + 1)]
fn add_one(g: &mut i32) {
    *g += 1;
}

let mut g = ghost!(41);
ghost! {
    add_one(&mut *g);
};
proof_assert!(g@ == 42);
  • Using a ghost access token:
struct Token;

struct Data {
    // ...
}

impl Data {
    fn new() -> (Data, Ghost<Token>) { /* */ }
    fn read(&self, token: &Ghost<Token>) -> T { /* */ }
    fn write(&self, t: T, token: &mut Ghost<Token>) { /* */ }
}

Ghost structures

Using imperative data structures in ghost code

Usual imperative structures like Vec, HashMap or HashSet cannot be used in ghost code. To be precise, you may notice that functions like Vec::push are not marked with the #[pure] attribute, and so they cannot be called in ghost code.

This is because this function (and other like it) allocate memory, which on the actual machine, is finite. This currently translates to a possible inconsistency when using Vec in ghost code:

use creusot_contracts::{proof_assert, ghost};
ghost! {
    let mut v = Vec::new();
    for _ in 0..=usize::MAX as u128 + 1 {
        v.push(0);
    }
    proof_assert!(v@.len() <= usize::MAX@); // by definition
    proof_assert!(v@.len() > usize::MAX@);  // uh-oh
}

This case might be forbidden in the future by adding a stronger precondition to Vec::push, but the point still stands: the capacity of a ghost vector should be infinite.

Ghost structures

As such, ghost code uses the mathematical structures Seq, FMap and FSet, and adds program functions onto them.

The above snippet becomes:

use creusot_contracts::{proof_assert, ghost, Int, logic::Seq};
ghost! {
    let mut s: Seq<Int> = Seq::new();
    for _ in 0..=usize::MAX as u128 + 1 {
        s.push_ghost(0);
    }
    // proof_assert!(s.len() <= usize::MAX@); // fails
    proof_assert!(s.len() > usize::MAX@);
}

A few things to note:

  • Seq, FMap and FSet are the counterparts for Vec, HashMap and HashSet respectively. They all live in the logic module.
  • Since s in directly the logical type Seq, we don't need the view operator @.
  • To avoid name clashes, these additional "ghost" functions are almost all suffixed with _ghost. See the documentation for each type to know the available methods, ghost and logical.

Int in ghost

You can manipulate values of type Int in ghost code, by using the int suffix on integer literals:

ghost! {
    let my_int = 42int;
};

Right now you cannot do much except pass it around: operations like + or * are only supported in pearlite.

Type Invariants

Overview

Defining a type invariant allows you to constrain a data type's set of valid values with a logical predicate that all values must satisfy. During verification, Creusot enforces that all type invariants are preserved across functions. Inside a function, values subject to type invariants may temporarily break their invariants as long as each value's invariant is restored before the value can be observed by another function.

Type invariants were added to Creusot as part of a Master's thesis available here.

Defining Type Invariants

To attach an invariant to a type, you implement the Invariant trait provided by Creusot. Here is an example:

struct SumTo10 {
    a: i32,
    b: i32,
}

// The type invariant constrains the set of valid `SumTo10`s to
// only allow values where the sum of both fields is equal to 10.
impl Invariant for SumTo10 {
    #[predicate]
    fn invariant(self) -> bool {
        pearlite! {
            self.a@ + self.b@ == 10
        }
    }
}

Enforcement of Type Invariants

Creusot enforces type invariants on function boundaries by generating additional pre- and postconditions based on the types of a function's arguments and return value. The type invariants of a function’s arguments are treated as additional preconditions and a type invariant of the return value corresponds to an extra postcondition. Here is an example:

// `inv` generically refers to the invariant of some value
#[requires(inv(x))] // generated by Creusot
#[ensures(inv(result))] // generated by Creusot
fn foo(x: SumTo10) -> SumTo10 {
    x
}

These generated pre- and postconditions require you to prove the invariants of any values used as arguments in function calls or returned values. Besides the proof obligations at function boundaries, you must also prove the type invariants of mutably borrowed values when the lifetimes of the created references end. When creating a mutable reference r, Creusot requires you to prove the type invariant of its current value at the end of r's lifetime, since r might have been used to break the invariant of the borrowed value. This lets Creusot assume the invariant of the final value ^r holds, simplifying the reasoning about mutable references. Here is an example:

fn swap() {
    let mut s = SumTo10 { a: 3, b: 7 }
    let r = &mut s;
    // Creusot can prophetically assume inv(^r) holds:
    proof_assert! { inv(^r) };

    let tmp = r.a;
    *r.a = r.b;
    *r.b = tmp;
    // The lifetime of r ends: We must prove inv(*r)

    proof_assert! { inv(v) }; // provable since v = ^r = *r
}

Structural Invariants

To determine the invariant of a particular type, Creusot considers both whether the user provided an explicit definition through the Invariant trait, as well as any invariants the can be derived automatically based on the type's definition. We call those automatically derived invariants structural invariants. When neither an explicit definition exists, nor a structural invariant, the type has the trivial invariant, which does not impose any constraints on the set of valid values.

Here are some examples demonstrating structural invariants of various types:

Type of xInvariant inv(x)
bool, u8, i32, ...true
&mut Fooinv(*x) && inv(^x)
&Fooinv(*x)
Box<Foo>inv(*x)
*const Foo, *mut Footrue
(Foo, Bar)inv(x.0) && inv(x.1)
struct Foo { f: Bar }inv(x.f)
enum Foo { A(Bar), B(Baz) }match x { A(y) => inv(y), B(z) => inv(z) }
Vec<Foo>inv(x[0]) && ... && inv(x[x.len()-1])

Command-line Interface

List of commands

Main commands

creusot

cargo creusot [-- [-p <CRATE>]]

Run the Creusot compiler.

Output Coma code in the verif/ directory.

Options

  • -p <CRATE>: Compile a specific crate <CRATE> in a multi-crate project.

prove

cargo creusot prove [-i] [<COMA_FILE>]

Verify contracts.

This first runs cargo creusot to be sure that the compiled code is up-to-date. Then why3find verifies the compiled Coma code: it generates verification conditions and tries to prove them.

Options

  • -i: Open the Why3 IDE on an unproved file to inspect its proof context.
  • <COMA_FILE>: Verify a specific file (corresponding to one Rust function).

doc

cargo creusot doc

Build documentation.

This is a variant of cargo doc that also renders contracts (requires and ensures), logic functions, and predicates.

clean

cargo creusot clean [--force] [--dry-run]

Remove dangling proof files.

Removing (or renaming) Rust functions also removes (or renames) its compiled Coma file. However, the Creusot compiler can't keep track of their associated proof files (proof.json, why3session.xml), which become dangling. cargo creusot will detect dangling files and print a warning to remind you to move those files if you want, otherwise you can remove them with cargo creusot clean.

Options

  • --force: Don't ask for confirmation before removing dangling files.
  • --dry-run: Only print the list of files that would be removed by cargo creusot clean.

Create package

new

cargo creusot new <NAME> [--main]

Create package named <NAME>.

Create a directory <NAME> and initialize it with starting configuration and source files.

Options

  • --main: Create main.rs for an executable crate. (By default, only a library crate lib.rs is created.)

init

cargo creusot init [<NAME>] [--main]

Create package in the current directory.

Options

  • <NAME>: Name of the package. (By default, it is the name of the directory.)
  • --main: Create main.rs for an executable crate. (By default, only a library crate lib.rs is created.)

config

cargo creusot config

Generate why3find configuration.

This is used to set up Creusot in an existing Rust package. You don't need to run this command if you used cargo creusot new or cargo creusot init.

Show configuration

setup status

cargo creusot setup status

Show the status of the Creusot installation.

Print tool locations and configuration paths.