Increment Simulation Example¶

This example demonstrates a simulation of a simple network performing an increment-and-write operation distributed across multiple engines. It involves:

One Mempool Worker engine to coordinate transactions.
Two Shard engines, managing keys "a" (97) and "b" (98) respectively.
Two initial transactions: 1. Write the value 3 to key "a". 2. Read the value from "a", increment it, and write the result to "b".
Nockma programs for each transaction, executed via the nockmaRunnable.

The simulation uses the selectFirstMessage strategy and illustrates the interaction flow between the client (initiating transactions), the Mempool Worker, Shards, and Executors.

Juvix Code

module arch.node.integration.examples.increment;

import prelude open;
import Stdlib.Prelude as IO;
import arch.node.types.basics open;
import arch.node.types.messages open;
import arch.node.types.identities open;
import arch.node.types.engine_config open;
import arch.node.types.engine_environment open;
import arch.node.types.engine_behaviour open;
import arch.node.types.engine open;
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;
import arch.node.integration.simulator open;
import arch.node.integration.visualizer open;
import arch.node.engines.mempool_worker_config open;
import arch.node.engines.mempool_worker_messages open;
import arch.node.engines.mempool_worker_environment open;
import arch.node.engines.mempool_worker_behaviour open;
import arch.node.engines.shard_config open;
import arch.node.engines.shard_environment open;
import arch.node.engines.shard_behaviour open;
import arch.node.engines.executor_config open;
import arch.node.engines.executor_environment open;
import arch.node.engines.executor_behaviour open;
import arch.system.state.resource_machine.notes.nockma open;
import arch.system.state.resource_machine.notes.runnable open;
import arch.system.state.resource_machine.notes.nockma_runnable open;

zeroNoun : Noun := Noun.Atom 0;

oneNoun : Noun := Noun.Atom 1;

keyA : Noun := Noun.Atom 97;

keyB : Noun := Noun.Atom 98;

val3 : Noun := Noun.Atom 3;

writeAOutputNoun : Noun :=
  Noun.Cell (Noun.Atom 0) (Noun.Cell (Noun.Cell keyA val3) zeroNoun);

writeAProgram : Noun := Noun.Cell oneNoun writeAOutputNoun;

incWriteProgram : Noun :=
  let
    const0 : Noun := Noun.Cell (Noun.Atom 1) (Noun.Atom 0);
    const98 : Noun := Noun.Cell (Noun.Atom 1) (Noun.Atom 98);
    getVal : Noun := Noun.Cell (Noun.Atom 0) (Noun.Atom 7);
    incVal : Noun := Noun.Cell (Noun.Atom 4) getVal;
    writePair : Noun := Noun.Cell const98 incVal;
    reqList : Noun := Noun.Cell writePair const0;
  in Noun.Cell const0 reqList;

initialState : Noun := Noun.Atom 0;

storage : Storage Nat Nat := emptyStorage;

initialGas : Nat := 1000;

externalInput1 : Noun := Noun.Cell (Noun.Atom 0) (Noun.Atom 0);

subject1 : Noun := Noun.Cell initialState externalInput1;

prog1Result : Result String (Pair Noun Nat) :=
  GasState.runGasState
    (nock storage (Noun.Cell subject1 writeAProgram))
    initialGas;

externalInput2 : Noun := Noun.Cell (Noun.Atom 97) (Noun.Atom 3);

subject2 : Noun := Noun.Cell initialState externalInput2;

prog2Result : Result String (Pair Noun Nat) :=
  GasState.runGasState
    (nock storage (Noun.Cell subject2 incWriteProgram))
    initialGas;

nodeId : NodeID := PublicKey.Curve25519PubKey "0xSIMNODE";

shardAId : EngineID := mkPair (some nodeId) "shardA";

shardBId : EngineID := mkPair (some nodeId) "shardB";

mempoolWorkerId : EngineID := mkPair (some nodeId) "mempoolWorker";

keyToShardMap (k : KVSKey) : EngineID :=
  if 
    | k == 97 := shardAId
    | k == 98 := shardBId
    | else := shardAId;

mempoolWorkerLocalCfg : MempoolWorkerLocalCfg :=
  MempoolWorkerLocalCfg.mk@{
    keyToShard := keyToShardMap;
  };

mempoolWorkerCfg : MempoolWorkerCfg :=
  EngineCfg.mk@{
    node := nodeId;
    name := "mempoolWorker";
    cfg := mempoolWorkerLocalCfg;
  };

mempoolWorkerEnv : MempoolWorkerEnv :=
  mempool_worker_environment_example.mempoolWorkerEnv;

mempoolWorker : Eng :=
  Eng.MempoolWorker
    Engine.mk@{
      cfg := mempoolWorkerCfg;
      env := mempoolWorkerEnv;
      behaviour := mempoolWorkerBehaviour;
    };

shardACfg : ShardCfg :=
  EngineCfg.mk@{
    node := nodeId;
    name := "shardA";
    cfg := ShardLocalCfg.mk;
  };

shardAEnv : ShardEnv := shard_environment_example.shardEnv;

shardA : Eng :=
  Eng.Shard
    Engine.mk@{
      cfg := shardACfg;
      env := shardAEnv;
      behaviour := shardBehaviour;
    };

shardBCfg : ShardCfg :=
  EngineCfg.mk@{
    node := nodeId;
    name := "shardB";
    cfg := ShardLocalCfg.mk;
  };

shardBEnv : ShardEnv := shard_environment_example.shardEnv;

shardB : Eng :=
  Eng.Shard
    Engine.mk@{
      cfg := shardBCfg;
      env := shardBEnv;
      behaviour := shardBehaviour;
    };

initialNode : Node :=
  Node.mkNode@{
    engines :=
      OMap.fromList
        [
          mkPair (snd mempoolWorkerId) mempoolWorker;
          mkPair (snd shardAId) shardA;
          mkPair (snd shardBId) shardB;
        ];
  };

txWriteA : TransactionCandidate KVSKey KVSKey Executable :=
  TransactionCandidate.mkTransactionCandidate@{
    label :=
      TransactionLabel.mkTransactionLabel@{
        read := [97];
        write := [97];
      };
    executable := writeAProgram;
  };

txIncWrite : TransactionCandidate KVSKey KVSKey Executable :=
  TransactionCandidate.mkTransactionCandidate@{
    label :=
      TransactionLabel.mkTransactionLabel@{
        read := [97];
        write := [98];
      };
    executable := incWriteProgram;
  };

clientSenderId : EngineID := mkPair none "client";

initialMessages : List (EngineMsg Msg) :=
  [
    EngineMsg.mk@{
      sender := clientSenderId;
      target := mempoolWorkerId;
      mailbox := none;
      msg :=
        Msg.MempoolWorker
          (MempoolWorkerMsg.TransactionRequest
            TransactionRequest.mkTransactionRequest@{
              tx := txWriteA;
              resubmission := none;
            });
    };
    EngineMsg.mk@{
      sender := clientSenderId;
      target := mempoolWorkerId;
      mailbox := none;
      msg :=
        Msg.MempoolWorker
          (MempoolWorkerMsg.TransactionRequest
            TransactionRequest.mkTransactionRequest@{
              tx := txIncWrite;
              resubmission := none;
            });
    };
  ];

initialNetworkState : NetworkState :=
  NetworkState.mkNetworkState@{
    nodes := OMap.singleton nodeId initialNode;
    messages := initialMessages;
    currentTime := left 0;
    incrementId := \{n := n};
    nextId := nodeId;
  };

simulationResult : String :=
  prettyPrintMessageList (simulate selectFirstMessage initialNetworkState 20);

simulationResult2 : Pair (List (EngineMsg Msg)) (List (EngineMsg Msg)) :=
  simulateWithFailures selectFirstMessage initialNetworkState 20;

main : IO.IO := IO.printStringLn simulationResult;

This setup defines the necessary components, initial state, and transaction logic using Nockma Nouns. The simulation is executed, and the resulting message trace is stored in simulationResult.