docs: init first sketch

This is a first sketch of user documentation for Aeneas to prove things
with Lean.

Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>

docs/user/book.toml

@@ -4,3 +4,6 @@ language = "en"
 multilingual = false
 src = "src"
 title = "Aeneas user documentation"
+
+[output.html]
+mathjax-support = true

docs/user/src/SUMMARY.md

@@ -6,6 +6,21 @@
 
 # Proving with Lean
 
-## Tactics guide
-
-- [Progress](./lean/tactics/progress.md)
+- [Getting started]()
+- [Defining Binary Search Trees in Rust](./rust/bst_def.md)
+  - [Extracting to Lean]()
+  - [Panic-freedomness]()
+- [Specifying Invariants in Lean]()
+  - [Invariants of a binary search tree](./lean/bst/invariants.md)
+  - [Picking mathematical representations](./lean/bst/math-repr.md)
+- [Verifying `Find` Operation]()
+  - [What does it mean to be in a tree?](./lean/bst/set_of_values.md)
+  - [Dealing with Loops](./lean/bst/loops.md)
+  - [Applying Known Specifications: `progress` tactic](./lean/bst/progress.md)
+- [Verifying Insert Operation]()
+  - [Dealing with Large Proofs]()
+  - [Dealing with Symmetry]()
+- [Verifying Height Operation](./lean/bst/height.md)
+  - [Dealing with Termination Issues](./lean/bst/termination.md)
+  - [Dealing with Machine Integers: `scalar_tac` Tactic](./lean/bst/scalars.md)
+  - [Refining the Translation](./lean/bst/refining.md)

docs/user/src/lean/bst/height.md

@@ -0,0 +1 @@
+# Verifying Height Operation

docs/user/src/lean/bst/invariants.md

@@ -0,0 +1,32 @@
+# Invariants of a binary search tree
+
+The binary search tree invariant \\( \textrm{BST}(T) \\) can be defined inductively:
+
+- \\( \textrm{BST}(\emptyset) \\) where \\( \emptyset \\) is the empty binary tree
+- yadayada
+
+Mirroring this mathematical definition in the Lean theorem prover yields to an inductive predicate:
+
+```lean
+-- A helper inductive predicate over trees
+
+inductive ForallNode (p: T -> Prop): Tree T -> Prop
+| none : ForallNode p none
+| some (a: T) (left: Tree T) (right: Tree T) : ForallNode p left -> p a -> ForallNode p right -> ForallNode p (some (Node.mk a left right))
+
+--- To express inequalities between values of `T`, it is necessary to require an linear order (also known as total order) over `T`.
+variable [LinearOrder T]
+inductive Invariant: Tree T -> Prop
+| none : Invariant none
+| some (a: T) (left: Tree T) (right: Tree T) : 
+  ForallNode (fun v => v < a) left -> ForallNode (fun v => a < v) right
+  -> Invariant left -> Invariant right -> Invariant (some (Node.mk a left right))
+```
+
+Once those definitions are provided, helper theorems on `ForallNode` and `Invariant` will be useful.
+
+As exercises, consider proving the following statements:
+
+- `ForallNode.not_mem {a: T} (p: T -> Prop) (t: Option (Node T)): ¬ p a -> ForallNode p t -> a ∉ Tree.set t`: given an element \\( a \\) and a predicate \\( p \\), if \\( \lnot p(a) \\) but all the nodes in the tree \\( t \\) verifies the predicate \\( p \\), then \\( a \\) cannot be part of that tree.
+- `singleton_bst {a: T}: Invariant (some (Node.mk a none none))` : the "singleton" tree, i.e. a tree with no subtrees, is a binary search tree.
+- `left_pos {left right: Option (Node T)} {a x: T}: BST.Invariant (some (Node.mk a left right)) -> x ∈ Tree.set (Node.mk a left right) -> x < a -> x ∈ Tree.set left`, that is a sub-tree localisation theorem by comparing \\( x \\) to the root.

docs/user/src/lean/bst/loops.md

@@ -0,0 +1 @@
+# Dealing with Loops

docs/user/src/lean/bst/math-repr.md

@@ -0,0 +1,169 @@
+# Picking mathematical representations
+
+While defining binary search trees and its operations, we needed to assume that `T`, the type of elements, supported a comparison operation:
+
+```rust,noplayground
+pub enum Ordering {
+    Less,
+    Equal,
+    Greater,
+}
+
+trait Ord {
+    fn cmp(&self, other: &Self) -> Ordering;
+}
+
+impl Ord for u32 {
+    fn cmp(&self, other: &Self) -> Ordering {
+        if *self < *other {
+            Ordering::Less
+        } else if *self == *other {
+            Ordering::Equal
+        } else {
+            Ordering::Greater
+        }
+    }
+}
+```
+
+To be able to verify that the binary search tree works the way we expect, we need two ingredients:
+
+- figure out what is the mathematical representation of the order we need for the binary search tree: in the invariant section, we chose `LinearOrder T` which is a total order over `T`. It's sufficient to build a theory of *sound* binary search trees.
+
+- ensure that actual trait implementations satisfy our mathematical refinement we need for our verification: prove that the `u32` implementation of `Ord` yields to a `LinearOrder U32` in Lean.
+
+## Why is it necessary to care about `Ord` ?
+
+Consider this implementation of `Ord` for `u32`:
+
+```rust,noplayground
+impl Ord for u32 {
+    fn cmp(&self, other: &Self) -> Ordering {
+        if *self == 5924 { panic!(); }
+        
+        if *self < *other {
+            Ordering::Less
+        } else if *self == *other {
+            Ordering::Equal
+        } else {
+            Ordering::Greater
+        }
+    }
+}
+```
+
+A `u32` tree based on that implementation will not have any issue as long as we never insert `5924` in there.
+
+From this, trait implementations have load-bearing consequences on the correctness of more complicated structures such as a tree and the verification needs to take them into account to ensure a complete correctness.
+
+Furthermore, this problem can arise if the mathematical representation chosen is too ideal: that is, no trait implementation can be written such that it fulfills the mathematical representation chosen, or, **worse**, there's no such mathematical object *at all*.
+
+If a whole verification is constructed on the top of an *impossible-to-fulfill-in-practice* mathematical representation, large changes may be necessary to repair the representation.
+
+## Scalar theory in Aeneas
+
+Aeneas provides a generic `Scalar` type mirroring some of the Rust scalar theory, i.e. scalar operations such as additions and multiplications are mirrored faithfully.
+
+In Rust, scalars does not form an ideal mathematical structure, that is: `U64` is not \(( \mathbb{N} \)).
+
+Likewise, additions of `U64` is well-defined as long as the result is contained in a `U64`, which means that the addition is fallible. 
+
+In practice, Rust will panic if addition overflows unexpectedly (i.e. the code makes no use of explicit overflowing addition operators), the extraction reflects this behavior by having most operations returns a `Result (Scalar ScalarTy)` where `ScalarTy` are the word sizes, e.g. `.U32`.
+
+Nonetheless, Rust scalars do enjoy bits of mathematical structure such as linear order definitions and panic-freedomness with their default trait implementations.
+
+## A linear order over `Scalar .U32`
+
+Here, we will give an example of a `LinearOrder` definition for the Aeneas scalars:
+
+```lean
+instance ScalarU32DecidableLE : DecidableRel (· ≤ · : U32 -> U32 -> Prop) := by
+  simp [instLEScalar]
+  -- Lift this to the decidability of the Int version.
+  infer_instance
+
+instance : LinearOrder (Scalar .U32) where
+  le_antisymm := fun a b Hab Hba => by
+    apply (Scalar.eq_equiv a b).2; exact (Int.le_antisymm ((Scalar.le_equiv _ _).1 Hab) ((Scalar.le_equiv _ _).1 Hba))
+  le_total := fun a b => by
+    rcases (Int.le_total a b) with H | H 
+    left; exact (Scalar.le_equiv _ _).2 H 
+    right; exact (Scalar.le_equiv _ _).2 H
+  decidableLE := ScalarU32DecidableLE
+```
+
+This definition just exploits the fact that Aeneas' scalars can be injected in \(( \mathbb{Z} \)) and that various properties can be transferred back'n'forth via an equivalence theorem.
+
+This definition is part of the Aeneas standard library, so you usually do not have to write your own definitions.
+
+If you find a missing generic definition that could be useful in general, do not hesitate to send a pull request to the Aeneas project.
+
+## An bundling of Rust orders in Lean world
+
+Nonetheless, the previous definition is insufficient on its own, as a user can provide its own `Ord` implementation, we need to bundle a user-provided `Ord` implementation with a verification-provided `Ord` specification.
+
+Consider the following:
+
+```lean
+variable {T: Type} (H: outParam (verification.Ord T))
+
+-- Panic-freedomness of the Rust `Ord` implementation `H`
+class OrdSpec [Ord T] where
+  infallible: ∀ a b, ∃ (o: verification.Ordering), H.cmp a b = .ok o ∧ compare a b = o.toLeanOrdering
+
+-- `a ≤ b <-> b ≥ a`
+class OrdSpecSymmetry [O: Ord T] extends OrdSpec H where
+  symmetry: ∀ a b, O.compare a b = (O.opposite.compare a b).toDualOrdering
+
+-- A generalized equality specification
+class OrdSpecRel [O: Ord T] (R: outParam (T -> T -> Prop)) extends OrdSpec H where
+  equivalence: ∀ a b, H.cmp a b = .ok .Equal -> R a b
+
+-- We specialize the previous specifications to the case of the equivalence relation `=`, equality.
+class OrdSpecLinearOrderEq [O: Ord T] extends OrdSpecSymmetry H, OrdSpecRel H Eq
+```
+
+With all those pieces, we only need to prove that the extracted `OrdU32` implementation fulfills `OrdSpecLinearOrderEq` which is one of the pre-requisite to benefit from a formal verification of binary search trees over Rust `u32` scalars.
+
+Here's a solution to that proof:
+
+```lean
+instance : OrdSpecLinearOrderEq OrdU32 where
+  infallible := fun a b => by
+    unfold Ord.cmp
+    unfold OrdU32
+    unfold OrdU32.cmp
+    rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq]
+    if hlt : a < b then 
+      use .Less
+      simp [hlt]
+    else
+      if heq: a = b
+      then
+      use .Equal
+      simp [hlt]
+      rw [heq]
+      else
+        use .Greater
+        simp [hlt, heq]
+  symmetry := fun a b => by
+    rw [Ordering.toDualOrdering, LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq]
+    rw [compare, Ord.opposite]
+    simp [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq]
+    split_ifs with hab hba hba' hab' hba'' _ hba₃ _ <;> tauto
+    exact lt_irrefl _ (lt_trans hab hba)
+    rw [hba'] at hab; exact lt_irrefl _ hab
+    rw [hab'] at hba''; exact lt_irrefl _ hba''
+    -- The order is total, therefore, we have at least one case where we are comparing something.
+    cases (lt_trichotomy a b) <;> tauto
+  equivalence := fun a b => by
+    unfold Ord.cmp
+    unfold OrdU32
+    unfold OrdU32.cmp
+    simp only []
+    split_ifs <;> simp only [Result.ok.injEq, not_false_eq_true, neq_imp, IsEmpty.forall_iff]; tauto; try assumption
+```
+
+Proving panic-freedomness, symmetry and equality comes from definition unfolding and going through the Rust code which is equal to a 'canonical' definition of `compare` assuming the existence of an linear order.
+
+Therefore, we just reuse the linear order properties to finish most of those proofs once all definitions are unfolded.

docs/user/src/lean/bst/progress.md

@@ -0,0 +1 @@
+# The Progress Tactic

docs/user/src/lean/bst/refining.md

@@ -0,0 +1 @@
+# Refining the Translation

docs/user/src/lean/bst/scalars.md

@@ -0,0 +1 @@
+# Dealing with Machine Integers: scalar_tac Tactic

docs/user/src/lean/bst/set_of_values.md

@@ -0,0 +1 @@
+# What does it mean to be in a tree?

docs/user/src/lean/bst/termination.md

@@ -0,0 +1 @@
+# Dealing with Termination Issues

docs/user/src/rust/bst_def.md

@@ -0,0 +1,118 @@
+# Defining Binary Search Trees in Rust
+
+## Pre-requisites
+
+Due to Aeneas limitations, we will not use Rust standard library for the order definitions, e.g. `Ord` / `Ordering`.
+
+We will define ours and we will also take them into account in the verification:
+
+```rust,noplayground
+pub enum Ordering {
+    Less,
+    Equal,
+    Greater,
+}
+
+trait Ord {
+    fn cmp(&self, other: &Self) -> Ordering;
+}
+
+impl Ord for u32 {
+    fn cmp(&self, other: &Self) -> Ordering {
+        if *self < *other {
+            Ordering::Less
+        } else if *self == *other {
+            Ordering::Equal
+        } else {
+            Ordering::Greater
+        }
+    }
+}
+```
+
+We will revisit those definitions in the chapter about mathematical representations because we will need to decide what extra properties we want to impose on an `Ord` as Rust allows many degenerate implementations of an order which will not lead to a working binary search tree.
+
+## Data structure
+
+We define trees in Rust following borrow checker constraints, e.g. a `Box` indirection is required.
+
+```rust,noplayground
+struct Node<T> {
+   value: T,
+   left: Option<Box<Node<T>>,
+   right: Option<Box<Node<T>>
+}
+
+type Tree<T> = Option<Box<Node<T>>>;
+```
+
+**Note**: `Box` is erased during translation, i.e. in Lean, no details about `Box` will be available.
+
+**Note 2** : We do not ask for `T` to have `Ord`, we will put this trait bound on the functions in the next section.
+
+## Operations on trees
+
+We will define two operations for this guide:
+
+- `height`, defined by: $$\textrm{height}(t) = 1 + \textrm{max}(\textrm{height}(t.\textrm{left}), \textrm{height}(t.\textrm{right}))$$
+- `insert` which inserts an item inside the binary search tree
+
+**Note** : Due to Aeneas limitations, we sometimes have to rewrite the code in a way that will be possible to extract to Lean, those situations are documented with a comment to explain why it is necessary.
+
+## `insert`
+
+We will need to define a container for our tree to hold our root:
+
+```rust,noplayground
+struct TreeSet<T> {
+   root: Tree<T>
+}
+
+impl<T: Ord> TreeSet<T> {
+    pub fn new() -> Self {
+        Self { root: None }
+    }
+
+    pub fn insert(&mut self, value: T) -> bool {
+        let mut current_tree = &mut self.root;
+
+        while let Some(current_node) = current_tree {
+            match current_node.value.cmp(&value) {
+                Ordering::Less => current_tree = &mut current_node.right,
+                Ordering::Equal => return false,
+                Ordering::Greater => current_tree = &mut current_node.left,
+            }
+        }
+
+        *current_tree = Some(Box::new(Node {
+            value,
+            left: None,
+            right: None,
+        }));
+
+        true
+    }
+}
+```
+
+`insert` returns whether the item was already in or not and mutates in-place the tree.
+
+## `find`
+
+```rust,noplayground
+    pub fn find(&self, value: T) -> bool {
+        let mut current_tree = &self.root;
+
+        while let Some(current_node) = current_tree {
+            match current_node.value.cmp(&value) {
+                Ordering::Less => current_tree = &current_node.right,
+                Ordering::Equal => return true,
+                Ordering::Greater => current_tree = &current_node.left,
+            }
+        }
+
+        false
+    }
+```
+
+We return whether we find the item or not in the tree by browsing it using the binary search tree invariant.