1: \begin{abstract}

2:   Probabilistic coupling is a powerful tool for analyzing pairs of probabilistic

3:   processes. Roughly, coupling two processes requires finding an appropriate

4:   witness process that models both processes in the same probability space.

5:   Couplings are powerful tools proving properties about the relation between two

6:   processes, include reasoning about convergence of distributions and

7:   \emph{stochastic dominance}---a probabilistic version of a monotonicity

8:   property.

9: 

10:   While the mathematical definition of coupling looks rather complex

11:   and cumbersome to manipulate, we show that the relational program

12:   logic pRHL---the logic underlying the EasyCrypt cryptographic proof

13:   assistant---already internalizes a generalization of probabilistic coupling.

14:   With this insight, constructing couplings is no harder than constructing

15:   logical proofs.  We demonstrate how to express and verify classic examples of

16:   couplings in pRHL, and we mechanically verify several couplings in EasyCrypt.

17: \end{abstract}

18: