Juvix imports

module arch.node.engines.executor_environment;

import prelude open;
import arch.node.types.messages open;
import arch.node.types.identities open;
import arch.node.types.engine_environment open;
import arch.node.engines.executor_messages open;
import arch.node.types.anoma_message as Anoma open;

Executor Environment¶

Overview¶

The executor environment maintains state needed during transaction execution including completed reads/writes and program state.

Auxiliary Juvix code

axiom executeStep : Executable
  -> ProgramState
  -> Pair KVSKey KVSDatum
  -> Result
    String
    (Pair ProgramState (List (Either KVSKey (Pair KVSKey KVSDatum))));

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

Mailbox states¶

The executor engine does not require complex mailbox states.

`ExecutorMailboxState`¶

syntax alias ExecutorMailboxState := Unit;

Local state¶

`ExecutorLocalState`¶

type ExecutorLocalState :=
  mkExecutorLocalState@{
    program_state : ProgramState;
    completed_reads : Map KVSKey KVSDatum;
    completed_writes : Map KVSKey KVSDatum;
  };

Arguments

program_state: Current state of the executing program
completed_reads: Map of keys to values that have been successfully read
completed_writes: Map of keys to values that have been successfully written

Timer Handle¶

The executor engine does not require timer handles.

`ExecutorTimerHandle`¶

syntax alias ExecutorTimerHandle := Unit;

The Executor Environment¶

`ExecutorEnv`¶

ExecutorEnv : Type :=
  EngineEnv
    ExecutorLocalState
    ExecutorMailboxState
    ExecutorTimerHandle
    Anoma.Msg;

Instantiation¶

executorEnv : ExecutorEnv :=
  mkEngineEnv@{
    localState :=
      mkExecutorLocalState@{
        program_state :=
          mkProgramState@{
            data := "";
            halted := false;
          };
        completed_reads := Map.empty;
        completed_writes := Map.empty;
      };
    mailboxCluster := Map.empty;
    acquaintances := Set.empty;
    timers := [];
  };