Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A beginner guide to Iris, Coq and separation logic

Elizabeth Dietrich

TL;DR

The work addresses the challenge of safe verification for concurrent algorithms by providing a beginner-friendly guide to Iris, Coq, and separation logic, emphasizing concrete, machine-checked proofs. It offers a practical workflow that builds from Coq basics to HeapLang proofs, Iris base logic, invariants, modalities, and ghost state, anchored by case studies. Core contributions include in-depth, example-driven explanations of tactics and notations, explicit coverage of separation logic, and curated references for further learning. Overall, the guide lowers barriers to formal verification in safety-critical systems by delivering actionable methodologies and reusable proof patterns for concurrent software correctness amid complex memory ownership and invariants.

Abstract

Creating safe concurrent algorithms is challenging and error-prone. For this reason, a formal verification framework is necessary especially when those concurrent algorithms are used in safety-critical systems. The goal of this guide is to provide resources for beginners to get started in their journey of formal verification using the powerful tool Iris. The difference between this guide and many others is that it provides (i) an in-depth explanation of examples and tactics, (ii) an explicit discussion of separation logic, and (iii) a thorough coverage of Iris and Coq. References to other guides and to papers are included throughout to provide readers with resources through which to continue their learning.

A beginner guide to Iris, Coq and separation logic

TL;DR

The work addresses the challenge of safe verification for concurrent algorithms by providing a beginner-friendly guide to Iris, Coq, and separation logic, emphasizing concrete, machine-checked proofs. It offers a practical workflow that builds from Coq basics to HeapLang proofs, Iris base logic, invariants, modalities, and ghost state, anchored by case studies. Core contributions include in-depth, example-driven explanations of tactics and notations, explicit coverage of separation logic, and curated references for further learning. Overall, the guide lowers barriers to formal verification in safety-critical systems by delivering actionable methodologies and reusable proof patterns for concurrent software correctness amid complex memory ownership and invariants.

Abstract

Creating safe concurrent algorithms is challenging and error-prone. For this reason, a formal verification framework is necessary especially when those concurrent algorithms are used in safety-critical systems. The goal of this guide is to provide resources for beginners to get started in their journey of formal verification using the powerful tool Iris. The difference between this guide and many others is that it provides (i) an in-depth explanation of examples and tactics, (ii) an explicit discussion of separation logic, and (iii) a thorough coverage of Iris and Coq. References to other guides and to papers are included throughout to provide readers with resources through which to continue their learning.

Paper Structure

This paper contains 44 sections, 50 equations, 37 figures.

Table of Contents

  1. Introduction
  2. Case Studies
  3. Summary and Outline
  4. Installing the necessary software
  5. Installing Opam
  6. Installing Coq
  7. Installing Iris
  8. What is Coq
  9. Basics of proof writing
  10. Proof Mode
  11. Proof State
  12. Tactics
  13. Separation Logic
  14. Basics
  15. "Points-To" Connective
  16. ...and 29 more sections

Figures (37)

  • Figure 1: Proof that every Boolean is either true or false.
  • Figure 2: After defining the Boolean lemma, we use tactic $\textcolor{blue}{Proof}$ to start our proof. This gives us the proof state of the theorem we must now prove.
  • Figure 3: After using the tactic $\textcolor{blue}{intros}$ we need to prove $b = true \lor b = false$ and the term "b" was added to our local context.
  • Figure 4: The tactic $\textcolor{blue}{destruct b}$ splits the proof according to the two cases and takes b from our local context to show all of the possibilities of its value. This is an example of a state with two subgoals.
  • Figure 5: The grammar of Iris propositions used in this user guide.
  • ...and 32 more figures