CoqToLeanAsm: x86 Macro Assembler in Lean 4

CoqToLeanAsm: x86 Macro Assembler in Lean 4

Table of Contents

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

14. Type Safety

14.1.	Preventing ESP as SIB Index
14.2.	Operand Size Consistency
14.3.	Immediate Size Checking
14.4.	Label Resolution

←13. Executable Verification 14.1. Preventing ESP as SIB Index→

14. Type Safety

One of the key benefits of embedding an assembler in a dependently-typed language is that many invalid programs are rejected at compile time.

14.1. Preventing ESP as SIB Index
14.2. Operand Size Consistency
14.3. Immediate Size Checking
14.4. Label Resolution

←13. Executable Verification 14.1. Preventing ESP as SIB Index→