Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)

TL;DR

Foxtrot is a novel higher-order separation logic designed for proving contextual refinement in higher-order concurrent probabilistic programs with local state, integrating advanced probabilistic and concurrency reasoning principles.

Contribution

It introduces Foxtrot, the first logic combining concurrency and probabilistic reasoning for higher-order programs, with mechanization in Rocq and Iris frameworks.

Findings

Proves soundness of Foxtrot using a novel axiom of choice within Iris.

Demonstrates Foxtrot's expressiveness on cryptographic and probabilistic examples.

Mechanized proofs in Rocq and Iris validate the logic's applicability.

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.