Runnable trait

module arch.system.state.resource_machine.notes.runnable;

import prelude open;

trait
type Runnable KVSKey KVSDatum Executable ProgramState :=
  mkRunnable@{
    executeStep
      : Executable
        -> ProgramState
        -> Pair KVSKey KVSDatum
        -> Result
          String
          (Pair ProgramState (List (Either KVSKey (Pair KVSKey KVSDatum))));
    halted : ProgramState -> Bool;
    startingState : ProgramState;
  };

executeStep:

Takes the executable code, current program state, and read key-value pair and returns either: - Error string on failure - New program state and list of either: - Left key for read requests - Right (key, value) for write requests