Probabilistic couplings are the foundation for many probabilistic relational program logics and arise when relating random sampling statements across two programs. In relational program logics, this manifests as dedicated coupling rules that, e.g., say we may reason as if two sampling statements return the same value. However, this approach fundamentally requires aligning or "synchronizing" the sampling statements of the two programs which is not always possible. In this paper, we develop Clutch, a higher-order probabilistic relational separation logic that addresses this issue by supporting asynchronous probabilistic couplings. We use Clutch to develop a logical step-indexed logical relational to reason about contextual refinement and equivalence of higher-order programs written in a rich language with higher-order local state and impredicative polymorphism. Finally, we demonstrate the usefulness of our approach on a number of case studies. All the results that appear in the paper have been formalized in the Coq proof assistant using the Coquelicot library and the Iris separation logic framework.

翻译：概率耦合是许多概率关系程序逻辑的基础，出现在关联两个程序中的随机采样语句时。在关系程序逻辑中，这表现为专用的耦合规则，例如，该规则允许我们推理两个采样语句返回相同值。然而，这种方法从根本上要求对齐或“同步”两个程序的采样语句，而这并非总是可行。在本文中，我们开发了Clutch——一种高阶概率关系分离逻辑，它通过支持异步概率耦合解决了这一问题。我们使用Clutch构建了一个逻辑步进索引的逻辑关系，以推理用丰富语言编写的高阶程序的上下文精炼和等价性，该语言支持高阶局部状态和超定义多态性。最后，我们通过一系列案例研究展示了我们方法的实用性。本文中所有结果已在Coq证明助手中使用Coquelicot库和Iris分离逻辑框架形式化。