Probabilistic programs often trade accuracy for efficiency, and are thus only approximately correct. It is important to obtain precise error bounds for these approximations, but existing approaches rely on simplifications that make the error bounds excesively coarse, or only apply to first-order programs. In this paper we present Eris, a higher-order separation logic for probabilistic programs written in an expressive higher-order language. Our key novelty is the introduction of error credits, a separation logic resource that tracks the error bound of a program. By representing error bounds as a resource, we recover the benefits of separation logic, including compositionality, modularity, and dependency between errors and program terms, allowing for more precise specifications. Moreover, we enable novel reasoning principles such as expectation-preserving error composition, amortized error reasoning, and proving almost-sure termination by induction on the error. We illustrate the advantages of our approach by proving amortized error bounds on a range of examples, including collision probabilities in hash functions, which allows us to write more modular specifications for data structures that use them as clients. We also use our logic to prove correctness and almost-sure termination of rejection sampling algorithms. All of our results have been mechanized in the Coq proof assistant using the Iris separation logic framework and the Coquelicot real analysis library.

翻译：概率程序常以精度换取效率，因此仅能实现近似正确。为这些近似获取精确的误差界至关重要，但现有方法依赖的简化手段导致误差界过于粗糙，或仅适用于一阶程序。本文提出Eris——一种针对用富有表现力的高阶语言编写的概率程序的高阶分离逻辑。我们的关键创新在于引入"错误信用度"这一分离逻辑资源，用于追踪程序的误差界。通过将误差界表示为资源，我们恢复了分离逻辑的优势，包括组合性、模块性以及误差与程序项之间的依赖关系，从而实现更精确的规约。此外，我们开创了新型推理原则，如保持期望的误差组合、摊销误差推理，以及通过误差归纳证明几乎必然终止。我们通过在一系列示例（包括哈希函数中的碰撞概率）上证明摊销误差界，展示了本方法的优势，这使我们能为使用这些哈希函数的数据结构编写更模块化的规约。我们还利用该逻辑证明了拒绝采样算法的正确性与几乎必然终止性。所有研究结果均已通过Iris分离逻辑框架和Coquelicot实数分析库在Coq证明助手中实现机械化。