CoqToLeanAsm: x86 Macro Assembler in Lean 4

 CoqToLeanAsm: x86 Macro Assembler in Lean 4

Ported from Kennedy, Benton, Jensen, Dagand (PPDP 2013)

This is a Lean 4 port of "Coq: The World's Best Macro Assembler?" by Andrew Kennedy, Nick Benton, Jonas Jensen, and Pierre-Évariste Dagand. The original paper appeared at PPDP 2013 and demonstrated how to use Coq's dependent types and tactic system to build a verified x86-32 assembler.

Contents

  1. 1. Overview
  2. 2. Applications from the Original Paper
  3. 3. Quick Start
  4. 4. Module Structure
  5. 5. Bit Vector Types
  6. 6. Registers
  7. 7. Instructions
  8. 8. Encoding
  9. 9. Control Flow Macros
  10. 10. Memory Model
  11. 11. Assembly
  12. 12. Examples with x86! Macro
  13. 13. Executable Verification
  14. 14. Type Safety
  15. 15. Common Assembly Idioms
  16. 16. Semantic Properties
  17. 17. References