10-Year Most Influential Paper Talk: Coq: the world's best macro assembler?
summary
Ten years ago a Coq formalization models a subset of 32-bit x86 with executable bit/byte memory, an assembler written in Coq that assembles assembly notation into hex bytes, and a proved roundtrip between encoding and decoding; dependent types and SSReflect bridge concrete bit-vectors and math integers; a separation-logic-style specification (a safety-as-continuation style) yields a correctness theorem relating machine code in memory to assertions; the generated binaries run on Windows and bare metal and the proofs are mechanized in Coq.
AI-written summary · about
chapters (23)
- 0:0010-year award intro
- 1:06Personal reflections
- 2:31Coq as macro assembler
- 3:34Verified OS concept
- 5:43Coq for machine code
- 7:12Assembler syntax in Coq
- 9:44Executable code from Coq
- 11:08Verified code on metal
- 11:30Modeling x86 with types
- 13:39x86 instruction set model
- 15:06Instruction decoding semantics
- 16:32x86 code generation
- 19:05Machine code macros
- 20:30DSLs to verified assembly
- 21:17Logic for correctness proofs
- 27:44Verification logic overview
- 28:04Original work limits
- 29:53Sail for ISA specs
- 32:23Bidirectional grammars
- 33:50Verification for Hack
- 37:26Type inference with continuations
- 40:25Conclusion and future
- 41:34Q&A
related talks
44mSession with the Coq Development Team
42mMetaCoq as a tool to prevent future unsoundness in Coq
23mVellvm: Formalizing the Informal
13mSpoq: Scaling Machine-Checkable Systems Verification in Coq
31mA Coq Library of Undecidable Problems
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
46mSession with the Coq Development Team
19mSystem-level weak memory models: The need for formalisation, ISA semantics integ...