2. Applications from the Original Paper

The original PPDP 2013 paper demonstrated several compelling applications that showcase the power of embedding an assembler in a proof assistant. This port preserves the core architecture while adapting it to Lean 4.

1. 2.1. Factorial with Printf (Paper Figure 1)
2. 2.2. Game of Life on Bare Metal (Paper Figure 2)
3. 2.3. Portable Executable Generation
4. 2.4. Multiplication by Constant (Paper Section 4.1)
5. 2.5. Calling Convention Abstraction (Paper Section 4.2)
6. 2.6. Regular Expression Compiler (Paper Section 4.3)
7. 2.7. Key Insight: Macros as Verified Abstractions