CoqToLeanAsm: x86 Macro Assembler in Lean 4

8.3. SIB byte in Detail

When the r/m field is 100 (would be ESP) with mod≠11, the processor expects a SIB byte to follow. This enables scaled indexed addressing:

 7   6   5   4   3   2   1   0
+---+---+---+---+---+---+---+---+
| scale |   index   |   base    |
+---+---+---+---+---+---+---+---+

scale (bits 7-6) is the scale factor:

  • 00 = ×1

  • 01 = ×2

  • 10 = ×4

  • 11 = ×8

index (bits 5-3) is the index register (ESP=100 means "no index")

base (bits 2-0) is the base register (EBP=101 with mod=00 means "disp32 only")

8.3.1. Example: Scaled Index Addressing (0x8B 0x04 0x8B)

[139#8, 4#8, 139#8]#eval encode 0 (Instr.MOVOP OpSize.Op32 (DstSrc.RM EAX (MemSpec.regIdx EBX (.ECX) Scale.S4)))

Breaking down:

  • 0x8B = MOV r32, r/m32 opcode

  • 0x04 = ModR/M: mod=00 (memory), reg=000 (EAX), r/m=100 (SIB follows)

  • 0x8B = SIB: scale=10 (×4), index=001 (ECX), base=011 (EBX)

8.3.2. Example: Scaled Index with Displacement (0x8B 0x44 0x8B 0x10)

[139#8, 68#8, 139#8, 16#8]#eval encode 0 (Instr.MOVOP OpSize.Op32 (DstSrc.RM EAX (MemSpec.regIdxDisp EBX (.ECX) Scale.S4 16)))
  • 0x8B = MOV r32, r/m32 opcode

  • 0x44 = ModR/M: mod=01 (memory+disp8), reg=000 (EAX), r/m=100 (SIB)

  • 0x8B = SIB: scale=10 (×4), index=001 (ECX), base=011 (EBX)

  • 0x10 = displacement (16 as signed byte)