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

11. Assembly

11.1.	The `assemble` Function
11.2.	`Program` Type

11.2. Program Type

←11.1. The assemble Function 12. Examples with x86! Macro→

11.2. `Program` Type

A program is a list of labeled instructions:

X86.Program : Type#check Program

←11.1. The assemble Function 12. Examples with x86! Macro→