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

9. Control Flow Macros

9.1.	The `ProgBuilder` Monad
9.2.	`ifThenElse`
9.3.	`X86.while`
9.4.	`proc`

←8.5. More Encoding Examples 9.1. The ProgBuilder Monad→

9. Control Flow Macros

High-level control flow constructs that expand to instruction sequences.

9.1. The ProgBuilder Monad
9.2. ifThenElse
9.3. X86.while
9.4. proc

←8.5. More Encoding Examples 9.1. The ProgBuilder Monad→