This crate contains the evaluation libraries and benchmarks for the RustHornBelt PLDI paper.
The crate includes the following benchmarks:
Each example is in its own file inside of src/
All RustHornBelt specifications are provided in src/prelude/
.
Creusot specifications are written in a first-order program logic, which includes two novel operators.
The ^
operator (pronounced final) accesses the prophecy of a mutable borrow, this corresponds to taking the second projection of the representation of a mutable borrow in RustHornBelt.
The @
operator (pronounced model) accesses the representation value of a type, like ⌊_⌋
in RustHornBelt.
To access the current value of a mutable borrow, we just use normal dereferencing, as it is just the value being pointed to at any moment by the borrow.
So the resolution of a mutable borrow can be expressed as the equality: ^ x == * x
, stating that the final value of x
equals the current value of x
.
git clone https://github.com/xldenis/creusot
cargo install --path creusot
opam pin add why3 https://gitlab.inria.fr/why3/why3.git#master
Install Z3 and CVC4.
Configure why3:
why3 config detect
make proofs
why3 ide -Lpath/to/creusot/prelude proofs.mlcfg