#### Coq: The world's best macro assembler?

##### Andrew Kennedy, Nick Benton, Jonas Jensen, Pierre-Evariste Dagand

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.