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

6. Registers

6.1.	General Purpose Registers
6.2.	Byte Registers
6.3.	Word Registers
6.4.	Segment Registers
6.5.	Variable-Width Registers

6.5. Variable-Width Registers

←6.4. Segment Registers 7. Instructions→

6.5. Variable-Width Registers

The VReg type family selects the appropriate register type based on OpSize:

VReg OpSize.Op8 : Type#check (VReg OpSize.Op8)

←6.4. Segment Registers 7. Instructions→