# A Quantitative Probabilistic Relational Hoare Logic

Martin Avanzini, Gilles Barthe, Davide Davoli, Benjamin Grégoire

► To cite this version:

Martin Avanzini, Gilles Barthe, Davide Davoli, Benjamin Grégoire. A Quantitative Probabilistic Relational Hoare Logic. POPL 2025 - 52nd ACM SIGPLAN Symposium on Principles of Programming Languages, Jan 2025, Denver (Colorado), United States. 10.1145/3704876. hal-04834149

HAL Id: hal-04834149

https://inria.hal.science/hal-04834149v1

Submitted on 16 Dec 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>
# A Quantitative Probabilistic Relational Hoare Logic

MARTIN AVANZINI, Centre Inria d'Université Côte d'Azur, France

GILLES BARTHE, MPI-SP, Germany and IMDEA Software Institute, Spain

DAVIDE DAVOLI, Centre Inria d'Université Côte d'Azur, France

BENJAMIN GRÉGOIRE, Centre Inria d'Université Côte d'Azur, France

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.

CCS Concepts: • Theory of computation → Program analysis.

Additional Key Words and Phrases: probabilistic programs, Hoare logic, formal verification

## ACM Reference Format:

Martin Avanzini, Gilles Barthe, Davide Davoli, and Benjamin Grégoire. 2025. A Quantitative Probabilistic Relational Hoare Logic. Proc. ACM Program. Lang. 9, POPL, Article 40 (January 2025), 29 pages. https://doi.org/10.1145/3704876

## 1 Introduction

Probabilistic Relational Hoare Logic (pRHL) [Barthe et al. 2009] is a program logic to reason about relational properties of probabilistic programs. In pRHL, judgments take the form

$$ \{R\} C \sim D \{S\}, $$

where $R, S$: Mem × Mem → {0, 1} are predicates on pairs of program memories Mem, and where C and D are programs in a probabilistic, imperative language pWhile. Informally, pRHL judgments capture that execution of the two programs C and D on $R$-related inputs yield $S$-related output distributions. The meaning of pRHL judgments can be made formal using a lifting from relations over states to relations over distributions of states. This lifting is defined formally using probabilistic couplings, a fundamental tool from stochastic processes theory and optimal transport [Levin et al. 2009; Lindvall 2002; Villani 2008]. Informally, the notion of lifting quantifies existentially over all couplings and can be used to combine two output distributions in such a way that their combination satisfies a desirable property.

Authors' Contact Information: Martin Avanzini, Centre Inria d'Université Côte d'Azur, Sophia Antipolis, France, martin.avanzini@inria.fr; Gilles Barthe, MPI-SP, Bochum, Germany, gilles.barthe@mpi-sp.org and IMDEA Software Institute, Pozuelo de Alarcon, Spain, gilles.barthe@mpi-sp.org; Davide Davoli, Centre Inria d'Université Côte d'Azur, Sophia Antipolis, France, davide.davoli@inria.fr; Benjamin Grégoire, Centre Inria d'Université Côte d'Azur, Sophia Antipolis, France, benjamin.gregoire@inria.fr.

Publication rights licensed to ACM. ACM acknowledges that this contribution was authored or co-authored by an employee, contractor or affiliate of a national government. As such, the Government retains a nonexclusive, royalty-free right to publish or reproduce this article, or to allow others to do so, for Government purposes only. Request permissions from owner/author(s).

© 2025 Copyright held by the owner/author(s). Publication rights licensed to ACM.

ACM 2475-1421/2025/1-ART40

https://doi.org/10.1145/3704876
$$ 
\begin{array}{l}
w \stackrel{\$}{\leftarrow} \{0, 1\} \times \{0, 1\} \stackrel{?}{\Rightarrow} x \stackrel{\$}{\leftarrow} \{0, 1\}; y \stackrel{\$}{\leftarrow} \{0, 1\}; w \leftarrow (x, y) \\
x \stackrel{\$}{\leftarrow} A; \text{ while } (x \in X) \text{ do } x \stackrel{\$}{\leftarrow} A \stackrel{?}{\Rightarrow} x \stackrel{\$}{\leftarrow} A \setminus X
\end{array}
$$

Fig. 1. Both equivalences are not provable in pRHL, 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$.

The coupling-based interpretation of pRHL has one major advantage: probabilistic reasoning is circumscribed to random assignments, and all reasoning about other instructions is based on Boolean-valued assertions. As a consequence, pRHL proofs can leverage practical verification techniques, including weakest verification calculus and SMT-based reasoning. pRHL and its variants are implemented in several proof tools, including CertiCrypt [Barthe et al. 2009], EasyCrypt [Barthe et al. 2011], the Foundational Cryptographic Framework [Petcher and Morrisett 2015], CryptHOL [Basin et al. 2020], and Iris [Gregersen et al. 2024; Tassarotti and Harper 2019]. These tools have been used extensively for mechanizing the security of cryptographic constructions.

In spite of its success, pRHL is incomplete, i.e. there exist semantically valid pRHL judgments that are not provable with the pRHL proof system. The main source of incompleteness is randomness alignment: loosely speaking, the pRHL proof system requires the existence of a control-flow preserving bijection between random assignments of the left and right program. As a consequence, it is generally impossible to relate programs which perform a different number of random assignments. For this reason, some tools like EasyCrypt combine pRHL with other proof techniques, notably eager/lazy sampling (which allows to move sampling around in programs) and reification (which allows to replace a code snippet by a single random assignment that samples a value from the semantics of the snippet). Yet, the combination of pRHL and these techniques remains incomplete. Completeness results for pRHL have remained elusive since its introduction more than 15 years ago.

Furthermore, the incompleteness of pRHL carries over to all its extensions for reasoning about quantitative properties. Since pRHL cannot be used to reason about quantitative relational properties, such as statistical distance, Kantorovich distance, or differential privacy [Dwork et al. 2006b], researchers have developed extensions of pRHL for specific properties. For instance, Barthe et al. [2017] introduce an extension of pRHL, called pRHLX, that produces a so-called product program that computes for every pair of inputs a coupling of the two output distributions. One can then use expectation-based program logics on the product program to obtain an upper bound on the statistical distance of the output distributions. An alternative is to use EpRHL [Barthe et al. 2018], an extension of pRHL that targets relational expectation properties. Finally, Barthe et al. [2012] use apRHL, an extension of pRHL based on approximate couplings, to reason about differential privacy. All these logics inherit the incompleteness from pRHL—and in some cases introduce further sources of incompleteness.

*Contributions.* This paper introduces eRHL, a novel program logic for reasoning about relational properties of probabilistic programs. The salient feature of eRHL is that it is a quantitative program logic, in the sense that its assertions are mappings from pairs of states to (positive extended) reals. Concretely, eRHL manipulates judgments of the form

$$ Z : \{\phi\} C \sim D \{\psi\}, $$

where Z is a type of auxiliary variables, and where $\phi, \psi : Z \to \text{Mem} \times \text{Mem} \to [0, \infty]$, the pre- and post-expectation, respectively. The validity of eRHL judgments is based on probabilistic couplings. Informally, it states that for all $z \in Z$ and memories $m_1$ and $m_2$, we have $\phi m_1 m_2 \geq \mathbb{E}_{\mu_0}[\psi z]$, where
$\mu_0$ ranges over all couplings of $[[C]]_{m_1}$ and $[[D]]_{m_2}$ (we defer the exact definition of couplings to technical sections).

eRHL is the first relational program logic for probabilistic programs that is supported by non-trivial completeness theorems for almost surely terminating (AST) programs. Concretely, we show that eRHL is sound and complete for several important properties:

- *Observational equivalence.* We show that eRHL characterizes observational equivalence. This is in contrast with pRHL, where strikingly simple examples of program equivalence cannot be proved due to randomness alignment constraints, see Figure 1.

- *Statistical distance.* We show that eRHL characterizes statistical distance between output distributions.

- *Differential privacy.* We show that eRHL captures both $\epsilon$- and $(\epsilon, \delta)$-differential privacy. This is in contrast with apRHL, where simple examples such as randomized response [Warner 1965] and privacy amplification by subsampling [Kasiviswanathan et al. 2008] cannot be proved.

- *pRHL validity.* We show that any valid pRHL judgment, stated within eRHL, can be proven. This is somewhat surprising, as validity in pRHL asserts the existence of a coupling, whereas provability of a eRHL judgment (implicitly) constructs a specific coupling. eRHL does not increase proof complexity, any existing pRHL proof can be embedded in eRHL in a natural way.

Our completeness results are established in two steps. First, we prove a completeness theorem for judgments of the form

$$Z: \{\phi\} C \sim D \{\psi_1 \oplus \psi_2\},$$

where the post-expectation can be decomposed into the “sum” of two independent expectations $\psi_1$ and $\psi_2$, depending only on the memory of C and D, respectively. This first theorem relies on two key facts: (a) quantitative assertions provide the necessary expressiveness to encode the semantics of random samplings, and therefore eliminate issues with randomness alignment; (b) validity in eRHL, formulated in terms of $\star$-couplings, does not require programs to have the same termination behavior. This eliminates the need for termination conditions in asymmetric proof rules. Second, we show that many eRHL statements are provably equivalent to a statement supported by our first completeness theorem. The existence of equivalent statements of the required form is obtained by Strassen’s theorem [Strassen 1965].

Then, we turn to adversarial computations. One main application of pRHL is reasoning about cryptography, which requires to reason about adversaries. We extend the programming language with adversary calls and introduce an adversary rule that can be viewed as a quantitative counterpart to the up-to-bad adversary rule from pRHL.

Finally, we illustrate the expressivity of eRHL with several examples that are out of scope of prior program logics, including examples of program equivalences and differential privacy. We also provide a few examples that were verified using prior logics, to showcase features of the logic not covered by the other examples.

*Comparison with [Aguirre et al. 2021; Barthe et al. 2018].* Our logic is not the first formalism to reason about quantitative properties of probabilistic programs. Prior approaches include the relational expectation logic EpRHL by [Barthe et al. 2018] and the relational pre-expectation calculus $\overline{\mathbb{R}}$ by [Aguirre et al. 2021].

The latter is designed to reason about expected sensitivity, i.e. about the expected distance between two outputs of the same program run on different inputs. $\overline{\mathbb{R}}$ computes for a single program C and a relational pre-expectation $\psi$ a pre-expectation $\phi$ such that $\phi m_1 m_2 \ge \min_{\mu_0} \mathbb{E}_{\mu_0}[\psi]$, where $\mu_0$ ranges over all couplings of $[[C]]_{m_1}$ and $[[C]]_{m_2}$. Our notion of validity generalizes their notion of validity to the case of two programs. $\overline{\mathbb{R}}$ is defined by structural induction on the command C. As already noted by [Aguirre et al. 2021], one cannot reason about expected sensitively exactly and
compositionally, because the expected sensitivity of a program *C*; *C'* cannot be established solely
from the expected sensitivity of its constituents—however, it can be over-approximated, which
guarantees soundness of $\overline{rp_e}$. More technically, the incompleteness is a consequence of the strong
constraints that $\overline{rp_e}$ imposes about randomness and control-flow alignment. When applied to an
instruction that samples from a (constant) distribution $\mu$, $\overline{rp_e}$ returns $\min_{\mu_0} \mathbb{E}_{\mu_0}[\psi]$, where $\mu_0$ ranges
over all couplings of $\mu$ with itself. When applied to a conditional instruction if *P* then *C* else *D*,
$\overline{rp_e}$ returns a pre-expectation that maps pairs of memories for which the evaluation of *P* disagree to
$\infty$. In contrast, eRHL achieves completeness (for a class of properties) by using one-sided rules to lift
randomness and control-flow alignment constraints and by carefully leveraging Strassen’s theorem.
It would be reasonably straightforward to follow the recipes laid out in our paper to incorporate
both ingredients in $\overline{rp_e}$—in fact, an extension of $\overline{rp_e}$ with one-sided rules is already discussed
in [Aguirre et al. 2021, Section 8]—and obtain a weakest relational pre-expectation calculus with
similar completeness properties as eRHL.

EpRHL [Barthe et al. 2018] is a predecessor of $\overline{rp_e}$. Their notion of validity is based on couplings, but otherwise, corresponds to ours. A minor difference is that their notion of validity compares an affine function of the expected value of the post-condition with the precondition, but said affine function is a technical artifact that does not seem to be required in applications. Contrary to $\overline{rp_e}$, EpRHL is defined by a proof system. However, the proof system only uses 2-sided rules, so EpRHL imposes similar alignment constraints as $\overline{rp_e}$.

Neither EpRHL nor $\overline{rp_e}$ considers recursive procedures and adversaries. Although it would be
possible to extend both formalisms with such constructs, some applications would also require
handling up-to-bad reasoning, thereby requiring a further extension.

*Comparison with Avanzini et al. [2024]*. Avanzini et al. [2024] defines a pre-expectation program logic for a core probabilistic with recursive procedures. Like eRHL, eHL proves upper-bounds of pre-expectation, i.e., functions taking values into extended positive reals. eRHL can be understood as a relational counterpart of eHL. Specifically, for each program construct, the rule in eHL gives rise to a corresponding one-sided and two-sided rule in eRHL. Moreover, the rule of consequence and the treatment of recursive procedures in eRHL is inspired from eHL. A main novelty of eRHL is that it embeds Strassen’s Theorem. Such an embedding is not considered in eHL, as eHL is not a relational program logic.

eHL is complete. The proof of completeness is by straightforward induction on the structure of
programs. The completeness of eHL is used implicitly in our completeness result. Specifically, there
is a derivation-preserving embedding of eHL into eRHL. Our one-sided completeness is a by-product
of the completeness of eHL and of the embedding.

*Organization of paper.* Section 2 defines the syntax and semantics of a core probabilistic language. Section 3 introduces ★-couplings and some auxiliary results. Section 4 presents eRHL and its soundness and completeness theorems. Section 5 studies connections between pRHL and eRHL— notable that eRHL is complete for pRHL judgments—provides our characterizations of total variation, differential privacy and Kantorovich-Rubenstein distances. Then, Section 6 presents extensions of the logic, noteworthy the integration of procedure and adversary calls. It also presents a proof of the PRF/PRP Switching Lemma within the logic. We conclude with related work (Section 7) and final remarks (Section 8). Some of the more involved proofs are relegated to the appendix.

## 2 Language

We consider an imperative programming *pWhile* that evolves probabilistically through the use of
sampling instructions.
**Syntax.** Let Var = {x, y, z, ...} a set of variables. The set Stmt of statements is defined by the following syntax:

$$C, D ::= \epsilon \mid x \leftarrow E \mid x \stackrel{\$}{\leftarrow} S \mid C; D \mid \text{if } P \text{ then } C \text{ else } D \mid \text{while } P \text{ do } C.$$

Here, $E \in \mathbf{Expr}$ is drawn from a set of expressions, $P \in \mathbf{BExpr}$ is a Boolean expression, and $S \in \mathbf{SExpr}$ a sampling expression. The statements are mostly standard. With $\epsilon$ we denote the empty program, that acts as a no-op. Semantically, it is the unit to sequence composition $C; D$. Syntactically, we sometimes write $C \vdash D$ if we intend to have $\epsilon$ as a unit also syntactically, that is $\epsilon \vdash C = C = C \vdash \epsilon$. The statement $x \leftarrow E$ gives the usual, deterministic assignment, whereas $x \stackrel{\$}{\leftarrow} S$ samples a value from $S$, and thereby makes the language probabilistic.

**Monadic Denotational Semantics.** Semantics of imperative statements can be given in many ways. Here, we endow the language with a denotational (monadic) style semantics, lending itself better to the proofs of soundness and completeness of our logic. Since statements are probabilistic, we interpret them as functions from states to (sub-)distributions of states, rather than as mere (partial) state transformers.

For a countable set $A$, let $\mathbf{D}A$ denote the set of (discrete) (sub-)distributions over $A$, i.e., functions $d: A \to [0, 1]$ with $|d| \triangleq \sum_{a \in A} d(a) \le 1$. We exclusively consider discrete distributions, as it suffices for our work. Distributions with $|d| = 1$ are called full distributions. The support $\text{supp}(d)$ of $d \in \mathbf{D}A$ is the set $\{a \in A \mid d(a) > 0\}$. The Dirac distribution $\delta_a$ collects all mass on $a$, i.e., $\delta_a(b) \triangleq 1$ if $a = b$ and $\delta_a(b) \triangleq 0$ otherwise. For two distributions $d_1 \in \mathbf{D}A$ and $d_2 \in \mathbf{D}B$, the product distribution $d_1 \times d_2 \in \mathbf{D}(A \times B)$ is defined by $(d_1 \times d_2)(a, b) = d_1(a) \cdot d_2(b)$ for all $a \in A$ and $b \in B$.

For an event $\mathcal{E} \subseteq A$ we denote by $\mathbb{P}_d[\mathcal{E}]$ the probability $\sum_{e \in \mathcal{E}} d(e)$. This notation extends to predicates $P: A \to \{0, 1\}$ in the natural way. Let $[0, \infty]$ denote the non-negative reals, adjoined with a top element $\infty$. For a function $f: A \to [0, \infty]$, we denote by $\mathbb{E}_d[f]$ the *expected value* $\sum_{a \in A} d(a) \cdot f(a) \in [0, \infty]$ of $f$ on $A$. Notice that when $f: A \to \{0, 1\}$, then $\mathbb{P}_d[f] = \mathbb{E}_d[f]$. We may sometimes write $\mathbb{E}_{a \leftarrow d}[e]$ rather than $\mathbb{E}_d[\lambda a. e]$.

The sub-distribution functor $\mathbf{D}$ forms a monad. The **unit** $\mathbf{unit}: A \to \mathbf{D}A$ returns on $a \in A$ the Dirac distribution $\delta_a$. The **bind** $\mathbf{dbind}: \mathbf{D}A \to (A \to \mathbf{D}B) \to \mathbf{D}B$ is defined as **dbind** $d f \triangleq \lambda b. \sum_{a \in \text{supp}(d)} d(a) \cdot f ab: \mathbf{D}B$. We may write **dlet** $a \leftarrow d$ in $f(a)$ for **dbind** $d f$. With **fail**: $\mathbf{D}A$ we denote the sub-distribution with empty support.

We model memories as mappings $m \in \text{Mem} \triangleq \text{Var} \to \text{Val}$ from variables to (a discrete set of) values $\text{Val}$. We write $m[x/v]$ for the memory obtained from $m$ by updating $x$ to $v$. We suppose that expressions $E \in \mathbf{Expr}$, Boolean expressions $P \in \mathbf{BExpr}$ and sampling expressions $S \in \mathbf{SExpr}$ are equipped with semantics $[[E]]_m: \text{Val}$, $[[P]]_m: \mathbb{B}$ and $[[S]]_m: \text{Val}$, respectively, indexed by the memory $m \in \text{Mem}$ in which these expressions are evaluated. We assume that sampling instructions are lossless, i.e. $[[S]]_m$ is a full distribution for all $m \in \text{Mem}$. The semantics of statements $[[C]]_m: \mathbf{D} \text{Mem}$ can now be defined in a standard way, see Figure 2.

**Almost sure termination.** Statements may terminate with a probability that is strictly smaller than one. We say that a statement is almost surely terminating (AST) if it terminates with probability 1 on all inputs.

## 3 Couplings

Before defining our coupling-based logic, we review the basic definition and properties of couplings. Recall that every sub-distribution $\mu \in \mathbf{D}(A_1 \times A_2)$ induces two marginals $\Pi_1(\mu) \in \mathbf{D}A_1$ and $\Pi_2(\mu) \in \mathbf{D}A_2$ satisfying the clauses $\Pi_1(\mu)(a_1) = \sum_{a_2} \mu(a_1, a_2)$ and $\Pi_2(\mu)(a_2) = \sum_{a_1} \mu(a_1, a_2)$.
<table><caption>Fig. 2. Semantics of statements.</caption><thead><tr><th>C ∈ Stmt</th><th>[[C]]<sub>m</sub></th></tr></thead><tbody><tr><td>ε</td><td>dunit m</td></tr><tr><td>x &larr; E</td><td>dunit m[x/[[E]]<sub>m</sub>]</td></tr><tr><td>x &larr; <sup>&epsilon;</sup>&#770; S</td><td>dlet v &larr; [[S]]<sub>m</sub> in dunit m[x/v]</td></tr><tr><td>C; D</td><td>dlet m' &larr; [[C]]<sub>m</sub> in [[D]]<sub>m'</sub></td></tr><tr><td>if P then C else D</td><td>sup<sub>i&isin;N</sub> [[while<sup>(i)</sup> P do C]]<sub>m</sub> where</td></tr><tr><td>while P do C</td><td>[[while<sup>(0)</sup> P do C]]<sub>m</sub> &asymp; fail</td></tr><tr><td>[[while<sup>(i+1)</sup> P do C]]<sub>m</sub> &asymp;</td><td>sup<sub>i&isin;N</sub> [[while<sup>(i)</sup> P do C]]<sub>m'</sub> if [[P]]<sub>m'</sub>,<br>dunit m otherwise.</td></tr></tbody></table>

**Definition 3.1 (Coupling).** A coupling of two sub-distributions $d_1 \in DA_1$ and $d_2 \in DA_2$ is a sub-distribution $\mu \in D(A_1 \times A_2)$ such that $\Pi_i(\mu) = d_i$ for $i = 1, 2$. We write $\mu \triangleright d_1 \& d_2$ if $\mu$ is a coupling between $d_1$ and $d_2$.

Strassen's theorem [Strassen 1965] establishes a striking equivalence between the existence of a coupling adhering to a relation $\mathcal{R}$, and a purely universal property. The following is a variation of Strassen's theorem for discrete distributions, accounting for a deficiency $\epsilon$. Strassen's original theorem is the instance with $\epsilon = 0$. Here, for a relation $\mathcal{R} \subseteq A \times B$ and $\mathcal{E} \subseteq A$, we use $\mathcal{R}(\mathcal{E}) \triangleq \{b \in B \mid \exists a \in \mathcal{E}. a \mathcal{R} b\}$ for the image of $\mathcal{E}$ under $\mathcal{R}$. For a set $\mathcal{F} \subseteq B$, we denote by $\mathcal{F}^{\mathcal{c}} \triangleq B \setminus \mathcal{F}$ its complement when $B$ is clear from context.

**PROPOSITION 3.2 (STRASSEN'S THEOREM (DISCRETE VERSION) WITH DEFICIENCY).** Let $d_1 \in DA$ and $d_2 \in DB$ be full distributions, let $\mathcal{R} \subseteq A \times B$ be a relation and let $0 \le \epsilon \le 1$. The following two statements are equivalent:

(1) there exists a coupling $\mu$ of $d_1$ and $d_2$ with $\mu(\mathcal{R}^{\mathcal{c}}) \le \epsilon$;

(2) for all $\mathcal{E} \subseteq A$, $d_1(\mathcal{E}) \le d_2(\mathcal{R}(\mathcal{E})) + \epsilon$, or equivalently, $d_1(\mathcal{E}) + d_2(\mathcal{R}(\mathcal{E})^{\mathcal{c}}) \le 1 + \epsilon$

Couplings are used to define the validity of pRHL statements. One consequence of this choice is that pRHL judgements must always relate programs that have the same probability of termination. This entails that every reasoning about one single program requires that the program is almost surely terminating. To avoid such requirements, we use an alternative notion, called $\star$-coupling, inspired from prior work on differential privacy [Barthe et al. 2019]. For a set $A$, let $A^{\star} \triangleq A \uplus \{\star\}$ and denote by $d^{\star} \in DA^{\star}$ the full distribution extending $d \in DA$ with $d^{\star}(\star) \triangleq 1 - |d|$.

**Definition 3.3 ($\star$-coupling).** A $\star$-coupling of two sub-distributions $d_1 \in DA_1$ and $d_2 \in DA_2$ is a full distribution $\mu \in D(A_1^* \times A_2^*)$ such that $\Pi_i(\mu) = d_i^*$ for $i = 1, 2$. We write $\mu \triangleright^* d_1 \& d_2$ if $\mu$ is a $\star$-coupling between $d_1$ and $d_2$.

Thus, a $\star$-coupling between $d_1$ and $d_2$ is a coupling between the extended distributions $d_1^*$ and $d_2^*$. Since $d^* = d$ whenever $d$ is a full distribution, the following is immediate.

**LEMMA 3.4.** Every coupling of full distributions $d_1$ and $d_2$ is a $\star$-coupling, and conversely.
# 4 Expectation based relational Hoare logic

We now introduce the expectation based relational Hoare logic eRHL and state our two main meta-theoretical theorems, namely soundness and the aforementioned completeness result.

Judgments. eRHL is a relational Hoare logic for reasoning about quantitative properties of probabilistic programs. As such, it generalises pre- and post-conditions to real-valued functions. Precisely, in eRHL judgments take the form

$$Z : \{\phi\} C \sim D \{\psi\},$$

where Z is a non-empty type of logical (or, auxiliary) variables, assertions $\phi, \psi: Z \to \text{Mem} \times \text{Mem} \to [0, \infty]$ are functions, the pre- and post-expectations, respectively, and C, D are statements.

**Definition 4.1 (Validity).** A judgment $Z : \{\phi\} C \sim D \{\psi\}$ is valid, written $\models Z : \{\phi\} C \sim D \{\psi\}$, if for every $z \in Z, m_1, m_2 \in \text{Mem}$,

$$\phi z(m_1, m_2) \geq \mathbb{E}_{\mu}[\psi^* z] \quad \text{for some } \mu \succcurlyeq \llbracket C \rrbracket_{m_1} \text{ & } \llbracket D \rrbracket_{m_2},$$

where $\psi^*$ is the extension of $\psi$ to a function $Z \to \text{Mem}^* \times \text{Mem}^* \to [0, \infty]$ given by

$$\psi^* z(m_1, m_2) \triangleq \begin{cases} \psi z(m_1, m_2) & \text{if } m_1, m_2 \in \text{Mem}, \\ 0 & \text{otherwise.} \end{cases}$$

Since validity is witnessed by $\star$-couplings, eRHL allows to relate programs that have different termination probabilities. Validity can be equivalently stated by directly lifting the post-expectations from memories to distributions, thereby highlighting the correspondence to the relational pre-expectation calculus $\overline{\mathbb{R}}$pe by Aguirre et al. [2021], that is defined in terms of such a lifting. Let $\psi^*: Z \to D \text{Mem} \times D \text{Mem} \to [0, \infty]$ be defined by $\psi^* z(d_1, d_2) \triangleq \inf_{\mu^* \succcurlyeq d_1 \& d_2} \mathbb{E}_{\mu}[\psi^* z]$.

**LEMMA 4.2.** *The following two statements are equivalent.*

(1) $\models Z : \{\phi\} C \sim D \{\psi\}$; and

(2) for every $z \in Z, m_1, m_2 \in \text{Mem}, \phi z(m_1, m_2) \geq \psi^* z(\llbracket C \rrbracket_{m_1}, \llbracket D \rrbracket_{m_2})$.

**Syntactic conventions.** To avoid notational overhead, we will represent assertions as real-valued expressions, using the following conventions. We use $E^{(1)}$ and $E^{(2)}$ to state that program variables occurring in expression E refer to the first and second memory supplied to the assertion, respectively. In particular, if $x \in \text{Var}$ is a program variable, then $x^{(1)}$ refer to the value of $x$ in C, and $x^{(2)}$ refers to $x$ in D. When notationally convenient, we may identify relations $\mathcal{R} \subseteq A^1 \times \dots \times A^n$ with their characteristic functions $1_{\mathcal{R}}: A^1 \times \dots \times A^n \to \{0, 1\}$, and thereby use them freely as assertions. To incorporate classical reasoning into eRHL, we use the guard operator $P \mid \phi$ as syntactic sugar for if P then $\phi$ else $\infty$. To prove validity of a judgment $Z : \{P \mid \phi\} C \sim D \{Q \mid \psi\}$ one can assume that input states are related by P, but dually, one has to establish that Q holds certainly. The type Z is usually a product type $Z = Z_1 \times \dots \times Z_n$, modelling n logical variables. In this case, we may write $z_1 \in Z_1, \dots, z_n \in Z_n : \{\phi\} C \sim D \{\psi\}$ to make the logical variables explicit. We omit Z from judgments, when not relevant.

## 4.1 Deductive system

As usual for relational logics, the deductive system underlying eRHL consists of two-sided, one-sided and logical rules. The rules are presented in Figure 3.

Two-sided rules apply to structurally equal programs. Rule [SKIP] and Rule [ASGN] directly reflect the statements' semantics within pre- and post-expectations. Rule [SAMPLE] compares two sampling instructions. The pre-expectation is computed explicitly from a coupling of the two sampling operations S and T. The next two rules deal with conditionals and loops. These rules
## Two-sided rules

$$ \begin{array}{c} \text{[SKIP]} \\ \vdash Z: \{\phi\} \epsilon \sim \epsilon \{\phi\} \\ \text{[SAMPLE]} \\ \quad \forall m_1, m_2. \mu(m_1, m_2) \triangleright [S]_{m_1} \& [T]_{m_2} \\ \vdash Z: \{\mathbb{E}_{(v_1,v_2)\leftarrow\mu}[\phi[x^{(1)}/v_1, y^{(2)}/v_2]]\} x \stackrel{\$}{\leftarrow} S \sim y \stackrel{\$}{\leftarrow} T \{\phi\} \end{array} $$

$$ \begin{array}{c} \text{[IF]} \\ \vdash Z: \{P^{(1)} \wedge Q^{(2)} | \phi\} C_1 \sim D_1 \{\psi\} \quad \vdash Z: \{\neg P^{(1)} \wedge \neg Q^{(2)} | \phi\} C_2 \sim D_2 \{\psi\} \\ \vdash Z: \{P^{(1)} \leftrightarrow Q^{(2)} | \phi\} \text{ if } P \text{ then } C_1 \text{ else } C_2 \sim \text{ if } Q \text{ then } D_1 \text{ else } D_2 \{\psi\} \end{array} $$

$$ \begin{array}{c} \text{[WHILE]} \\ \quad \vdash Z: \{P^{(1)} \wedge Q^{(2)} | \phi\} C \sim D \{P^{(1)} \leftrightarrow Q^{(2)} | \phi\} \\ \quad \vdash Z: \{P^{(1)} \leftrightarrow Q^{(2)} | \phi\} \text{ while } P \text{ do } C \sim \text{ while } Q \text{ do } \neg P^{(1)} \wedge \neg Q^{(2)} | \phi \} \end{array} $$

$$ \begin{array}{c} \text{[SEQ]} \\ \quad \vdash Z: \{\phi\} C_1 \sim D_1 \{\chi\} \quad \vdash Z: \{\chi\} C_2 \sim D_2 \{\psi\} \\ \quad \vdash Z: \{\phi\} C_1 \% C_2 \sim D_1 \% D_2 \{\psi\} \end{array} $$

## One-sided rules

$$ \begin{array}{c} \text{[ASGN-L]} \\ \vdash Z: \{\phi[x^{(1)}/E^{(1)}]\} x \leftarrow E \sim \epsilon \{\phi\} \end{array} \qquad \begin{array}{c} \text{[SAMPLE-L]} \\ \vdash Z: \{\mathbb{E}_{v \leftarrow S^{(1)}} [\phi[x^{(1)}/v]]\} x \stackrel{\$}{\leftarrow} S \sim \epsilon \{\phi\} \end{array} $$

$$ \begin{array}{c} \text{[IF-L]} \\ \vdash Z: \{P^{(1)} | \phi\} C_1 \sim \epsilon \{\psi\} \quad \vdash Z: \{\neg P^{(1)} | \phi\} C_2 \sim \epsilon \{\psi\} \\ \quad \vdash Z: \{\phi\} \text{ if } P \text{ then } C_1 \text{ else } C_2 \sim \epsilon \{\psi\} \end{array} \qquad \begin{array}{c} \text{[WHILE-L]} \\ \quad \vdash Z: \{P^{(1)} | \phi\} C \sim \epsilon \{\phi\} \\ \quad \vdash Z: \{\phi\} \text{ while } P \text{ do } C \sim \epsilon \{\neg P^{(1)} | \phi\} \end{array} $$

## Logical rules

$$ \begin{array}{c} \text{[CONSEQ]} \\ \quad \vdash Z' : \{\phi'\} C \sim D \{\psi'\} \\ \quad \forall m_1 m_2 d_1 d_2. (\forall z'. \phi' z' (m_1, m_2) \ge \inf_{\mu^*} d_1 \& d_2 \mathbb{E}_{\mu'} [\psi'^* z']) \\ \quad \Rightarrow (\forall z. \phi z (m_1, m_2) \ge \inf_{\mu^*} d_1 \& d_2 \mathbb{E}_{\mu} [\psi^* z]) \\ \quad \vdash Z : \{\phi\} C \sim D \{\psi\} \end{array} $$

$$ \begin{array}{c} \text{[NMOD-L]} \\ \quad x \notin \text{Mod}(C) \quad \vdash v \in \text{Val}, Z: \{x^{(1)} = v | \phi\} C \sim D \{\psi[x^{(1)}/v]\} \\ \quad \vdash Z: \{\phi\} C \sim D \{\psi\} \end{array} $$

$$ \begin{array}{c} \text{[STRASSEN]} \\ \quad \vdash M \subseteq \text{Mem}, z \in Z: \{1 + \phi\} C \sim D \{1_M^{(1)} + 1_{R_z(M)^c}^{(2)}\} \\ \quad \vdash z \in Z: \{\phi\} C \sim D \{1_{R_z^c}\} \quad C \text{ and } D \text{ AST} \end{array} $$

<caption>Fig. 3. Core rules of eRHL. Although not presented here, all depicted one-sided “left”-rules, as well as Rule [NMOD-L] come with symmetric “right”-rules.</caption>

are synchronous, in the sense that the compared statements evaluate in lock step. In Rule [IF], the classical pre-condition $P^{(1)} \leftrightarrow Q^{(2)}$ imposes that the evaluation of the two statements descend either both into the then-branch, or both into the else-branch. Thus, it is sufficient to compare the two branches synchronously. Similarly, Rule [WHILE] enforces that the two while-statements execute in lockstep through the classical assertion $P^{(1)} \leftrightarrow Q^{(2)}$. On the quantitative part of the assertion, the rule lifts an invariant $\phi$ on the bodies to one on the two while-statements. After completion, the rule asserts that the two guards are falsified, while in the premise, one can assume
that the two guards hold. The final two-sided rule, Rule [SEQ], deals with sequentially composed commands. It is reminiscent of the corresponding rule found in classical Hoare Logic that facilitates compositional reasoning. Through the equivalence $D = \epsilon_\flat D = D_\flat \epsilon$, it enables asynchronous reasoning through the application of one-sided rules.

Such one-sided rules, presented next in Figure 3, deal with judgments of the form

$$Z : \{\phi\} C \sim \epsilon \{\psi\}.$$

Although not explicitly shown in the Figure, symmetric rules $Z : \{\phi\} \epsilon \sim C \{\psi\}$ are also present in the logic. Here, $\chi \sim \lambda z (m_1, m_2)$. $\chi z (m_2, m_1)$ is the assertion symmetric to $\chi$. Conceptually, the one-side rules all follow their two-sided counterparts. Rules [ASGN-L] and [SAMPLE-L] explicitly compute the pre-expectation based on the post-expectation, rule [IF-L] performs case analysis on the conditional's guard, and Rule [WHILE-L] relies on an invariant on the loop's bodies.

The next set of rules, the *logical rules*, deal with proof structure. As standard in Hoare logics, also eRHL contains a *weakening rule*, or *rule of consequence*. In its simplest form, this rule permits strengthening of the post-, and weakening of the pre-expectation:

$$ \frac{\text{[WEAKEN]} \quad \phi \ge \phi' \quad \vdash Z : \{\phi'\} D \sim C \{\psi'\} \quad \psi' \ge \psi \quad \vdash Z : \{\phi\} C \sim D \{\psi\}}{} $$

Our Rule [CONSEQ] is inspired by the adaptation complete rule of Nipkow [2002]. It is more general than the usual weakening rule, and permits a change on logical variables. Adapting to our notations, Nipkow's rule for partial correctness of classical Hoare Logic reads as

$$ \frac{\vdash Z' : \{P'\} C \{Q'\} \quad \forall m m'. (\forall z'. P' z' m \Rightarrow Q' z' m') \Rightarrow (\forall z. P z m \Rightarrow Q z m') \quad \vdash Z : \{P\} C \{Q\}}{} $$

In our quantitative, relational logic, the input memory $m$ turns into a pair of input memories $m_1, m_2$, the output memory $m'$ into a pair of distributions $d_1, d_2$. The two inner implications reflect the validity of premise and conclusion, via Lemma 4.2.

Rule [NMOD-L] internalizes variables that remain constant throughout evaluation—the variables not in the set of variables Mod($C$) modified by $C^1$ as logical ones. This rule is relevant in practice as it permits deriving rules akin to the *frame rule* from separation logic, or the *rule of constancy*, in Hoare logics, as explained in a moment.

Rule [STRASSEN] incorporates Strassen's theorem with deficiency (see Proposition 3.2) into eRHL. In the rule, we denote by $\mathfrak{I}_S$ the characteristic function associated with a set $S$; $\mathcal{R}_z$ refers to a family of relations on memories, potentially parametric in $z$. The double line indicates that the rule can be applied in both directions. By the AST assumptions, the eRHL judgments witness the existence of a coupling on output distributions, thereby enabling the applications of Strassen's theorem. In the premise, corresponding to the universal statement (2) of Proposition 3.2, the set of memories $M$ is implicitly universally quantified. The conclusion, on the other hand, is a direct encoding of statement (1). The significance of this rule lies in its ability to prove an upper-bound on a relational property, in terms of an upper-bounds on sum of probability of two one-sided events.

## 4.2 Derived rules

In this section, we introduce derived rules that ease reasoning and will subsequently used in examples. Our first set of rules supports backward reasoning style akin to *weakest pre-condition (WP) reasoning*. Specifically, these rules reason on the final instruction in a sequence, and combine the rule specific to this instruction with Rule [SEQ]. As an example, Figure 4 lists a two-sided

<footnote n="1">¹ To be precise, a variable $x$ is modified by $C$ if $m x \neq m' x$ for some initial memory $m$ and final memory $m' \in \text{supp}(\mathfrak{I}_C)_m$.</footnote>
## WP-style rules for sampling instructions

$$ \frac{\mu \triangleright [S] \quad \llbracket T \rrbracket \quad \vdash Z : \{\phi\} C \sim D \{\mathbb{E}_{(v_1, v_2) \leftarrow \mu} [\psi[x^{(1)}/v_1, y^{(2)}/v_2]]\} \quad \frac{\vdash Z : \{\phi\} C; x \stackrel{\$}{\leftarrow} S \sim D; y \stackrel{\$}{\leftarrow} T \{\psi\}}{\vdash Z : \{\phi\} C; x \stackrel{\$}{\leftarrow} S \sim D \{\psi\}} \quad \frac{\vdash Z : \{\phi\} C \sim D \{\psi\}}{\vdash Z : \{\phi\} C; x \stackrel{\$}{\leftarrow} S \sim D \{\psi\}} $$

## Derived logical rules

$$ \frac{\text{[Inst]} \quad E \perp \text{Mod}(C) \cup \text{Mod}(D) \quad \vdash Z' : \{\phi\} C \sim D \{\psi\} \quad \frac{\vdash Z : \{\phi[z/E]\} C \sim D \{\psi[z/E]\}}{\vdash Z : \{\phi[z/E]\} C \sim D \{\psi[z/E]\}}}{\text{[Ctx]} \quad F[\cdot] \text{concave, non-decreasing} \quad F \perp \text{Mod}(C) \cup \text{Mod}(D) \quad \frac{\vdash Z : \{\phi\} C \sim D \{\psi\}}{\vdash Z : \{F[\phi]\} C \sim D \{F[\psi]\}}} $$

<caption>Fig. 4. Derived rules for practical applications.</caption>

Rule [WP-SAMPLE] and the left-sided Rule [WP-SAMPLE-L] for sampling instructions. Similar rules can be derived for other instructions. WP reasoning is commonly used to automate program verification. User intervention can be restricted to explicit weakening steps (e.g., applications of Rule [CONSEQ]) and the treatment of sampling instructions and while loops, where the coupling and invariant have to be supplied, respectively.

The second set of rules is made of logical rules that streamline reasoning in practice. Rule [Inst] in Figure 4 allows replacing logical variables with a constant expression E that evaluates to $z' \in Z'$, and whose logical variables are taken from Z. Rule [Ctx] allows placing assertions under a context $F[\cdot]$. It encompasses for instance a frame rule—taking $F[\cdot] = P \mid \square$ for predicate $P \perp \text{Mod}(C)$, $\text{Mod}(D)$—or the constant propagation law in pre-expectation calculi [Olmedo et al. 2016]—taking $F[\cdot] = \square + E$ where E is constant. Soundness of Rule [Ctx] is derived via Jensen's reverse inequality, which explains the side condition on $F$.<fnref n="2" />

As all of these rules are derived from the core rules from Figure 3, we may use them freely in the examples that we discuss next.

## 4.3 Examples

This section illustrates the logic at work with two examples—while simple, these examples are out of scope of prior approaches.

### 4.3.1 Two samplings vs. one sampling.
Our first example shows that eRHL does not impose random alignment constraints. As a simple instance, consider proofing equivalence of

$$ C \triangleq w \stackrel{\$}{\leftarrow} \{0, 1\} \times \{0, 1\} \quad \text{and} \quad D \triangleq x \stackrel{\$}{\leftarrow} \{0, 1\}; y \stackrel{\$}{\leftarrow} \{0, 1\}; w \leftarrow (x, y), $$

as mentioned in the introduction. As we will show in Corollary 5.4, the equivalence of C and D can be established by deriving the following judgment:

$$ \vdash z \in \{0, 1\}^2 : \{1\} C \sim D \{(z = w^{(1)}) + (z \neq w^{(2)})\}. $$

By exploiting linearity of expectation, and weakest pre-expectation reasoning on C via Rule [WP-SAMPLE-L], we reduce our goal to:

$$ \vdash z \in \{0, 1\}^2 : \{1\} \in \sim D \{\sum_{a,b \in \{0,1\}} \frac{1}{4}(z = (a,b)) + (z \neq w^{(2)})\}. $$

Reasoning similarly on D, this goal further reduces to:

$$ \vdash z \in \{0, 1\}^2 : \{1\} \in \sim D \{\sum_{a,b \in \{0,1\}} \frac{1}{4}[z = (a,b)] + \sum_{a,b \in \{0,1\}} \frac{1}{4}[z \neq (a,b)]\}. $$

<footnote n="2">² I.e., $F[p \cdot r_1 + (1-p) \cdot r_2] \ge p \cdot F[r_1] + (1-p) \cdot F[r_2]$ and $r_1 \ge r_2$ implies $F[r_1] \ge F[r_2]$.</footnote>
Now it is not difficult to see that the post-expectation sums up to 1 independently of $z \in \{0, 1\}^2$, thus the goal can be discharged with an application of Rule [SKIP].

### 4.3.2 Rejection sampling.
Next, we demonstrate a non-trivial application of eRHL in order to prove functional correctness of a simple rejection sampling algorithm

$$C_{RS} \triangleq x \stackrel{\$}{\leftarrow} A; \text{ while } x \in X \text{ do } x \stackrel{\$}{\leftarrow} A,$$

by proving it equivalent to $x \stackrel{\$}{\leftarrow} A \setminus X$, that samples the value of $x$ uniformly from $A \setminus X$. We fix $X \subset A$, thereby the reference implementation is well-defined and $C_{RS}$ is AST. Similar to before, as later justified by Corollary 5.4, we prove the equivalence by showing:

$$\vdash a \in A : \{1\} C_{RS} \sim x \stackrel{\$}{\leftarrow} X \setminus A \{(a = x^{(1)}) + (a \neq x^{(1)})\}.$$

The central proof step involves the reasoning around the loop within $C_{RS}$. As a preparatory step, we prove that it satisfies the invariant $\phi(x)$, given by

$$\phi(x) \triangleq \text{ if } x^{(1)} \notin X \text{ then } a = x^{(1)} \text{ else } \frac{a \in A \setminus X}{|A \setminus X|}.$$

Precisely, we have

$$\vdash a \in A : \{\phi(x^{(1)})\} \text{ while } x \in X \text{ do } x \stackrel{\$}{\leftarrow} A \sim \epsilon \{x^{(1)} \notin X \mid \phi(x^{(1)})\},$$

via an application of Rule [WHILE-L]. The premise $\vdash a \in A : \{x \in X \mid \phi(x)\} x \stackrel{\$}{\leftarrow} A \sim \epsilon \{\phi(x)\}$ is easily discharged via Rule [SAMPLE-L] and a weakening step, for the latter exploiting the classical pre-condition $x \in X$ and the first identity in

$$\mathbb{E}_{v \leftarrow A}[\phi(v)] = \frac{a \in A \setminus X}{|A \setminus X|} = \mathbb{E}_{v \leftarrow A \setminus X}[a = v]. \qquad (1)$$

By observing $x^{(1)} \notin X \mid \phi(x^{(1)}) \ge a = x^{(1)}$, and using the second identity in (1), the preparatory step on the loop allows us to establish

$$\vdash a \in A : \{\mathbb{E}_{v \leftarrow A \setminus X}[a = v]\} C_{RS} \sim \epsilon \{a = x^{(1)}\},$$

and consequently

$$\vdash a \in A : \{\mathbb{E}_{v \leftarrow A \setminus X}[a = v] + \mathbb{E}_{v \leftarrow A \setminus X}[a \neq v]\} C_{RS} \sim \epsilon \{(a = x^{(1)}) + \mathbb{E}_{v \leftarrow A \setminus X}[a \neq v]\},$$

by an application of Rule [CTX]. Using this as a premise to the right-sided version of Rule [WP-SAMPLE-L], we derive

$$\vdash a \in A : \{\mathbb{E}_{v \leftarrow A \setminus X}[a = v] + \mathbb{E}_{v \leftarrow A \setminus X}[a \neq v]\} C_{RS} \sim x \stackrel{\$}{\leftarrow} X \setminus A \{(a = x^{(1)}) + (a \neq x^{(2)})\}.$$

It is now sufficient to see that the pre-expectation is identical to 1.

## 4.4 Soundness and completeness

We are ready to present our two main meta-theoretical results, viz, soundness of eRHL and our completeness result.

**THEOREM 4.3 (SOUNDNESS).** *Any derivable judgment is valid, i.e.,

$$\vdash Z : \{\phi\} C \sim D \{\psi\} \Rightarrow \vdash Z : \{\phi\} C \sim D \{\psi\}.$$

Conversely, completeness (in the sense of Cook) states that every valid judgment is derivable. As for other relational Hoare logics, completeness is not obvious. Certainly, the two-sided fragment is incomplete, because two-sided rules require programs to have identical structure. A further difficulty with coupling-based logics is that the notion of validity existentially quantifies over
couplings, and thus it is not clear if the proof system can always be used to construct (implicitly) a coupling, when it exists.

In the following, we prove a partial completeness result, in three steps. We first start with a completeness result on one-sided judgments, i.e., where one of the programs is $\epsilon$. Then, we prove a limited completeness result, for a specific class of post-conditions. Finally, we use Strassen's theorem to extend this class of post-conditions to a more general class that encompasses the applications of eRHL discussed in Section 5.

*One-sided completeness.* For brevity, we present completeness for left-sided judgments. The central step behind one-sided completeness is given by the following auxiliary lemma, stating that a form of *most-general one-sided judgment* can be derived.

**LEMMA 4.4.** $\vdash Z : \{\lambda z (m_1, m_2)\} \mathbb{E}_{\llbracket C \rrbracket_{m_1} \times \llbracket D \rrbracket_{m_2}} [\phi z]$ $C \sim \epsilon \{\phi\}$, for any post-expectation $\phi$.

The lemma is provable by induction on the structure of C. One-sided completeness, as expressed by the following theorem, is now a direct consequence. Indeed, from the mentioned judgment, any valid one can be derived by one application of Rule [CONSEQ].

**THEOREM 4.5 (ONE-SIDED COMPLETENESS).** Any valid one-sided judgment is derivable, i.e.,

$$ \vdash Z : \{\phi\} C \sim \epsilon \{\beta\} \quad \Rightarrow \quad \vdash Z : \{\phi\} C \sim \epsilon \{\beta\}. $$

Dual, completeness for right-sided judgments, $Z : \{\phi\} \epsilon \sim C \{\beta\}$ can be obtained.

*A two-sided completeness result.* With Rule [SEQ], two dual one-sided judgments can always be combined to a two-sided one:

$$ \frac{\vdash Z : \{\phi\} C \sim \epsilon \{\chi\} \quad \vdash Z : \{\chi\} \epsilon \sim D \{\psi\} \qquad \vdash Z : \{\phi\} C \sim D \{\psi\}}{\text{[SEQ]}} $$

Through this observation, Lemma 4.4 can be extended to two-sided judgments as follows.

**LEMMA 4.6.** $\vdash Z : \{\lambda z (m_1, m_2)\} \mathbb{E}_{\llbracket C \rrbracket_{m_1} \times \llbracket D \rrbracket_{m_2}} [\phi z]$ $C \sim D \{\phi\}$, for any post-expectation $\phi$.

The pre-expectation is a reification of the ★-coupling implicit to the above proof, viz, the product coupling. Our main completeness result specializes the post-expectation to a combination $\phi \oplus \psi$ of two separate functions $\phi, \psi$, depending only on memories of the left and right program statement, respectively.

**THEOREM 4.7.** Let C, D be AST programs, let $\psi, \chi : Z \to \text{Mem} \to [0, \infty]$, and let $\oplus : [0, \infty] \times [0, \infty] \to [0, \infty]$ be any operator that commutes with the expectation in the following sense:

$$ \mathbb{E}_{\mu}[\phi \oplus \psi] = \mathbb{E}_{\mu}[\phi] \oplus \mathbb{E}_{\mu}[\psi]. $$

The following three statements are equivalent:

(1) $\vdash Z : \{\phi\} C \sim D \{\psi^{(1)} \oplus \chi^{(2)}\}$;

(2) $\vdash Z : \{\phi\} C \sim D \{\psi^{(1)} \oplus \chi^{(2)}\}$; and

(3) for all $z \in Z$, $m_1, m_2 \in \text{Mem}$, $\phi z (m_1, m_2) \ge \mathbb{E}_{\llbracket C \rrbracket_{m_1}}[\psi z] \oplus \mathbb{E}_{\llbracket D \rrbracket_{m_2}}[\chi z]$.

Here, the commutativity property ensures that

$$ \mathbb{E}_{\llbracket C \rrbracket_{m_1}}[\psi z] \oplus \mathbb{E}_{\llbracket D \rrbracket_{m_2}}[\chi z] = \mathbb{E}_{\llbracket C \rrbracket_{m_1}}\times\llbracket D \rrbracket_{m_2}[\psi^{(1)} \oplus \chi^{(2)}]. $$

Via this identity, the theorem is in essence an application of soundness (Theorem 4.3) (implication (1) $\Rightarrow$ (2)) and Lemma 4.6 (implication (3) $\Rightarrow$ (1)). AST is required only for the implication (2) $\Rightarrow$ (3) to hold.
<figure><img src="image_2.png" /><figcaption>Fig. 5. Two-sided rules of pRHL.</figcaption></figure>

**Discussion.** One potential drawback of our completeness theorem is that it requires to prove almost sure termination by external means, whereas it would be arguably more elegant to prove it *within* the logic. Indeed, there exist many logical formalisms to prove almost sure termination, see e.g. [McIver et al. 2018]. However, our interpretation of judgments does not lend itself to support such proofs, as it entails upper bounds rather than lower bounds on expected outcomes of the programs. Furthermore, designing practical methods for reasoning about lower bounds poses challenges of its own, see e.g. [Hark et al. 2020], which are beyond the scope of the current paper. However, as a point of comparison, we note that pRHL also requires external means to prove termination when applying one-sided rules for loops.

# 5 Applications

This section presents several applications of our results. The first result concerns completeness of eRHL w.r.t. pRHL. Second, it presents the characterisation of program equivalence within eRHL that was already used in the examples of the previous section. Finally, it presents completeness of eRHL wrt. several quantitative properties of interest: statistical distance, differential privacy, and the Kantorovich distance. All these results fundamentally rely on our completeness theorem (Theorem 4.7), and Strassen's theorem, as embodied by Rule [STRASSEN].

## 5.1 Completeness w.r.t. pRHL judgments

In pRHL, judgments take the form

$$ \{\mathcal{R}\} C \sim D \{S\}, $$

where $\mathcal{R}, S: \text{Mem} \times \text{Mem} \to \{0, 1\}$ are predicates on pairs of memories. Such a judgment asserts that on $\mathcal{R}$-related inputs, $C$ and $D$ yield $S$-related outputs. Assertions are lifted to distributions via couplings.

**Definition 5.1 (Semantics of pRHL Judgments).**

$$ \vdash_{\text{pRHL}} \{\mathcal{R}\} C \sim D \{S\} \quad \Leftrightarrow \quad [[C]]_{m_1} S^{\dagger} [[D]]_{m_2} \quad \text{for all } m_1 \mathcal{R} m_2, $$

where $d_1 S^{\dagger} d_2$ if there exists a coupling $\mu$ of $d_1$ and $d_2$ with $m_1 S m_2$ for all $(m_1, m_2) \in \text{supp}(\mu)$.

As for eRHL, pRHL consists of a set of two-sided, one-sided and logical proof rules. The two-sided rules are given in Figure 5. All the rules are based purely on Boolean reasoning, except for Rule [SAMPLE], where one has to establish a bijection on the random assignments. The remaining rules preserve this bijection alignment. They are reminiscent of the rules one expects from classical Hoare-logic, e.g., one has a compositional rule for sequential statements [SEQ], conditionals are
reasoned through case-analysis [IF], and proofs of while loops [WHILE] are facilitated through an invariant $\mathcal{R}$ on the loops body. Additional assumptions on guards enforce a synchronous control flow, but through a corresponding case rule programs with asynchronous control flow can be dealt with. As for eRHL, corresponding one-sided rules exist. An important difference is that the one-sided rule for loops imposes a termination condition:

$$ \frac{\text{[WHILE-L]} \quad \begin{array}{l} \{P^{(1)} \land \mathcal{R}\} C \sim \epsilon \{\mathcal{R}\} \quad \vdash \mathcal{R} \rightarrow \mathcal{R}_1^{(1)} \quad \mathcal{R}_1 \vdash \text{while } P \text{ do } C \text{ AST} \\ \text{\vdash}_{\text{pRHL}} \quad \{\mathcal{R}\} \text{ while } P \text{ do } C \sim \epsilon \{\neg P^{(1)} \land \mathcal{R}\} \end{array}}{\phantom{\text{[WHILE-L]}} \phantom{\vdash \mathcal{R} \rightarrow \mathcal{R}_1^{(1)}}} $$

The side-condition is essential to soundness of the rule, as the termination probability of the two programs has to coincide.

As a first step to our completeness result, we define a semantic preserving embedding of pRHL judgments into eRHL. Due to the fact that validity in eRHL is defined in terms of upper-bounds, our embedding of pRHL is defined by contra-position:

LEMMA 5.2 (SEMANTIC EMBEDDING OF pRHL).

$$ \vdash_{\text{pRHL}} \{\mathcal{R}\} C \sim D \{S\} \quad \Rightarrow \quad \vdash \{1_{\mathcal{R}^c}\} C \sim D \{1_{S^c}\}. $$

The converse holds when C and D are AST.

PROOF. For the direct implication, consider initial memories $m_1$ and $m_2$. If these are not $\mathcal{R}$-related, then any $\star$-coupling $\mu$ of the output distributions (e.g., the product $\star$-coupling) proves

$$ (1_{\mathcal{R}^c})(m_1, m_2) \geq \mathbb{E}_{\mu}[1_{S^c}^*] $$

since the right-hand side is trivially bounded by $(1_{\mathcal{R}^c})(m_1, m_2) = 1$. On the other hand, if the memories are $\mathcal{R}$-related, validity of the pRHL judgment yields a coupling $v$ of the output distributions whose support is related by $S$, i.e., $\mathbb{E}_v[1_{S^c}] = 0$. Extending this coupling, by placing the missing mass $1 - |v|$ on $(\star, \star)$, yields a $\star$-coupling $\mu$ that adheres again to the above inequality.

For the converse implication, observe that for $\mathcal{R}$-related inputs, validity of the eRHL judgment yields a $\star$-coupling $\mu$ for which $\mathbb{E}_{\mu}[1_{S^c}^*] = 0$. When C and D are AST, $\mu$ is also a coupling witnessing the validity of the pRHL judgment. $\square$

It is worth noting that under this interpretation, every pRHL rule can derived as a consequence of the corresponding eRHL rule. In this sense, eRHL constitutes a conservative extension of pRHL. Any pRHL proof can be turned, mechanically, into a corresponding eRHL proof. More interestingly, through Strassen's Theorem, every valid pRHL judgment is provable in eRHL.

THEOREM 5.3 (CHARACTERISATION OF pRHL JUDGMENTS). For AST programs C and D,

$$ \vdash_{\text{pRHL}} \{\mathcal{R}\} C \sim D \{S\} \quad \Leftrightarrow \quad \vdash \{1_{\mathcal{R}^c}\} C \sim D \{1_{S^c}\} $$

PROOF. For the direct implication, suppose $\vdash_{\text{pRHL}} \{\mathcal{R}\} C \sim D \{S\}$. Taking its semantic embedding (Lemma 5.2), an application of Strassen's theorem with deficiency (Proposition 3.2) yields

$$ \vdash M \subseteq \text{Mem} : \{1 + 1_{\mathcal{R}^c}\} C \sim D \{1_M + 1_{S(M)^c}\}. $$

This judgment falls into the fragment for which eRHL is complete (Theorem 4.7). An application of Rule [STRASSEN] yields then $\vdash \{1_{\mathcal{R}^c}\} C \sim D \{1_{S^c}\}$.

The converse implication follows more directly, using soundness (Theorem 4.3) and Lemma 5.2. $\square$
## 5.2 Program equivalence

Recall that two programs are equivalent if their semantics coincide, i.e. map identical inputs to identical output distributions.

**COROLLARY 5.4 (CHARACTERISATION OF PROGRAM EQUIVALENCE).** Let C and D be two AST programs. The following statements are equivalent:

(1) $\vdash m \in \text{Mem} : \{\mathcal{R} | 1\} C \sim D \{\lambda m (m_1, m_2) . (m = m_1) + (m \neq m_2)\}$;

(2) $[[C]]_{m_1} = [[D]]_{m_2}$ for all $m_1 \mathcal{R} m_2$.

*PROOF.* It is not difficult to reason that two full distributions $d_1$ and $d_2$ over A are equal iff

$$1 \geq \mathbb{P}_{x \leftarrow d_1} [a = x] + \mathbb{P}_{x \leftarrow d_2} [a \neq x] \text{ for all } a \in A.$$

Using that AST program statements yield full output distributions, the statement is thus a direct consequence of Theorem 4.7. □

Observe how the direct application of pRHL-completeness would require to prove a judgment that is parameterized by sets of memories, rather than a single one. The corollary can also be cast into a rule for program equivalence. Actually, the following rule is slightly more permissive, and allows reasoning about the value that two expressions take.

$$ \frac{\Gamma \vdash v \in \text{Val}, Z : \{P | 1\} C \sim D \{(E^{(1)} = v) + (F^{(2)} \neq v)\}}{\Gamma \vdash Z : \{P | 0\} C \sim D \{E^{(1)} \neq F^{(2)}\}} \quad \text{C and D AST} $$

## 5.3 Statistical distance

It is often the case that two programs are almost equivalent. In order to capture almost equivalence precisely, it is often useful to consider the statistical, or total variation distance, distance between output distributions.

*Definition 5.5 (Total Variation Distance).* The total variation distance between two full distributions of equal weight $d_1, d_2 \in DA$ is defined as

$$ \Delta_{\text{TV}}(d_1, d_2) \triangleq \sup_{\mathcal{E} \subseteq A} |d_1(\mathcal{E}) - d_2(\mathcal{E})| = \frac{1}{2} \sum_{a \in A} |d_1(a) - d_2(a)| = \inf_{\mu \succcurlyeq d_1 \& d_2} \mathbb{P}_{\mu}[\neq]. $$

The last equality is often known as the fundamental lemma of couplings. Based on this lemma, we can characterize the total variation distance between output distributions directly within eRHL.

**COROLLARY 5.6 (CHARACTERISATION OF TOTAL VARIATION).** Let C and D be two AST programs. The following are equivalent:

(1) $\vdash \{\mathcal{R} | \phi\} C \sim D \{1_{\neq}\}$; and

(2) $\Delta_{\text{TV}}([[C]]_{m_1}, [[D]]_{m_2}) \leq \phi(m_1, m_2)$ for all $m_1 \mathcal{R} m_2$.

*PROOF.* The implication (1) $\Rightarrow$ (2) follows by soundness (Theorem 4.3), and the fundamental lemma of coupling. For the converse implication, observe that by the fundamental lemma, (2) implies validity $\vdash \{\mathcal{R} | \phi\} C \sim D \{1_{\neq}\}$, and consequently

$$ \vdash \mathcal{M} \subseteq \text{Mem} : \{\mathcal{R} | 1 + \phi\} C \sim D \{1_{\mathcal{M}} + 1_{\mathcal{M}^c}\} $$

by Strassen's theorem with deficiency (Proposition 3.2). By Theorem 4.7 this valid judgment is derivable, which allows us to conclude (1) by one application of Rule [STRASSEN]. □
## 5.4 Differential privacy

Differential privacy [Dwork et al. 2006a] is a mathematically rigorous framework to design and analyze privacy-preserving statistical algorithms. The strength of differential privacy is to provide strong individual guarantees through probabilistic noise. The main idea of differential privacy is that running a program on two adjacent inputs, typically structured inputs that only differ in one item, yields two distributions that are similar w.r.t. specific notion of similarity. There exist many notions of differential privacy. In this work we adopt the original notion of $(\epsilon, \delta)$-differentially privacy:

**Definition 5.7 (Differential privacy [Dwork et al. 2006a])**. A program $C$ is $(\epsilon, \delta)$-differentially private on memories related by $\mathcal{R}$, if

$$ \forall \mathcal{E} \subseteq \text{Mem. } \mathbb{P}_{\llbracket C \rrbracket, m_1}[\mathcal{E}] \le \exp(\epsilon) \cdot \mathbb{P}_{\llbracket C \rrbracket, m_2}[\mathcal{E}] + \delta \quad \text{for all } m_1 \mathcal{R} m_2. $$

For AST programs, eRHL characterizes the set of $(\epsilon, \delta)$-differentially privacy, in the following way.

**COROLLARY 5.8 (CHARACTERISATION OF DIFFERENTIAL PRIVACY).** Let $C$ be AST. Then

$$ \vdash \mathcal{E} \subseteq \text{Mem} : \{\mathcal{R} \mid \delta + \exp(\epsilon)\} C \sim C \{1_{\mathcal{E}}^{(1)} + \exp(\epsilon) \cdot 1_{\mathcal{E}}^{(2)}\}. $$

if and only if $C$ is $(\epsilon, \delta)$-differentially private on memories related by $\mathcal{R}$.

**PROOF.** For AST $C$, $(\epsilon, \delta)$-differential privacy can be rephrased as

$$ \delta + \exp(\epsilon) \geq \mathbb{P}_{\llbracket C \rrbracket, m_1}[\mathcal{E}] + \exp(\epsilon) \cdot \mathbb{P}_{\llbracket C \rrbracket, m_2}[\mathcal{E}^c], $$

for all $\mathcal{E} \subseteq \text{Mem}$ and $\mathcal{R}$ related inputs $m_1, m_2$. The claim is thus a direct corollary to Theorem 4.7. $\square$

### 5.4.1 Example: Randomized response.
Randomized response [Warner 1965] is a simple mechanism to conduct surveys and data collection, while maintaining the privacy of individual respondents. Suppose each individual of a population has a private property and the goal of an interviewer is to measure the percentage of population that has this property. If each individual reveals to the interviewer whether it has the property or not, their privacy is compromised. In randomized response, instead, the individuals each toss a coin. Based on the output of the coin toss, an individual either reveals the information, or answer randomly to the question. Randomized response can be used to make an algorithm differentially private. As a simple example, consider

$$ C_{RR} \triangleq x \stackrel{\$}{\leftarrow} \{0,1\}; \text{ if } x = 1 \text{ then } y \stackrel{\$}{\leftarrow} \{0,1\} \text{ else } y \leftarrow b, $$

which, depending on the outcome $x$ of a tossed coin, either fills the variable $y$ with a random bit, or it stores in $y$ a private bit $b$. Privacy of $C_{RR}$ cannot be proven in apRHL. Informally, this is because apRHL features rules for basic mechanisms and rules for composing privacy budgets, but has no suitable primitive rule to reason about the kind of sampling behavior performed in $C_{RR}$.

We use eRHL to derive an $\epsilon$ for which $C_{RR}$ is $\epsilon$-differentially private. To this end, guided by Corollary 5.8, we derive

$$ \begin{align} \vdash \mathcal{E} \subseteq \{0,1\} : & \tag{†} \\ & \left\{ \begin{array}{@{}l@{}} \frac{1}{2} \cdot \mathbb{E}_{y \leftarrow \{0,1\}} [(y \in \mathcal{E}) + \exp(\epsilon) \cdot (y \notin \mathcal{E})] + \frac{1}{2} \cdot ((b^{(1)} \in \mathcal{E}) + \exp(\epsilon) \cdot (b^{(2)} \notin \mathcal{E})) \\ C_{RR} \sim C_{RR} \\ \{(y^{(1)} \in \mathcal{E}) + \exp(\epsilon) \cdot (y^{(2)} \notin \mathcal{E})\} \end{array} \right\} \notag \end{align} $$

by reasoning backward using only the two-sided rules. All sampling instructions are coupled via the identity coupling. By an application of Rule [WEAKEN],

$$ \vdash \mathcal{E} \subseteq \{0,1\} : \{\exp(\epsilon)\} C_{RR} \sim C_{RR} \{(y^{(1)} \in \mathcal{E}) + \exp(\epsilon) \cdot (y^{(2)} \notin \mathcal{E})\}. $$
follows for $\exp(\epsilon) \ge 3$, i.e., $C_{RR}$ is (log 3)-differentially private. To see this, observe that the pre-expectation in (†) is identical to

$$ \phi = \exp(\epsilon) + \frac{1}{2} \cdot \left( (1 - \exp(\epsilon)) \cdot \mathbb{E}_{y \leftarrow \{0,1\}} [y \in \mathcal{E}] + (b^{(1)} \in \mathcal{E}) - \exp(\epsilon) \cdot (b^{(2)} \in \mathcal{E}) \right). $$

The application of Rule [WEAKEN] requires $\exp(\epsilon) \ge \phi$, or equivalently,

$$ (\exp(\epsilon) - 1) \cdot \mathbb{E}_{y \leftarrow \{0,1\}} [y \in \mathcal{E}] \ge (b^{(1)} \in \mathcal{E}) - \exp(\epsilon) \cdot (b^{(2)} \in \mathcal{E}), $$

for all $\mathcal{E} \subseteq \{0, 1\}$. The only case where this inequality does not follow trivially is when $\mathcal{E}$ is a singleton set. In this case, $\mathbb{E}_{y \leftarrow \{0,1\}} [y \in \mathcal{E}] = \frac{1}{2}$, the right-hand side is at most 1, from which we infer that $\exp(\epsilon) \ge 3$ is indeed sufficient (and necessary). Note that this bound is tight [Dwork and Roth 2014].

### 5.4.2 Example: Privacy amplification by subsampling.
The subsampling mechanism is broadly employed in the design of differentially private mechanisms such as differentially private machine learning algorithms. As it does not rely on any feature of the algorithm it is applied to, it is also suitable for those applications where the target algorithm is only available as a black box.

In a nutshell, the subsampling mechanism amplifies the privacy guarantees of a differentially private algorithm $A$ by applying it to a small randomly sampled subset of records of an initial database. The effectiveness of the subsampling mechanism depends on how the subset is sampled. One of the simplest ways is to employ the so-called *Poisson Filter*. With this filter, each record in the initial dataset can be included in the final one—where the differentially private algorithm $A$ runs—with some probability $\gamma$. In our language, we can describe this construction as follows:

$$ C_A \triangleq U \stackrel{\$}{\leftarrow} \text{PoissonFilter}(|d|, \gamma); d \leftarrow d \ominus U; A $$

Here $d$ is the database, $\text{PoissonFilter}(n, \gamma)$ samples a Poisson filter with bias $\gamma$ for $n$ entries as a bitmask $U$, and $a \ominus U$ is the database obtained by masking elements with a distinguished element $\perp$ according to $U$.

Let $d_1 \le d_2$ denote that databases $d_1$ and $d_2$ coincide, up to possibly one entry set to $\perp$ in $d_1$. Based on Corollary 5.8, it can be shown that if $A$ is $(\epsilon, \delta)$-differentially private algorithm on $\leqslant$-related databases, then the subsampling amplified version $C_A$ is $(\epsilon_\gamma, \delta_\gamma)$-differentially private on $\leqslant$-related entries, for $\epsilon_\gamma \triangleq \log(1 + \gamma(\exp(\epsilon) - 1))$ and $\delta_\gamma \triangleq \delta \cdot \gamma$ [Smith 2009].

We outline the proof. Wlog. we suppose $A$ depends only on the initial database, i.e., it can be attributed a semantic $\llbracket A \rrbracket(d) : \text{D Mem}$. By an application of Lemma 4.6 on $A$ and WP-reasoning via two-sided rules, using the identity coupling on the sampling of the filter $U$, we derive

$$ \begin{array}{l} \vdash \mathcal{E} \subseteq \text{Mem}: \\ \quad \{d^{(1)} \le d^{(2)} \mid \mathbb{E}_{U \leftarrow \text{PoissonFilter}(n, \gamma)} [\mathbb{P}_{\llbracket A \rrbracket}(d^{(1)} \ominus U)] [\mathcal{E}] + \exp(\epsilon_\gamma) \cdot \mathbb{P}_{\llbracket A \rrbracket}(d^{(2)} \ominus U)] [\mathcal{E}]\} \\ C_A \sim C_A \\ \quad \{1_{\mathcal{E}}^{(1)} + \exp(\epsilon_\gamma) \cdot 1_{\mathcal{E}^c}^{(2)}\} \end{array} $$

Weakening the pre-expectation, reasoning identical to [Steinke 2022, Theorem 29] using the DP-assumption on $A$, now yields

$$ \vdash \mathcal{E} \subseteq \text{Mem} : \{d^{(1)} \le d^{(2)} \mid \gamma_\delta + \exp(\epsilon_\gamma)\} C_A \sim C_A \{1_{\mathcal{E}}^{(1)} + \exp(\epsilon_\gamma) \cdot 1_{\mathcal{E}^c}^{(2)}\}, $$

establishing our claim through Corollary 5.8. Note that the provided amplification bound is tight.

## 5.5 Kantorovich-Rubinstein distance

The Kantorovich-Rubinstein distance—also known as Wasserstein distance—measures how far two probability distributions $d_1, d_2 \in DA$ are apart, lifting a metric $\delta$ on $A$ to a metric $W_p^\delta$ on $DA$.
**Definition 5.9 (Kantorovich distance).** Let $\delta: A \times A \to [0, \infty]$ be a function. For $p \in [1, \infty)$, the Wasserstein $p$-distance between two full distributions $d_1, d_2 \in D A$ is defined as

$$W_p^{\delta}(d_1, d_2) \triangleq \inf_{\mu \succcurlyeq d_1 \& d_2} (\mathbb{E}_{(a_1, a_2) \leftarrow \mu} [\delta(a_1, a_2)^p])^{\frac{1}{p}}.$$

Notice that a direct consequence of this definition is that eRHL can prove upper bounds to the Kantorovich-Rubinstein distance between two programs, as it is stated by the following proposition.

**LEMMA 5.10.** If $\{\mathcal{R} | \phi\} C \sim D \{\delta^p\}$, then $\phi(m_1, m_2)^{\frac{1}{p}} \ge W_p^{\delta}([[C]]_{m_1}, [[D]]_{m_2})$ for all $m_1 \mathcal{R} m_2$.

While Lemma 5.10 establishes only an upper-bound, we can characterize the Kantorovich distance for the case $p = 1$ through the Kantorovich-Rubinstein duality.

**THEOREM 5.11 (KANTOROVICH-RUBINSTEIN DUALITY [KANTOROVICH AND RUBINShteIN 1958]).**
For a metric $\delta: A \times A \to [0, \infty]$,

$$W_1^{\delta}(d_1, d_2) = \inf_{\mu \succcurlyeq d_1 \& d_2} \mathbb{E}_{\mu}[\delta] = \sup_{f \in L_1} (\mathbb{E}_{d_1}[f] - \mathbb{E}_{d_2}[f]),$$

where the sup ranges over all 1-Lipschitz functions $L_1 \triangleq \{f \in \mathbb{R}^{\mathrm{Mem}} | ||f||_L \le 1\}$.

A direct consequence of Theorem 5.11 is the following sound and complete characterisation of the $W_1^{\delta}$ distance between pairs of AST programs, provided the metric is bounded.

**THEOREM 5.12 (CHARACTERISATION OF KANTOROVICH DISTANCE).** Let C and D be two AST programs. and let $\delta: \mathrm{Mem} \times \mathrm{Mem} \to [0, h]$ be a metric, where $0 \le h < \infty$. The following statements are equivalent:

(1) $\vdash f \in L_1: \{\mathcal{R} | \phi + h\} C \sim D \{f^{(1)} - f^{(2)} + h\}$; and

(2) $W_1^{\delta}([[C]]_{m_1}, [[D]]_{m_2}) \le \phi(m_1, m_2)$ for all $m_1 \mathcal{R} m_2$.

In (1), $f$ is a universally quantified 1-Lipschitz function. 1-Lipschitzness can be used in the proofs, e.g., via Rule [CONSEQ]. Note that since the difference between two applications of a 1-Lipschitz function $f$ is bounded by $h$, the post-expectation in (1) remains non-negative, independent of $f$.

**5.5.1 Example: Algorithmic stability of Stochastic Gradient Descent.** Algorithmic stability expresses the tendency of a learning mechanism to produce models that have similar performance on unseen examples and on the training dataset [Bousquet and Elisseeff 2002]. We revisit algorithmic stability of Stochastic Gradient Descent (SGD), a classic testbed for verification of relational expected properties, modeled as follows:

$$C_{SGD} \triangleq w \leftarrow w_0; t \leftarrow 0; \\ \text{while } t < T \text{ do} \\ \quad s \leftarrow S; \\ \quad g \leftarrow \nabla(\ell(s))(w); \\ \quad w \leftarrow w - \alpha_t \cdot g; \\ \quad t \leftarrow t + 1$$

This program runs on a set of examples $S \in A^n$ and “learns” a sequence of parameters $w \in \mathbb{R}^d$, repeatedly updating them in order to minimize a loss function $\ell: A \to \mathbb{R}^d \to [0, 1]$.

Hardt et al. [2016] has shown that SGD is $(\frac{2L^2}{n} \sum_{t=0}^{T-1} \alpha_t)$-uniformly stable for suitable loss-functions $\ell$ and step-sizes $\alpha_t$: for all examples $a \in A$, we have

$$|\mathbb{E}_{m \leftarrow [[C_{SGD}]]_{m_S}}[\ell(a, m(w))] - \mathbb{E}_{m \leftarrow [[C_{SGD}]]_{m_S}}[\ell(a, m(w))]| \le \frac{2L^2}{n} \sum_{t=0}^{T-1} \alpha_t,$$
where $m_S$ and $m_{S'}$ are memories storing training sets $S$ and $S'$, respectively, that differ in exactly one example, denoted by $m_S \approx_1 m_{S'}$ in the following.

Aguirre et al. [2021] have proven this statement in their pre-expectation calculus for probabilistic sensitivity. We re-cast the proof into eRHL. As a first step, a crucial observation is that the absolute distance of two expectations $|\mathbb{E}_{d_1}[f_1] - \mathbb{E}_{d_2}[f_2]|$, such as the one expressing algorithmic stability, is bounded from above itself by the Kantorovich distance $W_1^\delta$ given by the metric $\delta(a_1, a_2) = |f_1(a_1) - f_2(a_2)|$ (see e.g. [Aguirre et al. 2021, Theorem 2.4]). By Lemma 5.10, a sufficient condition for stability of $C_{SGD}$ is thus given by the eRHL judgment

$$a \in A : \{\approx_1 \frac{2L^2}{n} \sum_{t=0}^{T-1} \alpha_t\} C_{SGD} \sim C_{SGD} \{|\ell(a, w^{(1)}) - \ell(a, w^{(2)})|\}.$$

To derive this judgment, one can now proceed by reasoning identical to [Aguirre et al. 2021], using the two-sided rules of eRHL. The invariant computed in [Aguirre et al. 2021] serves essentially as an invariant in the application of Rule [WHILE].

Algorithmic stability of SGD was also established using EpRHL [Barthe et al. 2018]. In comparison to EpRHL's judgments, those of eRHL are only meant to reason about expected values, instead of reasoning about sensitivities and relational properties. This renders eRHL's proof system closer to that of apRHL and thus simpler than EpRHL's one.

# 6 Extensions of the logic

In this section, we extend our programming language and logic with recursive procedures and adversary calls, and illustrate how the resulting logic can be used to reason about cryptographic proofs. Throughout this section, we exclude Rule [STRASSEN] from the calculus. The technical reason is discussed after Theorem 6.1.

## 6.1 Procedure calls

We first consider the extension of our language with statically scoped, recursive procedures.

*Extensions of the language.* To model procedures, we introduce the set $Fun = \{f, g, ...\}$ of procedure names, and we assume that the set of variables Var is partitioned into local variables LVar and global variables GVar. Global variables should be understood as implicit input and output to procedures, while local ones are statically scoped. Because of this distinction each memory $m$ can be seen as the disjoint union of a global memory $m_g \in GMem$ with domain GVar and a local memory $m_l \in LMem$ with domain LVar. The set Stmt of statements now also includes the instruction $x \leftarrow^f E$, which executes the procedure $f$ with argument $E$ and assigns its return value to $x$. Zero or more than one argument can be passed to procedures as tuples. For simplicity, we require that $x$ is a local variable—this will simplify the rule for procedure calls in our logic—but nothing prevents us from writing $x \leftarrow^f f(E)$; $y \leftarrow x$ if we want to assign the result to a global variable $y$.

*Procedures* are declared through *procedure definition* of the form `proc f(x) C; return E`, where $x \in LVar$ is the *formal parameter*, $C \in Stmt$ the *body* and $E \in Expr$ the *return expression* of $f$. A *program* $P$ is a finite sequence of (mutually exclusive) *procedure definitions*. Throughout the following, we keep the program $P$ fixed, and we assume that it always contains the identity procedure `proc id(x) return x`, lifting the no-op statement $\epsilon$ to the level of procedures. This simplifies the treatment of one-sided judgments related to procedures.

*Semantics.* The interpretation of commands now also depends on a *procedure environment*

$$\eta : \text{Fun} \rightarrow (\text{GMem} \times \text{Val}) \rightarrow \text{D}(\text{GMem} \times \text{Val}),$$
attributing to each $f \in \text{Fun}$ its semantics $[f]_{m_g, v}^\eta \triangleq \eta f(m_g, v)$. The semantics of a procedure invocation $x \stackrel{\eta}{\leftarrow} f(E)$, evaluates $f$ on the global portion of the memory and the argument. After the execution of $f$, the global memory is updated and the return value is stored in $x$, captured in the semantics as follows:

$$[x \stackrel{\eta}{\leftarrow} f(E)]_m^\eta \triangleq \textbf{dlet} (m'_g, r) \leftarrow [f]_{m_g, [E]_m}^\eta \text{ in dunit } (m'_g \triangleright m_l[x/r]).$$

Apart from carrying a procedure environment, the semantics of statements depicted in Figure 2 remains otherwise identical.

Procedures can be mutually recursive. To formalize this, for each $n \in \mathbb{N}$ we first define procedure environments $\eta^{(n)}$ that reflect the semantics of procedures up to $n$ unfoldings of recursive calls, failing when this threshold has been reached:

$$\begin{array}{l}
\eta^{(0)} f \triangleq \lambda(m_g, v). \textbf{ fail} \\
\eta^{(n+1)} f \triangleq \lambda(m_g, v). \textbf{ dlet } m' \leftarrow ([C]_{m_g \omega m_l^0 [x/v]}^{\eta^{(n)}}) \textbf{ in dunit } (m'_g, [E]_{m'}) \\
\qquad \text{where (proc } f(x) C; return } E) \in P.
\end{array}$$

In the case $n \neq 0$, the local memory is initialized to an initial memory $m_l^0$, assigning to each variable $x \in LVar$ an (arbitrary but fixed) default value, and the formal parameter $x$ is bound by the argument. Upon completion of the procedure's body $C$, the return expression is evaluated and returned, together with the potentially modified global memory. The full semantics of a procedure are captured by letting the threshold $n$ be arbitrary large, as captured by the environment. $\eta_p \triangleq \sup_{n \in \mathbb{N}} \eta^{(n)}$ associated to $P$. As we keep $P$ fixed in the following, it is justified to abbreviate $[\cdot]_p$ by $[\cdot]$ in the following.

*Extension of eRHL.* To deal with procedures, we endow our logic with a *logical contexts* $\Gamma$, i.e., sets of auxiliary judgments of the form $Z : \{\alpha\} f \sim g \{\beta\}$ that relate pairs of procedures. Following the semantics of procedures, assertions $\alpha, \beta$ are drawn from $Z \to (\text{GMem} \times \text{Val}) \times (\text{GMem} \times \text{Val}) \to [0, \infty]$. In the pre-expectation $\alpha$, the two arguments of type $\text{GMem} \times \text{Val}$ refer to the global memory and the formal parameter of $f$ and $g$, respectively, while in the post-expectation $\beta$ they refer to the modified global memory and return value. Despite the change in type, validity is defined in line with that of ordinary judgments. Specifically, a judgment on procedures is valid, in notation $\vdash Z : \{\alpha\} f \sim g \{\beta\}$, if for every $z \in Z$, $i_1, i_2 \in \text{GMem} \times \text{Val}$,

$$\alpha z (i_1, i_2) \geq \mathbb{E}_{\mu} [\beta^* z] \text{ for some } \mu \triangleright [f]_{i_1} \& [g]_{i_2}.$$

*Procedure rules.* To support reasoning about procedure calls, all the deduction rules of eRHL are extended to carry an additional logical context $\Gamma$, e.g. the rule for sequencing statements takes now the form:

$$\frac{\frac{\begin{array}{l}
\text{[SEQ]} \\
\Gamma \vdash Z : \{\phi\} C_1 \sim D_1 \{\chi\} \quad \Gamma \vdash Z : \{\chi\} C_2 \sim D_2 \{\psi\} \\
\hline
\Gamma \vdash Z : \{\phi\} C_1 \ddagger C_2 \sim D_1 \ddagger D_2 \{\psi\}
\end{array}}{\text{[Call]} \quad \text{Rule [Call]} \quad \text{is the two-sided rule for procedure calls, lifting the auxiliary judgment } Z : \{\alpha\} f \sim g \{\beta\} \text{ from the logical context to a corresponding pair of calls. In the conclusion of the rule, the arguments } E \text{ and } F \text{ are supplied to the pre-expectation } \alpha, \text{ conversely, in the post-expectation } \beta \text{ the return parameters are substituted by the assigned variables } x \text{ and } y, \text{ respectively. Note that } \alpha \text{ and } \beta, \text{ parameterised by definition only on global memories, are implicitly lifted in the conclusion to functions on general memories. Rule [Call-L] follows its two-sided counterpart. Although not explicitly shown, the deductive system also includes the symmetrical version of Rule [Call-L].}}}}{\text{[Call-L]}}$$

Additional rules for procedures are in Figure 6. Rule [Call] is the two-sided rule for procedure calls, lifting the auxiliary judgment $Z : \{\alpha\} f \sim g \{\beta\}$ from the logical context to a corresponding pair of calls. In the conclusion of the rule, the arguments $E$ and $F$ are supplied to the pre-expectation $\alpha$, conversely, in the post-expectation $\beta$ the return parameters are substituted by the assigned variables $x$ and $y$, respectively. Note that $\alpha$ and $\beta$, parameterised by definition only on global memories, are implicitly lifted in the conclusion to functions on general memories. Rule [Call-L] follows its two-sided counterpart. Although not explicitly shown, the deductive system also includes the symmetrical version of Rule [Call-L].
$$ \begin{array}{l} \text{[CALL]} \\ \Gamma \vdash Z : \{\alpha[\arg^{(1)}/E^{(1)}, \arg^{(2)}/F^{(2)}]\} x \stackrel{\$}{\leftarrow} f(E) \sim y \stackrel{\$}{\leftarrow} g(F) \{\beta[\text{res}_1/x^{(1)}, \text{res}_2/y^{(2)}]\} \end{array} $$

$$ \begin{array}{l} \text{[CALL-L]} \\ \Gamma \vdash Z : \{\alpha[\arg^{(1)}/E^{(1)}, \arg^{(2)}/y^{(2)}]\} x \stackrel{\$}{\leftarrow} f(E) \sim \epsilon \{\beta[\text{res}^{(1)}/x^{(1)}, \text{res}^{(2)}/y^{(2)}]\} \end{array} $$

$$ \begin{array}{l} \text{[PROC]} \\ \text{(proc } f(x) C; \text{ return } E) \in P \qquad \text{(proc } g(x) D; \text{ return } F) \in P \\ \text{Init}_0 \triangleq \forall y \in \text{LVar. } y \neq x \Rightarrow y^{(1)} = m_l^0(x) = y^{(2)} \\ \Gamma \vdash Z : \{\text{Init}_0 | \alpha[\arg^{(1)}/x^{(1)}, \arg^{(2)}/x^{(2)}]\} C \sim D \{\beta[\text{res}^{(1)}/E^{(1)}, \text{res}^{(2)}/F^{(2)}]\} \\ \qquad \Gamma \vdash Z : \{\alpha\} f \sim g \{\beta\} \end{array} $$

$$ \begin{array}{l} \text{[PROCIND]} \\ \Delta = (Z_i : \{\alpha_i\} f_i \sim g_i \{\beta_i\})_{i=1,...,k} \\ \forall 1 \le i \le k. \Gamma \vdash Z_i : \{\alpha_i\} f_i \sim g_i \{\beta_i\} \quad \Gamma, \Delta \vdash Z : \{\phi\} C \sim D \{\psi\} \\ \qquad \Gamma \vdash Z : \{\phi\} C \sim D \{\psi\} \end{array} $$

<caption>Fig. 6. Procedure rules.</caption>

Rule [PROC] lifts an assertion relating the bodies of two procedures to a judgment on the procedures. In the pre-expectation of the premise, the classical condition reflects that upon invocation, the local memory is initialised to $m_l^0$, the substitution in the post-expectation relates the result parameter to the two return values. The rule is only interesting in combination with Rule [PROCIND], which enables inductive reasoning on procedures. This rule internalizes judgments on procedures $\Delta$ within the logical context, once all of them have been proven, via Rule [PROC].

The following theorem establishes the soundness of eRHL discussed in this section.

## THEOREM 6.1 (SOUNDNESS AND COMPLETENESS WITH PROCEDURES).

(1) Soundness: Any derivable judgment is valid, i.e.,

$$ \vdash Z : \{\phi\} C \sim D \{\psi\} \Rightarrow \vdash Z : \{\phi\} C \sim D \{\psi\}. $$

(2) Completeness: Any valid judgment in the form mentioned in Theorem 4.7 is derivable, i.e.,

$$ \vdash Z : \{\phi\} C \sim D \{\psi^{(1)} \oplus \chi^{(2)}\} \Rightarrow \vdash Z : \{\phi\} C \sim D \{\psi^{(1)} \oplus \chi^{(2)}\}. $$

The proof of soundness in the presence of recursive procedures is significantly more involved. It proceeds in two steps. First, we establish soundness wrt. approximated semantics, permitting recursion up-to depth $n \in \mathbb{N}$. This intermediate result, proven by induction on $n$ and side-induction on the structure of the derivation of the judgment, allows us to take care of by Rule [PROCIND], embodying inductive reasoning within eRHL. In effect, this first step yields a family of ★-couplings $(\mu_n)_{n \in \mathbb{N}}$ that witness validity of the derived judgment under approximated semantics $[\cdot, \cdot]^{\eta^{(n)}}$. As a second step, we then show that this sequence of ★-couplings converges, in a certain sense, to a ★-coupling $\mu$ that witnesses validity of the derived judgment under full semantics.

Alas, the first step fails for Rule [STRASSEN], due to the AST side-conditions, inherited from Strassen's theorem (Proposition 3.2). Since AST does not extend to the approximated semantics—an AST program may fail to evaluate to a full distribution under approximated semantics when the
recursion threshold *n* is reached—Strassen’s theorem cannot be applied. This does not mean that Rule [STRASSEN] is unsound, in general, in the presence of recursive procedures. However, one has to be careful in combination with inductive proofs through Rule [PROCIND], which would require additional book-keeping and thereby complicate the logic. As Rule [STRASSEN] is not strictly necessary for our completeness results—Strassen’s theorem can always be applied at the level of validity—we refrained from including the rules in the logic extended to procedures.

The completeness result can be proven following the outline given in Section 4.4, through one-sided completeness. Crucial, most-general (one-sided) judgments (Lemma 4.4) remain derivable under a most-general, one-sided logical context Γ. As the judgments in Γ are themselves derivable, Lemma 4.4 is recovered by one application of Rule [PROCIND]. From there, the proof proceeds identical to the fragment without procedures.

## 6.2 Adversaries

In this section, we consider an extension of our language and logic with adversary calls, i.e., invocations to arbitrary procedures that have access to global variables and an oracle.

*Extension of the language.* To extend the language, we permit *adversary calls* $x \leftarrow \mathcal{A}_f(E)$, where $\mathcal{A}$ is drawn from a set $\text{Adv} = \{\mathcal{A}, \mathcal{B}, \dots \}$ of *adversary names*. Each adversary call is parameterised by an *oracle*, i.e., a pre-defined procedure $f \in \text{Fun}$, accessible to $\mathcal{A}$ via a dedicated variable $\text{orcl}$.<fnref n="3" /> Adversaries $\mathcal{A}$ refer to arbitrary procedures, granted access to a subset $\text{GVar}_{\mathcal{A}} \subseteq \text{GVar}$ of global variables which are all read-only, except for a distinguished set of *writable variables* $\text{Write}_{\mathcal{A}} \subseteq \text{GVar}_{\mathcal{A}}$.

*Semantics.* To model adversarial code in the semantics, we index the interpretation of program statements by a second environment, the *adversary environment* $\zeta$. This environments maps each $\mathcal{A} \in \text{Adv}$ to a declaration

$$ \zeta \mathcal{A} = \text{proc} \mathcal{A}(x) C; \text{return } E. $$

Procedure calls in the body *C* are confined to *oracle calls* $x \stackrel{\zeta}{\rightleftharpoons} \text{orcl}(E)$, the oracle itself is determined at invocation time of the adversary. We require that adversary environments are consistent with accessible and writable variables, i.e., the body *C*—except during the invocation of the oracle— accesses only variables in $\text{GMem}_{\mathcal{A}}$, and modifies only those within $\text{Write}_{\mathcal{A}}$. For instance, if the adversary executes an instruction $x \leftarrow E$, then $x \in \text{Write}_{\mathcal{A}}$ and *E* mentions only variables in $\text{GMem}_{\mathcal{A}}$. Notice that the memory content of a global variable $x \notin \text{Write}_{\mathcal{A}}$ may change during an invocation of $\mathcal{A}_f$, precisely when it is modified while executing the supplied oracle *f*. The semantics of an adversary $\mathcal{A}_f$ parameterised by oracle *f* now follows that of an ordinary (non-recursive) procedure, with the code taken from the adversary environment, and the oracle $\text{orcl}$ effectively set to *f*:

$$ [\mathcal{A}_f]_{m_g, v}^{\eta, \zeta} \triangleq \text{dlet } m' \leftarrow [C]_{m_g \psi m_f^0 [x/v]}^{\eta [\text{orcl}/\eta \frown], \zeta} \text{ in dunit } (m'_g, [E]_{m'}) \text{ where } \zeta \mathcal{A} = \text{proc } \mathcal{A}(x) C; \text{return } E. $$

Similar to before, we write $[\cdot]^{\zeta}$ for $[\cdot]^{\eta, \zeta}$ when $\eta = \eta_p$.

*Extension of eRHL.* To extend the logic for programs with adversarial code, the notion of judgment can remain identical, apart from the fact that program statements may now contain adversarial calls. However, judgments will now be *valid* if validity in the original sense holds *independent of* the adversarial code, that is, $\vdash Z : \{\phi\} C \sim D \{\psi\}$ states that *for all adversary environments* $\zeta$, for

<footnote n="3">³In practice, we permit $\mathcal{A}$ to be parameterised by more than one oracle. Here, the restriction helps us to avoid notational overhead.</footnote>
<figure><img src="image_3.png" /><figcaption>Fig. 7. Adversary rules.</figcaption></figure>

all $z \in Z$, $m_1, m_2 \in \text{Mem}$, there exists $\mu \triangleright \mathcal{C}[m_1]^\zeta$ & $\mathcal{D}[m_2]^\zeta$ with $\phi z(m_1, m_2) \ge \mathbb{E}_\mu[\psi^\star z]$. Similar, validity for procedure declarations is defined by quantifying over all adversary environments.

**Adversary rules.** Figure 7 gives our adversarial rules. The first rule is the one-sided rule covering the cases where the adversary is invoked on the left, a symmetric right rule also present, although not shown in the figure. The assumptions placed on $\alpha$, with $\alpha \perp V$ indicating that $\alpha$ does not depend on variables $V$,<fnref n="4" /> establish that $\alpha$ remains invariant when executing the adversary. The premise on the oracle $f$ enforces that invariance is retained when the adversary invokes $f$.

The second rule in Figure 7 covers the invocation of identical adversaries $\mathcal{A}_f$ and $\mathcal{A}_g$ parameterised by different oracles. Similar in spirit to the one-sided rule, it lifts an invariant relating the two oracles to one that relates $\mathcal{A}_f$ and $\mathcal{A}_g$. To see this more clearly, in simplified form where a designated bad event $B$ never occurs, the rule reads as

$$ \begin{array}{l@{\quad}l@{\quad}l} \alpha \perp \text{Write}_{\mathcal{A}} & \alpha \perp \{\text{arg}^{(1)}, \text{arg}^{(2)}, \text{res}^{(1)}, \text{res}^{(2)}\} & \Gamma \vdash Z : \{=_{\text{arg,GMem}_{\mathcal{A}}} | \alpha\} f \sim g \{=_{\text{res,GMem}_{\mathcal{A}}} | \alpha\} \\ \multicolumn{3}{@{}l}{\Gamma \vdash Z : \{=_{\text{arg,GMem}_{\mathcal{A}}} | \alpha\} \mathcal{A}_f \sim \mathcal{A}_g \{=_{\text{res,GMem}_{\mathcal{A}}} | \alpha\}} \end{array} $$

The predicate $=x$ is short form for $x^{(1)} = x^{(2)}$, similar $=v$ asserts that all variables in $V$ coincide this way. Its usage in the rule keeps the control flow of the two compared adversary invocations synchronised, during execution of the adversarial code and when invoking the oracle. Again, the premise on $\alpha$ enforces that $\alpha$ remains invariant when executing the adversary code. By the last premise, invariance is retained. In this simplified form, as the control flow is identical on both sides, it is justified to consider only synchronized calls to the two oracles. No one-sided assumptions are needed.

To make the logic usable in practice, the rule incorporates reasoning up-to a bad event $B$. Once this event has been reached, the control flow of the two sides are allowed to diverge. Additional one-sided premises provide an invariant $\beta$ that has to hold.

The main theorem of this section states that our adversary rules are sound.

**THEOREM 6.2 (SOUNDNESS OF ADVERSARY RULES).** The adversary rules in Figure 7 are sound.

## 6.3 Example: PRF/PRP switching lemma

The PRP/PRF switching lemma is an important cryptographic result used to show that pseudorandom functions and pseudorandom permutations are computationally indistinguishable [Bellare and Rogaway 2004]. It states that an adversary $\mathcal{A}$ can distinguish a random function from a random

<footnote n="4">⁴ Formally, for $E \in \text{Expr}$ an expression on Mem we define $E \perp V$ iff $[E]_{m_1} = [E]_{m_2}$ for all $m_1, m_2$ that may differ only on $\text{Var} \setminus V$. This notation extends naturally to assertions.</footnote>
var l;
proc prf(x)
  if |l| ≥ Q then y ← ⊥
  elsif x ∈ dom(l) then y ← l(x)
  else y ← $A$;
  l ← (x, y) :: l;
return y
proc game_prf()
  l ← [];
  x ← $\mathcal{A}_{\text{prf}}$();
  return x

var l;
proc prp(x)
  if |l| ≥ Q then y ← ⊥
  elsif x ∈ dom(l) then y ← l(x)
  else y ← $A \ \text{codom}(l)$;
  l ← (x, y) :: l;
return y
proc game_prp()
  l ← [];
  x ← $\mathcal{A}_{\text{prp}}$();
  return x

<caption>Fig. 8. Functions game_prf and game_prp model a game where an adversary $\mathcal{A}$ is meant to distinguish between a function prf and prp, implementing a random function, and permutation, respectively.</caption>

permutation over $n$ elements, using at most $Q$ oracle queries, with probability at most $\frac{Q(Q-1)}{2 \cdot n}$. The corresponding games used in a game-based cryptographic proof are given in Figure 8. The oracles prf and prp, implementing a random function and random permutation over $\mathcal{A}$, respectively, are represented internally as an associate list $l$. The two oracles differs only in the sampling instruction. They stop answering once $Q \in \mathbb{N}$ distinct queries have been performed.

The switching lemma can be proven in eRHL by proving a bound on the total variation of the two games via Corollary 5.6, precisely, we have

$$ \vdash \{\frac{Q(Q-1)}{2|A|}\} \text{game\_prp} \sim \text{game\_prf}\{\text{res}^{(1)} \neq \text{res}^{(2)}\}, $$

assuming that the adversary $\mathcal{A}$ has no access to the internal representations $l$, i.e., $\text{GVar}_{\mathcal{A}} = \emptyset$. The crux of the underlying derivation lies in the application of the adversary rule [Adv], instantiated as follows. The bad event $B$ states that a collision occurred in prf, i.e., that $l(x_1) = l(x_2)$ for some $x_1 \neq x_2$, causing prf and prp to diverge. In case of a collision, we use the invariant $\beta \triangleq 1$. Finally, the invariant $\alpha$ covering the case where no collision occurred (yet) is given by $=l | \sum_{0 \le i < Q-n^{(1)}} \frac{i+n^{(1)}}{|A|}$, for $n \triangleq |l|$ the number of distinct queries carried out so far. Since the two associated lists are initially empty, this invariant is initially identical to $\frac{Q(Q-1)}{2|A|}$, as demanded by the proof.

Under this instantiation, the two one-sided premises of rule [Adv] are easily discharged, the remaining two-sided proof obligation

$$ \vdash \{\neg B \wedge =_{\text{arg},l} \left| \sum_{0 \le i < Q-n^{(1)}} \frac{i+n^{(1)}}{|A|} \right\} \text{prf} \sim \text{prp} \{\text{if } B \text{ then } 1 \text{ else } (=_{\text{res},l} \left| \sum_{0 \le i < Q-n^{(1)}} \frac{i+|l^{(1)}|}{|A|} \right\}) \} $$

can be derived using only two-sided rules. The only non-trivial part of the proof is where the inner else branches are compared. There, one proceeds by weakest precondition reasoning. When comparing the two sampling instruction, elements from $\mathcal{A}$ on the left not in $\text{codom}(l^{(1)})$ are coupled with identical elements on the right with probability $\frac{1}{|A|}$. The total missing mass on the remaining elements is divided, with equal probability $\frac{1}{|A| \cdot |A \setminus \text{codom}(l^{(1)})|}$ on the right. Using this coupling, the final weakening step follows from simple arithmetical reasoning on pre-expectations.

The PRP/PRF lemma has been proved using multiple systems, including Clutch [Gregersen et al. 2024] and pRHL. A key difference is that the entire proof is conducted directly within eRHL, whereas previous approaches use pRHL or a variant to prove conditional equivalence, and program semantics (or a non-relational logic) to upper bound the probability of the “bad” event, i.e. the complement of the event conditioning equivalence.
# 7 Related work

Expectation-based program logics. Seminal work by Kozen [Kozen 1985] uses pre-expectations for reasoning about probabilistic programs. McIver and Morgan [2005] introduce a weakest pre-expectation calculus for reasoning about the combination of probabilities and non-determinism. Their calculus is exact, but variants of the calculus can be used to prove upper or lower bounds on expected values. Reasoning about upper or lower bounds rather than exact values eases verification. However, reasoning about lower bounds is significantly harder than reasoning about upper bounds, see e.g. [Hark et al. 2020]. In general, these works focus on positive pre-expectations, that take values in the (extended) non-negative reals. Kaminski and Katoen [2017] explore how to generalize pre-expectation calculi to mixed-signed expectations; informally, the resulting calculus internalizes a proof that the expectation of the absolute value of the pre-expectation is well-defined.

Coupling-based program logics and calculi. Barthe et al. [2009] develop the foundations of pRHL, and prove in the Coq proof assistant its soundness w.r.t. a denotational semantics of programs. Barthe et al. [2015] establishes the connection with probabilistic couplings. It follows from the embedding of pRHL into eRHL that all examples in pRHL can be encoded into eRHL.

Several works explore couplings for higher-order probabilistic languages Aguirre et al. [2018]; Gregersen et al. [2024]; Tassarotti and Harper [2019]; Vasilenko et al. [2022] develop coupling-based logics for higher-order languages. It would be interesting to explore extensions of eRHL to the higher-order setting.

BlueBell [Bao et al. 2024] is a novel program logic that combines relational and non-relational reasoning for probabilistic programs. Specifically, BlueBell features a joint conditioning modality that supports reasoning about distribution laws, probabilistic couplings and their interactions. These interactions alleviate some of the constraints on randomness alignment, and allow proving some of the simple examples that are not provable in pRHL. On the other hand, tracking precisely distribution laws of program variables is generally challenging—similar to proving lower bounds on expected values.

Coupling-based logics for differential privacy. apRHL [Barthe et al. 2012] is an extension of pRHL to reason about differential privacy. apRHL manipulates judgments of the form $\{R\} C \sim_{\epsilon, \delta} D \{S\}$, where $\epsilon > 0$ and $0 \le \delta < 1$ are the usual parameters of differential privacy. The rules are similar to those of pRHL, except that they are instrumented to track the privacy budget through the derivation. Over the years, the expressiveness of apRHL was enhanced with the introduction of additional rules [Barthe et al. 2016a,b]. These rules provide useful additional reasoning principles that could be used to verify advanced examples such as the Sparse Vector Technique. However, basic examples such as randomized response and privacy amplification remain out of scope for these extended logics. Moreover, the repeated addition of new (and at times *ad hoc*) proof rules is rather unsatisfactory both from foundational and practical perspectives. This suggests that it would be beneficial to provide a tight integration between apRHL and eRHL. Unfortunately, the interpretation of apRHL uses different notions of approximate couplings, requiring a careful analysis of existing proof rules to determine if they can be embedded in eRHL. Broadly speaking, there exist three notions of approximate couplings: 1-couplings, which are similar to usual couplings and use a single witness, 2-couplings which use two witnesses, and 0-couplings, which formulate couplings as a generalization of Strassen's theorem. 0-couplings are used for instance in [Sato 2016]; 1-couplings are used for instance in [Barthe et al. 2012]; 2-couplings are used for instance in Albarghouthi and Hsu [2018]; Barthe et al. [2019]; Barthe and Olmedo [2013]; Hsu [2017]. All rules based on 0-couplings and on the 2-witness version of ⋆-coupling from [Barthe et al. 2019; Hsu 2017] are admissible in eRHL—in the latter case, this follows from the equivalence with the
0-coupling definition proved in [Hsu 2017]. It follows that all examples in these systems, including Above Threshold, can be encoded into eRHL.

*Coupling-based logics for Kantorovich distance.* eRHL can be used to establish upper bounds on Kantorovich distance. It subsumes other approaches, like the relational pre-expectation calculus $\overline{\mathbb{R}}\mathbb{e}$ by [Aguirre et al. 2021], and the relational expectation logic EpRHL by [Barthe et al. 2018]. One major difference with $\overline{\mathbb{R}}\mathbb{e}$ is that the latter selects for each sampling instruction the coupling that minimizes the Kantorovich distance. Since the Kantorovich distance is not compositional, $\overline{\mathbb{R}}\mathbb{e}$ does not always produce tight bounds. Moreover, $\overline{\mathbb{R}}\mathbb{e}$ imposes strong constraints on randomness alignment—similar to pRHL.

*Coupling-based logics for quantum programs.* One important application of pRHL is proving security of post-quantum cryptographic constructions. With the advent of post-quantum cryptography, i.e. classical algorithms that are secure against quantum adversaries, there is a strong incentive to extend coupling-based reasoning to quantum programs. Examples of such logics have been developed in [Barbosa et al. 2021; Barthe et al. 2020b; Unruh 2019]. To our best knowledge, the completeness of these logics has not been investigated.

*Automated proofs for probabilistic programs.* There is a large body of work that develops fully automated tools for (dis)proving properties of probabilistic programs. These tools use a broad range of probabilistic tools, notably martingales, probabilistic game semantics, and are not limited to using couplings. In some restricted settings, it is possible to achieve completeness and decidability, see e.g. [Kiefer et al. 2012] for equivalence and [Barthe et al. 2020a; Chadha et al. 2023] for differential privacy. However, the majority of works aims for incomplete methods for (approximate) equivalence [Chatterjee et al. 2024], Kantorovich distance [Wang et al. 2020], and differential privacy [Bichsel et al. 2018; Ding et al. 2018].

# 8 Conclusion

eRHL is a relational program logic for expectation-based properties of probabilistic programs. eRHL subsumes many prior coupling-based logics, and is the first relational probabilistic program logic to achieve soundness and completeness for non-trivial properties, and in particular program equivalence, statistical distance, differential privacy, and Kantorovich metric. It remains an open problem whether eRHL is complete.

# Acknowledgments

This research was supported by the Agence Nationale de la Recherche (French National Research Agency) as part of the France 2030 programme (ANR-22-PECY-0006) and through the project "Probabilistic Program Semantics" (ANR-19-CE48-0014).

# References

Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Ales Bizjak, Marco Gaboardi, and Deepak Garg. 2018. Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. In *Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings (Lecture Notes in Computer Science, Vol. 10801)*, Amal Ahmed (Ed.). Springer, 214–241. https://doi.org/10.1007/978-3-319-89884-1_8

Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2021. A pre-expectation calculus for probabilistic sensitivity. *Proc. ACM Program. Lang.* 5, POPL (2021), 1–28. https://doi.org/10.1145/3434333

AWS Albarghouthi and Justin Hsu. 2018. Synthesizing coupling proofs of differential privacy. *Proc. ACM Program. Lang.* 2, POPL (2018), 58:1–58:30. https://doi.org/10.1145/3158146
Martin Avanzini, Gilles Barthe, Benjamin Grégoire, Georg Moser, and Gabriele Vanoni. 2024. Hopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security Proofs. Proc. PACMPL (2024). Issue 8 (OOPSLA).

Jialu Bao, Emanuele D'Osualdo, and Azadeh Farzan. 2024. Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning. CoRR abs/2402.18708 (2024). https://doi.org/10.48550/ARXIV.2402.18708 arXiv:2402.18708

Manuel Barbosa, Gilles Barthe, Xiong Fan, Benjamin Grégoire, Shih-Han Hung, Jonathan Katz, Pierre-Yves Strub, Xiaodi Wu, and Li Zhou. 2021. EasyPQC: Verifying Post-Quantum Cryptography. In CCS '21: 2021 ACM SIGSAC Conference on Computer and Communications Security, Virtual Event, Republic of Korea, November 15 - 19, 2021, Yongdae Kim, Jong Kim, Giovanni Vigna, and Elaine Shi (Eds.). ACM, 2564-2586. https://doi.org/10.1145/3460120.3484567

Gilles Barthe, Rohit Chadha, Vishal Jagannath, A. Prasad Sistla, and Mahesh Viswanathan. 2020a. Deciding Differential Privacy for Programs with Finite Inputs and Outputs. In LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller (Eds.). ACM, 141-154. https://doi.org/10.1145/3373718.3394796

Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, and Pierre-Yves Strub. 2015. Relational reasoning via probabilistic coupling. CoRR abs/1509.03476 (2015). arXiv:1509.03476 http://arxiv.org/abs/1509.03476

Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2018. Proving expected sensitivity of probabilistic programs. Proc. ACM Program. Lang. 2, POPL (2018), 57:1-57:29. https://doi.org/10.1145/3158145

Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, and Pierre-Yves Strub. 2019. Relational ⋆-Liftings for Differential Privacy. Log. Methods Comput. Sci. 15, 4 (2019). https://doi.org/10.23638/LMCS-15(4:18)2019

Gilles Barthe, Noémie Fong, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2016a. Advanced Probabilistic Couplings for Differential Privacy. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, Vienna, Austria, October 24-28, 2016, Edgar R. Weippl, Stefan Katzenbeisser, Christopher Kruegel, Andrew C. Myers, and Shai Halevi (Eds.). ACM, 55-67. https://doi.org/10.1145/2976749.2978391

Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2016b. Proving Differential Privacy via Probabilistic Couplings. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, Martin Grohe, Eric Koskinen, and Natarajan Shankar (Eds.). ACM, 749-758. https://doi.org/10.1145/2933575.2934554

Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, and Santiago Zanella Béguelin. 2011. Computer-Aided Security Proofs for the Working Cryptographer. In Advances in Cryptology - CRYPTO 2011 - 31st Annual Cryptology Conference, Santa Barbara, CA, USA, August 14-18, 2011. Proceedings (Lecture Notes in Computer Science, Vol. 6841), Phillip Rogaway (Ed.). Springer, 71-90. https://doi.org/10.1007/978-3-642-22792-9_5

Gilles Barthe, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2017. Coupling proofs are probabilistic product programs. Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 161-174. https://doi.org/10.1145/3009837.3009896

Gilles Barthe, Benjamin Grégoire, and Santiago Zanella Béguelin. 2009. Formal Certification of Code-based Cryptographic Proofs. 90-101. https://doi.org/10.1145/1480881.1480894

Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, and Li Zhou. 2020b. Relational proofs for quantum programs. Proc. ACM Program. Lang. 4, POPL (2020), 21:1-21:29. https://doi.org/10.1145/3371089

Gilles Barthe, Boris Köpf, Federico Olmedo, and Santiago Zanella Béguelin. 2012. Probabilistic relational reasoning for differential privacy. In Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012, John Field and Michael Hicks (Eds.). ACM, 97-110. https://doi.org/10.1145/2103656.2103670

Gilles Barthe and Federico Olmedo. 2013. Beyond Differential Privacy: Composition Theorems and Relational Logic for f-divergences between Probabilistic Programs. In Automata, Languages, and Programming - 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part II (Lecture Notes in Computer Science, Vol. 7966), Fedor V. Fomin, Rusins Freivalds, Marta Z. Kwiatkowska, and David Peleg (Eds.). Springer, 49-60. https://doi.org/10.1007/978-3-642-39212-2_8

David A. Basin, Andreas Lochbihler, and S. Reza Sefidgar. 2020. CryptHOL: Game-Based Proofs in Higher-Order Logic. J. Cryptol. 33, 2 (2020), 494-566. https://doi.org/10.1007/S00145-019-09341-Z

Mihir Bellare and Phillip Rogaway. 2004. Code-Based Game-Playing Proofs and the Security of Triple Encryption. Cryptology ePrint Archive, Paper 2004/331. https://eprint.iacr.org/2004/331

Benjamin Bichsel, Timon Gehr, Dana Drachsler-Cohen, Petar Tsankov, and Martin T. Vechev. 2018. DP-Finder: Finding Differential Privacy Violations by Sampling and Optimization. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, Toronto, ON, Canada, October 15-19, 2018, David Lie, Mohammad Mannan, Michael Backes, and XiaoFeng Wang (Eds.). ACM, 508-524. https://doi.org/10.1145/3243734.3243863

Olivier Bousquet and André Elisseeff. 2002. Stability and generalization. The Journal of Machine Learning Research 2 (2002), 499-526.

Rohit Chadha, A. Prasad Sistla, Mahesh Viswanathan, and Bishnu Bhusal. 2023. Deciding Differential Privacy of Online Algorithms with Multiple Variables. In Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications
*Security, CCS 2023, Copenhagen, Denmark, November 26-30, 2023*, Weizhi Meng, Christian Damsgaard Jensen, Cas Cremers, and Engin Kirda (Eds.). ACM, 1761–1775. https://doi.org/10.1145/3576915.3623170

Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný, and Dorde Zikelic. 2024. Equivalence and Similarity Refutation for Probabilistic Programs. *Proc. ACM Program. Lang.* 8, PLDI (2024). https://doi.org/10.48550/ARXIV.2404.03430

Zeyu Ding, Yuxin Wang, Guanhong Wang, Danfeng Zhang, and Daniel Kifer. 2018. Detecting Violations of Differential Privacy. In *Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, Toronto, ON, Canada, October 15-19, 2018*, David Lie, Mohammad Mannan, Michael Backes, and XiaoFeng Wang (Eds.). ACM, 475–489. https://doi.org/10.1145/3243734.3243818

Cynthia Dwork, Krishnaram Kenthapadi, Frank McSherry, Ilya Mironov, and Moni Naor. 2006a. Our Data, Ourselves: Privacy Via Distributed Noise Generation. In *Advances in Cryptology - EUROCRYPT 2006*, Serge Vaudenay (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 486–503.

Cynthia Dwork, Frank McSherry, Kobbi Nissim, and Adam D. Smith. 2006b. Calibrating Noise to Sensitivity in Private Data Analysis. In *Theory of Cryptography, Third Theory of Cryptography Conference, TCC 2006, New York, NY, USA, March 4-7, 2006, Proceedings (Lecture Notes in Computer Science, Vol. 3876)*, Shai Halevi and Tal Rabin (Eds.). Springer, 265–284. https://doi.org/10.1007/11681878_14

Cynthia Dwork and Aaron Roth. 2014. The Algorithmic Foundations of Differential Privacy. *Found. Trends Theor. Comput. Sci.* 9, 3-4 (2014), 211–407. https://doi.org/10.1561/040000042

Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, and Lars Birkedal. 2024. Asynchronous Probabilistic Couplings in Higher-Order Separation Logic. *Proc. ACM Program. Lang.* 8, POPL (2024), 753–784. https://doi.org/10.1145/3632868

Moritz Hardt, Benjamin Recht, and Yoram Singer. 2016. Train faster, generalize better: stability of stochastic gradient descent. In *Proceedings of the 33rd International Conference on International Conference on Machine Learning - Volume 48* (New York, NY, USA) (ICML'16). JMLR.org, 1225–1234.

Marcel Hark, Benjamin Lucien Kaminski, Jürgen Giesl, and Joost-Pieter Katoen. 2020. Aiming low is harder: induction for lower bounds in probabilistic program verification. *Proc. ACM Program. Lang.* 4, POPL (2020), 37:1–37:28. https://doi.org/10.1145/3371105

Justin Hsu. 2017. *Probabilistic Couplings for Probabilistic Reasoning*. Ph. D. Dissertation. University of Pennsylvania. http://arxiv.org/abs/1710.09951

Benjamin Lucien Kaminski and Joost-Pieter Katoen. 2017. A Weakest Pre-expectation Semantics for Mixed-sign Expectations. 1–12. https://doi.org/10.1109/LICS.2017.8005153

Leonid Vasilevich Kantorovich and SG Rubinshtein. 1958. On a space of totally additive functions. *Vestnik of the St. Petersburg University: Mathematics* 13, 7 (1958), 52–59.

Shiva Prasad Kasiviswanathan, Homin K. Lee, Kobbi Nissim, Sofya Raskhodnikova, and Adam D. Smith. 2008. What Can We Learn Privately?. In *49th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2008, October 25-28, 2008, Philadelphia, PA, USA*. IEEE Computer Society, 531–540. https://doi.org/10.1109/FOCS.2008.27

Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, and James Worrell. 2012. APEX: An Analyzer for Open Probabilistic Programs. In *Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings (Lecture Notes in Computer Science, Vol. 7358)*, P. Madhusudan and Sanjit A. Seshia (Eds.). Springer, 693–698. https://doi.org/10.1007/978-3-642-31424-7_51

Dexter Kozen. 1985. A Probabilistic PDL. *J. Comput. Syst. Sci.* 30, 2 (1985), 162 – 178. https://doi.org/10.1016/0022-0000(85)90012-1

David A. Levin, Yuval Peres, and Elizabeth L. Wilmer. 2009. *Markov chains and mixing times*. American Mathematical Society.

Torgny Lindvall. 2002. *Lectures on the coupling method*. Courier Corporation.

Annabelle McIver and Carroll Morgan. 2005. *Abstraction, refinement and proof for probabilistic systems*. Springer Science & Business Media.

Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, and Joost-Pieter Katoen. 2018. A new proof rule for almost-sure termination. *Proc. ACM Program. Lang.* 2, POPL (2018), 33:1–33:28. https://doi.org/10.1145/3158121

Tobias Nipkow. 2002. *Hoare Logics in Isabelle/HOL*. Springer Netherlands, Dordrecht, 341–367. https://doi.org/10.1007/978-94-010-0413-8_11

Federico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2016. Reasoning about Recursive Probabilistic Programs. 672–681. https://doi.org/10.1145/2933575.2935317

Adam Petcher and Greg Morrisett. 2015. The Foundational Cryptography Framework. In *Principles of Security and Trust—4th International Conference, POST 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings (Lecture Notes in Computer Science, Vol. 9036)*, Riccardo Focardi and Andrew C. Myers (Eds.). Springer, 53–72. https://doi.org/10.1007/978-3-662-46666-7_4
Tetsuya Sato. 2016. Approximate Relational Hoare Logic for Continuous Random Samplings. In *The Thirty-second Conference on the Mathematical Foundations of Programming Semantics*, MFPS 2016, Carnegie Mellon University, Pittsburgh, PA, USA, May 23-26, 2016 (*Electronic Notes in Theoretical Computer Science*, Vol. 325), Lars Birkedal (Ed.). Elsevier, 277–298. https://doi.org/10.1016/J.ENTCS.2016.09.043

Adam D. Smith. 2009. Differential privacy and the secrecy of the sample. https://adamdsmith.wordpress.com/2009/09/02/sample-secrecy/

Thomas Steinke. 2022. Composition of Differential Privacy & Privacy Amplification by Subsampling. arXiv:2210.00597 [cs.CR] https://arxiv.org/abs/2210.00597

Volker Strassen. 1965. The existence of probability measures with given marginals. *The Annals of Mathematical Statistics* (1965), 423–439. http://projecteuclid.org/euclid.aoms/1177700153

Joseph Tassarotti and Robert Harper. 2019. A separation logic for concurrent randomized programs. Proc. ACM Program. Lang. 3, POPL (2019), 64:1–64:30. https://doi.org/10.1145/3290377

Dominique Unruh. 2019. Quantum relational Hoare logic. Proc. ACM Program. Lang. 3, POPL (2019), 33:1–33:31. https://doi.org/10.1145/3290346

Elizaveta Vasilenko, Niki Vazou, and Gilles Barthe. 2022. Safe couplings: coupled refinement types. Proc. ACM Program. Lang. 6, ICFP (2022), 596–624. https://doi.org/10.1145/3547643

Cédric Villani. 2008. *Optimal transport: old and new*.

Peixin Wang, Hongfei Fu, Krishnendu Chatterjee, Yuxin Deng, and Ming Xu. 2020. Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time. Proc. ACM Program. Lang. 4, POPL (2020), 25:1–25:30. https://doi.org/10.1145/3371093

Stanley L. Warner. 1965. Randomized Response: A Survey Technique for Eliminating Evasive Answer Bias. J. Amer. Statist. Assoc. 60, 309 (1965), 63–69. https://doi.org/10.1080/01621459.1965.10480775