Completeness of Iris-Based Program Logics

Traditionally, proof systems such as program logics come with two core theorems: soundness and completeness. The role of soundness is obvious: we want to be sure that arguments carried out inside the logic actually lead to correct conclusions. Completeness complements that by ensuring that the logic does not limit expressivity: in principle, any correct result can be obtained within the confines of the logic. This result typically has to be stated relative to the completeness of the assertion logic that is used to reason about pre- and postconditions.

Over the past decade, the Iris framework has emerged as a widely used foundation for building separation logics. While Iris-based logics typically come with a soundness proof, none of them come with a proof of completeness. In fact, it is not entirely clear how to translate the typical recipe for relative completeness to Iris-based logics: these logics are higher-order, which means there is no separation of assertion logic and specification logic. Furthermore, the languages these logics reason about are also typically higher-order, enabling forms of recursion that go beyond a simple while loop (e.g., Landin’s Knot). In this paper, we present the first approach for establishing completeness of Iris-based program logics, and we show the generality of our methodology by applying it to a range of different logics described in prior work, including partial and total concurrent separation logics for a higher-order ML-like language, two quantitative logics (for bounding execution time and probabilistic errors), and a relational logic for proving refinement. All our results have been mechanized in the Rocq prover.

Recommended citation: Johannes Hostert, Zichen Zhang, Puming Liu, Simon Oddershede Gregersen, Ralf Jung, and Joseph Tassarotti. 2026. Completeness of Iris-Based Program Logics. https://u8cat.github.io/files/complete.pdf
Download Paper | Download Bibtex