Engine Simulator¶

Module Setup and Core Types¶

The main simulator module with essential imports and the message selection strategy type definition.

module arch.node.integration.simulator;

import prelude open;

open OMap;

import arch.node.types.basics open public;
import arch.node.types.messages open public;
import arch.node.types.identities open;
import arch.node.types.engine_config open public;
import arch.node.types.engine_environment open;
import arch.node.types.engine_behaviour open;
import arch.node.types.engine open public;
import arch.node.types.anoma_engines open;
import arch.node.types.anoma_message open;
import arch.node.types.anoma_config open;
import arch.node.types.anoma_environment open;

MessageSelector : Type :=
  (messages : List (EngineMsg Msg))
    -> Option (Pair (EngineMsg Msg) (List (EngineMsg Msg)));

selectFirstMessage
  (messages : List (EngineMsg Msg))
  : Option (Pair (EngineMsg Msg) (List (EngineMsg Msg))) :=
  case messages of
    | [] := none
    | msg :: rest := some (mkPair msg rest);

Network and Node State Types¶

Data structures for representing nodes, network state, and the overall simulation environment.

type Node :=
  mkNode@{
    engines : OMap EngineName Eng;
  };

type NetworkState :=
  mkNetworkState@{
    nodes : OMap NodeID Node;
    messages : List (EngineMsg Msg);
    currentTime : Time;
    incrementId : NodeID -> NodeID;
    nextId : NodeID;
  };

Guard Execution and Action Processing¶

Core logic for executing guard outputs and processing engine actions based on triggers.

executeGuardOutput
  {C S B H A AM AC AE : Type}
  (output : GuardOutput C S B H A AM AC AE)
  (eng : Engine C S B H A AM AC AE)
  (trigger : TimestampedTrigger H AM)
  : Option (ActionEffect S B H AM AC AE) :=
  case output of
    | GuardOutput.mk@{action := ActionExec.Seq actions; args := args} :=
      let
        terminating
        executeAction
          (acts : List (Action C S B H A AM AC AE))
          (currentEnv : EngineEnv S B H AM)
          : Option (ActionEffect S B H AM AC AE) :=
          case acts of
            | [] := none
            | act :: rest :=
              case
                act
                  ActionInput.mk@{
                    args := args;
                    cfg := Engine.cfg eng;
                    env := currentEnv;
                    trigger := trigger;
                  }
              of
                | none := executeAction rest currentEnv
                | some effect :=
                  case executeAction rest (ActionEffect.env effect) of
                    | none := some effect
                    | some nextEffect :=
                      some
                        ActionEffect.mk@{
                          env := ActionEffect.env nextEffect;
                          msgs :=
                            ActionEffect.msgs effect
                              ++ ActionEffect.msgs nextEffect;
                          timers :=
                            ActionEffect.timers effect
                              ++ ActionEffect.timers nextEffect;
                          engines :=
                            ActionEffect.engines effect
                              ++ ActionEffect.engines nextEffect;
                        };
      in executeAction actions (Engine.env eng);

Engine Evaluation and Execution¶

Functions for evaluating guards and executing actions for specific engines, including both typed and untyped variants.

terminating
evaluateAndExecute
  {C S B H A AM AC AE : Type}
  (eng : Engine C S B H A AM AC AE)
  (msg : EngineMsg AM)
  : Option
    (Pair
      (List (EngineMsg AM))
      (Pair (List (Pair AC AE)) (Engine C S B H A AM AC AE))) :=
  let
    trigger :=
      TimestampedTrigger.mkTimestampedTrigger@{
        time := right 0;
        trigger :=
          Trigger.MessageArrived@{
            msg := msg;
          };
      };
    behaviour := Engine.behaviour eng;
    guardResult :=
      case EngineBehaviour.guards behaviour of
        | GuardEval.First guards :=
          let
            terminating
            tryGuard
              (gs : List (Guard C S B H A AM AC AE))
              : Option (GuardOutput C S B H A AM AC AE) :=
              case gs of
                | [] := none
                | g :: rest :=
                  case g trigger (Engine.cfg eng) (Engine.env eng) of
                    | none := tryGuard rest
                    | some output := some output;
          in tryGuard guards
        | GuardEval.Any guards :=
          let
            terminating
            tryGuard
              (gs : List (Guard C S B H A AM AC AE))
              : Option (GuardOutput C S B H A AM AC AE) :=
              case gs of
                | [] := none
                | g :: rest :=
                  case g trigger (Engine.cfg eng) (Engine.env eng) of
                    | none := tryGuard rest
                    | some output := some output;
          in tryGuard guards;
    actionResult :=
      case guardResult of
        | none := none
        | some output := executeGuardOutput output eng trigger;
    updatedEngine :=
      case actionResult of
        | none := none
        | some effect := some eng@Engine{env := ActionEffect.env effect};
  in case updatedEngine of
       | none := none
       | some newEng :=
         case actionResult of
           | none := none
           | some effect :=
             some
               (mkPair
                 (ActionEffect.msgs effect)
                 (mkPair (ActionEffect.engines effect) newEng));

Engine Dispatcher¶

The large dispatcher function that handles evaluation and execution for all engine types in the system.

evaluateAndExecuteEng
  (eng : Eng)
  (msg : EngineMsg Msg)
  : Option (Pair (List (EngineMsg Msg)) (Pair (List (Pair Cfg Env)) Eng)) :=
  case eng of
    | Eng.IdentityManagement e :=
      case evaluateAndExecute e msg of {
        | none := none
        | some (mkPair msgs (mkPair cfgEnvPairs newEng)) :=
          some
            (mkPair msgs (mkPair cfgEnvPairs (Eng.IdentityManagement newEng)))
      }
    | Eng.Decryption e :=
      case evaluateAndExecute e msg of {
        | none := none
        | some (mkPair msgs (mkPair cfgEnvPairs newEng)) :=
          some (mkPair msgs (mkPair cfgEnvPairs (Eng.Decryption newEng)))
      }
    | Eng.Encryption e :=
      case evaluateAndExecute e msg of {
        | none := none
        | some (mkPair msgs (mkPair cfgEnvPairs newEng)) :=
          some (mkPair msgs (mkPair cfgEnvPairs (Eng.Encryption newEng)))
      }
    | Eng.Commitment e :=
      case evaluateAndExecute e msg of {
        | none := none
        | some (mkPair msgs (mkPair cfgEnvPairs newEng)) :=
          some (mkPair msgs (mkPair cfgEnvPairs (Eng.Commitment newEng)))
      }
    | Eng.Verification e :=
      case evaluateAndExecute e msg of {
        | none := none
        | some (mkPair msgs (mkPair cfgEnvPairs newEng)) :=
          some (mkPair msgs (mkPair cfgEnvPairs (Eng.Verification newEng)))
      }
    | Eng.ReadsFor e :=
      case evaluateAndExecute e msg of {
        | none := none
        | some (mkPair msgs (mkPair cfgEnvPairs newEng)) :=
          some (mkPair msgs (mkPair cfgEnvPairs (Eng.ReadsFor newEng)))
      }
    | Eng.SignsFor e :=
      case evaluateAndExecute e msg of {
        | none := none
        | some (mkPair msgs (mkPair cfgEnvPairs newEng)) :=
          some (mkPair msgs (mkPair cfgEnvPairs (Eng.SignsFor newEng)))
      }
    | Eng.Naming e :=
      case evaluateAndExecute e msg of {
        | none := none
        | some (mkPair msgs (mkPair cfgEnvPairs newEng)) :=
          some (mkPair msgs (mkPair cfgEnvPairs (Eng.Naming newEng)))
      }
    | Eng.LocalKeyValueStorage e :=
      case evaluateAndExecute e msg of {
        | none := none
        | some (mkPair msgs (mkPair cfgEnvPairs newEng)) :=
          some
            (mkPair msgs (mkPair cfgEnvPairs (Eng.LocalKeyValueStorage newEng)))
      }
    | Eng.Logging e :=
      case evaluateAndExecute e msg of {
        | none := none
        | some (mkPair msgs (mkPair cfgEnvPairs newEng)) :=
          some (mkPair msgs (mkPair cfgEnvPairs (Eng.Logging newEng)))
      }
    | Eng.WallClock e :=
      case evaluateAndExecute e msg of {
        | none := none
        | some (mkPair msgs (mkPair cfgEnvPairs newEng)) :=
          some (mkPair msgs (mkPair cfgEnvPairs (Eng.WallClock newEng)))
      }
    | Eng.LocalTSeries e :=
      case evaluateAndExecute e msg of {
        | none := none
        | some (mkPair msgs (mkPair cfgEnvPairs newEng)) :=
          some (mkPair msgs (mkPair cfgEnvPairs (Eng.LocalTSeries newEng)))
      }
    | Eng.Router e :=
      case evaluateAndExecute e msg of {
        | none := none
        | some (mkPair msgs (mkPair cfgEnvPairs newEng)) :=
          some (mkPair msgs (mkPair cfgEnvPairs (Eng.Router newEng)))
      }
    | Eng.TransportProtocol e :=
      case evaluateAndExecute e msg of {
        | none := none
        | some (mkPair msgs (mkPair cfgEnvPairs newEng)) :=
          some (mkPair msgs (mkPair cfgEnvPairs (Eng.TransportProtocol newEng)))
      }
    | Eng.TransportConnection e :=
      case evaluateAndExecute e msg of {
        | none := none
        | some (mkPair msgs (mkPair cfgEnvPairs newEng)) :=
          some
            (mkPair msgs (mkPair cfgEnvPairs (Eng.TransportConnection newEng)))
      }
    | Eng.PubSubTopic e :=
      case evaluateAndExecute e msg of {
        | none := none
        | some (mkPair msgs (mkPair cfgEnvPairs newEng)) :=
          some (mkPair msgs (mkPair cfgEnvPairs (Eng.PubSubTopic newEng)))
      }
    | Eng.Storage e :=
      case evaluateAndExecute e msg of {
        | none := none
        | some (mkPair msgs (mkPair cfgEnvPairs newEng)) :=
          some (mkPair msgs (mkPair cfgEnvPairs (Eng.Storage newEng)))
      }
    | Eng.MempoolWorker e :=
      case evaluateAndExecute e msg of {
        | none := none
        | some (mkPair msgs (mkPair cfgEnvPairs newEng)) :=
          some (mkPair msgs (mkPair cfgEnvPairs (Eng.MempoolWorker newEng)))
      }
    | Eng.Executor e :=
      case evaluateAndExecute e msg of {
        | none := none
        | some (mkPair msgs (mkPair cfgEnvPairs newEng)) :=
          some (mkPair msgs (mkPair cfgEnvPairs (Eng.Executor newEng)))
      }
    | Eng.Shard e :=
      case evaluateAndExecute e msg of {
        | none := none
        | some (mkPair msgs (mkPair cfgEnvPairs newEng)) :=
          some (mkPair msgs (mkPair cfgEnvPairs (Eng.Shard newEng)))
      }
    | Eng.Ticker e :=
      case evaluateAndExecute e msg of {
        | none := none
        | some (mkPair msgs (mkPair cfgEnvPairs newEng)) :=
          some (mkPair msgs (mkPair cfgEnvPairs (Eng.Ticker newEng)))
      }
    | Eng.Template e :=
      case evaluateAndExecute e msg of {
        | none := none
        | some (mkPair msgs (mkPair cfgEnvPairs newEng)) :=
          some (mkPair msgs (mkPair cfgEnvPairs (Eng.Template newEng)))
      }
    | Eng.TemplateMinimum e :=
      case evaluateAndExecute e msg of
        | none := none
        | some (mkPair msgs (mkPair cfgEnvPairs newEng)) :=
          some (mkPair msgs (mkPair cfgEnvPairs (Eng.TemplateMinimum newEng)));

Network State Management¶

Functions for managing network state updates, including adding new engines and updating existing ones.

addNewEngine
  (state : NetworkState)
  (nodeId : NodeID)
  (cfg : Cfg)
  (env : Env)
  : NetworkState :=
  case OMap.lookup nodeId (NetworkState.nodes state) of
    | none := state
    | some node :=
      case mkEng nodeId (mkPair cfg env) of
        | none := state
        | some (mkPair newEng newEngineId) :=
          let
            engineName := snd newEngineId;
            updatedNode :=
              node@Node{engines := OMap.insert
                engineName
                newEng
                (Node.engines node)};
          in state@NetworkState{nodes := OMap.insert
            nodeId
            updatedNode
            (NetworkState.nodes state)};

updateNetworkState
  (state : NetworkState)
  (target : EngineID)
  (eng : Eng)
  (msgs : List (EngineMsg Msg))
  (cfgEnvPairs : List (Pair Cfg Env))
  : NetworkState :=
  let
    nodeId :=
      case target of
        | mkPair none _ := none
        | mkPair (some nid) _ := some nid;
    engineName := snd target;
    state' :=
      case nodeId of
        | none := state
        | some nid :=
          case OMap.lookup nid (NetworkState.nodes state) of
            | none := state
            | some n :=
              state@NetworkState{nodes := OMap.insert
                nid
                n@Node{engines := OMap.insert engineName eng (Node.engines n)}
                (NetworkState.nodes state)};
    stateWithMessages :=
      state'@NetworkState{messages := NetworkState.messages state ++ msgs};
    finalState :=
      foldl
        \{s (mkPair cfg env) :=
          case nodeId of
            | none := s
            | some nid := addNewEngine s nid cfg env}
        stateWithMessages
        cfgEnvPairs;
  in finalState;

Core Simulation Logic¶

The main step function and simulation loops for processing messages and running the simulation.

step
  (selector : MessageSelector)
  (state : NetworkState)
  : Pair NetworkState (Option (EngineMsg Msg)) :=
  let
    selected := selector (NetworkState.messages state);
  in case selected of
       | none := mkPair state none
       | some (mkPair msg rest) :=
         let
           state' := state@NetworkState{messages := rest};
           target := EngineMsg.target msg;
           nodeId :=
             case target of
               | mkPair none _ := none
               | mkPair (some nid) _ := some nid;
           engineName := snd target;
           engine :=
             case nodeId of
               | none := none
               | some nid :=
                 case OMap.lookup nid (NetworkState.nodes state) of
                   | none := none
                   | some n := OMap.lookup engineName (Node.engines n);
         in case engine of
              | none := mkPair state' none
              | some eng :=
                let
                  result := evaluateAndExecuteEng eng msg;
                in case result of
                     | none := mkPair state' none
                     | some (mkPair msgs (mkPair cfgEnvPairs newEng)) :=
                       mkPair
                         (updateNetworkState
                           state'
                           target
                           newEng
                           msgs
                           cfgEnvPairs)
                         (some msg);

terminating
simulate
  (selector : MessageSelector)
  (state : NetworkState)
  (steps : Nat)
  : List (EngineMsg Msg) :=
  case steps of
    | zero := []
    | suc n :=
      let
        nextPair := step selector state;
        newState := fst nextPair;
        processedMsgOpt := snd nextPair;
        restMsgs := simulate selector newState n;
      in case processedMsgOpt of
           | none := restMsgs
           | some processedMsg := processedMsg :: restMsgs;

terminating
simulateWithFailures
  (selector : MessageSelector)
  (state : NetworkState)
  (steps : Nat)
  : Pair (List (EngineMsg Msg)) (List (EngineMsg Msg)) :=
  case steps of
    | zero := mkPair [] []
    | suc n :=
      let
        selected := selector (NetworkState.messages state);
      in case selected of
           | none :=
             let
               recursiveResult := simulateWithFailures selector state n;
             in recursiveResult
           | some (mkPair msg rest) :=
             let
               state' := state@NetworkState{messages := rest};
               nextPair := step selector state;
               newState := fst nextPair;
               processedMsgOpt := snd nextPair;
               recursiveResult := simulateWithFailures selector newState n;
               successMsgs := fst recursiveResult;
               failedMsgs := snd recursiveResult;
             in case processedMsgOpt of
                  | none := mkPair successMsgs (msg :: failedMsgs)
                  | some processedMsg :=
                    mkPair (processedMsg :: successMsgs) failedMsgs;