面向高阶并发概率程序的情境化细化（延长版）

我们提出了 Foxtrot，这是第一个用于证明高阶并发概率程序情境细化的分离逻辑。从宏观层面看，Foxtrot 继承了标准并发分离逻辑中的各种并发推理原则，例如不变式和幽灵资源，并支持高级概率推理原则，以推理由并发线程引起的复杂概率分布，例如磁带预采样和通过误差放大进行的归纳。由于语言中概率与并发的结合以及 Foxtrot 模型的复杂性，这些强大的推理原则的集成极具挑战性；逻辑的可靠性依赖于 Iris 逻辑中的 Axiom of Choice 版本，而这一用法在此前基于 Iris 的逻辑工作中从未出现。我们在广泛的示例范围内展示了 Foxtrot 的表达能力，包括对抗性 von Neumann 硬币以及 Sodium 加密软件库中 $\mathsf{randombytes\_uniform}$ 函数。所有结果都在 Rocq 证明助理和 Iris 分离逻辑框架中实现。