Releases: creusot-rs/creusot
v0.2.0
Following is the changelog of Creusot, a verification tool for safe Rust programs. Using Creusot you can prove -- formally -- that your Rust program behaves in a specific manner.
Creusot allows you to annotate your code using contracts which describe correctness conditions for your program. Creusot then uses SMT solvers to check that these contracts hold for all possible runs of the program. All of this is done statically without running your program, and contracts are erased at compilation time.
Creusot is currently best suited for the verification of code like data-structures or algorithm implementations, and less so for systems which interact heavily with the outside world or exploit concurrency. Notable projects using Creusot include the CreuSAT verified SAT solver and the Sprout SMT solver.
Creusot is still very experimental software, you should expect some obscure crashes and missing features.
Cargo Creusot
Cargo creusot saw several minor improvements especially with regards to configurations.
Users upgrading from v0.1
will need to regenerate their configuration by running cargo creusot setup install
.
Pearlite
This release introduces the foundations of termination checking in Creusot by providing two new macros: #[terminates]
and #[pure]
.
#[terminates]
indicates that a function terminates, these functions are allowed to crash or run out of memory.#[pure]
these functions are total, they must terminate and cannot exhibit any side-effects.
The termination check generated by Creusot is currently overly conservative and does not support loops or mutally recursive functions.
We expect to lift this restriction in future releases.
While terminates
functions may call either pure
or terminates
functions, pure
can only call other pure
functions.
Creusot Backend
This change should mostly not be user-visible, but we want to disclose it both to encourage users to bring up any problems they encounter when moving to 0.2 and to share our vision for future releases.
Version 0.2 marks the transition of Creusot to the new intermediate verification language Coma. Coma is designed as a modern kernal language for the Why3 platform and offers incredible flexibility while keeping an extermely minimal core. This replaces our usage of MLCFG in Creusot as the language we target.
Using Coma we have a solution for the specification of closures which could allow us to elide significant portions of specifications in proofs.
We don't currently leverage this, but expect it to be ready by version 0.3.
We expect the primary noticable change to be a regression in the labels for proof tasks in logical functions, if you notice any other regressions including newly failing proofs, please report them on github.
Why3find support
The code generated by Creusot was changed to be drop-in compatible with why3find
, an alternative cli-driven frontend for why3.
You can run why3find prove creusot_generated_file.coma
, so long as the directory this is run in contains a copy of the prelude
folder of Creusot.
Future verisons will integrate this natively into cargo creusot
.
v0.1.1
Creusot 0.1
The following are the release notes for the first official version of Creusot, a verification tool for safe Rust programs. Using Creusot you can prove -- formally -- that your Rust program behaves in a specific manner.
Creusot allows you to annotate your code using contracts which describe correctness conditions for your program. Creusot then uses SMT solvers to check that these contracts hold for all possible runs of the program. All of this is done statically without running your program, and contracts are erased at compilation time.
Creusot is currently best suited for the verification of code like data-structures or algorithm implementations, and less so for systems which interact heavily with the outside world or exploit concurrency. Notable projects using Creusot include the CreuSAT verified SAT solver and the Sprout SMT solver.
Since this is the first release of Creusot, we will cover the currently implemented features and aspects of Rust which are supported.
Creusot is still very experimental software, you should expect some obscure crashes and missing features.
Getting Started with Creusot
To get started as a user with Creusot, we recommend checking out the README.
Cargo Integration
Creusot provides the cargo creusot
binary which serves to make verification of crates simple.
To get started with Creusot, you can run cargo creusot
on your crate, generating proof obligations in target/your-crate.mlcfg
.
These proof obligations can be discharged using Why3 and the Why3 IDE.
cargo creusot setup
To help you manage your Creusot and Why3 installations, we provide cargo creusot setup
.
Through this command you can install, or view the Creusot specific Why3 configuration and prover installations.
Setup and manage Creusot's installation
Usage: creusot setup <COMMAND>
Commands:
status Show the current status of the Creusot installation
install Setup Creusot or update an existing installation
help Print this message or the help of the given subcommand(s)
Options:
-h, --help Print help
cargo creusot setup install
can currently download and install binaries for CVC4
, CVC5
and Z3
. Eventually it will also be capable of installing Alt-Ergo
and Why3
for you (currently these need to be installed separately using opam). See the README for detailed installation instructions.
'External' versions of supported provers can be provided via the --external
flag.
Supported Language Features
Creusot supports a large portion of the Rust language, some of these language constructs are listed below:
Basic Language constructs
Control flow: All control flow syntax is supported:while
, loop
, for
, if
, else
, let if
, let else
, break
, continue
, etc..
Borrows Creusot has complete support for all forms of borrowing in Rust. This includes mutable borrows. You can create borrows, reborrow fields, store borrows in types, all operations on borrows are supported.
Traits
Traits Decls & Impls: Curently, we support traits with associated methods types, and constants. We also handle implementations of these traits.
GATs are currently unsupported.
Bounds: We support trait bounds involving associated types.
Bounds involving GATs, const generics, or HRTB are unsupported.
Trait Objects: Trait objects are not supported.
Closures
Creusot supports most closures in Rust, including FnOnce
, FnMut
or Fn
, and we also support move
closures. Async closures are not supported as Creusot does not support async
code currently.
Iterators
By building off our support for closures and traits, we provide extensive support for iterators and iterator chains in Creusot.
Unsupported Language Features
Equally important are the parts of Rust which are unsupported by Creusot, if your code uses these you will need to rewrite it before Creusot can help you verify your code.
Async
Async code is currently unsupported by Creusot, we do not support generators or coroutines in our encoding.
Unsafe
Creusot's verification relies on the Rust type system's ownership so we cannot verify code using raw pointers.
When raw pointers are encountered, Creusot will not crash but instead generate verification conditions which will be unprovable for almost anything.
This allows trivial usage of mutable pointers for things like vec![]
.
Trait Objects
We do not currently support trait object reasoning. Like with raw pointers we generate verification conditions which are useless for anything beyond the most trivial checks.
This allows usage of println!()
or similar macros to work.
HRTB & GATs
Advanced features like Higher-Ranked Trait Bounds or Generic Associated Types are not currently supported by Creusot.
Specification Language: Pearlite
To enable verification, Creusot provides a specification language called Pearlite which you can use to annotate your code with assertions code must satisfy. Pearlite includes many features that are targeted to make specific kinds of Rust code verifiable, which we will list below.
Contracts & Assertions
Pearlite provides several forms of contracts you can use to specify your code:
#[requires(..)]
specifies a precondition for a function. This accepts a Pearlite expression as argument. Requires clauses will be checked at all program function call sites.#[ensures(..)
specifies a postcondition for a function. Accepts a Pearlite expression. Creusot will check that all function exits uphold the postcondition.#[variant(..)]
specifies a variant which can be used to show that a function terminates. A variant clause must evaluate to a type with a strictly decreasing, finite size (aka a well-founded order in math speak). Examples of this are positive integers, or any Rust type defined withBox
. This will be enforced at all recursive calls.#[invariant(..)]
specifies a loop invariant, a property which is true throughout every iteration of a loop. Invariants are the only thing Creusot uses to reason about the behavior of loops. This is checked at loop entry and at the end of each loop iteration.proof_assert!(..)
is a Pearlite analogue to Rust'sassert!
macro. It allows you to assert the truth value of a Pearlite expression, which may mention ghost code.#[trusted]
tells Creusot not to generate any proof obligations for the attached function.
Pearlite Expressions
Pearlite is a total, functional language with a syntax similar to Rust. It extends the syntax of Rust expressions in several minor ways, and more importantly has different semantics, implied by its totality.
This means that operations like a + b
are always defined, even for values which would panic in ordinary Rust. Instead, in Pearlite they would produce an unspecified value.
Basic Syntax
Pearlite syntax corresponds of basic Rust expressions: variables, literals, let bindings, if-else, match, function calls & type constructors, extended with a few new operations.
We provide quantifiers forall<x : T, ..> expr
and exists<x : T, .. > expr
for univeral and existential quantification respectively.
We also have the postfix "model" operator @
which is a sugar for Creusot's ShallowModel
trait.
The most important operation in Pearlite is the ^
final operator which is used to dereference a mutable borrow at the end of its lifetime.
Pearlite can be written in two different ways, either as ordinary Rust, in which case you are restricted to the Rust syntax fragment of Pearlite, or using the pearlite!{}
macro which provides our additional syntax:
#[predicate]
fn my_function(x: Int) -> bool {
x >= 0 // can use basic pearlite here
}
#[predicate]
fn exists_inverse(y : Int) -> bool {
pearlite! { exists< x : Int> x + y == 0 }
}
Pearlite contract clauses are implicitly wrapped in a pearlite!
macro invocation.
Mutable Borrows
Rust code uses lots of mutable borrows, so having an efficient method for reasoning about them and proving code using borrows is important.
Pearlite provides the ^
final value operator which mirrors *
by dereferencing in the "future" of a borrow.
Using this we could specify a simple increment function as follows:
#[requires(x < 1000u32)]
#[ensures(^ x == *x + 1u32)]
fn incr(x : &mut u32) { *x += 1}
This postcondition can be read as "the final value of x is its initial value + 1".
Where the ^
final value becomes particularly handy is when functions return mutable borrows, like the following:
#[ensures(^ result == (^x).0)]
#[ensures(* result == (* x).0)]
fn project(x: &mut (u32, bool)) -> &mut u32 {
&mut x.0
}
By adding this postcondition stating that the final value of the result is the same as the final value of the first field of x
, Creusot can track updates to the x
through the returned borrow.
This kind of code which mirrors a specification for the current and final values is so common that we also provide "logical (re) borrowing" as a syntactic sugar. The prior example could instead be written as:
#[ensures(result == &mut x.0)]
fn project(x: &mut (u32, bool)) -> &mut u32 {
&mut x.0
}
Logical Types
In verification, we often want to use abstractions which have nicer mathematical properties than real-world types and values (like unbounded integers, mathematical sets, etc...).
Several of these types are provided as part of the Pearlite standard library:
Int
the type of mathematical integers. You can convert a machine integer to anInt
by taking its modelx@
.Seq<T>
the type of sequences, useful for reason...