1: \begin{abstract}

2: \emph{Couplings} are a powerful mathematical tool for reasoning about pairs of

3: probabilistic processes. Recent developments in formal verification identify a

4: close connection between couplings and \Sprhl, a relational program logic

5: motivated by applications to provable security, enabling formal construction of

6: couplings from the probability theory literature. However, existing work using

7: \Sprhl merely shows existence of a coupling and does not give a way to prove

8: quantitative properties about the coupling, needed to reason about

9: mixing and convergence of probabilistic processes. Furthermore, \Sprhl\ is

10: inherently incomplete, and is not able to capture some advanced forms of

11: couplings such as shift couplings. We address both problems as follows.

12:   

13: First, we define an extension of \Sprhl, called \Sprprhl, which explicitly

14: constructs the coupling in a \Sprhl derivation in the form of a probabilistic product program

15: that simulates two correlated runs of the original program. Existing

16: verification tools for probabilistic programs can then be directly applied to

17: the probabilistic product to prove quantitative properties of the coupling.

18: Second, we equip \Sprprhl\ with a new rule for $\kwhile$ loops, where reasoning

19: can freely mix synchronized and unsynchronized loop iterations. Our proof

20: rule can capture examples of \emph{shift couplings}, and the logic is relatively

21: complete for deterministic programs.

22: 

23: We show soundness of \Sprprhl and use it to analyze two classes of

24: examples. First, we verify rapid mixing using

25: different tools from coupling: standard coupling, shift coupling, and

26: \emph{path coupling}, a compositional principle for combining local

27: couplings into a global coupling. Second, we verify

28: (approximate) equivalence between a source and an optimized program

29: for several instances of loop optimizations from the literature.

30: \end{abstract}

31: