add guide chapter on Binary Search Tree

illustrates various aspects of modularity / building a container data structure

 - view
 - well_formed() / type_invariants
 - genericity using traits
 - implementing Clone generically

source/docs/guide/src/SUMMARY.md

@@ -82,6 +82,13 @@
   - [Pointers](./pointers.md)
   - [Concurrency](concurrency.md)
 
+- [Verifying a container library: Binary Search Tree](./container_bst.md)
+  - [First draft](./container_bst_first_draft.md)
+  - [Encapsulating well-formedness with type invariants](./container_bst_type_invariant.md)
+  - [Making it generic](./container_bst_generic.md)
+  - [Implementing `Clone`](./container_bst_clone.md)
+  - [Full source for examples](./container_bst_all_source.md)
+
 - [Understanding the guarantees of a verified program](./guarantees.md)
   - [Assumptions and trusted components](./tcb.md)
   - [Memory safety is conditional on verification](./memory-safety.md)

source/docs/guide/src/container_bst.md

@@ -0,0 +1,7 @@
+# Verifying a container library
+
+In this section, we'll learn how to verify a simple container library, specifically,
+via an example of a _map_ data structure using a binary search tree.
+In the case study, we'll explore various considerations for
+writing a modular specification
+that encapsulates verfication details as well as implementation details.

source/docs/guide/src/container_bst_all_source.md

@@ -0,0 +1,23 @@
+# Full source for examples
+
+ * [First draft](#first-draft)
+ * [Version with type invariants](#version-with-type-invariants)
+ * [Version with generic key type and Clone implementation](#version-with-generic-key-type-and-clone-implementation)
+
+## First draft
+
+```rust
+{{#include ../../../rust_verify/example/guide/bst_map.rs:all}}
+```
+
+## Version with type invariants
+
+```rust
+{{#include ../../../rust_verify/example/guide/bst_map_type_invariant.rs:all}}
+```
+
+## Version with generic key type and Clone implementation
+
+```rust
+{{#include ../../../rust_verify/example/guide/bst_map_generic.rs:all}}
+```

source/docs/guide/src/container_bst_clone.md

@@ -0,0 +1,109 @@
+# Implementing Clone
+
+As a finishing touch, let's implement `Clone` for `TreeMap<K, V>`.
+The main trick here will be in figuring out the correct specification for `TreeMap::<K, V>::Clone`.
+
+Naturally, such an implementation will require both `K: Clone` and `V: Clone`.
+However, to write a sensible clone implementation for the tree, we have to consider
+what the implementations of `K::clone` and `V::clone` actually do.
+
+Generally speaking, Verus imposes no constraints on the implementations of the `Clone`,
+so it is not necessarily true that a `clone()` call will return a value that is spec-equal
+to its inputs.
+
+With this in mind, we're going to prove the following signature for `TreeMap<K, V>::clone`:
+
+```rust
+{{#include ../../../rust_verify/example/guide/bst_map_generic.rs:clone_signature}}
+    {
+        ...
+    }
+}
+```
+
+### Dealing with `K::clone`
+
+In order to clone all the keys, we need `K::clone` to respect the ordering of elements; otherwise,
+we'd need to resort all the keys on clone in order for the resulting tree to be valid.
+However, it's not likely that is desirable behavior. If `Clone` doesn't respect the
+`TotalOrdered` implementation, it's likely a user bug.
+
+A general way to handle this would be to require that `Clone` actually be compatible
+with the total-ordering in some sense.
+However, you'll
+recall from the previous section that we're already simplifying the "total ordered" specification
+a bit. Likewise, we're going to continue to keep things simple here by also requiring
+that `K: Copy`.
+
+As a result, we'll be able to prove that our `TreeMap` clone implementation can preserve
+all keys exactly, even when compared via spec equality. That is, we'll be able to
+ensure that `[email protected]() =~= [email protected]()`.
+
+### Dealing with `V::clone`
+
+So what about `V`? Again, we don't know _a priori_ what `V::clone` does. It might return
+values unequal to the imput; it might even be nondeterminstic. Therefore,
+a cloned `TreeMap` may have different values than the original.
+
+In order to specify `TreeMap::<K, V>::clone` as generically as possible, we choose
+to write its ensures clause _in terms of_ the ensures clause for `V::clone`.
+This can be done using `[`call_ensures`](./exec_funs_as_values.md)`.
+The predicate `call_ensures(V::clone, (&self@[key],), res@[key])` effectively says
+"`self@[key]` and `res@[key]` are a possible input-output pair for `V::clone`".
+
+### Understanding the implications of the signature
+
+Let's do a few examples.
+
+First, consider cloning a `TreeMap::<u64, u32>`. The Verus standard library provides
+a specification for `u32::clone`; it's the same as a copy, i.e., a cloned `u32` always
+equals the input. As a result, we can deduce that cloning a `TreeMap::<u64, u32>` will
+preserve its `view` exactly. We can prove this using [extensional equality](./extensional_equality.md).
+
+```rust
+{{#include ../../../rust_verify/example/guide/bst_map_generic.rs:clone_u32}}
+```
+
+We can do the same for _any_ type where `clone` guarantees spec-equality. Here's another
+example with a user-defined type.
+
+```rust
+{{#include ../../../rust_verify/example/guide/bst_map_generic.rs:clone_int_wrapper}}
+```
+
+This works because of the postcondition on `IntWrapper::clone`, that is, `ensures *s == self`.
+If you're new to this style, it might seem initially surprising that 
+`IntWrapper::clone` has any effect on the verification of `test_clone_int_wrapper`, since
+it doesn't directly call `IntWrapper::clone`. In this case, the postcondition is referenced
+indirectly via `TreeMap<u64, IntWrapper>:clone`.
+
+Let's do one more example, this time with a _less_ precise clone function.
+
+```rust
+{{#include ../../../rust_verify/example/guide/bst_map_generic.rs:clone_weird_int}}
+```
+
+This example is a bit pathological; our struct, `WeirdInt`, has an extra field that doesn't
+get cloned. You could imagine real-life scenarios that have this property (for example,
+if every struct needs to have a unique identifier). Anyway, the postcondition of
+`WeirdInt::clone` doesn't say both objects are equal, only that the `int_value` fields are equal.
+This postcondition can then be inferred for each value in the map, as shown.
+
+### Implementing `TreeMap::<K, V>::Clone`.
+
+As usual, we write the implementation as a recursive function.
+
+It's not necessary to implement `Node::Clone`; one could instead just implement a normal
+recursive function as a helper for `TreeMap::Clone`; but it's more Rust-idiomatic to do it
+this way. This lets us call `Option<Node<K, V>>::Clone`
+in the implementation of `TreeMap::clone` (the spec for `Option::clone` is provided by
+vstd). However, you can see that there are a few 'gotchas' that need
+to be worked around.
+
+```rust
+{{#include ../../../rust_verify/example/guide/bst_map_generic.rs:clone_full_impl}}
+```
+
+## Full source
+
+The full source for this example can be found [here](./container_bst_all_source.md#version-with-generic-key-type-and-clone-implementation).

source/docs/guide/src/container_bst_first_draft.md

@@ -0,0 +1,148 @@
+# A simple binary search tree
+
+In this section, we're going to be implementing and verifying a Binary Search Tree (BST).
+
+In the study of data structures, there are
+[many](https://en.wikipedia.org/wiki/Red%E2%80%93black_tree)
+[known](https://en.wikipedia.org/wiki/AVL_tree)
+[ways](https://en.wikipedia.org/wiki/Treap)
+[to](https://en.wikipedia.org/wiki/Splay_tree)
+[balance](https://en.wikipedia.org/wiki/B-tree)
+a binary search tree.
+To keep things simple, we won't be implementing of them—instead,
+we'll be implemented a straightforward,
+_unbalanced_ binary search tree. Improving the design to be more efficient will be left
+as an exercise.
+
+Furthermore, our first draft of an implementation is going to be mapping keys
+of the fixed orderable type, `u64`, to values of type `V`. In a later chapter,
+we'll change the keys to also be generic, thus mapping `K` to `V` for arbitrary types
+`K` and `V`.
+
+## The implementation
+
+### The structs
+
+We'll start by defining the tree shape itself, which contains one (key, value) pair at every
+node. We make no distinction between "leaf nodes" and "interior nodes". Rather, every node
+has an optional left child and an optional right child.
+Furthermore, the tree might be entirely empty, in which case there is no root.
+
+```rust
+{{#include ../../../rust_verify/example/guide/bst_map.rs:StructsDef}}
+```
+
+Note that only `TreeMap` is marked `pub`. Its field, `root`, as well as the `Node` type
+as a whole, are implementation details, thus private to the module.
+
+### The abstract view
+
+When creating a new data structure, there are usually two things to do first:
+
+ * Establish an interpretation of the data structure as some abstract datatype that will
+   be used to write specifications.
+ * Establish the well-formedness invariants of the data structure.
+
+We'll do the first one first (in part because it will actually help with the second).
+In this case, we want to interpret the data structure as a
+[`Map<u64, V>`](https://verus-lang.github.io/verus/verusdoc/vstd/map/struct.Map.html).
+We can define such a function recursively.
+
+```rust
+{{#include ../../../rust_verify/example/guide/bst_map.rs:AsMapDef}}
+```
+
+Again note that only `Tree::as_map` is marked `pub`, and furthermore, that it's marked
+`closed`. The definition of `as_map` is, again, an implementation detail.
+
+It is customary to also implement the
+[`View` trait](https://verus-lang.github.io/verus/verusdoc/vstd/view/trait.View.html)
+as a convenience. This lets client refer to the map implementation using the `@` notation,
+e.g., `tree_map@` as a shorthand for `tree_map.view()`.
+We'll be writing our specifications in terms of `tree_map.view()`.
+
+```rust
+{{#include ../../../rust_verify/example/guide/bst_map.rs:ViewDef}}
+```
+
+### Establishing well-formedness
+
+Next we establish well-formedness. This amounts to upholding the BST ordering property,
+namely, that for every node _N_, the nodes in _N_'s left subtree have keys less than
+_N_, while the nodes in _N_'s right subtree have keys greater than _N_.
+Again, this can be defined by a recursive `spec` function.
+
+```rust
+{{#include ../../../rust_verify/example/guide/bst_map.rs:WellFormedDef}}
+```
+
+### Implementing a constructor: `TreeMap::new()`
+
+Defining a constructor is simple; we create an empty tree with no root.
+The specification indicates that the returned object must represent the _empty_ map.
+
+```rust
+{{#include ../../../rust_verify/example/guide/bst_map.rs:new}}
+```
+
+Recall that `tree_map@` is equivalent to `tree_map.as_map()`.
+An inspection the definition of `tree_map.as_map()` and `Node::optional_as_map()` should
+make it apparent this will be the empty set when `root` is `None`.
+
+Observe again that this specification does not refer to the tree internals at all,
+only that it is well-formed and that its abstract view is the empty map.
+
+### Implementing the `insert` operation
+
+We can also implement `insert` using a recursive traversal. We search for the given node,
+using the well-formedness conditions to prove that we're doing the right thing.
+During this traversal, we'll either find a node with the right key, in which case we update
+the `value`, or we'll reach a leaf without ever finding the desired node, in which case we
+create a new node.
+
+(Aside: One slight snag has to do with a limitation of Verus's handing of mutable references.
+Specifically, Verus doesn't yet support an easy to get a
+`&mut T` out of a `&mut Option<T>`. To get around this, we use [`std::mem::swap`](https://doc.rust-lang.org/std/mem/fn.swap.html) to get ownership of the node.)
+
+```rust
+{{#include ../../../rust_verify/example/guide/bst_map.rs:insert}}
+```
+
+Observe that the specification of `TreeMap::insert` can be given in terms of
+[`Map::insert`](https://verus-lang.github.io/verus/verusdoc/vstd/map/struct.Map.html#method.remove).
+
+### Implementing the `delete` operation
+
+Implementing `delete` is a little harder, because if we need to remove an interior node,
+we might have to reshape the tree a bit. However, since we aren't trying to follow
+any particular balancing strategy, it's still not that bad:
+
+```rust
+{{#include ../../../rust_verify/example/guide/bst_map.rs:delete}}
+```
+
+Observe that the specification of `TreeMap::delete` can be given in terms of
+[`Map::remove`](https://verus-lang.github.io/verus/verusdoc/vstd/map/struct.Map.html#method.remove).
+
+### Implementing the `get` operation
+
+Finally, we implement and verify `TreeMap::get`.
+This function looks up a key and returns an `Option<&V>` (`None` if the key isn't in the
+`TreeMap`).
+
+```rust
+{{#include ../../../rust_verify/example/guide/bst_map.rs:get}}
+```
+
+### Using the `TreeMap` as a client
+
+A short client program illustrates how we can reason about the `TreeMap` as if it were
+a [`Map`](https://verus-lang.github.io/verus/verusdoc/vstd/map/struct.Map.html).
+
+```rust
+{{#include ../../../rust_verify/example/guide/bst_map.rs:test}}
+```
+
+## Full source
+
+The full source for this example can be found [here](./container_bst_all_source.md#first-draft).

source/docs/guide/src/container_bst_generic.md

@@ -0,0 +1,83 @@
+# Making it generic
+
+In the previous sections, we devised a `TreeMap<V>` which a fixed key type (`u64`).
+In this section, we'll show to make a `TreeMap<K, V>` which is generic over the key type `K`.
+
+## Defining a "total order"
+
+The main reason this is challenging is that the BST requires a way of _comparing_
+values of `K`, both for equality, for obtaining an ordering. This comparison is used both
+in the implementation (to find the node for a given key, or to figure out where such
+a node should be inserted) and in the well-formedness invariants that enforce
+the BST ordering property.
+
+We can define the concept of ["total order"](https://en.wikipedia.org/wiki/Total_order)
+generically by creating a trait.
+
+```rust
+{{#include ../../../rust_verify/example/guide/bst_map_generic.rs:trait}}
+```
+
+This trait simultaneously:
+
+ * Requires a binary relation `le` to exist
+ * Requires it to satisfy the properties of a total order
+ * Requires an `executable` three-way comparison function to exist
+
+There's one simplification we've made here: we're assuming that "equality" is the comparison
+function is the same as [spec equality](./equality.md).
+This isn't always suitable; some datatypes may have more that one way to represent the same
+logical value. A more general specification would allow an ordering that respects
+some arbitrary equivalence relation.
+This is how [`vstd::hash_map::HashMapWithView`](https://verus-lang.github.io/verus/verusdoc/vstd/hash_map/struct.HashMapWithView.html) works, for example.
+To keep things simple for this demonstration, though, we'll use a total ordering that respects
+spec equality.
+
+### Updating the struct and definitions
+
+We'll start by updating the structs to take a generic parameter `K: TotalOrdered`.
+
+```rust
+{{#include ../../../rust_verify/example/guide/bst_map_generic.rs:structs}}
+```
+
+We'll also update the well-formedness condition use the generic `K::le` instead of integer `<=`.
+Where the original definition used `a < b`, we now use `a.le(b) && a != b`.
+
+```rust
+{{#include ../../../rust_verify/example/guide/bst_map_generic.rs:well_formed}}
+```
+
+Meanwhile, the definition of `as_map` doesn't rely on the ordering function,
+so it can be left alone, the same as before.
+
+### Updating the implementations and proofs
+
+Updating the implementations take a bit more work, since we need more substantial proof code.
+Whereas Verus has good automation for integer inequalities (`<`), it has no such automation
+for our new, hand-made `TotalOrdered` trait. Thus, we need to add proof code to invoke
+its properties manually.
+
+Let's take a look at `Node::get`.
+
+The meat of the proof roughly goes as follows:
+
+Supoose we're looking for the key `key` which compares less than `self.key`.
+Then we need to show that recursing into the left subtree gives the correct answer; for this,
+it suffices to show that `key` is _not_ in the right subtree.
+
+Suppose (for contradiction) that `key` _were_ in the right subtree.
+Then (by the well-formedness invariant), we must have `key > self.key`.
+But we already established that `key < self.key`. Contradiction.
+(Formally, this contradiction can be obtained by invoking antisymmetry.)
+
+```rust
+{{#include ../../../rust_verify/example/guide/bst_map_generic.rs:node_get}}
+```
+
+We can update `insert` and `delete` similarly, manually inserting lemma calls to invoke
+the total-ordering properties where necessary.
+
+## Full source
+
+The full source for this example can be found [here](./container_bst_all_source.md#version-with-generic-key-type-and-clone-implementation).