CoqToLeanAsm: x86 Macro Assembler in Lean 4

8.1. Instruction Format

A typical x86 instruction has the following structure:

[Prefix] Opcode [ModR/M] [SIB] [Displacement] [Immediate]
  • Prefix (0-4 bytes): Operand size override (0x66), address size override (0x67), segment override, REP/REPNE, LOCK

  • Opcode (1-3 bytes): The operation to perform

  • ModR/M (0-1 bytes): Specifies register and addressing mode

  • SIB (0-1 bytes): Scale-Index-Base for complex addressing

  • Displacement (0, 1, 2, or 4 bytes): Memory offset

  • Immediate (0, 1, 2, or 4 bytes): Constant operand