CoqToLeanAsm: x86 Macro Assembler in Lean 4

9.4. proc

Procedure with stack frame:

X86.proc (name : String) (localBytes : Nat := 0) (body : ProgBuilder Unit) : ProgBuilder Unit#check proc X86.procPrologue (localBytes : Nat := 0) : ProgBuilder Unit#check procPrologue X86.procEpilogue : ProgBuilder Unit#check procEpilogue

Generates:

  PUSH EBP
  MOV EBP, ESP
  SUB ESP, frameSize
  ; body
  MOV ESP, EBP
  POP EBP
  RET