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
  • Multiple Reading Depths
  • Chapters Overview
  • Other Distributed Files
  • Practicalities
    • System Requirements
    • Feedback Welcome
    • Exercises
    • 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
    • The Power of the Frame Rule with Respect to Allocation
    • Deallocation in Separation Logic
    • Combined Reading and Freeing of a Reference
    • Nondeterminism: Specifying Random Output Values
  • 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
    • Computing Factorial using State
  • Summary
  • Optional Material
  • Historical Notes

Representation Predicates    (Repr)

  • First Pass
    • 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
    • Free Function for Lists
    • In-Place Reversal Function for Lists
  • More Details
    • A Stack Represented as a List and a Size
    • Formalization of the Tree Representation Predicate MTree
    • Alternative Characterization of MTree
    • Additional Tooling for MTree
    • Deep-Copy of a Tree
    • Computing the Sum of the Items in a Tree
    • Verification of a Counter Function with Local State
  • 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
    • Factorial Function in Continuation-Passing Style
    • In-Place Concatenation Function in Continuation-Passing Style
    • Historical Notes

Heap Predicates    (Hprop)

  • First Pass
    • Description of Memory States
    • Heap Predicates
    • Extensionality for Heap Predicates
    • Fundamental Properties of Operators
    • Postconditions: Type, Syntax, and Extensionality
    • Introduction and Inversion Lemmas for Basic Operators
    • Proofs of Fundamental Properties
  • More Details
    • Alternative Definitions for Heap Predicates
  • Optional Material
    • More on the Definition of the Existential Quantifier
    • Formulation of the Extensionality Axioms
    • Historical Notes

Heap Entailment    (Himpl)

  • First Pass
    • Definition of Entailment
    • Entailment for Postconditions
    • Frame Rule for Entailment
    • Rules for Proving Entailments
    • Extracting Information from Heap Predicates
    • The xsimpl Tactic
    • The xchange Tactic
    • Identifying True and False Entailments
  • More Details
    • Proving Entailments by Hand
    • Inside the xchange Tactic
  • Optional Material
    • Proofs of Rules for Entailment
    • Historical Notes

Structural Reasoning Rules    (Triples)

  • First Pass
    • Formalized Syntax of the Programming Language
    • Formalized Semantics of the Programming Language
    • Definition of Triples
    • Structural Rules
    • Derived Structural Rules
  • More Details
    • Proof of the Consequence Rule
    • Proof of the Frame Rule
    • Proof of the Extraction Rules
    • Rule for Naming Heaps
  • Optional Material
    • An Alternative Structural Rule for Existentials
    • Small-Step Semantics
    • Equivalence Between Small-Step and Omni-Big-Step
    • Small-Step-Based Triples
    • Separation Logic Triples for Quasi-Deterministic Semantics
    • Historical Notes

Reasoning Rules for Term Constructs    (Rules)

  • First Pass
    • Rules for Term Constructors
    • Primitive Arithmetic Operations
    • Primitive Heap-Manipulating Operations
    • Program Verification using the Reasoning Rules
  • More Details
    • Triple for Terms with Same Semantics
    • The Combined Let-Frame Rule
  • Optional Material
    • Alternative Specification Style for Pure Preconditions
    • Alternative Specification Style for Result Values
    • Historical Notes

The Magic Wand and Other Operators    (Wand)

  • First Pass
    • Definition of the Operator hforall
    • Definition of the Operator hor
    • Definition of the Operator hand
    • Definition of the Magic Wand Operator: hwand
    • Definition of the Magic Wand Operator for Postconditions: qwand
    • Simplifications of Magic Wands using xsimpl
    • Summary of All the Separation Logic Operators
    • The Ramified Frame Rule
  • More Details
    • Benefits of the Ramified Frame Rule
    • Some Tempting, But False, Properties of the Magic Wand
  • Optional Material
    • Equivalence Between Alternative Definitions of the Magic Wand
    • Equivalence Results for the Magic Wand for Postconditions
    • Historical Notes

Semantics of Weakest Preconditions    (WPsem)

  • First Pass
    • Definition of Weakest Preconditions
    • Structural Rules in Weakest-Precondition Style
    • Reasoning Rules for Terms in Weakest-Precondition Style
  • More Details
    • Combined Structural Rule
  • Optional Material
    • Weakest Preconditions Derived from Triples, a First Route
    • Weakest Preconditions Derived From Triples, a Second Route
    • Equivalent Characterizations of wp
    • Texan Triples
    • Historical Notes

Weakest Precondition Generator    (WPgen)

  • First Pass
    • The Basic Structure of wpgen
    • Step 1: wpgen as a Recursive Function over Terms
    • Step 2: wpgen Reformulated to Eagerly Match on the Term
    • Step 3: wpgen Reformulated with Auxiliary Definitions
    • Step 4: wpgen Augmented with Support for Structural Rules
  • More Details
    • Definition of wpgen for Each Term Construct
    • Computing with wpgen
    • Optimizing the Readability of wpgen's Output
    • Extension of wpgen to Handle Structural Rules
    • Implementation of X-tactics
    • Reasoning about Local Functions
    • Proof Structure and Proof Automation
  • Optional Material
    • Additional Tactics xconseq and xframe
    • Evaluation of wpgen Recursively inside Local Functions
    • Historical Notes

Soundness of the Weakest Precondition Generator    (WPsound)

  • More Details
    • Definition of the Predicate formula_sound
    • Soundness for the Case of Sequences
    • Soundness for the Other Term Constructs
    • Soundness of the Predicate Transformer mkstruct
    • Lemmas Capturing Properties of Iterated Substitutions
    • Main Induction for the Soundness Proof of wpgen
    • Statement of Soundness of wpgen for Closed Terms
  • Optional Material
    • Proofs of Properties of Iterated Substitution

Affine Separation Logic    (Affine)

  • First Pass
    • Motivation for the Discard Rule
    • Statement of The Discard Rule
    • Fine-grained Control of Collectable Predicates
    • The Affine-Top Heap Predicate: \GC
    • Example Instantiations of heap_affine
    • Definition of a Partially Affine Separation Logic
  • More Details
    • Discard Rules in WP Style
    • Revised Definition of mkstruct
    • The Tactic xaffine and the Behavior of xsimpl on \GC
    • Tactics for Applying the Discard Rules
  • Optional Material
    • Alternative Statement for Distribution of haffine on Quantifiers
    • Deriving the Rule GC-Post from the Rule GC-Pre
    • Historical Notes

Reasoning about Arrays    (Arrays)

  • First Pass
    • Large-Footprint Specifications for Array Operations
    • Small-Footprint Specifications for Array Operations
    • Heap Predicate for Array Segments
    • Derived Segment-Based Specifications for Array Operations
    • Verification of the Safety of QuickSort
  • More Details
    • Formalization of Sorted Lists
    • Formalization of Arrays of Integer Values
    • Functional Correctness of Quicksort
    • Realization of hheader and hcell
    • Realization of hseg and harray
    • Focus Lemmas for Array Segments
  • Optional Material
    • Semantics of Pointer Arithmetic
    • Semantics of Low-Level Block Allocation
    • Low-Level Implementation of Arrays
    • Verification of Low-Level Operations for Arrays
  • Appendix
    • Verification of the Pivot Function

Reasoning about Records    (Records)

  • First Pass
    • Representation of Individual Record Fields
    • Representation of Sets of Fields
    • Representation of Records
    • Reasoning about Reads from Record Fields
    • Reasoning about Writes To Record Fields
    • Reasoning about Record Allocation with Initializers
  • Optional Material
    • Implementation of Record Accesses using Pointer Arithmetic
    • Specification of Record Accesses w.r.t. hfields
    • Specification of Record Accesses w.r.t. hrecord
    • Implementation of Record Allocation without Initialization
    • Implementation of Record Allocation with Initialization
    • Extending xapp to Support Record Access Operations

Conclusion and Perspectives    (Postscript)

  • Beyond the Scope of This Course
  • 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
    • Values and Substitutions
    • Small-Step Semantics
    • Omni-Big-Step Semantics of primitive operations
    • Omni-Big-Step Semantics
  • Heap Predicates
    • Hprop and Entailment
    • Definition of Heap Predicates
    • Basic Properties of Separation Logic Operators
    • Properties of haffine
  • Reasoning Rules
    • Definition of Separation Logic Triples.
    • Soundness of Triples w.r.t. the Small-Step Semantics
    • Structural Properties of the eval Predicate
    • Structural Rules
    • Rules for Terms
    • Rules for Heap-Manipulating Primitive Operations
    • Rules for Other Primitive Operations
  • 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
    • Additional Tooling for xapp
    • Notations for Triples and wpgen
    • Notation for Concrete Terms
    • Scopes, Coercions and Notations for Concrete Programs
  • Additional Separation Logic Operators
    • Disjunction: Definition and Properties of hor
    • Conjunction: Definition and Properties of hand
  • Generalization to N-ary Functions
    • Smart Constructors for N-ary Functions and Applications
    • Evaluation Rules for N-ary Constructs
    • Tooling for N-ary Functions and Applications
    • Implementation of the Tactic xwp
    • Specification of Array Operations
    • Specification of Record Operations
  • Demo Programs

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
    • Domain
    • Disjoint and Domain
    • Disjointness
    • Union
    • Compatibility
    • 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
    • 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 Tactic for 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
    • Definition of Omni-Big-Step 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
  • Separation Logic
    • Definition of Separation Logic triples
    • Key Properties of Omni-Big-Step Semantics
    • Structural Rules
    • Reasoning Rules for Terms
    • Specification of Primitive Operations
  • Bonus: Example Proof