Contextual Refinement of Higher-Order Concurrent Probabilistic Programs

TL;DR

Foxtrot presents the first higher-order probabilistic concurrent separation logic capable of proving contextual refinement for higher-order concurrent probabilistic programs with local state. It introduces a novel refinement judgment built on a relational Iris-based model, supported by a robust set of coupling rules, presampling tapes, fragmentation techniques, and error-credits to handle complex interactions between probability and concurrency. The approach is demonstrated through challenging case studies, including an adversarial von Neumann coin and the Sodium library’s randombytes_uniform, with all results mechanized in Rocq. This work advances the ability to reason about termination probabilities and equivalences in highly concurrent probabilistic software, with potential impact on cryptography, randomized data structures, and concurrent systems verification.

Abstract

We present Foxtrot, the first higher-order separation logic for proving contextual refinement of higher-order concurrent probabilistic programs with higher-order local state. From a high level, Foxtrot inherits various concurrency reasoning principles from standard concurrent separation logic, e.g. invariants and ghost resources, and supports advanced probabilistic reasoning principles for reasoning about complex probability distributions induced by concurrent threads, e.g. tape presampling and induction by error amplification. The integration of these strong reasoning principles is highly non-trivial due to the combination of probability and concurrency in the language and the complexity of the Foxtrot model; the soundness of the logic relies on a version of the axiom of choice within the Iris logic, which is not used in earlier work on Iris-based logics. We demonstrate the expressiveness of Foxtrot on a wide range of examples, including the adversarial von Neumann coin and the $\mathsf{randombytes\_uniform}$ function of the Sodium cryptography software library. All results have been mechanized in the Rocq proof assistant and the Iris separation logic framework.

Figures (7)

• Figure 1: Systems for proving contextual refinement (Logic = implemented as a logic, ND = only nondeterminism).
• Figure 2: Entropy mixer example.
• Figure 3: Batch-sampling example.
• Figure 4: Rejection sampler example.
• Figure 5: Adversarial von Neumann coin example.

Theorems & Definitions (11)

• definition 1: Approximate Coupling
• theorem 1: Adequacy
• lemma 1: Fundamental Lemma of Binary Logical Relations
• theorem 2: Soundness
• lemma 2: Fundamental Lemma of Unary Logical Relations
• lemma 3
• lemma 4
• lemma 5
• definition 2
• lemma 6: Iris Choice