CoqToLeanAsm: x86 Macro Assembler in Lean 4

8.5. More Encoding Examples

[5#8, 120#8, 86#8, 52#8, 18#8]#eval encode 0 (Instr.BOP OpSize.Op32 BinOp.ADD (DstSrc.RI EAX 0x12345678)) -- XOR EAX, EAX (common idiom to zero a register) -- Shorter than MOV EAX, 0 (2 bytes vs 5 bytes) [49#8, 192#8]#eval encode 0 (Instr.BOP OpSize.Op32 BinOp.XOR (DstSrc.RR EAX EAX)) -- PUSH EBP = 0x55 (uses short encoding 50+rd) [85#8]#eval encode 0 (Instr.PUSH (Src.R EBP)) -- MOV EBP, ESP = 0x89 0xE5 [137#8, 229#8]#eval encode 0 (Instr.MOVOP OpSize.Op32 (DstSrc.RR EBP ESP))