CoqToLeanAsm: x86 Macro Assembler in Lean 4

7.6. Control Flow

Conditional jumps use Condition and a polarity flag:

X86.Condition.Z : Condition#check Condition.Z -- Zero/Equal (ZF=1) X86.Condition.B : Condition#check Condition.B -- Below/Carry (CF=1) X86.Condition.S : Condition#check Condition.S -- Sign (SF=1) X86.Condition.O : Condition#check Condition.O -- Overflow (OF=1) X86.Condition.L : Condition#check Condition.L -- Less (signed: SF≠OF) X86.Condition.LE : Condition#check Condition.LE -- Less or Equal (signed) X86.Condition.BE : Condition#check Condition.BE -- Below or Equal (unsigned) Instr.JCCrel Condition.Z true : Tgt Instr#check Instr.JCCrel Condition.Z true -- JNZ label (jump if not zero, polarity=false inverts) Instr.JCCrel Condition.Z false : Tgt Instr#check Instr.JCCrel Condition.Z false -- JMP label (unconditional jump) X86.Instr.JMPrel (tgt : JmpTgt) : Instr#check Instr.JMPrel -- CALL label (procedure call) X86.Instr.CALLrel (tgt : JmpTgt) : Instr#check Instr.CALLrel -- RET (return from procedure) Instr.RETOP 0 : Instr#check Instr.RETOP 0 -- RET 8 (pop 8 extra bytes before return) Instr.RETOP 8 : Instr#check Instr.RETOP 8