A Deductive System for Contract Satisfaction Proofs
summary
Claims a sound-and-complete deductive system for relative bisimulation that characterizes relative trace equality via a nested coinductive–inductive fixpoint, implemented and machine-checked in the Rocq proof assistant. The implementation uses four core proof rules plus up-to techniques, handles asynchronous interleaving of hardware and contract steps, and succeeds on two case studies (a sequentializing contract and an always mispredict contract). Artifacts and evaluations are available.
AI-written summary · about
chapters (7)
- 0:00Introduction
- 1:27Leakage contracts
- 3:12Relative simulation proof
- 7:27Trace equality challenges
- 9:12Deductive system
- 12:22Case studies
- 13:49Conclusion & Q&A
related talks
58mAutomating Relational Verification of Infinite-State Programs
21mEnhancing Symbolic Execution with Machine-Checked Safety Proofs
23mSecurity Reasoning via Substructural Dependency Tracking
25mBehavioral simulation for smart contracts
27mProofs of proofs: incremental verifiability from recursion and accumulation
50mTrust but Verify: Scaling Deductive Verification with Abstract Interpretation
17mProving capability safety in the presence of indirect sentries
31mSound Symbolic Execution via Abstract Interpretation and its Application to Sec...