1.3. Design Philosophy

The assembler uses dependent types to ensure correctness:

1. Type-safe operand sizes: The OpSize type indexes register and immediate types via VWord and VReg, preventing mismatched operand sizes. An 8-bit register cannot be used where a 32-bit operand is expected.

2. Structured addressing modes: Memory operands use MemSpec, which captures the full range of x86 addressing: base, index, scale factor, displacement. The NonSPReg type statically prevents using ESP as an index register.

3. Verified encoding: Each Instr variant maps to exactly one encoding via encode. These encodings can be verified against real assembler output using rfl proofs.

4. Compositional assembly: Programs are built from instruction sequences using ProgBuilder, which handles label allocation and forward reference resolution.