Couplings are a powerful tool for proving rapid mixing of probabilistic processes, with applications across many fields of mathematics and computer science. A recent development in formal verification identifies a close connection between couplings and pRHL, a relational program logic motivated by applications to provable security. This close connection opens the door to using the program logic pRHL far beyond its envisioned scope, for verifying examples from the coupling literature. However, there is a technical challenge: whereas many applications of coupling requires reasoning about the coupled process, every derivation in pRHL merely proves its existence. Moreover, pRHL is inherently incomplete, and as a consequence, is not able to capture some advanced forms of couplings such as shift couplings. We address both problems as follows.

First, we define a proof-relevant program logic, called prpRHL, which makes explicit the coupling in a pRHL derivation, in the form of a product program that simulates two correlated runs of the original program. Existing verification tools for probabilistic programs can then be directly applied to the probabilistic product to prove quantitative properties of the coupling, for instance, for analyzing the speed of convergence of the probabilistic process.

Second, we equip prpRHL with a powerful rule for While loops, in which one can freely interleave synchronized and unsynchronized loop iterations. Our proof rule is sufficiently expressive to capture examples of shift couplings, and is relatively complete for deterministic programs.

We show soundness of prpRHL and use it to analyze two classes of examples. The first class of examples considers rapid mixing using different tools from coupling: standard coupling, shift coupling, and path coupling, a compositional principle for combining local couplings into a global coupling. The second class of examples proves (approximate) equivalence between a source and an optimized program, for several instances of loop optimizations from the literature.