WP-Preserving Compilation -- Preserving Weakest Preconditions For End-to-End Verification
summary
Claims a compilation chain that preserves weakest preconditions by proving source and compiled programs denote bisimilar interaction trees interpreted in Iris. Implements a Rust-to-rock transpiler prototype and a toy Imp→CSP compiler and proves a lemma: bisimilar ITrees imply identical weakest-precondition judgments. Addresses effects by specifying pre/post for each event (uses program logic Salakart). Work is at early stages: upper compilation passes are mostly implemented, full end-to-end lowering and nontrivial memory/representation mismatches remain unresolved.
AI-written summary · about
chapters (12)
- 0:00WP-Preserving Compilation intro
- 1:57Compiler verification goals
- 2:40Interaction trees foundation
- 4:07Weakest precondition with I3
- 5:57Source and target semantics
- 6:38Compiler verification challenges
- 9:51Toy language approach
- 10:11Q&A: Monads and effects
- 11:33Q&A: Alternatives to I3
- 13:45Q&A: Rust compiler semantics
- 15:56Q&A: Bisimulation in proofs
- 18:07Closing remarks
related talks
31mBlame-Preserving Secure Compilation
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
25mComposing Secure Compilers
29mTowards Formally Verified Just-In-Time Compilation
01h 06mVerifying a compiler through equational means
19mAn Iris Instance for Verifying CompCert C Programs
18mPreservation of Speculative Constant-time by Compilation
15mCompiling with Continuations, Correctly