CoqToLeanAsm: x86 Macro Assembler in Lean 4

8. Encoding

x86 instruction encoding is notoriously complex, with variable-length instructions and multiple encoding options for the same operation. The encode function handles all details, producing the exact same bytes as a production assembler like NASM.

  1. 8.1. Instruction Format
  2. 8.2. ModR/M byte in Detail
  3. 8.3. SIB byte in Detail
  4. 8.4. Encoding Verification with rfl
  5. 8.5. More Encoding Examples