Sequential Specs

Range

Consider the following stub
class Range {
private:
    unsigned long _begin;
    size_t _size;
    ...
};

of a Range class in C++ implementing contiguous address sets as intervals. To write specs for C++ functions that operate on Ranges, we: (1) Implement a Coq model of the Range class; (2) Write a representation predicate that connects Coq Ranges to the representation of C++ Ranges in memory.

Coq Model of Range

Let's consider the Coq model first. We build it as a Coq Record with two fields, begin and size, corresponding the the fields of the C++ struct. In our model, we represent both values as Z; our representation predicate will impose additional nonnegativity constraints.

An example Range, the interval (inclusive 10, 13), is built as:

To extract the begin and size of a Range like range_ex, one can use projections corresponding to the fields: Compute range_ex.(begin). = 10 : Z Compute range_ex.(size). = 3 : Z

Range: Representation Predicate

Now let's write the representation predicate. It will refer to the _begin and _size fields of the C++ struct, which are autogenerated by cpp2v as:

Here's the first version, which follows the style discussed in the first chapter. It's a Definition in Coq that takes two parameters, the fractional permission q (which could be 1, indicating write permission), and r : Range, the Coq model of the range.

RangeR3 is a function (predicate), which when applied to a start address ("this"), will assert the memory representation starting at that address. This function nature can be made explicit using as_Rep, which gives us explicit access to the this pointer as a function argument.

To make thigs even more explicit, we can distribute the this |-> over the **:

this |-> (_begin |-> ulongR q r.(begin))

means "at the address this + offset_of(_begin)", there's an unsigned integer r.(begin) held with permission q. Access to the "this" pointer is usually not necessary and only adds verbosity. However, at some places, e.g. in doubly linked lists, it is necessary: for example, the next node of a doubly linked list stores the "this" pointer in its prev field.

Binary Search Trees

In this section, we implement the representation predicate for binary search trees corresponding to the following C++ struct:
template <typename T = int>
struct Tree {
  T _data;
  Tree<T>* _left;
  Tree<T>* _right;
};

Unsorted Binary Trees

Following our recipe, we first define a Coq model of (unsorted) trees:

leaf is the empty tree. node d l r is the tree node containing data d, left subtree l and right subtree r. tree is polymorphic; it contains data d of type A for any type A. Below, we'll instantiate tree to A := Z and to other types. For example, here's the tree with root 3, left child 1, and right child 5.

We can define pure Coq functions on tree for use in specs. For example, in_tree x t is the proposition that reads "tree x contains key t". It's defined by recursion on t. A leaf never contains a key (represented by False). Key x is in_tree node y l r when: (1) x = y; or (2) x is in the left subtree l; or (3) x is in the right subtree r.

Now we define the representation predicate treeR for trees. treeR is parameterized inside a Section by: (1) A : Type, the type of data stored in the trees; and (2) R : Qp -> A -> Rep, a representation predicate for A. We'll use R to define how that data stored in the tree is represented in memory.

The treeR predicate is defined by recursion on the Coq tree t. Leaves are represented by the nullptr, which we write as:
[| this = nullptr |]

When the tree is a node d l r, we assert that field _data contains R q d (representation of d with permission q) and that there exist pointers lp and rp stored at the _left and _right fields. We separately assert that: (1) At lp, there's a treeR q l, memory implementing the left subtree; and (2) At rp, there's a treeR q r, memory implementing the right subtree.

Sorted Binary Trees

To build sorted trees from unsorted ones, we define a Coq predicate, sorted t. A leaf is always sorted. A node d l r when l is sorted, r is sorted, all the values in l are less than d, and all the values in r are greater than d. This definition additionally implies that the tree contains no duplicate keys.

The representation predicate ZbstR q t uses sorted to lift treeR to sorted trees of Zs.

(fun q z => uintR q z) instantiates treeR's parameter R to the representation predicate of unsigned integers.

Count

count is a Coq function that computes the number of nodes in a Coq tree.

= 0 : Z Compute count ex_tree. = 3 : Z count_spec uses Coq count to specify a C++ function that counts the number of nodes in a BST:
unsigned int Tree::count() const;

For more details the syntax/notations for writing the specifications of functions, please refer to cpp2v/doc/specs.md. We trim the count in the postcondition since it might overflow. Alternatively, we could impose a bounds condition in the precondition:
  \pre [| bound W64 Unsigned (count t) |]

count doesn't require that t be sorted so the prepost uses just treeR, not ZbstR.

Insert

Here's the spec for a function that inserts a key into a tree:
bool Tree::insert(int);

On duplicate keys, insert does nothing (we treat the tree as a set rather than a multiset).

More intensionally, we could write this spec using a Coq implementation of insert:

EXERCISE: Linked Lists

FILL_IN in the representation predicate for linked lists, represented in Coq by the datatype llist and in C++ by the struct:
struct List {
  int _data;
  List* next;
};

The empty linked list is represented by nullptr.

Range Maps

Here's a Coq model and representation predicate for "Range Maps", binary trees of Entries that associate ranges of addresses to payloads.
  template<typename T>
  struct Entry {
    Range _range;
    T _payload;
  };

  template<typename T>
  using EntryTree = Tree<Entry<T>>;

The Coq model of an Entry tracks Ranges and payloads of type T.

Here's the corresponding representation predicate:

One range is less than another if its begin value is less-than.

Entries are less-than when their Ranges are less-than.

A tree of Entries is sorted if the Entries are sorted by Entry_lt.

The representation predicate of an Entry BST:

Putting the pieces together, here's the function spec for lookup, which maps an address x in a trees of Entries to the corresponding Entry, if any.

borrow_from all borrow, which is used in lookup_spec below, encapsulates a pattern for "borrowing" the resources borrow from a larger world all. With borrow_from you get access to two disjoint resources: (1) You have access to borrow; and (2) If you give up borrow, you get back all.

Using borrow, we can write the specification for lookup:

The postcondition is keyed on the Boolean result r, with r=true indicating a successful lookup.

A pointer to the looked-up entry is passed in the out parameter out.

We also return a "borrow" from the Entry_bstR q t, the fact that at p there's an EntryR q e with a matching Range.

When r=false, we assert that there was no payload p corresponding to the looked-up value x.

(Note: This spec allows the implementation to change the out parameter arbitrarily in the error case.)