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分离逻辑框架中实现机械化。