Approximate Relational Reasoning for Higher-Order Probabilistic Programs

TL;DR

Approxis introduces a novel higher-order approximate relational separation logic for RandML, enabling modular reasoning about approximate equivalences in probabilistic programs by treating error as a separable resource. It unifies approximate coupling rules, many-to-one and fragmented couplings, and an error amplification mechanism to derive both approximate and exact contextual equivalences, even for higher-order stateful programs. The authors validate Approxis through case studies such as the PRP/PRF switching lemma, IND$-CPA security, and rejection sampling on B+ trees, all mechanized in Coq atop Iris. The semantic model plus soundness result show that refinement judgements yield actual ε-equivalences of program executions, providing a robust framework for cryptographic security proofs and beyond. This work lays the groundwork for scalable, modular verification of security properties in expressive probabilistic languages and points to future extensions in concurrency, time-analysis, and differential privacy.

Abstract

Properties such as provable security and correctness for randomized programs are naturally expressed relationally as approximate equivalences. As a result, a number of relational program logics have been developed to reason about such approximate equivalences of probabilistic programs. However, existing approximate relational logics are mostly restricted to first-order programs without general state. In this paper we develop Approxis, a higher-order approximate relational separation logic for reasoning about approximate equivalence of programs written in an expressive ML-like language with discrete probabilistic sampling, higher-order functions, and higher-order state. The Approxis logic recasts the concept of error credits in the relational setting to reason about relational approximation, which allows for expressive notions of modularity and composition, a range of new approximate relational rules, and an internalization of a standard limiting argument for showing exact probabilistic equivalences by approximation. We also use Approxis to develop a logical relation model that quantifies over error credits, which can be used to prove exact contextual equivalence. We demonstrate the flexibility of our approach on a range of examples, including the PRP/PRF switching lemma, IND\$-CPA security of an encryption scheme, and a collection of rejection samplers. All of the results have been mechanized in the Coq proof assistant and the Iris separation logic framework.

Figures (5)

• Figure 1: Example implementation of idealized RF and RP, parameterized by $N = |\mathsf{dom}\,\mathsf{irf}| = |\mathsf{dom}\,\mathsf{irp}|$.
• Figure 2: A selection of the deterministic program-logic rules of Approxis.
• Figure 3: A selection of program-logic rules of Approxis for the probabilistic operations.
• Figure 4: Inductive definition of the specification-coupling precondition $\mathsf{scpl} \sigma \precsim_{\varepsilon} \rho \left\{\Phi\right\}$.
• Figure 5: Standard weakest-precondition rules.

Theorems & Definitions (21)

• Lemma 2.1: PRP/PRF Switching Lemma
• Lemma 2.2: Weak PRP/PRF Switching Lemma
• Lemma 2.3
• Definition 3.1: Distribution
• Lemma 3.2: Discrete Distribution Monad
• Definition 3.3: Expected value
• Definition 3.4: Approximate Coupling
• Lemma 3.5
• Corollary 3.6
• Lemma 3.7