Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning
arXiv:2402.18708 · doi:10.1145/3704894
Abstract
We present Bluebell, a program logic for reasoning about probabilistic programs where unary and relational styles of reasoning come together to create new reasoning tools. Unary-style reasoning is very expressive and is powered by foundational mechanisms to reason about probabilistic behaviour like independence and conditioning. The relational style of reasoning, on the other hand, naturally shines when the properties of interest compare the behaviour of similar programs (e.g. when proving differential privacy) managing to avoid having to characterize the output distributions of the individual programs. So far, the two styles of reasoning have largely remained separate in the many program logics designed for the deductive verification of probabilistic programs. In Bluebell, we unify these styles of reasoning through the introduction of a new modality called "joint conditioning" that can encode and illuminate the rich interaction between conditional independence and relational liftings; the two powerhouses from the two styles of reasoning.
arXiv comment23 pages + 53 pages of appendix
References in corpus (9)
- LightDP: Towards Automating Differential Privacy Proofs
- Proving Differential Privacy with Shadow Execution
- Relational reasoning via probabilistic coupling
- A Separation Logic for Concurrent Randomized Programs
- A Probabilistic Separation Logic
- This Is the Moment for Probabilistic Loops
- Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
- A Separation Logic for Negative Dependence
- Proving Hypersafety Compositionally