Software Foundations Logo
Volume 6: Separation Logic Foundations
  • Table of Contents
  • Index
  • Roadmap

Introduction to the Course    (Preface)

  • Welcome
  • Separation Logic
  • Separation Logic in a proof assistant
  • Several Possible Depths of Reading
  • List of Chapters
  • Other Distributed Files
  • Practicalities
    • Feedback Welcome
    • Exercises
    • System Requirements
    • Note for CoqIDE Users
    • Recommended Citation Format
  • Thanks

Basic Proofs in Separation Logic    (Basic)

  • A First Taste
    • Parsing of Programs
    • Specification of the Increment Function
    • Verification of the Increment Function
    • A Function with a Return Value
  • Separation Logic Operators
    • Increment of Two References
    • Aliased Arguments
    • A Function that Takes Two References and Increments One
    • Transfer from one Reference to Another
    • Specification of Allocation
    • Allocation of a Reference with Greater Contents
    • Deallocation in Separation Logic
    • Combined Reading and Freeing of a Reference
  • Recursive Functions
    • Axiomatization of the Mathematical Factorial Function
    • A Partial Recursive Function, Without State
    • A Recursive Function with State
    • Trying to Prove Incorrect Specifications
    • A Recursive Function Involving two References
  • Summary
  • Historical Notes

Representation Predicates    (Repr)

  • First Pass
    • Formalization of the List Representation Predicate
    • Alternative Characterizations of MList
    • In-place Concatenation of Two Mutable Lists
    • Smart Constructors for Linked Lists
    • Copy Function for Lists
    • Length Function for Lists
    • Alternative Length Function for Lists
    • In-Place Reversal Function for Lists
  • More Details
    • Sized Stack
    • Formalization of the Tree Representation Predicate
    • Alternative Characterization of MTree
    • Additional Tooling for MTree
    • Tree Copy
    • Computing the Sum of the Items in a Tree
    • Verification of a Counter Function with Local State
    • Verification of a Counter Function with Local State, With Abstraction
  • Optional Material
    • Specification of a Higher-Order Repeat Operator
    • Specification of an Iterator on Mutable Lists
    • Computing the Length of a Mutable List using an Iterator
    • A Continuation-Passing-Style, In-Place Concatenation Function
    • Historical Notes

Heap Predicates    (Hprop)

  • First Pass
    • Syntax and Semantics
    • Description of the State
    • Heap Predicates
    • Extensionality for Heap Predicates
    • Type and Syntax for Postconditions
    • Separation Logic Triples and the Frame Rule
    • Example of a Triple: the Increment Function
  • More Details
    • Example Applications of the Frame Rule
    • Power of the Frame Rule with Respect to Allocation
    • Notation for Heap Union
    • Introduction and Inversion Lemmas for Basic Operators
  • Optional Material
    • Alternative, Equivalent Definitions for Separation Logic Triples
    • Alternative Definitions for Heap Predicates
    • Additional Explanations for the Definition of \∃
    • Formulation of the Extensionality Axioms
    • Historical Notes

Heap Entailment    (Himpl)

  • First Pass
    • Definition of Entailment
    • Entailment for Postconditions
    • Fundamental Properties of Separation Logic Operators
    • Introduction and Elimination Rules w.r.t. Entailments
    • Extracting Information from Heap Predicates
    • Consequence, Frame, and their Combination
    • The Extraction Rules for Triples
  • More Details
    • Identifying True and False Entailments
    • Proving Entailments by Hand
    • The xsimpl Tactic
    • The xchange Tactic
  • Optional Material
    • Proofs for the Separation Algebra
    • Proof of the Consequence Rule
    • Proof of the Extraction Rules for Triples
    • Alternative Structural Rule for Existentials
    • Historical Notes

Reasoning Rules    (Rules)

  • First Pass
    • Semantic of Terms
    • Rules for Terms
    • Specification of Primitive Operations
    • Review of the Structural Rules
    • Verification Proof in Separation Logic
    • What's Next
  • More Details
    • Alternative Specification Style for Pure Preconditions
    • The Combined let-frame Rule Rule
    • Proofs for the Rules for Terms
    • Proofs for the Arithmetic Primitive Operations
    • Proofs for Primitive Operations Operating on the State
  • Optional Material
    • Reasoning Rules for Recursive Functions
    • Alternative Specification Style for Result Values.
    • Historical Notes

Semantics of Weakest Preconditions    (WPsem)

  • First Pass
    • Notion of Weakest Precondition
    • Structural Rules in Weakest-Precondition Style
    • Reasoning Rules for Terms, in Weakest-Precondition Style
  • More Details
    • Other Reasoning Rules for Terms
  • Optional Material
    • A Concrete Definition for Weakest Precondition
    • Equivalence Between all Definitions Of wp
    • An Alternative Definition for Weakest Precondition
    • Extraction Rule for Existentials
    • Combined Structural Rule
    • Alternative Statement of the Rule for Conditionals
    • Definition of wp Directly from hoare
    • Historical Notes

Weakest Precondition Generator    (WPgen)

  • First Pass
  • More Details
    • Definition of wpgen for Term Rules
    • Computing with wpgen
    • Optimizing the Readability of wpgen Output
    • Extension of wpgen to Handle Structural Rules
    • Lemmas for Handling wpgen Goals
    • An Example Proof
    • Making Proof Scripts More Concise
    • Further Improvements to the xapp Tactic.
    • Demo of a Practical Proof using x-Tactics.
  • Optional Material
    • Tactics xconseq and xframe
    • Soundness Proof for wpgen
    • Guessing the Definition of mkstruct
    • Proof of Properties of Iterated Substitution
    • Historical Notes

The Magic Wand Operator    (Wand)

  • First Pass
    • Intuition for the Magic Wand
    • Definition of the Magic Wand
    • Characteristic Property of the Magic Wand
    • Magic Wand for Postconditions
    • Frame Expressed with hwand: the Ramified Frame Rule
    • Ramified Frame Rule in Weakest-Precondition Style
    • Automation with xsimpl for hwand Expressions
    • Evaluation of wpgen Recursively in Locally Defined Functions
  • More Details
    • Benefits of the Ramified Rule over the Consequence-Frame Rule
    • Properties of hwand
  • Optional Material
    • Equivalence Between Alternative Definitions of the Magic Wand
    • Operator hforall
    • Alternative Definition of qwand
    • Equivalence between Alternative Definitions of the Magic Wand
    • Simplified Definition of mkstruct
    • Texan Triples
    • Direct Proof of wp_ramified Directly from Hoare Triples
    • Conjunction and Disjunction Operators on hprop
    • Summary of All Separation Logic Operators
    • Historical Notes

Affine Separation Logic    (Affine)

  • First Pass
    • Motivation for the Discard Rule
    • Statement of the Discard Rule
    • Fine-grained Control on Collectable Predicates
    • Definition of heap_affine and of haffine
    • Definition of the "Affine Top" Heap Predicates
    • Properties of the \GC Predicate
    • Instantiation of heap_affine for a Fully Affine Logic
    • Instantiation of heap_affine for a Fully Linear Logic
    • Refined Definition of Separation Logic Triples
    • Soundness of the Existing Rules
    • Soundness of the Discard Rules
    • Discard Rules in WP Style
    • Exploiting the Discard Rule in Proofs
    • Example Proof Involving Discarded Heap Predicates
  • More Details
    • Revised Definition of mkstruct
    • The Tactic xaffine, and Behavior of xsimpl on \GC
    • The Proof Tactics for Applying the Discard Rules
  • Optional Material
    • Alternative Statement for Distribution of haffine on Quantifiers
    • Pre and Post Rules
    • Low-level Definition of Refined Triples
    • Historical Notes

Arrays and Records    (Struct)

  • First Pass
    • Representation of a Set of Consecutive Cells
    • Representation of an Array with a Block Header
    • Specification of Allocation
    • Specification of the Deallocation
    • Specification of Array Operations
    • Representation of Individual Records Fields
    • Representation of Records
    • Example with Mutable Linked Lists
    • Reading in Record Fields
    • Writing in Record Fields
    • Allocation of Records
    • Deallocation of Records
    • Combined Record Allocation and Initialization
  • More Details
    • Extending xapp to Support Record Access Operations
    • Deallocation Function for Lists
  • Optional Material
    • Refined Source Language
    • Realization of hheader
    • Introduction and Elimination Lemmas for hcells and harray
    • Proving the Specification of Allocation and Deallocation
    • Splitting Lemmas for hcells
    • Specification of Pointer Arithmetic
    • Specification of the length Operation to Read the Header
    • Encoding of Array Operations using Pointer Arithmetic
    • Encoding of Record Operations using Pointer Arithmetic
    • Specification of Record Operations w.r.t. hfields and hrecord
    • Specification of Record Allocation and Deallocation

Assertions, Loops, N-ary Functions    (Rich)

  • First Pass
    • Reasoning Rule for Assertions
    • Semantics of Conditionals not in Administrative Normal Form
    • Semantics and Basic Evaluation Rules for While-Loops
    • Separation-Logic-friendly Reasoning Rule for While-Loops
  • More Details
    • Semantics and Basic Evaluation Rules for For-Loops
    • Treatment of Generalized Conditionals and Loops in wpgen
    • Notation and Tactics for Manipulating While-Loops
    • Example of the Application of Frame During Loop Iterations
    • Reasoning Rule for Loops in an Affine Logic
    • Curried Functions of Several Arguments
    • Primitive n-ary Functions
  • Optional Material
    • A Coercion for Parsing Primitive N-ary Applications
    • Historical Notes

Triples for Nondeterministic Languages    (Nondet)

  • First Pass
    • Non-Deterministic Big-Step Semantics: the Predicate evaln
    • Interpretation of evaln w.r.t. eval
    • Triples for Non-Deterministic Big-Step Semantics
    • Triple-Style Reasoning Rules for a Non-Deterministic Semantics.
  • More Details
    • Weakest-Precondition Style Presentation.
    • Hoare Logic WP-Style Rules for a Non-Deterministic Semantics.
    • Separation Logic WP-Style Rules for a Non-Deterministic Semantics.
  • Optional Material
    • Interpretation of evaln w.r.t. eval and terminates
    • Small-Step Evaluation Relation
    • Small-Step Characterization of evalns: Attempts
    • Small-Step Characterization of evaln: A Solution
    • Triples for Small-Step Semantics
    • Reasoning Rules for seval
    • Reasoning Rules for hoarens
    • Equivalence Between Non-Deterministic Small-Step and Big-Step Sem.
    • Historical Notes

Triples for Partial Correctness    (Partial)

  • First Pass
    • Big-Step Characterization of Partial Correctness
    • From Total to Partial Correctness
    • Characterization of Divergence
    • Big-Step-Based Reasoning Rules
    • Big-Step-Based Reasoning Rules for Divergence
  • Optional Material
    • Interpretation of evalnp w.r.t. eval and safe
    • Small-Step Characterization of Partial Correctness
    • Reasoning Rules w.r.t. Small-Step Characterization
    • Small-Step Characterization of Divergence
    • Coinductive, Small-Step Characterization of Partial Correctness
    • Equivalence Between the Two Small-Step Charact. of Partial Correctness
    • Equivalence Between Small-Step and Big-Step Partial Correctness
    • Historical Notes

Conclusion and Perspectives    (Postscript)

  • Beyond the Scope of This Course
  • Historical Notes
  • Tools Leveraging Separation Logic
  • Related Courses
  • Acknowledgments

Bibliography    (Bib)

  • Resources cited in this volume

Appendix - The Full Construction    (LibSepReference)

  • Imports
    • Extensionality Axioms
    • Variables
    • Finite Maps
  • Source Language
    • Syntax
    • Coq Tweaks
    • Substitution
    • Semantics
  • Heap Predicates
    • Hprop and Entailment
    • Definition of Heap Predicates
    • Basic Properties of Separation Logic Operators
    • Properties of haffine
  • Reasoning Rules
    • Evaluation Rules for Primitives in Separation Style
    • Hoare Reasoning Rules
  • Definition of total correctness Hoare Triples.
    • Definition of Separation Logic Triples.
    • Structural Rules
    • Rules for Terms
    • Triple-Style Specification for Primitive Functions
    • Alternative Definition of wp
  • WP Generator
    • Definition of Context as List of Bindings
    • Multi-Substitution
    • Definition of wpgen
  • Practical Proofs
    • Lemmas for Tactics to Manipulate wpgen Formulae
    • Tactics to Manipulate wpgen Formulae
    • Notations for Triples and wpgen
    • Notation for Concrete Terms
    • Scopes, Coercions and Notations for Concrete Programs
  • Bonus
    • Disjunction: Definition and Properties of hor
    • Conjunction: Definition and Properties of hand
    • Treatment of Functions of 2 and 3 Arguments
    • Bonus: Triples for Applications to Several Arguments
    • Specification of Record Operations
  • Demo Programs
    • The Decrement Function

Appendix - Finite Maps    (LibSepFmap)

  • Representation of Finite Maps
    • Representation of Potentially-Infinite Maps as Partial Functions
    • Representation of Finite Maps as Dependent Pairs
    • Predicates on Finite Maps
  • Poperties of Operations on Finite Maps
    • Equality
    • Disjointness
    • Union
    • Compatibility
    • Domain
    • Disjoint and Domain
    • Read
    • Update
    • Removal
  • Tactics for Finite Maps
    • Tactic disjoint for proving disjointness results
    • Tactic rew_map for Normalizing Expressions
    • Tactic fmap_eq for Proving Equalities
  • Existence of Fresh Locations
    • Consecutive Locations
    • Existence of Fresh Locations
    • Existence of a Smallest Fresh Locations
    • Existence of Nonempty Heaps

Appendix - Program Variables    (LibSepVar)

  • Representation of Program Variables
    • Representation of Variables
    • Tactic case_var
  • Representation of List of Variables
    • Definition of Distinct Variables
    • Definition of n Distinct Variables
    • Generation of n Distinct Variables
  • Notation for Program Variables
    • Program Variables Expressed Using Definitions
    • Program Variables Expressed Using Notation, with a Quote Symbol
  • Optional Material
    • Bonuse: the Tactic var_neq

Appendix - Simplification of Entailments    (LibSepSimpl)

  • A Functor for Separation Logic Entailment
  • Assumptions of the functor
    • Operators
    • Notation
    • Properties Assumed by the Functor
  • Body of the Functor
    • Properties of himpl
    • Properties of qimpl
    • Properties of hstar
    • Representation Predicates
    • rew_heap Tactic to Normalize Expressions with hstar
    • Auxiliary Tactics Used by xpull and xsimpl
    • Tactics xsimpl and xpull for Heap Entailments
  • Demos

Appendix - Minimalistic Soundness Proof    (LibSepMinimal)

  • Source Language
    • Syntax
    • Semantics
    • Automation for Heap Equality and Heap Disjointness
  • Heap Predicates and Entailment
    • Extensionality Axioms
    • Core Heap Predicates
    • Entailment
    • Properties of hstar
    • Properties of hpure
    • Properties of hexists
    • Properties of hforall
    • Properties of hsingle
    • Basic Tactics for Simplifying Entailments
    • Reformulation of the Evaluation Rules for Primitive Operations.
  • Hoare Logic
    • Definition of Total Correctness Hoare Triples
    • Structural Rules for Hoare Triples
    • Reasoning Rules for Terms, for Hoare Triples
    • Specification of Primitive Operations, for Hoare Triples.
  • Separation Logic
    • Definition of Separation Logic triples
    • Structural Rules
    • Reasoning Rules for Terms
    • Specification of Primitive Operations
  • Bonus: Example Proof