CoqToLeanAsm: x86 Macro Assembler in Lean 4

15.2. Function Prologue and Epilogue

Standard cdecl function setup:

-- Prologue (3 bytes)
push ebp        ; 55
mov ebp, esp    ; 89 E5

-- Epilogue (3 bytes)
mov esp, ebp    ; 89 EC
pop ebp         ; 5D
ret             ; C3

With the x86! macro:

def prologue : Program := x86! {
  push ebp
  mov ebp, esp
}

def epilogue : Program := x86! {
  mov esp, ebp
  pop ebp
  ret
}