verus
forked from verus-lang/verus
Star 0
Fork 0
Watch
verus source docs guide src container_bst_generic.md
3.5 kB · 83 lines
Markdown
at master

Making it generic #

In the previous sections, we devised a TreeMap<V> which used a fixed key type (u64). In this section, we'll show how 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, and to obtain 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" generically by creating a trait.

{{#include ../../../../examples/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" in the comparison function is the same as spec equality. This isn't always suitable; some datatypes may have more than 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 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.

{{#include ../../../../examples/guide/bst_map_generic.rs:structs}}

We'll also update the well-formedness condition to use the generic K::le instead of integer <=. Where the original definition used a < b, we now use a.le(b) && a != b.

{{#include ../../../../examples/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 takes 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:

Suppose 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.)

{{#include ../../../../examples/guide/bst_map_generic.rs:node_get}}

We can update insert, delete, and get_mut 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.