First Pass

This chapter explains how to specify operations on ML-style records in Separation Logic. In ML-like languages, a record is an allocated object whose header field stores the number of fields of the record. Concretely, each field is stored at a specific offset relative to the header. 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.

Thus, at a low level, such a 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 predicate hfield p k v, written p`.k ~~> v, to describe the contents of the field named k of the record at location p. The chapter starts by presenting the representation predicate hfield, as well as a higher-level predicate named hrecord for describing all fields at once. The second part of the chapter presents the specification of access and allocation operations. The last part explains how to implement and verify these operations using block allocation and pointer arithmetic.

Representation of Individual Record Fields

Let us assume that each field name corresponds to a nonnegative offset. Let field denote the type of field names, an alias for nat.

The predicate hfield p k v, written p`.k ~~> v, asserts that the field k of the record p stores the value v. This predicate is presented as an abstract predicate to the end user. Internally, it may be defined using pointer arithmetic.

Writing (hheader 2 p) \* (p`.head ~~> x) \* (p`.tail ~~> q) to describe a list cell record is fairly verbose and cumbersome to manipulate. To improve the situation, we introduce a generic representation predicate for records. This predicate allows us 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. These predicates will be used for stating both small-footprint and large-footprint specifications for record operations.

Representation of Sets of Fields

A record field is described as the pair of a field and a value stored in this field.

A record is described as a list of fields.

We let the meta-variable kvs range over such lists.

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, kvs decomposes as a head (k,v) and a tail kvs'. The predicate p`.k ~~> v describes the field at offset k, with contents v. The predicate hfields kvs' p describes the remaining fields.

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. For technical reasons associated with coercions, we need to separately define notation for parsing, where a cast to the type val is included, from notation for printing, where such a cast is not included.

Representation of Records

The heap predicate hrecord kvs p describes a record by covering 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 n p, where n should be such that the keys in the list kvs are between 0 inclusive and n exclusive. A permissive definition of hrecord kvs p would allow the fields from the list kvs to be permuted arbitrarily. However, to avoid complications related to permutations, we make in this course the simplifying assumptions that fields are always listed in the order of their 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 n natural numbers, that is, 0; 1; ...; n-1.

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

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

The following lemma may be used to convert a concrete hrecord predicate into a hheader and a conjunction of hfield predicates. In the statement below, LibListExec.length is a variant of LibList.length that computes in Coq using simpl or reflexivity.

For example, let us show how to convert from p ~~~> `{ head := x ; tail := q } to the conjunction of hheader 2 p and p`.head ~~> x and p`.tail ~~> q.

Reasoning about Reads from 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 p denotes the location of a record. Observe that k is not a program value of type val, but rather a name for a natural number. The expression val_get_field has type field → val, and for a given field k the expression val_get_field k is a value, which may be applied in the program syntax to a pointer p.

The read operation val_get_field k p is written 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, the read operation val_get_field 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. Note that the operation hfields_lookup k kvs returns an option val, because we cannot presume that the field k occurs in kvs.

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

Third, the read operation val_get_field can be specified with respect to the predicate hrecord kvs p, describing the full record, including its header. The corresponding specification shown below follows a similar pattern as the specification of hfield.

Reasoning about Writes To 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 where v is the new value for the field.

The operation val_set_field k p v is abbreviated Set p`.k ':= v.

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

Alternatively, it may be specified in terms of hfields or hrecord, using an auxiliary function called hrecord_update. This function computes an updated list of fields to reflect the action of a write operation. Concretely, hrecord_update k w kvs replaces the contents of the field named k with the value w. It returns a 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 follows a similar pattern.

Reasoning about Record Allocation with Initializers

In ML, records may only be allocated by providing values to initialize every field. This allocation operation can be defined in an arity-generic way. However, to avoid technicalities, we here present only its specialization for arity 2. For example, the notation `{ head := x; tail := q } stands for the term (val_new_hrecord_2 head tail) x q. Here, val_new_hrecord_2 is a Coq function that expects two names as arguments and produces a value. For example, the expression val_new_hrecord_2 head tail is a value that may be applied to two arguments in the program syntax.

The record allocation operation `{ k<sub>1</sub> := v<sub>1</sub> ; k<sub>2</sub> := v<sub>2</sub> } is specified as follows. The premises k<sub>1</sub> = 0 and k<sub>2</sub> = 1 enforce the field names to be provided in increasing order, starting from zero. The postcondition describes a record at address p using the predicate p ~~~> `{ k₁ := v₁ ; k₂ := v₂ }, i.e., hrecord ((k₁,v₁)::(k₂,v₂)::nil) p.

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

This completes the presentation of the formalization of the mechanisms for reasoning about records. These mechanisms were illustrated throughout the chapter Repr.

Optional Material

In this section, we explain how val_get_field, val_set_field, and val_new_hrecord_2 can be realized in terms of block allocation and pointer arithmetic, following the same approach as in the previous chapter on arrays. In particular, we use a similar proof set up.

Implementation of Record Accesses using Pointer Arithmetic

The get operation on a field, written p`.k, is encoded as val_get (p+1+k). In the definition shown below, the braces around nat_to_Z k are used to embed the Coq natural number k into the code, in the form of an integer represented in the grammar of terms using the implicit coercion val_int.

The set operation on a field, written Set p`.k := v, is encoded as val_set (p+1+k) v.

Specification of Record Accesses w.r.t. hfields

The specifications triple_get_field and triple_set_field proved in the previous section correspond to small-footprint specifications, with preconditions mentioning a single field. Corollaries to these specifications can be established with preconditions mentioning a list of fields, with preconditions expressed using hfields.

Specification of Record Accesses w.r.t. hrecord

This section further refines the specification for val_get_field and val_set_field, into specification expressed using hrecord. For val_get_field, the proof is straightforward.

For val_set_field, however, we need an auxiliary lemma about hfields_update, showing that the update operation preserves the names of the fields. This lemma is established in two steps.

We are then ready to derive the specification for val_set_field.

Implementation of Record Allocation without Initialization

Recall that a record with n fields is represented as a memory block of size n+1. The first memory cell in the block corresponds to the header, and stores the number of fields, that is, the value n. The n other cells store the value associated with each of the fields. The operation that allocates and initializes a fresh record with specific values can be implemented in two stages. The first function, named val_alloc_hrecord, takes a list of n field names, and allocates a record with n fields, with contents specified as "uninitialized". The second function, named val_new_hrecord, takes n field names and n values. It invokes the first function to allocate the record, then performs one write per field to store the provided values into the corresponding memory cells. The present section focuses on the first part, namely the allocation without initialization. The Coq value val_alloc_hrecord ks depends on a list of field names. This value corresponds to a function that, when applied to a unit argument, allocates a record with length ks fields. The operation (val_alloc_hrecord ks) () is only specified when ks corresponds to a list of names whose unfolding is of the form 0 :: 1 :: 2 :: ... (n-1). The implementation of this operation allocates a block of size n+1 at a fresh location p, then sets the header cell to the value n, then returns the address p. In the statement below, the expression {LibListExec.length ks} in braces computes in Coq the expression length ks, and inserts the result in the code as a constant integer -- that is, as a value of the form val_int (LibListExec.length ks).

A key auxiliary result asserts that, if kvs is a list of key-value pairs such that the keys correspond to consecutive field names, then a list of fields described as hfields kvs p corresponds to a range of consecutive cells as described by hrange (List.map snd kvs) (p+1), for the definition of hrange given in Arrays.

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 ks = nat_seq 0 (length ks) checks that the list ks contains consecutive offsets starting from zero. Recall that LibListExec.length is a variant of LibList.length that computes in Coq (using simpl or reflexivity). Likewise LibListExec.map is a computable version of LibList.map.

The interest of using the computable counterparts of the function length and map is that a call to simpl will yield exactly the expected result, with lists indexed using field names. For example, the allocation of a list cell is specified as follows.

Implementation of Record Allocation with Initialization

We now show the implementation of record initialization in the particular case of records with exactly 2 fields. Recall that val_new_hrecord_2 k₁ k₂ denotes a Coq value of type val, which may be applied in the grammar of terms to two arguments, x₁ and x₂. The definition below shows an implementation for val_new_hrecord_2. In this definition, 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.

This completes the verification of the implementation of record operations in terms of block allocation and pointer arithmetic. The generalization of val_new_hrecord_2 to handle arbitrary arities involves more technical meta-programming, beyond the scope of this course.

Extending xapp to Support Record Access Operations

This section generalizes the tactic xapp to enable it to automatically reason about read and write on records specified using hrecord. The lemma xapp_get_field_lemma reformulates the specification triple_get_field_hrecord in weakest-precondition form. Its statement takes the form: H ==> \∃ kvs, (hrecord kvs p) \* (match ... with Some .. ⇒ ..), where the match construct reflects the preconditions hfields_lookup k kvs = Some v.

Likewise, the lemma xapp_set_field_lemma reformulates the specification triple_set_field_hrecord. The assumption hfields_update k v kvs = Some ks' is also captured by a pattern matching.

The hook xapp_nosubst_for_records, invoked by xapp, is then implemented by exploiting the two lemmas above, in conjunction with xsimpl.

The above definition is the one used in LibSepReference. It was put to practice in the chapters Basic and Repr.