Le marteau-pilon, forges et aciéries de Saint-Chamond, Joseph-Fortuné LAYRAUD, 1889
Creusot is a deductive verifier for Rust code. It verifies your code is safe from panics, overflows, and assertion failures. By adding annotations you can take it further and verify your code does the correct thing.
Creusot works by translating Rust code to WhyML, the verification and specification language of Why3. Users can then leverage the full power of Why3 to (semi)-automatically discharge the verification conditions!
See ARCHITECTURE.md for technical details.
If you would like to cite Creusot in academic contexts, we encourage you to use our ICFEM'22 publication.
To get an idea of what verifying a program with Creusot looks like, we encourage you to take a look at some of our test suite:
- Zeroing out a vector
- Binary search on Vectors
- Sorting a vector
- IterMut
- Normalizing If-Then-Else Expressions
More examples are found in creusot/tests/should_succeed.
- CreuSAT is a verified SAT solver written in Rust and verified with Creusot. It really pushes the tool to its limits and gives an idea of what 'use in anger' looks like.
- Another big project is in the works :)
- Set up Rust
- Install
rustup
, to get the suitable Rust toolchain
- Install
- Set up Why3 and Alt-Ergo
- Get
opam
, the package manager for OCaml - Create an opam switch with OCaml 4.14.1:
$ opam switch create creusot ocaml.4.14.1 $ eval $(opam env --switch=creusot)
- Pin
why3
tomaster
and install it:
$ opam pin -n why3 --dev-repo $ opam pin -n why3-ide --dev-repo $ opam install zarith ocamlgraph camlzip why3 why3-ide
- Pin
alt-ergo
to version 2.4.3 and install it:
$ opam pin alt-ergo 2.4.3
- Get
- Clone the creusot repo at any directory you like
- Build Creusot
- Enter the cloned directory and run:
this will build the$ cargo install --path creusot-rustc $ cargo install --path cargo-creusot
cargo-creusot
andcreusot-rustc
executables and place them in~/.cargo/bin
. - Set up Creusot
This will download additional solvers (Z3, CVC4, CVC5) and configure Why3 to use them.
$ cargo creusot setup install
See HACKING.md for information on the developer workflow for hacking on the Creusot codebase.
The recommended way for users to verify programs with Creusot is to use cargo-creusot
.
All you need to do is enter your project and run cargo creusot
!
This will generate MLCFG files in target/debug/
which can then be loaded into Why3.
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.
To add contracts to your programs you will need to use the creusot-contracts
crate by adding it as a dependency:
# Cargo.toml
[dependencies]
creusot-contracts = { path = "/path/to/creusot/creusot-contracts" }
Adding this dependency will make the contract macros available in your code. These macros will erase themselves when compiled with rustc
.
To add Creusot-only trait implementations or code, you can use cfg(creusot)
to toggle.
You must also 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.
To load your files in Why3, we recommend using the ide
script provided in the Creusot repository.
You may also copy both this script and the prelude
directory in your project to have a fully self contained proof environment.
To load your proofs in Why3, run:
REPO/ide PATH/TO/OUTPUT.mlcfg
From there standard proof strategies of Why3 work. We 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.
First, you will need to depend on the creusot-contracts
crate, add it to your Cargo.toml
and enable the contracts
feature to turn on contracts.
Currently Creusot uses 4 different kinds of contract expressions: requires
, ensures
, invariant
and variant
.
The most basic are requires
and ensures
, which can be attached to a Rust function declaration like so:
#[requires(... precondition ...)]
#[ensures(... postcondition ...)]
fn my_function(i: u32) -> bool { ... }
You can attach as many ensures
and requires
clauses as you would like, in any order.
Inside a function, you can attach invariant
clauses to loops, these are attached on top of the loop rather than inside, like:
#[invariant(... loop invariant ...)]
while ... { ... }
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.
We also have features for controlling verification.
First, 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")
}
Causing Creusot to assume the contracts are true.
By default in Creusot, integers are represented with bounds-checking. This can be tedious or difficult to prove in certain cases, so we can disable bounds checking by passing the --unbounded
flag to Creusot.
Contracts and logic functions are written in Pearlite, a specification language for Rust we are developing. Pearlite 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
andexists
), logical implication==>
, logical equalitya == b
, labels - Rust specific logical expressions: access to the final value of a mutable reference
^
, access to the model of an object@
We also 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 alogic
function is replaced with a panic). You can use pearlite syntax for any part in the logic function by marking that part with thepearlite! { ... }
macro.If you need to use the prophecy operator
^
on a mutable reference, you need to mark the function#[logic(prophetic)]
. -
A
predicate
is a logical function which returns a proposition (in practice, returns a boolean value).
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.
You can also give a custom model to your type.
To do that, you just implement the Model
trait (provided in creusot_contracts
) specifying the associated type Model
.
You give a trusted spec that defines the model (which can be accessed by @
) on primitive functions.
For example, the following gives a spooky data type MyPair<T, U>
a nice pair model.
impl<T, U> Model for MyPair<T, U> {
type Target = (T, U);
}
#[trusted]
#[ensures(@result == (a, b))]
fn my_pair<T, U>(a: T, b: U) -> MyPair<T, U> {
...
}