Stellis: A Strategy Language for Purifying Separation Logic Entailments

TL;DR

Stellis addresses the automation gap in separation-logic entailment proofs by introducing a domain-specific strategy language to purify entailments, removing spatial predicates via pattern-guided actions. It couples a soundness-generation algorithm with a Rocq-based reduction theorem to guarantee that strategy-driven transformations preserve entailment validity, and it implements a verification workflow that outputs Rocq proofs. In evaluation on 229 entailments from linked data structures and a microkernel memory module, Stellis purifies 219 entailments (95.6%) using 5 libraries and 98 strategies, with total automation time around 0.33 seconds. The work enables reusable automation libraries, supports frame inference, and provides a principled foundation for engine-level correctness without needing to trust the purifier's implementation.

Abstract

Automatically proving separation logic entailments is a fundamental challenge in verification. While rule-based methods rely on separation logic rules (lemmas) for automation, these rule statements are insufficient for describing automation strategies, which usually involve the alignment and elimination of corresponding memory layouts in specific scenarios. To overcome this limitation, we propose Stellis, a strategy language for purifying separation logic entailments, i.e., removing all spatial formulas to reduce the entailment to a simpler pure entailment. Stellis features a powerful matching mechanism and a flexible action description, enabling the straightforward encoding of a wide range of strategies. To ensure strategy soundness, we introduce an algorithm that generates a soundness condition for each strategy, thereby reducing the soundness of each strategy to the correctness of its soundness condition. Furthermore, based on a mechanized reduction soundness theorem, our prototype implementation generates correctness proofs for the overall automation. We evaluate our system on a benchmark of 229 entailments collected from verification of standard linked data structures and the memory module of a microkernel, and the evaluation results demonstrate that, with such flexibility and convenience provided, our system is also highly effective, which automatically purifies 95.6% (219 out of 229) of the entailments using 5 libraries with 98 strategies.

Figures (5)

• Figure 1: Example strategies in Stellis
• Figure 2: The workflow of our framework
• Figure 3: Syntax of entailments. $t$ represents terms, $p$ and $s$ respectively represent pure and spatial formulas, and $E$ represents entailments.
• Figure 4: Syntax of Stellis. $\hat{f}$ extends the syntax of $f$ with pattern variables $?x$ for term binding.
• Figure 5: More example strategies in Stellis