CN tutorial

For a first example, let’s look at a simple arithmetic function: add, shown below, takes two int arguments, x and y, and returns their sum.

Running CN on the example produces an error message:

CN rejects the program because it has C undefined behaviour, meaning it is not safe to execute. CN points to the relevant source location, the addition x+y, and paragraph §6.5#5 of the C language standard that specifies the undefined behaviour. It also puts a link to an HTML file with more details on the error to help in diagnosing the problem.

Inspecting this HTML report (as we do in a moment) gives us possible example values for x and y that cause the undefined behaviour and hint at the problem: for very large values for x and y, such as 1073741825 and 1073741824, the sum of x and y can exceed the representable range of a C int value: 1073741825 + 1073741824 = 2^31+1, so their sum is larger than the maximal int value, 2^31-1.

Here x and y are signed integers, and in C, signed integer overflow is undefined behaviour (UB). Hence, add is only safe to execute for smaller values. Similarly, large negative values of x and y can cause signed integer underflow, also UB in C. We therefore need to rule out too large values for x and y, both positive and negative, which we do by writing a CN function specification.

Shown below is our first function specification, for add, with a precondition that constrains x and y such that the sum of x and y lies between -2147483648 and 2147483647, so within the representable range of a C int value.

In detail:

Running CN on the annotated program passes without errors. This means with our specified precondition, add is safe to execute.

We may, however, wish to be more precise. So far the specification gives no information to callers of add about its output. To also specify the return values we add a postcondition, using the ensures keyword.

Here we use the keyword return, only available in function postconditions, to refer to the return value, and equate it to sum as defined in the preconditions, cast back to i32 type: add returns the sum of x and y.

Running CN confirms that this postcondition also holds.

One final refinement of this example. CN defines constant functions MINi32, MAXi64, etc. so that specifications do not need to be littered with unreadable numeric constants.

Two things to note: * These are constant functions, so they require a following (). * The type of MINi32() is i32, so if we want to use it as a 64-bit constant we need to add the explicit coercion (i64).

In the original example CN reported a type error due to C undefined behaviour. While that example was perhaps simple enough to guess the problem and solution, this can become quite challenging as program and specification complexity increases. Diagnosing type errors is therefore an important part of using CN. CN tries to help with that by producing detailed error information, in the form of an HTML error report.

Let’s return to the type error from earlier (add without precondition) and take a closer look at this report. The report comprises two sections.

Path. The first section, “Path to error”, contains information about the control-flow path leading to the error.

When type checking a C function, CN checks each possible control-flow path through the program individually. If CN detects UB or a violation of user-defined specifications, CN reports the problematic control-flow path, as a nested structure of statements: paths are split into sections, which group together statements between high-level control-flow positions (e.g. function entry, the start of a loop, the invocation of a continue, break, or return statement, etc.); within each section, statements are listed by source code location; finally, per statement, CN lists the typechecked sub-expressions, and the memory accesses and function calls within these.

In our example, there is only one possible control-flow path: entering the function body (section “function body”) and executing the block from lines 2 to 4, followed by the return statement at line 3. The entry for the latter contains the sequence of sub-expressions in the return statement, including reads of the variables x and y.

In C, local variables in a function, including its arguments, are mutable and their address can be taken and passed as a value. CN therefore represents local variables as memory allocations that are manipulated using memory reads and writes. Here, type checking the return statement includes checking memory reads for x and y, at their locations &ARG0 and &ARG1. The path report lists these reads and their return values: the read at &ARG0 returns x (that is, the value of x originally passed to add); the read at &ARG1 returns y. Alongside this symbolic information, CN displays concrete values:

For now, ignore the pointer values {@0; 4} for x and {@0; 0} for y.

These concrete values are part of a counterexample: a concrete valuation of variables and pointers in the program that that leads to the error. (The exact values may vary on your machine, depending on the version of Z3 installed on your system.)

Proof context. The second section, below the error trace, lists the proof context CN has reached along this control-flow path.

“Available resources” lists the owned resources, as discussed in later sections.

“Variables” lists counterexample values for program variables and pointers. In addition to x and y, assigned the same values as above, this includes values for their memory locations &ARG0 and &ARG1, function pointers in scope, and the __cn_alloc_history, all of which we ignore for now.

Finally, “Constraints” records all logical facts CN has learned along the path. This includes user-specified assumptions from preconditions or loop invariants, value ranges inferred from the C-types of variables, and facts learned during the type checking of the statements. Here (add without precondition) the only constraints are some contraints inferred from C-types in the code.

Let’s apply what we know so far to another simple arithmetic example.

The function doubled, shown below, takes an int n, defines a as n incremented, b as n decremented, and returns the sum of the two.

We would like to verify this is safe, and that doubled returns twice the value of n. Running CN on doubled leads to a type error: the increment of a has undefined behaviour.

As in the first example, we need to ensure that n+1 does not overflow and n-1 does not underflow. Similarly also a+b has to be representable at int type.

We can specify these using a similar style of precondition as in the first example. We first define n_ as n cast to type i64 — i.e. a type large enough to hold n+1, n-1 and a+b for any possible i32 value for n. Then we specify that decrementing n_ does not go below the minimal int value, that incrementing n_ does not go above the maximal value, and that n doubled is also in range. These preconditions together guarantee safe execution.

To capture the functional behaviour, the postcondition specifies that return is twice the value of n.

Quadruple. Specify the precondition needed to ensure safety of the C function quadruple, and a postcondition that describes its return value.

Abs. Give a specification to the C function abs, which computes the absolute value of a given int value. To describe the return value, use CN’s ternary “_ ? _ : _” operator. Given a boolean b, and expressions e1 and e2 of the same basetype, b ? e1 : e2 returns e1 if b holds and e2 otherwise.

Given a C-type T and pointer p, the resource Owned<T>(p) asserts ownership of a memory cell at location p of the size of C-type T. It is CN’s equivalent of a points-to assertion in separation logic (indexed by C-types T).

In this example we can ensure the safe execution of read by adding a precondition that requires ownership of Owned<int>(p), as shown below. For now ignore the notation take ... = Owned<int>(p). Since read maintains this ownership, we also add a corresponding postcondition, whereby read returns ownership of p after it is finished executing, in the form of another Owned<int>(p) resource.

This specifications means that

However, a caller of read may also wish to know that read actually returns the correct value, the pointee of p, and also that it does not change memory at location p. To phrase both we need a way to refer to the pointee of p.

In CN resources have outputs. Each resource outputs the information that can be derived from ownership of the resource. What information is returned is specific to the type of resource. A resource Owned<T>(p) (for some C-type T) outputs the pointee value of p, since that can be derived from the resource ownership: assume you have a pointer p and the associated ownership, then this uniquely determines the pointee value of p.

CN uses the take-notation seen in the example above to refer to the output of a resource, introducing a new name binding for the output. The precondition take v1 = Owned<int>(p) from the precondition does two things: (1) it assert ownership of resource Owned<int>(p), and (2) it binds the name v1 to the resource output, here the pointee value of p at the start of the function. Similarly, the postcondition introduces the name v2 for the pointee value on function return.

That means we can use the resource outputs from the pre- and postcondition to strengthen the specification of read as planned. We add two new postconditions: we specify

Aside. In standard separation logic the equivalent specification for read could have been phrased as follows (where return binds the return value in the postcondition):

CN’s take notation is just alternative syntax for quantification over the values of resources, but a useful one: the take notation syntactically restricts how these quantifiers can be used to ensure CN can always infer them.

Quadruple. Specify the function quadruple_mem, that is similar to the earlier quadruple function, except that the input is passed as an int pointer. Write a specification that takes ownership of this pointer on entry and returns this ownership on exit, leaving the pointee value unchanged.

Abs. Give a specification to the function abs_mem, which computes the absolute value of a number passed as an int pointer.

In the specifications we have written so far, functions that receive resources as part of their precondition also return this ownership in their postcondition.

Let’s try the read example from earlier again, but with a postcondition that does not return the ownership:

CN rejects this program with the following message:

CN has typechecked the function, verified that it is safe to execute under the precondition (given ownership Owned<int>(p)), and that the function (vacuously) satisfies its postcondition. But, following the check of the postcondition it finds that not all resources have been “used up”.

Given the above specification, read leaks memory: it takes ownership, does not return it, but also does not deallocate the owned memory or otherwise dispose of it. In CN this is a type error.

CN’s resource types are linear (as opposed to affine). This means not only that resources cannot be duplicated, but also that resources cannot simply be dropped or “forgotten”. Every resource passed into a function has to either be used up by it, by returning it or passing it to another function that consumes it, or destroyed, by deallocating the owned area of memory (as we shall see later).

CN’s motivation for linear tracking of resources is its focus on low-level systems software. CN checks C programs, in which, unlike higher-level garbage-collected languages, memory is managed manually, and memory leaks are typically very undesirable.

As a consequence, function specifications have to do precise “book-keeping” of their resource footprint, and, in particular, return any unused resources back to the caller.

Aside from the Owned resource seen so far, CN has another built-in resource type: Block. Given a C-type T and pointer p, Block<T>(p) asserts the same ownership as Owned<T>(p) — so ownership of a memory cell at p the size of type T — but in contrast to Owned, Block memory is not necessarily initialised.

CN uses this distinction to prevent reads from uninitialised memory:

Since Owned carries the same ownership as Block, just with the additional information that the Owned memory is initalised, a resource Owned<T>(p) is “at least as good” as Block<T>(p) — an Owned<T>(p) resource can be used whenever Block<T>(p) is needed. For instance CN’s type checking of a write to p requires a Block<T>(p), but if an Owned<T>(p) resource is what is available, this can be used just the same. This allows an already-initialised memory cell to be over-written again.

Unlike Owned, whose output is the pointee value, Block has no meaningful output: its output is void/unit.

Let’s explore resources and their outputs in another example. The C function incr takes an int pointer p and increments the pointee value.

In the precondition we assert ownership of resource Owned<int>(p), binding its output/pointee value to v1, and use v1 to specify that p must point to a sufficiently small value at the start of the function not to overflow when incremented. The postcondition asserts ownership of p with output v2, as before, and uses this to express that the value p points to is incremented by incr: v2 == v1+1i32.

If we incorrectly tweaked this specification and used Block<int>(p) instead of Owned<int>(p) in the precondition, as below, then CN would reject the program.

CN reports:

The Owned<int>(p) resource required for reading is missing, since, as per precondition, only Block<int>(p) is available. Checking the linked HTML file confirms this. Here the section “Available resources” lists all resource ownership at the point of the failure:

Zero. Write a specification for the function zero, which takes a pointer to uninitialised memory and initialises it to 0.

In-place double. Give a specification for the function inplace_double, which takes an int pointer p and doubles the pointee value: specify the precondition needed to guarantee safe execution and a postcondition that captures the function’s behaviour.

When functions manipulate multiple pointers, we can assert their ownership just like before. However (as in standard separation logic) pointer ownership is unique, so simultaneous ownership of Owned or Block resources for two pointers requires these pointers to be disjoint.

The following example shows the use of two Owned resources for accessing two different pointers: function add reads two int values in memory, at locations p and q, and returns their sum.

This time we use C’s unsigned int type. In C, over- and underflow of unsigned integers is not undefined behaviour, so we do not need any special preconditions to rule this out. Instead, when an arithmetic operation at unsigned type goes outside the representable range, the value “wraps around”.

The CN variables m and n (resp. m2 and n2) for the pointee values of p and q before (resp. after) the execution of add have CN basetype u32, so unsigned 32-bit integers, matching the C unsigned int type. Like C’s unsigned integer arithmetic, CN unsigned int values wrap around when exceeding the value range of the type.

Hence, the postcondition return == m+n holds also when the sum of m and n is greater than the maximal unsigned int value.

In the following we will sometimes use unsigned integer types to focus on specifying memory ownership, rather than the conditions necessary to show absence of C arithmetic undefined behaviour.

Swap. Specify the function swap, which takes two owned unsigned int pointers and swaps their values.

Transfer. Write a specification for the function transfer, shown below.

While one might like to think of a struct as a single (compound) object that is manipulated as a whole, C permits more flexible struct manipulation: given a struct pointer, programmers can construct pointers to individual struct members and pass these as values, even to other functions.

CN therefore cannot treat resources for compound C types, such as structs, as primitive, indivisible units. Instead, Owned<T> and Block<T> are defined inductively in the structure of the C-type T.

For struct types T, the Owned<T> resource is defined as the collection of Owned resources for its members (as well as Block resources for any padding bytes in-between). The resource Block<T>, similarly, is made up of Block resources for all members (and padding bytes).

To handle code that manipulates pointers into parts of a struct object, CN can automatically decompose a struct resource into the member resources, and recompose it, as needed. The following example illustrates this.

Recall the function zero from our earlier exercise. It takes an int pointer to uninitialised memory, with Block<int> ownership, and initialises the value to zero, returning an Owned<int> resource with output 0.

Now consider the function init_point, shown below, which takes a pointer p to a struct point and zero-initialises its members by calling zero twice, once with a pointer to struct member x, and once with a pointer to y.

As stated in its precondition, init_point receives ownership Block<struct point>(p). The zero function, however, works on int pointers and requires Block<int> ownership.

CN can prove the calls to zero with &p->x and &p->y are safe because it decomposes the Block<struct point>(p) into two Block<int>, one for member x, one for member y. Later, the reverse happens: following the two calls to zero, as per zero’s precondition, init_point has ownership of two adjacent Owned<int> resources – ownership for the two struct member pointers, with the member now initialised. Since the postcondition of init_point requires ownership Owned<struct point>(p), CN combines these back into a compound resource. The resulting Owned<point struct> resource has for an output the struct value s2 that is composed of the zeroed member values for x and y.

To handle the required resource inference, CN “eagerly” decomposes all struct resources into resources for the struct members, and “lazily” re-composes them as needed.

We can see this if, for instance, we experimentally change the transpose example from above to force a type error. Let’s insert an /*@ assert(false) @*/ CN assertion in the middle of the transpose function (more on CN assertions later), so we can inspect CN’s proof context shown in the error report.

The precondition of transpose asserts ownership of an Owned<struct point>(p) resource. The error report now instead lists under “Available resources” two resources:

Here member_shift<s>(p,m) is the CN expression that constructs, from a struct s pointer p, the “shifted” pointer for its member m.

When the function returns the two member resources are recombined “on demand” to satisfy the postcondition Owned<struct point>(p).

Init point. Insert CN assert(false) statements in different statement positions of init_point and check how the available resources evolve.

Transpose (again). Recreate the transpose function from before, now using the swap function verified earlier (for struct upoint, with unsigned member values).

Let’s see how this applies to a first example of an array-manipulating function. Function read takes three arguments: the base pointer p of an int array, the length n of the array, and an index i into the array; read then returns the value of the i-th array cell.

The CN precondition requires

On exit the array ownership is returned again.

This specification, in principle, should ensure that the access p[i] is safe. However, running CN on the example produces an error: CN is unable to find the required ownership for reading p[i].

The reason is that when searching for a required resource, such as the Owned resource for p[i] here, CN’s resource inference does not consider iterated resources. Quantifiers, as used by iterated resources, can make verification undecidable, so, in order to maintain predictable type checking, CN delegates this aspect of the reasoning to the user.

To make the Owned resource required for accessing p[i] available to CN’s resource inference we have to “extract” ownership for index i out of the iterated resource.

Here the CN comment /*@ extract Owned<int>, i; @*/ is a CN “ghost statement”/proof hint that instructs CN to instantiate any available iterated Owned<int> resource for index i. In our example this operation splits the iterated resource into two:

is split into

After this extraction step, CN can use the (former) extracted resource to justify the access p[i].

Following an extract statement, CN moreover remembers the extracted index and can automatically “reverse” the extraction when needed: after type checking the access p[i] CN must ensure the function’s postcondition holds, which needs the full array ownership again (including the extracted index i); remembering the index i, CN then automatically merges resources (1) and (2) again to obtain the required full array ownership, and completes the verification of the function.

So far the specification only guarantees safe execution but does not specify the behaviour of read. To address this, let’s return to the iterated resources in the function specification. When we specify take a1 = each ... here, what is a1? In CN, the output of an iterated resource is a map from indices to resource outputs. In this example, where index j has CN type i32 and the iterated resource is Owned<int>, the output a1 is a map from i32 indices to i32 values — CN type map<i32,i32>. (If the type of j was i64 and the resource Owned<char>, a1 would have type map<i64,u8>.)

We can use this to refine our specification with information about the functional behaviour of read.

We specify that read does not change the array — the outputs a1 and a2, taken before and after running the function, are the same — and that the value returned is a1[i], a1 at index i.

Array read two. Specify and verify the following function, array_read_two, which takes the base pointer p of an unsigned int array, the array length n, and two indices i and j. Assuming i and j are different, it returns the sum of the values at these two indices.

Swap array. Specify and verify swap_array, which swaps the values of two cells of an int array. Assume again that i and j are different, and describe the effect of swap_array on the array value using the CN map update expression a[i:v], which denotes the same map as a, except with index i updated to v.

The array examples covered so far manipulate one or two individual cells of an array. Another typical pattern in code working over arrays is to loop, uniformly accessing all cells of an array, or sub-ranges of it.

In order to verify code with loops, CN requires the user to supply loop invariants — CN specifications of all owned resources and the constraints required to verify each iteration of the loop.

Let’s take a look at a simple first example. The following function, init_array, takes the base pointer p of a char array and the array length n and writes 0 to each array cell. .exercises/init_array.c

If, for the moment, we focus just on proving safe execution of init_array, ignoring its functional behaviour, a specification might look as above: on entry init_array takes ownership of an iterated Owned<char> resource — one Owned resource for each index i of type u32 (so necessarily greater or equal to 0) up to n; on exit init_array returns the ownership.

To verify this, we have to supply a loop invariant that specifies all resource ownership and the necessary constraints that hold before and after each iteration of the loop. Loop invariants are specified using the keyword inv, followed by CN specifications using the same syntax as in function pre- and postconditions. The variables in scope for loop invariants are all in-scope C variables, as well as CN variables introduced in the function precondition. In loop invariants, the name of a C variable refers to its current value (more on this shortly).

The main condition here is unsurprising: we specify ownership of an iterated resource for an array just like in the the pre- and postcondition.

The second thing we need to do, however, is less straightforward. Recall that, as discussed at the start of the tutorial, function arguments in C are mutable, and so CN permits this as well.While in this example it is obvious that p and n do not change, CN currently requires the loop invariant to explicitly state this, using special notation {p} unchanged (and similarly for n).

Note. If we forget to specify unchanged, this can lead to confusing errors. In this example, for instance, CN would verify the loop against the loop invariant, but would be unable to prove a function postcondition seemingly directly implied by the loop invariant (lacking the information that the postcondition’s p and n are the same as the loop invariant’s). Future CN versions may handle loop invariants differently and treat variables as immutable by default.

The final piece needed in the verification is an extract statement, as used in the previous examples: to separate the individual Owned<char> resource for index j out of the iterated Owned resource and make it available to the resource inference, we specify extract Owned<char>, j;.

With the extract statements in place, CN accepts the function.

However, on closer look, the specification of init_array is overly strong: it requires an iterated Owned resource for the array on entry. If, as the name suggests, the purpose of init_array is to initialise the array, then a precondition asserting only an iterated Block resource for the array should also be sufficient. The modified specification is then as follows.

This specification should hold: assuming ownership of an uninitialised array on entry, each iteration of the loop initialises one cell of the array, moving it from Block to Owned “state”, so that on function return the full array is initialised. (Recall that stores only require Block ownership of the written memory location, so ownership of not-necessarily-initialised memory.)

To verify this modified example we again need a loop invariant. This time, the loop invariant is more involved, however: since each iteration of the loop initialises one more array cell, the loop invariant has to do precise book-keeping of the initialisation status of the array.

To do so, we partition the array ownership into two parts: for each index of the array the loop has already visited, we have an Owned resource, for all other array indices we have the (unchanged) Block ownership.

Let’s go through this line-by-line:

As before, we also have to instruct CN to extract ownership of individual array cells out of the iterated resources:

Init array reverse. Verify the function init_array_rev, which has the same specification as init_array2, but initializes the array in decreasing index order (from right to left).

Prove a specification for the following program that reveals only that it returns a pointer to a number that is greater than the number pointed to by its argument.

Here is another syntax for external / unknown functions, together with an example of a loose specification:

With this basic infrastructure in place, we can start specifying and verifying list-manipulating functions. First, append.

Here is its specification (in a separate file, because we’ll want to use it multiple times below.)

Here is a simple destructive append function. Note the two uses of the unfold annotation in the body, which are needed to help the CN typechecker.

Here is an allocating list copy function with a pleasantly light annotation burden.

Finally, here is a slightly tricky in-place version of merge sort that avoids allocating any new list cells in the splitting step by taking alternate cells from the original list and linking them together into two new lists of roughly equal lengths.

Allocating append. Fill in the CN annotations on IntList_append2. (You will need some in the body as well as at the top.)

Note that it would not make sense to do the usual functional-programming trick of copying xs but sharing ys. (Why?)

Length. Add annotations as appropriate:

List deallocation. Fill in the body of the following procedure and add annotations as appropriate:

Length with an accumulator. Add annotations as appropriate:

The specification of list reversal in CN relies on the familiar recursive list reverse function, with a recursive helper.

To reason about the C implementation of list reverse, we need to help the SMT solver by enriching its knowledge base with a couple of facts about lists. The proofs of these facts require induction, so in CN we simply state them as lemmas and defer the proofs to Coq.

Having stated these lemmas, we can now complete the specification and proof of IntList_rev. Note the two places where apply is used to tell the SMT solver where to pay attention to the lemmas.

For comparison, here is another way to write the program, using a while loop instead of recursion, with its specification and proof.

Sized stacks: Fill in annotations where requested:

The syntax of the C language does not actually include constants. Instead, the convention is to use the macro preprocessor to replace symbolic names by their definitions before the C compiler ever sees them.

This raises a slight awkwardness in CN, because CN specifications and annotations are written in C comments, so they are not transformed by the preprocessor. However, we can approximate the effect of constant values by defining constant functions. We’ve been working with some of these already, e.g., MINi32(), but it is also possible to define our own constant functions. Here is the officially approved idiom:

Here’s how it works:

Of course, we could achieve the same effect by defining the CN function CONST() directly…​

…​but this version repeats the number 1 in two places — a potential source of nasty bugs!

A queue is a linked list with O(1) operations for adding things to one end (the "back") and removing them from the other (the "front"). Here are the C type definitions:

A queue consists of a pair of pointers, one pointing to the front element, which is the first in a linked list of `int_queueCell`s, the other pointing directly to the last cell in this list. If the queue is empty, both pointers are NULL.

Abstractly, a queue just represents a list, so we can reuse the seq type from the list examples earlier in the tutorial.

Given a pointer to an int_queue struct, this predicate grabs ownership of the struct, asserts that the front and back pointers must either both be NULL or both be non-NULL, and then hands off to an auxiliary predicate IntQueueFB. (Conceptually, IntQueueFB is part of IntQueuePTR, but CN currently allows conditional expressions only at the beginning of predicate definitions, not after a take.)

IntQueueFB is where the interesting part starts:

First, we case on whether the front of the queue is NULL. If so, then the queue is empty and we return the empty sequence.

If the queue is not empty, we need to walk down the linked list of elements and gather up all their values into a sequence. But we must treat the last element of the queue specially, for two reasons. First, because the push operation is going to follow the back pointer directly to the last list cell without traversing all the others, we need to take that element now rather than waiting to get to it at the end of the recursion starting from the front. Second, and relatedly, there will be two pointers to this final list cell — one from the back field and one from the next field of the second to last cell (or the front pointer, if there is only one cell in the list), so we need to be careful not to take this cell twice.

Accordingly, we begin by take`ing the tail cell and passing it separately to the `IntQueueAux predicate, which has the job of walking down the cells from the front and gathering all the rest of them into a sequence. We take the result from IntQueueAux and snoc on the very last element.

The assert (is_null(B.next)) here gives the CN verifier a crucial piece of information about an invariant of the representation: The back pointer always points to the very last cell in the list, so its next field will always be NULL.

Finally, the IntQueueAux predicate recurses down the list of cells.

Its first argument (f) starts out at front and progresses through the list on recursive calls; its b argument is always a pointer to the very last cell.

When f and b are equal, we have reached the last cell and there is nothing to do. (We don’t even have to build a singleton list: that’s going to happen one level up, in IntQueueFB.)

Otherwise, we take the fields of the f, make a recurive call to IntQueueAux to process the rest of the cells, and cons the first field of this cell onto the resulting sequence before returning it. (Again, we need to help the CN verifier by explicitly informing it of the invariant that we know, that C.next cannot be null if f and b are different.)

Now we need a bit of boilerplate: just as with linked lists, we need to be able to allocate and deallocate queues and queue cells. There are no interesting novelties here.

Exercise: The function for creating an empty queue just needs to set both of its fields to NULL. See if you can fill in its specification.

The push and pop operations are more involved. Let’s look at push first.

Here’s the unannotated C code — make sure you understand it.

Exercise: Before reading on, see if you can write down a reasonable top-level specification for this operation.

(One thing you might find odd about this code is that there’s a return statement at the end of each branch of the conditional, rather than a single return at the bottom. The reason for this is that, when CN analyzes a function body containing a conditional, it effectively copies all the code after the conditional into each of the branches. Then, if verification encounters an error related to this code — e.g., "you didn’t establish the ensures conditions at the point of returning — the error message will be confusing because it will not be clear which branch of the conditional it is associated with.)

Now, here is the annotated version of the push operation.

The case where the queue starts out empty (q->back == 0) is easy. CN can work it out all by itself.

The case where the starting queue is nonempty is more interesting. The push operation messes with the end of the sequence of queue elements, so we should expect that validating push is going to require some reasoning about this sequence. Here, in fact, is the lemma we need.

This says, in effect, that we have two choices for how to read out the values in some chain of queue cells of length at least 2, starting with the cell front and terminating when we get to the next cell following some given cell p — call it c. We can either gather up all the cells from front to c, or we can gather up just the cells from front to p and then snoc on the single value from c.

When we apply this lemma, p will be the old back cell and c will be the new one. But to prove it (by induction, of course), we need to state it more generally, allowing p to be any internal cell in the list starting at front and c its successor.

The reason we need this lemma is that, to add a new cell at the end of the queue, we need to reassign ownership of the old back cell. In the precondition of push, we took ownership of this cell separately from the rest; in the postcondition, it needs to be treated as part of the rest (so that the new back cell can now be treated specially).

One interesting technicality is worth noting: After the assignment q->back = c we can no longer prove IntQueueFB(q->front, oldback), but we don’t care, since we want to prove IntQueueFB(q->front, q->back). However, crucially, IntQueueAux(q->front, oldback) is still true.

Now let’s look at the pop operation. Here is the un-annotated version:

Exercise: Again, before reading on, see if you can write down a plausible top-level specification. (For extra credit, see how far you can get with verifying it!)

Here is the fully annotated pop code:

There are three annotations to explain. Let’s consider them in order.

First, the split_case on is_null(q->front) is needed to tell CN which of the branches of the if at the beginning of the IntQueueFB predicate it can "unpack". (IntQueuePtr can be unpacked immediately because it is unconditional, but IntQueueFB cannot.)

The guard/condition for IntQueueFB is is_null(front), which is why we need to do a split_case on this value. On one branch of the split_case, we have a contradiction: the fact that before == Seq_Nil{} (from IntQueueFB) conflicts with before != Seq_Nil from the precondition, so that case is immediate. On the other branch, CN now knows that the queue is non-empty as required and type checking proceeds.

When h == q->back, we are in the case where the queue contains just a single element, so we just need to NULL out its front and back fields and deallocate the dead cell. The unfold annotation is needed because the snoc function is recursive, so CN doesn’t do the unfolding automatically.

Finally, when the queue contains two or more elements, we need to deallocate the front cell, return its first field, and redirect the front field of the queue structure to point to the next cell. To push the verification through, we need a simple lemma about the snoc function:

The crucial part of this lemma is the last three lines, which express a simple, general fact about snoc: if we form a sequence by calling snoc to add a final element B.first to a sequence with head element x and tail Q, then the head of the resulting sequence is still x, and its tail is snoc (Q, B.first).

The requires clause and the first three lines of the ensures clause simply set things up so that we can name the various values we are talking about. Since these values come from structures in the heap, we need to take ownership of them. And since lemmas in CN are effectively just trusted functions that can also take in ghost values, we need to take ownership in both the requires and ensures clauses. (Taking them just in the requires clause would imply that they are consumed and deallocated when the lemma is applied — not what we want!)

(The only reason we can’t currently prove this lemma in CN is that we don’t have `take`s in CN statements, because this is just a simple unfolding.)

Exercise: Investigate what happens when you make each of the following changes to the queue definitions. What error does CN report? Where are the telltale clues in the error report that suggest what the problem was?

Exercise: The conditional in the pop function tests whether or not f == b to find out whether we have reached the last element of the queue. Another way to get the same information would be to test whether f->next == 0. Can you verify this version?

Note: I (BCP) have not worked out the details, so am not sure how hard this is (or if it is even not possible, though I’d be surprised). Please let me know if you get it working!

Exercise: Looking at the code for the pop operation, it might seem reasonable to move the identical assignments to x in both branches to above the if. This doesn’t "just work" because the ownership reasoning is different. In the first case, ownership of h comes from IntQueueFB (because h == q->back). In the second case, it comes from IntQueueAux (because h != q->back).

Can you generalize the snoc_facts lemma to handle both cases? You can get past the dereference with a split_case but formulating the lemma before the return will be a bit more complicated.

Note: Again, this has not been shown to be possible, but Dhruv believes it should be!

A doubly linked list is a linked list where each node has a pointer to both the next node and the previous node. This allows for O(1) operations for adding or removing nodes anywhere in the list. Here is the C type definition:

The idea behind the representation of this list is that we don’t keep track of the front or back, but rather we take any node in the list and have a sequence to the left and to the right of that node. The left and right are from the point of view of the node itself, so left is kept in reverse order. Additionally, similarly to in the Imperative Queues example, we can reuse the seq type.

The predicate for this datatype is a bit complicated. The idea is that we first want to own the node that is passed in. Then, we want to follow all of the prev pointers to own everything backwards from the node. We want to do the same for the next pointers to own everything forwards from the node. This is how we construct our left and right fields.

Note that Dll_at takes ownership of the node passed in, and then calls Own_Backwards and Own_Forwards which recursively take ownership of the rest of the list and add their values to the left and right sequences, respectively.

Additionally, you will notice that Own_Forwards and Own_Backwards include ptr_eq assertions for the prev and next pointers. This is to ensure that the nodes in the list are correctly doubly linked. For example, the line assert (ptr_eq(n.prev, prev_pointer)); in Own_Forwards ensures that the current node correctly points backward to the previous node in the list. The line assert(ptr_eq(prev_node.next, p)); ensures that the previous node correctly points forward to the current node. The same can be said for these assertions in Own_Backwards.

All three of these predicates stop once they reach a null pointer. In this way, we can ensure that the only null pointers in the list are at the beginning and end of the list.

Before we move on to the functions that manipulate the doubly linked list, we need to define a few "getter" functions that will allow us to access the fields of our Dll datatype. This will make our specifications much easier to write.

We also must include some boilerplate code for allocation and deallocation.

And we compile all of these files into a single header file.

Lastly, an important note about this representation of a doubly linked list is that there is no higher level representation of the list (such as the int_queue structure in the Imperative Queues section). This makes it difficult to reason about adding and removing things from a list that may be empty at some times. If we have an empty list, we do not want any identifier of this list to disappear altogether. To work around this problem, we represent an empty list as a null pointer and require that every function that manipulates the list must return a pointer to somewhere in the list. This way, we can always have a pointer to the list, even if it is empty.

Now we can move on to an initialization function. Since an empty list is represented as a null pointer, we will look at initializing a singleton list (or in other words, a list with only one item).

The add and remove functions are where it gets a little tricker. Let’s start with add. Here is the unannotated version: