Reorganise sections, and improve the explanation of ShallowModel

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)

guide/src/requires_ensures.md → 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<i32>`. 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<i32>`: 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<i32>` to get a `i32`.
+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/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).
 

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 <!-- TODO: explain 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
 

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.

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<T>`, 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<T>`), so we may as well be manipulating an exact copy of the value. 
+- The interpretation of `Box<T>` 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.

guide/src/mutable_borrows.md → 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
 

guide/src/model.md → 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<T, U>` a nice pair model.
 
@@ -23,3 +23,8 @@ fn my_pair<T, U>(a: T, b: U) -> MyPair<T, U> {
     MyPair(a, b)
 }
 ```
+
+<!-- TODO:
+- Shallow model for base types
+- explain DeepModel
+ -->