First Pass

This chapter explains how to specify operations on ML-style arrays in Separation Logic. In ML languages, an array of size n is an allocated block of size n+1 with a header field that stores the length of the array. To perform a get or a set operation on an array, the programmer provides the pointer to the array object, that is, the address of the header cell, as well as the index on which to operate. This chapter starts with a presentation of large-footprint operations for arrays, expressed with respect to a representation predicate of the form harray L p. Then, it presents small-footprint specifications for the same operations, involving a representation predicate of the form hcell v p i for representing each cell, as well as a predicate, written hheader p n for representing the header field. We will illustrate the benefits of small-footprint specifications for reasoning about the recursive function quicksort, which operates on array segments. Segments are described using the heap predicate harray_seg L p i . Array segments allow "framing" the parts of the arrays that are not involved in a recursive call. The "more details" part of the chapter explains how to define the predicates hheader, hcell, hseg, and harray with respect to the representation of heaps as a finite map from locations to values. The "optional material" part of the chapter shows how to implement and verify make, length, get, and set in terms of block allocation and pointer arithmetics.

Large-Footprint Specifications for Array Operations

The heap predicate harray L p asserts that an array allocated is allocated at address p, and that its elements are described by the list L. At this stage, let us axiomatize this predicate.

The operation val_array_make n v allocates a fresh array of length n, such that each of its cells contains the value v.

The specifications of val_array_make requires the length n to be nonnegative. The output array is described as a list made of n copies of the value v. This list is written LibList.make (abs n) v, where abs converts the integer n into a natural number.

Alternatively, the array produced by make n v can be described extensionally, as a list L of length n such that all its elements are equal to v. This alternative statement of the postcondition is, however, much more verbose.

The operation val_array_length p returns the length of the array allocated at location p.

The specification for val_array_length expects a heap predicate of the form harray L p, and asserts that the return value is the length of the logical list L. The postcondition repeats harray L p to capture the fact that the array is not modify during the operation.

The operation val_array_get p i returns the contents of the i-th cell of the array at location p.

The specification of val_array_get is as follows. The precondition describes the array in the form harray L p, with a premise that requires the index i to be in the valid range, that is, between zero (inclusive) and the length of L (exclusive). The postcondition asserts that the result value is the i-th value of the list L, written nth (abs i) L. The postcondition repeats harray L p because the array is unchanged.

The operation val_array_set p i v updates the contents of the i-th cell of the array at location p.

The specification of val_array_set admits the same precondition as val_array_get, with harray L p and the constraint 0 ≤ i < length L. Its postcondition describes the updated array using a predicate of the form harray L' p, where L' corresponds to the update of the i-th item of the list L with the value v, written update (abs i) v L.

Small-Footprint Specifications for Array Operations

The large-footprint specifications presented above are sufficently expressive for verifying sequential programs manipulating arrays. Yet, they are too limited for verifying a parallel program that concurrently updates two independent segments of an array. In fact, even the verification of certain sequential programs can benefit from the use of smaller-footprint specifications, which require the ownership not of the whole array but only of a specific subset of the array cells. For example, the quicksort divide-and-conquer function sorts the elements over a given range of cells. In what follows, we present small-footprint specifications for operating on individual cells and for operating on array segments, then present the proof of quicksort. Small-footprint specifications are expressed using the heap predicate for individual cells and for header cells. The heap predicate hcell v p i asserts that the cell at index i in the array p stores the value v. Internally, hcell v p i may be defined as (p+i) ~~> v.

The heap predicate hheader n p asserts that the header cell of the array at address p stores the length n. Internally, hheader n p may be defined as p ~~> n.

To read the length of an array, it is sufficient to provide the heap predicate associated with the header field of that array. In other words, there is no need to have the ownership of any cell of an array for reading its length.

To read or write in a given array cell, it is sufficient to provide the hcell predicate associated with that cell. There is no need to own the header cell or other cells of the array.

Note: technically, a ML runtime performs bound checks on get and set operations, to ensure that the indices provided fall within the array. These bound-checks operations do involve a read to the header field. Thus, it may appear that the header cell ought to be involved in the specification of get and set. Yet, providing the hheader predicate is not required for verifying the correctness a program. If one wanted to formally verify a runtime system, one would argue instead that headers are read-only cells, and the runtime system would keep at hand a "fraction" of the hheader predicate to justify its reads in header cells.

Heap Predicate for Array Segments

So far, we have presented small-footprint specifications expressed in terms of hheader and hcell. Yet, the creation of an array via the operation val_array_make n v produces a heap predicate of the form harray L p. Thus, there remain to explain how to convert an harray predicate into the separating conjunction of a hheader predicate and of a set of hcell predicates. The auxiliary predicate hseg L p j describes an "array segment": it describes the iterated separating conjunction of the predicate hcell over a set of consecutive cells starting at index j, with elements described by the list L. For example hseg (x₀::x₁::x₂::nil) p j corresponds to hcell x₀ p (j+0) \* hcell x₁ p (j+1) \* hcell x₂ p (j+2).

If the list L is empty, then the predicate hseg nil p j is equivalent to the empty heap predicate. In particular, it does not assert that j is a valid index in the array. (The proof of this lemma and the following one appears further in the file.)

If the list L is a singleton list, then the predicate hseg (v::nil) p j is equivalent to the hcell v p j.

A key result captures how a range of consecutive cells may be split in two parts. Concretely, a heap predicate describing a segment with elements (L₁++L₂) can be split into a prediate describing a first segment with elements L₁, and another predicate describing a second segment with elements L₂. The two parts can be merged back into the original form at any time, as captured by the equality symbol in the statement below.

For verifying programs, two corollaries are convenient. The lemma hseg_cons isolates the first cell of a segment, whereas the lemma hseg_last isolates the last cell of a segment.

These two corollaries themselves admin additional reformulations that help merge back the isolated head and tail cells. The statements do not constraint the offsets to be syntactically of the form j + 1 or j + length L₁, but instead introduces arithmetic equalities that the tactic math can generally handle.

Derived Segment-Based Specifications for Array Operations

For reasoning about programs that operate over array segments, e.g. quicksort, it is convenient to specify the functions make, length, get and set exclusively in terms of hheader and hseg. The lemma triple_array_length_header specifies length in terms hheader. For the other operations, we consider the following derived specifications.

Verification of the Safety of QuickSort

Let us illustrate the benefits of these segment-based specifications through the reasoning about the divide-and-conquer quicksort function. For simplicity, let us consider an array that stores integer values. The implementation of quicksort is standard, using an auxiliary pivot function. The operation pivot p i n processes the segment of array p that starts at index i and is made of n elements. The pivot function considers an arbitrary element from that segment as pivot. It then reorders the elements from the segment, separating the values less than or equal to the pivot value from the values greater than the pivot value. The function returns the index at which the pivot value ends up being stored in the segment.   let pivot p i n = ...
    (* pivot modifies an array p,
       and returns the index j of a pivot value x,
       with j in the range i ≤ j < i+n,
       such that elements in the range i .. j-1 are smaller than x,
       and elements in the range j+1 .. i+n-1 are no smaller than x. *)

  (* quicksort sort an array p on the range of indices i .. i+n-1. *)
  let rec quicksort p i n =
    if n > 1 then begin
      let j = pivot p i n in
      let n₁ = j - i in
      quicksort p i n₁;
      quicksort p (j+1) (n-n₁-1)
    end As a warm-up before establishing the full functional correctness of quicksort, we begin by establishing the safety and the termination of the code. In other words, the aim is to prove that every array access is valid, through the use of array-segment specifications. This safety proof captures the essence of the ownership reasoning at play, including the framing process over recursive calls. In the "more details" section, we will generalize the proof to justify that quicksort correctly sorts its input array. The safety specification of pivot asserts that pivot p i n operates on a range of size n, starting at index i of the array p. This range is described in the precondition by a list L, and in the postcondition by a list L'. This list L' decomposes as L₁ ++ x :: L₂, where x denotes the pivot value. In the full correctness proof, we will assert that L₁ contains values smaller than x, and L₂ values no smaller than x, but for establishing safety these assertions are not needed.

The recursive function quicksort p i n sorts an segment of length n, starting at index i, in the array p.

Exercise: 4 stars, standard, especially useful (triple_quicksort_safety)

Prove that quicksort operates on the targeted array segment without interferring with the other cells of the array. This property is captured by the specification shown below. Hint: use xapp triple_pivot_safety to reason about the call to pivot.

More Details

Formalization of Sorted Lists

To refine the above safety proof into a functional correctness proof, we first need to formalize the notation of permutation and of sortedness. The predicate permut L L' asserts that L' is a permutation of the list L.

The predicate permut is reflexive and symmetric.

If L' is a permutation of L, then L' has the same length as L.

If L₁' is a permutation of L₁, and L₂' is a permutation of L₂, then the concatenation L₁' ++ L₂' is a permutation of L₁ ++ L₂. This result, and its corollaries for cons and last are stated next.

Swapping of consecutive elements, or moving the first element to the last position, yield valid permutations.

If a property P holds for all elements of a list L, it also holds for all the elements of any permutation of L.

The predicate sorted L asserts that L is a sorted list of integers.

The proposition list_of_gt x L asserts that all elements in L are greater than x. Symmetrically, the proposition list_of_le x L asserts that all elements in L is no greater than x.

Two key lemmas for verifying sorting algorithms are stated below. First, if L is sorted, then adding an element x no greater than elements in L to the front of L yields a sorted list.

Second, if L₁ is a sorted list, if x is no less than the elements in L₁, and if x::L₂ is a sorted list, then L₁ ++ x :: L₂ is sorted.

Formalization of Arrays of Integer Values

To specify quicksort and other functions manipulating lists of integers, it is useful to introduce a convertion function named vals_int, which converts converts a list of integer (type list int) into a list of values (type list val). In particular, hseg (vals_int L) p i describes an array segment containing integer values.

To reason about these operations, we add rewriting rules to the tactic rew_list and rew_listx. The latter is a variant of rew_list that includes a larger number of rewriting lemmas, including e.g. properties operations such as LibList.map.

Functional Correctness Proof for Quicksort

In order to verify quicksort, we need to refine the specification of the pivot function to include functional correctness properties. The postcondition of the pivot operation describes the elements in the segment as the list L'. This list decomposes as L₁ ++ x :: L₂, where x corresponds to the pivot. This time, the assertions list_of_le x L₁ and list_of_gt x L₂ are included.

Exercise: 5 stars, standard, optional (triple_quicksort)

Prove that quicksort sorts the array segment targeted by its arguments. Hint: use xapp triple_pivot.

The function quicksort_full p sorts all the elements stored in the array at address p.

The predicate harray L p is defined as the conjunction of hheader (length L) p, which captures the fact that the header stores the length of the list L, and of hseg L p 0, which describes "full" array segment, ranging from the first to the last cell of the array.

Exercise: 2 stars, standard, optional (triple_quicksort_full)

Prove that val_quicksort_full sorts an array. Hint: use xchange and xchange <- on harray_eq to convert between harray and hseg.

Realization of hheader and hcell

So far, the predicates hheader and hcell were axiomatized. Let us show how they can be realized with respect to the representation of the memory state, of type heap. The predicates hseg and harray can then be defined on top of hheader and hcell. Following the standard memory layout of allocated blocks in ML programs, we represent ML-style array of size n as a memory block of size n+1. The first cell, called the "header cell", stores the length of the array. The remaining cells store the elements from the array. The heap predicate hheader n p describes a cell at location p with contents n. Recall that the definition of hheader is opaque to the user, thus there is no risk that the programmer attempts to reason about code that modifies header fields.

The following lemma is useful for folding or unfolding the definition.

The predicate hcell v p i asserts that the cell at index i from the array at address p stores the value p. We defined this predicate by asserting that the cell in memory at address p+1+i stores the value v. Thus, as first approximation, the predicate hcell v p i could be defined as (p + 1 + abs i) ~~> v. The actual definition also embeds the assertion i ≥ 0 to guarantee that i refers to a valid index, and that p + 1 + abs i computes the expected offset.

The following lemma is useful for folding or unfolding the definition.

The corollary stated below extracts the property i ≥ 0 from hcell v p i .

Realization of hseg and harray

The heap predicate hseg for array segments can be defined in terms of hcell as shown earlier on.

The predicate for full arrays harray can be defined as the pair of a predicate hheader covering the header cell, and a segment covering the full range of the array, described using hseg.

The lemma harray_eq can be used for folding or unfolding harray.

When proving properties about hseg L p j, one frequently faces a mismatch between hseg L p j₁ and hseg L p j₂, where j₁ and j₂ are provably equal yet do not unify. To avoid cluttering proofs, the following lemma and associated hint are very useful.

We prove the lemmas hseg_nil and hseg_one and hseg_cons, which we presented and exploited earlier in this chapter.

Exercise: 3 stars, standard, especially useful (hseg_app)

Prove the splitting lemma for array segments. Hint: rew_list is helpful to simplify list operations. Recall that xsimpl helps proving equalities on hprop.

Focus Lemmas for Array Segments

With a predicate harray L p at hand, it may be useful to isolate the cell at an index i, that is, to extract the predicate hcell v p i, where 0 ≤ i < length L and v = LibList.nth (abs i) L. By giving back the predicate hcell v p i, one gets back the original predicate harray L p.

The lemma above, called a "focus" lemma or "borrowing" lemma in Rust's terminology only supports reading into the "focused" cell at index i. It does not allow modifying the contents of the cell. Indeed, if hcell v p i is updated to hcell w p i, then the magic wand hcell v p i \−∗ harray L p can no longer be exploited. Fortunately, it is straightforward to generalize the focus lemma into a form that supports updates. The general focus lemma shown below makes use of a universal quantification over the value w that the cell i may contain after potential update operations.

The focus lemmas are not easy to read, yet they are critically useful. Without them, we would need to repeat a number of tedious splitting and merging steps.

Exercise: 4 stars, standard, especially useful (hseg_focus)

Prove the focus lemma for array segments. Hint: although a proof by induction is possible, a simpler proof can be achieved by exploiting the lemmas LibList.list_middle_inv, LibList.nth_middle and LibList.update_middle. Besides, recall that lemma Inhab_val proves Inhab val.

In the statement above, k is an index relative to the start of the segment. The focus lemma can also be expressed in terms of absolute indices. Below, i denotes a valid array index that falls in the targeted segment.

We can derive the focus lemma for harray from that for hseg.

Exercise: 3 stars, standard, especially useful (harray_focus_read)

Prove that the "focus-read" lemma is a direct consequence of the general version of the focus lemma harray_focus. Hint: use LibList.update_nth_same.

Optional Material

In this section, we show how to implement array operations in terms of lower-level primitive operations such as block allocation and pointer arithmetic.

Semantics of Pointer Arithmetics

The operation val_ptr_add p n applies to a pointer p and an integer n, and returns the address p+n. In other words, it computes the address of the n-th cell past the cell at location p. We assume val_ptr_add to be a primitive of the language.

The evaluation rule and the general specification for pointer addition are shown below. They both require p+n to be a nonnegative integer.

For the math tactic provided by the TLC library to operate well on goals involving expressions of the form p+n involved in calls to val_ptr_add, we need a small tweak. We instantiate a hook of the math tactic to registier loc as transparent type for this tactic.

For the purpose of this course, we only need to shift pointers by a nonnegative number of cells. We show below a simplified specification featuring the premise n ≥ 0 instead of p+n ≥ 0.

Semantics of Low-Level Block Allocation

The operation val_alloc n allocates a block of n consecutive cells. It is specified as shown below. Starting from a state sa, it produces a state described as the union of sb and sa, where sb consists of consecutive of n consecutive cells. In the evaluation rule shown below, Fmap.conseq L p builds a state with a range of cells starting a location p, and with contents described by the list L. Each of these cells is specified as having the special value val_uninit as contents.

The specification of val_alloc is expressed using the heap predicate hrange L p. This predicate describes a range of consecutive cells. In short, hrange L p characterizes heaps produces by Fmap.conseq L p. The structure of the recursive definition of hrange resembles that of hseg.

The allocation operation val_alloc is then specified as producing a heap described using hrange for a list of uninitialized values. Note: in ML, uninitialized values are never exposed to the programmer; val_alloc is only meant to be invoked internally by the runtime system.

Low-Level Implementation of Arrays

We are now ready to explain how a runtime system could implement the operations length, get, set, and make on arrays, in terms of val_alloc and val_ptr_add for allocating memory blocks and computing pointer offsets, as well as val_get and val_set for reading and writing into individual memory cells.

The operation that obtains the length of an array is implemented by reading the integer stored into the header field of that array.

The operation that reads into an array cell, written val_array_get p i, is implemented as a read at the location p + 1 + abs i.

The operation that reads into an array cell, written val_array_set p i v, is implemented as a write of v at the location p + 1 + abs i.

The auxiliary function fill is used to implement make. The operation fill p i n v fills the range of the array p, starting at index i, with n copies of the value v. The code below provides a naive recursive implementation of fill.

The operation val_array_make n v creates an array of length n filled with copies of the value v. It is implemented as the allocation of a block of length n+1 at a fresh address p, followed by the write of the value n in the header, and with a call to fill p 0 n v for filling the n cells of the array p with copies of the value v.

Verification of Low-Level Operations for Arrays

The purpose of this section is to prove that the implementations presented above for length, get, set, and make indeed satisfy the specifications axiomatized for them earlier in this chapter. For these proofs, we need to set the definition of hheader as transparent.

We also add a hint for xapp, to automatically handle the arithmetic preconditions arising from calls to val_ptr_add and val_alloc.

Moreover, we customize the behavior of the "*" suffix that appears in next to Coq tactics, for this symbol to trigger not a call to eauto but instead a call to eauto with maths.

Here are the proofs for the small-footprint specifications.

Then, the proofs of specifications operating on array segments (hseg).