Merge pull request #975 from arnaudgolfouse/guide

Guide with mdbook

.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

README.md

@@ -80,135 +80,12 @@ 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](https://creusot-rs.github.io/creusot/).
 
-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<T, U>` a nice pair model.
-```rust
-impl<T, U> Model for MyPair<T, U> {
-    type Target = (T, U);
-}
-#[trusted]
-#[ensures(@result == (a, b))]
-fn my_pair<T, U>(a: T, b: U) -> MyPair<T, U> {
-  ...
-}
-```
+See [HACKING.md](HACKING.md) for information on the developer workflow for
+hacking on the Creusot codebase.

guide/src/SUMMARY.md

@@ -1,3 +1,17 @@
 # Summary
 
 - [Quickstart](./quickstart.md)
+- [Basic concepts](./basic_concepts.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)
+- [Type invariants](./type_invariants.md)

guide/src/basic_concepts.md

@@ -0,0 +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.

guide/src/basic_concepts/invariants.md

@@ -0,0 +1,14 @@
+# Invariants
+
+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 ... { ... }
+```
+
+<!-- TODO: Better documentation on `#[invariant]`:
+
+- precise syntax (mention pearlite)
+- meaning
+- common patterns, examples -->

guide/src/basic_concepts/proof_assert.md

@@ -0,0 +1,6 @@
+# `proof_assert!`
+
+TODO:
+
+- Syntax
+- usage

guide/src/basic_concepts/requires_ensures.md

@@ -0,0 +1,46 @@
+# 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]
+}
+```
+
+Note the **shallow model** (`@`) operator: it is needed to convert the Rust type `&[i32]` to a logical type `Seq<i32>`. Else, we could not call `[T]::len`, which is a program function (and not a logical one).
+
+To learn more, see the chapter on [Pearlite](../pearlite.md) and [ShallowModel](../shallow_model.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:
+- use the `@` operator on the slice to get a `Seq<i32>`
+- we can then index this `Seq<i32>` to get a `i32`.

guide/src/basic_concepts/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.
+
+<!-- TODO: be more precise:
+- where exactly is `variant` allowed ?
+- At least one example -->

guide/src/logic_functions.md

@@ -0,0 +1,72 @@
+# Logic functions
+
+We 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.
+- 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 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).
+
+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<i32>) -> bool {
+    pearlite! {
+        forall<i: Int> i >= 0 && i < s.len() ==> s[i]@ == 1
+    }
+}
+
+#[ensures(all_ones(result@))]
+#[ensures(result@.len() == n@)]
+pub fn make_ones(n: usize) -> Vec<i32> {
+    creusot_contracts::vec![1; n]
+}
+```
+
+Recursion:
+
+```rust
+TODO
+```
+
+Prophetic:
+
+```rust
+TODO
+```
+
+<!-- TODO: Explain `#[open(...)]` -->

guide/src/pearlite.md

@@ -0,0 +1,35 @@
+# Pearlite
+
+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 <!-- TODO: explain labels -->
+- 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
+
+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: Int> i >= 0 && i < list@.len() ==> list@[i] == 0)]
+fn requires_all_zeros(list: &[i32]) {
+    // ...
+}
+```