Properties such as provable security and correctness for randomized programs are naturally expressed relationally as approximate equivalences. As a result, a number of relational program logics have been developed to reason about such approximate equivalences of probabilistic programs. However, existing approximate relational logics are mostly restricted to first-order programs without general state. In this paper we develop Approxis, a higher-order approximate relational separation logic for reasoning about approximate equivalence of programs written in an expressive ML-like language with discrete probabilistic sampling, higher-order functions, and higher-order state. The Approxis logic recasts the concept of error credits in the relational setting to reason about relational approximation, which allows for expressive notions of modularity and composition, a range of new approximate relational rules, and an internalization of a standard limiting argument for showing exact probabilistic equivalences by approximation. We also use Approxis to develop a logical relation model that quantifies over error credits, which can be used to prove exact contextual equivalence. We demonstrate the flexibility of our approach on a range of examples, including the PRP/PRF switching lemma, IND\$-CPA security of an encryption scheme, and a collection of rejection samplers. All of the results have been mechanized in the Coq proof assistant and the Iris separation logic framework.

翻译：随机化程序的可证明安全性与正确性等属性，自然地以近似等价关系的形式表达。因此，已有多种关系程序逻辑被开发用于推理概率程序的此类近似等价关系。然而，现有的近似关系逻辑大多局限于无通用状态的一阶程序。本文提出了Approxis，一种用于高阶近似关系分离逻辑，用于推理以类ML表达性语言编写的程序之间的近似等价性，该语言包含离散概率采样、高阶函数与高阶状态。Approxis逻辑在关系设定中重构了误差信用的概念，以推理关系近似性，这使得表达性的模块化与组合概念、一系列新的近似关系规则以及通过近似展示精确概率等价性的标准极限论证内化成为可能。我们还利用Approxis构建了一个量化误差信用的逻辑关系模型，该模型可用于证明精确的上下文等价性。我们通过一系列示例展示了本方法的灵活性，包括PRP/PRF转换引理、加密方案的IND\$-CPA安全性以及一组拒绝采样器。所有结果均在Coq证明辅助器与Iris分离逻辑框架中实现了机械化验证。