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

Separation Logic for Sequential Programs (Functional Pearl)

Keywords: CCS Concepts:, Theory of computation → Separation logic; Logic and verification Separation Logic, Coq, Program verification

This paper presents a simple mechanized formalization of Separation Logic for sequential programs. This formalization is aimed for teaching the ideas of Separation Logic, including its soundness proof and its recent enhancements. The formalization serves as support for a course that follows the style of the successful Software Foundations series, with all the statement and proofs formalized in Coq. This course only assumes basic knowledge of λ-calculus, semantics and logics, and therefore should be accessible to a broad audience.

INTRODUCTION

Separation Logic brought a major breakthrough in the area of program verification [O'Hearn 2019] (Gödel Prize citation). Since its introduction, Separation Logic has made its way into a number of practical tools that are used on a daily basis for verifying programs ranging from operating systems kernels [START_REF] Xu | A practical verification framework for preemptive OS kernels[END_REF]] and file systems [START_REF] Chen | Using Crash Hoare Logic for Certifying the FSCQ File System[END_REF] to data structures [START_REF] Pottier | Verifying a Hash Table and Its Iterators in Higher-Order Separation Logic[END_REF]] and graph algorithms [START_REF] Guéneau | Formal Proof and Analysis of an Incremental Cycle Detection Algorithm[END_REF]]. These programs are written in various programming languages, including machine code [START_REF] Myreen | Hoare Logic for Realistically Modelled Machine Code[END_REF], assembly [START_REF] Ni | Certified Assembly Programming with Embedded Code Pointers[END_REF] [START_REF] Chlipala | The Bedrock Structured Programming System: Combining Generative Metaprogramming and Hoare Logic in an Extensible Program Verifier[END_REF]], C-language [START_REF] Appel ; Dockins | Program logics for certified compilers[END_REF], OCaml [START_REF] Charguéraud | Characteristic Formulae for the Verification of Imperative Programs[END_REF]], SML [START_REF] Kumar | CakeML: A Verified Implementation of ML[END_REF], and Rust [START_REF] Jung | RustBelt: Securing the Foundations of the Rust Programming Language[END_REF].

The key ideas of Separation Logic were devised by John Reynolds, inspired in part by older work by [START_REF] Burstall | Some Techniques for Proving Correctness of Programs which Alter Data Structures[END_REF]. Reynolds presented his ideas in lectures given in the fall of 1999. The proposed rules turned out to be unsound, but O'Hearn and Ishtiaq [2001] noticed a strong relationship with the logic of bunched implications [START_REF] O'hearn | The Logic of Bunched Implications[END_REF], leading to ideas on how to set up a sound program logic. Soon afterwards, the seminal publications on Separation Logic appeared at the CSL workshop [START_REF] O'hearn | Local Reasoning about Programs that Alter Data Structures[END_REF]] and at the LICS conference [START_REF] Reynolds | Separation Logic: A Logic for Shared Mutable Data Structures[END_REF]].

Today, when I teach students about Separation Logic, many of them find it hard to believe that Separation Logic has not been around for ever, or at least for as long as program verification exists. Perhaps the best way to truly value Reynold's contribution is to realize that, following the introduction of the first program logics in the late sixties [START_REF] Floyd | Assigning meanings to programs[END_REF][START_REF] Hoare | An axiomatic basis for computer programming[END_REF], people have tried for 30 years to verify programs without Separation Logic.

Given its great interest, Separation Logic should presumably be taught to most, if not all, students in the field of programming languages. While Concurrent Separation Logic is a notoriously hard topic [START_REF] Jung | Iris from the ground up: A modular foundation for higher-order concurrent separation logic[END_REF][START_REF] O'hearn | Separation logic[END_REF], Separation Logic for sequential programs is accessible to master students with basic knowledge in logic and semantics. There exists a number of courses that cover Separation Logic for sequential programs, from Reynold's course notes [2006] to modern courses presenting Separation Logic in the context of mechanized proofs, e.g., [Appel 2014;[START_REF] Birkedal | Lecture Notes on Iris: Higher-Order Concurrent Separation Logic[END_REF]Chlipala 2018a]. However, as we argue in detail in the related work section, existing presentations of Separation Logic either axiomatize the logic and omit important aspects of the soundness proof, or present a soundness proof that involves a number of technical obstacles that get in the way of the students' understanding.

This paper presents a formalization of Separation Logic for sequential programs that, we believe, is simple enough that master students can follow through every detail of its soundness proof, interactively in the Coq proof assistant. Actually, the main contribution of the work described in this paper is a course, entitled Foundations of Separation Logic and written in the style of the Software Foundations series [Pierce and many contributors 2016]. The present paper consists of a summary of the material from that course, with formal definitions formatted using LaTeX. We refer to the supplementary material [START_REF] Charguéraud | [END_REF]] for the proofs omitted from this paper, as well as numerous additional examples, exercises, comments, and discussion of alternative definitions.

This paper also includes the presentation five key features of Separation Logic that were introduced after the seminal paper from 2002.

(1) The ramified frame rule is a concise and practical rule that combines the frame rule and the rule of consequence into a single rule. The ramified frame rule is essential for automatically simplifying entailments in a robust way ( §7.3).

(2) The magic wand operator can be generalized from heap predicates to postconditions. The magic wand operator for postconditions is useful for languages featuring terms with return values, in particular to state the ramified frame rule.

(3) The inductive reasoning rule for loops allows applying the frame rule over the remaining iterations of a loop. This rule typically saves the need to introduce list segments or tree contexts in the statement of loop invariants. In particular, it saves a considerable amount of work when verifying functions that go down a tree-shaped data structure using a while loop. Such functions are pervasive in C implementations of tree-based containers. (4) The weakest-precondition calculus is, just like in Hoare Logic, a central ingredient for setting up practical verification tools for Separation Logic. In particular, the weakest-precondition style presentation enables better factorization in the statement of reasoning rules, and simplifies the set up of tactics that help instantiating the rules. [START_REF] Appel | Program Logics for Certified Compilers[END_REF] The coexistence of linear heap predicates and affine heap predicates is a must-have for any language equipped with a GC ( §8.2). We explain how to set up a Separation Logic with customizable control over which heap predicates are linear and which ones are affine. Such a set up allows to control which heap predicates may be freely discarded.

The features listed above might appear to be somewhat technical, yet there are absolutely essential for taking full advantage of Separation Logic. The formalization of Separation Logic that we present targets a λ-calculus with imperative features. We consider this language for two reasons. First, the λ-calculus has proved well-suited for teaching programming language semantics in general, as it abstracts away from the details of industrial programming languages. Second, targeting an ML-style language with immutable variables and mutable heap-allocated memory cells leads to the simplest formulation of the reasoning rules, avoiding a number of complications associated with mutable variables. In technical terms, our Coq formalization relies on a standard deep embedding of an imperative λ-calculus. This embedding features: an inductive definition of the abstract syntax tree, a recursive definition of the capture-avoiding substitution function, and an inductive definition of the operational semantics. We consider a big-step semantics to simplify the soundness proof.

Our formalization targets the simplest variant of Separation Logic. The heap predicates are defined as higher-order logic predicates, that is, as plain Coq definitions. The reasoning rules of the logic are stated as lemmas that are proved correct with respect to the big-step evaluation rules. In technically terms, our formalization consists of a shallow embedding of Separation Logic in Coq. This approach naturally yields a very expressive higher-order Separation Logic. It is employed by the majority of practical verification tools that embed Separation Logic in a proof assistant. It thus makes sense to teach that approach to students that will use or develop those verification tools.

By presenting our course notes on Separation Logic, whose contents are summarized in the present paper, we aim to make the following contributions.

(1) We present a mechanized soundness proof for Separation Logic for sequential programs that we believe to be more accessible to students than previously-available proofs.

(2) We present the first course on Separation Logic written in the style of the Software Foundations series. This presentation style, in which every definition and every lemma is presented via its mechanized statement, has been successfully employed for teaching material related to logic and programming languages. Note that the course is focused on the foundations of Separation Logic and the description of its features. It does not (yet) include a large collection of examples illustrating how to specify and verify data structures and algorithms.

(3) We present, within a same paper, five key features that were previously scattered in the literature from the past decade: the ramified frame rule, the magic wand for postconditions, the inductive reasoning technique for loops, the customizable control of affinity, and the weakest-precondition style presentation of the reasoning rules.

This paper is organized as follows. We first give an overview of the key features of Separation Logic ( §2). We then present the operators of the logic ( §3), the syntax and semantics of the language ( §4), the definition of triples and the statement of the reasoning rules ( §5). Next, we describe additional techniques: inductive reasoning for loops ( §6), the magic wand operator ( §7), the generalization to a partially-affine logic ( §8), and the presentation in weakest-precondition style ( §9). Finally, we give references for all the ideas presented, and discuss related work ( §10).

The supplementary material [START_REF] Charguéraud | [END_REF]] accompanying the present submission contains: (1) the full contents of the course, both in Coq and HTML format, (2) a file that contains just the core definitions and soundness proof (SLFMinimal.v), and (3) an appendix to the present paper. This appendix includes statistics on our soundness proof for Separation Logic ( §A), background on extensionality axioms ( §B), the presentation of the proofs of representative reasoning rules ( §C), an example Separation Logic proof ( §D), an illustration of the benefits of the frame rule in the proof of recursive functions ( §E), a solution to the cps-append verification challenge proposed by Reynolds ( §F), a discussion of alternative structural rules ( §G), a description of the treatment of assertions ( §I), of arrays and records ( §H), and n-ary functions ( §J), and the description of an algorithm for simplifying entailment relations ( §K).

OVERVIEW OF THE FEATURES OF SEPARATION LOGIC

This section gives an overview of the features that are specific to Separation Logic: the separating conjunction and the frame rule, which enable local reasoning and small-footprint specifications, the treatment of aliasing, the specification of recursive pointer-based data structures such as mutable linked lists, and the ability to ensure complete deallocation of all allocated data.

The Frame Rule

In Hoare logic, the behavior of a command t is specified through a triple, written {H } t {Q }, where the precondition H describes the input state and the postcondition Q describes the output state.

Whereas in Hoare Logic H and Q describe the whole memory state, in Separation Logic they describe only a fragment of the memory state, a fragment that includes all the resources involved in the execution of the command t.

The frame rule asserts that if a command t safely executes in a given piece of state, then it also executes safely in a larger piece of state. More precisely, if t executes in a state described by H and produces a final state described by Q, then this program can also be executed in a state that extends H with a disjoint piece of state described by H ′ . The corresponding final state consists of Q extended with H ′ , capturing the fact that the additional piece of state is unmodified by the execution of t. The frame rule enables local reasoning, defined as follows [START_REF] O'hearn | Local Reasoning about Programs that Alter Data Structures[END_REF].

To understand how a program works, it should be possible for reasoning and specification to be confined to the cells that the program actually accesses. The value of any other cell will automatically remain unchanged.

The frame rule is stated using the separating conjunction, written ⋆, which is a binary operator over heap predicates. In Separation Logic, pieces of states are traditionnally called heaps, and predicate over heaps are called heap predicates. Given two heap predicates H and H ′ , the heap predicate H ⋆ H ′ describes a heap made of two disjoint parts, one that satisfies H and one that satisfies H ′ . The statement of the frame rule, shown below, asserts that any triple remains valid when extending both its precondition and its postcondition with an arbitrary predicate H ′ .

{H } t {Q } {H ⋆ H ′ } t {Q ⋆ H ′ }
frame-for-commands where t is a command.

In this paper, we do not consider a language of commands but a language based on the λ-calculus, with programs described as terms that evaluate to values. (The language is formalized in §4.1.) In that setting, a specification triple takes the form {H } t {λx . H ′ }, where H describes the input state, x denotes the value produced by the term t, and H ′ describes the output state, with x bound in H ′ . For such triples, the frame rule is stated either as:

{H } t {λx . H ′′ } {H ⋆ H ′ } t {λx . H ′′ ⋆ H ′ }
frame where t is a term producing a value, and x fv(H ′ )

or, more concisely, as:

{H } t {Q } {H ⋆ H ′ } t {Q . ⋆ H ′ } frame where Q . ⋆ H ≡ λv. (Q v ⋆ H ).

Separation Logic Specifications

What makes Separation Logic work smoothly in practice is that specifications are expressed using a small number of operators for defining heap predicates, such that these operators interact well with the separating conjunctions. The most important operators are summarized below-they appear in examples throughout the rest of this section, and are formally defined further on ( §3.2).

• p → v, to be read "p points to v", describes a single memory cell, allocated at address p, with contents v.

• [ ] describes an empty state.

• [P] also describes an empty state, and moreover asserts that the proposition P is true.

• H 1 ⋆H 2 describes a heap made of two disjoint parts, one described by H 1 and another described by H 2 . • ∃ ∃x . H and ∀ ∀x . H are used to quantify variables in Separation Logic assertions.

We call these operators the core heap predicate operators, because all the other Separation Logic operators can be defined in terms of these core operators.

The heap predicate operators appear in the statement of preconditions and postconditions. For example, consider the specification of the function incr, which increments the contents of a reference cell. It is specified using a triple of the form {H } (incr p) {Q }.

Example 2.1 (Specification of the increment function).

∀p n.

{p → n} (incr p) {λ_. p → (n + 1)}

The precondition describes the existence of a memory cell that stores an integer value, through the predicate p → n. The postcondition describes the final heap in the form p → (n + 1), reflecting the increment of the contents. The "λ_. " symbol at the head of the postcondition indicates that the value returned by incr p, namely the unit value, needs not be assigned a name.

Throughout the rest of the paper, the outermost universal quantifications (e.g., "∀p n.") are left implicit, following standard practice.

Implications of the Frame Rule

The precondition in the specification of incr p describes only the reference cell involved in the function call, and nothing else. Consider now the execution of incr p in a heap that consists of two distinct memory cells, the first one being described as p → n, and the other being described as q → m. In Separation Logic, the conjunction of these two heap predicates are described by the heap predicate (p → n) ⋆ (q → m). There, the separating conjunction (a.k.a. the star) captures the property that the two cells are distinct. The corresponding postcondition of incr p describes the updated cell p → (n + 1) as well as the other cell q → m, whose contents is not affected by the call to the increment function. The corresponding Separation Logic triple is therefore stated as follows.

Example 2.2 (Application of the frame rule on the specification of the increment function).

{(p → n) ⋆ (q → m)} (incr p) {λ_. (p → n + 1) ⋆ (q → m)}
The above triple is derivable from the one stated in Example 2.1 by applying the frame rule to add the heap predicate q → m both to the precondition and to the postcondition. More generally, any heap predicate H can be added to the original, minimalist specification of incr p. Thus we have:

{(p → n) ⋆ H } (incr p) {λ_. (p → n + 1) ⋆ H }.

Treatment of Potentially-Aliased Arguments

We next discuss the case of potentially-aliased reference cells. In the previous example, we have considered two reference cells p and q assumed to be distinct from each other. Consider now a function that expects as arguments two reference cells, at addresses p and q, and increments both. Potentially, the two arguments might correspond to the same reference cell. The function thus admits two specifications. The first one describes the case of two distinct arguments, using separating conjunction to assert the difference. The second one describes the case of two aliased arguments, that is, the case p = q, for which the precondition describes only one reference cell.

Example 2.3 (Potentially aliased arguments). The function:

let incr_two p q = (incr p; incr q) admits the following two specifications.

{(p → n) ⋆ (q → m)} (incr_two p q) {λ_. (p → n + 1) ⋆ (q → m + 1)} {p → n} (incr_two p p) {λ_. (p → n + 2)}

Small-Footprint Specifications

A Separation Logic triple captures all the interactions that a term may have with the memory state. Any piece of state that is not described explicitly in the precondition is guaranteed to remain untouched. Separation Logic therefore encourages small footprint specifications, i.e., specifications that mention nothing but what is strictly needed. The small-footprint specifications for the primitive operations ref, get and set are stated and explained next.

Example 2.4 (Specification of primitive operations on references).

{[ ]} (ref v) {λr . ∃ ∃p. [r = p] ⋆ (p → v)} {p → v} (get p) {λr . [r = v] ⋆ (p → v)} {p → v} (set p v ′ ) {λ_. (p → v ′ )}
The operation ref v can execute in the empty state, described by [ ]. It returns a value, named r , that corresponds to a pointer p, such that the final heap is described by p → v. In the postcondition, the variable p is quantified existentially, and the pure predicate [r = p] denotes an equality between the value r and the address p, viewed as an element from the grammar of values (formalized in §4.1). The operation get p requires in its precondition the existence of a cell described by p → v.

Its postcondition asserts that the result value, named r , is equal to the value v, and that the final heap remains described by p → v. The operation set p v ′ also requires a heap described by p → v.

Its postcondition asserts that the updated heap is described by p → v ′ . The result value, namely unit, is ignored.

The possibility to state a small-footprint specification for the allocation operation captures an essential property: the reference cell allocated by ref is implicitly asserted to be distinct from any pre-existing reference cell. This property can be formally derived by applying the frame rule to the specification triple for ref. For example, the triple stated below asserts that if a cell described by q → v ′ exists before the allocation operation ref v, then the new cell described by p → v is distinct from that pre-existing cell. This freshness property is captured by the separating conjunction

(p → v) ⋆ (q → v ′ ).
Example 2.5 (Application of the frame rule to the specification of allocation).

{q → v ′ } (ref v) {λr . ∃ ∃p. [r = p] ⋆ (p → v) ⋆ (q → v ′ )}
The strength of the separating conjunction is even more impressive when involved in the description of recursive data structures such as mutable lists, which we present next.

Representation of Mutable Lists

A mutable linked list consists of a chain of cells. Each cell contains two fields: the head field stores a value, which corresponds to an item from the list; the tail field stores either a pointer onto the next cell in the list, or the null pointer to indicate the end of the list. Definition 2.6 (Representation of a list cell). A list cell allocated at address p, storing the value v and the pointer q, is represented by two singleton heap predicates, in the form:

(p.head → x ) ⋆ (p.tail → q)
where "p.k" is a notation for the address p + k, and "head ≡ 0" and "tail ≡ 1" denote the offsets.

A mutable linked list is described by a heap predicate of the form Mlist L p, where p denotes the address of the head cell and L denotes the logical list of the elements stored in the mutable list. The predicate Mlist is called a representation predicate, because it relates the pair made of a pointer p and of the heap-allocated data structure that originates at p together with the logical representation of this data structure, namely the list L.

The predicate Mlist is defined recursively on the structure of the list L. If L is the empty list, then p must be null. Otherwise, L is of the form x :: L ′ . In this case, the head field of p stores the item x, and the tail field of p stores a pointer q such that Mlist L ′ q describes the tail of the list. The case disjunction is expressed using Coq's pattern-matching construct.

Definition 2.7 (Representation of a mutable list).

Mlist L p ≡ match L with | nil ⇒ [p = null] | x :: L ′ ⇒ ∃ ∃q. (p.head → x ) ⋆ (p.tail → q) ⋆ (Mlist L ′ q)
Example 2.8 (Application of the predicate Mlist to a list of length 3). To see how Mlist unfolds on a concrete example, consider the example of a mutable list storing the values 8, 5, and 6.

Mlist (8 :: 5 :: 6 ::

nil) p ≡ ∃ ∃p 1 . (p.head → 8) ⋆ (p.tail → p 1 ) ⋆ ∃ ∃p 2 . (p 1 .head → 5) ⋆ (p 1 .tail → p 2 ) ⋆ ∃ ∃p 3 . (p 2 .head → 6) ⋆ (p 2 .tail → p 3 ) ⋆ [p 3 = null]
Observe how the definition of Mlist, by iterating the separating conjunction operator, ensures that all the list cells are distinct from each other. In particular, Mlist precludes the possibility of cycles in the linked list, and precludes inadvertent sharing of list cells with other mutable lists.

Definition 2.7 characterizes Mlist by case analysis on whether the list L is empty. Another, equivalent definition instead characterizes Mlist by case analysis on whether the pointer p is null. This alternative definition is very useful because most list-manipulating programs involve code that tests whether the list pointer at hand is null. Definition 2.9 (Alternative definition for Mlist).

Mlist L p ≡ If (p = null) then [L = nil] else ∃ ∃xL ′ q. [L = x :: L ′ ] ⋆ (p.head → x ) ⋆ (p.tail → q) ⋆ (Mlist L ′ q)
Note that this alternative definition is not recognized as structurally-recursive by Coq. Its statement may be formulated as an equality, and proved correct with respect to Definition 2.7.

Operations on Mutable Lists

Consider a function that concatenates two mutable lists in-place. This function expects two pointers p 1 and p 2 that denote the addresses of two mutable lists described by the logical lists L 1 and L 2 , respectively. The first list is assumed to be nonempty. The concatenation operation updates the last cell of the first list so that it points to p 2 , the head cell of the second list. After this operation, the mutable list at address p 1 is described by the concatenation L 1 + + L 2 .

Example 2.10 (Specification of in-place append for mutable lists).

p 1 null ⇒ {(Mlist L 1 p 1 ) ⋆ (Mlist L 2 p 2 )} (mappend p 1 p 2 ) {λ_. Mlist (L 1 + + L 2 ) p 1 }
Observe how the specification above reflects the fact that the cells of the second list are absorbed by the first list during the operation. These cells are no longer independently available, hence the absence of the representation predicate Mlist L 2 p 2 from the postcondition.

Remark 2.11 (Alternative placement of pure preconditions). The hypothesis p 1 null from the specification of the append function may be equivalently placed inside the precondition:

{[p 1 null] ⋆ (Mlist L 1 p 1 ) ⋆ (Mlist L 2 p 2 )} (mappend p 1 p 2 ) {λ_. Mlist (L 1 + + L 2 ) p 1 }.
Yet, in general, leaving pure hypotheses as premises outside of triples tends to improve readability.

As second example, consider a function that takes as argument a pointer p to a mutable list, and allocates an entirely independent copy of that list, made of fresh cells. This function is specified as shown below. The precondition describes the input list as Mlist L p, and the postcondition describes the output heap as Mlist L p ⋆ Mlist L p ′ , where p ′ denotes the address of the new list.

Example 2.12 (Specification of a copy function for mutable lists).

{Mlist L p} (mcopy p) {λr . ∃ ∃p ′ . [r = p ′ ] ⋆ (Mlist L p) ⋆ (Mlist L p ′ )}
The separating conjunction from the postcondition asserts that the original list and its copy do not share any cell: they are entirely disjoint from each other. An implementation and a proof for the function mcopy is given in the appendix. The key steps of that proof are summarized next.

Proof. The specification of mcopy is proved by induction on the length of the list L. When the list is nonempty, Mlist L p unfolds as (p.head → x ) ⋆ (p.tail → q) ⋆ (Mlist L ′ q). The induction hypothesis allows to assume the specification to hold for the recursive call of mcopy on the tail of the list, with the precondition Mlist L ′ q. Over the scope of that call, the frame rule is used to put aside the head cell, described by (p.head → x ) ⋆ (p.tail → q). Let q ′ denote the result of the recursive call, and let p ′ denote the address of a freshly-allocated list cell storing the value x and the tail pointer q ′ . The final heap is described by:

(p.head → x ) ⋆ (p.tail → q) ⋆ (Mlist L ′ q) ⋆ (p ′ .head → x ) ⋆ (p ′ .tail → q ′ ) ⋆ (Mlist L ′ q ′ )
which may be folded to (Mlist L p) ⋆ (Mlist L p ′ ), matching the claimed postcondition. □

In the above proof, the frame rule enables reasoning about a recursive call independently of all the cells that have already been traversed by the outer recursive calls to mcopy. Without the frame rule, one would have to describe the full list at an arbitrary point during the recursion. Doing so requires describing the list segment made of cells ranging from the head of the initial list up to the pointer on which the current recursive call is made. Stating an invariant involving list segments is doable, yet involves more complex definitions and assertions. More generally, for a program manipulating tree-shaped data structures, the frame rule saves the need to describe a tree with a subtree carved out of it, thereby saving a significant amount of proof effort.

Reasoning about Deallocation

Consider a programming language with explicit deallocation. For such a language, proofs in Separation Logic guarantee two essential properties: (1) a piece of data is never accessed after its deallocation, and (2) every allocated piece of data is eventually deallocated.

The operation free p deallocates the reference cell at address p. This deallocation operation is specified through the following triple, whose precondition describes the cell to be freed by the predicate p → v, and whose postcondition is empty, reflecting the loss of that cell. Definition 2.13 (Specification of the free operation).

{p → v} (free p) {λ_. [ ]}

There is no way to get back the predicate p → v once it is lost. Because p → v is required in the precondition of all operations involving the reference p, Separation Logic ensures that no operations on p can be performed after its deallocation.

The next examples show how to specify the deallocation of a list cell and of a full list.

Example 2.14 (Deallocation of a list cell). The function mfree_cell deallocates a list cell.

{(p.head → x ) ⋆ (p.tail → q)} (mfree_cell p) {λ_. [ ]}.
Example 2.15 (Deallocation of a mutable list). The function mfree_list deallocates a list by recursively deallocating each of its cells. Its implementation is shown below (using ML syntax, even though the language considered features null pointers and explicit deallocation). let rec mfree_list p = if p != null then (let q = p.tail in mfree_cell p; mfree_list q)

The specification of mfree_list admits the precondition Mlist L p, describing the mutable list to be freed, and admits an empty postcondition, reflecting the loss of that list.

{Mlist L p} (mfree_list p) {λ_. [ ]}
Remark 2.16 (Languages with implicit garbage collection). For languages equipped with a garbagecollector, Separation Logic can be adapted to allow freely discarding heap predicates (see §8).

HEAP PREDICATES AND ENTAILMENT

Representation of Heaps

Let loc denote the type of locations, i.e., of memory addresses. This type may be realized using, e.g., natural numbers. Let val denote the type of values. The grammar of values depends on the programming language. Its formalization is postponed to §4.

A heap (i.e., a piece of memory state) may be represented as a finite map from locations to values. The finiteness property is required to ensure that fresh locations always exist. Let fmap α β denote the type of finite maps from a type α to an (inhabited) type β.

Definition 3.1 (Representation of heaps). The type heap is defined as "fmap loc val".

Thereafter, let h denote a heap, that is, a piece of state. Let h 1 ⊥ h 2 assert that two heaps have disjoint domains, i.e., that no location belongs both to the domain of h 1 and to that of h 2 . Let h 1 ⊎ h 2 denote the union of two disjoint heaps. (The union operation may return arbitrary results when applied to non-disjoint arguments, i.e., arguments with overlapping domains.)

Heap Predicates

A heap predicate, written H , is a predicate that asserts properties of a heap.

Definition 3.2 (Heap predicates).

A heap predicate is a predicate of type heap → Prop.

The core heap predicate operators, informally introduced in §2.2, are realized as predicates over heaps, as shown below and explained next.

Definition 3.3 (Core heap predicates).

Heap predicate operator Notation Definition

empty predicate [ ] λh. h = ∅ pure fact [P] λh. h = ∅ ∧ P singleton p → v λh. h = (p → v) ∧ p null separating conjunction H 1 ⋆ H 2 λh. ∃h 1 h 2 . h 1 ⊥ h 2 ∧ h = h 1 ⊎ h 2 ∧ H 1 h 1 ∧ H 2 h 2 existential quantifier ∃ ∃x . H λh. ∃x . H h universal quantifier ∀ ∀x . H λh. ∀x . H h
The definitions for the core heap predicates all take the form λh. P, where P denotes a proposition. The empty predicate, written [ ], characterizes a heap equal to the empty heap, written ∅. The pure predicate, written [P], also characterizes an empty heap, and moreover asserts that the proposition P is true. The singleton heap predicate, written p → v, characterizes a heap described by a singleton map, written p → v, which binds p to v. This predicate embeds the property p null, capturing the invariant that no data may be allocated at the null location. The separating conjunction, written H 1 ⋆ H 2 , characterizes a heap h that decomposes as the disjoint union of two heaps h 1 and h 2 , with h 1 satisfying H 1 and h 2 satisfying H 2 . The existential and universal quantifiers of Separation Logic allow quantifying entities at the level of heap predicates (heap → Prop), in contrast to the standard Coq quantifiers that operate at the level of propositions (Prop). Note that the quantifiers ∃ ∃x . H and ∀ ∀x . H may quantify values of any type, without restriction. In particular, they allow quantifying over heap predicates or proof terms.

Remark 3.4 (Encodings between the empty and the pure heap predicate). In Coq, the pure heap predicate [P] can be encoded as "∃ ∃(p : P ). [ ]", that is, by quantifying over the existence of a proof term p for the proposition P. Note that the empty heap predicate [ ] is equivalent to [True].

Remark 3.5 (Other operators). Traditional presentations of Separation Logic include four additional operators, ⊥, ⊤, ∨ ∨, and ∧ ∧. These four operators may be encoded in terms of the ones from Definition 3.3, with the help of Coq's conditional construct. The table below presents the relevant encodings, in addition to providing direct definitions of these operators as predicates over heaps.

Heap predicate operator Notation Definition

Encoding bottom ⊥ λh. False [False] top ⊤ λh. True ∃ ∃(H : heap → Prop). H disjunction H 1 ∨ ∨ H 2 λh. (H 1 h ∨ H 2 h) ∃ ∃(b : bool). If b then H 1 else H 2 non-separating conjunction H 1 ∧ ∧ H 2 λh. (H 1 h ∧ H 2 h) ∀ ∀(b : bool). If b then H 1 else H 2
Definition 3.6 (Representation predicate for lists defined with disjunction). The representation predicate for lists introduced in Definition 2.8 can be reformulated using the disjunction operator instead of relying on pattern-matching. The corresponding definition, which may be useful if the host logic does not feature a pattern-matching construct, is as follows.

Mlist L p ≡ [p = null] ⋆ [L = nil] ∨ ∨ [p null] ⋆ ∃ ∃xL ′ q. [L = x :: L ′ ] ⋆ (p.head → x ) ⋆ (p.tail → q) ⋆ (Mlist L ′ q)

Entailment

The entailment relation, written H 1 ⊢ H 2 , asserts that any heap satisfying H 1 also satisfies H 2 . Definition 3.7 (Entailment relation).

H 1 ⊢ H 2 ≡ ∀h. H 1 h ⇒ H 2 h
Entailment is used to state reasoning rules and to state properties of the heap predicates operators. The entailment relation defines an order relation on the set of heap predicates. Lemma 3.8 (Entailment defines an order on the set of heap predicates).

himpl-refl

H ⊢ H himpl-trans H 1 ⊢ H 2 H 2 ⊢ H 3 H 1 ⊢ H 3 himpl-antisym H 1 ⊢ H 2 H 2 ⊢ H 1 H 1 = H 2
The antisymmetry property concludes on an equality between two heap predicates. To establish such an equality, it is necessary to exploit the principle of predicate extensionality. This principle asserts that if two predicates P and P ′ , when applied to any argument x, yield logically equivalent propositions, then these two predicates can be considered equal in the logic. (See the appendix for details.) The antisymmetry property plays a critical role for stating the key properties of Separation Logic operators in the form of equalities, as detailed next.

pure-l

P ⇒ (H ⊢ H ′ ) ([P] ⋆ H ) ⊢ H ′ exists-l ∀x . (H ⊢ H ′ ) (∃ ∃x . H ) ⊢ H ′ forall-l ([a/x] H ) ⊢ H ′ (∀ ∀x . H ) ⊢ H ′ exists-monotone ∀x . (H ⊢ H ′ ) (∃ ∃x . H ) ⊢ (∃ ∃x . H ′ ) pure-r (H ⊢ H ′ ) P H ⊢ (H ′ ⋆ [P]) exists-r H ⊢ ([a/x] H ′ ) H ⊢ (∃ ∃x . H ′ ) forall-r ∀x . (H ⊢ H ′ ) H ⊢ (∀ ∀x . H ′ ) forall-monotone ∀x . (H ⊢ H ′ ) (∀ ∀x . H ) ⊢ (∀ ∀x . H ′ )
Fig. 1. Useful properties for pure facts and quantifiers, with respect to entailment.

There are 6 fundamental properties of the separating conjunction operator. The first three capture the fact that (⋆, [ ]) forms a commutative monoid: the star is associative, commutative, and admits the empty heap predicate as neutral element. The next two describe how quantifiers may be extruded from arguments of the star operator. The extraction rule star-exists is stated using an equality because the entailment relation holds in both directions. On the contrary, the extraction rule star-forall is stated using a simple entailment relation because the reciprocal entailment does not hold-for a counterexample, consider the case where the type of x is unhabited. The rule star-monotone-r describes a monotonicity property; it is explained afterwards. Lemma 3.9 (Fundamental properties of the star).

star-assoc:

(

H 1 ⋆ H 2 ) ⋆ H 3 = H 1 ⋆ (H 2 ⋆ H 3 ) star-comm: H 1 ⋆ H 2 = H 2 ⋆ H 1 star-neutral-r: H ⋆ [ ] = H star-exists: (∃ ∃x . H 1 ) ⋆ H 2 = ∃ ∃x . (H 1 ⋆ H 2 ) (if x H 2 ) star-forall: (∀ ∀x . H 1 ) ⋆ H 2 ⊢ ∀ ∀x . (H 1 ⋆ H 2 ) (if x H 2 )
star-monotone-r:

H 1 ⊢ H ′ 1 H 1 ⋆ H 2 ⊢ H ′ 1 ⋆ H 2
The monotonicity rule can be read from bottom to top: when facing a proof obligation of the form

H 1 ⋆ H 2 ⊢ H ′ 1 ⋆ H 2 ,
one may cancel out H 2 on both sides, leaving the proof obligation H 1 ⊢ H ′ 1 . Remark 3.10 (Symmetric version of the monotonicity rule). The monotonicity rule is sometimes also presented in its symmetric variant, stated below. It is provably equivalent to star-monotone-r.

H 1 ⊢ H ′ 1 H 2 ⊢ H ′ 2 H 1 ⋆ H 2 ⊢ H ′ 1 ⋆ H ′ 2 star-monotone
The useful properties associated with pure facts and quantifiers appear in Fig. 1. The application of a number of reasoning rules for entailment can be automated by means of a tactic. (One such tactic is described in the appendix.) Other properties may also be derived, such as

([P 1 ]⋆[P 2 ]) = [P 1 ∧P 2 ].
Yet, when a simplification tactic is available, one does not need to state such properties explicitly.

The entailment relation may be employed to express how a specific piece of information can be extracted from a given heap predicate. For example, from p → v, one can extract the information p null. Likewise, from a heap predicate of the form p → v 1 ⋆ p → v 2 , where the same location p is described twice, one can derive a contradiction, because the separating conjunction asserts disjointness. These two results are formalized as follows.

Lemma 3.11 (Properties of the singleton heap predicate).

single-not-null: (p → v) ⊢ (p → v) ⋆ [p null] single-conflict: (p → v 1 ) ⋆ (p → v 2 ) ⊢ [False]

Generalization to Postconditions

In the imperative λ-calculus considered in this paper and formalized further on ( §4), a term evaluates to a value. A postcondition thus describes both an output value and an output state. Definition 3.12 (Type of postconditions). A postcondition has type: val → heap → Prop.

Thereafter, we let Q range over postconditions. To obtain concise statements of the reasoning rules of Separation Logic for an imperative λ-calculus, it is convenient to extend separating conjunction and entailment to operate on postconditions. To that end, we generalize the predicates H ⋆ H ′ and H ⊢ H ′ by introducing the predicates Q .

⋆ H ′ and Q . ⊢ Q ′ , written with a dot to suggest pointwise extension. These two predicates are formalized next. Definition 3.13 (Separating conjunction between a postcondition and a heap predicate).

Q . ⋆ H ≡ λv. (Q v ⋆ H )
This operator appears for example in the statement of the frame rule (recall §2.1). The entailment relation for postconditions is a pointwise extension of the entailment relation for heap predicates: Q entails Q ′ if and only if, for any value v, the heap predicate

Q v entails Q ′ v.
Definition 3.14 (Entailment between postconditions).

Q . ⊢ Q ′ ≡ ∀v. (Q v ⊢ Q ′ v)
This entailment defines an order on postconditions. It appears for example in the statement of the consequence rule, which allows strengthening the precondition and weakening the postcondition.

Example 3.15 (Rule of consequence).

H ⊢ H ′ {H ′ } t {Q ′ } Q ′ . ⊢ Q {H } t {Q } conseqence

LANGUAGE SYNTAX AND SEMANTICS

The definition of triples depends on the details of the programming language. Thus, let us first describe the syntax and the semantics of terms.

Syntax

We consider an imperative call-by-value λ-calculus. The syntactic categories are primitive functions π , values v, and terms t. The grammar of values is intended to denote closed values, that is, values without occurrences of free variables. This design choice leads to a simple substitution function, which may be defined as the identity over all values. The primitive operations fall in two categories. First, they include the state-manipulating operations for allocating, reading, writing, and deallocating references. Second, they include Boolean and arithmetic operations. For brevity, we include only the addition and division operations.

The values include the unit value tt, boolean literals b, integer literals n, memory locations p, primitive operations π , and recursive functions μ f .λx .t. The latter construct is written with a hat symbol to denote the fact this value is closed.

The terms include variables, values, function invocation, sequence, let-bindings, conditionals, and function definitions. The latter construct is written µ f .λx .t, this time without a hat symbol. Definition 4.1 (Syntax of the language).

π := ref | get | set | free | (+) | (÷) v := tt | b | n | p | π | μ f .λx .t t := v | x | (t t ) | let x = t in t | if t then t else t | µ f .λx .t eval-val v/s ⇓ v/s eval-fix (µ f .λx .t )/s ⇓ ( μ f .λx .t )/s eval-app v 1 = μ f .λx .t ([v 2 /x] [v 1 /f ] t )/s ⇓ v ′ /s ′ (v 1 v 2 )/s ⇓ v ′ /s ′ eval-let t 1 /s ⇓ v 1 /s ′ ([v 1 /x] t 2 )/s ′ ⇓ v/s ′′ (let x = t 1 in t 2 )/s ⇓ v/s ′′ eval-if If b then (t 1 /s ⇓ v ′ /s ′ ) else (t 2 /s ⇓ v ′ /s ′ ) (if b then t 1 else t 2 )/s ⇓ v ′ /s ′ eval-ref p dom s (ref v)/s ⇓ p/(s[p := v]) eval-free p ∈ dom s (free p)/s ⇓ tt/(s ∖ p) eval-get p ∈ dom s (get p)/s ⇓ (s[p])/s eval-set p ∈ dom s (set p v)/s ⇓ tt/(s[p := v])
eval-add A non-recursive function λx . t may be viewed as a recursive function µ f .λx .t with a dummy name f . Likewise, a sequence (t 1 ; t 2 ) may be viewed as a let-binding of the form let x = t 1 in t 2 for a dummy name x. The Coq formalization actually includes these two constructs explicitly in the grammar to avoid unnecessary complications associated with the elimination of dummy variables.

((+) n 1 n 2 )/s ⇓ (n 1 + n 2 )/s eval-div n 2 0 ((÷) n 1 n 2 )/s ⇓ (n 1 ÷ n 2 )/s
Although our syntax technically allows for arbitrary terms, for simplicity we assume terms to be written in "administrative normal form" (A-normal form), that is, "let x = t 1 in t 2 " is the sole sequencing construct: no sequencing is implicit in any other construct. For instance, the conditional construct "if t then t 1 else t 2 " must be encoded as "let x = t in if x then t 1 else t 2 ". This presentation is intended to simplify the statement of the evaluation rules and reasoning rules. Note that many practical program verification tools perform code normalization as a preliminary step.

Semantics

Thereafter, we use the meta-variable s to denote a variable of type heap that corresponds to a full memory state at a given point in the execution, in contrast to the meta-variable h, which denotes a heap that may correspond to only a piece of the memory state.

The semantics of the language is described by the big-step judgment t/s ⇓ v/s ′ , which asserts that the term t, starting from the state s, evaluates to the value v and the final state s ′ . Definition 4.2 (Semantics of the language). The evaluation rules appear in Fig. 2.

The rules are standard. A value evaluates to itself. Likewise, a function evaluates to itself. The evaluation rules for function calls and let-bindings involve the standard (capture-avoiding) substitution operation: [v/x] t denotes the substitution of x by v throughout the term t. The evaluation rule for conditionals is stated concisely using Coq's conditional construct. The primitive operations on reference cells are described using operations on finite maps: dom s denotes the domain of the state s, the operation s[p] returns the value associated with p, the operation s ∖ p removes the binding on p, and the operation s[p : = v] sets or updates a binding from p to v.

TRIPLES AND REASONING RULES

Separation Logic Triples

Separation Logic is a refinement of Hoare logic. Interestingly, Separation Logic triples can be defined in terms of Hoare triples.

A Hoare triple, written HOARE {H } t {Q }, asserts that in any state s satisfying the precondition H , the evaluation of the term t terminates and produces output value v and output state s ′ , as described by the evaluation judgment t/s ⇓ v/s ′ . Moreover, the output value and output state satisfy the postcondition Q, in the sense that Q v s ′ holds. This definition captures termination: it defines a total correctness triple. (The definition can be easily adapted to capture partial correctness only.) Definition 5.1 (Total correctness Hoare triple).

HOARE {H } t {Q } ≡ ∀s. H s ⇒ ∃v. ∃s ′ . (t/s ⇓ v/s ′ ) ∧ (Q v s ′ )
Whereas a Hoare triple describes the evaluation of a term with respect to the whole memory state, a Separation Logic triple describes the evaluation of a term with respect to only a fragment of the memory state. To relate the two concepts, it suffices to quantify over "the rest of the state", that is, the part of the state that the evaluation of the term is not concerned with.

A Separation Logic triple, written {H } t {Q }, asserts that, for any heap predicate H ′ describing the "rest of the state", the Hoare triple HOARE {H ⋆ H ′ } t {Q .

⋆ H ′ } holds. This formulation effectively bakes in the frame rule, by asserting from the very beginning that specifications are intended to preserve any resource that is not mentioned in the precondition.

{H } t {Q } ≡ ∀H ′ . HOARE {H ⋆ H ′ } t {Q . ⋆ H ′ }
To fully grasp the meaning of a Separation Logic triple, it helps to contemplate an alternative definition expressed directly with respect to the evaluation judgment. This alternative definition, shown below, reads as follows: if the input state decomposes as a part h 1 that satisfies the precondition H and a disjoint part h 2 that describes the rest of the state, then the term t terminates on a value v, producing a heap made of a part h ′ 1 and, disjointly, the part h 2 which was unmodified; moreover, the value v and the heap h ′ 1 together satisfy the postcondition Q. Definition 5.3 (Alternative definition of total correctness Separation Logic triples).

{H } t {Q } ≡ ∀h 1 . ∀h 2 . H h 1 h 1 ⊥ h 2 ⇒ ∃v. ∃h ′ 1 .        h ′ 1 ⊥ h 2 t/(h 1 ⊎ h 2 ) ⇓ v/(h ′ 1 ⊎ h 2 ) Q v h ′ 1
The reasoning rules of Separation Logic fall in three categories. First, the structural rules: they do not depend on the details of the language. Second, the reasoning rules for terms: there is one such rule for each term construct of the language. Third, the specification of the primitive operations: there is one such rule for each primitive operation. All these rules are presented next.

Structural Rules

The structural rules of Separation Logic include the consequence rule and the frame rule, which were already discussed, and two rules for extracting pure facts and existential quantifiers out of preconditions. (The role of these rules is illustrated in the example proof presented in the appendix.) Lemma 5.4 (Structural rules of Separation Logic). The following reasoning rules can be stated as lemmas and proved correct with respect to the interpretation of triples given by Definition 5.2.

consequence H ⊢ H ′ {H ′ } t {Q ′ } Q ′ . ⊢ Q {H } t {Q } frame {H } t {Q } {H ⋆ H ′ } t {Q . ⋆ H ′ } prop P ⇒ {H } t {Q } {[P] ⋆ H } t {Q } exists ∀x . {H } t {Q } {∃ ∃x . H } t {Q }
The frame rule may be exploited in practice as a forward reasoning rule: given a triple {H } t {Q }, one may derive another triple by extending both the precondition and the postcondition with a heap predicate H ′ . This rule is, however, almost unusable as a backward reasoning rule: indeed, it is extremely rare for a proof obligation to be exactly of the form {H ⋆ H ′ } t {Q .

⋆ H ′ }. In order to exploit the frame rule in backward reasoning, one usually needs to first invoke the consequence rule. The effect of a combined application of the consequence rule followed with the frame rule is captured by the combined consequence-frame rule, stated below. Lemma 5.5 (Combined conseqence-frame rule).

H ⊢ H 1 ⋆ H 2 {H 1 } t {Q 1 } Q 1 . ⋆ H 2 . ⊢ Q {H } t {Q } consequence-frame
This combined rule applies to a proof obligation of the form {H } t {Q }, with no constraints on the precondition nor the postcondition. To prove this triple from an existing triple {H 1 } t {Q 1 }, it suffices to show that the precondition H decomposes as H 1 ⋆H 2 , and to show that the postcondition Q can be recovered from Q 1 .

⋆H 2 . The "framed" heap predicate H 2 can be computed as the difference between H and H 1 . In practice, though, rather than trying to instantiate H 2 in the consequence-frame rule, it is more effective to exploit the ramified frame rule ( §7.3).

Rules for Terms

The program logic includes one rule for each term construct. The corresponding rules are stated below and explained next. Lemma 5.6 (Reasoning rules for terms in Separation Logic). The following rules can be stated as lemmas and proved correct with respect to the interpretation of triples given in Definition 5.2.

H ⊢ (Q v) {H } v {Q } val H ⊢ (Q ( μ f .λx .t )) {H } (µ f .λx .t ) {Q } fix v 1 = μ f .λx .t {H } ([v 2 /x] [v 1 /f ] t ) {Q } {H } (v 1 v 2 ) {Q } app {H } t 1 {λv. H ′ } {H ′ } t 2 {Q } {H } (t 1 ; t 2 ) {Q } seq {H } t 1 {Q ′ } ∀v. {Q ′ v} ([v/x] t 2 ) {Q } {H } (let x = t 1 in t 2 ) {Q } let b = true ⇒ {H } t 1 {Q } b = false ⇒ {H } t 2 {Q } {H } (if b then t 1 else t 2 ) {Q } if
The rules val and fix apply to terms that correspond to closed values. A value evaluates to itself, without modifying the state. If the heap at hand is described in the precondition by the heap predicate H , then this heap, together with the value v, should satisfy the postcondition. This implication is captured by the premise H ⊢ Q v. Note that the rules val and fix can also be formulated using triples featuring an empty precondition. Lemma 5.7 (Small-footprint reasoning rules for values).

{ [ ] } v {λr . [r = v]} val' { [ ] } (µ f .λx .t ) {λr . [r = ( μ f .λx .t )]} fix'
The app rule merely reformulates the β-reduction rule. It asserts that reasoning about the application of a function to a particular argument amounts to reasoning about the body of this function in which the name of the argument gets substituted with the value of the argument involved in the application. This rule is typically exploited to begin the proof of the specification triple for a function. Once established, such a specification triple may be invoked for reasoning about calls to that function.

The seq rule asserts that a sequence "t 1 ; t 2 " admits precondition H and postcondition Q provided that t 1 admits the precondition H and a postcondition describing a heap satisfying H ′ , and that t 2 admits the precondition H ′ and the postcondition Q. (The result value v produced by t 1 is ignored.)

The let rule enables reasoning about a let-binding of the form "let x = t 1 in t 2 ". It reads as follows. Assume that, in the current heap described by H , the evaluation of t 1 produces a postcondition Q ′ . Assume also that, for any value v that the evaluation of t 1 might produce, the evaluation of [v/x] t 2 in a heap described by Q ′ v produces the postcondition Q. Then, under the precondition H , the term "let x = t 1 in t 2 " produces the postcondition Q.

The if rule enables reasoning about a conditional. Its statement features two premises: one for the case where the condition is the value true, and one for the case where it is the value false.

Specification of Primitive Operations

The third and last category of reasoning rules corresponds to the specification of the primitive operations of the language. The operations on references have already been discussed ( §2. 5 and §2.8). The arithmetic operations admit specifications that involve only empty heaps.

Lemma 5.8 (Specification for primitive operations).

ref:

{[ ]} (ref v) {λr . ∃ ∃p. [r = p] ⋆ (p → v)} get: {p → v} (get p) {λr . [r = v] ⋆ (p → v)} set: {p → v} (set p v ′ ) {λ_. (p → v ′ )} free: {p → v} (free p) {λ_. [ ]} add: {[ ]} ((+) n 1 n 2 ) {λr . [r = n 1 + n 2 ]} div: n 2 0 ⇒ {[ ]} ((÷) n 1 n 2 ) {λr . [r = n 1 ÷ n 2 ]}
This completes the presentation of the reasoning rules of Separation Logic. Technically, these 18 reasoning rules suffice to verify imperative programs, although additional infrastructure helps obtain more concise proof scripts. The Coq formalization of the material from Sections §3, §4, and §5 amount to 564 non-blank lines of Coq script. It includes 23 definitions, 59 lemmas, 24 lines of tactic definitions, and 117 lines of proofs. We encourage the reader to check out the corresponding file, which is called SLFMinimal.v in the supplementary material [START_REF] Charguéraud | [END_REF]].

INDUCTIVE REASONING FOR LOOPS

Pointer-manipulating programs are typically written using loops. Although loops can be simulated using recursive functions, it simplifies the proofs to include direct reasoning rules for them. Let us assume in this section the presence of a while-loop construct, written "while t 1 do t 2 ".

A loop "while t 1 do t 2 " is equivalent to its one-step unfolding: if t 1 evaluates to true, then t 2 is executed and the loop proceeds; otherwise the loop terminates on the unit value. The rules eval-while and while shown below capture this one-step unfolding principle. Lemma 6.1 (Evaluation rule and reasoning rules for while loops). eval-while (if t 1 then (t 2 ; while t One may establish a triple about the behavior of a while loop by conducting a proof by induction over a decreasing measure or well-founded relation, exploiting the induction hypothesis to reason about the "remaining iterations". Note that this approach is essentially equivalent to encoding the loop as a tail-recursive function, yet without the boilerplate associated with an encoding. Example 6.2 (Length of a list using a while loop). Consider the following code fragment, which sets the contents of s to the length of the mutable list at location p. Applying the while rule reveals the conditional on whether !r is null. In the case where it is not null, s is incremented, r is set to the tail of the current list, and the loop starts over. To reason about this "recursive invocation" of the while-loop, it suffices to apply the frame rule to put aside the head cell described by a predicate of the form (p.head → x ) ⋆ (p.tail → q), and to apply the induction hypothesis to the tail of the list described by Mlist L ′ q, where L = x :: L ′ .

1 do t 2 ) else tt)/s ⇓ v/s ′ (while t 1 do t 2 )/s ⇓ v/s ′ while {H } (if
The above example shows that, by carrying a proof by induction, it is possible to apply the frame rule over the remaining iterations of a loop. Doing so would not be possible with a reasoning rule that imposes a loop invariant to be valid both at the entry point and exit point of the loop body. Indeed, such a loop invariant would necessarily involve the description of a list segment.

THE MAGIC WAND OPERATOR

Definition and Properties of the Magic Wand

The magic wand, also known as separating implication, is an additional heap predicate operator, written H 1 -⋆H 2 , and read "H 1 wand H 2 ". Although it is technically possible to carry out all Separation Logic proofs without the magic wand, this operator helps to state several reasoning rules and specifications more concisely.

Intuitively, H 1 -⋆H 2 defines a heap predicate such that, if starred with H 1 , it produces H 2 . In other words, the magic wand satisfies the cancellation rule H 1 ⋆ (H 1 -⋆H 2 ) ⊢ H 2 . The magic wand operator can be formally defined in at least four different ways.

Definition 7.1 (Magic wand). The magic wand operator is equivalently characterized by:

(1)

H 1 -⋆H 2 ≡ λh. ∀h ′ . h ⊥ h ′ ∧ H 1 h ′ ⇒ H 2 (h ⊎ h ′ ) (2) H 1 -⋆H 2 ≡ ∃ ∃H 0 . H 0 ⋆ (H 1 ⋆ H 0 ) ⊢ H 2 (3) H 0 ⊢ (H 1 -⋆H 2 ) ⇔ (H 1 ⋆ H 0 ) ⊢ H 2
(4) H 1 -⋆H 2 satisfies the following introduction and elimination rules.

(H 1 ⋆ H 0 ) ⊢ H 2 H 0 ⊢ (H 1 -⋆H 2 ) wand-intro H 1 ⋆ (H 1 -⋆H 2 ) ⊢ H 2 wand-cancel
The first characterization asserts that H 1 -⋆H 2 holds of a heap h if and only if, for any disjoint heap h ′ satisfying H 1 , the union of the two heaps h ⊎ h ′ satisfies H 2 .

The second characterization describes a heap satisfying a predicate H 0 that, when starred with H 1 entails H 2 . This characterization shows that the magic wand can be encoded using previouslyintroduced concepts from higher-order Separation Logic.

The third characterization consists of an equivalence that provides both an introduction rule and an elimination rule. The left-to-right direction is equivalent to the cancellation rule wand-cancel stated in definition (4). The right-to-left direction corresponds exactly to the introduction rule from definition (4), namely wand-intro, which reads as follows: to show that a heap described by H 0 satisfies the magic wand H 1 ⋆ H 2 , it suffices to prove that H 1 starred with H 0 entails H 2 .

In practice, the following properties are useful for working with the magic wand and for implementing a tactic that simplifies the proof obligations that arise from the ramified frame rule ( §7.3). Lemma 7.2 (Useful properties of the magic wand).

wand-monotone

H ′ 1 ⊢ H 1 H 2 ⊢ H ′ 2 (H 1 -⋆H 2 ) ⊢ (H ′ 1 -⋆H ′ 2 ) wand-self [ ] ⊢ (H -⋆H )
wand-pure-l P

([P] -⋆H ) = H wand-curry ((H 1 ⋆ H 2 ) -⋆H 3 ) = (H 1 -⋆(H 2 -⋆H 3 ))
wand-star

((H 1 -⋆H 2 ) ⋆ H 3 ) ⊢ (H 1 -⋆(H 2 ⋆ H 3 ))
Lemma 7.3 (Partial concellation of a magic wand). If the left-hand side of a magic wand involves the separating conjunction of several heap predicates, it is possible to cancel out just one of them with an occurrence of the same heap predicate occurring outside of the magic wand. For example, the entailment

H 2 ⋆ (H 1 ⋆ H 2 ⋆ H 3 ) -⋆H 4 ⊢ (H 1 ⋆ H 3 ) -⋆H 4 is obtained by cancelling H 2 .

Magic Wand for Postconditions

Just as useful as the magic wand is its generalization to postconditions, which is involved for example in the statement of the ramified frame rule ( §7.3). This operator, written Q 1 . -⋆ Q 2 , takes as argument two postconditions Q 1 and Q 2 and produces a heap predicate.

Definition 7.4 (Magic wand for postconditions). The operator (. -⋆ ) is equivalently defined by:

(1) Q 1 . -⋆ Q 2 ≡ ∀ ∀v. (Q 1 v) -⋆(Q 2 v) (2) Q 1 . -⋆ Q 2 ≡ λh. ∀vh ′ . h ⊥ h ′ ∧ Q 1 v h ′ ⇒ Q 2 v (h ⊎ h ′ ) (3) Q 1 . -⋆ Q 2 ≡ ∃ ∃H 0 . H 0 ⋆ (Q 1 . ⋆ H 0 ) . ⊢ Q 2 (4) H 0 ⊢ (Q 1 . -⋆ Q 2 ) ⇔ (Q 1 . ⋆ H 0 ) . ⊢ Q 2 (5) Q 1 .
-⋆ Q 2 satisfies the following introduction and elimination rules.

(Q 1 . ⋆ H 0 ) . ⊢ Q 2 H 0 ⊢ (Q 1 . -⋆ Q 2 ) qwand-intro Q 1 . ⋆ (Q 1 . -⋆ Q 2 ) . ⊢ Q 2 qwand-cancel
Lemma 7.5 (Useful properties of the magic wand for postconditions). qwand-monotone

Q ′ 1 . ⊢ Q 1 Q 2 . ⊢ Q ′ 2 (Q 1 . -⋆ Q 2 ) ⊢ (Q ′ 1 . -⋆ Q ′ 2 ) qwand-self [ ] ⊢ (Q . -⋆ Q ) qwand-star ((Q 1 . -⋆ Q 2 ) . ⋆ H ) ⊢ (Q 1 . -⋆ (Q 2 ⋆ H )) qwand-specialize Q 1 . -⋆ Q 2 ⊢ (Q 1 v) . -⋆ (Q 2 v)

Ramified Frame Rule

One key practical application of the magic wand operator appears in the statement of the ramified frame rule. This rule reformulates the consequence-frame rule in a manner that is both more concise and better-suited for automated processing. Recall the rule conseqence-frame, which is reproduced below. To exploit it, one must provide a predicate H 2 describing the "framed" part.

Providing the heap predicate H 2 by hand in proofs involves a prohibitive amount of work; it is strongly desirable that H 2 may be inferred automatically.

The predicate H 2 can be computed as the difference between H and H 1 . Automatically computing this difference is relatively straightforward in simple cases, however this task becomes quite challenging when H and H 1 involve numerous quantifiers. Indeed, it is not obvious to determine which quantifiers from H should be cancelled against those from H 1 , and which quantifiers should be carried over to H 2 .

The benefit of the ramified frame rule is that it eliminates the problem altogether. The key idea is to observe that the premise

Q 1 . ⋆ H 2 . ⊢ Q from the conseqence-frame rule is equivalent to H 2 . ⊢ (Q 1 . -⋆ Q ),
by the 4th characterization of Definition 7.4. Thus, in the other premise H ⊢ H 1 ⋆H 2 , the heap predicate H 2 may be replaced with Q 1 . -⋆ Q. The ramified-frame rule appears below. Lemma 7.6 (Ramified frame rule). ramified-frame reformulates consequence-frame.

consequence-frame

H ⊢ H 1 ⋆ H 2 {H 1 } t {Q 1 } Q 1 . ⋆ H 2 . ⊢ Q {H } t {Q } ramified-frame {H 1 } t {Q 1 } H ⊢ H 1 ⋆ (Q 1 . -⋆ Q ) {H } t {Q } 8 PARTIALLY-AFFINE SEPARATION LOGIC

Linear and Affine Heap Predicates

The Separation Logic presented so far is well-suited for a language with explicit deallocation. It is, however, impractical for a language equipped with a garbage collector. Indeed, it does not provide any rule for discarding the description of pieces of state that are ready for the garbage collector to dispose of. The aim of this section is to refine the definitions presented so far to support rules that enable discarding certain heap predicates from either the precondition or the postcondition. The formalization presented is general enough to allow fine-tuning between affine heap predicates, which may be freely discarded, and linear heap predicates, which, on the contrary, must remain accounted for. For example, linearity is useful to ensure that every file handle opened eventually gets closed, or to ensure that every lock acquired eventually gets released. To that end, the reasoning rules should not allow discarding the heap predicates that represent linear resources.

In technical terms, a Separation Logic is said to be linear if no heap predicates can be discardedlike in original presentations of Separation Logic. A Separation Logic is said to be affine if any heap predicates may be freely discarded at any time. The purpose of this section is to set up a partially-affine Separation Logic, in which both linear and affine heap predicates may coexist.

Customizable Characterization of Affine Heap Predicates

The predicate affine H asserts that the heap predicate H may be freely discarded. This predicate is defined in terms of a lower-level predicate, written haffine h, that characterizes which heaps may be discarded. This predicate is axiomatized. Two specific instantiations are presented: one that treats all heaps as discardable, leading to a fully-affine logic, and one that treats none of them as discardable, leading to a fully-linear logic, equivalent to the logic developed so far. Definition 8.1 (Axiomatization of affine heaps). The predicate haffine h must satisfy two rules:

haffine ∅ staffine-empty haffine h 1 haffine h 2 h 1 ⊥ h 2 haffine (h 1 ⊎ h 2 ) staffine-union
The predicate affine H characterizes heap predicates that hold only of affine heaps.

Definition 8.2 (Definition of affine heap predicates). affine H ≡ ∀h. H h ⇒ haffine h

The rules presented next establish that the composition of affine heap predicates yield affine heap predicates. In other words, the predicate affine is stable by composition. For example, a heap predicate H 1 ⋆ H 2 is affine provided that H 1 and H 2 are both affine. A heap predicate ∃ ∃x . H is affine provided that H is affine for any variable x. Likewise, a heap predicate ∀ ∀x . H is affine provided that H is affine for any variable x, with a technical restriction asserting that the type of x must be inhabited (because, otherwise, the hypothesis would be vacuous). In practice, the application of these rules is automated using a tactic, thus the process of justifying that a heap predicate is affine is in most cases totally transparent for the user.

To state the reasoning rules that enable discarding affine heap predicates, it is helpful to introduce the affine top heap predicate, which is written ⊤ ⊤. Whereas the top heap predicate (written ⊤ and defined as "λh. true") holds of any heap, the affine top predicate holds only of any affine heap. Definition 8.4 (Affine top). The predicate ⊤ ⊤ can be equivalently defined in two ways.

(1) ⊤ ⊤ ≡ λh. haffine h

(2) ⊤ ⊤ ≡ ∃ ∃H .

[affine H ] ⋆ H

There are three important properties of ⊤ ⊤. The first one asserts that any affine heap predicate H entails ⊤ ⊤. The second one asserts that the predicate ⊤ ⊤ is itself affine. The third one asserts that several copies of ⊤ ⊤ are equivalent to a single ⊤ ⊤.

Lemma 8.5 (Properties of affine top).

affine

H H ⊢ ⊤ ⊤ atop-r affine ⊤ ⊤ affine-atop (⊤ ⊤ ⋆ ⊤ ⊤) = ⊤ ⊤ star-atop-atop
All the aforementioned definitions and lemmas hold for any predicate haffine satisfying the axiomatization from Definition 8.1. Two extreme instantiations of haffine are particularly interesting.

Example 8.6 (Fully-affine Separation Logic). The definition "haffine h ≡ True" satisfies the requirements of Definition 8.1, and leads to a Separation Logic where all heap predicates may be freely discarded. In that setting, (affine H ) ⇔ True, and ⊤ ⊤ = ⊤ = (λh. true) = (∃ ∃H . H ).

Example 8.7 (Fully-linear Separation Logic). The definition "haffine h ≡ (h = ∅)" satisfies the requirements of Definition 8.1, and leads to a Separation Logic where no heap predicate may be freely discarded. In that setting, (affine H ) ⇔ (H ⊢ [ ]), and ⊤ ⊤ = [ ] = (λh. h = ∅).

Triples for a Partially-Affine Separation Logic

To accommodate reasoning rules that enable freely discarding affine heap predicates, it suffices to refine the definition of a Separation Logic triple (Definition 5.2) by integrating the affine top predicate ⊤ ⊤ into the postcondition of the underlying Hoare triple, as formalized next. triple involving t and Q entails wp t Q. The second characterization consists of a reformulation of the first characterization in terms of basic logic operators.

The third characterization defines wp t Q as a predicate over a heap h, asserting that wp t Q holds of the heap h if and only if the evaluation of the term starting from a heap equal to h produces the postcondition Q.

The fourth characterization asserts that wp t Q is entailed by any heap predicate H satisfying the triple {H } t {Q }. This characterization shows that the notion of weakest precondition can be expressed as a derived notion in terms of the core heap predicate operators.

The fifth characterization asserts that any triple of the form {H } t {Q } may be equivalently reformulated by replacing this triple with H ⊢ wp t Q.

The developer of a practical tool based on Separation Logic may choose to take either triples or weakest-preconditions as a primitive notion; the other notion may then be derived in terms of that primitive notion. The notion of triple is typically defined in terms of wp using characterization [START_REF] Appel | Program Logics for Certified Compilers[END_REF], in the right-to-left direction. Reciprocally, the definition of wp can be defined in terms of triples. The choice of the encoding depends on the strength of the host logic with respect to existential quantification. Definition (3) makes weaker assumptions, whereas Definition (4) leverages the ability to existentially quantify over heap predicates. Definition (4), which is expressed at the level of heap predicates, is generally much simpler to manipulate in proofs.

WP-Style Structural Rules

The structural reasoning rule can be reformulated in weakest-precondition style, as follows.

Lemma 9.2 (Structural rules in weakest precondition style).

Q . ⊢ Q ′ wp t Q ⊢ wp t Q ′ wp-consequence (wp t Q ) ⋆ H ⊢ wp t (Q . ⋆ H ) wp-frame affine H (wp t Q ) ⋆ H ⊢ (wp t Q ) wp-discard-pre wp t (Q . ⋆ ⊤ ⊤) ⊢ wp t Q wp-atop-post
The rule wp-conseqence captures a monotonicity property. The rule wp-frame reads as follows: if I own a heap in which the execution of t produces the postcondition Q, and, separately, I own a heap satisfying H , then, altogether, I own a heap in which the execution of t produces both Q and H . These four structural rules may be combined into a single rule, called wp-ramified-frame-atop, which subsumes all the other structural rules of Separation Logic. Lemma 9.3 (Ramified frame rule in weakest precondition style).

(wp t Q ) ⋆ (Q . -⋆ (Q ′ . ⋆ ⊤ ⊤)) ⊢ (wp t Q ′ )
wp-ramified-frame-atop

WP-Style Rules For Terms

The weakest-precondition style reformulation of the reasoning rules for terms yields rules that are similar to the corresponding Hoare logic rules. For example, the rule for sequence is as follows.

wp t 1 (λv. wp t 2 Q ) ⊢ wp (t 1 ; t 2 ) Q wp-seq
This rule can be read as follows: if I own a heap in which the execution of t 1 produces a heap in which the execution of t 2 produces the postcondition Q, then I own a heap in which the execution of the sequence "t 1 ; t 2 " produces Q. The other reasoning rules for terms appear below.

Lemma 9.4 (Reasoning rules for terms in weakest precondition style).

wp-val

Q v ⊢ wp v Q wp-fix Q ( μ f .λx .t ) ⊢ wp (µ f .λx .t ) Q wp-app v 1 = μ f .λx .t wp ([v 2 /x] [v 1 /f ] t ) Q ⊢ wp (v 1 v 2 ) Q wp t 1 (λv. wp ([v/x] t 2 ) Q ) ⊢ wp (let x = t 1 in t 2 ) Q wp-let If b then (wp t 1 Q ) else (wp t 2 Q ) ⊢ wp (if b then t 1 else t 2 ) Q wp-if

WP-Style Function Specifications

Function specifications were so far expressed using triples of the form {H } ( f v) {Q }. These specifications may be equivalently expressed using assertions of the form H ⊢ wp ( f v) Q.

The primitive operations are specified using wp as shown below. For example, the allocation operation ref v produces a postcondition Q, provided that the result of extending the current precondition with p → v yields Q p. In the formal statement of the specification wp-ref, observe how the address p is quantified universally in the left-hand side of the entailment. Lemma 9.5 (Specification of primitive operations in weakest-precondition style).

wp-ref :

∀ Q v. ∀ ∀p. (p → v) -⋆(Q p) ⊢ wp (ref v) Q wp-get : ∀ Q p. (p → v) ⋆ (p → v) -⋆(Q v) ⊢ wp (get p) Q wp-set : ∀ Q p v v ′ . (p → v) ⋆ ∀ ∀r . (p → v ′ ) -⋆(Q r ) ⊢ wp (set p v ′ ) Q wp-free : ∀ Q p v. (p → v) ⋆ ∀ ∀r . (Q r )) ⊢ wp (free p) Q
Remark: wp-set and wp-free can also be stated by specializing the variable r to the unit value tt.

There exists a general pattern for translating from conventional triples to weakest-precondition style specifications. The following lemma covers the case of a specification involving a single auxiliary variable named x. It may easily be generalized to a larger number of auxiliary variables. Lemma 9.6 (Specifications in weakest-precondition style). Let v denote a value that may depend on a variable x, and let H ′ denote a heap predicate that may depend on the variables x and r .

{H } t {λr . ∃ ∃x . [r = v] ⋆ H ′ } ⇔ ∀Q. H ⋆ (∀ ∀x . H ′ -⋆(Q v)) ⊢ wp t Q
Stating specifications in weakest-precondition style is not at all mandatory for working with reasoning rules in weakest-precondition style. Indeed, one may continue stating specifications using conventional triples, which one might find more intuitive to read, and exploit the following rule for reasoning about function applications. Lemma 9.7 (Variant of the ramified frame rule for proof obligations in wp style).

{H 1 } t {Q 1 } H ⊢ H 1 ⋆ (Q 1 . -⋆ Q ) H ⊢ wp t Q ramified-frame-for-wp 10 RELATED WORK
For a broad survey of Separation Logic, we refer to O'Hearn's CACM paper [2019]. In particular, its appendix covers practical automated and semi-automated tools based on Separation Logic, such as Infer [START_REF] Calcagno | Moving Fast with Software Verification[END_REF], VeriFast [START_REF] Philippaerts | Software Verification with VeriFast: Industrial Case Studies[END_REF], or Viper [START_REF] Müller | Viper: A Verification Infrastructure for Permission-Based Reasoning[END_REF]. In this related work section, we focus on tools that leverage Separation Logic in interactive proofs assistants for verifying sequential programs, and on the comparison with other teaching material.

Original Presentation of Separation Logic

Traditional presentations of Separation Logic target command-based languages, which involve mutable variables in addition to heap-allocated data. In that setting, the statement of the frame rule involves a side-condition to assert that the mutable variables occurring in the framed heap predicate are not modified by the command. Up to minor differences in presentation, many fundamental concepts appeared in the first descriptions of Separation Logic [START_REF] O'hearn | Local Reasoning about Programs that Alter Data Structures[END_REF][START_REF] Reynolds | Separation Logic: A Logic for Shared Mutable Data Structures[END_REF]]:

• the grammar of heap predicate operators, except the pure heap predicate [P], and with the limitation that quantifiers ∃ ∃x . H and ∀ ∀x . H range only over integer values; • the rule of consequence and the frame rules;

• a variant of the rule exists (this variant is named exists2 in the appendix);

• the fundamental properties of the star operator described in Lemma 3.9;

• the small footprint specifications for primitive state-manipulating operations,

• the definition of Mlist, stated by pattern-matching over the list structure like in Definition 2.7;

• the characterization of the magic wand operator via characterizations (1), ( 3) and ( 4) from Definition 7.1, but not characterization (2), which involves quantification over heap predicates; • the example of a copy function for binary trees;

• the encoding of records and arrays using pointer arithmetics (described in the appendix).

Additional Features of Separation Logic

The original presentation of Separation Logic consists of a first-order logic for a first-order language. [START_REF] Biering | BI Hyperdoctrines and Higher-Order Separation Logic[END_REF][START_REF] Biering | BI-Hyperdoctrines, Higher-Order Separation Logic, and Abstraction[END_REF] tackled the generalization to higher-order quantification-the possibility to quantify over propositions and heap predicates-through the introduction of BI-hyperdoctrines. [START_REF] Neelakantan | Modular verification of the subject-observer pattern via higher-order separation logic[END_REF] formalized the subject-observer pattern with a strong form of information hiding between the subject and the client. This work illustrated how higher-order Separation Logic supports data abstraction. [START_REF] Birkedal | Semantics of separation-logic typing and higher-order frame rules[END_REF][START_REF] Birkedal | Semantics of separation-logic typing and higher-order frame rules for algol-like languages, PrakashEditor Panangaden[END_REF] tackled the generalization of Separation Logic to higher-order languages, where functions may take functions as arguments. To avoid complications with mutable variables, the authors considered a version of Algol with immutable variables and first-order heaps-heap cells can only store integer values. Specifications are presented using dependent types: a triple {H } t {Q } is expressed by the fact that the term t admits the type "{H } • {Q }". One key idea from this work is to bake-in the frame rule into the interpretation of triples, that is, to quantify over a heap predicate describing the rest of the state, as in Definition 5.2. The technique of the baked-in frame rule later proved successful in mechanized proofs. For example, it appears in the HOL4 formalization by [START_REF] Myreen | Hoare Logic for Realistically Modelled Machine Code[END_REF] (see §3.2, as well as §2.4 from Myreen's PhD thesis [2008]) and in the Coq formalization by [START_REF] Appel ; Dockins | Program logics for certified compilers[END_REF] (see Definition 9). [START_REF] Reus | Separation Logic for Higher-Order Store[END_REF] presented a generalization of Separation Logic to higher-order stores, where heap cells may store functions whose execution may act over the heap. The former work targets a language that features storable, parameter-less procedures. Its model, developed on paper, was then simplified by [START_REF] Birkedal | A Simple Model of Separation Logic for Higher-Order Store[END_REF] using the technique of the baked-in frame rule.

Another approach to tackling the circularity issues associated with higher-order quantification and higher-order stores consists of using the step indexing technique [START_REF] Jamil | Semantics of Types for Mutable State[END_REF][START_REF] Appel | An Indexed Model of Recursive Types for Foundational Proof-Carrying Code[END_REF][START_REF] Appel | A Very Modal Model of a Modern, Major, General Type System[END_REF]]. In that approach, a heap predicate depends not only on a heap but also on a natural number, which denotes the number of execution steps for which the predicate is guaranteed to hold. This approach was later exploited in VST, which provided the first higher-order concurrent Separation Logic [START_REF] Hobor | Oracle Semantics for Concurrent Separation Logic[END_REF]. [START_REF] Ni | Certified Assembly Programming with Embedded Code Pointers[END_REF] presented the XCAP framework, formalized in Coq. It targets an assemblylevel language with embedded code pointers, thereby supporting both higher-order functions and higher-order stores. XCAP features impredicative polymorphism, allowing heap predicates to quantify over heap predicates. This work addresses the same problem as the aforementioned work through a more syntactic approach.

When reasoning about first-class functions, the notion of nested triple naturally appears: triples may occur inside the pre-or post-condition of other triples. Nested triples were described in work by [START_REF] Schwinghammer | Nested Hoare Triples and Frame Rules for Higher-Order Store[END_REF] for functions stored in the heap, and in work by [START_REF] Kasper Svendsen | Verifying Generics and Delegates[END_REF]] for higher-order functions (more precisely, for delegate functions). Nested triples are naturally supported by shallow embeddings of Separation Logic in higher-order logic proof assistants. This possibility is mentioned explicitly by [START_REF] Wang | A Simple Model for Certifying Assembly Programs with First-Class Function Pointers[END_REF]], but was already implicitly available in earlier formalizations, e.g. [START_REF] Appel ; Dockins | Program logics for certified compilers[END_REF]. [START_REF] Neel | Verifying Event-Driven Programs Using Ramified Frame Properties[END_REF] introduced the idea of a ramified frame rule. The general statement of the ramified rule stated as in Lemma 7.6 appeared in [START_REF] Hobor | The Ramifications of Sharing in Data Structures[END_REF]. Users of the tools VST [START_REF] Cao | Proof pearl: Magic wand as frame[END_REF] and Iris [START_REF] Jung | RustBelt: Securing the Foundations of the Rust Programming Language[END_REF]] have advertised for the interest of this rule.

The magic wand between postconditions, written Q 1 . -⋆ Q 2 , as opposed to the use of an explicit quantification ∀ ∀v. Q 1 v -⋆Q 2 v, appears to have first been employed by [START_REF] Bengtson | Charge![END_REF]. This operator is described in the book by [START_REF] Appel | Program Logics for Certified Compilers[END_REF]. The five equivalent characterizations of this operator give in Definition 7.4 appear to be a (very minor) contribution of the present paper.

Regarding while loops, the possibility to frame over the remaining iterations ( §6) is inherently available when a loop is encoded as a recursive functions, or when a loop is presented in CPS-styletypical with assembly-level code [START_REF] Chlipala | Mostly-Automated Verification of Low-Level Programs in Computational Separation Logic[END_REF][START_REF] Ni | Certified Assembly Programming with Embedded Code Pointers[END_REF]. The statement of a reasoning rule directly applicable to a non-encoded loop construct, and allowing to frame over the remaining iterations, has appeared independently in work by [START_REF] Charguéraud | Characteristic Formulae for Mechanized Program Verification[END_REF] and [START_REF] Tuerk | Local Reasoning about While-Loops[END_REF].

A number of interesting extensions of Separation Logic for deterministic sequential programs were beyond the scope of the present paper. Let us cite a few.

The notion of Separation Algebra [START_REF] Calcagno | Local Action and Abstract Separation Logic[END_REF][START_REF] Dockins | A Fresh Look at Separation Algebras and Share Accounting[END_REF][START_REF] Gotsman | Precision and the Conjunction Rule in Concurrent Separation Logic[END_REF][START_REF] Klein | Mechanised Separation Algebra[END_REF]] is useful for developing a Separation Logic framework independently from the details of the programming language. [START_REF] Costanzo | A Case for Behavior-Preserving Actions in Separation Logic[END_REF] present a refined definition of local reasoning to ensure that, whenever a program runs safely on some state, adding more state would have no effect on the program's behavior; their definition is useful in particular for nondeterministic programs and programs executed in a finite memory. Fictional Separation Logic [Jensen and Birkedal 2012] generalizes the interpretation of separating conjunction beyond physical separation, and explains how to combine several separation algebras. Temporary read-only permissions [START_REF] Charguéraud | Temporary Read-Only Permissions for Separation Logic[END_REF]] provide a simpler alternative to fractional permission for manipulating duplicatable read-only resources in a sequential program. Time credits [START_REF] Charguéraud | Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation[END_REF]] allow for amortized cost analysis. Time receipts [START_REF] Mével | Time credits and time receipts in Iris[END_REF]] may be used to establish lower bounds on the execution time. The higher-order frame [START_REF] Birkedal | Semantics of separation-logic typing and higher-order frame rules[END_REF][START_REF] Birkedal | Semantics of separation-logic typing and higher-order frame rules for algol-like languages, PrakashEditor Panangaden[END_REF] and the higher-order anti-frame [START_REF] Pottier | Hiding local state in direct style: a higher-order anti-frame rule[END_REF][START_REF] Schwinghammer | A Semantic Foundation for Hidden State[END_REF]] allow reasoning about hidden state in sequential programs.

Mechanized Presentations of Separation Logic

Gordon [1989] presents the first mechanization of Hoare logic in higher-order logic, using the HOL tool. Gordon's pioneering work was followed by numerous formalizations of Hoare logic, targeting various programming languages. Mechanizations of Separation Logic appeared later. Here again, we restrict our discussion to the verification of sequential programs. [START_REF] Yu | Building Certified Libraries for PCC: Dynamic Storage Allocation[END_REF][START_REF] Yu | Building Certified Libraries for PCC: Dynamic Storage Allocation[END_REF] present the CAP framework, implemented in Coq. It supports reasoning about low-level code using Separation Logic-style rules, and is applied to the verification of a dynamic storage allocation library. [START_REF] Ni | Certified Assembly Programming with Embedded Code Pointers[END_REF] present the XCAP framework, already mentioned in the previous section, to reason about embedded code pointers. XCAP was also applied to reasoning about x86 context management code [START_REF] Ni | Using XCAP to Certify Realistic Systems Code: Machine Context Management[END_REF]]. [START_REF] Feng | Modular Verification of Assembly Code with Stack-Based Control Abstractions[END_REF] present the SCAP framework, for reasoning about stack-based control abstractions, including exceptions and setjmp/longjmp operations. SCAP is also applied to the verification of Baker's incremental copying garbage collector [START_REF] Mccreight | A General Framework for Certifying Garbage Collectors and Their Mutators[END_REF]]. [START_REF] Feng | An Open Framework for Foundational Proof-Carrying Code[END_REF] present the OCAP framework that generalizes XCAP for supporting interoperability of different verification systems, including SCAP. [START_REF] Cai | Certified Self-Modifying Code[END_REF] present the GCAP framework for reasoning about self-modifying code, and apply Separation Logic to support local reasoning on both program code and regular data structures. [START_REF] Feng | Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads[END_REF] presents the first verified implementation of a preemptive thread runtime that exploits hardware interrupts; this runtime is linked to verified context switch primitives, using the OCAP and the SCAP frameworks. [START_REF] Wang | A Simple Model for Certifying Assembly Programs with First-Class Function Pointers[END_REF] present ISCAP, a step-indexed, direct-style operational semantics with support for first-class pointers. [START_REF] Weber | Towards Mechanized Program Verification with Separation Logic[END_REF] formalizes in Isabelle/HOL a first-order Separation Logic for a simple while language. This work includes a soundness proof for the frame rule, and the verification of the classic in-place list reversal example.

Preoteasa [2006] formalize in PVS a first-order Separation Logic, with the additional feature that it supports recursive procedures. This work includes the verification of a collection of recursive procedures for computing the parse tree associated with an arithmetic expression. [START_REF] Marti | Formal Verification of the Heap Manager of an Operating System Using Separation Logic[END_REF] formalize in Coq a Separation Logic library, and used it for the verification of the heap manager of an operating system. [START_REF] Tuch | Types, Bytes, and Separation Logic[END_REF] present a shallow embedding of Separation Logic in Isabelle/HOL, for a subset of the C language, with support for interpreting values at the byte level when required. Their framework is applied to the verification of the memory allocator of a microkernel. Its logic was later extended to support predicates for mapping virtual to physical addresses, and thereby reason about the effects of virtual memory [START_REF] Kolanski | Types, Maps and Separation Logic[END_REF]. [START_REF] Klein | Mechanised Separation Algebra[END_REF] present a re-usable library for Separation Algebras, including support for automation. [START_REF] Appel ; Dockins | Program logics for certified compilers[END_REF] formalize in Coq a Separation logic for Cminor. This work led to the VST tool, which supports the verification of concurrent C code [START_REF] Appel | Verified Software Toolchain[END_REF][START_REF] Appel | Program Logics for Certified Compilers[END_REF]Cao et al. 2018a]. VST leverages step-indexed definitions and features a later modality [START_REF] Dockins | Multimodal Separation Logic for Reasoning About Operational Semantics[END_REF][START_REF] Hobor | Oracle Semantics for Concurrent Separation Logic[END_REF][START_REF] Hobor | A Theory of Indirection via Approximation[END_REF]. [START_REF] Myreen | Hoare Logic for Realistically Modelled Machine Code[END_REF] formalize Separation Logic in HOL4. This work eventually lead to the CakeML compiler, described further on. [START_REF] Varming | Higher-Order Separation Logic in Isabelle/HOLCF[END_REF] demonstrate the possibility to formalize higher-order Separation Logic as a shallow embedding in Isabelle/HOLCF. Nanevski et al. [2008b] and [START_REF] Chlipala | Effective Interactive Proofs for Higher-Order Imperative Programs[END_REF] present the Ynot tool, which consists of an axiomatic embedding in Coq of Hoare Type Theory (HTT) [START_REF] Nanevski | Polymorphism and Separation in Hoare Type Theory[END_REF][Nanevski et al. , 2008a]]. HTT is a presentation of higher-order Separation Logic with higher-order stores in the form of a type system for a dependently typed functional language. In Ynot, like in HTT, a Coq term t admits the Coq type "ST H Q" to express the specification {H } t {Q }. In Ynot, programs are shallowly embedded in Coq: they are expressed using Coq primitive constructs and axiomatized monadic constructs for effects. The frame rule takes the form of an identity coercion of type

ST H Q → ST (H ⋆ H ′ ) (λv. Q v ⋆ H ′ ).
For specifications involving auxiliary variables, Ynot supports ghost arguments, which appear like normal function arguments except that they are erased at runtime. [START_REF] Charguéraud | Characteristic Formulae for the Verification of Imperative Programs[END_REF] presents the CFML tool, which supports the verification of OCaml programs. CFML does not state reasoning rules directly in Coq; instead, a program is verified by means of its characteristic formula, which corresponds to a form of strongest postcondition. These characteristic formulae are generated as Coq axioms by an external tool that parses input programs in OCaml syntax. CFML was extended to support asymptotic cost analysis [START_REF] Charguéraud | Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation[END_REF][START_REF] Charguéraud | Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits[END_REF]. CFML initially hard-wired fully-affine triples, featuring unrestricted discard rules, and later integrated the customizable predicate haffine ( §8) [START_REF] Guéneau | Formal Proof and Analysis of an Incremental Cycle Detection Algorithm[END_REF]. [START_REF] Tuerk | A separation logic framework for HOL[END_REF] presents in HOL4 the Holfoot tool, formalizing in particular the rules of Abstract Separation Logic [START_REF] Calcagno | Local Action and Abstract Separation Logic[END_REF].

Chlipala [2011,2013] presents in Coq the Bedrock framework, for the verification of programs written at the assembly level. Bedrock has been, for example, put to practice to verify a cooperative threading library and an implementation of a domain-specific language for XML processing. These software components were interfaced with hardware components of mobile robots [START_REF] Chlipala | From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification[END_REF]]. [START_REF] Bengtson | Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq[END_REF] present a shallow embedding of higher-order Separation Logic in Coq, demonstrating the use of nested triples for reasoning about object-oriented code. Following up on that work, [START_REF] Bengtson | Charge![END_REF] developed in Coq the Charge! tool, which handles a subset of Java. [START_REF] Jensen | High-Level Separation Logic for Low-Level Code[END_REF] give a modern presentation of a Separation Logic for low-level code, exploiting in particular the (higher-order) frame connective [START_REF] Birkedal | Semantics of separation-logic typing and higher-order frame rules[END_REF][START_REF] Birkedal | Relational Parametricity and Separation Logic[END_REF][START_REF] Neelakantan | Verifying Higher-Order Imperative Programs with Higher-Order Separation Logic[END_REF]. Building on that work, [START_REF] Kennedy | Coq: The World's Best Macro Assembler?[END_REF] show how to write assembly syntax and generate x86 machine code inside Coq.

The CakeML verified compiler [START_REF] Kumar | CakeML: A Verified Implementation of ML[END_REF], implemented in HOL, takes SML-like programs as input and produces machine code as output. It exploits Separation Logic to prove the garbage collector [START_REF] Sandberg Ericsson | A Verified Generational Garbage Collector for CakeML[END_REF]. It also exploits Separation Logic to set up a CFML-style characteristic formula generator, extended with support for catchable exceptions and I/O [START_REF] Guéneau | Verified Characteristic Formulae for CakeML[END_REF]. The characteristic formulae are used to verify the standard library for CakeML.

The Iris framework [START_REF] Jung | RustBelt: Securing the Foundations of the Rust Programming Language[END_REF][START_REF] Jung | Higher-Order Ghost State[END_REF][START_REF] Jung | Iris from the ground up: A modular foundation for higher-order concurrent separation logic[END_REF][START_REF] Jung | Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning[END_REF][START_REF] Krebbers | The Essence of Higher-Order Concurrent Separation Logic[END_REF], implemented in Coq, supports higher-order concurrent Separation Logic. Like VST, Iris features a later modality and step-indexed definitions. Iris exploits weakest-precondition style reasoning rules ( §9) and function specifications are stated as in Lemma 9.6, although using syntactic sugar to make specifications resemble conventional triples. Iris is defined as a fully-affine logic, with an affine entailment. [START_REF] Tassarotti | A Higher-Order Logic for Concurrent Termination-Preserving Refinement[END_REF] present an extension of Iris with linear heap predicates.

The Mosel framework [START_REF] Krebbers | MoSeL: A General, Extensible Modal Framework for Interactive Proofs in Separation Logic[END_REF] generalizes Iris' tooling to a large class of separation logics, targeting both affine and linear separation logics, and combinations thereof. On top of Iris, [START_REF] Bizjak | Iron: Managing Obligations in Higher-Order Concurrent Separation Logic[END_REF] present the encoding of two logics that enable tracking of linear resources that are transferable among dynamically allocated threads. The first one, called Iron, leverages fractional permissions to encode trackable resources, and allow, e.g., reasoning about deallocation of shared resources. The second one, called Iron++, hides away the use of fractions, and recovers essentially a linear Separation Logic with support for trackable invariants. [START_REF] Bannister | Backwards and Forwards with Separation Logic[END_REF] discuss techniques for forward and backward reasoning in Separation Logic. Their work, presented in Isabelle/HOL, introduces the separating coimplication operator to improve automation. Separating coimplication is the dual of separating conjunction, just like septraction [START_REF] Vafeiadis | A Marriage of Rely/Guarantee and Separation Logic[END_REF] is the dual of separating implication. Separating coimplication forms a Galois connection with septraction, just like separating conjunction forms a Galois connection with separating implication. Lammich [2019a,b] present a refinement framework that leverages Separation Logic to refine from Isabelle/HOL definitions to verified code in LLVM intermediate representation. It is applied to the production of a number of algorithms, including an efficient KMP string search implementation.

Tutorials on Separation Logic

There exists a number of course notes on Separation Logic. Many of them follow the presentation from Reynolds' article [2002] and course notes [2006]. These course notes consider languages with mutable variables, whose treatment adds complexity to the reasoning rules. The Separation Logic is presented as a first-order logic on its own, without attempt to relate it in a way or another to the higher-order logic of a proof assistant. The soundness of the logic is generally only skimmed over, with a few lines explaining how to justify the frame rule.

A few courses present Separation Logic in relation with its application in mechanized proofs. Appel's book Program Logics For Certified Compilers [2014] presents a formalization of a Separation Logic targeting the C semantics from CompCert [START_REF] Leroy | Formal Verification of a Realistic Compiler[END_REF]]. More recently, [START_REF] Appel | Verifiable C[END_REF] published a volume part of the Software Foundations series, entitled Verifiable C. This volume is a tutorial for VST [Cao et al. 2018a], a tool that supports reasoning about actual C code. As of 2020, the tutorial covers the verification of data structures, including linked lists, stacks, hashtables, as well as functions manipulating strings.

The presence of mutable variables, in addition to other specificities of the C memory model, makes the presentation unnecessarily complex for a first exposure to Separation Logic and to its soundness proof. The author is aware of two other mechanized Separation Logic tutorials that target a λ-calculus based language, with immutable variables and return values for terms.

The Iris tutorial by [START_REF] Birkedal | Lecture Notes on Iris: Higher-Order Concurrent Separation Logic[END_REF] presents the core ideas of Iris' concurrent Separation Logic [START_REF] Krebbers | The Essence of Higher-Order Concurrent Separation Logic[END_REF]. Chapters 3 and 4 introduce heap predicates and Separation Logic for sequential programs. Unlike in Iris' Coq formalization, which leverages a shallow embedding of Separation Logic, the tutorial presents the heap predicate in deep embedding style, via a set of typing rules for heap predicates. The realization of these predicates is not explained, and the tutorial does not discuss how the reasoning rules are proved sound with respect to the small-step semantics of the language. The logic presented targets partial correctness, not total correctness, and only the case of an affine logic is covered.

Chlipala's course notes [Chlipala 2018a] feature a chapter on Separation Logic, accompanied with a corresponding Coq formalization meant to be followed by students [Chlipala 2018b]. The material includes a proof of soundness, as well as the verification of a few example programs. Chlipala's chapter focuses on the core of Separation Logic-it does not cover any of the enhancements listed in the introduction. The programming language is described in mixed-embedding style: the syntax includes a constructor Bind, which represents bindings using Coq functions, in higher-order abstract syntax style. The rest of the syntax consists of operations for allocation and deallocation, for reading and writing integer values into the heap, plus the constructors Return, Loop, and Fail. These constructs are dependently-typed: a term that produces a value of type α admits the type cmd α. Altogether, this design allows for a concise formalization of the source language, yet, we believe, at the price of an increased cost of entry for the reader unfamiliar with the techniques involved. The core heap predicates are formalized like in Ynot [START_REF] Chlipala | Effective Interactive Proofs for Higher-Order Imperative Programs[END_REF]]. Triples are defined in deep embedding style, via an inductive definition whose constructors correspond to the reasoning rules. This deep embedding presentation requires "not-entirely-obvious" inversion lemmas, which are not needed in our approach. The soundness proof establishes a partial correctness result expressed via preservation and progress lemmas. Chlipala's approach appears well suited for reasoning about an operating system kernel that should never terminate, or reasoning about concurrent code. However, for reasoning about sequential executions of functions that do terminate, our total correctness proof carried out with respect to a big-step semantics yields a stronger result, via a simpler proof.

A STATISTICS ON THE MINIMAL SOUNDNESS PROOF FOR SEPARATION LOGIC

B PREDICATE EXTENSIONALITY

In proof assistants such as HOL or Isabelle/HOL, extensionality is built-in. In Coq, it needs to be either axiomatized, or derived from two more fundamental extensionality axioms: extensionality for functions and extensionality for propositions. These standard axioms are formally stated as follows.

predicate-extensionality: ∀A. ∀(P P ′ : A → Prop). (P x ⇔ P ′ x ) ⇒ (P = P ′ ) functional-extensionality:

∀A B. ∀( f f ′ : A → B). ( f x = f ′ x ) ⇒ ( f = f ′ ) propositional-extensionality: ∀(P P ′ : Prop). (P ⇔ P ′ ) ⇒ (P = P ′ )
In summary, one may take functional-extensionality and propositional-extensionality as axioms in Coq, then from these two derive predicate-extensionality and, as a corollary, the antisymmetry rule for heap entailment (himpl-antisym).

C EXAMPLE PROOFS OF REASONING RULES C.1 Proof of A Structural Rule

To illustrate the kind of reasoning involved in the proof of structural rules, consider the proof of the combined consequence-frame rule.

Lemma C.1 (Combined conseqence-frame rule).

H ⊢ H 1 ⋆ H 2 {H 1 } t {Q 1 } Q 1 . ⋆ H 2 . ⊢ Q {H } t {Q } consequence-frame
Proof. The consequence rule is straightforward to establish for Hoare triples, based on the definition of entailment (Definitions 3.7 and 3.14) and of Hoare triples (Definition 5.1), in which the precondition appears as hypothesis and the postcondition as conclusion of a logical implication.

Let us prove the consequence-frame rule with respect to the interpretation of Separation Logic triples given in Definition 5.2.

⋆ H ′ ⊢ H ⋆ (H 2 ⋆ H ′ ) and Q . ⋆ (H 2 ⋆ H ′ ) . ⊢ Q . ⋆ H ′ .
To prove the first entailment, first exploit rule star-assoc to rewrite it as H ⋆H ′ ⊢ (H ⋆H 2 ) ⋆H ′ , then observe that the resulting entailment follows from the premise H ⊢ H 1 ⋆ H 2 by rule starmonotone-r. To prove the second entailment, let us begin by revealing the definition of the entailment for postconditions (recall Definition 3.14). The second entailment is equivalent to

(Q v) ⋆ (H 2 ⋆ H ′ ) ⊢ (Q v) ⋆ H ′ . It follows from the premise Q 1 . ⋆ H 2 . ⊢ Q, which implies (Q 1 v) ⋆ H 2 ⊢ (Q v)
, by exploiting the rules star-assoc and star-monotone-r just like for the first entailment. □

C.2 Proof of a Reasoning Rule for Terms

To illustrate the kind of reasoning involved in the proof of reasoning rules for terms, consider the case of sequences. The proof is two-step: first establish a Hoare logic reasoning rule for sequences, then derive its Separation Logic counterpart.

Lemma C.2 (Reasoning rule for seqences in Hoare Logic).

HOARE {H } t 1 {λv. H ′ } HOARE {H ′ } t 2 {Q } HOARE {H } (t 1 ; t 2 ) {Q } hoare-seq
Proof. The evaluation rule for sequence is a simplified version of the evaluation rule for letbindings, stated as shown below.

t 1 /s ⇓ v 1 /s ′ t 2 /s ′ ⇓ v/s ′′ (t 1 ; t 2 )/s ⇓ v/s ′′ eval-seq
Recall from Definition 5.1 the interpretation of Hoare triples. Consider a state s satisfying the precondition H , that is, such that H s holds. The goal is to find v and s ′ such that (t 1 ; t 2 )/s ⇓ v/s ′ and Q v s ′ hold.

By the first premise HOARE {H } t 1 {λv. H ′ } applied that state s, there exists v 1 and s ′ 1 such that t 1 /s ⇓ v 1 /s ′ 1 and (λv. H ′ ) v 1 s ′ 1 hold. The latter simplifies to H ′ s ′ 1 . By the second premise {H ′ } t 2 {Q } applied to the state s ′ 1 , which satisfies the precondition H ′ , there exists v and s ′ such that t 2 /s ⇓ v/s ′ and Q v s ′ hold. The latter corresponds to one half of the conclusion.

Applying the evaluation rule for sequence eval-seq to the judgments t 1 /s ⇓ v 1 /s • Introducing and eliminating v simplifies the proof obligation into an instance of rule set: {p → n} (set p (n + 1)) {λ_. p → (n + 1)}.

□ E BENEFITS OF THE FRAME RULE IN THE PROOF OF A RECURSIVE FUNCTION

The frame rule allows for simpler proofs than what could be achieved without it. To substantiate this claim, let us present the proof of the copy function in Separation Logic, then discuss how it would be more complicated without the frame rule.

let rec mcopy p = if p == null then null else { head = p.head; tail = mcopy p.tail }

Proof. The proof of the specification stated in Example 2.12 is carried out by induction on the length of the list L. The induction hypothesis allows in particular to assume the specification to hold for the recursive call.

At the entry of the body of the function, the state corresponds to the precondition, that is, to Mlist L p. To reason by case analysis on whether p is null, we exploit Definition 2.9.

• Case p = null. In this case, L = nil and the function returns the value null. This value is named p ′ in the postcondition. The new piece of postcondition to establish is Mlist L p ′ . By Definition 2.8, because L = nil, the predicate Mlist L p ′ is equivalent to p ′ = null. Hence, the postcondition is satisfied. • Case p null. In this case, L decomposes as x :: L ′ , and the current state is described by the heap predicate (p.head → x ) ⋆ (p.tail → q) ⋆ (Mlist L ′ q). The operations performed by the code are verified as follows.

-The read operation p.head returns the value x, and p.tail returns the address q.

-The recursive call mcopy q creates a copy of the list represented by L ′ . By induction hypothesis applied to L ′ , this recursive call can be assumed to satisfy the triple:

{Mlist L ′ q} (mcopy q) {λr ′ . ∃ ∃q ′ . [r ′ = q ′ ] ⋆ (Mlist L ′ q) ⋆ (Mlist L ′ q ′ )}.

-Applying the frame rule to that triple and to (p.head → x ) ⋆ (p.tail → q) yields the triple:

{(p.head → x ) ⋆ (p.tail → q) ⋆ (Mlist L ′ q)} (mcopy q) {λr ′ . ∃ ∃q ′ . [r ′ = q ′ ] ⋆ (p.head → x ) ⋆ (p.tail → q) ⋆ (Mlist L ′ q) ⋆ (Mlist L ′ q ′ )}

which enables reasoning about the recursive call in the current state. -Let q ′ denote the result of the recursive call, and let p ′ denote the result of the record allocation operation{ head = p.head; tail = q' } . This record allocation produces a heap described by (q.head → x ) ⋆ (q.tail → q ′ ). -Thus, the final state is described by: (p.head → x ) ⋆ (p.tail → q) ⋆ (Mlist L ′ q) ⋆ (p ′ .head → x ) ⋆ (p ′ .tail → q ′ ) ⋆ (Mlist L ′ q ′ ) which may be folded to (Mlist L p) ⋆ (Mlist L p ′ ), matching the claimed postcondition. □ Intuitively, in the above reasoning, the frame rule is invoked at each recursive call on the head cell of the input list. One is therefore able to reason about a recursive call to mcopy by assuming that it makes a copy of a sublist, independently of all the cells that have already been traversed by the outer recursive calls to mcopy.

Without the frame rule, one would have to describe the full list at an arbitrary point during the recursion. Doing so requires describing the list segment made of cells ranging from the head of the initial list up to the pointer on which the current recursive call is made. Stating an invariant involving list segments is doable yet involves more complex definitions and assertions.

More generally, for a program manipulating tree-shaped data structures, the frame rule saves the need to describe a tree with a subtree carved out of it. The ability to invoke the frame rule in proofs carried out by induction allows to reason locally about the work performed by the recursive call, without having to explicitly describe the whole context in which this recursive call is taking place, thereby saving a significant amount of proof effort.

F REASONING ABOUT HIGHER-ORDER FUNCTIONS

Example F.1 (Reynold's CPS-append challenge). Consider the (nontrivial) function shown below. It takes as arguments two mutable lists, and returns an address describing the head of a list whose cells correspond to the concatenation of the two input lists. The function is implemented by means of a recursive function that expects a continuation, named k in the code, to be invoked on the output list. Each recursive call is made with a fresh continuation, responsible for updating the tail pointer of the list cell at hand before invoking the current continuation.

• For each magic wand of the form Q . -⋆ Q ′ , if a predicate of the form Q v also occurs on the left-hand side, then specialize this magic wand to

Q v . -⋆ Q ′ v, cancel out Q v, leaving Q ′ v.
(3) On the right-hand side:

• If a pure fact [P] occurs on the right-hand side, remove it and generate a subgoal asserting the proposition P. • It a quantifier ∃ ∃x . H occurs on the right-hand side, instantiate x with a value v, leaving [v/x] H . The value v may be provided by the user (via arguments passed to the tactic xsimpl), or it may be realized as a Coq unification variable (a.k.a. evar). ⊢ Q ′ , replace it with the proof obligation ∀x . (Q x ⊢ Q ′ x ) and continue simplifying the inner entailment.

Several papers investigate specifically the automation of entailment simplification or resolution, e.g., [START_REF] Hóu | Automated Theorem Proving for Assertions in Separation Logic with All Connectives[END_REF][START_REF] Hóu | Proof Tactics for Assertions in Separation Logic[END_REF][START_REF] Lee | A Proof System for Separation Logic with Magic Wand[END_REF].

Fig. 2 .

 2 Fig. 2. Evaluation rules, in big-step style

Definition 5 .

 5 2 (Total correctness Separation Logic triple).

  let r = ref p and s = ref 0 in while !r != null do (incr s; r := !r.tail) done The triple {Mlist L p ⋆ r → p ⋆ s → 0} (while ... done) {λ_. Mlist L p ⋆ r → null ⋆ s → |L|} specifies the behavior of the loop. Its proof is conducted by induction on the statement: ∀Lnp. {Mlist L p ⋆ r → p ⋆ s → n} (while ... done) {λ_. Mlist L p ⋆ r → null ⋆ s → n + |L|}.

  ⋆ H ′′ }, as required. □ D VERIFICATION OF THE INCREMENT FUNCTION To illustrate the use of the reasoning rules, let us present the proof of the increment function. Consider the following implementation. incr ≡ μ_ .λp. let n = get p in let m = (+) n 1 in set p m Example D.1 (Verification of the increment function). The following statement holds. ∀p n. {p → n} (incr p) {λ_. p → (n + 1)} Proof. Consider particular values of p and n.• Applying rule app leaves:{p → n} (let n = get p in let m = (+) n 1 in set p m) {λ_. p → (n + 1)}.• Applying rule let withQ ′ instantiated as λr . [r = n] ⋆ (p → n) leaves two subgoals. The first one is: {p → n} (get p) {λr . [r = n] ⋆ (p → n)}.It is an instance of the rule get. The second subgoal is:∀v. {[v = n] ⋆ p → n} (let m = (+) v 1 in set p m) {λ_. p → (n + 1)}.• Introducing v, applying the rule prop to extract[v = n] from the precondition, then substituting n for v turns the proof obligation into:{p → n} (let m = (+) n 1 in set p m) {λ_. p → (n + 1)}.• Applying again the rule let, this time with Q ′ instantiated as λr . [r = n + 1] ⋆ (p → n). leaves two subgoals. The first one is: {p → n} ((+) n 1) {λr . [r = n +1] ⋆ (p → n)}. Applying the frame rule with H ′ instantiated as p → n yields an instance of the rule add. The second subgoal is: ∀v. {[v = n + 1] ⋆ p → n} (set p v) {λ_. p → (n + 1)}.

  t 1 then (t 2 ; while t 1 do t 2 ) else tt) {Q } {H } (while t 1 do t 2 ) {Q }

	Separation Logic for Sequential Programs (Functional Pearl)	116:17

Proc. ACM Program. Lang., Vol. 4, No. ICFP, Article 116. Publication date: August 2020.

  Lemma 8.3 (Sufficient conditions for affinity of a heap predicate).

	affine-empty	affine-pure	affine-star affine H 1	affine H 2
	affine [ ]	affine [P]	affine (H 1 ⋆ H 2 )
	affine-exists
	∀x . affine H

affine (∃ ∃x . H ) affine-forall ∀x . affine H the type of x is inhabited affine (∀ ∀x . H ) affine-star-pure P ⇒ affine H affine ([P] ⋆ H )

  The conclusion {H } t {Q } is equivalent to ∀H ′ . HOARE {H ⋆ H ′ } t {Q . ⋆ H ′ }. Consider a particular heap predicate H ′ . Invoking the premise {H 1 } t {Q 1 } on the predicate H 2 ⋆H ′ yields HOARE {H ⋆(H 2 ⋆ H ′ )} t {Q . ⋆ (H 2 ⋆ H ′ )}. By the consequence rule of Hoare logic, to derive HOARE {H ⋆ H ′ } t {Q . ⋆ H ′ }, it suffices to establish the entailments H

  ′ 1 and t 2 /s ⇓ v/s ′ yields (t 1 ; t 2 )/s ⇓ v/s ′ , which corresponds to the second half of the conclusion. □ Lemma C.3 (Reasoning rule for seqences in Separation Logic). {H } t 1 {λv. H ′ } {H ′ } t 2 {Q } {H } (t 1 ; t 2 ) {Q } seq Proof. Recall from Definition 5.2 the interpretation of Separation Logic triples: {H } (t 1 ; t 2 ) {Q } is equivalent to ∀H ′′ . HOARE {H ⋆ H ′′ } (t 1 ; t 2 ) {Q . ⋆ H ′′ }. Consider a particular heap predicate H ′′ . By the first premise {H } t 1 {λv. H ′ } applied to that H ′′ , one derives HOARE {H ⋆H ′′ } t 1 {(λv. H ′ ) . ⋆ H ′′ }. In that judgment, the postcondition (λv. H ′ ) . ⋆ H ′′ simplifies to λv. (H ′ ⋆ H ′′ ). By the second premise {H ′ } t 2 {Q } applied to the same H ′′ , one derives HOARE {H ′ ⋆H ′′ } t 2 {Q . ⋆H ′′ }. Applying the Hoare logic reasoning rule for sequences (hoare-seq from Lemma C.2) to the two judgments HOARE {H ⋆ H ′′ } t 1 {λv. (H ′ ⋆ H ′′ )} and HOARE {H ′ ⋆ H ′′ } t 2 {Q . ⋆ H ′′ } yields HOARE {H ⋆ H ′′ } (t 1 ; t 2 ) {Q .

  • Remove expressions of the form H -⋆H or Q . -⋆ Q, which are entailed by [ ].(4) On both sides:• If a predicate H occurs on the both sides, and H is not ⊤ ⊤, then remove H from both sides.• If the entailment is of the formH 0 ⊢ (H 1 -⋆H 2 ), then replace it with (H 1 ⋆ H 0 ) ⊢ H 2 . Likewise, replace H 0 ⊢ (Q 1 . -⋆ Q 2 ) with (Q 1 . ⋆ H 0 ) . ⊢ 2 . • If the entailment is of the form [ ] ⊢ [ ],then the entailment is true. • It the entailment is of the form H ⊢ ⊤ ⊤, replace it with the proof obligation affine H . • If the entailment is of the form H ⊢ (∀ ∀x . H ′ ), replace it with the proof obligation ∀x . (H ⊢ H ′ ) and continue simplifying the inner entailment. • If the goal is of the form Q .

Proc. ACM Program. Lang., Vol. 4, No. ICFP, Article 116. Publication date: August 2020.

ACKNOWLEDGMENTS

I wish to thank François Pottier and Armaël Guéneau, with whom I have worked on extensions of Separation Logic. I am grateful to Jacques-Henri Jourdan, who explained to me a number of techniques used in Iris. I also wish to thank the anonymous reviewers for their useful suggestions, as well as Andrew Appel, Lars Birkedal, Adam Chlipala, Magnus Myreen, Gerwin Klein, Peter Lammich, and Zhong Shao, who helped complete the related work section. This research was partly supported by the French National Research Organization (project VOCAL ANR-15-CE25-008).

Definition 8.8 (Refined definition of triples for Separation Logic).

Note that, with the fully-linear instantiation described in Example 8.7, the predicate ⊤ ⊤ is equivalent to the empty heap predicate, therefore Definition 8.8 is strictly more general than Definition 5.2. Lemma 8.9 (Reasoning rules for refined Separation Logic triples). All the previouslymentioned reasoning rules, in particular the structural rules (Lemma 5.4) and the reasoning rules for terms (Lemma 5.6), remain correct with respect to the refined definition of triples (Definition 8.8).

The discard rules, which enable discarding affine heap predicates, may be stated in a number of ways. The three variants that are most useful in practice are shown below. These three variants have expressive power with respect to discarding heap predicates.

The rule discard-pre allows discarding a user-specified predicate H ′ from the precondition, provided that H ′ is affine. Without this rule, the user would have to carry this heap predicate H ′ through the proof until it appears in a postcondition.

The rule atop-post allows extending the postcondition with ⊤ ⊤, allowing a subsequent proof step to yield an entailment relation of the form Q 1 .

⊢ (Q . ⋆ ⊤ ⊤), allowing to discard unwanted pieces from Q 1 . This rule is useful in "manual" proofs, i.e., proofs carried out with limited tactic support.

The rule ramified-frame-atop extends the ramified frame rule so that its entailment integrates the predicate ⊤ ⊤, allowing to discard unwanted pieces from either H or Q 1 . This rule is a key building block for a practical tool that implements a partially-affine Separation Logic. Lemma 8.10 (Discard rules). discard-pre

Semantic Weakest Precondition

The notion of weakest precondition has been used pervasively in the development of practical tools based on Hoare logic. Recent work has shown that this notion also helps streamlining the set up of practical tools based on Separation Logic. The semantic weakest precondition of a term t with respect to a postcondition Q denotes a heap predicate, written wp t Q, which corresponds to the weakest precondition H satisfying the triple {H } t {Q }. The notion of "weakest" is to be understood with respect to the entailment relation, which induces an order relation on the set of heap predicates (recall Lemma 3.8). The definition of the predicate wp can be formalized in at least five different ways. The corresponding definitions are shown below and commented next. Definition 9.1 (Semantic weakest precondition). The predicate wp is equivalently characterized by:

(1)

The first characterization asserts that wp t Q is the weakest precondition: it is a valid precondition for a triple for the term t with the postcondition Q. Moreover, any other valid precondition H for a let cps_append p1 p2 = let rec aux p k = if p == null then k p2 else aux p.tail p2 (fun r => (p.tail <-r); k p) in aux p1 (fun r => r)

This function admits the following Separation Logic specification, which describes the two disjoint input lists represented by L 1 and L 2 , respectively, and the result list represented by

The crux of the proof consists of providing the appropriate specification for the internal recusive function aux. This specification reads as follows. Assume the continuation k to admit the postcondition Q when invoked on a list p 3 describing a list of the form L + + L 2 , and with an auxiliary heap described by H . Then, the call aux p 1 k also admits the postcondition Q (indeed, the ultimate action performed by aux is to invoke its continuation k) under the precondition including (Mlist L p), which corresponds to a sublist of (Mlist L 1 p 1 ), including (Mlist L 2 p 2 ), which is exploited only in the base case where p becomes null, and including H .

In this statement, H describes, in an abstract way, the cells from list p 1 that have already passed by. The introduction of such an abstract heap predicate H is a common pattern for CPS-style functions.

The verification of the function cps_append was first conducted in XCAP [START_REF] Ni | Certified Assembly Programming with Embedded Code Pointers[END_REF]. In this pioneering work, the function is programmed in a assembly-level language with embedded code pointers, and the proof involving several hundreds of lines of Coq script. The verification of cps_append was later carried out in CFML [START_REF] Charguéraud | Characteristic Formulae for the Verification of Imperative Programs[END_REF]]. In that framework, the function is programmed in 4 lines of OCaml and verified using 9 lines of Coq proofs.

G ALTERNATIVE STRUCTURAL RULES

Lemma 5.4 presents 4 core structural reasoning rules: conseqence, frame, prop and exists.

The rule prop for extracting pure facts may in fact be seen as a particular instance of the rule exists for extracting existential quantifiers. Indeed, as pointed out in Remark 3.4, the heap predicate [P] is equal to ∃ ∃(p : P ). [ ]. Besides, the quantification "∀(p : P ). ..." is equivalent to the implication "P ⇒ ...".

The rule exists is very useful in practice, although its statement does not appear in the original papers on Separation Logic. These papers instead formulated a rule featuring an existential quantifier both in the precondition and the postcondition. In a ML-style language, it would corresponds to the rule exists2 shown below. The rules exists and exists2 yield equivalent expressive power, that is, they may be derived from one another (in the presence of the rule conseqence, and exists-r and exists-l from Fig. 1). Compared with exists2, the statement of exists is more concise and better-suited for practical purpose.

The rule forall, stated below, is also useful in practice. This rule is derivable from the conseqence, and forall-l from Fig. 1. Lemma G.1 (Other structural rules).

H ARRAYS AND RECORDS

This section briefly summarizes the key ideas involved in the treatment of arrays and records. Details may be found in the accompanying Coq development.

Note that the presentation does not take into account the notion of "allocated blocks", and the usual restriction that the free operation can only be invoked on the head of an allocated block. We are currently working on a refinement of the definitions that would enforce this property.

H.1 Arrays

The programming language is assumed to include two additional primitive operations: alloc n for allocating n consecutive cells, and dealloc n p for deallocating n consecutive cell starting from address p. It is possible to refine the Separation Logic to ensure that deallocation operations are only invoked on the head of allocated blocks-details are beyond the scope of the present paper.

The allocated cells are assigned as contents a special uninitialized value, written ⊥. The semantics of read operations may be adapted to prevent read operations in uninitialized cells, by adding a premise of the form v ⊥ to the specification of get.

The i-th cell of an array allocated at address p corresponds to the cell at address p + i.

Definition H.1 (Representation of consecutive cells). The heap predicate cells L p describes consecutive cells allocated in the range [p, p + |L|), whose contents are the items from the list L.

Lemma H.2 (Specification of array operations).

For functions that process an array by making recursive calls to increasingly-smaller segments of the array, the following range-split lemma allows splitting the segment at hand and applying the frame rule to the segment that is not involved in the recursive call. One thereby gets for free the fact that cells in that segment are unmodified during the recursive call.

Lemma H.3 (Splitting a range of cells). (cells (L

Another useful result is the following focus lemma, which allows isolating the i-th cell out of a range of consecutive cells starting at address p and described by a list L, so as to perform operations on that cell in isolation from the rest of the range. Subsequently, the cell with its updated contents v may be merged back into the range. This logical operation involves cancelling a magic wand. Lemma H.4 (Focusing on a cell from a range). Assume 0 ≤ i < |L|. Definition H.6 (Representation of records). Consider for example the record {head = x; tail = q}, with the offsets head ≡ 0 and tail ≡ 1. This record may be represented in three different ways:

(1) as "cells (x :: q :: nil) p", just like an array of length 2, (2) as "(p.head → x ) ⋆ (p.tail → q)", with two separated fields, (3) as "record (head, x ) :: (tail, q) :: nil) p", where the heap predicate record K p describes a record at location p and whose field names and contents are described by the association list K.

To each of these three representations of records correspond different specifications for allocation, deallocation, read and write operations. The third representation is the one that scales better to large programs, because: (1) it groups the fields of a same record into a single predicate, thereby reducing the number of conjuncts, (2) it allows describing the ownership of an arbitrary subset of the fields, (3) it allows providing items in any order, and (4) with appropriate syntactic sugar it may be written in the form p → {head := x; tail := q}, which is easy to read.

I TREATMENT OF ASSERTIONS (DYNAMIC CHECKS)

The language construct "assert t" expresses a Boolean assertion. If the term t evaluates to the value true, the assertion produces unit. Otherwise, the term "assert t" gets stuck-the program halts on an error. The verification of a program should statically ensure that: (1) the body of every assertion evaluates to true, and (2) the program remains correct when assertions are disabled either via a compiler option such as -noassert in OCaml, or via the programming pattern "if debug then assert t", where debug denotes a compilation flag. The assert rule, shown below, satisfies these two properties. Lemma I.1 (Evaluation rules and reasoning rule for assertions).

eval-assert-enabled t/s ⇓ true/s ′ (assert t )/s ⇓ tt/s ′ eval-assert-disabled

The term "assert false" denotes inaccessible branches of the code. A valid triple for this term can only be derived from a false precondition: {[False]} (assert false) {Q }.

Remark I.3 (Assertions involving write operations). Interestingly, the reasoning rule assert is not limited to read-only terms. For example, consider the Union-Find data structure, which involves the operation find that performs path compression. The evaluation of an assertion of the form assert (find x = find y) may involve write operations. It nevertheless preserves all the invariants of the data structure. These invariants would be captured by the heap predicate H from rule assert.

J TREATMENT OF FUNCTIONS OF SEVERAL ARGUMENTS

Functions of several arguments may be represented as curried functions (fun x y => t), as tupled functions (fun (x,y) => t), or as native n-ary functions (like, e.g., in the C language),

The curried function µ f .λx 1 .λx 2 . t is represented as µ f .λx 1 .(µ_.λx 2 .t ). An application takes the form (v 0 v 1 v 2 ). The reasoning rule for such an application, app2, generalizes the rule app. A version of this rule may be stated for every arity. Alternatively, an arity-generic rule may be devised, although in practice it requires tactic support for synthesizing the lists of variables and arguments. Lemma J.1 (Reasoning rule for curried functions of arity 2).

A language featuring primitive n-ary functions more naturally admits arity-generic reasoning rules. In such a language, µ f .λx .t denotes a function f expecting a list x of arguments of the form "x 1 :: ... :: x n :: nil", and the n-ary application term v 0 v denotes the application of a value v 0 to a list of arguments v of the form "v 1 :: ... :: v n :: nil".

Lemma J.2 (Reasoning rule for primitive n-ary functions).

Remark: it is possible to set up coercions in Coq such that an application written in curried style v 0 v 1 ... v n gets interpreted as the n-ary application v 0 (v 1 :: ... :: v n :: nil).

K A TACTIC FOR SIMPLIFYING ENTAILMENTS

In practical proofs, entailment relations to be established typically involve dozens of tokens, e.g.:

Proving such entailment relations by manually invoking the appropriate reasoning rules involves an overwhelming amount of work. Thus, for practical program verification, automation is a must-have. Ideally, an automated procedure should not only be able to discharge true entailments, it should also be able to perform all the "obvious" simplifications, leaving what remains of the entailment for a manual processing step by the user. Nearly all practical verification framework come with some amount of tooling for simplifying entailments.

One may also wish that the simplification tactic systematically produces as output an entailment that is logically equivalent to its input. However, there are a number of simplifications that are technically not equivalence-preserving, yet nearly always desirable to perform. It seems to make sense to nevertheless apply these simplifications, taking into account that the user always has the ability to "lock" certain subexpressions for preventing simplifications involving them.

In what follows, we describe (in informal terms) a strategy for simplifying triples in a systematic and predictable manner. The corresponding tactic is named xsimpl in the Coq development. (It is entirely implemented in Ltac.) The tactic named xpull is a variant of xsimpl that is limited to performing simplifications only on the left-hand side.

Definition K.1 (Tactic for simplifying entailment). The tactic first attempts to perform simplifications in the left-hand side, then in the right-hand side, then it attempts to perform simplifications that involve both sides. It may iterate this process several times, as long as progress is made.

(1) On each of the two sides, independently:

• Remove empty heap predicates and normalize expressions with respect to associativity.

• Collapse occurrences of the predicate ⊤ ⊤, so that there is at most one occurrence at top-level on each side. • Bring all existential quantifiers and pure facts to the front of each side.

(2) On the left-hand side:

• Pull out pure facts and existential quantifiers out into the Coq context.

• For each magic wand of the form (H 1 ⋆ ...H n ) -⋆H ′ , if one of the H i also occurs on the left-hand side, cancel H i out as explained Lemma 7.3.