CoqToLeanAsm: x86 Macro Assembler in Lean 4

9.3. X86.while

Loop construct:

X86.while (ptest : ProgBuilder Unit) (cc : Condition) (cv : Bool) (pbody : ProgBuilder Unit) : ProgBuilder Unit#check X86.while X86.doWhile (pbody ptest : ProgBuilder Unit) (cc : Condition) (cv : Bool) : ProgBuilder Unit#check doWhile

Pattern:

loop_start:
  ; test (sets flags)
  Jcc loop_end
  ; body
  JMP loop_start
loop_end: