CoqToLeanAsm: x86 Macro Assembler in Lean 4

7.4. Data Movement Examples

Instr.MOVOP OpSize.Op32 (DstSrc.RR EAX EBX) : Instr#check Instr.MOVOP OpSize.Op32 (DstSrc.RR EAX EBX) -- MOV reg, imm: MOV EAX, 42 Instr.MOVOP OpSize.Op32 (DstSrc.RI EAX 42) : Instr#check Instr.MOVOP OpSize.Op32 (DstSrc.RI EAX 42) -- MOV reg, mem: MOV EAX, [EBX] Instr.MOVOP OpSize.Op32 (DstSrc.RM EAX (MemSpec.reg EBX)) : Instr#check Instr.MOVOP OpSize.Op32 (DstSrc.RM EAX (MemSpec.reg EBX)) -- MOV mem, reg: MOV [EBX], EAX Instr.MOVOP OpSize.Op32 (DstSrc.MR (MemSpec.reg EBX) EAX) : Instr#check Instr.MOVOP OpSize.Op32 (DstSrc.MR (MemSpec.reg EBX) EAX) -- PUSH reg Instr.PUSH (Src.R EAX) : Instr#check Instr.PUSH (Src.R EAX) -- PUSH imm Instr.PUSH (Src.I 100) : Instr#check Instr.PUSH (Src.I 100) -- POP reg Instr.POP (RegMem.R EBX) : Instr#check Instr.POP (RegMem.R EBX)