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
7.
Instructions
7.1.
Instruction Categories
7.2.
Memory Addressing
7.3.
Operand Types
7.4.
Data Movement Examples
7.5.
Arithmetic Operations
7.6.
Control Flow
←
6.5. Variable-Width Registers
7.1. Instruction Categories
→
7. Instructions
The x86 instruction set is represented by the
Instr
inductive type.
7.1.
Instruction Categories
7.2.
Memory Addressing
7.3.
Operand Types
7.4.
Data Movement Examples
7.5.
Arithmetic Operations
7.6.
Control Flow
←
6.5. Variable-Width Registers
7.1. Instruction Categories
→