Releases: creusot-rs/creusot
Creusot v0.10.0
Creusot v0.9.0
See the CHANGELOG.
Creusot v0.8.0
See the CHANGELOG.
Creusot v0.7.0
See the CHANGELOG.
v0.6.0
v0.5.0
v0.4.0
v0.3.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
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)
Contributors
Assets 2
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.