تقرير
Approximate Relational Reasoning for Higher-Order Probabilistic Programs
العنوان: | Approximate Relational Reasoning for Higher-Order Probabilistic Programs |
---|---|
المؤلفون: | Haselwarter, Philipp G., Li, Kwing Hei, Aguirre, Alejandro, Gregersen, Simon Oddershede, Tassarotti, Joseph, Birkedal, Lars |
سنة النشر: | 2024 |
المجموعة: | Computer Science |
مصطلحات موضوعية: | Computer Science - Logic in Computer Science, Computer Science - Programming Languages |
الوصف: | 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. |
نوع الوثيقة: | Working Paper |
URL الوصول: | http://arxiv.org/abs/2407.14107 |
رقم الأكسشن: | edsarx.2407.14107 |
قاعدة البيانات: | arXiv |
كن أول من يترك تعليقا!