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.

翻译：我们提出 Foxtrot，这是首个用于证明带有高阶局部状态的高阶并发概率程序上下文精化的高阶分离逻辑。从高层来看，Foxtrot 继承了标准并发分离逻辑中的各种并发推理原理，例如不变量和幽灵资源，并支持用于推理并发线程引起的复杂概率分布的高级概率推理原理，例如磁带预采样和基于错误放大的归纳。由于语言中概率与并发性的结合以及 Foxtrot 模型的复杂性，这些强推理原理的整合具有高度非平凡性；该逻辑的可靠性依赖于 Iris 逻辑中某种版本的选择公理，这在先前基于 Iris 的逻辑工作中未曾使用。我们通过一系列广泛示例展示了 Foxtrot 的表达能力，包括对抗性冯·诺依曼硬币问题和 Sodium 加密软件库中的 $\mathsf{randombytes\_uniform}$ 函数。所有结果已在 Rocq 证明助手和 Iris 分离逻辑框架中机械化。