Quickstart

Installation

Install Creusot and why3 as described in the README.

Write specifications

Create a new project, and import creusot-contracts to start writing specifications:

# Cargo.toml
[package]
name = "add_one"
version = "0.1.0"
edition = "2021"

[dependencies]
creusot-contracts = { path = "/PATH/TO/CREUSOT/creusot-contracts" }

Remark This may only work if you're using the same rust toolchain that was used to build creusot: you can copy the rust-toolchain file into the root of your project to make sure the correct toolchain is selected.

Then you can start writing specifications:

#![allow(unused)]
fn main() {
// src/lib.rs
use creusot_contracts::*;

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

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.

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:

#![allow(unused)]
fn main() {
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:

#![allow(unused)]
fn main() {
fn head(v: &[i32]) -> i32 {
    v[0]
}
}

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

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

Note the shallow model (@) 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 ShallowModel.

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:

#![allow(unused)]
fn main() {
#[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:

#![allow(unused)]
fn main() {
#[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:

#![allow(unused)]
fn main() {
#[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.

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:

#![allow(unused)]
fn main() {
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:

#![allow(unused)]
fn main() {
#[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:

#![allow(unused)]
fn main() {
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:

#![allow(unused)]
fn main() {
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:

#![allow(unused)]
fn main() {
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:

#![allow(unused)]
fn main() {
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:

#![allow(unused)]
fn main() {
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 shallow model of an object @

Logical implication

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

#![allow(unused)]
fn main() {
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:

#![allow(unused)]
fn main() {
#[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:

#![allow(unused)]
fn main() {
#[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:

#![allow(unused)]
fn main() {
#[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:

#![allow(unused)]
fn main() {
TODO
}

Prophetic:

#![allow(unused)]
fn main() {
TODO
}

Shallow model

You can implement the @ operator for your type. To do that, you just implement the creusot_contracts::ShallowModel trait specifying the associated type ShallowModelTy.

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

#![allow(unused)]
fn main() {
struct MyPair<T, U>(T, U);

impl<T, U> ShallowModel for MyPair<T, U> {
    type ShallowModelTy = (T, U);

    #[logic]
    #[open]
    fn shallow_model(self) -> Self::ShallowModelTy {
        (self.0, self.1)
    }
}

#[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:

#![allow(unused)]
fn main() {
#[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:

#![allow(unused)]
fn main() {
#[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:

#![allow(unused)]
fn main() {
#[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):

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

Use mutual recursion, like in the following example:

#![allow(unused)]
fn main() {
#[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

#![allow(unused)]
fn main() {
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

#![allow(unused)]
fn main() {
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:

The recursion check passed on the dependencies of the current crate.
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:

#![allow(unused)]
fn main() {
// 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:

#![allow(unused)]
fn main() {
#[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 GhostBox<T> are the counterparts of snapshot! and Snapshot<T>.

`ghost!` blocks

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

#![allow(unused)]
fn main() {
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 a GhostBox<T>, or implement Copy
When writing an outer variable, the variable must be a GhostBox<T>
The output of the ghost! block will automatically be wrapped in GhostBox::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.

`GhostBox<T>`

The GhostBox<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 ShallowModel as the underlying type, meaning you can use the @ operator directly.

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

Examples

Creating and modifying a ghost variable:

#![allow(unused)]
fn main() {
let mut g = ghost!(50);
ghost! {
    *g *= 2;
};
proof_assert!(g@ == 100);
}

Calling a function in ghost code:

#![allow(unused)]
fn main() {
#[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:

#![allow(unused)]
fn main() {
struct Token;

struct Data {
    // ...
}

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

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:

#![allow(unused)]
fn main() {
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:

#![allow(unused)]
fn main() {
// `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:

#![allow(unused)]
fn main() {
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 `x`	Invariant `inv(x)`
`bool, u8, i32, ...`	`true`
`&mut Foo`	`inv(*x) && inv(^x)`
`&Foo`	`inv(*x)`
`Box<Foo>`	`inv(*x)`
`const Foo, mut Foo`	`true`
`(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])`

Creusot User Guide