A quantitative probabilistic relational Hoare logic

TL;DR

ERHL introduces a quantitative relational Hoare logic for probabilistic programs, enabling reasoning about relational properties via pre/post-expectations and star-couplings. It overcomes randomness-alignment constraints of prior logics (PRHL, apRHL) and achieves soundness and completeness for almost-surely terminating programs, subsuming observational equivalence, statistical distance, and differential privacy. The framework is validated through non-trivial examples (e.g., rejection sampling, randomized response) and extended to handle procedures and adversaries, including a PRF/PRP switching lemma. The work also connects ERHL to Kantorovich distances and SGD stability, providing a unified, mechanically verifiable approach with broad cryptographic and privacy-related applications.

Abstract

We introduce eRHL, a program logic for reasoning about relational expectation properties of pairs of probabilistic programs. eRHL is quantitative, i.e., its pre- and post-conditions take values in the extended non-negative reals. Thanks to its quantitative assertions, eRHL overcomes randomness alignment restrictions from prior logics, including PRHL, a popular relational program logic used to reason about security of cryptographic constructions, and apRHL, a variant of PRHL for differential privacy. As a result, eRHL is the first relational probabilistic program logic to be supported by non-trivial soundness and completeness results for all almost surely terminating programs. We show that eRHL is sound and complete with respect to program equivalence, statistical distance, and differential privacy. We also show that every PRHL judgment is valid iff it is provable in eRHL. We showcase the practical benefits of eRHL with examples that are beyond reach of PRHL and apRHL.

Figures (9)

• Figure 1: Both equivalences are not provable in , due to constraints on randomness alignment. The first equivalence relates programs that do not perform the same number of samplings. The second equivalence relates rejection sampling in $A\setminus X$ implemented as a loop with a uniform distribution over $A\setminus X$.
• Figure 2: Semantics of statements.
• Figure 3: Core rules of . Although not presented here, all depicted one-sided "left"-rules, as well as Rule \ref{['erhls:Nmod-L']} come with symmetric "right"-rules.
• Figure 4: Derived rules for practical applications.
• Figure 5: Two-sided rules of .

Theorems & Definitions (57)

• definition 1: Coupling
• proposition 1: Strassen's Theorem (Discrete Version) with Deficiency
• definition 2: $\star$-coupling
• lemma 1
• definition 3: Validity
• lemma 2
• definition 4: Semantics of Judgments
• lemma 3: Semantic Embedding of
• proof
• theorem 1: Characterisation of Judgments