Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions

Neta Elad, Adithya Murali, Sharon Shoham

TL;DR

This work addresses fundamental incompleteness in Separation Logic with Inductive Definitions (SLID) by introducing Weak Separation Logic (WSL), which relaxes key semantic constraints and exposes the sources of proof failure. It identifies an effectively determined-heap (EDH) fragment of WSL and provides a complete first-order encoding that enables complete validity checking for this fragment, linking fold/unfold reasoning to FO-instantiations. The authors demonstrate soundness of fold/unfold in WSL and establish a complete framework for EDH via FO translation, while also diagnosing failures through rogue models synthesized with symbolic-structures representations. An implemented prototype translates SL entailments to FO, tests a benchmark of 700+ problems, and yields a partial taxonomy of rogue models, offering practical guidance for overcoming proof failures and improving automated reasoning for heap-manipulating programs.

Abstract

For over two decades Separation Logic has been arguably the most popular framework for reasoning about heap-manipulating programs, as well as reasoning about shared resources and permissions. Separation Logic is often extended to include inductively-defined predicates, interpreted as least fixpoints, forming Separation Logic with Inductive Definitions (SLID). Many theoretical and practical advances have been made in developing automated proof mechanisms for SLID, but these mechanisms are imperfect, and a deeper understanding of their failures is desired. As expressive as Separation Logic is, it is not surprising that it is incomplete, and in fact, it contains several sources of incompleteness that defy automated reasoning. In this paper we study these sources of incompleteness and how they relate to failures of proof mechanisms. We place SLID within a larger logic, that we call Weak Separation Logic (WSL). We prove that unlike SLID, WSL is complete for a non-trivial fragment of quantified entailments with background theories and inductive definitions, via a reduction to first-order logic (FOL). Moreover, we show that the ubiquitous fold/unfold proof mechanism is sound and complete for theory-free, quantifier-free WSL entailments with inductive definitions. Through this, we understand proof failures as stemming from nonstandard models present in WSL, but not allowed in SLID. These rogue models are typically infinite, and we use the formalism of symbolic structures to represent and automatically find them. We present a prototype tool that implements the FOL encoding of WSL and test it on an existing benchmark, which contains over 700 quantified entailment problems with inductive definitions. Our tool is able to find counter-models to many of the examples, and we provide a partial taxonomy of the rogue models, shedding some light on real-world proof failures.

Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions

TL;DR

This work addresses fundamental incompleteness in Separation Logic with Inductive Definitions (SLID) by introducing Weak Separation Logic (WSL), which relaxes key semantic constraints and exposes the sources of proof failure. It identifies an effectively determined-heap (EDH) fragment of WSL and provides a complete first-order encoding that enables complete validity checking for this fragment, linking fold/unfold reasoning to FO-instantiations. The authors demonstrate soundness of fold/unfold in WSL and establish a complete framework for EDH via FO translation, while also diagnosing failures through rogue models synthesized with symbolic-structures representations. An implemented prototype translates SL entailments to FO, tests a benchmark of 700+ problems, and yields a partial taxonomy of rogue models, offering practical guidance for overcoming proof failures and improving automated reasoning for heap-manipulating programs.

Abstract

For over two decades Separation Logic has been arguably the most popular framework for reasoning about heap-manipulating programs, as well as reasoning about shared resources and permissions. Separation Logic is often extended to include inductively-defined predicates, interpreted as least fixpoints, forming Separation Logic with Inductive Definitions (SLID). Many theoretical and practical advances have been made in developing automated proof mechanisms for SLID, but these mechanisms are imperfect, and a deeper understanding of their failures is desired. As expressive as Separation Logic is, it is not surprising that it is incomplete, and in fact, it contains several sources of incompleteness that defy automated reasoning. In this paper we study these sources of incompleteness and how they relate to failures of proof mechanisms. We place SLID within a larger logic, that we call Weak Separation Logic (WSL). We prove that unlike SLID, WSL is complete for a non-trivial fragment of quantified entailments with background theories and inductive definitions, via a reduction to first-order logic (FOL). Moreover, we show that the ubiquitous fold/unfold proof mechanism is sound and complete for theory-free, quantifier-free WSL entailments with inductive definitions. Through this, we understand proof failures as stemming from nonstandard models present in WSL, but not allowed in SLID. These rogue models are typically infinite, and we use the formalism of symbolic structures to represent and automatically find them. We present a prototype tool that implements the FOL encoding of WSL and test it on an existing benchmark, which contains over 700 quantified entailment problems with inductive definitions. Our tool is able to find counter-models to many of the examples, and we provide a partial taxonomy of the rogue models, shedding some light on real-world proof failures.

Paper Structure

This paper contains 30 sections, 13 theorems, 24 equations, 3 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Overview
  3. Fold/Unfold Proof Mechanisms
  4. Weak Separation Logic
  5. Rogue Models
  6. Preliminaries
  7. First-Order Logic
  8. A Weak Separation Logic
  9. Separation Logic with Inductive Definitions and Theories
  10. From Separation Logic to Weak Separation Logic
  11. Completeness of Effectively Determined-Heap WSL via First-Order Encoding
  12. Encoding of EDH(WSL)EDH(WSL)edh(wsl)edh(wsl) EDH(WSL) entailments in FOLFOLfolfol FOL
  13. Translation of universal, conjunctive SLSLslsl SL formulas
  14. Translation of systems of inductive definitions
  15. Fold/Unfold Proof Mechanisms: Soundness and Completeness
  16. ...and 15 more sections

Key Result

theorem 7

A WSLWSLwslwsl WSL entailment $\varphi \vdash^{\Phi}_{ WSL } \exists \bm{u}. \mathop{\bigvee}_i \psi_i$ is valid iff or, equivalently, iff is unsatisfiable (where $\Gamma^\mathcal{T}$ is the first-order axiomatization of the theory).

Figures (3)

  • Figure 1: A rogue counter-model to the entailment of \ref{['eq:lseg-ind']}, depicted both explicitly (on the left) and as a symbolic structure (on the right). Locations in the heap are shown as circles, $\mapsto$ arrows represent the points-to relation. The $\texttt{lseg}$ lines show the relevant list segments ending with $c$, others omitted to avoid clutter. Formally, the points-to relation is defined as $\curlybracs*{a \mapsto 0, c \mapsto b, b \mapsto nil} \cup \midbracs*{i \mapsto i + 1}{i \geq 0}$, and the list segment relation is defined as $\curlybracs*{ \langle*\rangle{a,a}, \langle*\rangle{a,c}, \langle*\rangle{c,c}, \langle*\rangle{c,b}, \langle*\rangle{c,nil} \langle*\rangle{b,b}, \langle*\rangle{b,nil} } \cup \midbracs*{\langle*\rangle{a,i}}{i \geq 0} \cup \midbracs*{\langle*\rangle{i,c}}{i \geq 0} \cup \midbracs*{\langle*\rangle{i,j}}{0 \leq i \leq j}$.
  • Figure 2: Recursive definition of satisfaction in Separation Logic. The $\bowtie$ symbol stands for either $=$ or $\neq$, the $\mathcal{Q}$ symbol stands for either $\forall$ or $\exists$, and $\eta = \eta_1 \uplus \eta_2$ is shorthand for $\eta = \eta_1 \cup \eta_2 \land \eta_1 \cap \eta_2 = \emptyset$.
  • Figure 3: Abstract fold/unfold is a complete proof mechanism for WSLWSLwslwsl WSL : proof structure.

Theorems & Definitions (47)

  • definition 1: Vocabulary of Separation Logic
  • definition 2: Syntax of SL formulas
  • definition 3: Heap structures
  • definition 4: Satisfaction of SL formulas
  • definition 5: System of inductive definitions
  • definition 6: Transformer for system of inductive definitions
  • definition 7: Determined-heap structure
  • definition 8: Separation Logic
  • definition 9
  • Claim 1
  • ...and 37 more