Arthur Charguéraud
email: arthur.chargueraud@inria.fr

Higher-Order Representation Predicates in Separation Logic

Keywords: D, 2, 4 [Software/Program Verification]: Formal methods Keywords Separation Logic, Representation Predicates

In Separation Logic, representation predicates are used to describe mutable data structures, by establishing a relationship between the entry point of the structure, the piece of heap over which this structure spans, and the logical model associated with the structure. When a data structure is polymorphic, such as in the case of a container, its representation predicate needs to be parameterized not just by the type of the items stored in the structure, but also by the representation predicates associated with these items. Such higher-order representation predicates can be used in particular to control whether containers should own their items. In this paper, we present, through a collection of practical examples, solutions to the challenges associated with reasoning about accesses into data structures that own their elements.

Introduction

Separation Logic [START_REF] Peter | Local reasoning about programs that alter data structures[END_REF][START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF] is a Hoare-style program logic that is particularly well-suited for modular verification of mutable data structures. In this logic, specifications are expressed in terms of representation predicates, which establish a relationship between the entry point of a structure, the piece of heap over which this structure spans, and the logical model associated with the structure (e.g., a sequence, a set, a map, etc.).

Separation Logic was originally presented as a first-order logic, and was subsequently extended to a higher-order setting [START_REF] Biering | BIhyperdoctrines, higher-order separation logic, and abstraction[END_REF]. This extension was motivated by two essential features associated with the possibility of quantifying over heap predicates, i.e., predicates over pieces of heap. The first one is abstraction: existential quantification over heap predicates gives the ability to hide the pieces of heap that are private to a data structure. The second is modularity: universal quantification over representation predicates gives the ability to specify a polymorphic data structure in terms of the representation predicate describing the elements stored in this structure. In this paper, we focus on modularity.

To illustrate the modularity offered by higher-order representation predicates, and to explain the challenges associated with them, we consider the classic example of queues. O'Hearn et al. [START_REF] Peter | Separation and information hiding[END_REF] present a representation predicate for queues that is parameterized by the heap predicate describing the elements stored in the queue. However, this parameterization could only take place at the metalevel, due to their use of a first-order logic. Biering et al. [START_REF] Biering | BIhyperdoctrines, higher-order separation logic, and abstraction[END_REF] describe the same example, this time in a higher-order Separation Logic, in which the heap predicate describing the elements can be quantified within the logic. Svendsen et al. [START_REF] Kasper Svendsen | Verifying generics and delegates[END_REF] present a slightly different representation predicate for queues, describing a queue storing program values as a list of mathematical values, establishing a connection between program values and their corresponding mathematical values through the representation predicate provided for describing the elements. We follow their approach.

The specification for push (enqueue) and pop (dequeue) operations on queues can be expressed as shown below. There, 𝑝 Queueof 𝑅 𝐿 denotes the representation predicate for a queue object allocated at location 𝑝; 𝑅 denotes the representation predicate for the elements; and 𝐿 denotes the list of mathematical values describing the queue-𝐿 is the model of the queue.

@𝑥𝑝𝑅𝑋𝐿. t𝑝

Queueof 𝑅 𝐿 ‹ 𝑥 𝑅 𝑋u ppush 𝑥 𝑝q t𝜆_. 𝑝 Queueof 𝑅 p𝐿`𝑋 :: nilqu @𝑝𝑅𝑋𝐿. t𝑝 Queueof 𝑅 p𝑋 :: 𝐿qu ppop 𝑝q t𝜆𝑥. 𝑝 Queueof 𝑅 𝐿 ‹ 𝑥 𝑅 𝑋u Above, '𝜆_. " denotes the unit value returned by push, and "𝜆𝑥. " denotes the value 𝑥 returned by pop. The heap predicate 𝑥 𝑅 𝑋 establishes a relationship between a program value 𝑥 and the corresponding mathematical value 𝑋, and describes a nonempty piece of heap in the case where 𝑥 corresponds to an object allocated in memory. In Svendsen et al.'s presentation, all values in the specification language (e.g. 𝑥 and 𝑋) belong to a global type called Val. By contrast, in this paper, we will assign proper types to the values involved (see §4.4).

In the specifications given above, observe the ownership transfer at play. The push operation migrates the ownership of an element, described by 𝑥 𝑅 𝑋, from the client to the queue data structure. Reciprocally, the pop operation gives back to the client the ownership of the element returned. This form of ownership transfer is very useful for the client of the data structure, who would otherwise be required to separately maintain, in addition to the queue representation predicate, an assertion describing the ownership of the elements stored in the queue.

Yet, the specification of a container data structure using a representation predicate that includes the ownership of the elements raises an important challenge. This challenge comes from the fact that a read in the data structure cannot simply return the ownership of the item read, otherwise multiple reads would lead to duplicating the owernership of this item. To illustrate the problem, consider the function peek, which returns the element at the head of the queue, but without taking it out of the queue. On the one hand, if the spec-ification of peek does not transfer ownership of the head element, then the client code will be prevented from inspecting the head element, effectively making peek useless. On the other hand, if the specification of peek transfers ownership of the head element, then the ownership of this element would be duplicated, thus the corresponding specification, shown below, would be incorrect.

(Incorrect) @𝑝𝑅𝑋𝐿. t𝑝 Queueof 𝑅 p𝑋 :: 𝐿qu ppeek 𝑝q t𝜆𝑥. 𝑝 Queueof 𝑅 p𝑋 :: 𝐿q ‹ 𝑥 𝑅 𝑋u

The magic wand, a traditional tool from Separation Logic [START_REF] Peter | Local reasoning about programs that alter data structures[END_REF][START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF], brings a solution to the specification of peek. The magic wand, written 𝐻 1 ´‹𝐻, describes a piece of heap, call it 𝐻 2 , such that, if 𝐻 2 is extended with 𝐻 1 , then the result would be exactly 𝐻. In other words, the heap predicate 𝐻 1 ‹ p𝐻 1 ´‹𝐻q can be converted into 𝐻. Using the magic wand, we can specify peek as follows.

t𝑝 Queueof 𝑅 p𝑋 :: 𝐿qu ppeek 𝑝q t𝜆𝑥. 𝑥 𝑅 𝑋 ‹ p𝑥 𝑅 𝑋 ´‹ 𝑝 Queueof 𝑅 p𝑋 :: 𝐿qqu This specification of peek is sufficient for most practical applications. Its only limitation is that, after a call to peek, the queue cannot be acted upon before the ownership of the head element has been given back to the queue. Indeed, the magic wand form does not match the pre-condition of other operations such as push or pop.

The magic wand can be used, like in the example of peek, to reason about containers in which a single piece of ownership is carved out. However, when multiple pieces need to be carved out independently, as it is the case for example with arrays that own their elements, the magic wand falls short of solving the challenge of reasoning about accesses. For the specific case of mutable lists, which have been used extensively in the Separation Logic literature, the introduction of list segments comes to the rescue. Yet, the notion of list segments does not generalize so easily to more complex tree-based and array-based data structures.

In this paper, we describe techniques for detaching the ownership of items from trees and arrays that own their elements, and also for carving out the ownership of entire subtrees from given trees. The main contributions of this paper are the following.

´Mutable lists: using them, we give a gentle introduction to higher-order representation predicate and present the rewriting rules that are useful in practice for reasoning about them. We have not found such material in prior publications.

´Arrays: we present a representation predicates for describing subsets of cells from an array that owns its elements, as well as rules for converting between a description where the array owns its elements and one where it does not. We illustrate such conversions using matrices that either have disjoint rows or possibly-aliased rows. We have not seen this type of conversions described in prior work, although they are needed in practice.

´Records: we present a systematic pattern for introducing higherorder representation predicates for records. These predicates allow us to control, on a field per field basis, whether the items stored in the fields should be owned. Such use of higher-order representation predicates for describing record fields that do not have a polymorphic type appears to be novel.

´Trees with holes and cut subtrees: we present a novel technique that allows us to detach the ownership of items stored in a tree, and also to detach the ownership of entire subtrees. This technique supports reasoning about trees that contain several missing pieces, and reasoning about the reattaching of items and subtrees that may have been modified or permuted arbitrarily.

´Polymorphic recursion: we show that a tree data structures involving polymorphic recursion can be very elegantly described using a higher-order representation predicate that is recursively applied to itself. As far as we know, this is the first formalization of a mutable data structure involving polymorphic recursion.

A majority (although not all) of the definitions presented in this paper have been formalized and put to practice using CFML [START_REF] Charguéraud | Characteristic formulae for the verification of imperative programs[END_REF][START_REF] Charguéraud | Characteristic formulae for the verification of imperative programs[END_REF]. This tool takes as input an un-annotated ML program and generates its characteristic formula, reflecting the program semantics as a Coq logical formula. The details of characteristic formulae is not relevant to this paper; only matters the fact that CFML provides a Coq library that includes a shallow embedding of Separation Logic in Coq, and that many of the examples presented in this paper have been formalized in that setting.

The paper begins with a short justification of the choice of the logic and the programming language used to present the examples, and with a presentation of the minimal background on Separation Logic required for reading this paper.

Logic and Source Language

The definitions of higher-order representation predicates requires a higher-order logic specification language. In this paper, we present the definitions of logical data types and of representation predicate assuming the logic of the Coq proof assistant [START_REF] Coq | The Coq proof assistant reference manual[END_REF]. Note, however, that these definitions could be similarly formalized in other generalpurpose, higher-order logic theorem provers.

The notion of representation predicates is not specific to any particular programming language. The choice of a concrete language for presenting data structures and example programs in this paper was guided by two constraints. First, because polymorphism plays a key role in this paper, we want a language that makes polymorphism explicit in the definitions of data types, and that supports polymorphic recursion. Second, for describing mutable lists and trees without introducing a cumbersome sum type that would clutter definitions, we want a language that includes null pointers.

As we do not know of a programming language that features both well-typed polymorphic recursion and null pointers, we consider an artificial language, the same one as used by CFML [START_REF] Charguéraud | Characteristic formulae for the verification of imperative programs[END_REF][START_REF] Charguéraud | Characteristic formulae for the verification of imperative programs[END_REF]. This language inherits the syntax and semantics of OCaml [START_REF] Leroy | The Objective Caml system[END_REF] but at the same time offers null pointers. For the purpose of ML type inference, we assume null to be polymorphic, i.e. to have type "@𝐴. 𝐴". However, once we have a well-typed ML program, we type-check it again using a different type system, called weak-ML ([3], Section 4.3), in particular to ensure that null can only be used in places where a pointer value is expected.

Weak-ML essentially consists of an erasure of ML in which all pointer values, including null, admit the constant type loc, and in which all functions admit the constant type func. The only role of weak-ML is to reflect program values other than pointers and functions at their corresponding type in the logic. For example, an OCaml value that is an option on a boolean in the program is described as an option on a boolean in Coq (the assertion language). Weak-ML is not meant to enforce any type safety property, it simply keeps track of the types of program values in order to reflect them in the Separation Logic. The fact that functions and dereferencing operations indeed return values of the type claimed by the programmer is verified through the Separation Logic reasoning. In summary, although the choice of this artificial programming language might be debatable, it is motivated by the existing formalizations conducted using CFML, and by the fact that the use of null pointers simplify many definitions. In any case, the ideas presented in this paper can be adapted to other programming language.

Background on Separation Logic

In Separation Logic, a heap predicate has type Heap Ñ Prop and characterizes a portion of the heap. The fundamental combinators for heap predicates are agnostic to the representation of heaps, that is, to the definition of the type Heap. These combinators can either be axiomatized, or they can be defined in a standard higher-order logic. The latter amounts to constructing a shallow embedding of Separation Logic in a standard higher-order logic. This was done for example in Coq (e.g. [START_REF] Charguéraud | Characteristic formulae for the verification of imperative programs[END_REF][START_REF] Nanevski | Polymorphism and separation in hoare type theory[END_REF]) and in Isabelle/HOL (e.g. [START_REF] Varming | Higher-order separation logic in isabelle/HOLCF[END_REF]). In this paper, we assume a shallow embedding construction.

The definitions of these combinators are shown below and explained next. There, ℎ denotes a heap, 𝐻 denotes a heap predicate, and 𝑃 denotes a proposition.

r𝑃 s " 𝜆ℎ. ℎ " H ^𝑃 𝐻1 ‹ 𝐻2 " 𝜆ℎ. Dℎ1ℎ2. ℎ1 K ℎ2 ^ℎ " ℎ1 Z ℎ2 ^𝐻1 ℎ1 ^𝐻2 ℎ2 D D𝑥. 𝐻 " 𝜆ℎ. D𝑥. 𝐻 ℎ
The pure heap predicate r𝑃 s characterizes an empty heap and at the same time asserts that 𝑃 holds. The empty predicate, written r s, is a shorthand for rTrues. Existential quantification is lifted to the level of heap predicates, taking the form D D𝑥. 𝐻. The separating conjunction (a.k.a. star) of two heap predicates takes the form 𝐻1 ‹ 𝐻2 and asserts that the heap can be partitioned in two disjoint parts: one that satisfies 𝐻1 and one that satisfies 𝐻2. Its definition involves two auxiliary notions: ℎ1 K ℎ2 asserts that the heaps ℎ1 and ℎ2 have disjoint domains; ℎ1 Z ℎ2 denotes the union of two disjoint heaps. Moreover, we write AE 𝑖P𝐼 𝐻𝑖 for iterating the separating conjunction on a collection of heap predicates p𝐻𝑖q𝑖P𝐼 .

Separation Logic also relies on a primitive heap predicate for describing an atomic piece of heap. The exact form of this predicate depends on the view of memory exposed by the programming language. In a low-level view of memory such as that of the C programming language, the type Heap is interpreted as a map from locations to machine words, and the heap predicate 𝑙 ãÑ 𝑛 asserts that the memory cell at location 𝑙 stores the word 𝑛. Building on top of this predicate, one can derive higher-level predicates describing, say, a record object laid out in memory.

In a high-level view of memory such as that of the OCaml programming language, the type Heap may be interpreted as an heterogeneous map from locations to values. We write 𝑝 Þ Ñ𝐴 𝑣 to describe a singleton heap binding 𝑝 to a value 𝑣 of type 𝐴.

We typically omit the type annotation. For example, we write 𝑝 Þ Ñ t|hd=𝑣; tl=𝑝1 |u to assert that a list-cell record with two fields storing the value 𝑣 and 𝑝 1 is allocated in memory at location 𝑝.

Here, 𝑝 and 𝑝 1 have type loc, and 𝑣 is a value of some type 𝑎, where 𝑎 is the logical type associated with the program value 𝑣.

Throughout the paper, we illustrate the use of heap predicates in the specification of functions. The specification of a function typically takes the form @𝑥. t𝐻u p𝑓 𝑥q t𝜆𝑦. 𝐻 1 u, where 𝑥 denotes the argument, 𝑦 denotes the output value, 𝐻 denotes the precondition describing the input heap, and 𝐻 1 denotes the postcondition describing the output heap. The Separation Logic triples are given their standard, total correctness interpretation. 1

Mutable Lists

We begin with the study of mutable lists, a simple data structure that nevertheless suffices to motivate and illustrate a number of challenges associated with higher-order representation predicates.

@ℎ 1 ℎ 2 . " 𝐻 ℎ 1 ℎ 1 K ℎ 2 ñ D𝑣ℎ 1 1 ℎ 3 . $ ' & ' % 𝑡 {ℎ 1 Zℎ 2 ó 𝑣 {ℎ 1 1 Zℎ 2 Zℎ 3 ℎ 1 1 K ℎ 2 K ℎ 3 𝑄 𝑣 ℎ 1 1

Implementation of Null-Terminated Mutable Lists

A mutable list consists of a sequence of cells. Each cell has a pointer to the next cell. The null pointer denotes the end of the list. More precisely, each cell is represented as a two-field record, with one field for the head, storing an element from the list, and one field for the back, storing a pointer to the rest of the list.

The code below shows the record data type, which is parameterized, followed by an example mutable list storing two integers.

type 'a cell = { mutable hd : 'a; mutable tl : 'a cell } let demo = { hd = 8; tl = { hd = 5; tl = null } }

Traditional, First-Order List Representation Predicate

In Separation Logic [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF], a mutable list is described by a heap predicate of the form Mlist 𝐿 𝑝, asserting that, at pointer 𝑝, there exists a list storing the values described by the list 𝐿. Here, 𝑝 is a logical value of type loc that describes a memory location, and 𝐿 is a logical value of type list 𝐴, for some type 𝐴. For example, the demo list defined in §4.1 is described by the heap predicate demo Mlist p8 :: 5 :: nilq.

To improve the readability of heap descriptions, we introduce an arrow notation that we will use for all heap predicates that have a main entry point. We let 𝑝 𝑄 be a notation for "𝑄 𝑝", that is, for the application of the predicate 𝑄 to the value 𝑝. In particular, we write 𝑝 Mlist 𝐿 in place of Mlist 𝐿 𝑝, to better suggest the intuition that "at 𝑝, we find a list described by 𝐿".

The heap predicate 𝑝 Mlist 𝐿 is defined by structural recursion over the list 𝐿, as shown below. When the list is null, the heap predicate simply asserts that 𝑝 must be null, in the empty heap. When the list 𝐿 is of the form 𝑥 :: 𝐿 1 , the heap predicate asserts the existence of a list cell described by the predicate 𝑝 Þ Ñ t|hd=𝑥; tl=𝑝 1 |u, where 𝑝 1 is the pointer to the tail of the list. Thus, 𝑝 1

Mlist 𝐿 1 describes the tail of the list.

𝑝

Mlist 𝐿 " match 𝐿 with | nil ñ r𝑝 " nulls

| 𝑥 :: 𝐿 1 ñ D D𝑝 1 . 𝑝 Þ Ñ t|hd=𝑥; tl=𝑝 1 |u ‹ 𝑝 1 Mlist 𝐿 1
Note that the star operator that appears in the above definition ensures that all list cells involved are disjoint from each other. Note also the use of the existential quantification on 𝑝 1 , which introduces abstraction by hiding the locations of the intermediate list cells.

To illustrate a function specification involving Mlist, consider the function copy, which copies a mutable list. This function admits the specification shown below, where 𝑝 is the pointer to the input list and 𝑝 1 is the pointer on the output list.

@𝑝𝐿. t𝑝

Mlist 𝐿u pcopy 𝑝q t𝜆𝑝 1 . 𝑝 Mlist 𝐿 ‹ 𝑝 1 Mlist 𝐿u

The specification above asserts in particular that the cells of the output list are disjoint from the cells of the input list, and that the input list was left unaltered by the copy process.

Towards Higher-Order List Representation Predicate

Consider the case of a program that manipulates a mutable list of disjoint mutable lists. To reason about such a data structure, it can be convenient to establish a direct relationship between the entry pointer to the outer list, and the logical representation of the data structure, which is a list of lists, that is, a logical value of type list plist 𝐴q. We are thus seeking for a heap predicate, written MlistofMlist, to relate a pointer 𝑝 with a list of lists. For example, a concrete instance of such a predicate might be:

𝑝

MlistofMlist pp5 :: 7 :: nilq :: p8 :: 3 :: nilq :: pnilq :: p4 :: nilq :: nilq.

There are two main approaches to defining the heap predicate

MlistofMlist. The first approach consists of describing first the outer list, and then describing the iterated separating conjunction of the inner lists. In the formal definition shown below, 𝐾 has type list loc and describes the list of the pointers stored in the outer list, whereas 𝐿 has type list plist 𝐴q, for some 𝐴, and describes the list of the inner lists. In the definition shown below, |𝐿| denotes the length of 𝐿, and the iterated star asserts that the mutable list found at address 𝐾r𝑖s describes the list 𝐿r𝑖s.

𝑝

MlistofMlist 𝐿 " D D𝐾. r |𝐾| " |𝐿| s ‹ 𝑝 Mlist 𝐾 ‹ AE 𝑖 P r0, |𝐿|q p𝐾r𝑖sq

Mlist p𝐿r𝑖sq

A second approach to defining MlistofMlist is to generalize the definition of the predicate Mlist, to account for the fact that each element from the outer list is itself an entry point into a mutable list. In the definition shown below, 𝑥 has type loc and describes a pointer to one of the inner lists, whereas 𝑋 has type list 𝐴 and describes the logical representation of the corresponding list.

𝑝

MlistofMlist 𝐿 " match 𝐿 with | nil ñ r𝑝 " nulls

| 𝑋 :: 𝐿 1 ñ D D𝑥𝑝 1 . 𝑝 Þ Ñ t|hd=𝑥; tl=𝑝 1 |u ‹ 𝑝 1 MlistofMlist 𝐿 1 ‹ 𝑥 Mlist 𝑋
The two definitions presented above for MlistofMlist can be easily proved equivalent (by induction on 𝐿). Compared with the first definition, the second one generalizes better to the case of tree-shaped data structures (see §7). Hence, we thereafter follow the second approach. We will nevertheless exploit the equivalence between the two definitions on a few occasions.

In the example above, we considered the case of a mutable list of mutable lists. In general, we could have mutable lists of any kind of mutable objects, for example mutable lists of references, mutable lists of arrays, mutable lists of mutable queues, etc. In what follows, we generalize the definition of MlistofMlist to a higher-order predicate of the form Mlistof 𝑅, that is, a higherorder representation predicate for lists that takes as argument the representation predicate that applies to the elements.

Higher-Order List Representation Predicate

We define a higher-order representation predicate for lists, written 𝑝 Mlistof 𝑅 𝐿. This definition, which generalizes that of MlistofMlist simply by replacing Mlist with an abstract representation predicate 𝑅, is as follows.

𝑝

Mlistof 𝑅 𝐿 " match 𝐿 with | nil ñ r𝑝 " nulls

| 𝑋 :: 𝐿 1 ñ D D𝑥𝑝 1 . 𝑝 Þ Ñ t|hd=𝑥; tl=𝑝 1 |u ‹ 𝑝 1 Mlistof 𝑅 𝐿 1 ‹ 𝑥 𝑅 𝑋
This definition is highly polymorphic, so it is worth making explicit all the types involved. Recall that 𝑝 Mlistof 𝑅 𝐿 is a notation for Mlistof 𝑅 𝐿 𝑝, and that, similarly, 𝑥 𝑅 𝑋 is a notation for 𝑅 𝑋 𝑥. Recall also that both these heap predicates have type Hprop, that is Heap Ñ Prop. Let 𝑎 denote the type of the concrete values stored in the mutable list beginning at address 𝑝. The variable 𝑥 that appears in the definition has type 𝑎. Let 𝐴 denote the logical type associated with these concrete values. The variable 𝑋 that appears in the definition has type 𝐴 and 𝐿 has type list 𝐴. The abstract representation predicate 𝑅 thus has type 𝐴 Ñ 𝑎 Ñ Hprop, and Mlistof admits the following type:

Mlistof : @𝐴𝑎. p𝐴 Ñ 𝑎 Ñ Hpropq Ñ list 𝐴 Ñ loc Ñ Hprop.

Importantly, Mlistof is a strict generalization of Mlist, in the sense that we can define a heap predicate Id such that Mlistof Id yields exactly Mlist. The predicate Id is defined as follows:

Id " 𝜆𝑋. 𝜆𝑥. r𝑥 " 𝑋s.

Note that Id is polymorphic and has type @𝐴. 𝐴 Ñ 𝐴 Ñ Hprop.

For this definition of Id, we can prove the intended equality2 :

𝑝

Mlistof Id 𝐿 " 𝑝 Mlist 𝐿.

Now that we have defined Mlistof, it remains to see how we use it in practice to state specifications of functions manipulating mutable lists of possibly-mutable objects.

Example: a Higher-Order Copy Function

In §4.2, we considered a specification for a copy function that duplicates the structure of a list. A naive generalization of the specification, shown below, would be incorrect, because it would duplicate the ownership of the list items.

(Incorrect) @𝑝𝐿. t𝑝

Mlistof 𝑅 𝐿u pcopy 𝑝q

t𝜆𝑝 1 . 𝑝 Mlistof 𝑅 𝐿 ‹ 𝑝 1 Mlistof 𝑅 𝐿u
The problem is that the copy function considered only performs a shallow copy of the list, not a deep copy. If we really want to specify the behavior of the copy function on a list described by 𝑝

Mlistof 𝑅 𝐿, because of the sharing induced we first need to change the heap description to 𝑝

Mlist 𝐾 ‹ AE 𝑖 𝐾r𝑖s
Mlist 𝐿r𝑖s for some 𝐾, exploiting the equivalence stated in §4.3.

If, however, we consider a function that performs a deep copy of the list, then we can give an interesting specification in terms of 𝑝 Mlistof 𝑅 𝐿. Let deepcopy be a function that, while duplicating the list structure, makes calls to a given function 𝑓 for constructing copies of the elements. We can specify the higher-order function deepcopy as shown below. The first part of the specification describes the hypothesis made about the behavior of 𝑓 as a copy function for the elements, whereas the remaining part describes the pre-and post-condition associated with applications of deepcopy to 𝑓 and to a pointer 𝑝 on a mutable list.

@𝑓 𝑝𝑅𝐿.

`@𝑥𝑋. t𝑥 𝑅 𝑋u p𝑓 𝑥q

t𝜆𝑥 1 . 𝑥 𝑅 𝑋 ‹ 𝑥 1 𝑅 𝑋u ñ t𝑝 Mlistof 𝑅 𝐿u pdeepcopy 𝑓 𝑝q t𝜆𝑝 1 . 𝑝 Mlistof 𝑅 𝐿 ‹ 𝑝 1 Mlistof 𝑅 𝐿u

Example: Mutable List of Functions with Local State

In this example, we consider a mutable list of counter functions. These counter functions have an internal state implemented using a reference, but this reference is not directly accessible. We then traverse the list using a higher-order iterator, making a call to each of the counters to update their internal states.

A counter function is a function that, each time it is called, returns the next natural number. A fresh counter function can be constructed as shown below, by allocating a reference cell with initial value 0 and then returning a function that increments the counter and returns its current value. let mkcounter () = let r = ref 0 in (fun () -> incr r; get r)

We define a predicate, written 𝑓 Count 𝑛, to assert that the function closure 𝑓 denotes a counter whose current state is 𝑛. This heap predicate describes in particular the ownership of the local state of the function, that is, the reference cell associated with it. The predicate 𝑓 Count 𝑛 is defined as shown below. Note that 𝑓 is a value of type func (recall §2). Observe in particular how the concrete address of the reference cell implementing the state of the counter is existentially quantified.

𝑓

Count 𝑛 " D D𝑟. p𝑟 ãÑ 𝑛q ‹ r@𝑖. t𝑟 ãÑ 𝑖u p𝑓 ()q t𝜆𝑥. r𝑥 " 𝑖 `1s ‹ p𝑟 ãÑ 𝑖 `1qus

Instances of the predicate Count can be introduced for example by exploiting the specification of mkcounter, which is as follows.

tr su pmkcounter ()q t𝜆𝑓. 𝑓

Count 0u

The definition of 𝑓

Count 𝑛 is hidden from the end-user;

only the specification shown below is exposed. This specification asserts that a call to a counter 𝑓 increments its internal state, denoted as 𝑖, and returns the value of the new internal state.

t𝑓 Count 𝑖u p𝑓 ()q t𝜆𝑥. 𝑓 Count p𝑖 `1q ‹ r𝑥 " 𝑖 `1su

Remark: our specification of calls to the counter function is similar to that presented by Svendsen et al. [START_REF] Kasper Svendsen | Verifying generics and delegates[END_REF], although they do not attempt to hide the implementation of the inner state.

We are now ready to verify the following program, which allocates two counters, increments the first one, then creates a mutable list with the two counters, and iterates over the list a function that increments every counter. Below, miter denotes a higher-order iterator on mutable lists (its definition is not shown).

let a = mkcounter() in let b = mkcounter() in let n = a() in let p = { hd = a; tl = { hd = b; tl = null }} in miter (fun f -> ignore(f())) p
The state before the creation of the list 𝑝 is described by: 𝑎 Count 1 ‹ 𝑏 Count 0. The state after the creation of the list 𝑝 is described by: 𝑝 Mlistof Count p1 :: 0 :: nilq. The state after the iteration of the function (fun f -> f()) on each of the elements the list 𝑝 is described by: 𝑝 Mlistof Count p2 :: 1 :: nilq.

It remains to present the proof steps involved for reasoning about the call to miter. We show below the specification of miter. It is similar in spirit to the specification of a fold function presented by Svendsen et al. [START_REF] Kasper Svendsen | Verifying generics and delegates[END_REF]. Below, 𝐿 denotes the input (logical) list, 𝐿 1 denotes the output (logical) list, and 𝐼 denotes the loop invariant which relates the current state with the already-processed prefixes 𝐾 and 𝐾 1 of the lists 𝐿 and 𝐿 1 . The variable 𝑋 denotes an element from 𝐿, and 𝑓 denotes a counter, i.e. a concrete element stored in the mutable list. We use the notation p𝐾&𝑋q as a shorthand for 𝐾 `p𝑋 :: nilq.

@𝑔𝑝𝐼𝑅𝑅 1 𝐿. `@𝑓 𝑋𝐾𝐾 1 𝑇. 𝐿 " 𝐾 `𝑋 :: 𝑇 ñ t𝐼 𝐾 𝐾 1 ‹ 𝑓 𝑅 𝑋u p𝑔 𝑓 q t𝜆_. D D𝑋 1 . 𝐼 p𝐾&𝑋q p𝐾 1 &𝑋 1 q ‹ 𝑓 𝑅 1 𝑋 1 u ñ t𝑝 Mlistof 𝑅 𝐿 ‹ 𝐼 nil nilu pmiter 𝑔 𝑝q t𝜆_. D D𝐿 1 . 𝑝 Mlistof 𝑅 1 𝐿 1 ‹ 𝐼 𝐿 𝐿 1 u
In our example, 𝑓 is a pointer to a function closure, and "𝑔 𝑓 " reduces to an invocation of the counter, that is, to "ignore𝑓 pq". To reason about the call to miter, we exploit the above specification by taking 𝐿 " 1 :: 0 :: nil and 𝐿 1 " 2 :: 1 :: nil. We instantiate 𝑅 as Count and define 𝐼 such that: 𝐼 𝐾 𝐾 1 " r𝐾 1 " map p`1q 𝐾s.

The proof obligation arising from the premise, and associated with reasoning about the call to the function (fun f -> f()), is:

@𝑥𝐾𝐾 1 𝑋. tr𝐾 1 " map p`1q 𝐾s ‹ 𝑓 Count 𝑋u pignorep𝑓 pqqq t𝜆_. D D𝑋 1 . rp𝐾&𝑋q " map p`1q p𝐾 1 &𝑋 1 qs ‹ 𝑓 Count 𝑋 1 u
One can check that, if we instantiate 𝑋 1 as 𝑋 `1, and ignore the return value, then specification above is derivable from the exposed specification for counter functions stated earlier, that is:

t𝑓 Count 𝑖u p𝑓 ()q t𝜆𝑥. r𝑥 " 𝑖 `1s ‹ 𝑓 Count p𝑖 `1qu
In conclusion, the predicate Mlistof can be used to describe mutable lists, not only those storing plain pointer structures, but also those storing functions with local state. Moreover, as this example shows, a higher-order representation predicate such as

Mlistof can be smoothly integrated into the specification of higherorder iterators.

List Segments

In this section, we adapt the traditional list segment heap predicate to a higher-order representation predicate, following the same approach as for null-terminated lists.

Representation of List Segments

The

| 𝑋 :: 𝐿 1 ñ D D𝑥𝑝 1 . 𝑝 Þ Ñ t|hd=𝑥; tl=𝑝 1 |u ‹ 𝑝 1 Mlistsegof 𝑅 𝑞 𝐿 1 ‹ 𝑥 𝑅 𝑋
Note that null-terminated lists are a special case of list segments:

𝑝 Mlistof 𝑅 𝐿 " 𝑝 Mlistsegof 𝑅 null 𝐿.
We have experienced that the following equalities are very useful for reasoning about programs manipulating list segments.

null Mlistsegof 𝑅 𝑞 𝐿 " r𝐿 " nil ^𝑞 " nulls

𝑝 Mlistsegof 𝑅 𝑞 p𝐿1 `𝐿2q " D D𝑝 1 . 𝑝 Mlistsegof 𝑅 𝑝 1 𝐿1 ‹ 𝑝 1 Mlistsegof 𝑅 𝑞 𝐿2 𝑝 Mlistsegof 𝑅 𝑞 p𝐿&𝑋q " D D𝑥𝑝 1 . 𝑝 Mlistsegof 𝑅 𝑝 1 𝐿 ‹ 𝑝 1 Þ Ñ t|hd=𝑥; tl=𝑞|u ‹ 𝑥 𝑅 𝑋 𝑝 Mlistsegof 𝑅 𝐿 ‹r𝑝 ‰ nulls " D D𝑥𝑝 1 𝑋𝐿 1 . r𝐿 " 𝑋 :: 𝐿 1 s ‹ 𝑝 Þ Ñ t|hd=𝑥; tl=𝑝 1 |u ‹ 𝑝 1 Mlistsegof 𝑅 𝐿 1 ‹ 𝑥 𝑅 𝑋

Example: Getting and Reading the 𝑛-th Cell of a List

The function nth, whose code appears next, returns the 𝑖-th cell of a mutable list.

let rec nth (i:int) (p:'a cell) = if i = 0 then p else nth (i-1) (p.tl)

If the pre-condition for this function describes a full list of the form 𝑝 Mlistof 𝑅 𝐿, what could the post-condition be? The challenge is that the location returned by nth corresponds to one of the locations existentially quantified by Mlistof. For describing the post-condition, it appears that we have little choice but to introduce a list segment that splits the list at the location returned by nth. This can be done in two ways: either the list can be logically split between the pre-and the post-condition, or this split can be anticipated and be performed beforehand in the reasoning.

In the first case, the specification of nth takes the following form. Below, 𝑞 denotes the return value, and the list gets split into a prefix segment 𝑝 Mlistsegof 𝑅 𝑞 𝐿1 and a suffix 𝑞 Mlistof 𝑅 𝐿2. @𝑝𝐿𝑖. t𝑝

Mlistof 𝑅 𝐿 ‹ r0 ď 𝑖 ă |𝐿|su pnth i pq t𝜆𝑞. D D𝐿1𝐿2. 𝑝 Mlistsegof 𝑅 𝑞 𝐿1 ‹ 𝑞 Mlistof 𝑅 𝐿2 ‹ r𝐿 " 𝐿1 `𝐿2 ^|𝐿1| " 𝑖su
Note that the pieces from the post-condition can be merged back into the form 𝑝 Mlistof 𝑅 𝐿 by using the rewriting rule for concatenation of list segments presented near the end of 5.1.

In the second case, the specification of nth has a smaller footprint: it only describes the prefix segment 𝑝 Mlistsegof 𝑅 𝑞 𝐿 actually traversed by the function.

@𝑖𝑝𝐿. t𝑝

Mlistsegof 𝑅 𝑞 𝐿 ‹ r|𝐿| " 𝑖su pnth i pq t𝜆𝑟. 𝑝

Mlistsegof 𝑅 𝑞 𝐿 ‹ r𝑟 " 𝑞su

Although it requires the user to split ahead of time the list into list segments (which can be achieved using the same rewriting rule for concatenation of list segments), this second specification is much simpler to state.

Consider now the program "(nth i p).hd <-v", which calls the function nth to obtain the pointer to the cell at index 𝑖, and then updates the value stored in this cell. Starting from a heap described by 𝑝

Mlistof 𝑅 𝐿, we first argue that, if 𝑖 is a valid index in 𝐿, then 𝐿 can be decomposed as 𝐿1 `𝑋 :: 𝐿2. Using the rewriting rules from §5.1, we then change the heap predicate to:

𝑝 Mlistsegof 𝑅 𝑞 𝐿1 ‹ 𝑞 Þ Ñ t|hd=𝑥; tl=𝑟|u ‹ 𝑟 Mlistof 𝑅 𝐿2 ‹ 𝑥 𝑅 𝑋.
for some 𝑞, 𝑟 and 𝑥. Exploiting the second specification of nth shown above, we establish that the call to nth i p returns exactly the address 𝑞. The write operation on this cell thus involves the predicate 𝑞 Þ Ñ t|hd=𝑥; tl=𝑟|u. After reasoning about the write operation, the heap predicate may be folded back into an instance of Mlistof using the same rewriting rules in the other direction.

Example: Mutable Queues with an Abstract Interface

Through this example, we illustrate the use of list segments in the implementation of a mutable queue data structure. We also present an abstract interface for a mutable queue module, with an interface involving a higher-order representation predicate.

We implement a mutable queue as a list segment, maintaining two pointers: one on the head of the list, and one on the tail of the list. To avoid the need to treat specially the empty queue, we ensure that the underlying list is always made of at least one cell. To that end, we consider that the value stored in the last cell of the list is irrelevant. The record storing the head and tail pointers admits the following signature, where the type cell is that defined in §4.1.

type 'a queue = { mutable front : 'a cell; mutable back : 'a cell; }

We introduce the representation predicate 𝑝 Queueof 𝑅 𝐿, to assert that, at address 𝑝 in memory, there exists a mutable queue represented by the list 𝐿, when the elements stored are represented by the representation predicate 𝑅. The definition, shown below, asserts the existence of the queue record, the existence of the list segment that begins on the front pointer and reaches the back pointer, and the existence of the last cell, at the back of the queue, whose contents is ignored.

𝑝 Queueof 𝑅 𝐿 " D D𝑓 𝑏. 𝑝 Þ Ñ t|front=𝑓 ; back=𝑏|u ‹ 𝑓 Mlistsegof 𝑅 𝑏 𝐿 ‹ D D𝑥𝑦. 𝑏 Þ Ñ t|hd=𝑥; tl=𝑦|u
Figure 1 shows an abstract specification for a queue module. The function create produces a queue represented by the empty list. The function is_empty returns a boolean 𝑏 indicating whether the queue is empty. This function leaves the queue unaltered. The function push adds an element described by 𝑥 𝑅 𝑋 to the back of the queue. Note that push effectively transfers the ownership of 𝑥 to the queue.

The function pop extracts an element from the front of the queue. Symmetrical to push, pop transfers back to the client the ownership of the front element. A second specification is also provided for pop. Although this second specification is more verbose than the former, it is slightly more convenient to use in practice-it saves the need to perform, beforehand, a case analysis on the list.

The function peek returns the element at the front of the queue, without removing it from the queue. As explained in the introduction, this function can be elegantly specified using the magic wand. The magic wand, written 𝐻 1 ´‹𝐻, describes a piece of heap, call it 𝐻 2 , such that, if 𝐻 2 is extended with 𝐻 1 , then the result would be exactly 𝐻. It is defined as follows. (Remark: the equality that appears below could also be weakened into an entailment relation.)

𝐻 1 ´‹𝐻 " D D𝐻 2 . 𝐻 2 ‹ r𝐻 1 ‹ 𝐻 2 " 𝐻s
Last, the function transfer migrates all the elements from the second queue at the back of the first queue. It thus leaves the second queue empty.

Although we do not show the details here, we are able to prove that the particular queue implementation based on list segments described previously does satisfy the abstract specification for queues.

From First-Order to Higher-Order Specifications

The specifications of a mutable queue presented in Figure 1 account for the fact that the queue structure owns its elements. This ownership of the elements is very convenient for the client of the queue module. Indeed, if the specifications were not accounting for the ownership of the elements stored in the queue, then, during the verification process, we would need to separately maintain the ownership of a queue of pointer values, and a set of the elements contained in the queue. In practice, the use of a higher-order representation predicate typically saves a lot of proof effort to the client of a queue data structure.

However, for the implementer of queue data structures, the verification with respect to a higher-order representation predicate involves a little bit more work than the verification with respect to a first-order representation predicate. Indeed, with a first-order representation predicate, invariants and specifications are a slightly simpler, as they need not mention representation predicates for the elements, such as 𝑥 𝑅 𝑋. Interestingly, though, we can prove once and for all that any specification of a queue expressed using a first-order representation predicate can be turned into a specification expressed using a higher-order representation predicate. The idea is that, given any heap predicate of the form 𝑝 Queue 𝐿, we can derive a definition of 𝑝 Queueof 𝑅 𝐿 using a iterated star over the elements stored in the queue (recall §4.3), and we can then lift the specifications expressed in terms of 𝑝 Queue 𝐿 into corresponding specifications expressed in terms of 𝑝 Queueof 𝑅 𝐿. We give below an example below illustrating the lifting of the specifications of push. Recall that 𝐿&𝑋 is a shorthand for 𝐿`p𝑋 :: nilq. @ Queue. Note that the same kind of lifting lemma could be derived just as well for any other specification from Figure 1. In summary, specifications of a data structure with higher-order representation predicates are very useful for reasoning about client code, and there are two ways to establish them: either by verifying an implementation of the data structure directly with respect to the higher-order representation predicate, or by verifying it only with respect to a first-order representation predicate and then lifting the specifications to their higher-order counterparts. The second approach typically pays off when verifying several implementations that satisfy a same interface, e.g. several queue data structures.

Records

In the previous section, we introduced a higher-order representation predicate called Mlistof to describe mutable lists. In this section, we apply a similar idea to records. For each record type, we generate a higher-order representation predicate that controls, on a per-field basis, whether the contents of each field should be owned.

Representation Predicate for List Cells

Recall the definition of Mlistof from §4.4. This definition involves, for the case of nonempty lists, the following heap predicate:

D D𝑥𝑝 1 . 𝑝 Þ Ñ t|hd=𝑥; tl=𝑝 1 |u ‹ 𝑥 𝑅 𝑋 ‹ 𝑝 1 Mlistof 𝑅 𝐿 1 .
This predicate is made of three parts: (1) a heap predicate describing a single list cell made of two fields, (2) a heap predicate describing the contents of the first field of this record, and (3) a heap predicate describing the contents of the second field of this record. We introduce a higher-order representation predicate for list cells, written 𝑝 Mcellof 𝑅1 𝑉1 𝑅2 𝑉2. This predicate describes a list cell at location 𝑝, and relies on the representation predicates 𝑅1 and 𝑅2 for describing the content of the two fields. We thereby establish a direct relationship with the corresponding logical values 𝑉1 and 𝑉2 describing the logical content of the two fields. The predicate Mcellof is defined as follows.

𝑝 Mcellof 𝑅1 𝑉1 𝑅2 𝑉2 " D D𝑣1𝑣2. 𝑝 Þ Ñ t|hd=𝑣1; tl=𝑣2|u ‹ 𝑣1 𝑅1 𝑉1 ‹ 𝑣2 𝑅2 𝑉2
Remark: when writing 𝑝

Mcellof 𝑅1 𝑉1 𝑅2 𝑉2, the names of the fields hd and tl no longer appear explicitly. One could nevertheless set up a custom notation to make these names appear explicitly.

Using the predicate Mcellof, we revisit the definition of Mlistof and express it in a much more concise manner, as shown below.

𝑝

Mlistof 𝑅 𝐿 " match 𝐿 with | nil ñ r𝑝 " nulls

| 𝑋 :: 𝐿 1 ñ 𝑝 Mcellof 𝑅 𝑋 pMlistof 𝑅q 𝐿 1
Technical remark: it is no longer obvious that the definition of Mlistof shown above is structurally recursive on its argument 𝐿.

Nevertheless, Coq accepts it thanks to its ability to unfold on-thefly the definition of Mcellof when checking the guard condition. In §6.3, we will explain how to specify, in terms of Mcellof, read and write operations in record fields. But first, we consider the simpler case of references, which consist of single-field records.

Representation Predicate for References

A reference is a record with a single field named contents. The higher-order representation predicate for references is as follows.

𝑝

Refof 𝑅 𝑉 " D D𝑣. 𝑝 Þ Ñ t|contents=𝑣|u ‹ 𝑣 𝑅 𝑉

In general, given a heap described by 𝑝

Refof 𝑅 𝑉 , it is not possible to directly specify the behavior of a read operation into the reference without first making the existentially-quantified value 𝑣 appear explicitly. To make 𝑣 appear, it would suffice to unfold the definition of Refof. However, doing so would mean that the manipulation of references would involve two different predicates, one of the form 𝑝

Refof 𝑅 𝑉 and one of the form 𝑝 Þ Ñ t|contents=𝑣|u. We find it more effective to specify read and write operations on references only in terms of the predicate Refof.

Moreover, specifications expressed in terms of the representation predicate generalize better to the case of records with several fields.

To that end, we rely on the identity representation predicate Id. Recall from §4.4 that Id is defined as 𝜆𝑋𝑥. r𝑥 " 𝑋s. We have:

𝑝 Refof Id 𝑣 " 𝑝 Þ Ñ t|contents=𝑣|u.
Thus, when the heap is described by 𝑝 Refof Id 𝑣, we can specify that a read in 𝑝 returns exactly the value 𝑣. In summary, to read a reference described by a heap predicate 𝑝 Refof 𝑅 𝑣, we can first focus on its content field, by exploiting the equality:

𝑝

Refof 𝑅 𝑉 " D D𝑣. 𝑝 Refof Id 𝑣 ‹ 𝑣 𝑅 𝑉 then we can read in the reference using the predicate 𝑝 Refof Id 𝑣, obtaining the value 𝑣. Once we are done with manipulating 𝑣, and possibly after modifying the structure that 𝑣 might point to, we may fold back to the form 𝑝 Refof 𝑅 𝑉 1 , for some 𝑉 1 , by exploiting the same equality in the reverse direction.

The operations for creating, reading, and writing in focused reference are specified as follows. Note that these specifications are simply an alternative presentation of the axiomatic specifications of record operations, as provided by the program logic. Having a fine-grained control over which fields should be focused is particularly useful when a record has many fields but only a few of them need to be accessed, as it greatly reduces the number of variables that need to be introduced. The rewriting rule shown below allows one to focus on the first field when it is applied from left to right, and, symmetrically, to unfocus on this field when it is applied from right to left.

𝑝 Mcellof 𝑅1 𝑉1 𝑅2 𝑉2 " D D𝑣1. 𝑝 Mcellof Id 𝑣1 𝑅2 𝑉2 ‹ 𝑣1 𝑅1 𝑉1
Above, observe that, when operating on the first field, the second field can be either focused or unfocused: 𝑅2 may be any representation predicate, including Id. A symmetrical rule (not shown) allows for focusing or unfocusing on the second field of the record. Like we did previously for references (in §6.2), we provide specifications for read and write operations stated in terms of the predicate Mcellof. They are restricted to fields that are focused, i.e. that are represented using Id. For example, to read and write in the head field, we exploit the following specifications.

Mcellof Id 𝑤 𝑅2 𝑉2u

Note that the focus/unfocus rewriting rules and the specifications above are automatically generated by the tool CFML given the signature of the record that appears in the source code.

Here again, as done previously for references (in §6.2), we derive specifications that account for ownership transfer. For example, we show next the specifications of allocation and read operations.

t𝑣1 𝑅1 𝑉1 ‹ 𝑣2 𝑅2 𝑉2u pt|hd=𝑣1; tl=𝑣2|uq t𝜆𝑝. 𝑝 Mcellof 𝑅1 𝑉1 𝑅2 𝑉2u t𝑝 Mcellof 𝑅1 𝑉1 𝑅2 𝑉2u p𝑝.hdq t𝜆𝑣1. D D𝑅1. 𝑝 Mcellof Id 𝑣1 𝑅2 𝑉2 ‹ 𝑣1 𝑅1 𝑉1u
In summary, read and write operations on records can be assigned (at least) three different types of specifications: (1) specifications that operate on the low-level heap predicate 𝑝 Þ Ñ t|hd=𝑣1; tl=𝑣2|u, (2) specifications that operate on a focused predicate of the form 𝑝

Mcellof Id 𝑣1 𝑅2 𝑉2, and (3) specifications that perform on-the-fly focus operations starting from an unfocused predicate of the form 𝑝 Mcellof 𝑅1 𝑉1 𝑅2 𝑉2. As we argued, in order to limit the number of heap predicates, we choose to never manipulate the low-level heap predicate as in ( 1), but to only work in terms of Mcellof, using specifications of type ( 2) and (3).

We have found, when carrying proofs in CFML, that having access to both specifications of type ( 2) and ( 3) helps shorten the proof scripts significantly. That said, in a system with a sufficientlyhigh degree of automation for focus and unfocus operations, it might be possible for specifications of type (3) to be automatically derived from specifications of type [START_REF] Biering | BIhyperdoctrines, higher-order separation logic, and abstraction[END_REF], in which case only specifications of type ( 2) would need to be stated explicitly.

Trees

We next generalize our results from lists to trees. We begin with binary trees, in particular binary search trees, then cover n-ary trees, and bootstrapped trees, which involve polymorphic recursion. We also present a technique for specifying trees in which items or subtrees have been carved out.

Implementation of Binary Trees

We consider binary trees with items stored in the nodes, implemented as records with three fields, as shown below. Leaves are represented with the null value.

type 'a node = { mutable item : 'a; mutable left : 'a node; mutable right : 'a node; }

To describe such trees in the logic, we introduce a type of purely functional trees. In Coq, this datatype is defined as follows.

Inductive tree (A:Type) : Type := | Leaf : tree A | Node : A Ñ tree A Ñ tree A Ñ tree A.

Specification of Binary Trees

The representation predicate for binary trees follows the exact same construction as that of the predicate Mlistof introduced in §4.4.

𝑝

Mtreeof 𝑅 𝑇 " match 𝑇 with

| Leaf ñ r𝑝 " nulls | Node 𝑋 𝑇1 𝑇2 ñ D D𝑥𝑝1𝑝2. 𝑝 Þ Ñ t|item=𝑥; left=𝑝1; right=𝑝2|u ‹ 𝑥 𝑅 𝑋 ‹ 𝑝1 Mtreeof 𝑅 𝑇1 ‹ 𝑝2 Mtreeof 𝑅 𝑇2
Following the introduction of the higher-order representation predicate Mcellof for list cells (recall §6.1), we introduce a predicate Nodeof for describing node cells.

𝑝

Nodeof 𝑅1 𝑉1 𝑅2 𝑉2 𝑅3 𝑉3 " D D𝑣1𝑣2𝑣3. 𝑝 Þ Ñ t|item=𝑣1; left=𝑣2; right=𝑣3|u ‹ 𝑣1 𝑅1 𝑉1 ‹ 𝑣2 𝑅2 𝑉2 ‹ 𝑣3 𝑅3 𝑉3
Using Nodeof, the body of the definition of 𝑝 Mtreeof 𝑅 𝑇 can be simplified as follows.

𝑝

Mtreeof 𝑅 𝑇 " match 𝑇 with | Leaf ñ r𝑝 " nulls | Node 𝑋 𝑇1 𝑇2 ñ 𝑝 Nodeof 𝑅 𝑋 pMtreeof 𝑅q 𝑇1
pMtreeof 𝑅q 𝑇2

Binary Search Trees

A binary search tree is a binary tree satisfying specific invariants: smaller values in the left subtree, greater values in the right subtree. There are two approaches to enforcing those invariants. The first approach consists of extending the predicate Mtreeof to augment it with additional invariants. The second approach consists of reusing the predicate Mtreeof unchanged, and separately enforcing invariants on the logical tree (i.e. the tree written 𝑇 above). The second approach has two major benefits over the former: it enables us to share the definition of Mtreeof between all binary trees implementation, and it allows us to state and prove lemmas about tree operations completely outside of the Separation Logic fragment, that is, through reasoning that only involves pure predicates over logical trees. In what follows, we apply the second approach described above, first to the case of a binary search tree storing integers, and then to a binary search tree storing arbitrary mutable objects.

For the case of integers, we introduce a heap predicate, written 𝑝 Msearchtree 𝐸, to assert that the binary search tree rooted at location 𝑝 represents a set of integers 𝐸. This predicate asserts the existence of a pure tree 𝑇 , such that the tree rooted at 𝑝 describes 𝑇 , and such that 𝑇 satisfies the invariants of being a search tree representing 𝐸. The latter property is characterized by an auxiliary inductively-defined predicate, called search, which is parameterized by the order relation on the items, written ă. Note that, the representation predicate Mtreeof is applied to Id because in this first example the items are just integers and thus do not point to other pieces of heap. The definitions are as follows.

𝑝 Msearchtree 𝐸 " D D𝑇. 𝑝 Mtreeof Id 𝑇 ‹ rsearchă 𝑇 𝐸s searchă Leaf H search 𝑇1 𝐸1 search 𝑇2 𝐸2 @𝑦 P 𝐸1. 𝑦 ă 𝑥 @𝑦 P 𝐸2. 𝑥 ă 𝑦 searchă pNode 𝑥 𝑇1 𝑇2q pt𝑥u Y 𝐸1 Y 𝐸2q
For the case of trees with items that are arbitrary mutable objects, we need to assume a representation predicate 𝑅 for the items. We also need to specify the comparison function used for comparing items. It is specified as follows.

@𝑣1𝑣2𝑉1𝑉2. t𝑣1 𝑅 𝑉1 ‹ 𝑣2 𝑅 𝑉2u pcompare 𝑣1 𝑣2q t𝜆𝑛. 𝑣1 𝑅 𝑉1 ‹ 𝑣2 𝑅 𝑉2 ‹ rif 𝑛 " 0 then 𝑉1 " 𝑉2 else if 𝑛 ă 0 then 𝑉1 ă 𝑉2 else 𝑉2 ă 𝑉1s u
Remark: for simplicity, we assume here the existence of a total order over the items, although in general two items might be considered equivalent even when the items are not logically equal, and we moreover assume that comparison function to only depend on the items being compared, and not on a global state. The higher-order version of the binary search tree representation predicate, parameterized by ă and 𝑅, appears next.

𝑝

Msearchtreeofă 𝑅 𝐸 " D D𝑇. 𝑝 Mtreeof 𝑅 𝑇 ‹ rsearchă 𝑇 𝐸s Note that the above definition is polymorphic in both 𝑎, the type of items in the program, and 𝐴, the type at which items are described in the logic. The representation predicate 𝑅 has type 𝐴 Ñ 𝑎 Ñ Hprop, the order relation păq has type 𝐴 Ñ 𝐴 Ñ Prop, the tree 𝑇 has type tree 𝐴, and the set 𝐸 has type set 𝐴, where set corresponds to the built-in sets from the logic.

Trees with List of Subtrees

We next consider a slightly more challenging tree structure, in which each tree node consists of an item and a mutable list of subtrees. In the OCaml type definition shown below, cell is the type of list cells introduced in §4.1.

type 'a node = { mutable item : 'a; mutable children : ('a node) cell }

The higher-order representation predicate for nodes follows the exact same pattern as for other records (recall §6.1).

𝑝

Nodeof 𝑅1 𝑉1 𝑅2 𝑉2 " D D𝑣1𝑣2. 𝑝 Þ Ñ t|item=𝑣1; children=𝑣2|u ‹ 𝑣1 𝑅1 𝑉1 ‹ 𝑣2 𝑅2 𝑉2
The trees are represented in the logic by the following datatype.

Inductive tree (A:Type) :

Type := | Leaf : tree A | Node : A Ñ list (tree A) Ñ tree A.
The higher-order representation predicate 𝑝 Narytreeof 𝑅 𝑇 describes trees with list of subtrees. In the definition shown below, the key ingredient is the use of the representation predicate

Mlistof pNarytreeof 𝑅q for describing the mutable list of subtrees.

𝑝

Narytreeof 𝑅 𝑇 " match 𝑇 with | Leaf ñ r𝑝 " nulls | Node 𝑋 𝐿 ñ 𝑝 Nodeof 𝑅 𝑋 pMlistof pNarytreeof 𝑅qq 𝐿
In summary, by composing higher-order representation predicates to obtain Mlistof pNarytreeof 𝑅q, we are able to describe in a very concise manner the ownership of a mutable list and of all the subtrees whose roots are stored in that list.

Bootstrapped Trees

In this section, we consider a data structure called bootstrapped chunked bags to illustrate the design of higher-order representation predicates for data structures involving polymorphic recursion. This structure represents a bag (i.e. an unordered multiset of values) that supports push and pop operations in constant time, and supports merge and split operations in logarithmic time. 3 These operations are particularly useful in the design of parallel algorithms.

Bootstrapped chunked bags are parameterized by a constant k, and are constructed using chunks. A chunk is an array of capacity k, and thus can be used to represent bags storing up to k items. A bootstrapped chunked bag consists of several layers. The first layer contains a chunk of items. The second layer contains a chunk of chunks of items. The third layer contains a chunk of chunks of chunks of items, and so on.

For example, assume k = 10. Then, a bag storing 162 items could be represented with a first-layer chunk storing 2 items, a second-layer chunk storing 6 chunks of 10 items each, and a third layer chunk that stores a single chunk, which itself contains 10 chunks of 10 items each.

In what follows, we omit the details of the representation of chunks. We simply assume a type 'a chunk for chunks, and a corresponding representation predicate, written 𝑐 Chunkof 𝑅 𝐸, to assert that at location 𝑐 there exists a chunk that represents a multiset of items 𝐸, when these items are reflected in the logic using the representation predicate 𝑅.

An empty bag is represented as the null pointer. A nonempty bag is represented as a record made of a chunk of elements (the current layer) and a bag of chunks of elements (the next layers).

Note that elements stored at the first layer are base items, whereas elements stored in the deeper layers are pointers on chunks.

type 'a bag = { mutable head : 'a chunk; mutable next : ('a chunk) bag }

The higher-order representation predicate associated with this record type is defined following the same pattern as before.

𝑝

Nodeof 𝑅1 𝑉1 𝑅2 𝑉2 " D D𝑣1𝑣2. 𝑝 Þ Ñ t|head=𝑣1; next=𝑣2|u ‹ 𝑣1 𝑅1 𝑉1 ‹ 𝑣2 𝑅2 𝑉2
The layer structure is represented in the logic as shown below.

Inductive layer : Type Ñ Type := | Empty : @A, layer A | Layer : @A, multiset A Ñ layer (multiset A) Ñ layer A.

To relate the memory layout of bootstrapped chunked bag with its logical model, we introduce the predicate 𝑝 Layersof 𝑅 𝑇 . In the definition shown below, a nonempty layer consists of two parts: a chunk of items, represented by a multiset 𝐸 1 , and a bag of chunks, described by the representation predicate Layersof pChunkof 𝑅q.

𝑝

Layersof 𝑅 𝑇 " match 𝑇 with | Empty ñ r𝑝 " nulls | Layer 𝐸 1 𝑇 1 ñ 𝑝 Nodeof pChunkof 𝑅q 𝐸 1 pLayersof pChunkof𝑅qq 𝑇 1
Observe the polymorphic recursion at play here: the argument 𝑅 of Layersof becomes instantiated at the next level with Chunkof 𝑅.

Thus, when unfolding the recursive definitions, the representation predicates associated with deeper layers take the form: Chunkof pChunkof ...pChunkof 𝑅q...q.

It remains to define a heap predicate, written 𝑝 Bagof 𝑅 𝐸, to assert that, at the memory location 𝑝, there exists a chunked bag data structure that represents the multiset 𝐸, when items are represented using the representation predicate 𝑅. The definition, shown below, involves an auxiliary inductively-defined predicate Layerbag 𝑇 𝐸, which asserts that 𝐸 is the multiset obtained by collecting all the elements stored in the leaves of the tree 𝑇 .

𝑝

Bagof 𝑅 𝐸 " D D𝑇. 𝑝 Layersof 𝑅 𝑇 ‹ rLayerbag 𝑇 𝐸s Layerbag Empty H Layerbag 𝑇 1 𝐺 Layerbag pLayer 𝐸 1 𝑇 1 q p𝐸 1 Z flatten 𝐺q Above, flatten is an operation that takes as argument a multiset of multisets of items, and returns the union of these multisets.

The predicate 𝑝 Bagof 𝑅 𝐸 is involved in the specification of bag operations. For example, the specification of push is shown below. It is very similar to that for mutable queues (from Figure 1).

t𝑝

Bagof 𝑅 𝐸 ‹ 𝑥 𝑅 𝑋u ppush 𝑥 𝑝q t𝜆_. 𝑝

Bagof 𝑅 p𝐸 Z t𝑋uqu

In conclusion, data structures involving polymorphic recursion can be naturally described using a higher-order representation predicate in which the argument 𝑅 gets instantiated on recursive calls with the representation predicate itself, here Chunkof 𝑅.

Trees with Holes and Cut Subtrees

In this section, we present a technique for allowing one to detach the ownership of some items from a tree that owns its items (tree with holes), and/or to detach one or more entire subtrees from the tree (tree with cut subtrees). We present this technique using as running example the binary trees defined in §7.1. The predicate Nodeof, which we use thereafter for describing tree nodes, is that introduced in §7.2.

The central idea for describing trees with holes is to extend the type tree that is used to describe binary trees in the logic with two additional constructors, called Hole and Cut. First, the constructor Hole is similar to the constructor Node describing nodes, except that the item of the node considered is not owned: it is described using Id instead of 𝑅, where 𝑅 is the representation predicate 𝑅 normally describing the items. Second, the constructor Cut takes one location as argument. The intention is that Cut 𝑞 describes the fact that the subtree rooted at 𝑞 has been cut out from the main tree. Note that the contents of the cut out subtree is not described, in the sense that the constructor Cut appears like a leaf in the logical tree.

Inductive tree (a:Type) (A:Type) :

Type := | Leaf : tree A | Node : A Ñ tree A Ñ tree A Ñ tree A | Hole : a Ñ tree A Ñ tree A Ñ tree A | Cut : loc Ñ tree A.
We then generalize the representation predicate 𝑝

Mtreeof 𝑅 𝑇 to account for the two new constructors. In particular, when 𝑇 is of the form Cut 𝑞, we simply enforce that 𝑞 be equal to 𝑝, somewhat like we did for list segments. The updated definition appears next.

𝑝

Mtreeof 𝑅 𝑇

" match 𝑇 with | Leaf ñ r𝑝 " nulls | Node 𝑋 𝑇1 𝑇2 ñ 𝑝 Nodeof 𝑅 𝑋 pMtreeof 𝑅q 𝑇1 pMtreeof 𝑅q 𝑇2 | Hole 𝑥 𝑇1 𝑇2 ñ 𝑝 Nodeof Id 𝑥 pMtreeof 𝑅q 𝑇1 pMtreeof 𝑅q 𝑇2 | Cut 𝑞 ñ r𝑝 " 𝑞s
We may convert between a Node and a Hole as follows.

𝑝

Mtreeof 𝑅 pNode 𝑋 𝑇1 𝑇2q " D D𝑥. 𝑝 Mtreeof 𝑅 pHole 𝑥 𝑇1 𝑇2q ‹ 𝑥 𝑅 𝑋 For creating Hole and Cut nodes in-depth in the tree, we need tree surgery operations. To that end, we define a notion of path and substitution in trees. A path, written 𝑖, is represented as a list of booleans, with each boolean indicating whether to go down a left branch or a right branch. Note that a valid path would never go down through a Leaf or a Cut constructor. A predicate (whose definition is not shown), written path 𝑖 𝑇 𝑇 1 , asserts that 𝑖 is a valid path in 𝑇 , and that 𝑇 1 is the subtree reached by 𝑖. A substitution operation (whose definition is not shown), written subst 𝑖 𝑇 1 𝑇 , replaces the subtree at path 𝑖 in 𝑇 with 𝑇 1 . Note that this operation is undefined if 𝑖 is not a valid path in 𝑇 .

With these definitions, we are equipped to state the definitions of the central tree surgery lemma, which asserts that the subtree found at a valid path can be cut out from the main tree, or, reciprocally, merged back into the tree.

path 𝑖 𝑇 𝑇 1 ñ 𝑝 Mtreeof 𝑅 𝑇 " D D𝑞. 𝑝 Mtreeof 𝑅 psubst 𝑖 pCut 𝑞q 𝑇 q ‹ 𝑞 Mtreeof 𝑅 𝑇 1
It remains to give the specification of the function find, which takes a path as argument and returns a pointer to the corresponding subtree. If we assume that the targeted subtree has already been isolated in the logic, then we can easily specify the return value of find, as shown below.

t𝑝 Mtreeof 𝑅 𝑇 ‹ rpath 𝑖 𝑇 pCut 𝑞qsu pfind 𝑖 𝑝q t𝜆𝑥. 𝑝 Mtreeof 𝑅 𝑇 ‹ r𝑥 " 𝑞su Note that this specification allows for the tree 𝑇 to have arbitrary many holes in it, as long as these holes are not on the path 𝑖 followed by the function find. Also, observe how close this specification is from that of function nth provided at the end for §5.2.

It is also possible to combine the specification above with the tree surgery lemma. This yields the following specification. t𝑝 Mtreeof 𝑅 𝑇 ‹ rpath 𝑖 𝑇 𝑇 1 su pfind 𝑖 𝑝q t𝜆𝑞. 𝑝 Mtreeof 𝑅 psubst 𝑖 pCut 𝑞q 𝑇 q ‹ 𝑞 Mtreeof 𝑅 𝑇 1 u If the intention is to fold back the unaltered subtree into the main tree, then the post-condition in the above specification may be simplified using the magic wand (recall §5.3). The alternative post-condition shown below describes the ownership of the subtree and provides an instance of the magic wand asserting that when this subtree is given back, then the original tree is recovered.

𝜆𝑞. 𝑞

Mtreeof 𝑅 𝑇 1 ‹p𝑞 Mtreeof 𝑅 𝑇 1 ‹ 𝑝 Mtreeof 𝑅 𝑇 q Although the magic wand can be handy for some specific applications, tree with holes and cut subtrees are much more general. In particular, they support reasoning about trees that contain several holes, and support merging back subtrees that may have been modified or permuted in arbitrary ways.

Arrays 8.1 Individual Cells

In Separation Logic, the ownership of a single cell of an array can be described by a predicate of the form Cell 𝑖 𝑣 𝑝, where 𝑝 is the location of the array, 𝑖 is the index of the cell, and 𝑣 is the value stored in this cell. With our arrow notation, this predicate can be written 𝑝 Cell 𝑖 𝑣 . One may also introduce a specific notation for arrays, e.g. 𝑝r𝑖s

𝑣 , yet we will not need such a notation in this paper. Remark: the ownership of two distinct cells of an array takes the form 𝑝 Cell 𝑖 𝑣 ‹ 𝑝 Cell 𝑖 1 𝑣 1 . It may be surprizing at first that 𝑝 appears to the left of two arrows separated by a star operator, but there is nothing wrong here.

Under a low-level view of memory such as in the C programming language, the predicate 𝑝 Cell 𝑖 𝑣 can be defined as p𝑝 `𝑖q ãÑ 𝑣, by relying on pointer arithmetic in order to build on top of the heap predicate describing the ownership of a single memory cell. This presentation was followed in particular in the original paper on Separation Logic [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF]. However, in higher-level programming languages that do not expose pointer arithmetic, we simply treat Cell as an abstract, primitive heap predicate.

We next define Cellof, the higher-order version of the representation predicate Cell, following the same pattern as for Refof ( §6.2). The equality state below allows may be exploited to focus at once on all cells covered by 𝑀 , introducing a map 𝑇 describing the concrete values stored in these cells. For accessing a particular cell of the array, an alternative to focusing on all cells consists of first isolating the cell targeted, and then focusing only on this cell. The isolation operation is described below, where we write 𝑀 z𝑖 for the map 𝑀 with the key 𝑖 removed.

𝑝

𝑝

Cellsof

𝑝

Cellsof 𝑅 𝑀 when 𝑖 P dom 𝑀 " 𝑝 Cellsof 𝑅 p𝑀 z𝑖q ‹ 𝑝 Cellof 𝑅 𝑖 p𝑀 r𝑖sq
The following operation is also very useful for rearranging groups.

𝑝

Cellsof 𝑅 p𝑀1 Z 𝑀2q " 𝑝 Cellsof 𝑅 𝑀1 ‹ 𝑝 Cellsof 𝑅 𝑀2
For example, to specify a recursive quicksort function which takes as argument an array 𝑝, and two indices 𝑖 and 𝑗 in between which to sort the array, we would request in the precondition a predicate of the form 𝑝 Cellsof 𝑅 𝑀 with the hypothesis that the domain of 𝑀 matches the interval from 𝑖 to 𝑗. For reasoning about the recursive calls after the pivot phase, we split the (updated) map describing the array into three parts, corresponding to the cells storing values that are smaller than, equal to, or greater than the pivot value. Thanks to the frame rule, we automatically obtain, for each recursive call, the fact that the cells outside the range of the recursive call are not modified. Once the two recursive calls are completed, we may then merge back the updated maps in order to obtain a post-condition mentioning a map whose domain is the same as in the pre-condition.

Length Predicate

So far, we have only described the cells from an array, but not the length of the array. In many languages, such as OCaml, the length of the array in stored in the header, and is accessible to the programmer using a function called length. To specify this function, we need a predicate to keep track of the length of the array. In other languages, such as C, there is no array header, yet we still need to keep track of its length in order to correctly specify the deallocation operation.

To specify the length, we introduce another primitive heap predicate, written 𝑝 Arraysize 𝑛 (or, equivalently Arraysize 𝑛 𝑝), to assert that an array of size 𝑛 is allocated at location 𝑝. This predicate suffices, in particular, to specify the length function, as follows. Observe in particular how the pre-condition of free ensures two important properties: first, that the ownership of all the cells from the array is given back; and second, that the cells must be focused, so as to ensure the absence of memory leaks.

Example: Representation of Matrices

We consider matrices represented as arrays of arrays, first in the case where the rows consists of disjoint arrays, and second in the case where the rows might be shared. In both case, we assume the elements of the matrix to be represented by a predicate 𝑅 of type 𝑎 Ñ 𝐴 Ñ Hprop, for some 𝑎 and 𝐴. For the case of a matrix with possibly-aliased rows, we need to separately describe three parts. First, we describe the main array, which stores the locations of the arrays describing the rows. Assume this array is at location 𝑝, and represented with a map 𝑇 of type map int loc. The corresponding heap predicate is 𝑝 Arrayof Id 𝑇 . Second, we describe a group of arrays representing the possibly-shared rows. To that end, we make use of a map 𝐺 that binds locations to maps describing the rows, each of type map int 𝐴. In other words, 𝐺 has type map loc pmap int 𝐴q. The group of arrays is described by an iterated star over the bindings in 𝐺, more precisely: AE p𝑢,𝑈 qP𝐺 𝑢 Arrayof 𝑅 𝑈 . Third, we may establish a connection between the outer array 𝑇 , the inner arrays described by 𝐺, and the matrix 𝑀 being represented by the whole data structure, as follows.

𝑝

AliasedRowsMatrixof Interestingly, thanks to the rule that allows to focus at once on all cells from an array, we can convert, at the logical level, from a matrix made of disjoint rows (Matrixof) to a matrix made a possiblyaliased rows (AliasedRowsMatrixof). Even more interestingly, if we are able to prove that a matrix with possibly-aliased rows is actually represented by an outer array that contains pointers that are all distinct from each other, then the reciprocal conversion (from AliasedRowsMatrixof to Matrixof) is possible.

In summary, the representation predicate Arrayof pArrayof 𝑅q describes an outer array that owns the inner arrays, whereas the predicate Arrayof Id describes an outer array that does not own the inner arrays, the latter being described using a group of arrays each described using the predicate Arrayof 𝑅.

Conclusion

Separation Logic is a powerful approach to the modular specification and verification of mutable data structures. Higher-order representation predicates further increase modularity by offering the possibility to control, a posteriori, whether a container should own or not the items that it stores. This possibility has been identified by previous work [START_REF] Biering | BIhyperdoctrines, higher-order separation logic, and abstraction[END_REF][START_REF] Peter | Separation and information hiding[END_REF][START_REF] Kasper Svendsen | Verifying generics and delegates[END_REF]. In this paper, we investigate this idea further, considering a number of practical applications. In particular, we present a uniform pattern for reasoning about an access operation in a structure that owns its elements: first focus on the piece of data considered in order to detach the ownership of this item from the ownership of the structure, then reason about the access operation, and finally unfocus in order to fold back to the original form. One remaining challenge is to investigate to what extent the focus and unfocus operations can be automated in proof scripts.

t𝑝

  Mcellof Id 𝑣1 𝑅2 𝑉2u p𝑝.hdq t𝜆𝑥. 𝑝 Mcellof Id 𝑣1 𝑅2 𝑉2 ‹ r𝑥 " 𝑣1su t𝑝 Mcellof Id 𝑣1 𝑅2 𝑉2u p𝑝.hd<-𝑤q t𝜆_. 𝑝

Cellof

  𝑅 𝑖 𝑉 " D D𝑣. 𝑝 Cell 𝑖 𝑣 ‹ 𝑣 𝑅 𝑉 The specifications of read and write operations also closely resemble their counterparts on references. They are restricted to focused cells, represented using Id, as shown below. t𝑝 Cellof Id 𝑖 𝑣u p𝑝r𝑖sq t𝜆𝑥. 𝑝 Cellof Id 𝑖 𝑣 ‹ r𝑥 " 𝑣su t𝑝 Cellof Id 𝑖 𝑣u p𝑝r𝑖s <-𝑤q t𝜆_. 𝑝 Cellof Id 𝑖 𝑤u 8.2 Groups of Cells We next define the predicate 𝑝 Cellsof 𝑅 𝑀 to describe a subset of the cells from a same array-either a strict subset, or all the cells from the array. Here, 𝑀 denotes a finite map whose domain corresponds to the indices of the cells considered, and whose values correspond to the logical descriptions of the values stored in these cells. The definition is as follows. 𝑝 Cellsof 𝑅 𝑀 " ae 𝑖Pdom 𝑀 𝑝 Cellof 𝑅 𝑖 p𝑀 r𝑖sq

t𝑝

  Arraysize 𝑛u plength 𝑝q t𝜆𝑥. 𝑝 Arraysize 𝑛 ‹ r𝑥 " 𝑛su We next introduce a predicate, written 𝑝 Arrayof 𝑅 𝑀 to package the ownership of all the cells of the array together with its Arraysize predicate. The formal definition is as follows. 𝑝 Arrayof 𝑅 𝑀 " D D𝑛. rdom 𝑀 " [0, 𝑛)s ‹ 𝑝 Arraysize 𝑛 ‹ 𝑝 Cellsof 𝑅 𝑀 It is convenient in practice to state derived specifications in terms of Arrayof for the length function, for read and write operations in focused arrays, as well as for focus operations. Due to lack of space, we only include present two of these specifications. t𝑝 Arrayof 𝑅 𝑀 u plength 𝑝q t𝜆𝑥. 𝑝 Arrayof 𝑅 𝑀 ‹ r𝑥 " |𝑀 |su 𝑖 P dom 𝑀 ñ t𝑝 Arrayof Id 𝑀 u p𝑝r𝑖sq t𝜆𝑥. 𝑝 Arrayof Id 𝑀 ‹ r𝑥 " 𝑀 r𝑖ssu We also assign concise specifications to the function alloc, which allocates an array of given size without initializing its cells, and to the function free, which deallocates an array. In the specifications shown below, |𝑀 | denotes the number of bindings in 𝑀 . tr su palloc 𝑛q t𝜆𝑝. D D𝑀. 𝑝 Arrayof Id 𝑀 ‹ r|𝑀 | " 𝑛su t𝑝 Arrayof Id 𝑀 u pfree 𝑝q t𝜆_. r su

For

  the case of a matrix with non-aliased rows, we introduce the predicate 𝑝 Matrixof 𝑅 𝑀 , where 𝑀 describes a mathematical matrix storing elements of type 𝐴. In the definition shown below, dims 𝑀 returns the width and the height of the matrix, and 𝐾, of type map int pmap int 𝐴q, denotes the logical value associated with the array of arrays. 𝑝 Matrixof 𝑅 𝑀 " D D𝐾. 𝑝 Arrayof pArrayof 𝑅q 𝐾 ‹ » -D𝑛𝑚. p𝑛, 𝑚q " dims 𝑀 ^dom 𝐾 " r0, 𝑛q ^@𝑖 P r0, 𝑛q. dom p𝐾r𝑖sq " r0, 𝑚q ^@𝑗 P r0, 𝑚q. 𝐾r𝑖sr𝑗s " 𝑀𝑖,𝑗 fi fl

  heap predicate 𝑝 Mlistsegof 𝑅 𝑞 𝐿 asserts that, starting at pointer 𝑝, the heap contains the beginning of a mutable list segment, such that the elements contained between 𝑝 (inclusive) and 𝑞 (exclusive) are described by the list 𝐿 . The formal definition, shown below, differs from the definition of 𝑝 Mlistof 𝑅 𝐿 in that r𝑝 " nulls gets replaced with [p = q].

𝑝

Mlistsegof 𝑅 𝑞 𝐿 " match 𝐿 with | nil ñ r𝑝 " 𝑞s

  𝜆𝑏. r𝑏 " true ô 𝐿 " nils ‹ 𝑝 Queueof 𝑅 𝐿u 𝑝2 Queueof 𝑅 𝐿2 u ptransfer 𝑝1 𝑝2q t 𝜆_. 𝑝1 Queueof 𝑅 p𝐿1 `𝐿2q ‹ 𝑝2 Queueof 𝑅 nilu Figure 1. Mutable queue specification that includes ownership transfer for the elements.

	tr s		u pcreate()q t	𝜆𝑝. 𝑝	Queueof 𝑅 nilu
	t𝑝	Queueof 𝑅 𝐿	u pis_empty 𝑝q t
	t𝑝	Queueof 𝑅 𝐿 ‹ 𝑥 𝑅 𝑋	u ppush 𝑥 𝑝q t	𝜆_. 𝑝	Queueof 𝑅 p𝐿&𝑋qu
	t𝑝	Queueof 𝑅 p𝑋 :: 𝐿q	u ppop 𝑝q t	𝜆𝑥. 𝑝	Queueof 𝑅 𝐿 ‹ 𝑥 𝑅 𝑋u
	t𝑝	Queueof 𝑅 𝐿 ‹ r𝐿 ‰ nils					Queueof 𝑅 𝐿 1 ‹ 𝑥 𝑅 𝑋u
	t𝑝	Queueof 𝑅 p𝑋 :: 𝐿q	u ppeek 𝑝q t	𝜆𝑥. 𝑥	𝑅 𝑋 ‹ p𝑥	𝑅 𝑋 ´‹ 𝑝	Queueof 𝑅 p𝑋 :: 𝐿qqu
	t𝑝1	Queueof 𝑅 𝐿1 ‹
				¨@𝑝𝑅𝐿.	𝑝	Queueof 𝑅 𝐿 "
								Queueof 𝑅 p𝐿&𝑋qu ˘

D D𝐾. r |𝐾| " |𝐿| s ‹ 𝑝 Queue 𝐾 ‹ AE 𝑖 P r0, |𝐿|q p𝐾r𝑖sq 𝑅 p𝐿r𝑖sq ' ^`@𝑥𝑝𝐿. t𝑝 Queue 𝐿u ppush 𝑥 𝑝q t𝜆_. 𝑝 Queue p𝐿&𝑥qu ñ `@𝑥𝑝𝑋𝐿. t𝑝 Queueof 𝑅 𝐿 ‹ 𝑥 𝑅 𝑋u ppush 𝑥 𝑝q t𝜆_. 𝑝 u ppop 𝑝q t 𝜆𝑥. D D𝑋𝐿 1 . r𝐿 " 𝑋 :: 𝐿 1 s ‹ 𝑝

  Refof Id 𝑣u pget 𝑝q t𝜆𝑥. 𝑝 Refof Id 𝑣 ‹ r𝑥 " 𝑣su t𝑝 Refof Id 𝑣u pset 𝑝 𝑤q t𝜆_. 𝑝 Refof Id 𝑤u It is also possible to derive specifications that, to some extent, operate on unfocused references, described by a predicate of the form 𝑝 Refof 𝑅 𝑉 for an arbitrary 𝑅. These specifications, shown below, combine the specifications shown above with ownership trans-fer of the contents of the reference.Refof 𝑅 𝑉 u pget 𝑝q t𝜆𝑣. 𝑝 Refof Id 𝑣 ‹ 𝑣 𝑅 𝑉 u t𝑝 Refof 𝑅 𝑉 ‹ 𝑤 𝑅 1 𝑉 1 u pset 𝑝 𝑤q t𝜆_. 𝑝 Refof 𝑅 1 𝑉 1 ‹ pD D𝑣. 𝑣 𝑅 𝑉 quIn the specification of set, the post-condition includes the description of a piece of heap D D𝑣. 𝑣 𝑅 𝑉 , which typically corresponds to an object that has become inaccessible. On the one hand, if the program logic is affine, pieces of heaps can be safely discarded, so it is safe to drop D D𝑣. 𝑣 𝑅 𝑉 from the post-condition of set. On the other hand, if the program logic is linear, then the heap predicate D D𝑣. 𝑣 𝑅 𝑉 likely indicates a memory leak whenever 𝑅 is not equal to Id. 6.3 Access to Record Fields We now come back to the study of the list predicate Mcellof, which we use to illustrate how to specify focus operations as well as read and write operations on records with multiple fields. Unfolding the definition of Mcellof (given in §6.1) allows one to convert from a view where all fields are owned to a view where none of the fields is owned. If, however, instead of unfolding the definition of Mcellof, we use rewriting rules to introduce the identity representation predicate Id, then we are able to control, on a

	t𝑣	𝑅 𝑉 u pref 𝑣q t𝜆𝑝. 𝑝	Refof 𝑅 𝑉 u
	t𝑝
			tr su pref 𝑣q t𝜆𝑝. 𝑝	Refof Id 𝑣u
			t𝑝

per-field basis, which fields should be focused (i.e. ready for read and write operations) and which fields should remain unfocused (i.e. owned).

  𝑅 𝑀 " D D𝑇. rdom 𝑀 " dom 𝑇 s ‹ 𝑝 Cellsof Id 𝑇 For convenience, read and write operations can be specified directly on a group of focused cells. Below, we write 𝑀 r𝑖 :" 𝑤s to denote the update of 𝑀 with a binding from 𝑖 to 𝑤. 𝑖 P dom 𝑀 ñ t𝑝 Cellsof Id 𝑀 u p𝑝r𝑖sq t𝜆𝑥. 𝑝 Cellsof Id 𝑀 ‹ r𝑥 " 𝑀 r𝑖ssu t𝑝 Cellsof Id 𝑀 u p𝑝r𝑖s <-𝑤q t𝜆_. 𝑝 Cellsof Id p𝑀 r𝑖 :" 𝑤squ

	‹	AE 𝑖Pdom 𝑀 p𝑇 r𝑖sq	𝑅 p𝑀 r𝑖sq

  D𝑛𝑚. p𝑛, 𝑚q " dims 𝑀 ^dom 𝑇 " r0, 𝑛q ^@𝑖 P r0, 𝑛q. 𝑇 r𝑖s P dom 𝐺 ^@𝑗 P r0, 𝑚q. 𝐺r𝑇 r𝑖ssr𝑗s " 𝑀𝑖,𝑗

			𝑅 𝑀 "
	D D𝑇 𝐺. 𝑝	Arrayof Id 𝑇 ‹	AE	p𝑢,𝑈 qP𝐺 𝑢	Arrayof 𝑅 𝑈
		»				fi
	‹	-				fl

A triple t𝐻u 𝑡 t𝑄u is interpreted as shown below, where ó denotes the big-step evaluation judgment, ℎ 1 describes the heap on which 𝑡 operates, ℎ

describes the framed heap untouched by the evaluation of 𝑡, 𝑣 describes the output value, ℎ[START_REF] Umut | Theory and practice of chunked sequences[END_REF] 1 describes the modified heap, and ℎ

describes the discarded pieces of heap. Explanations can be found in a previous paper[START_REF] Charguéraud | Characteristic formulae for the verification of imperative programs[END_REF].

The equality 𝑝 Mlistof Id 𝐿 " 𝑝 Mlist 𝐿 relates two heap predicates. It should be interpreted according to predicate extensionality, as the logical equivalence between the two predicates on all heaps. Formally:p𝑄 1 " 𝑄 2 q " p@ℎ. 𝑄 1 ℎ ô 𝑄 2 ℎq.In fact, by further exploiting predicate extensionality, we could even prove the equality: Mlistof Id " Mlist.

Remark: the bootstrapped chunked bags presented here are a simplification of bootstrapped chunked sequences[START_REF] Umut | Theory and practice of chunked sequences[END_REF], which were recently proposed as an alternative to finger trees[START_REF] Hinze | Finger trees: a simple general-purpose data structure[END_REF] and to an earlier structure by Tarjan et al[START_REF] Kaplan | Persistent lists with catenation via recursive slow-down[END_REF], for improving constant factors and space consumption. Bootstrapped chunked bags may also be viewed as a generalization of the bootstrapped catenable lists presented by Okasaki[START_REF] Okasaki | Purely Functional Data Structures[END_REF].

Acknowledgements

I wish to thank François Pottier for fruitful discussions. This research was partly supported by the French national research organization ANR (grant ANR-15-CE25-0008).