Approximate Relational Reasoning for Higher-Order Probabilistic Programs
<|reference_start|>Approximate Relational Reasoning for Higher-Order Probabilistic Programs: 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.<|reference_end|>
@article{haselwarter2024approximate,
    title={Approximate Relational Reasoning for Higher-Order Probabilistic Programs},
    author={Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre, Simon
  Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal},
    journal={arXiv preprint arXiv:2407.14107},
    year={2024},
    archivePrefix={arXiv},
    eprint={2407.14107},
    primaryClass={cs.LO cs.PL}
}