Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
summary
Provides a new higher-order relational separation logic called Clutch that proves contextual refinement for a language with impredicative polymorphism, higher-order local state and probabilistic choice. It introduces pre-sampling tapes (tape-annotated flips and tape ownership as a separation-logic resource) to encode asynchronous couplings, gives a step-indexed logical relation that implies contextual equivalence, mechanizes all proofs in Coq atop Iris and Coquelicot, and ships reusable artifacts and examples (including ElGamal fragments) on GitHub/Zenodo.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 0:22Probabilistic programs example
- 2:27Goals and language features
- 3:52Contextual refinement and relations
- 5:56Coupling logic and soundness
- 7:00Pre-sampling tapes intro
- 9:29Asynchronous coupling with tapes
- 11:14Proving refinement with tapes
- 12:18Clutch logic summary
- 12:38Opening the floor for questions
related talks
21mHyper Separation Logic
21mModular Verification of Differential Privacy in Probabilistic Higher-Order Separation(…)
21mSeparation Logics for Probability, Concurrency, and Security
26mCryptis: Cryptographic Reasoning in Separation Logic
23mSecurity Reasoning via Substructural Dependency Tracking
30mVerifying Reliable Network Components in a Distributed Separation Logic with Dep...
19mMechanized Logical Relations for Termination-Insensitive Noninterference
19mA quantitative probabilistic relational Hoare logic