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

TL;DR

This paper analyzes the sources of incompleteness in proof mechanisms for Separation Logic with Inductive Definitions (SLID), introduces a complete fragment within a larger logic WSL, and presents a tool to identify proof failures.

Contribution

It establishes a complete fragment of WSL for quantified entailments, relates proof failures to nonstandard models, and provides a prototype tool for automatic counter-model finding.

Findings

WSL is complete for certain quantified entailments.

Fold/unfold proof mechanism is sound and complete for theory-free, quantifier-free WSL.

The tool successfully finds counter-models in a benchmark of 700+ problems.

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.