CoqToLeanAsm: x86 Macro Assembler in Lean 4

2.1. Factorial with Printf (Paper Figure 1)

The paper's opening example computes factorials of 10 and 12, printing results via an external printf function. This demonstrates:

  • Procedure macros: letproc for locally-scoped procedure definitions

  • Calling conventions: call_cdecl3 expands to push arguments and clean stack

  • While loops: while (CMP ECX, EBX) CC_LE true (...) for structured control

  • Inline data: ds "Factorial of %d is %d" for string constants

The assembled code runs directly on Windows after makePEfile generates a PE executable.