Certifying Derivation of State Machines from Coroutines
summary
A compiler implemented as a Coq tactic turns programs written with freer-monad coroutines into explicit state-machine code by searching for equivalence proofs; it supports coroutine storage (binary-tree lookup) to manage thousands of connections. A concrete TLS core with extracted Haskell is built and runs with reasonable throughput, but end-to-end compilation is very slow (compile times measured in hours) and generated code currently trails hand-written Haskell by tens of percent. Artifacts and proofs are available.
AI-written summary · about
chapters (15)
- 0:00Intro
- 1:11TLS1.3 RFC: Simple Server Diagram
- 1:48One Connection: Blocking I/O
- 2:18More Connections, More Threads?
- 3:12Production Code: State Machines
- 4:07Risk: Superfluous Transitions (artificial example)
- 4:37OpenSSL 1998-2014
- 5:44Generating State Machines
- 7:06Nested Protocols
- 9:27Generating Nested State Machines
- 9:59Coq Encoding as Freer Monads
- 11:01Coroutines for Free!
- 11:49Per-connection State in Coroutines
- 14:38Prototype HTTPS Server Latency
- 15:10Future Directions
related talks
25mVerifying LLM powered Code Transformations with Equivalence Checking
12mAutomated Synthesis of Verified Firewalls
21mSecurely Compiling F* Programs With IO and Then Linking Them Against Weakly-Typ...
21mEnhancing Symbolic Execution with Machine-Checked Safety Proofs
58mAutomating Relational Verification of Infinite-State Programs
36mCorps: A Core Calculus of Hierarchical Choreographic Programming
23mThe Last Yard: Foundational End-to-End Verification of High-Speed Cryptography
15mMy Journey in Secure Compilation