Completeness of Iris-Based Program Logics

external page Johannes Hostert, external page Zichen Zhang, external page Puming Liu, external page Simon Oddershede Gregersen, external page Ralf Jung, external page Joseph Tassarotti

Theorem 17 and Condition 18 from the paper, showing the condition at the heart of the completeness proof. — Condition 18, which is sufficient for completeness.

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 have had a proof of completeness. 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.