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建立了一个逻辑步骤索引的逻辑关系，用于推理用包含高阶局部状态和谓词多态的丰富语言编写的高阶程序的上下文精化与等价性。最后，我们通过一系列案例研究展示了我们方法的实用性。本文中的所有结果均已使用Coquelicot库和Iris分离逻辑框架在Coq证明助手中进行了形式化。