From fc03feb93b56cefc3fe585decee078e2ea0c0ded Mon Sep 17 00:00:00 2001 From: arnaudgolfouse Date: Wed, 20 Mar 2024 14:11:38 +0100 Subject: [PATCH 1/4] Improve the guide - Various placeholder sections - Section on final reborrows - Section on requires/ensures - Section on snapshots --- guide/src/SUMMARY.md | 9 ++++ guide/src/basic_concepts.md | 1 + guide/src/invariants.md | 7 +++ guide/src/logic_functions.md | 7 +++ guide/src/mutable_borrows.md | 85 +++++++++++++++++++++++++++++++++++ guide/src/pearlite.md | 7 +++ guide/src/proof_assert.md | 6 +++ guide/src/quickstart.md | 35 +++++++++++++++ guide/src/requires_ensures.md | 52 +++++++++++++++++++++ guide/src/snapshots.md | 40 +++++++++++++++++ 10 files changed, 249 insertions(+) create mode 100644 guide/src/basic_concepts.md create mode 100644 guide/src/invariants.md create mode 100644 guide/src/logic_functions.md create mode 100644 guide/src/mutable_borrows.md create mode 100644 guide/src/pearlite.md create mode 100644 guide/src/proof_assert.md create mode 100644 guide/src/requires_ensures.md create mode 100644 guide/src/snapshots.md diff --git a/guide/src/SUMMARY.md b/guide/src/SUMMARY.md index df00cc81a..fba565bfc 100644 --- a/guide/src/SUMMARY.md +++ b/guide/src/SUMMARY.md @@ -1,3 +1,12 @@ # Summary - [Quickstart](./quickstart.md) +- [Basic concepts](./basic_concepts.md) + - [`requires` and `ensures`](requires_ensures.md) + - [Invariants](invariants.md) + - [`proof_assert`](proof_assert.md) +- [Pearlite](./pearlite.md) +- [Logic functions](logic_functions.md) +- [Snapshots](snapshots.md) +- [Mutable borrows](mutable_borrows.md) +- [Type invariants](./type_invariants.md) diff --git a/guide/src/basic_concepts.md b/guide/src/basic_concepts.md new file mode 100644 index 000000000..dbb278946 --- /dev/null +++ b/guide/src/basic_concepts.md @@ -0,0 +1 @@ +# Basic concepts diff --git a/guide/src/invariants.md b/guide/src/invariants.md new file mode 100644 index 000000000..314a50860 --- /dev/null +++ b/guide/src/invariants.md @@ -0,0 +1,7 @@ +# Invariants + +TODO: Documentation on `#[invariant]`: + +- syntax +- meaning +- common patterns diff --git a/guide/src/logic_functions.md b/guide/src/logic_functions.md new file mode 100644 index 000000000..6d97e60f9 --- /dev/null +++ b/guide/src/logic_functions.md @@ -0,0 +1,7 @@ +# Logic functions + +TODO: + +- Explain the syntax and usage of `#[logic]` functions +- Explain `#[logic(prophetic)]` +- Explain `#[open(...)]` diff --git a/guide/src/mutable_borrows.md b/guide/src/mutable_borrows.md new file mode 100644 index 000000000..4a5f76b1d --- /dev/null +++ b/guide/src/mutable_borrows.md @@ -0,0 +1,85 @@ +# Mutable borrows + +Model of a mutable borrow + +## Final reborrows + +The above model is incomplete: in order to preserve soundness (see the [Why is this needed ?](#why-is-this-needed-) section), we need to add a third field to the model of mutable borrows, which we call the _id_. + +Each new mutable borrow gets a unique id, including reborrows. However, this is too restrictive: with this, the identity function cannot have its obvious spec (`#[ensures(result == input)]`), because a reborrow happens right before returning. + +To fix this, we introduce **final reborrows**: + +A reborrow is considered final if the prophecy of the original borrow depends only on the reborrow. +In that case, the reborrow id can be inherited: + +- If this is a reborrow of the same place (e.g. `let y = &mut *x`), the new id is the same. +- Else (e.g. `let y = &mut x.field`), the new id is deterministically derived from the old. + +### Examples + +In most simple cases, the reborrow is final: + +```rust +let mut i = 0; +let borrow = &mut i; +let reborrow = &mut *borrow; +// Don't use `borrow` afterward +proof_assert!(reborrow == borrow); + +#[ensures(result == x)] +fn identity(x: &mut T) -> &mut T { + x +} +``` + +It even handles reborrowing of fields: + +```rust +let mut pair = (1, 2); +let mut borrow = &mut pair; +let borrow_0 = &mut borrow.0; +proof_assert!(borrow_0 == &mut borrow.0); +``` + +However, this is not the case if the original borrow is used after the reborrow: + +```rust +let mut i = 0; +let borrow = &mut i; +let reborrow = &mut *borrow; +*borrow = 1; +proof_assert!(borrow == reborrow); // unprovable + // Here the prophecy of `borrow` is `1`, + // which is a value completely unrelated to the reborrow. +``` + +Or if there is an indirection based on a runtime value: + +```rust +let mut list = creusot_contracts::vec![1, 2]; +let borrow: &mut [i32] = &mut list; +let borrow_0 = &mut borrow[0]; +proof_assert!(borrow_0 == &mut borrow[0]); // unprovable +``` + +### Why is this needed ? + +In essence, to prevent the following unsound code: + +```rust +pub fn unsound() { + let mut x: Snapshot = snapshot! { true }; + let xm: &mut Snapshot = &mut x; + let b: &mut Snapshot = &mut *xm; + let bg: Snapshot<&mut Snapshot> = snapshot! { b }; + proof_assert! { ***bg == true && *^*bg == true }; + let evil: &mut Snapshot = &mut *xm; + proof_assert! { (evil == *bg) == (*^evil == true) }; + *evil = snapshot! { if evil == *bg { false } else { true } }; + proof_assert! { **evil == !*^evil }; + proof_assert! { **evil == !**evil }; +} +``` + +If borrows are only a pair of current value/prophecy, the above code can be proven, and in particular it proves `**evil == !**evil`, a false assertion. diff --git a/guide/src/pearlite.md b/guide/src/pearlite.md new file mode 100644 index 000000000..3b03ad264 --- /dev/null +++ b/guide/src/pearlite.md @@ -0,0 +1,7 @@ +# Pearlite + +TODO: +- When can it be used +- The 'model' operator +- The `==>` operator +- `forall`, `exists` \ No newline at end of file diff --git a/guide/src/proof_assert.md b/guide/src/proof_assert.md new file mode 100644 index 000000000..49d8ca1c1 --- /dev/null +++ b/guide/src/proof_assert.md @@ -0,0 +1,6 @@ +# `proof_assert!` + +TODO: + +- Syntax +- usage diff --git a/guide/src/quickstart.md b/guide/src/quickstart.md index acb98436e..55bcf69ac 100644 --- a/guide/src/quickstart.md +++ b/guide/src/quickstart.md @@ -1 +1,36 @@ # Quickstart + +Install Creusot and why3 as described in the [README](https://github.com/creusot-rs/creusot). + +Then, create a new project, and import creusot-contracts to start writing specifications: + +```toml +# Cargo.toml +[package] +name = "add_one" +version = "0.1.0" +edition = "2021" + +[dependencies] +creusot-contracts = { path = "/PATH/TO/CREUSOT/creusot-contracts" } + +``` + +```rust +// src/lib.rs +use creusot_contracts::*; + +#[requires(x < i32::MAX)] +#[ensures(result@ == x@ + 1)] +pub fn add_one(x: i32) -> i32 { + x + 1 +} +``` + +Then, launch the why3 ide: + +```sh +cargo creusot why3 ide +``` + +The documentation for the why3 ide can be found [here](https://www.why3.org/doc/starting.html#getting-started-with-the-gui). diff --git a/guide/src/requires_ensures.md b/guide/src/requires_ensures.md new file mode 100644 index 000000000..a424f6329 --- /dev/null +++ b/guide/src/requires_ensures.md @@ -0,0 +1,52 @@ +# requires and ensure + +Most of what you will be writing with creusot will be `requires` and `ensures` clauses. That is: **preconditions** and **postconditions**. + +Together, those form the **contract** of a function. This is in essence the "logical signature" of your function: when analyzing a function, only the contract of other functions is visible. + +## Preconditions with `requires` + +A _precondition_ is an assertion that must hold when entering the function. For example, the following function accesses a slice at index `0`: + +```rust +fn head(v: &[i32]) -> i32 { + v[0] +} +``` + +So we must require that the slice has at least one element: + +```rust +#[requires(v@.len() >= 1)] +fn head(v: &[i32]) -> i32 { + v[0] +} +``` + +## An aside on models + +When writing specifications, the language used is similar to, but not exactly Rust. It is called _Pearlite_. + +In Pearlite, types are the _logical_ types: we don't have `i32`, `Vec` or `HashMap`, but `Int` (mathematical integer, unbounded), `Seq` (sequence of objects) and `Map` (mapping of objects). + +Additionally, we cannot use most functions that we are accustomed to, like `Vec::len`, because they are not purely logical functions. To get around this, types can define their **model**, which is their equivalent in the logical world : we can then call functions and methods on these logical types. + +In this case, the model of `&[i32]` is a sequence `Seq`: we access this model by using the `@` suffix operator. + +To learn more, see the chapters on [models](TODO) and [Pearlite](./pearlite.md). + +## Postconditions with `ensures` + +A _postcondition_ is an assertions that is proven true at the end of the function. The return value of the function can be accessed via the `result` keyword. + +In the case of the example above, we want to assert that the returned integer is the first of the slice: + +```rust +#[requires(v@.len() >= 1)] +#[ensures(v@[0] == result)] +fn head(v: &[i32]) -> i32 { + v[0] +} +``` + +Note that we can index a `Seq` to get a `i32`. diff --git a/guide/src/snapshots.md b/guide/src/snapshots.md new file mode 100644 index 000000000..eb2cdb914 --- /dev/null +++ b/guide/src/snapshots.md @@ -0,0 +1,40 @@ +# Snapshots + +A useful tool to have in proofs is the `Snapshot` type (`creusot_contracts::Snapshot`). `Snapshot` is: + +- a zero-sized-type +- created with the `snapshot!` macro +- whose model is the model of `T` +- that can be dereferenced in a logic context. + +## Example + +They can be useful if you need a way to remember a previous value, but only for the proof: + +```rust +#[ensures(permutation_of((*array)@, (^array)@))] +#[ensures(is_sorted(^array))] +fn insertion_sort(array: &mut [i32]) { + let original = snapshot!(*array); // remember the original value + let n = array.len(); + #[invariant(permutation_of(original@, (*array)@))] + for i in 1..n { + let mut j = i; + #[invariant(permutation_of(original@, (*array)@))] + while j > 0 { + if array[j - 1] > array[j] { + array.swap(j - 1, j); + } + } + } +} + +#[logic] +fn permutation_of(s1: Seq, s2: Seq) -> bool { + // ... +} +#[logic] +fn is_sorted(s: Seq) -> bool { + // ... +} +``` From 3fdf29720144171393804e8168141a0f93217db4 Mon Sep 17 00:00:00 2001 From: arnaudgolfouse Date: Wed, 20 Mar 2024 15:04:36 +0100 Subject: [PATCH 2/4] Move explanations from the README to the guide --- README.md | 132 ++-------------------------------- guide/src/SUMMARY.md | 5 +- guide/src/basic_concepts.md | 12 ++++ guide/src/invariants.md | 13 +++- guide/src/logic_functions.md | 73 +++++++++++++++++-- guide/src/model.md | 25 +++++++ guide/src/mutable_borrows.md | 2 +- guide/src/pearlite.md | 38 ++++++++-- guide/src/quickstart.md | 22 +++++- guide/src/requires_ensures.md | 2 +- guide/src/trusted.md | 14 ++++ guide/src/variants.md | 7 ++ 12 files changed, 200 insertions(+), 145 deletions(-) create mode 100644 guide/src/model.md create mode 100644 guide/src/trusted.md create mode 100644 guide/src/variants.md diff --git a/README.md b/README.md index 1d390ec1c..d762ee1bb 100644 --- a/README.md +++ b/README.md @@ -80,135 +80,13 @@ More examples are found in [creusot/tests/should_succeed](creusot/tests/should_s $ cargo creusot setup install ``` -# Hacking on Creusot - -See [HACKING.md](HACKING.md) for information on the developer workflow for -hacking on the Creusot codebase. - # Verifying with Creusot and Why3 -The recommended way for users to verify programs with Creusot is to use `cargo-creusot`. -All you need to do is enter your project and run `cargo creusot`! -This will generate MLCFG files in `target/debug/` which can then be loaded into Why3. - -This may only work if you're using the same rust toolchain that was used to build `creusot`: -you can copy the [`rust-toolchain`](./ci/rust-toolchain) file into the root of your project to -make sure the correct toolchain is selected. - -To add contracts to your programs you will need to use the `creusot-contracts` crate by adding it as a dependency: -```toml -# Cargo.toml - -[dependencies] -creusot-contracts = { path = "/path/to/creusot/creusot-contracts" } -``` - -Adding this dependency will make the contract macros available in your code. These macros will erase themselves when compiled with `rustc`. -To add Creusot-only trait implementations or code, you can use `cfg(creusot)` to toggle. - -You must also explicitly use the `creusot_contracts` crate in your code (which should be the case once you actually prove things, but not necessarily when you initially set up a project), such as with the line: - -```rust -use creusot_contracts::*; -``` - -or you will get a compilation error complaining that the `creusot_contracts` crate is not loaded. - -## Proving in Why3 - -To load your files in Why3, we recommend using the [`ide`](./ide) script provided in the Creusot repository. -You may also copy both this script and the `prelude` directory in your project to have a fully self contained proof environment. - -To load your proofs in Why3, run: - -``` -REPO/ide PATH/TO/OUTPUT.mlcfg -``` - -From there standard proof strategies of Why3 work. We recommend section 2.3 of this [thesis](https://sarsko.github.io/_pages/SarekSkot%C3%A5m_thesis.pdf) for a brief overview of Why3 and Creusot proofs. - -We plan to improve this part of the user experience, but that will have to wait until Creusot gets more stable and complete. -If you'd like to help, a prototype VSCode plugin for Why3 is [in development](https://github.com/xldenis/whycode), it should make the experience much smoother when complete. - -# Writing specs in Rust programs - -## Using Creusot for your Rust code + +See the [guide](./guide/). -First, you will need to depend on the `creusot-contracts` crate, add it to your `Cargo.toml` and enable the `contracts` feature to turn on contracts. -## Kinds of contract expressions - -Currently Creusot uses 4 different kinds of contract expressions: `requires`, `ensures`, `invariant` and `variant`. - -The most basic are `requires` and `ensures`, which can be attached to a Rust function declaration like so: -```rust -#[requires(... precondition ...)] -#[ensures(... postcondition ...)] -fn my_function(i: u32) -> bool { ... } -``` -You can attach as many `ensures` and `requires` clauses as you would like, in any order. - -Inside a function, you can attach `invariant` clauses to loops, these are attached on *top* of the loop rather than inside, like: -```rust -#[invariant(... loop invariant ...)] -while ... { ... } -``` - -A `variant` clause can be attached either to a function like `ensures`, or `requires` or to a loop like `invariant`, it should contain a strictly decreasing expression which can prove the termination of the item it is attached to. - -## Controlling verification - -We also have features for controlling verification. - -First, the `trusted` marker lets Creusot trust the implementation and specs. -More specifically, you can put `#[trusted]` on a function like the following: -```rust -#[trusted] -#[ensures(result == 42u32)] -fn the_answer() -> u32 { - trusted_super_oracle("the answer to life, the universe and everything") -} -``` - -Causing Creusot to assume the contracts are true. - -### Unbounded integers - -By default in Creusot, integers are represented with bounds-checking. This can be tedious or difficult to prove in certain cases, so we can disable bounds checking by passing the `--unbounded` flag to Creusot. - - -## Pearlite - -Contracts and logic functions are written in Pearlite, a specification language for Rust we are developing. Pearlite can be seen as a pure, immutable fragment of Rust which has access to a few additional logical operations and connectives. In practice you have: -- Base Rust expressions: matching, function calls, let bindings, binary and unary operators, tuples, structs and enums, projections, primitive casts, and dereferencing -- Logical Expressions: quantifiers (`forall` and `exists`), logical implication `==>`, *logical* equality `a == b`, labels -- Rust specific logical expressions: access to the **final** value of a mutable reference `^`, access to the *model* of an object `@` - -We also provide two new attributes on Rust functions: `logic` and `predicate`. - -Marked `#[logic]` or `#[predicate]`, a function can be used in specs and other logical conditions (`requires`/`ensures` and `invariant`). They can use ghost functions. -The two attributes have the following difference. -- A `logic` function can freely have logical, non-executable operations, such as quantifiers, logic equalities, etc. Instead, this function can't be called in normal Rust code (the function body of a `logic` function is replaced with a panic). - You can use pearlite syntax for any part in the logic function by marking that part with the `pearlite! { ... }` macro. - - If you need to use the prophecy operator `^` on a mutable reference, you need to mark the function `#[logic(prophetic)]`. -- A `predicate` is a logical function which returns a proposition (in practice, returns a boolean value). - -When you write *recursive* `ghost`, `logic` or `predicate` functions, you have to show that the function terminates. -For that, you can add `#[variant(EXPR)]` attribute, which says that the value of the expression `EXPR` strictly decreases (in a known well-founded order) at each recursive call. -The type of `EXPR` should implement the `WellFounded` trait. +# Hacking on Creusot -You can also give a custom *model* to your type. -To do that, you just implement the `Model` trait (provided in `creusot_contracts`) specifying the associated type `Model`. -You give a trusted spec that defines the model (which can be accessed by `@`) on primitive functions. -For example, the following gives a spooky data type `MyPair` a nice pair model. -```rust -impl Model for MyPair { - type Target = (T, U); -} -#[trusted] -#[ensures(@result == (a, b))] -fn my_pair(a: T, b: U) -> MyPair { - ... -} -``` +See [HACKING.md](HACKING.md) for information on the developer workflow for +hacking on the Creusot codebase. diff --git a/guide/src/SUMMARY.md b/guide/src/SUMMARY.md index fba565bfc..c121b6ecb 100644 --- a/guide/src/SUMMARY.md +++ b/guide/src/SUMMARY.md @@ -4,9 +4,12 @@ - [Basic concepts](./basic_concepts.md) - [`requires` and `ensures`](requires_ensures.md) - [Invariants](invariants.md) + - [Variants](variants.md) - [`proof_assert`](proof_assert.md) +- [Trusted](./trusted.md) - [Pearlite](./pearlite.md) - [Logic functions](logic_functions.md) - [Snapshots](snapshots.md) -- [Mutable borrows](mutable_borrows.md) +- [Model](model.md) + - [Mutable borrows](mutable_borrows.md) - [Type invariants](./type_invariants.md) diff --git a/guide/src/basic_concepts.md b/guide/src/basic_concepts.md index dbb278946..e032aeaad 100644 --- a/guide/src/basic_concepts.md +++ b/guide/src/basic_concepts.md @@ -1 +1,13 @@ # Basic concepts + +Every Creusot macro will erase themselves when compiled normally: they only exist when using `cargo creusot`. + +If you need to have Creusot-only code, you can use the `#[cfg(creusot)]` attribute. + +Note that you must explicitly use the `creusot_contracts` crate in your code (which should be the case once you actually prove things, but not necessarily when you initially set up a project), such as with the line: + +```rust +use creusot_contracts::*; +``` + +or you will get a compilation error complaining that the `creusot_contracts` crate is not loaded. diff --git a/guide/src/invariants.md b/guide/src/invariants.md index 314a50860..e488e0bee 100644 --- a/guide/src/invariants.md +++ b/guide/src/invariants.md @@ -1,7 +1,14 @@ # Invariants -TODO: Documentation on `#[invariant]`: +Inside a function, you can attach `invariant` clauses to loops, these are attached on _top_ of the loop rather than inside, like: -- syntax +```rust +#[invariant(... loop invariant ...)] +while ... { ... } +``` + + diff --git a/guide/src/logic_functions.md b/guide/src/logic_functions.md index 6d97e60f9..77198416c 100644 --- a/guide/src/logic_functions.md +++ b/guide/src/logic_functions.md @@ -1,7 +1,72 @@ # Logic functions -TODO: +We provide two new attributes on Rust functions: `logic` and `predicate`. -- Explain the syntax and usage of `#[logic]` functions -- Explain `#[logic(prophetic)]` -- Explain `#[open(...)]` +Marked `#[logic]` or `#[predicate]`, a function can be used in specs and other logical conditions (`requires`/`ensures` and `invariant`). They can use ghost functions. +The two attributes have the following difference: + +- A `logic` function can freely have logical, non-executable operations, such as quantifiers, logic equalities, etc. Instead, this function can't be called in normal Rust code (the function body of a `logic` function is replaced with a panic). + You can use pearlite syntax for any part in the logic function by marking that part with the `pearlite! { ... }` macro. +- A `predicate` is a logical function which returns a proposition (in practice, returns a boolean value). + +## Recursion + +When you write *recursive* `ghost`, `logic` or `predicate` functions, you have to show that the function terminates. +For that, you can add `#[variant(EXPR)]` attribute, which says that the value of the expression `EXPR` strictly decreases (in a known well-founded order) at each recursive call. +The type of `EXPR` should implement the `WellFounded` trait. + +## Prophetic functions + +As seen in the [model](./model.md) chapter, a mutable borrow contains a _prophetic_ value, whose value depends on future execution. In order to preserve the soundness of the logic, `#[logic]` functions are not allowed to observe that value: that is, they cannot call the prophetic `^` operator. + +If you really need a logic function to use that operator, you need to mark it with `#[logic(prophetic)]`/`#[predicate(prophetic)]` instead. In exchange, this function cannot be called from ghost code (unimplemented right now). + +A normal `#[logic]` function cannot call a `#[logic(prophetic)]` function. + +## Examples + +Basic example: + +```rust +#[logic] +fn logic_add(x: Int, y: Int) -> Int { + x + y +} + +#[requires(x < i32::MAX)] +#[ensures(result@ == logic_add(x@, 1))] +pub fn add_one(x: i32) -> i32 { + x + 1 +} +``` + +Pearlite block: + +```rust +#[predicate] +fn all_ones(s: Seq) -> bool { + pearlite! { + forall i >= 0 && i < s.len() ==> s[i]@ == 1 + } +} + +#[ensures(all_ones(result@))] +#[ensures(result@.len() == n@)] +pub fn make_ones(n: usize) -> Vec { + creusot_contracts::vec![1; n] +} +``` + +Recursion: + +```rust +TODO +``` + +Prophetic: + +```rust +TODO +``` + + diff --git a/guide/src/model.md b/guide/src/model.md new file mode 100644 index 000000000..2ed27256f --- /dev/null +++ b/guide/src/model.md @@ -0,0 +1,25 @@ +# Model + +You can give a custom _model_ to your type. +To do that, you just implement the `creusot_contracts::ShallowModel` trait specifying the associated type `ShallowModelTy`. It can then be accessed with the `@` operator. + +For example, the following gives a spooky data type `MyPair` a nice pair model. + +```rust +struct MyPair(T, U); + +impl ShallowModel for MyPair { + type ShallowModelTy = (T, U); + + #[logic] + #[open] + fn shallow_model(self) -> Self::ShallowModelTy { + (self.0, self.1) + } +} + +#[ensures(result@ == (a, b))] +fn my_pair(a: T, b: U) -> MyPair { + MyPair(a, b) +} +``` diff --git a/guide/src/mutable_borrows.md b/guide/src/mutable_borrows.md index 4a5f76b1d..33345dc6e 100644 --- a/guide/src/mutable_borrows.md +++ b/guide/src/mutable_borrows.md @@ -1,6 +1,6 @@ # Mutable borrows -Model of a mutable borrow +TODO: Model of a mutable borrow ## Final reborrows diff --git a/guide/src/pearlite.md b/guide/src/pearlite.md index 3b03ad264..744673d11 100644 --- a/guide/src/pearlite.md +++ b/guide/src/pearlite.md @@ -1,7 +1,35 @@ # Pearlite -TODO: -- When can it be used -- The 'model' operator -- The `==>` operator -- `forall`, `exists` \ No newline at end of file +Pearlite is the language used in: + +- contracts (`ensures`, `requires`, `invariant`, `variant`) +- `proof_assert!` +- the `pearlite!` macro + +It can be seen as a pure, immutable fragment of Rust which has access to a few additional logical operations and connectives. In practice you have: + +- Base Rust expressions: matching, function calls, let bindings, binary and unary operators, tuples, structs and enums, projections, primitive casts, and dereferencing +- Logical Expressions: quantifiers (`forall` and `exists`), logical implication `==>`, _logical_ equality `a == b`, labels +- Rust specific logical expressions: access to the **final** value of a mutable reference `^`, access to the [model](./model.md) of an object `@` + +## Logical implication + +Since `=>` is already a used token in Rust, we use `==>` to mean implication: + +```rust +proof_assert!(true ==> true); +proof_assert!(false ==> true); +proof_assert!(false ==> false); +// proof_assert!(true ==> false); // incorrect +``` + +## Quantifiers + +The logical quantifiers ∀ and ∃ are written `forall` and `exists` in Pearlite: + +```rust +#[requires(forall i >= 0 && i < list@.len() ==> list@[i] == 0)] +fn requires_all_zeros(list: &[i32]) { + // ... +} +``` diff --git a/guide/src/quickstart.md b/guide/src/quickstart.md index 55bcf69ac..6a4d6655e 100644 --- a/guide/src/quickstart.md +++ b/guide/src/quickstart.md @@ -1,8 +1,12 @@ # Quickstart +## Installation + Install Creusot and why3 as described in the [README](https://github.com/creusot-rs/creusot). -Then, create a new project, and import creusot-contracts to start writing specifications: +## Write specifications + +Create a new project, and import creusot-contracts to start writing specifications: ```toml # Cargo.toml @@ -13,9 +17,14 @@ edition = "2021" [dependencies] creusot-contracts = { path = "/PATH/TO/CREUSOT/creusot-contracts" } - ``` +**Remark** This may only work if you're using the same rust toolchain that was used to build `creusot`: +you can copy the [`rust-toolchain`](https://github.com/creusot-rs/creusot/blob/master/ci/rust-toolchain) file into the root of your project to +make sure the correct toolchain is selected. + +Then you can start writing specifications: + ```rust // src/lib.rs use creusot_contracts::*; @@ -27,10 +36,17 @@ pub fn add_one(x: i32) -> i32 { } ``` -Then, launch the why3 ide: +## Prove with Why3 + +Finally, launch the why3 ide: ```sh cargo creusot why3 ide ``` The documentation for the why3 ide can be found [here](https://www.why3.org/doc/starting.html#getting-started-with-the-gui). + +We also recommend section 2.3 of this [thesis](https://sarsko.github.io/_pages/SarekSkot%C3%A5m_thesis.pdf) for a brief overview of Why3 and Creusot proofs. + +We plan to improve this part of the user experience, but that will have to wait until Creusot gets more stable and complete. +If you'd like to help, a prototype VSCode plugin for Why3 is [in development](https://github.com/xldenis/whycode), it should make the experience much smoother when complete. diff --git a/guide/src/requires_ensures.md b/guide/src/requires_ensures.md index a424f6329..5111983b0 100644 --- a/guide/src/requires_ensures.md +++ b/guide/src/requires_ensures.md @@ -33,7 +33,7 @@ Additionally, we cannot use most functions that we are accustomed to, like `Vec: In this case, the model of `&[i32]` is a sequence `Seq`: we access this model by using the `@` suffix operator. -To learn more, see the chapters on [models](TODO) and [Pearlite](./pearlite.md). +To learn more, see the chapters on [models](./model.md) and [Pearlite](./pearlite.md). ## Postconditions with `ensures` diff --git a/guide/src/trusted.md b/guide/src/trusted.md new file mode 100644 index 000000000..fbac047da --- /dev/null +++ b/guide/src/trusted.md @@ -0,0 +1,14 @@ +# Trusted + +The `trusted` marker lets Creusot trust the implementation and specs. +More specifically, you can put `#[trusted]` on a function like the following: + +```rust +#[trusted] +#[ensures(result == 42u32)] +fn the_answer() -> u32 { + trusted_super_oracle("the answer to life, the universe and everything") +} +``` + +TODO: trusted traits diff --git a/guide/src/variants.md b/guide/src/variants.md new file mode 100644 index 000000000..b97ad815b --- /dev/null +++ b/guide/src/variants.md @@ -0,0 +1,7 @@ +# Variants + +A `variant` clause can be attached either to a function like `ensures`, or `requires` or to a loop like `invariant`, it should contain a strictly decreasing expression which can prove the termination of the item it is attached to. + + From f22dfec5eb30b41537ee59220912b1ceedf543cf Mon Sep 17 00:00:00 2001 From: arnaudgolfouse Date: Wed, 20 Mar 2024 17:05:37 +0100 Subject: [PATCH 3/4] Link to the guide built in CI This also removes the `guide-ci.yml` workflow, since the example we want to test need Creusot instead of normal Rust. --- .github/workflows/guide-ci.yml | 29 ----------------------------- .github/workflows/guide.yml | 2 -- README.md | 3 +-- 3 files changed, 1 insertion(+), 33 deletions(-) delete mode 100644 .github/workflows/guide-ci.yml diff --git a/.github/workflows/guide-ci.yml b/.github/workflows/guide-ci.yml deleted file mode 100644 index 761ba1586..000000000 --- a/.github/workflows/guide-ci.yml +++ /dev/null @@ -1,29 +0,0 @@ -name: User Guide CI -on: - push: - paths: - - guide/** - -jobs: - test: - name: Test - runs-on: ubuntu-latest - permissions: - contents: write # To push a branch - pull-requests: write # To create a PR from that branch - steps: - - uses: actions/checkout@master - - name: Install Rust - run: | - rustup set profile minimal - rustup toolchain install stable - rustup default stable - - name: Install latest mdbook - run: | - tag=$(curl 'https://api.github.com/repos/rust-lang/mdbook/releases/latest' | jq -r '.tag_name') - url="https://github.com/rust-lang/mdbook/releases/download/${tag}/mdbook-${tag}-x86_64-unknown-linux-gnu.tar.gz" - mkdir bin - curl -sSL $url | tar -xz --directory=bin - echo "$(pwd)/bin" >> $GITHUB_PATH - - name: Run tests - run: mdbook test guide \ No newline at end of file diff --git a/.github/workflows/guide.yml b/.github/workflows/guide.yml index 0086bc4f1..1ef0589a1 100644 --- a/.github/workflows/guide.yml +++ b/.github/workflows/guide.yml @@ -24,8 +24,6 @@ jobs: echo `pwd`/mdbook >> $GITHUB_PATH - name: Build Book run: | - # This assumes your book is in the root of your repository. - # Just add a `cd` here if you need to change to another directory. mdbook build guide - name: Setup Pages uses: actions/configure-pages@v2 diff --git a/README.md b/README.md index d762ee1bb..50051b780 100644 --- a/README.md +++ b/README.md @@ -82,8 +82,7 @@ More examples are found in [creusot/tests/should_succeed](creusot/tests/should_s # Verifying with Creusot and Why3 - -See the [guide](./guide/). +See the [guide](https://creusot-rs.github.io/creusot/). # Hacking on Creusot From 4f5677eb0744f5dda53e02606b7ee53b226f97b4 Mon Sep 17 00:00:00 2001 From: arnaudgolfouse Date: Wed, 20 Mar 2024 21:52:06 +0100 Subject: [PATCH 4/4] Reorganise sections, and improve the explanation of ShallowModel --- guide/src/SUMMARY.md | 14 ++++++++------ guide/src/{ => basic_concepts}/invariants.md | 0 guide/src/{ => basic_concepts}/proof_assert.md | 0 .../src/{ => basic_concepts}/requires_ensures.md | 16 +++++----------- guide/src/{ => basic_concepts}/variants.md | 0 guide/src/logic_functions.md | 2 +- guide/src/pearlite.md | 2 +- guide/src/representation_of_types.md | 3 +++ guide/src/representation_of_types/most_types.md | 14 ++++++++++++++ .../mutable_borrows.md | 10 +++++++++- guide/src/{model.md => shallow_model.md} | 11 ++++++++--- 11 files changed, 49 insertions(+), 23 deletions(-) rename guide/src/{ => basic_concepts}/invariants.md (100%) rename guide/src/{ => basic_concepts}/proof_assert.md (100%) rename guide/src/{ => basic_concepts}/requires_ensures.md (56%) rename guide/src/{ => basic_concepts}/variants.md (100%) create mode 100644 guide/src/representation_of_types.md create mode 100644 guide/src/representation_of_types/most_types.md rename guide/src/{ => representation_of_types}/mutable_borrows.md (82%) rename guide/src/{model.md => shallow_model.md} (71%) diff --git a/guide/src/SUMMARY.md b/guide/src/SUMMARY.md index c121b6ecb..ebd6a1022 100644 --- a/guide/src/SUMMARY.md +++ b/guide/src/SUMMARY.md @@ -2,14 +2,16 @@ - [Quickstart](./quickstart.md) - [Basic concepts](./basic_concepts.md) - - [`requires` and `ensures`](requires_ensures.md) - - [Invariants](invariants.md) - - [Variants](variants.md) - - [`proof_assert`](proof_assert.md) + - [`requires` and `ensures`](basic_concepts/requires_ensures.md) + - [Invariants](basic_concepts/invariants.md) + - [Variants](basic_concepts/variants.md) + - [`proof_assert`](basic_concepts/proof_assert.md) - [Trusted](./trusted.md) +- [Representation of types](representation_of_types.md) + - [Most types](representation_of_types/most_types.md) + - [Mutable borrows](representation_of_types/mutable_borrows.md) - [Pearlite](./pearlite.md) - [Logic functions](logic_functions.md) +- [Shallow model](./shallow_model.md) - [Snapshots](snapshots.md) -- [Model](model.md) - - [Mutable borrows](mutable_borrows.md) - [Type invariants](./type_invariants.md) diff --git a/guide/src/invariants.md b/guide/src/basic_concepts/invariants.md similarity index 100% rename from guide/src/invariants.md rename to guide/src/basic_concepts/invariants.md diff --git a/guide/src/proof_assert.md b/guide/src/basic_concepts/proof_assert.md similarity index 100% rename from guide/src/proof_assert.md rename to guide/src/basic_concepts/proof_assert.md diff --git a/guide/src/requires_ensures.md b/guide/src/basic_concepts/requires_ensures.md similarity index 56% rename from guide/src/requires_ensures.md rename to guide/src/basic_concepts/requires_ensures.md index 5111983b0..0b17f7771 100644 --- a/guide/src/requires_ensures.md +++ b/guide/src/basic_concepts/requires_ensures.md @@ -23,17 +23,9 @@ fn head(v: &[i32]) -> i32 { } ``` -## An aside on models +Note the **shallow model** (`@`) operator: it is needed to convert the Rust type `&[i32]` to a logical type `Seq`. Else, we could not call `[T]::len`, which is a program function (and not a logical one). -When writing specifications, the language used is similar to, but not exactly Rust. It is called _Pearlite_. - -In Pearlite, types are the _logical_ types: we don't have `i32`, `Vec` or `HashMap`, but `Int` (mathematical integer, unbounded), `Seq` (sequence of objects) and `Map` (mapping of objects). - -Additionally, we cannot use most functions that we are accustomed to, like `Vec::len`, because they are not purely logical functions. To get around this, types can define their **model**, which is their equivalent in the logical world : we can then call functions and methods on these logical types. - -In this case, the model of `&[i32]` is a sequence `Seq`: we access this model by using the `@` suffix operator. - -To learn more, see the chapters on [models](./model.md) and [Pearlite](./pearlite.md). +To learn more, see the chapter on [Pearlite](../pearlite.md) and [ShallowModel](../shallow_model.md). ## Postconditions with `ensures` @@ -49,4 +41,6 @@ fn head(v: &[i32]) -> i32 { } ``` -Note that we can index a `Seq` to get a `i32`. +Note that we: +- use the `@` operator on the slice to get a `Seq` +- we can then index this `Seq` to get a `i32`. diff --git a/guide/src/variants.md b/guide/src/basic_concepts/variants.md similarity index 100% rename from guide/src/variants.md rename to guide/src/basic_concepts/variants.md diff --git a/guide/src/logic_functions.md b/guide/src/logic_functions.md index 77198416c..c641b0f8a 100644 --- a/guide/src/logic_functions.md +++ b/guide/src/logic_functions.md @@ -17,7 +17,7 @@ The type of `EXPR` should implement the `WellFounded` trait. ## Prophetic functions -As seen in the [model](./model.md) chapter, a mutable borrow contains a _prophetic_ value, whose value depends on future execution. In order to preserve the soundness of the logic, `#[logic]` functions are not allowed to observe that value: that is, they cannot call the prophetic `^` operator. +As seen in the chapter on [mutable borrow](./representation_of_types/mutable_borrows.md), a mutable borrow contains a _prophetic_ value, whose value depends on future execution. In order to preserve the soundness of the logic, `#[logic]` functions are not allowed to observe that value: that is, they cannot call the prophetic `^` operator. If you really need a logic function to use that operator, you need to mark it with `#[logic(prophetic)]`/`#[predicate(prophetic)]` instead. In exchange, this function cannot be called from ghost code (unimplemented right now). diff --git a/guide/src/pearlite.md b/guide/src/pearlite.md index 744673d11..41c587c82 100644 --- a/guide/src/pearlite.md +++ b/guide/src/pearlite.md @@ -10,7 +10,7 @@ It can be seen as a pure, immutable fragment of Rust which has access to a few a - Base Rust expressions: matching, function calls, let bindings, binary and unary operators, tuples, structs and enums, projections, primitive casts, and dereferencing - Logical Expressions: quantifiers (`forall` and `exists`), logical implication `==>`, _logical_ equality `a == b`, labels -- Rust specific logical expressions: access to the **final** value of a mutable reference `^`, access to the [model](./model.md) of an object `@` +- Rust specific logical expressions: access to the **final** value of a mutable reference `^`, access to the [shallow model](./shallow_model.md) of an object `@` ## Logical implication diff --git a/guide/src/representation_of_types.md b/guide/src/representation_of_types.md new file mode 100644 index 000000000..277c6fc01 --- /dev/null +++ b/guide/src/representation_of_types.md @@ -0,0 +1,3 @@ +# Representation of types + +Creusot translates Rust code to Why3. But Rust types don't always exists in Why3, and would not have the same semantics: thus we need to map each Rust type to a Why3 type. \ No newline at end of file diff --git a/guide/src/representation_of_types/most_types.md b/guide/src/representation_of_types/most_types.md new file mode 100644 index 000000000..252e00b81 --- /dev/null +++ b/guide/src/representation_of_types/most_types.md @@ -0,0 +1,14 @@ +# Base types + +Most type have a very simple interpretation in Why3: + +- The interpretation for a scalar type (`i32`, `bool`, `f64`, ...) is itself. +- The interpretation of `[T]` is `Seq`, the type of sequences. +- The interpretation of `&T` is the interpretation of `T`. + + Creusot is able to assume that `T` and `&T` behave the same, because of the "shared xor mutable" rule of Rust: we won't be able to change the value (interior mutability is handled by defining a special model for e.g. `Cell`), so we may as well be manipulating an exact copy of the value. +- The interpretation of `Box` is the interpretation of `T`. + + This is because a `Box` uniquely own its content: it really acts exactly the same as `T`. +- Structures and enums are interpreted by products and sum types. +- The interpretation of `&mut T` is a bit more complicated: see the next section. diff --git a/guide/src/mutable_borrows.md b/guide/src/representation_of_types/mutable_borrows.md similarity index 82% rename from guide/src/mutable_borrows.md rename to guide/src/representation_of_types/mutable_borrows.md index 33345dc6e..33c35c811 100644 --- a/guide/src/mutable_borrows.md +++ b/guide/src/representation_of_types/mutable_borrows.md @@ -1,6 +1,14 @@ # Mutable borrows -TODO: Model of a mutable borrow +In Creusot, mutable borrows are handled via **prophecies**. A mutable borrow `&mut T` contains: + +- The current value (of type `T`) written in the borrow. +- The _last_ value written in the borrow, called the **prophecy**. + +This works in the underlying logic by performing two key steps: + +- When the borrow is created, the prophecy is given a special `any` value. We don't know it yet, we will trust the logic solvers to find its actual value based on later operations. +- When dropping the borrow, Creusot adds the assumption `current == prophecy`. We call that **resolving the prophecy**. ## Final reborrows diff --git a/guide/src/model.md b/guide/src/shallow_model.md similarity index 71% rename from guide/src/model.md rename to guide/src/shallow_model.md index 2ed27256f..86070f894 100644 --- a/guide/src/model.md +++ b/guide/src/shallow_model.md @@ -1,7 +1,7 @@ -# Model +# Shallow model -You can give a custom _model_ to your type. -To do that, you just implement the `creusot_contracts::ShallowModel` trait specifying the associated type `ShallowModelTy`. It can then be accessed with the `@` operator. +You can implement the `@` operator for your type. +To do that, you just implement the `creusot_contracts::ShallowModel` trait specifying the associated type `ShallowModelTy`. For example, the following gives a spooky data type `MyPair` a nice pair model. @@ -23,3 +23,8 @@ fn my_pair(a: T, b: U) -> MyPair { MyPair(a, b) } ``` + +