CoqToLeanAsm: x86 Macro Assembler in Lean 4

10.1. Memory

Memory is modeled as a function from addresses to bytes:

X86.Memory.empty : Memory#check Memory.empty -- All zeros X86.Memory.readByte (m : Memory) (addr : DWord) : Byte#check Memory.readByte -- Read single byte X86.Memory.writeByte (m : Memory) (addr : DWord) (v : Byte) : Memory#check Memory.writeByte -- Write single byte X86.Memory.readDWord (m : Memory) (addr : DWord) : DWord#check Memory.readDWord -- Read 32-bit value (little-endian) X86.Memory.writeDWord (m : Memory) (addr v : DWord) : Memory#check Memory.writeDWord -- Write 32-bit value