Everything is now brought together in a single structure called MState, which represents the machine's MState This structure holds the memory, registers, the code, a program counter (PC), and a termination flag. The program counter points to the next instruction to be executed, while the termination flag indicates whether the machine state has halted or if further evaluation should continue.

structure MState : Type

The state of the abstract machine: its memory, registers, program counter, loaded code, and termination flag.

• memory : Memory

  The data memory of the machine.

• registers : Registers

  The register file of the machine.

• pc : ProgramCounter

  The program counter, pointing at the next instruction to execute.

• code : Code

  The program (code) loaded into the machine.

• terminated : Bool

  Whether the machine has halted.

def DefaultMState : MState

The initial machine state: empty memory and registers, program counter 0, not terminated, and the default code.

Equations

• DefaultMState = { memory := EmptyMemory, registers := EmptyRegisters, pc := 0, code := DefaultCode, terminated := false }

def MState.currInstruction (ms : MState) : Instr

The instruction at the current program counter.

Equations

• ms.currInstruction = TMap.get ms.code.instructionMap ms.pc

def MState.incPc (ms : MState) : MState

Increment the program counter by one.

Equations

• ms.incPc = { memory := ms.memory, registers := ms.registers, pc := ms.pc + 1, code := ms.code, terminated := ms.terminated }

def MState.setPc (ms : MState) (p : UInt64) : MState

Set the program counter to p.

Equations

• ms.setPc p = { memory := ms.memory, registers := ms.registers, pc := p, code := ms.code, terminated := ms.terminated }

def MState.setRegister (ms : MState) (r : Registers) : MState

Replace the register file with r.

Equations

• ms.setRegister r = { memory := ms.memory, registers := r, pc := ms.pc, code := ms.code, terminated := ms.terminated }

def MState.addRegister (ms : MState) (i v : UInt64) : MState

Set register i to value v.

Equations

• ms.addRegister i v = { memory := ms.memory, registers := (i ↦ v; ms.registers), pc := ms.pc, code := ms.code, terminated := ms.terminated }

def MState.getRegisterAt (ms : MState) (i : UInt64) : UInt64

Read the value of register i.

Equations

• ms.getRegisterAt i = TMap.get ms.registers i

def MState.setMemory (ms : MState) (m : Memory) : MState

Replace the memory with m.

Equations

• ms.setMemory m = { memory := m, registers := ms.registers, pc := ms.pc, code := ms.code, terminated := ms.terminated }

def MState.addMemory (ms : MState) (i v : UInt64) : MState

Set memory address i to value v.

Equations

• ms.addMemory i v = { memory := (i ↦ v; ms.memory), registers := ms.registers, pc := ms.pc, code := ms.code, terminated := ms.terminated }

def MState.getMemoryAt (ms : MState) (i : UInt64) : UInt64

Read the value at memory address i.

Equations

• ms.getMemoryAt i = TMap.get ms.memory i

def MState.setInstructionMap (ms : MState) (sc : InstructionMap) : MState

Replace the instruction map of the loaded code.

Equations

• One or more equations did not get rendered due to their size.

def MState.setCode (ms : MState) (code : Code) : MState

Replace the loaded code with code.

Equations

• ms.setCode code = { memory := ms.memory, registers := ms.registers, pc := ms.pc, code := code, terminated := ms.terminated }

def MState.setLabels (ms : MState) (l : LabelMap) : MState

Replace the label map of the loaded code.

Equations

• One or more equations did not get rendered due to their size.

def MState.setTerminated (ms : MState) (bool : Bool) : MState

Set the termination flag.

Equations

• ms.setTerminated bool = { memory := ms.memory, registers := ms.registers, pc := ms.pc, code := ms.code, terminated := bool }

def MState.getLabelAt (ms : MState) (s : String) : Option UInt64

Look up the target index of label s, if present.

Equations

• ms.getLabelAt s = PMap.get ms.code.labels s

def MState.createStandardState (c : Code) : MState

Build a fresh machine state running the code c.

Equations

• MState.createStandardState c = { memory := DefaultMState.memory, registers := DefaultMState.registers, pc := DefaultMState.pc, code := c, terminated := DefaultMState.terminated }

def MState.jump (ms : MState) (s : String) : MState

This creates a Machine state with the pointer which the label [s] points to. If there is no label [s] in code.labels, terminated is set to true.

Equations

• One or more equations did not get rendered due to their size.