CoqToLeanAsm: x86 Macro Assembler in Lean 4

7.1. Instruction Categories

  • Instr.MOVOP - Data movement

  • Instr.BOP - Binary ALU operations (ADD, SUB, AND, OR, XOR, CMP)

  • Instr.UOP - Unary operations (INC, DEC, NOT, NEG)

  • Instr.SHIFTOP - Shift and rotate

  • Instr.JCCrel - Conditional jumps

  • Instr.JMPrel - Unconditional jump

  • Instr.CALLrel - Procedure call

  • Instr.RETOP - Return from procedure

  • Instr.PUSH / Instr.POP - Stack operations