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 --creusot-contracts /PATH/TO/CREUSOT/creusot-contracts
Remark The path /PATH/TO/CREUSOT
should be either absolute, or relative to the package-name
directory to be created by that command,
not relative to the current directory.
That command creates a directory package-name
containing the basic elements of a Rust project verified with Creusot.
The command-line option --creusot-contracts /PATH/TO/CREUSOT/creusot-contracts
sets the dependency path in the package manifest Cargo.toml
:
# Cargo.toml
[package]
name = "project-name"
version = "0.1.0"
edition = "2021"
[dependencies]
creusot-contracts = { path = "/PATH/TO/CREUSOT/creusot-contracts" }
The project 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
-
Run the Creusot translation.
$ cargo creusot
-
Run the Why3find prover.
$ cargo creusot prove
Run the Why3find prover on specific files:
$ cargo creusot prove verif/[COMA_FILES]
-
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]