Encode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic
summary
Claims a mechanical reduction of ∀∃ relational Hoare triples to ordinary unary Hoare triples by redefining relational validity and internalizing the ∀∃ pattern into an Exec predicate so existing provers need no logic extensions. Provides a formal encoding function and a soundness equivalence proof that encoded Hoare triples are valid iff the original relational triples are, maps relational proof rules to standard ones, and ships a Rock implementation with evaluated reusable artifacts and reproduced results.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 0:22Program correctness with Hoare triples
- 1:50Layered proof for code refinement
- 2:52Relational Hoare logic for refinement
- 3:58Encoding ∀∃ logic into standard Hoare logic
- 5:01Bit mask example and assertions
- 6:30Execution predicate core idea
- 7:12Encoding rules for low-level evaluation
- 7:56Encoding rules for high-level evaluation
- 8:17Proving example with symbolic execution
- 9:19Proving loop with execution predicate
- 10:23Conclusion and Rocq implementation
- 11:08Q&A
related talks
27mUnrealizability Logic
40mRelational Reasoning in Object-based Programs
23mSpecifying and Verifying Future Conditions
01h 05mVerifying Infinitely Many Programs at Once
20mOn Extending Incorrectness Logic with Backwards Reasoning
28mReasoning about Distributed Reconfigurable Systems
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
22mExecution Time Program Verification With Tight Bounds