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.