Asynchronous Probabilistic Couplings in Higher-Order Separation Logic

Abstract

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.

References in corpus (3)

• Proving Expected Sensitivity of Probabilistic Programs
• Step-Indexed Logical Relations for Probability (long version)
• A Separation Logic for Negative Dependence

Cited by in corpus (7)

• Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
• Approximate Relational Reasoning for Higher-Order Probabilistic Programs
• Tachis: Higher-Order Separation Logic with Credits for Expected Costs
• Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning
• Almost-Sure Termination by Guarded Refinement
• Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants
• GradInf: Gradient Estimation as Probabilistic Inference