CoqToLeanAsm: x86 Macro Assembler in Lean 4

7.3. Operand Types

7.3.1. DstSrc - Destination-Source Pairs

For two-operand instructions:

X86.DstSrc.RR {s : OpSize} : VReg s → VReg s → DstSrc s#check DstSrc.RR -- reg, reg X86.DstSrc.RM {s : OpSize} : VReg s → MemSpec → DstSrc s#check DstSrc.RM -- reg, [mem] X86.DstSrc.MR {s : OpSize} : MemSpec → VReg s → DstSrc s#check DstSrc.MR -- [mem], reg X86.DstSrc.RI {s : OpSize} : VReg s → VWord s → DstSrc s#check DstSrc.RI -- reg, imm X86.DstSrc.MI {s : OpSize} : MemSpec → VWord s → DstSrc s#check DstSrc.MI -- [mem], imm

7.3.2. RegMem - Register or Memory

X86.RegMem.R {s : OpSize} : VReg s → RegMem s#check RegMem.R -- Register operand X86.RegMem.M {s : OpSize} : MemSpec → RegMem s#check RegMem.M -- Memory operand

7.3.3. Src - Source Operand

X86.Src.I : DWord → Src#check Src.I -- Immediate value X86.Src.R : Reg → Src#check Src.R -- Register X86.Src.M : MemSpec → Src#check Src.M -- Memory