First Pass

This chapter introduces support for reasoning about arrays and records. In the first part of this chapter, we present the representation predicates for these structures, and present the statement of the specifications associated with operations on arrays and records. In the second part of this chapter, we show how these specifications can be realized, with respect to a memory model that exposes a representation of headers for allocated blocks. More precisely, we show how to implement array and record operations using a pointer arithmetic primitive operation, and we establish the correctness of the specifications with respect to the semantics of the allocation, deallocation, and pointer arithmetic operations. The memory model that we consider is somewhat artificial, in the sense that it does not perfectly match the memory model of an existing language----it lies somewhere between the memory model of C and that of OCaml. Nevertheless, this memory model has the benefits of its simplicity, and it suffices to illustrate formal proofs involving block headers and pointer arithmetics.

Representation of a Set of Consecutive Cells

The cells from an array of length k can be represented as a range of k consecutive cells, starting at some location p. In other words, the array cells have addresses from p inclusive to p+k exclusive. The heap predicate hcells L p represents a consecutive set of cells starting at location p and whose elements are described by the list L. The length of the list L corresponds to the length of the array. On paper, we could write something along the lines of: \bigstar_{x at index i in L} { (p+i) ~~> x }. In Coq, we define the predicate hcells L p by recursion on the list L, with the pointer p incremented by one unit at each cell, as follows.

The description of a set of consecutive cells can be split in two parts, at an arbitrary index. Concretely, if we have hcells (L₁++L₂) p, then we can separate the left part hcells L₁ p from the right part hcells L₂ q, where the address q is equal to p + length L₁. Reciprocally, the two parts can be merged back into the original form at any time.

This "splitting lemma for arrays" is useful for carrying out local reasoning on arrays. For example, in the recursive quicksort algorithm, the specification requires a description of the segment to be sorted; the representation of this segment is split so that subsegments can be provided for reasoning about the recursive calls. One thereby obtains for free the fact that the cells outside of the targeted segment remain unmodified.

Representation of an Array with a Block Header

An array consists of a "header", and of the description of its cells. The header is a heap predicate that describes the length of the array.

• In OCaml, the header consists of a physical memory cell at the head of the array. This cell may be queried to obtain the length of the array.
• In C, the header is a logical notion. It describes the length of the allocated block, and it used in Separation Logic to specify the behavior of the deallocation function, which can only be called on the address of an allocated block, deallocating the full block at once.

In this course, we follow the OCaml view, with physical headers. The predicate hheader k p asserts the existence of an allocated block at location p, such that the contents of the block is made of k cells, not counting the header cell. For the moment, we leave its definition abstract.

The heap predicate hheader k p should capture the information that p is not null. Indeed blocks cannot be allocated at the null location.

An array is described by the predicate harray L p, where the list L describes the contents of the cells. This heap predicate covers both the header, which describes a block of length equal to length L, and the contents of the cells, described by hcells L (p+1). Note that p+1 corresponds to the address of the first cell of the array, located immediately past the header cell that sits at location p.

Specification of Allocation

The primitive operation val_alloc k allocates a block made of k consecutive cells.

The operation val_alloc k is specified as producing an array whose cells contain the special "uninitialized value", written val_uninit. The assume val_uninit to be part of the grammar of values.
    Check val_uninit : val. More precisely, the postcondition of val_alloc k is of the form funloc p ⇒ harray L p, where the list L is defined as the repetition of k times the value val_uninit. This list is written LibList.make k val_uninit.

In practice, the operation val_alloc is applied to a non-negative integer, which might not necessarily be syntactically a natural number. Hence, the following lemma, which specifies val_alloc n for n ≥ 0, is more handy to use.

The specification above turns out to be often unnecessarily precise. For most applications, it is sufficient for the postcondition to describe the array as harray L p for some unspecified list L of length n. This weaker specification is stated and proved next.

Remark: in OCaml, one must provide an initialization value explicitly, so there is no such thing as val_uninit; in JavaScript, val_uninit is called undefined; in Java, arrays are initialized with zeros; in C, uninitialized data should not be read. In that language, one would typically implement this policy by restricting the evaluation rule for the read operation, adding a premise of the form v ≠ val_uninit to ensure that uninitialized values cannot be read.

Specification of the Deallocation

The deallocation operation val_dealloc p deallocates the block allocated at location p.

The specification of val_dealloc p features a precondition that requires an array of the form harray L p, and an empty postcondition.

Observe that the harray L p predicate includes a header of the form hheader k p, ensuring that a block can be deallocated only once.

Specification of Array Operations

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 nth (abs i) L, and mentions the unmodified array, still described by harray L p.

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 update (abs i) v L.

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

There are two useful specifications for val_array_length. The first one operates with the heap predicate harray L p. The return value is the length of the list L.

The second specification for val_array_length operates only on the header of the array. This small-footprint specification is useful to read the length of an array whose cells are described by separated segments, that is, after hcells_concat_eq has been exploited.

Representation of Individual Records Fields

A record can be represented just like an array, with the field names corresponding to offsets in that array. We let field denote the type of field names, an alias for nat.

For example, consider a mutable list cell allocated at location p. It is represented in memory as:

• a header at location p, storing the number of fields, that is, the value 2;
• a cell at location p+1, storing the contents of the head field,
• a cell at location p+2, storing the contents of the tail field.

Concretely, the record can be represented by the heap predicate: (hheader 2 p) \* ((p+1) ~~> x) \* ((p+2) ~~> q). To avoid exposing pointer arithmetic to the end-user, we introduce the "record field" notation p`.k ~~> v to denote (p+1+k) ~~> v. For example, with the definition of the field offsets head := 0 and tail := 1, the same record as before can be represented as: (hheader 2 p) \* (p`.head ~~> x) \* (p`.tail ~~> q).

Representation of Records

Describing, e.g., a list cell record in the form (hheader 2 p) \* (p`.head ~~> x) \* (p`.tail ~~> q) in particularly verbose and cumbersome to manipulate. To improve the situation, we next introduce generic representation predicate for records that allows to describe the same list cell much more concisely, as p ~~~>`{ head := x; tail := q }. It what follows, we show how to implement this notation by introducing the heap predicates hfields and hrecords. We then represent the specifications of record operations with respect to those predicates. A record field is described as the pair of a field and a value stored in this field.

A record consists of a list of fields.

We let the meta-variable kvs denote such lists.

A list cell with head field x and tail field q is represented by the list (head,x)::(tail,q)::nil. To support the syntax `{ head := x; tail := q }, we introduce the following notation.

The heap predicate hfields kvs p asserts that, at location p, one finds the representation of the fields described by the list kvs. The predicate hfields kvs p is defined recursively on the list kvs. If kvs is empty, the predicate describes the empty heap predicate. Otherwise, it describes a first field, at offset k and with contents v, as the predicate p`.k ~~> v, and it describes the remaining fields recursively.

The heap predicate hrecord kvs p describes a record: it covers not just all the fields of the record, but also the header. The cells are described by hfields kvs p, and the header is described by hheader z p, where nb should be such that the keys in the list kvs are between 0 inclusive and nb exclusive. A permissive definition of hrecord kvs p would allow the fields from the list kvs to be permuted arbitrarily. Yet, to avoid complications related to permutations, we make in this course the simplifying assumptions that fields are always listed in the order of their associated offsets. The auxiliary predicate maps_all_fields z kvs asserts that the keys from the association list kvs correspond exactly to the sequence made of the first nb natural numbers, that is, 0; 1; ...; nb-1.

The predicate hrecord kvs p exploits maps_all_fields z kvs to relate the value nb stored in the header with the association list kvs that describes the contents of the fields.

The heap predicate hrecord kvs p captures in particular the invariant that the location p is not null.

We introduce the notation p ~~~> kvs for hrecord kvs p, allowing to write, e.g., p ~~~>`{ head := x; tail := q }.

Example with Mutable Linked Lists

Recall the definition of the representation predicate MList, which was introduced in Basic.

Recall the statement of the lemma MList_if, which reformulates the definition of MList with a case analysis on p = null. Observe the use of the lemma hrecrod_not_null to exploit the fact that a record cannot be allocated at the null location.

Reading in Record Fields

The read operation is described by an expression of the form val_get_field k p, where k denotes a field name, and where p denotes the location of a record. Technically, val_get_field k is a value, and this value is applied to the pointer p. Hence, val_get_field has type field → val.

The read operation val_get_field k p is abbreviated as p`.k.

The operation val_get_field k p can be specified at three levels. First, its small-footprint specification operates at the level of a single field, described by p`.k ~~> v. The specification is very similar to that of val_get. The return value is exactly v.

Second, this operation can be specified with respect to a list of fields, described in the form hfields kvs p. To that end, we introduce a function called hfields_lookup for extracting the value v associated with a field k in a list of record fields kvs. The operation hfields_lookup k kvs returns a result of type option val, because we cannot presume that the field k occurs in kvs, even though it is always the case in practice.

Under the assumption that hfields_lookup k kvs returns Some v, the read operation val_get_field k p is specified to return v. The corresponding specification appears below.

Third and last, the read operation can be specified with respect to the predicate hrecord kvs p, describing the full record, including its header. The specification is similar to the previous one.

Writing in Record Fields

The write operation is described by an expression of the form val_set_field k p v, where k denotes a field name, and where p denotes the location of a record, and v is the new value for the field.

The write operation val_get_field k p v is abbreviated as Set p`.k ':= v.

Like for the read operation, the write operation can be specified at three levels. First, at the level of an individual field.

Then, at the level of hfields and hrecord. To that end, we introduce an auxiliary function called hrecord_update for computing the updated list of fields following an write operation. Concretely, hrecord_update k w kvs replaces the contents of the field named k with the value w. It returns some description kvs' of the record fields, provided the update operation succeeded, i.e., provided that the field k on which the update is to be performed actually occurs in the list kvs.

The specification in terms of hfields is as follows.

The specification in terms of hrecord is similar.

Allocation of Records

Because records are internally described like arrays, records may be allocated and deallocated using the operations val_alloc and val_dealloc, just like for arrays. That said, it is useful to express derived specifications for these two operations stated in terms of representation predicate hrecord, which describes a full record in terms of the list of its fields. For allocation, one needs to provide, at some point, the fields names for the record being allocated. These fields names may be described by a list of field names of type list field. This list, written ks, should be equivalent to a list of consecutive natural numbers 0 :: 1 :: ... :: n-1, where n denotes the number of fields. The interest of introducing the list ks is to provide readable names in place of numbers. The operation val_alloc_hrecord ks is implemented by invoking val_alloc on the length of ks.

The specification of val_alloc_hrecord ks involves an empty precondition and a postcondition of the form hrecord kvs p, where the list kvs maps the fields names from ks to the value val_uninit. The premise expressed in terms of nat_seq ensures that the list ks contains consecutive offsets starting from zero. In the statement below, LibListExec.length is a variant of LibList.length that computes in Coq (using simpl or reflexivity). Likewise for LibListExec.map, which is equivalent to LibList.map.

For example, the allocation of a list cell is specified as follows.

Deallocation of Records

Deallocation of a record, written val_dealloc_hrecord p, is implemented as val_dealloc p.

The specification of this operation simply requires as precondition the full record description, in the form hrecord kvs p, and yields the empty postcondition.

To improve readability, we introduce the notation Delete p for record deallocation.

For example, the following corollary to triple_dealloc_hrecord may be used to reason about the deallocation of a list cell.

Combined Record Allocation and Initialization

It is often useful to allocate a record and immediately initialize its fields. To that end, we introduce the operation val_new_hrecord, which applies to a list of fields and to values for these fields. This operation can be defined in an arity-generic way, yet, to avoid technicalities, we only present its specialization for arity 2.

In the definition below, the expression in braces val_alloc_hrecord (k₁::k₂::nil) refers to a Coq term, embedded in the syntax of program terms.

To improve readability, we introduce notation to allow writing, e.g., `{ head := x; tail := q } for the allocation and initialization of a list cell.

This operation is specified as follows.

For example, the operation mcons x q allocates a list cell with head value x and tail pointer q.

More Details

Extending xapp to Support Record Access Operations

The tactic xapp can be refined to automatically invoke the lemmas triple_get_field_hrecord and triple_set_field_hrecord, which involve preconditions of the form hfields_lookup k kvs = Some v and hfields_update k v kvs = Some ks', respectively. The auxiliary lemmas reformulate the specification triples in weakest-precondition form. The premise takes the form H ==> \∃ kvs, (hrecord kvs p) \* match ... with Some .. ⇒ ... This presentation enables using xsimpl to extract the description of the record, named kvs, before evaluating the lookup or update function for producing the suitable postcondition.

Deallocation Function for Lists

Recall that our Separation Logic set up enforces that all allocated data eventually gets properly deallocated. In what follows, we present a function for recursively deallocating an entire mutable list.

The operation mfree_list deallocates all the cells in a given list. It is implemented as a recursive function that invokes mfree_cell on every cell that it traverses.     let rec mfree_list p =
      if p != null then begin
        let q = p.tail in
        delete p;
        mfree_list q
      end

The precondition of mfree_list p requires a full list MList L p. The postcondition is empty: the entire list is destroyed.

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

Verify the function mfree_list. Hint: the overall pattern of the proof follows that used for the function triple_mcopy, from chapter Repr.

Optional Material

The aim of this bonus section is to show how to establish the specifications presented in this chapter. To that end, we consider an extended language, featuring the operations val_alloc and val_dealloc, which operates on blocks of cells.

Refined Source Language

We assume that every allocated block features a "header cell", represented explicitly in the memory state. To describe this header cell, we introduce a special value, written val_header k, where k denotes the length of the block that follows the header.

Note that values of the form val_header k should never be introduced by source terms. They are only introduced in heaps by the evaluation of val_alloc, and they should never leak in program terms. The operation val_alloc k is specified as shown below. Starting from a state sa, it produces a state sb \u sa (i.e., the union of sb and sa), where sb consists of consecutive of k+1 consecutive cells. The head cell stores the special value val_header k, while the k following cells store the special value val_uninit, describing uninitialized cells.

The operation val_dealloc p is specified as shown below. Assume a state of the form sb \u sa, where sb consists of consecutive of k+1 consecutive cells. Assume the first of these cells to store the special value val_header k. Then, the deallocation operation removes the block described by sb, and leaves the state sa.

Rather than extending the language with primitive operations for reading and writing in array cells and record fields, we simply include a pointer arithmetic operation, named val_ptr_add, and use it to encode all other access operations.

The operation val_ptr p n applies to a pointer p and an integer n, and returns the address p+n.

Note that the specification above allows the integer n to be negative, as long as p+n is nonnegative. That said, thereafter we only apply eval_ptr_add to nonnegative arguments. We also introduce the primitive operation val_length p, which returns the number stored in the header block at address p. This operation is useful to implement the function val_array_length, which reads the length of an array.

Realization of hheader

The heap predicate hheader k p describes a cell at location whose contents is the special value val_header k, and with the invariant that p is not null. hheader k p is defined as p ~~> (val_header k) \* \[p ≠ null].

Like other heap predicates, the definition of hheader is associated with an introduction and an elimination lemma.

The heap predicate hheader k p captures the invariant p ≠ null.

The definition of hheader is meant to show that one can prove all the specifications axiomatized so far. Note, however, that this definition should not be revealed to the end user. In other words, it should be made "strongly opaque". (Technically, this could be achieved by means of a functor in Coq.) Otherwise, the user could exploit the val_set operation to update the contents of a header field, replacing p ~~> (val_header k) with p ~~> v for another value v, thereby compromising the invariants of the memory model.

Introduction and Elimination Lemmas for hcells and harray

The heap predicates hcells and harray have their introduction and elimination lemmas stated as follows. These lemmas are useful for establishing the specifications of the allocation and of the deallocation operations.

Proving the Specification of Allocation and Deallocation

Following the usual pattern, we first establish a reasoning rule for allocation at the level of Hoare logic.

We then derive the Separation Logic reasoning rule.

The two corollaries to triple_alloc_nat follow. The first one applies to an integer argument, as opposed to a natural number.

The second corollary weakens the postcondition by not specifying the contents of the allocated cells.

We also establish the specification of deallocation, first w.r.t. Hoare triples, then w.r.t. Separation Logic triples.

Splitting Lemmas for hcells

The description of the cells of an array can be split in pieces, allowing to describe only portions of the array.

In order to reason about the read or write operation on a specific cell, we need to isolate this cell from the other cells of the array. Then, after the operation, we need to fold back to the view on the entire array. The isolation process is captured in a general way by the following "focus lemma". It reads as follows. Assume hcells L p to initially describe a segment of an array. Then, the k-th cell from this segment can be isolated as a predicate (p+k) ~~> v, where v denotes the k-th item of L, that is LibList.nth k L. What remains of the heap can be described using the magic wand operator as ((p+k) ~~> v) \−∗ (hcells L p), which captures the idea that when providing back the cell at location p+k, one regains the ownership of the original segment. The following statement describes a focus lemma.

The above lemma is, however, limited to read operations. Indeed, it imposes the cell (p+k) ~~> v to be merged back into the array segment, without modification to the original contents v. The lemma can be generalized into a form that takes into account the possibility of folding back the array segment with a modified contents for the cell at p+k, described by (p+k) ~~> w, for any value w. The updated segment gets described as update k w L.

The above focus lemma immediately extends to a full array described in the form harray L p.

Specification of Pointer Arithmetic

The operation val_ptr_add p n adds an integer n to the address p. This operation is used for encoding array and record operations by accessing cells at specific offsets. The specification of val_ptr_add directly reformulates the evaluation rule. It is established following the usual pattern for primitive operations.

The following lemma specializes the specification for the case where the argument n is equal to a natural number k. This reformulation avoids the abs function, and is more practical for the encodings that we consider further in the subsequent sections.

Specification of the length Operation to Read the Header

To establish triple_length, we follow the same proof pattern as for triple_get.

Encoding of Array Operations using Pointer Arithmetic

An access to the i-th cell of an array at location p can be encoded as an access to the cell at location p+i+1.

Let's first state and prove two auxiliary arithmetic lemmas that are needed in the proofs below.

The length operation on an array, written val_array_length p, is encoded as val_length p, where val_length is the primitive operation for reading the contents of a header.

The get operation on an array, written val_array_get p i, is encoded as val_get (p+i+1).

The set operation on an array, written val_array_set p i v, is encoded as val_set (p+i+1) v.

Encoding of Record Operations using Pointer Arithmetic

An access to the k-th field of a record at location p can be encoded as an access to the cell at location p+k+1.

The get operation on a field, written p`.k, is encoded as val_get (p+k+1).