Coq: The world’s best macro assembler?

Abstract

📜 Abstract

We describe a Coq formalization of a subset of the x86 architecture. One emphasis of the model is brevity: using dependent types, type classes and notation we give the x86 semantics a makeover that counters its reputation for baroqueness. We model bits, bytes, and memory concretely using functions that can be computed inside Coq itself; concrete representations are mapped across to mathematical objects in the SSREFLECT library (naturals, and integers modulo 2 n ) to prove theorems. Finally, we use notation to support conventional assembly code syntax inside Coq, including lexically-scoped labels. Ordinary Coq definitions serve as a powerful “macro” feature for everything from simple conditionals and loops to stack-allocated local variables and procedures with parameters. Assembly code can be assembled within Coq, producing a sequence of hex bytes. The assembler enjoys a correctness theorem relating machine code in memory to a separation-logic formula suitable for program verification.

Description

✨ Summary

The paper presents a Coq-based framework for modeling, programming, assembling, and reasoning about a subset of the x86 instruction-set architecture. Its central design goal is to keep the formalization executable and relatively concise while retaining strong typing and machine-level fidelity. The authors use dependent types, type classes, implicit coercions, indexed inductive types, monadic abstractions, and custom notation to make low-level code readable inside Coq.

Executable machine model: Bits and words are represented concretely as tuples of booleans, with types parameterized by word length. The model includes bytes, 16-bit words, 32-bit words, 64-bit words, registers, flags, memory, instruction decoding, and instruction execution.
Mathematical reasoning over concrete data: Concrete bit-vector representations are connected to natural numbers and integers modulo powers of two through the SSReflect/Mathematical Components ecosystem. This allows arithmetic properties, such as associativity of addition, to be proved using established algebraic lemmas.
Structured memory and I/O abstractions: Memory is represented as finite partial maps implemented using tries. Reader and writer terms provide functional, imperative, and logical interpretations of byte sequences, supporting reuse across decoding, encoding, execution, and specification.
Assembly embedded in Coq: Custom notation supports assembly syntax resembling Intel notation. Lexically scoped labels are implemented using higher-order abstract syntax, while ordinary Coq definitions act as user-defined macros.
Verified assembly: The framework can assemble programs inside Coq into hexadecimal machine code. The authors prove that instruction decoding is a left inverse of encoding and establish that assembling code preserves the relevant correctness properties.
Program-level abstractions: The system supports loops, conditionals, procedures, stack-allocated locals, calling conventions, data directives, and scoped labels. Examples include factorial computation, a Game of Life implementation, and a regular-expression compiler targeting x86 machine code.
Verification connection: Assembled machine code is related to separation-logic specifications, enabling machine-level programs to be verified within the same environment used to define and assemble them.

The paper reports that the concrete bit-vector implementation is executable inside Coq, achieving approximately 150,000 32-bit increments per second and 11,000 32-bit additions on the reported test machine. The model deliberately covers only a subset of x86, and several aspects remain incomplete, including branch-displacement decisions, richer memory permissions, and some external executable-format tooling. The authors also identify scalability concerns: computation performed directly inside Coq can be slower and more memory-intensive than extracted native code, and opaque definitions in supporting libraries can interfere with computation.

The paper was later presented as a PPDP 2023 10-Year Most Influential Paper, indicating formal recognition by the conference community of its longer-term influence. (2023.splashcon.org) Its approach has also been explicitly cited as inspiration for later verified-assembler experiments, including an experimental Lean 4 macro assembler targeting zkEVM-related development; that project describes itself as inspired by the paper but is not evidence of production or industrial deployment. (github.com) The search found references in subsequent formal-verification and instruction-set work, but no independently documented industrial product adoption directly attributable to this paper. The paper’s concrete legacy is therefore primarily methodological: integrating executable ISA models, embedded assembly notation, verified encoding, and program specifications in a single proof-assistant environment. (microsoft.com)