feat: add engine simulator with message passing and pretty printing (#355)

Implements a simulator function that steps from an initial network
state, delivering messages and accumulating the delivered messages in a
list, which can be processed into, for example, a message passing
diagram.

Also implements a nockma runnable instance and fixed bugs associated
with sim implementaion.

---------

Co-authored-by: Jonathan Cubides <[email protected]>

Author: AHartNtkn

docs/arch/node/engines/commitment.juvix.md

@@ -60,7 +60,7 @@ maintaining the security of the underlying signing keys.
 ```juvix
 CommitmentEngine : Type :=
   Engine
-    CommitmentCfg
+    CommitmentLocalCfg
     CommitmentLocalState
     CommitmentMailboxState
     CommitmentTimerHandle

docs/arch/node/engines/commitment_behaviour.juvix.md

@@ -158,7 +158,7 @@ CommitmentActionArguments : Type := List CommitmentActionArgument;
     ```juvix
     CommitmentAction : Type :=
       Action
-        CommitmentCfg
+        CommitmentLocalCfg
         CommitmentLocalState
         CommitmentMailboxState
         CommitmentTimerHandle
@@ -175,7 +175,7 @@ CommitmentActionArguments : Type := List CommitmentActionArgument;
     ```juvix
     CommitmentActionInput : Type :=
       ActionInput
-        CommitmentCfg
+        CommitmentLocalCfg
         CommitmentLocalState
         CommitmentMailboxState
         CommitmentTimerHandle
@@ -203,7 +203,7 @@ CommitmentActionArguments : Type := List CommitmentActionArgument;
     ```juvix
     CommitmentActionExec : Type :=
       ActionExec
-        CommitmentCfg
+        CommitmentLocalCfg
         CommitmentLocalState
         CommitmentMailboxState
         CommitmentTimerHandle
@@ -242,11 +242,11 @@ commitAction
     case getEngineMsgFromTimestampedTrigger tt of {
     | some emsg :=
       case emsg of {
-      | EngineMsg.mk@{msg := Anoma.PreMsg.MsgCommitment (CommitmentMsg.Request request)} :=
+      | EngineMsg.mk@{msg := Anoma.Msg.Commitment (CommitmentMsg.Request request)} :=
         let
           signedData := Signer.sign
-            (CommitmentCfg.signer (EngineCfg.cfg cfg))
-            (CommitmentCfg.backend (EngineCfg.cfg cfg))
+            (CommitmentLocalCfg.signer (EngineCfg.cfg cfg))
+            (CommitmentLocalCfg.backend (EngineCfg.cfg cfg))
             (RequestCommitment.data request);
           responseMsg := ReplyCommitment.mkReplyCommitment@{
             commitment := signedData;
@@ -259,7 +259,7 @@ commitAction
               sender := getEngineIDFromEngineCfg cfg;
               target := EngineMsg.sender emsg;
               mailbox := some 0;
-              msg := Anoma.PreMsg.MsgCommitment (CommitmentMsg.Reply responseMsg)
+              msg := Anoma.Msg.Commitment (CommitmentMsg.Reply responseMsg)
             }
           ];
           timers := [];
@@ -292,7 +292,7 @@ commitActionLabel : CommitmentActionExec := ActionExec.Seq [ commitAction ];
     ```juvix
     CommitmentGuard : Type :=
       Guard
-        CommitmentCfg
+        CommitmentLocalCfg
         CommitmentLocalState
         CommitmentMailboxState
         CommitmentTimerHandle
@@ -311,7 +311,7 @@ commitActionLabel : CommitmentActionExec := ActionExec.Seq [ commitAction ];
     ```juvix
     CommitmentGuardOutput : Type :=
       GuardOutput
-        CommitmentCfg
+        CommitmentLocalCfg
         CommitmentLocalState
         CommitmentMailboxState
         CommitmentTimerHandle
@@ -328,7 +328,7 @@ commitActionLabel : CommitmentActionExec := ActionExec.Seq [ commitAction ];
     ```juvix
     CommitmentGuardEval : Type :=
       GuardEval
-        CommitmentCfg
+        CommitmentLocalCfg
         CommitmentLocalState
         CommitmentMailboxState
         CommitmentTimerHandle
@@ -348,12 +348,12 @@ Condition
 ```juvix
 commitGuard
   (tt : TimestampedTrigger CommitmentTimerHandle Anoma.Msg)
-  (cfg : EngineCfg CommitmentCfg)
+  (cfg : CommitmentCfg)
   (env : CommitmentEnv)
   : Option CommitmentGuardOutput :=
   case getEngineMsgFromTimestampedTrigger tt of {
     | some EngineMsg.mk@{
-        msg := Anoma.PreMsg.MsgCommitment (CommitmentMsg.Request _);
+        msg := Anoma.Msg.Commitment (CommitmentMsg.Request _);
       } := some GuardOutput.mk@{
         action := commitActionLabel;
         args := [];
@@ -371,7 +371,7 @@ commitGuard
 ```juvix
 CommitmentBehaviour : Type :=
   EngineBehaviour
-    CommitmentCfg
+    CommitmentLocalCfg
     CommitmentLocalState
     CommitmentMailboxState
     CommitmentTimerHandle

docs/arch/node/engines/commitment_config.juvix.md

@@ -18,6 +18,7 @@ tags:
     import prelude open;
     import arch.node.engines.commitment_messages open;
     import arch.system.identity.identity as Identity;
+    import arch.system.identity.identity as Identity;
     import arch.node.types.engine open;
     import arch.node.types.messages open;
     import arch.node.types.identities open;
@@ -29,20 +30,20 @@ tags:
 
 The commitment engine configuration contains static information for commitment engine instances, namely the signer and the backend.
 
-## The Commitment Configuration
+## The Commitment Local Configuration
 
-The configuration of a Commitment Engine instance includes the identity's signing capabilities.
+### `CommitmentLocalCfg`
 
-### `CommitmentCfg`
+The type for engine-specific local configuration.
 
-<!-- --8<-- [start:CommitmentCfg] -->
+<!-- --8<-- [start:CommitmentLocalCfg] -->
 ```juvix
-type CommitmentCfg := mk@{
+type CommitmentLocalCfg := mk@{
   signer : Identity.Signer Backend Signable Commitment;
   backend : Backend;
 };
 ```
-<!-- --8<-- [end:CommitmentCfg] -->
+<!-- --8<-- [end:CommitmentLocalCfg] -->
 
 ???+ code "Arguments"
 
@@ -52,17 +53,29 @@ type CommitmentCfg := mk@{
     `backend`:
     : The backend to use for signing.
 
+## The Commitment Configuration
+
+### `CommitmentCfg`
+
+<!-- --8<-- [start:CommitmentCfg] -->
+```juvix
+CommitmentCfg : Type :=
+  EngineCfg
+    CommitmentLocalCfg;
+```
+<!-- --8<-- [end:CommitmentCfg] -->
+
 #### Instantiation
 
 <!-- --8<-- [start:commitmentCfg] -->
 ```juvix extract-module-statements
 module commitment_config_example;
 
-  commitmentCfg : EngineCfg CommitmentCfg :=
+  commitmentCfg : CommitmentCfg :=
     EngineCfg.mk@{
       node := PublicKey.Curve25519PubKey "0xabcd1234";
       name := "commitment";
-      cfg := CommitmentCfg.mk@{
+      cfg := CommitmentLocalCfg.mk@{
         signer := Identity.Signer.mkSigner@{
           sign := \{_ x := Signature.Ed25519Signature "0xabcd1234"};
         };

docs/arch/node/engines/decryption.juvix.md

@@ -64,7 +64,7 @@ decryption keys.
 ```juvix
 DecryptionEngine : Type :=
   Engine
-    DecryptionCfg
+    DecryptionLocalCfg
     DecryptionLocalState
     DecryptionMailboxState
     DecryptionTimerHandle

docs/arch/node/engines/decryption_behaviour.juvix.md

@@ -168,7 +168,7 @@ DecryptionActionArguments : Type := List DecryptionActionArgument;
     ```juvix
     DecryptionAction : Type :=
       Action
-        DecryptionCfg
+        DecryptionLocalCfg
         DecryptionLocalState
         DecryptionMailboxState
         DecryptionTimerHandle
@@ -185,7 +185,7 @@ DecryptionActionArguments : Type := List DecryptionActionArgument;
     ```juvix
     DecryptionActionInput : Type :=
       ActionInput
-        DecryptionCfg
+        DecryptionLocalCfg
         DecryptionLocalState
         DecryptionMailboxState
         DecryptionTimerHandle
@@ -215,7 +215,7 @@ DecryptionActionArguments : Type := List DecryptionActionArgument;
     ```juvix
     DecryptionActionExec : Type :=
       ActionExec
-        DecryptionCfg
+        DecryptionLocalCfg
         DecryptionLocalState
         DecryptionMailboxState
         DecryptionTimerHandle
@@ -254,12 +254,12 @@ decryptAction
     case getEngineMsgFromTimestampedTrigger tt of {
     | some emsg :=
       case EngineMsg.msg emsg of {
-      | Anoma.PreMsg.MsgDecryption (DecryptionMsg.Request request) :=
+      | Anoma.Msg.Decryption (DecryptionMsg.Request request) :=
         let
           decryptedData :=
             Decryptor.decrypt
-              (DecryptionCfg.decryptor (EngineCfg.cfg cfg))
-              (DecryptionCfg.backend (EngineCfg.cfg cfg))
+              (DecryptionLocalCfg.decryptor (EngineCfg.cfg cfg))
+              (DecryptionLocalCfg.backend (EngineCfg.cfg cfg))
               (RequestDecryption.data request);
           responseMsg := case decryptedData of {
             | none := ReplyDecryption.mkReplyDecryption@{
@@ -278,7 +278,7 @@ decryptAction
               sender := getEngineIDFromEngineCfg cfg;
               target := EngineMsg.sender emsg;
               mailbox := some 0;
-              msg := Anoma.PreMsg.MsgDecryption (DecryptionMsg.Reply responseMsg)
+              msg := Anoma.Msg.Decryption (DecryptionMsg.Reply responseMsg)
             }
           ];
           timers := [];
@@ -309,7 +309,7 @@ decryptActionLabel : DecryptionActionExec := ActionExec.Seq [ decryptAction ];
     ```juvix
     DecryptionGuard : Type :=
       Guard
-        DecryptionCfg
+        DecryptionLocalCfg
         DecryptionLocalState
         DecryptionMailboxState
         DecryptionTimerHandle
@@ -326,7 +326,7 @@ decryptActionLabel : DecryptionActionExec := ActionExec.Seq [ decryptAction ];
     ```juvix
     DecryptionGuardOutput : Type :=
       GuardOutput
-        DecryptionCfg
+        DecryptionLocalCfg
         DecryptionLocalState
         DecryptionMailboxState
         DecryptionTimerHandle
@@ -345,7 +345,7 @@ decryptActionLabel : DecryptionActionExec := ActionExec.Seq [ decryptAction ];
     ```juvix
     DecryptionGuardEval : Type :=
       GuardEval
-        DecryptionCfg
+        DecryptionLocalCfg
         DecryptionLocalState
         DecryptionMailboxState
         DecryptionTimerHandle
@@ -365,12 +365,12 @@ Condition
 ```juvix
 decryptGuard
   (tt : TimestampedTrigger DecryptionTimerHandle Anoma.Msg)
-  (cfg : EngineCfg DecryptionCfg)
+  (cfg : DecryptionCfg)
   (env : DecryptionEnv)
   : Option DecryptionGuardOutput :=
   case getEngineMsgFromTimestampedTrigger tt of {
     | some EngineMsg.mk@{
-        msg := Anoma.PreMsg.MsgDecryption (DecryptionMsg.Request _);
+        msg := Anoma.Msg.Decryption (DecryptionMsg.Request _);
       } := some GuardOutput.mk@{
         action := decryptActionLabel;
         args := []
@@ -388,7 +388,7 @@ decryptGuard
 ```juvix
 DecryptionBehaviour : Type :=
   EngineBehaviour
-    DecryptionCfg
+    DecryptionLocalCfg
     DecryptionLocalState
     DecryptionMailboxState
     DecryptionTimerHandle

docs/arch/node/engines/decryption_config.juvix.md

@@ -20,6 +20,7 @@ tags:
     import arch.node.types.engine open;
     import arch.node.types.messages open;
     import arch.system.identity.identity as Identity;
+    import arch.system.identity.identity as Identity;
     import arch.node.types.identities open;
     ```
 
@@ -29,21 +30,23 @@ tags:
 
 The decryption engine configuration contains static information for decryption engine instances.
 
-## The Decryption Configuration
+## The Decryption Local Configuration
 
 The configuration of a Decryption Engine instance includes the identity's
 decryption capabilities.
 
-### `DecryptionCfg`
+### `DecryptionLocalCfg`
 
-<!-- --8<-- [start:DecryptionCfg] -->
+The type for engine-specific local configuration.
+
+<!-- --8<-- [start:DecryptionLocalCfg] -->
 ```juvix
-type DecryptionCfg := mk@{
+type DecryptionLocalCfg := mk@{
   decryptor : Identity.Decryptor Backend Plaintext Ciphertext;
   backend : Backend;
 };
 ```
-<!-- --8<-- [end:DecryptionCfg] -->
+<!-- --8<-- [end:DecryptionLocalCfg] -->
 
 ???+ code "Arguments"
 
@@ -53,17 +56,29 @@ type DecryptionCfg := mk@{
     `backend`:
     : The backend to use for decryption.
 
-### Instantiation
+## The Decryption Configuration
+
+### `DecryptionCfg`
+
+<!-- --8<-- [start:DecryptionCfg] -->
+```juvix
+DecryptionCfg : Type :=
+  EngineCfg
+    DecryptionLocalCfg;
+```
+<!-- --8<-- [end:DecryptionCfg] -->
+
+#### Instantiation
 
 <!-- --8<-- [start:decryptionCfg] -->
 ```juvix extract-module-statements
 module decryption_config_example;
 
-  decryptionCfg : EngineCfg DecryptionCfg :=
+  decryptionCfg : DecryptionCfg :=
     EngineCfg.mk@{
       node := PublicKey.Curve25519PubKey "0xabcd1234";
       name := "decryption";
-      cfg := DecryptionCfg.mk@{
+      cfg := DecryptionLocalCfg.mk@{
         decryptor := Identity.Decryptor.mkDecryptor@{
           decrypt := \{_ x := some x};
         };

docs/arch/node/engines/encryption.juvix.md

@@ -80,7 +80,7 @@ recipient, but also to other identities with approved access rights.
 ```juvix
 EncryptionEngine : Type :=
   Engine
-    EncryptionCfg
+    EncryptionLocalCfg
     EncryptionLocalState
     EncryptionMailboxState
     EncryptionTimerHandle