Approximate Relational Reasoning for Higher-Order Probabilistic Programs
arXiv:2407.14107 · doi:10.1145/3704877
Abstract
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.
Camera-ready POPL submission including additional appendix
References in corpus (14)
- Proving Differential Privacy via Probabilistic Couplings
- Advanced Probabilistic Couplings for Differential Privacy
- Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Programs
- Relational reasoning via probabilistic coupling
- Proving Expected Sensitivity of Probabilistic Programs
- A Probabilistic Separation Logic
- Amortised Resource Analysis with Separation Logic
- Approximate Relational Hoare Logic for Continuous Random Samplings
- Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
- ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity
- A Separation Logic for Negative Dependence
- Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
- Approximate Relational Reasoning for Higher-Order Probabilistic Programs
- Tachis: Higher-Order Separation Logic with Credits for Expected Costs