def MState.jif (ms : MState) (reg : UInt64) (lbl : String) (cond : UInt64 → Bool) : MState

def MState.jif' (ms : MState) (reg1 reg2 : UInt64) (lbl : String) (cond : UInt64 → UInt64 → Bool) : MState

def MState.runOneStep (ms : MState) : MState

This function evaluates the given machine state to a new one. Tt represents the nxt function from the paper LUNDBERG, Didrik, et al. Hoare-style logic for unstructured programs. In: International Conference on Software Engineering and Formal Methods. Cham: Springer International Publishing, 2020. S. 193-213.

Generally, if the terminated of the State is false and the instruction is legal and evaluateable, a new State is returned holding the next instructions and the updated storage. When the instruction is not legal (e.g. jmp s, there is no label s), terminated is set to true.

def MState.runNSteps (ms : MState) (n : ℕ) : MState

Runs runOneStep n times. It represents the function nxt^n from LUNDBERG, Didrik, et al. Hoare-style logic for unstructured programs. In: International Conference on Software Engineering and Formal Methods. Cham: Springer International Publishing, 2020. S. 193-213.

def MState.nextInstruction (ms : MState) : Instr