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
Documentation using cargo creusot doc now includes functions specifications and logic function bodies (Arnaud Golfouse @arnaudgolfouse).
Proof obligations are now generated in a separate verif directory, and by default cargo creusot will generate one coma file per module in your program, this can enable faster iteration by only loading relevant submodules during verification.
The old behavior can be restored by passing the --monolithic flag.
Note: We are planning on removing the --focus-on option with the arrival of modular code generation.
The cargo creusot why3 ide has been made aware of this behavior.
Creusot IDE
Not strictly speaking part of this release, we have recently published a new Creusot IDE extension on the VSCode Marketplace.
The extension currently provides syntax highlighting for Creusot, and dynamically updates the proof status within VSCode.
It also has support for running why3find on proofs that have pending obligations by interacting with an icon in the sidebar.
Pearlite
Several minor but still important changes were made to Pearlite in this release, their descriptions follow.
Nested Trusted
The semantics of #[trusted] were slightly altered, the attribute is now inherited, which means that placing it on a module marks all contained functions as trusted. (Xavier Denis @xldenis, request by Molly MacLaren @mojeanmac)
Type invariants & Resolution
Type invariants were completely overhauled, several unsoundnesses were resolved in the process.
Invariants are now added as pre and post conditions to program functions, but are not enforced for logical constructs.
Logical functions and quantifiers no longer provide the invariant, meaning that you must explicitly guard them if you require the invariant to be upheld for a type. This enables future support for empty types.
The resolution trait no longer uses specialization (meaning you no longer have to add min_specialization to your projects). Users should also now use the new, bare resolve functions if needed.
Resolution also comes with a proof obligation to demonstrate the soundness of user-provided implementations of the Resolve trait.
Syntax changes & bug fixes
New syntax to specify triggers in quantifiers (David Ewert @dewert99). Triggers can be added to quantifiers in the following way: forall<x : T, .. > #![trigger exp1,..,expN] exp.
Multi-triggers are supported by providing multiple comma separated values.
Fixes to #[derive(DeepModel)] for structs (Arnaud Golfouse @arnaudgolfouse).
Creusot standard library
The API support for VecDeque was extended, adding indexing, and a custom Resolve implementation. (David Ewert @dewert99)
New specifications for map and filter were added. While proven, the specification for filter is currently hard to successfully apply in projects, we expect revisions in future releases.
Several changes were made to the GhostPtrMap module. (@dewert99)
The ShallowModel trait was renamed to View which is hoped to be less confusing. (Armaël Guéneau @Armael)
Creusot Backend
Place-oriented reasoning
This release marks the complete transition of Creusot to a fully "place oriented" mode of reasoning.
For users, what this means, is generally an easier time working with type invariants, specifically with partially initialized structures and the closing of several lingering unsoundnesses.
Closures
Several crashes with regards to closures (especially nested) were fixed.
Support was added for proof_assert! inside of closures.
Structural Resolution
A new intrinsic structural_resolve generates a resolution statement from the conjunction of fields of a type. All user-defined implementations must be weaker than this.
Ownership in Ghost code
An initial, experimental version of ownership in ghost code was added, reintroducing the ghost! macro. Future releases will flesh out support in this area. (@arnaudgolfhouse)
Coma
A major unsoundness in our encoding of pattern matching in Coma was solved. We found that this was exploited by solvers in a single test of our suite (though without affecting the end reuslt of the proof).
The issue was resolved.
Identifiers generated in Coma are now stable, meaning that re-organizing Rust code should not lead to any changes in generated proofs. This should improve the obsolecence of proofs in Why3. (Li-yao Xia @Lysxia)
SMT Solvers
The Alt-Ergo solver was upgraded to version 2.6.0. As a bonus, it is now installed by cargo creusot setup itself instead of opam. (Armaël Guéneau @Armael)
