Preface: Introduction to the Course

Welcome

This electronic book is Volume 6 of the Software Foundations series, which presents the mathematical underpinnings of reliable software. In this volume, you will learn about the foundations of Separation Logic, a practical approach for the modular verification of imperative programs. In particular, this volume presents the building blocks for constructing a program verification tool. It does not, however, focus on reasoning about data structures and algorithms using Separation Logic. This aspect is covered to some extent by Volume 5 of Software Foundations, which presents Verifiable C, a program logic and proof system for C. For OCaml programs, this aspect will be covered in a yet-to-be-written volume presenting CFML, a tool that builds upon all the techniques presented in this volume. You are only assumed to understand the material in Software Foundations Volume 1 (Logical Foundations), and the two chapters on Hoare Logic (Hoare and Hoare2) from Software Foundations Volume 2 (PL Foundations). The reading of Volume 5 is not a prerequisite. The exposition here is intended for a broad range of readers, from advanced undergraduates to PhD students and researchers. A large fraction of the contents of this course is also written up in traditional LaTeX-style presentation, in the ICFP'20 article: Separation Logic for Sequential Programs, by Arthur Charguéraud. The long version of this paper is available from: http://www.chargueraud.org/research/2020/seq_seplogic/seq_seplogic.pdf. This paper includes, in particular, a 5-page historical survey of contributions to mechanized presentations of Separation Logic, featuring 100+ citations. For a broader survey of Separation Logic, we recommend Peter O'Hearn's 2019 survey, which is available from: https://dl.acm.org/doi/10.1145/3211968-- including the supplemental material linked near the bottom of that page.

Separation Logic

Separation Logic is a program logic: it enables one to establish that a program satisfies its specification. Specifications are expressed using triples of the form {H} t {Q}. Whereas in Hoare logic the precondition H and the postcondition Q describe the whole memory state, in Separation Logic, H and Q describe only a fragment of the memory state. This fragment includes the resources necessary to the execution of t. A key ingredient of Separation Logic is the frame rule, which enables modular proofs. It is stated as follows.

{ H } t { Q }
{ H \* H' } t { Q \* H' }

The above rule asserts that if a term t executes correctly with the resources H and produces Q, then the term t admits the same behavior in a larger memory state, described by the union of H with a disjoint component H', producing the postcondition Q extended with that same resource H' unmodified. The star symbol \* denotes the separating conjunction operator of Separation Logic. Separation Logic can be exploited in three kind of tools.

• Automated proofs: the user provides only the code, and the tool locates sources of potential bugs. A good automated tool provides feedback that, most of time, is relevant.
• Semi-automated proofs: the user provides not just the code, but also specifications and invariants. The tool then leverages automated solvers (e.g., SMT solvers) to discharge proof obligations.
• Interactive proofs: the user provides not just the code and its specifications, but also a detailed proof script justifying the correctness of the code. These proofs may be worked on interactively using a proof assistant such as Coq.

The present course focuses on the third approach, that is, the integration of Separation Logic in an interactive proof assistant. This approach has been successfully put to practice throughout the world, using various proof assistants (Coq, Isabelle/HOL, HOL), targeting different languages (Assembly, C, SML, OCaml, Rust...), and for verifying various kind of programs, ranging from low-level operating system kernels to high-level data structures and algorithms.

Separation Logic in a proof assistant

The benefits of exploiting Separation Logic in a proof assistant include at least four major points:

• higher-order logic provides virtually unlimited expressiveness that enables formulating arbitrarily complex specifications and invariants;
• a proof assistant provides a unified framework to prove both the implementation details of the code and the underlying mathematical results form, e.g., results from theory or graph theory;
• proof scripts may be easily maintained to reflect on a change to the source code;
• the fact that Separation Logic is formalized in the proof assistant provides high confidence in the correctness of the tool.

Pretty much all the tools that leverage Separation Logic in a proof assistant are constructed following the same schema:

• A formalization of the syntax and semantics of the source language. This is called a deep embedding of the programming language.
• A definition of Separation Logic predicates as predicates from higher-order logic. This is called a shallow embedding of the program logic.
• A definition of Separation Logic triples as a predicate, the statements of the reasoning rules as lemmas, and the proof of these reasoning rules with respect to the semantics.
• An infrastructure that consists of lemmas, tactics and notation, allowing for the verification of concrete programs to be carried out through relatively concise proof scripts.
• Applications of this infrastructure to the verification of concrete programs.

The purpose of this course is to explain how to set up such a construction. To that end, we consider in this course the simplest possible variant of Separation Logic, and apply it to a minimalistic imperative programming language. The language essentially consists of a lambda-calculus with references. This language admits a simple semantics and avoids in particular the need to distinguish between stack variables and heap- allocated variables. Advanced chapters from the course explains how to add support for loops, records, arrays, and n-ary functions.

Several Possible Depths of Reading

The material is organized in such a way that it can be easily adapted to the amount of time that the reader is ready to invest in the course. The course contains 13 chapters, not counting the Preface and Postface. These chapters are organized in 3 major parts, as pictured in the dependency diagram.

• The short curriculum includes only the 5 first chapters (ranging from chapter Basic to chapter Rules).
• The medium curriculum includes 3 additional chapters (ranging from chapter WPsem to chapter Wand).
• The full curriculum includes 5 more chapters (ranging from chapter Partial to chapter Rich).

In addition, each chapter is decomposed in three parts.

• The First Pass section presents the most important ideas only. The course in designed in such a way that it is possible to read only the First Pass section of every chapter. The reader may be interested in going through all these sections to get the big picture, before revisiting each chapter in more details.
• The More Details section presents additional material explaining in more depth the meaning and the consequences of the key results. This section also contains descriptions of the most important proofs. By default, readers would eventually read all this material.
• The Optional Material section typically contains the remaining proofs, as well as discussions of alternative definitions. The Optional Material sections are all independent from each other. They would typically be of interest to readers who want to understand every detail, readers who are seeking for a deep understanding of a particular notion, and readers who are looking for answers to specific question.

List of Chapters

The first two chapters, namely chapters Basic and Repr give a primer on how to prove imperative programs in Separation Logic, thus focusing on the end user's perspective. All the other chapters focus on the implementor's perspective, explaining how Separation Logic is defined and how a practical verification tool can be constructed. The list of chapters appears below. The numbering corresponds to teaching units: if the chapters were taught as part of a University course, one could presumably aim to cover one teaching unit per week.

• (1) Basic: introduction to the core features of Separation Logic, illustrated using short programs manipulating references.
• (1) Repr: introduction to representation predicates in Separation Logic, in particular for describing mutable lists and trees.
• (2) Hprop: definition of the core operators of Separation Logic, of Hoare triples, and of Separation Logic triples.
• (2) Himpl: definition of the entailment relation, statement and proofs of its fundamental properties, and description of the simplification tactic for entailment.
• (3) Rules: statement and proofs of the reasoning rules of Separation Logic, and example proofs of programs using these rules.
• (4) WPsem: definition of the semantic notion of weakest precondition, and statement of rules in weakest-precondition style.
• (4) WPgen: presentation of a function that effectively computes the weakest precondition of a term, independently of its specification.
• (5) Wand: introduction of the magic wand operator and of the ramified frame rule, and extension of the weakest-precondition generator for handling local function definitions.
• (5) Affine: description of a generalization of Separation Logic with affine heap predicates, which are useful, in particular, for handling garbage-collected programming languages.
• (6) Struct: specification of array and record operations, and encoding of these operations using pointer arithmetic.
• (6) Rich: description of the treatment of additional language constructs, including loops, assertions, and n-ary functions.
• (7) Nondet: definition of triples for non-deterministic programming languages.
• (7) Partial: definition of triples for partial correctness only, i.e., for not requiring termination proofs.

Other Distributed Files

The chapters listed above depend on a number of auxiliary files, which the reader does not need to go through, but might be interested in looking at, either by curiosity, or for checking out a specific implementation detail.

• LibSepReference: a long file that defines the program verification tool that is used in the first two chapters, and whose implementation is discussed throughout the other chapters. Each chapter from the course imports this module, as opposed to importing the chapters that precedes it.
• LibSepVar: a formalization of program variables, together with a bunch of notations for parsing variables.
• LibSepFmap: a formalization of finite maps, which are used for representing the memory state.
• LibSepSimpl: a functor that implements a powerful tactic for automatically simplifying entailments in Separation Logic.
• LibSepMinimal: a minimalistic formalization of a soundness proof for Separation Logic, corresponding to the definitions and proofs presented in the ICFP'20 paper mentioned earlier.
• All other Lib* files are imports from the TLC library, which is described next.

The TLC library is a collection of general purpose theory and tactics developed over the years by Arthur Charguéraud. The TLC library is exploited in this course to streamline the presentation. TLC provides, in particular, extensions for classical logic and tactics that are particularly well-suited for meta-theory. Prior knowledge of TLC is not required, and all exercises can be completed without using TLC tactics. The classical logic aspects of TLC are presented at the moment they appear in the course. The TLC tactics are also briefly described upon their first occurrence. Moreover, most of these tactics are presented in the chapter UseTactics of Software Foundations Volume 2 (Programming Language Foundations).

Practicalities

Feedback Welcome

If you intend to use this course either in class of for self-study, the author, Arthur Charguéraud, would love to hear from you. Just knowing in which context the course has been used and how much of the course students were able to cover is very valuable information. If you plan on providing any non-small amount of feedback, do not hesitate to ask the author to be added as contributor to the github repository. In particular, please do not hesitate to improve the formulation of the English sentences throughout this volume, as the author is not a native speaker.

Exercises

Each chapter includes numerous exercises. The star rating scheme is described in the Preface of Software Foundations Volume 1 (Logical Foundations). Disclaimer: the difficulty ratings currently in place are highly speculative! You feedback is very much welcome. Disclaimer: the auto-grading system has not been tested for this volume. If you are interested in using auto-grading for this volume, please contact the author.

System Requirements

The Preface of Software Foundations Volume 1 (Logical Foundations) describes how to install Coq. The files you are reading have been tested with Coq 8.12.

Note for CoqIDE Users

CoqIDE typically works better with its asynchronous proof mode disabled. To load all the course files in CoqIDE, use the following command line.
  coqide -async-proofs off -async-proofs-command-error-resilience off -Q . Basic.v &

Recommended Citation Format

If you want to refer to this volume in your own writing, please do so as follows:
   @book {Charguéraud:SF6,
   author = {Arthur Charguéraud},
   title = "Separation Logic Foundations",
   series = "Software Foundations",
   volume = "6",
   year = "2021",
   publisher = "Electronic textbook",
   note = {Version 1.0, \URL{http://softwarefoundations.cis.upenn.edu} },
   }

Thanks

The development of the technical infrastructure for the Software Foundations series has been supported, in part, by the National Science Foundation under the NSF Expeditions grant 1521523, The Science of Deep Specification.

Basic: Basic Proofs in Separation Logic

A First Taste

This chapter gives an overview of the basic features of Separation Logic. Those features are illustrated using example programs, which are specified and verified using a particular Separation Logic framework, the construction of which is presented throughout the course. This chapter introduces the following notions:

• "Heap predicates", which are used to describe memory states in Separation Logic.
• "Specification triples", of the form triple t H Q, which relate a term t, a precondition H, and a postcondition Q.
• "Entailment proof obligations", of the form H ==> H' or Q ===> Q', which assert that a pre- or post-condition is weaker than another one.
• "Verification proof obligations", of the form PRE H CODE F POST Q, which internally leverage a form of weakest-precondition.
• Custom proof tactics, called "x-tactics", which are specialized tactics for carrying out the verification proofs.

The "heap predicates" used to describe memory states are presented throughout the chapter. They include:

• p ~~> n, which describes a memory cell at location p with contents n,
• \[], which describes an empty state,
• \[P], which also describes an empty state, and moreover asserts that the proposition P is true,
• H₁ \* H₂, which describes a state made of two disjoint parts: H₁ and H₂,
• \∃ x, H, which is used to quantify variables in postconditions.

All these heap predicates admit the type hprop, which describes predicates over memory states. Technically, hprop is defined as state→Prop. The verification of practical programs is carried out using x-tactics, identified by the leading "x" letter in their name. These tactics include:

• xwp or xtriple to begin a proof,
• xapp to reason about an application,
• xval to reason about a return value,
• xif to reason about a conditional,
• xsimpl to simplify or prove entailments (H ==> H' or Q ===> Q').

In addition to x-tactics, the proof scripts exploit standard Coq tactics, as well as tactics from the TLC library. SOONER: Recall what the TLC library is. The relevant TLC tactics, which are described when first use, include:

• math, which is a variant of lia for proving mathematical goals,
• induction_wf, which sets up proofs by well-founded induction,
• gen, which is a shorthand for generalize dependent, a tactic also useful to set up induction principles.

For simplicity, we assume all programs to be written in A-normal form, that is, with all intermediate expressions being named by a let-binding. For each program, we first show its code using OCaml-style syntax, then formally define the code in Coq using an ad-hoc notation system, featuring variable names and operators all prefixed by a quote symbol.

The Increment Function

As first example, consider the function incr, which increments the contents of a mutable cell that stores an integer. In OCaml syntax, this function is defined as:     fun p ⇒
      let n = ! p in
      let m = n + 1 in
      p := m

We describe this program in Coq using a custom set of notations for the syntax of imperative programs. (There is no need to learn how to write programs in this ad-hoc syntax: source code is provided for all the programs involved in this course.) The definition for the function incr appears below. This function is a value, so it has, like all values in our framework, the type val.

The quotes that appear in the source code are used to disambiguate between the keywords and variables associated with the source code, and those from the corresponding Coq keywords and variables. The fun keyword should be read like the fun keyword from OCaml. The specification of incr p, shown below, is expressed using a "Separation Logic triple". A triple is formally expressed by a proposition of the form triple t H Q. By convention, we write the precondition H and the postcondition Q on separate lines.

Here p denotes the address in memory of the reference cell provided as argument to the increment function. In technical vocabulary, p is the "location" of a reference cell. All locations have type loc, thus the argument p of incr has type loc. In Separation Logic, the "heap predicate" p ~~> n describes a memory state in which the contents of the location p is the value n. In the present example, n denotes an integer value. The behavior of the operation incr p consists of updating the memory state by incrementing the contents of the cell at location p, so that its new contents are n+1. Thus, the memory state posterior to the increment operation can be described by the heap predicate p ~~> (n+1). The result value returned by incr p is the unit value, which does not carry any useful information. In the specification of incr, the postcondition is of the form fun _ ⇒ ... to indicate that there is no need to bind a name for the result value. The general pattern of a specification thus includes:

• Quantification of the arguments of the functions---here, the variable p.
• Quantification of the "ghost variables" used to describe the input state---here, the variable n.
• The application of the predicate triple to the function application incr p, which is the term being specified by the triple.
• The precondition describing the input state---here, the predicate p ~~> n.
• The postcondition describing both the output value and the output state. The general pattern is fun r ⇒ H', where r names the result and H' describes the final state. Here, the final state is described by p ~~> (n+1).

Note that we have to write p ~~> (n+1) using parentheses around n+1, because p ~~> n+1 would get parsed as (p ~~> n) + 1. Our next step is to prove the specification lemma triple_incr which specifies the behavior of the function incr. We conduct the verification proof using x-tactics.

xwp begins the verification proof. The proof obligation is displayed using the custom notation PRE H CODE F POST Q. The CODE part does not look very nice, but one should be able to somehow recognize the body of incr. Indeed, if we ignore the details and perform the alpha-renaming from v to n and v₀ to m, the CODE section reads like:
              Let' n := (App val_get p) in
              Let' m := (App val_add n 1) in
              App val_set p m

which is somewhat similar to the original source code.

The remainder of the proof performs some form of symbolic execution. One should not attempt to read the full proof obligation at each step, but instead only look at the current state, described by the PRE part (here, p ~~> n), and at the first line only of the CODE part, where one can read the code of the next operation to reason about. Each function call is handled using the tactic xapp. We reason about the operation !p that reads into p; this read operation returns the value n.

We reason about the addition operation n+1.

We reason about the update operation p := n+1, thereby updating the state to p ~~> (n+1).

At this stage, the proof obligation takes the form _ ==> _, which require checking that the final state matches what is claimed in the postcondition. We discharge it using the tactic xsimpl.

The command below associates the specification lemma triple_incr with the function incr in a hint database, so that if we subsequently verify a program that features a call to incr, the xapp tactic is able to automatically invoke the lemma triple_incr.

The proof framework can be used without any knowledge about the implementation of the notation PRE H CODE F POST Q nor about the implementation of the x-tactics. Readers with prior experience in program verification may nevertheless be interested to know that PRE H CODE F POST Q is defined as the entailment H ==> F Q, where F is a form of weakest-precondition that describes the behavior of the code.

A Function with a Return Value

As a second example, let's specify a function that performs simple arithmetic computations. The function, whose code appears below, expects an integer argument n, computes a as n+1, then computes b as n-1, and finally returns a+b. The function thus always returns 2*n.

We specify this function using the the triple notation, in the form triple (example_let n) H (fun r ⇒ H'), where r, of type val, denotes the output value. To denote the fact that the input state is empty, we write \[] in the precondition. To denote the fact that the output state is empty, we could use \[]. Yet, if we write just fun r ⇒ \[] as postcondition, we would have said nothing about the output value r produced by a call example_let. Instead, we would like to specify that the result r is equal to 2*n. To that end, we write the postcondition fun r ⇒ \[r = 2*n], which actually stands for fun (r:val) ⇒ [r = val_int (2*n)], where the coercion [val_int] translates the integer value [2*n] into the corresponding value of type [val] from the programming language.

The verification proof script is very similar to the previous one. The x-tactics xapp performs symbolic execution of the code. Ultimately, we need to check that the expression computed, (n + 1) + (n - 1), is equal to the specified result, that is, 2*n. We exploit the TLC tactics math to prove this mathematical result.

The Function quadruple

Consider the function quadruple, which expects an integer n and returns its quadruple, that is, the value 4*n.

Exercise: 1 star, standard, especially useful (triple_quadruple)

Specify and verify the function quadruple to express that it returns 4*n, following the template of triple_example_let.

The Function inplace_double

Consider the function inplace_double, which expects a reference on an integer, reads twice in that reference, then updates the reference with the sum of the two values that were read.

Exercise: 1 star, standard, especially useful (triple_inplace_double)

Specify and verify the function inplace_double, following the template of triple_incr.

Separation Logic Operators

Increment of Two References

Consider the following function, which expects the addresses of two reference cells, and increments both of them.

The specification of this function takes the form triple (incr_two p q) H (fun _ ⇒ H'), where r denotes the result value of type unit. The precondition describes two references cells: p ~~> n and q ~~> m. To assert that the two cells are distinct from each other, we separate their description with the operator \*. This operator called "separating conjunction" in Separation Logic, and is also known as the "star" operator. Thus, the precondition is (p ~~> n) \* (q ~~> m), or simply p ~~> n \* q ~~> m. The postcondition describes the final state as is p ~~> (n+1) \* q ~~> (m+1), where the contents of both cells is increased by one unit compared with the precondition. The specification triple for incr_two is thus as follows.

The verification proof follows the usual pattern. Note that, from here on, we use the command Proof using. instead of just Proof., to enable asynchronous proof checking, a feature that allows for faster navigation in scripts when using CoqIDE.

We register the specification triple_incr_two in the database, to enable reasoning about calls to incr_two.

Aliased Arguments

The specification triple_incr_two correctly describes calls to the function incr_two when providing it with two distinct reference cells. Yet, it says nothing about a call of the form incr_two p p. Indeed, in Separation Logic, a state described by p ~~> n cannot be matched against a state described by p ~~> n \* p ~~> n, because the star operator requires its operand to correspond to disjoint pieces of state. What happens if we nevertheless try to exploit triple_incr_two to reason about a call of the form incr_two p p, that is, with aliased arguments? Let's find out, by considering the operation aliased_call p, which does execute such a call.

A call to aliased_call p should increase the contents of p by 2. This property can be specified as follows.

If we attempt the proof, we get stuck. Observe how xapp reports its failure to make progress.

In the above proof, we get stuck with a proof obligation of the form: \[] ==> (p ~~> ?m) \* _, which requires showing that from an empty state one can extract a reference p ~~> ?m for some integer ?m. What happened is that when matching the current state p ~~> n against p ~~> ?n \* p ~~> ?m (which corresponds to the precondition of triple_incr_two with q = p), the internal simplification tactic was able to cancel out p ~~> n in both expressions, but then got stuck with matching the empty state against p ~~> ?m. The issue here is that the specification triple_incr_two is specialized for the case of non-aliased references. It is possible to state and prove an alternative specification for the function incr_two, to cover the case of aliased arguments. Its precondition mentions only one reference, p ~~> n, and its postcondition asserts that its contents gets increased by two units. This alternative specification can be stated and proved as follows.

By exploiting the alternative specification, we are able to verify the specification of aliased_call p, which invokes incr_two p p. In order to indicate to the xapp tactic that it should invoke the lemma triple_incr_two_aliased and not triple_incr_two, we provide that lemma as argument to xapp, by writing xapp triple_incr_two_aliased.

A Function that Takes Two References and Increments One

Consider the following function, which expects the addresses of two reference cells, and increments only the first one.

We can specify this function by describing its input state as p ~~> n \* q ~~> m, and describing its output state as p ~~> (n+1) \* q ~~> m. Formally:

Observe, however, that the second reference plays absolutely no role in the execution of the function. In fact, we might equally well have described in the specification only the existence of the reference that the code actually manipulates.

Interestingly, the specification triple_incr_first, which mentions the two references, is derivable from the specification triple_incr_first', which mentions only the first reference. The proof of this fact uses the tactic xtriple, which turns a specification triple of the form triple t H Q into the form PRE H CODE t POST Q, thereby enabling this proof obligation to be processed by xapp. Here, we invoke the tactic xapp triple_incr_first', to exploit the specification triple_incr_first'.

More generally, in Separation Logic, if a specification triple holds, then this triple remains valid when we add the same heap predicate to both the precondition and the postcondition. This is the "frame" principle, a key modularity feature that we'll come back to later on in the course.

Transfer from one Reference to Another

Consider the transfer function, whose code appears below.

Exercise: 1 star, standard, especially useful (triple_transfer)

State and prove a lemma called triple_transfer specifying the behavior of transfer p q in the case where p and q denote two distinct references.

Exercise: 1 star, standard, especially useful (triple_transfer_aliased)

State and prove a lemma called triple_transfer_aliased specifying the behavior of transfer when it is applied twice to the same argument. It should take the form triple (transfer p p) H Q.

Specification of Allocation

Consider the operation ref v, which allocates a memory cell with contents v. How can we specify this operation using a triple? The precondition of this triple should be the empty heap predicate, written \[], because the allocation can execute in an empty state. The postcondition should assert that the output value is a pointer p, such that the final state is described by p ~~> v. It would be tempting to write the postcondition fun p ⇒ p ~~> v. Yet, the triple would be ill-typed, because the postcondition of a triple must be of type val→hprop, and p is an address of type loc. Instead, we need to write the postcondition in the form fun (r:val) ⇒ H', where r denotes the result value, and somehow we need to assert that r is a value of the form val_loc p, for some location p, where val_loc is the constructor that injects locations into the grammar of program values. To formally quantify the variable, we use an existential quantifier for heap predicates, written \∃. The correct postcondition for ref v is fun (r:val) ⇒ \∃ (p:loc), \[r = val_loc p] \* (p ~~> v). The complete statement of the specification appears below. Note that the primitive operation ref v is written ref v in the Coq syntax.

The pattern fun r ⇒ \∃ p, \[r = val_loc p] \* H) occurs whenever a function returns a pointer. Thus, this pattern appears pervasively. To improve concision, we introduce a specific notation for this pattern, shortening it to funloc p ⇒ H.

Using this notation, the specification triple_ref can be reformulated more concisely, as follows.

Remark: the CFML tool features a technique that generalizes the notation funloc to all return types, by leveraging type-classes. Unfortunately, the use of type-classes involves a number of technicalities that we wish to avoid in this course. For that reason, we employ only the funloc notation, and use existential quantifiers explicitly for other types.

Allocation of a Reference with Greater Contents

Consider the following function, which takes as argument the address p of a memory cell with contents n, allocates a fresh memory cell with contents n+1, then returns the address of that fresh cell.

The precondition of ref_greater needs to assert the existence of a cell p ~~> n. The postcondition of ref_greater should asserts the existence of two cells, p ~~> n and q ~~> (n+1), where q denotes the location returned by the function. The postcondition is thus written funloc q ⇒ p ~~> n \* q ~~> (n+1), which is a shorthand for fun (r:val) ⇒ \∃ q, \[r = val_loc q] \* p ~~> n \* q ~~> (n+1). The complete specification of ref_greater is:

Exercise: 2 stars, standard, especially useful (triple_ref_greater_abstract)

State another specification for the function ref_greater, called triple_ref_greater_abstract, with a postcondition that does not reveal the contents of the fresh reference q, but instead only asserts that it is greater than the contents of p. To that end, introduce in the postcondition an existentially quantified variable called m, with m > n. Then, derive the new specification from the former one, following the proof pattern employed in the proof of triple_incr_first_derived.

Deallocation in Separation Logic

Separation Logic tracks allocated data. In its simplest form, Separation Logic enforces that all allocated data is eventually deallocated. Technically, the logic is said to "linear" as opposed to "affine". Let us illustrate what happens if we forget to deallocate a reference. Consider the following program, which computes the successor of a integer n by storing it into a reference cell, then incrementing that reference, and finally returning its contents.

The operation succ_using_incr_attempt n admits an empty precondition, and a postcondition asserting that the final result is n+1. Yet, if we try to prove this specification, we get stuck.

In the above proof script, we get stuck with the entailment p ~~> (n+1) ==> \[], which indicates that the current state contains a reference, whereas the postcondition describes an empty state. We could attempt to patch the specification to account for the left-over reference. This yields a provable specification.

However, while the above specification is provable, it is not especially useful, since the piece of postcondition \∃ p, p ~~> (n+1) is of absolutely no use to the caller of the function. Worse, the caller will have its own state polluted with \∃ p, p ~~> (n+1) and will have no way to get rid of it apart from incorporating it into its own postcondition. The right solution is to alter the code to free the reference once it is no longer needed, as shown below. We assume the source language includes a deallocation operation written free p. (This operation does not exist in OCaml, but let us nevertheless continue using OCaml syntax for writing programs.)

This program may now be proved correct with respect to the intended specification. Observe in particular the last call to xapp below, which corresponds to the free operation. The final result is the value of the variable x. To reason about it, we exploit the tactic xval, as illustrated below.

Remark: if we verify programs written in a language equipped with a garbage collector (like, e.g., OCaml), we need to tweak the Separation Logic to account for the fact that some heap predicates can be freely discarded from postconditions. This variant of Separation Logic will be described in the chapter Affine.

Combined Reading and Freeing of a Reference

The function get_and_free takes as argument the address p of a reference cell. It reads the contents of that cell, frees the cell, and returns its contents.

Exercise: 2 stars, standard, especially useful (triple_get_and_free)

Prove the correctness of the function get_and_free.

Recursive Functions

Axiomatization of the Mathematical Factorial Function

Our next example consists of a program that evaluates the factorial function. To specify this function, we consider a Coq axiomatization of the mathematical factorial function, named facto.

Note that we have purposely not specified the value of facto on negative arguments.

A Partial Recursive Function, Without State

In the rest of the chapter, we consider recursive functions that manipulate the state. To gently introduce the necessary techniques for reasoning about recursive functions, we first consider a recursive function that does not involve any mutable state. The function factorec computes the factorial of its argument.     let rec factorec n =
      if n ≤ 1 then 1 else n * factorec (n-1)

The corresonding code in A-normal form is slightly more verbose.

A call factorec n can be specified as follows:

• the initial state is empty,
• the final state is empty,
• the result value r is such that r = facto n, when n ≥ 0.

In case the argument is negative (i.e., n < 0), we have two choices:

• either we explicitly specify that the result is 1 in this case,
• or we rule out this possibility by requiring n ≥ 0.

Let us follow the second approach, in order to illustrate the specification of partial functions. There are two possibilities for expressing the constraint n ≥ 0:

• either we use as precondition \[n ≥ 0],
• or we place an assumption (n ≥ 0) → _ to the front of the triple, and use an empty precondition, that is, \[].

The two presentations are totally equivalent. By convention, we follow the second presentation, which tends to improve both the readability of specifications and the conciseness of proof scripts. The specification of factorec is thus stated as follows.

Let's walk through the proof script in detail, to see in particular how to set up the induction, how to reason about the recursive call, and how to deal with the precondition n ≥ 0.

We set up a proof by induction on n to obtain an induction hypothesis for the recursive calls. Recursive calls are made each time on smaller values, and the last recursive call is made on n = 1. The well-founded relation downto 1 captures this recursion pattern. The tactic induction_wf is provided by the TLC library to assist in setting up well-founded inductions. It is exploited as follows.

Observe the induction hypothesis IH. By unfolding downto as done in the next step, this hypothesis asserts that the specification that we are trying to prove already holds for arguments that are smaller than the current argument n, and that are greater than or equal to 1.

We may then begin the interactive verification proof.

We reason about the evaluation of the boolean condition n ≤ 1.

The result of the evaluation of n ≤ 1 in the source program is described by the boolean value isTrue (n ≤ 1), which appears in the CODE section after Ifval. The operation isTrue is provided by the TLC library as a conversion function from Prop to bool. The use of such a conversion function (which leverages classical logic) greatly simplifies the process of automatically performing substitutions after calls to xapp. We next perform the case analysis on the test n ≤ 1.

Doing so gives two cases. In the "then" branch, we can assume n ≤ 1.

Here, the return value is 1.

We check that 1 = facto n when n ≤ 1.

In the "else" branch, we can assume n > 1.

We reason about the evaluation of n-1

We reason about the recursive call, implicitly exploiting the induction hypothesis IH with n-1.

We justify that the recursive call is indeed made on a smaller argument than the current one, that is, n.

We justify that the recursive call is made to a nonnegative argument, as required by the specification.

We reason about the multiplication n * facto(n-1).

We check that n * facto (n-1) matches facto n.

A Recursive Function with State

The example of factorec was a warmup. Let's now tackle a recursive function involving mutable state. The function repeat_incr p m makes m times a call to incr p. Here, m is assumed to be a nonnegative value.     let rec repeat_incr p m =
      if m > 0 then (
        incr p;
        repeat_incr p (m - 1)
      )

In the concrete syntax for programs, conditionals without an 'else' branch are written if t₁ then t₂ end. The keyword end avoids ambiguities in cases where this construct is followed by a semi-column.

The specification for repeat_incr p requires that the initial state contains a reference p with some integer contents n, that is, p ~~> n. Its postcondition asserts that the resulting state is p ~~> (n+m), which is the result after incrementing m times the reference p. Observe that this postcondition is only valid under the assumption that m ≥ 0.

Exercise: 2 stars, standard, especially useful (triple_repeat_incr)

Prove the specification of the function repeat_incr. Hint: the structure of the proof resembles that of triple_factorec'.

In the previous examples of recursive functions, the induction was always performed on the first argument quantified in the specification. When the decreasing argument is not the first one, additional manipulations are required for re-generalizing into the goal the variables that may change during the course of the induction. Here is an example illustrating how to deal with such a situation.

Trying to Prove Incorrect Specifications

We established for repeat_incr p n a specification with the constraint m ≥ 0. What if we did omit it? Where would we get stuck in the proof? Clearly, something should break, because when m < 0, the call repeat_incr p m terminates immediately. Thus, when m < 0 the final state is like the initial state p ~~> n, and not equal to p ~~> (n + m). Let us investigate how the proof breaks.

At this point, we are requested to justify that the current state p ~~> n matches the postcondition p ~~> (n + m), which amounts to proving n = n + m.

When the specification features the assumption m ≥ 0, we can prove this equality because the fact that we are in the else branch means that m ≤ 0, thus m = 0. However, without the assumption m ≥ 0, the value of m could very well be negative. Note that there exists a valid specification for repeat_incr that does not constrain m but instead specifies that the state always evolves from p ~~> n to p ~~> (n + max 0 m). The corresponding proof scripts exploits two properties of the max function.

Here is the most general specification for the function repeat_incr.

A Recursive Function Involving two References

Consider the function step_transfer p q, which repeatedly increments a reference p and decrements a reference q, until q reaches zero.     let rec step_transfer p q =
      if !q > 0 then (
        incr p;
        decr q;
        step_transfer p q
      )

The specification of step_transfer is essentially the same as that of the function transfer presented previously, the only difference being that we here assume the contents of q to be nonnegative.

Exercise: 2 stars, standard, especially useful (triple_step_transfer)

Verify the function step_transfer. Hint: to set up the induction, follow the pattern shown in the proof of triple_repeat_incr'.

Historical Notes

The key ideas of Separation Logic were devised by John Reynolds, inspired in part by older work by [Burstall 1972]. Reynolds presented his ideas in lectures given in the fall of 1999. The proposed rules turned out to be unsound, but [Ishtiaq and O'Hearn 2001] noticed a strong relationship with the logic of bunched implications by [O'Hearn and Pym 1999], 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 [O'Hearn, Reynolds, and Yang 2001] and at the LICS conference [Reynolds 2002]. The Separation Logic specifications and proof scripts using x-tactics presented in this file are directly adapted from the CFML tool (2010-2020), which is developed mainly by Arthur Charguéraud. The notations for Separation Logic predicates are directly inspired from those introduced in the Ynot project (2006-2008). See chapter Postface for references.

Repr: Representation Predicates

First Pass

SOONER AC: polish As explained in the preface chapters from there on are made of 3 parts: first pass, more details, optional material. This chapter introduces the notion of representation predicate, which is typically used for describing mutable data structures. For example, this chapter introduces the heap predicate MList L p to describe a mutable linked list whose head cell is at location p, and whose elements are described by the Coq list L. This chapter explains how to specify and verify functions that operate on mutable linked lists and mutable trees. It also presents representation predicates for functions that capture local state, such as a counter function. This chapter assumes a programming language featuring records, and it assumes the Separation Logic to support heap predicates for describing records. For example, p ~~~>`{ head := x; tail := q} describes a record allocated at location p, with a head field storing the value x and a tail field storing the value q. In this course, for simplicity, we implement field names as natural numbers---e.g., head is defined as 0 and tail as 1. Details on the formalization of records are postponed to chapter Struct. This chapter introduces a few additional tactics:

• xfun to reason about a function definition.
• xchange for exploiting transitivity of ==>.

Formalization of the List Representation Predicate

A mutable list cell is a two-cell record, featuring a head field and a tail field.

The heap predicate p ~~~>`{ head := x; tail := q} describes a record allocated at location p, with a head field storing x and a tail field storing q. A mutable list consists of a chain of cells, terminated by null. The heap predicate MList L p describes a list whose head cell is at location p, and whose elements are described by the list L. This predicate is defined recursively on the structure of L:

• if L is empty, then p is the null pointer,
• if L is of the form x::L', then p is not null, the head field of p contains x, and the tail field of p contains a pointer q such that MList L' q describes the tail of the list.

Alternative Characterizations of MList

The following reformulations are helpful in proofs, allowing us to fold or unfold the definition using a tactic called xchange.

Another characterization of MList L p is useful for proofs. Whereas the original definition is by case analysis on whether L is empty, the alternative one is by case analysis on whether p is null:

• if p is null, then L is empty,
• otherwise, L decomposes as x::L', the head field of p contains x, and the tail field of p contains a pointer q such that MList L' q describes the tail of the list.

The lemma below is stated using an entailment. The reciprocal entailment is also true, but we do not need it so we do not bother proving it here.

In-place Concatenation of Two Mutable Lists

The function append shown below expects a nonempty list p₁ and a list p₂, and it updates p₁ in place so that its tail gets extended by the cells from p₂.     let rec append p₁ p₂ =
      if p₁.tail == null
        then p₁.tail <- p₂
        else append p₁.tail p₂

The append function is specified and verified as follows. The proof pattern is representative of that of many list-manipulating functions, so it is essential that the reader follow through every step of the proof.

The induction principle provides an hypothesis for the tail of L₁, i.e., for the list L₁', such that the relation list_sub L₁' L₁ holds.

To begin the proof, we reveal the head cell of p₁. We let q₁ denote the tail of p₁, and L₁' the tail of L₁.

We then reason about the case analysis.

If q₁' is null, then L₁' is empty.

In this case, we set the pointer, then we fold back the head cell.

Otherwise, if q₁' is not null, we reason about the recursive call using the induction hypothesis, then we fold back the head cell.

Smart Constructors for Linked Lists

This section introduces two smart constructors for linked lists, called mnil and mcons. The operation mnil() is intended to create an empty list. Its implementation simply returns the value null. Its specification asserts that the return value is a pointer p such that MList nil p holds.

Observe that the specification triple_mnil does not mention the null pointer anywhere. This specification may thus be used to specify the behavior of operations on mutable lists without having to reveal low-level implementation details that involve the null pointer. The operation mcons x q is intended to allocate a fresh list cell, with x in the head field and q in the tail field. The implementation of this operation allocates and initializes a fresh record made of two fields. The allocation operation leverages the New construct, which is notation for a operation called val_new_hrecord_2, which we here view as a primitive operation. (The chapter Struct describes an encoding of this function in terms of the allocation and write operations.)

The operation mcons admits two specifications: one that describes only the fresh record allocated, and one that combines it with a list representation of the form Mlist q L to produce as postcondition an extended list of the form Mlist p (x::L). The first specification is as follows.

The second specification is derived from the first.

Copy Function for Lists

The function mcopy takes a mutable linked list and builds an independent copy of it. This program illustrates the use the of functions mnil and mcons, and gives another example of a proof by induction.     let rec mcopy p =
      if p == null
        then mnil ()
        else mcons (p.head) (mcopy p.tail)

The precondition of mcopy requires a linked list MList L p. Its postcondition asserts that the function returns a pointer p' and a list MList L p', in addition to the original list MList L p. The two lists are totally disjoint and independent, as captured by the separating conjunction symbol (the star).

The proof script is very similar in structure to the previous ones. While playing the script, try to spot the places where:

• mnil produces an empty list of the form MList nil p',
• the recursive call produces a list of the form MList L' q',
• mcons produces a list of the form MList (x::L') p'.

Length Function for Lists

The function mlength takes a mutable linked list and computes its length.     let rec mlength p =
      if p == null
        then 0
        else 1 + mlength p.tail

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

Prove the correctness of the function mlength.

Alternative Length Function for Lists

In the previous section, the function mlength computes the length using a recursive function that returns an integer. In this section, we consider an alternative implementation that uses an auxiliary reference cell to keep track of the number of cells traversed so far. The list is traversed recursively, incrementing the contents of the reference once for every cell. The corresponding implementation is shown below. The variable c denotes the location of the auxiliary reference cell.     let rec listacc c p =
      if p == null
        then ()
        else (incr c; listacc c p.tail)

    let mlength' p =
      let c = ref 0 in
      listacc c p;
      !c

Exercise: 3 stars, standard, especially useful (triple_mlength')

Prove the correctness of the function mlength'. Hint: start by stating a lemma triple_acclength expressing the specification of the recursive function acclength. Then, register that specification for subsequent use by xapp using the command Hint Resolve triple_acclength : triple. Finally, complete the proof of the specification triple_mlength'.

In-Place Reversal Function for Lists

The function mrev takes as argument a pointer on a mutable list, and returns a pointer on the reverse list, that is, a list with elements in the reverse order. The cells from the input list are reused for constructing the output list---the operation is "in-place". Its implementation appears next.     let rec mrev_aux p₁ p₂ =
      if p₂ == null
        then p₁
        else (let p₃ = p₂.tail in
              p₂.tail <- p₁;
              mrev_aux p₂ p₃)

    let mrev p =
      mrev_aux p null

Exercise: 5 stars, standard, optional (triple_mrev)

Prove the correctness of the functions mrev_aux and mrev. Hint: start by stating a lemma mtriple_rev_aux expressing the specification of the recursive function mrev_aux. Then, register the specification using Hint Resolve triple_acclength : triple.. Finally, complete the proof of triple_mrev. Hint: don't forget to generalize all the necessary variables before applying the well-founded induction principle.

More Details

Sized Stack

In this section, we consider the implementation of a mutable stack with constant-time access to its size, i.e., to the number of items it stores. The stack structure consists of a 2-field record, storing a pointer on a mutable linked list, and an integer storing the length of that list. The stack implementation exposes a function to create an empty stack, a function for reading the size, and push and pop methods for operating at the top of the stack.     type 'a stack = { data : 'a list; size : int }

    let create () =
      { data = nil; size = 0 }

    let sizeof s =
      s.size

    let push p x =
      s.data <- mcons x s.data;
      s.size <- s.size + 1

    let pop s =
      let p = s.data in
      let x = p.head in
      let q = p.tail in
      delete p;
      s.data <- q in
      s.size <- s.size - 1;
      x

The representation predicate for the stack takes the form Stack L s, where s denotes the location of the record describing the stack, and where L denotes the list of items stored in the stack. The underlying mutable list is described as MList L p, where p is the location p stored in the first field of the record. The definition of Stack is as follows.

Observe that the predicate Stack does not expose the address of the mutable list; this adress is existentially quantified in the definition. The predicate Stack also does not expose the size of the stack, as this value can be deduced as length L.

The sizeof operation returns the contents of the size field of a stack.

The push operation extends the head of the list, and increments the size field.

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

Prove the following specification for the push operation.

The push operation extracts the element at the head of the list, updates the data field to the tail of the list, and decrements the size field.

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

Prove the following specification for the pop operation.

Formalization of the Tree Representation Predicate

So far in this chapter, we have presented the representation of mutable lists in Separation Logic. We next consider the generalization to mutable binary trees. Just like mutable lists are specified with respect to Coq's purely functional lists, mutable binary trees are specified with respect to purely functional trees. For simplicity, let us consider a definition specialized for trees storing integer values in the nodes. The corresponding inductive definition is as shown below. A node from a logical tree takes the form Node n T₁ T₂, where n is an integer and T₁ and T₂ denote the two subtrees. A leaf is represented by the constructor Leaf.

A mutable tree node consists of a three-cell record, featuring an field storing an integer named "item", and two pointers named "left" and "right", denoting the pointers to the left and right subtrees, respectively.

The heap predicate p ~~~>`{ item := n; left := p₁; right := p₂ } describes a record allocated at location p, describing a node storing the integer n, with its two subtrees at locations p₁ and p₂. An empty tree is represented using the null pointer. The representation predicate MTree T p, of type hprop, asserts that the mutable tree structure with root at location p describes the logical tree T. The predicate is defined recursively on the structure of T:

• if T is a Leaf, then p is the null pointer,
• if T is a node Node n T₁ T₂, then p is not null, and at location p one finds a record with field contents n, p₁ and p₂, with MTree T₁ p₁ and MTree T₂ p₂ describing the two subtrees.

Alternative Characterization of MTree

Just like for MList, it is very useful for proofs to state three lemmas that paraphrase the definition of MTree. The first two lemmas correspond to folding/unfolding rules for leaves and nodes.

The third lemma reformulates MTree T p using a case analysis on whether p is the null pointer. This formulation matches the case analysis typically perform in the code of functions operating on trees.

Additional Tooling for MTree

For reasoning about recursive functions over trees, it is useful to exploit the well-founded order associated with "immediate subtrees". This order, named tree_sub, can be exploited for a tree T by invoking the tactic induction_wf IH: tree_sub T.

For allocating fresh tree nodes as a 3-field record, we introduce the operation mnode n p₁ p₂, defined and specified as follows.

The first specification of mnode describes the allocation of a record.

The second specification, derived from the first, asserts that, if provided the description of two subtrees T₁ and T₂ at locations p₁ and p₂, the operation mnode n p₁ p₂ builds, at a fresh location p, a tree described by Mtree [Node n T₁ T₂] p.

Exercise: 2 stars, standard, optional (triple_mnode')

Prove the specification triple_mnode' for node allocation.

Tree Copy

The operation tree_copy takes as argument a pointer p on a mutable tree and returns a fresh copy of that tree. It is constructed in similar way to the function mcopy for lists.     let rec tree_copy p =
      if p = null
        then null
        else mnode p.item (tree_copy p.left) (tree_copy p.right)

Exercise: 3 stars, standard, optional (triple_tree_copy)

Prove the specification of tree_copy.

Computing the Sum of the Items in a Tree

The operation mtreesum takes as argument the location p of a mutable tree, and it returns the sum of all the integers stored in the nodes of that tree. Consider the implementation that traverses the tree and uses an auxiliary reference cell for maintaining the sum of all the items visited so far.     let rec treeacc c p =
      if p ≠ null then (
        c := !c + p.item;
        treeacc c p.left;
        treeacc c p.right)

    let mtreesum p =
      let c = ref 0 in
      treeacc c p;
      !c

The specification of mtreesum is expressed in terms of the logical operation treesum which computes the sum of the node items stored in a logical tree. This operation is defined in Coq as a fixed point.

Exercise: 4 stars, standard, optional (triple_mtreesum)

Prove the correctness of the function mlength'. Hint: start by stating a lemma triple_treeacc, then register it using the command Hint Resolve triple_treeacc : triple.. Finally, complete the proof of the specification triple_mtreesum.

Verification of a Counter Function with Local State

In this section, we present another kind of representation predicate: one that describes a function with an internal, mutable state.

A counter function is a function f such that, each time it is invoked, returns the next integer, starting from 1. The function create_counter produces a fresh counter function. Concretely, if create_counter() produces the counter f, then the first call to f() returns 1, the second call to f() returns 2, the third call to f() returns 3, and so on. The counter function can be implemented using a reference cell, named p, that stores the integer last returned by the counter. Initially, the contents of the reference p is zero. Each time the counter is queried, the contents of p is increased by one unit, and the new value of the contents is returned to the caller.     let create_counter () =
       let p = ref 0 in
       (fun () → (incr p; !p))

The remaining of this section presents two set of specifications, each covering both the specification of a counter function and the specification of a function that creates a fresh counter function. The first specification is the most direct: it exposes the existence of a reference p. Doing so, however, reveals implementation details about the counter function. The second specification is more abstract: it successfully hides the description of the internal representation of the counter, and states specification only in terms of a representation predicate, called IsCounter f n, that exposes only the identity of the counter function and its current value, but not the existence of the reference p. Let's begin with the simple, direct specification. The proposition CounterSpec f p asserts that the counter function f has its internal state stored in a reference cell at location p, in the sense that invoking f in a state p ~~> m updates the state to p ~~> (m+1) and produces the output value m+1.

The function create_counter creates a fresh counter. Its precondition is empty. Its postcondition describes the existence of a reference cell p ~~> 0, for an existentially quantified location p, and such that the proposition CounterSpec f p holds. Observe the use of the tactic xfun for reasoning about a function definition.

Given a counter function described by CounterSpec f p, a call to the function f on a unit argument, in an input state of the form p ~~> n for some n, produces the state p ~~> (n+1) and the output value n+1. Observe how this specification applies to any function f satisfying CounterSpec f p.

In the proof above, we were able to directly apply the assumption Hf. In general, however, for reasoning about a call to an abstract function f, it is generally needed to first invoke the tactic xwp.

Let's now make the specifications more abstract, by hiding away the description of the reference cells from the client of the specifications. To that end, we introduce the heap predicate IsCounter f n, which relates a function f, its current value n, and the piece of memory state involved in the implementation of this function. This piece of memory is of the form p ~~> n for some location p, such that CounterSpec f p holds. Here, p gets quantified existentially.

Using IsCounter, we can reformulate the specification of create_counter is a more abstract and more concise manner, with a postcondition simply asserting that the fresh counter function f initialized at zero is described by the heap predicate IsCounter f 0.

Likewise, we can reformulate the specification of a call to a counter function f. Such a call, under precondition IsCounter f n for some n, admits the precondition IsCounter f (n+1), and returns n+1.

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

Prove the abstract specification for a counter function. Hint: use xtriple at some point.

Optional Material

Specification of a Higher-Order Repeat Operator

As a warm-up before presenting the specifications of higher-order iterators such as iter and fold over mutable lists, we present the specification of an higher-order operator named repeat. A call to repeat f n executes n successives calls to f on the unit value, that is, calls to f().     let rec repeat f n =
      if n > 0 then (f(); repeat f (n-1))

For simplicity, let us assume for now n ≥ 0. The specification of repeat n f is expressed in terms of an invariant, named I, describing the state in-between every two calls to f. Initially, we assume the state to satisfy f 0. We assume that, for every index i in the range from 0 (inclusive) to n (exclusive), a call f() takes the state from one satisfying f i to one satisfying f (i+1). The specification below asserts that, under these assumptions, after the n calls to f(), the final state satisfies f n. The specification takes the form:
    n ≥ 0 →
    Hypothesis_on_f →
    triple (repeat f n)
      (I 0)
      (fun u ⇒ I n).

where the hypothesis of f captures the following specification:
    0 ≤ i < n →
    triple (f ())
      (I i)
      (fun u ⇒ I (i+1))

The complete specification of repeat n f appears below.

To establish that specification, we carry out a proof by induction over the judgment:
    triple (repeat f m)
      (I (n-m))
      (fun u ⇒ I n)).

which asserts that, when there remains m calls to perform, the current state is described by I (n-m), that is, the current index i is equal to n-m.

Specification of an Iterator on Mutable Lists

The operation miter takes as argument a function f and a pointer p on a mutable list, and invokes f on each of the items stored in that list.     let rec miter f p =
      if p ≠ null then (f p.head; miter f p.tail)

The specification of miter follows the same structure as that of the function repeat from the previous section, with two main differences. The first difference is that the invariant is expressed not in terms of an index i ranging from 0 to n, but in terms of a prefix of the list L being traversed, ranging from nil to the full list L. The second difference is that the operation miter f p requires in its precondition, in addition to I nil, the description of the mutable list MList L p. This predicate is returned in the postcondition, unchanged, reflecting on the fact that the iteration does not alter the list.

Exercise: 5 stars, standard, especially useful (triple_miter)

Prove the correctness of triple_miter.

For exploiting the specification triple_miter to reason about a call to miter, it is necessary to provide an invariant I of type list val → hprop, that is, of the form fun (K:list val) ⇒ .... This invariant, which cannot be inferred automatically, should describe the state at the point where the iteration has traversed a prefix K of the list L. Concretely, for reasoning about a call to miter, one should exploit the tactic xapp (triple_iter (fun K ⇒ ...)).

Computing the Length of a Mutable List using an Iterator

We can compute the length of a mutable list by iterating over that list a function that increments a reference cell once for every item.     let mlength_using_miter p =
      let c = ref 0 in
      miter (fun x → incr c) p;
      !c

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

Prove the correctness of mlength_using_iter. Hint: use xfun. intros f Hf for reasoning about the function definition, then use xapp for reasoning about a call to f by inlining its code.

A Continuation-Passing-Style, In-Place Concatenation Function

The following program was proposed in the original article on Separation Logic by John Reynolds as a challenge for verification. This function, called cps_append, is similar to the function append presented previously: it also performs in-place concatenation of two lists. It differs in that it is implemented using a recursive, continuation-passing style function to perform the work. The presentation of cps_append p₁ p₂ is also slightly different: this operation returns a pointer p₃ that describes the head of the result of the concatenation, and it works even if p₁ corresponds to an empty list. The code of cps_append involves an auxiliary function cps_append_aux. This code appears at first like a puzzle: it takes a good drawing and several minutes to figure out how it works. Observe in particular how the recursive call is invoked as part of the continuation.     let rec cps_append_aux p₁ p₂ k =
      if p₁ == null
        then k p₂
        else cps_append_aux p₁.tail p₂ (fun r ⇒ (p₁.tail <- r); k p₁)

    let cps_append p₁ p₂ =
      cps_append_aux p₁ p₂ (fun r ⇒ r)

Exercise: 5 stars, standard, optional (triple_cps_append)

Specify and verify cps_append_aux, then verify cps_append.

The main function cps_append simply invokes cps_append_aux with a trivial continuation.

This concludes the formal verification of Reynolds' verification challenge.

Historical Notes

The representation predicate for lists appears in the seminal papers on Separation Logic: the notes by Reynolds from the summer 1999, updated the next summer [Reynolds 2000], and the publication by [O’Hearn, Reynolds, and Yang 2001]. Most presentations of Separation Logic target partial correctness, whereas this chapters targets total correctness. The specifications of recursive functions are established using the built-in induction mechanism offered by Coq. The specification of higher-order iterators requires higher-order Separation Logic. Being embedded in the higher-order logic of Coq, the Separation Logic that we work with is inherently higher-order. Further information on the history of higher-order Separation Logic for higher-order programs may be found in section 10.2 of http://www.chargueraud.org/research/2020/seq_seplogic/seq_seplogic.pdf.

Hprop: Heap Predicates

Tweak to simplify the use of definitions and lemmas from LibSepFmap.v.

First Pass

In the programming language that we consider, a concrete memory state is described as a finite map from locations to values.

• A location has type loc.
• A value has type val.
• A state has type state.

Details will be presented in the chapter Rules. To help distinguish between full states and pieces of state, we let the type heap be a synonymous for state but with the intention of representing only a piece of state. Throughout the course, we write s for a full memory state (of type state), and we write h for a piece of memory state (of type heap). In Separation Logic, a piece of state is described by a "heap predicate", i.e., a predicate over heaps. A heap predicate has type hprop, defined as heap→Prop, which is equivalent to state→Prop. By convention, throughout the course:

• H denotes a heap predicate of type hprop; it describes a piece of state,
• Q denotes a postcondition, of type val→hprop; it describes both a result value and a piece of state. Observe that val→hprop is equivalent to val→state→Prop.

This chapter presents the definition of the key heap predicate operators from Separation Logic:

• \[] denotes the empty heap predicate,
• \[P] denotes a pure fact,
• p ~~> v denotes a singleton heap,
• H₁ \* H₂ denotes the separating conjunction,
• Q₁ \*+ H₂ denotes the separating conjunction, between a postcondition and a heap predicate,
• \∃ x, H denotes an existential.

This chapter also introduces the formal definition of triples:

• a Hoare triple, written hoare t H Q, features a precondition H and a postcondition Q that describe the whole memory state in which the execution of the term t takes place.
• a Separation Logic triple, written triple t H Q, features a pre- and a postcondition that describes only the piece of the memory state in which the execution of the term t takes place.

This chapter and the following ones exploit a few additional TLC tactics to enable concise proofs.

• applys is an enhanced version of eapply.
• applys_eq is a variant of applys that enables matching the arguments of the predicate that appears in the goal "up to equality" rather than "up to conversion".
• specializes is an enhanced version of specialize.
• lets and forwards are forward-chaining tactics that enable instantiating a lemma.

What these tactics do should be fairly intuitive where they are used. Note that all exercises can be carried out without using TLC tactics. For details, the chapter UseTactics.v from the "Programming Language Foundations" volume explains the behavior of these tactics.