CoqToLeanAsm: x86 Macro Assembler in Lean 4

10.3. ProcState

Full processor state combining registers, flags, and memory:

X86.ProcState.empty : ProcState#check ProcState.empty X86.ProcState.eip (s : ProcState) : DWord#check ProcState.eip -- Get instruction pointer X86.ProcState.setEIP (s : ProcState) (v : DWord) : ProcState#check ProcState.setEIP -- Set instruction pointer X86.ProcState.push (s : ProcState) (v : DWord) : ProcState#check ProcState.push -- Push to stack X86.ProcState.pop (s : ProcState) : ProcState × DWord#check ProcState.pop -- Pop from stack