1.1. Why a Verified Assembler?

Traditional assemblers like NASM, GAS, or MASM are trusted components in the toolchain. When they produce incorrect output, the resulting bugs are extremely difficult to diagnose because the generated code doesn't match the source. A verified assembler provides:

1. Correctness by construction: The encoding functions are total and deterministic. Each instruction variant maps to exactly one byte sequence.

2. Type-level guarantees: Lean's type system prevents invalid instruction combinations at compile time. You cannot accidentally use ESP as a SIB index register.

3. Proved properties: Key encoding properties can be proved using rfl (definitional equality), giving mathematical certainty about the output.

4. Executable specification: The assembler serves as both documentation and implementation—the specification is the code.