1.2. Key Features

The assembler provides:

• Bit-precise types using Lean 4's BitVec for Byte, Word, and DWord

• Full x86-32 register model including Reg, ByteReg, and SegReg

• Comprehensive instruction encoding with ModR/M byte and SIB byte generation

• Separation logic predicates via SPred for reasoning about memory and registers

• Multi-pass assembler with the assemble function for forward reference resolution

• Control flow macros including ifThenElse, X86.while, and proc

• Intel-style syntax via the x86! macro for readable assembly programs