Juvix imports

module arch.node.engines.naming_behaviour;

import prelude open;
import arch.node.types.messages open;
import Data.Set.AVL open;
import Stdlib.Data.List.Base open;
import Stdlib.Trait.Ord open;
import Stdlib.Data.Bool.Base open;
import arch.node.types.engine_behaviour open;
import arch.node.types.engine_environment open;
import arch.node.types.identities open;
import arch.node.engines.naming_messages open;
import arch.node.engines.naming_environment open;
import arch.node.types.anoma_message open;

Naming Dynamics

Overview

The behavior of the Naming Engine define how it processes incoming messages and updates its state accordingly.

Action labels

type NamingActionLabel :=
  | DoResolveName {identityName : IdentityName}
  | DoSubmitNameEvidence {evidence : IdentityNameEvidence}
  | DoQueryNameEvidence {externalIdentity : ExternalIdentity};

DoResolveName

DoResolveName { identityName : IdentityName }

This action label corresponds to resolving a name to associated external identities.

DoResolveName action effect

This action does the following:

Aspect	Description
State update	No change to the local state.
Messages to be sent	A ResolveNameResponse message is sent to the requester, containing matching external identities.
Engines to be spawned	No engines are spawned by this action.
Timer updates	No timers are set or cancelled.

DoSubmitNameEvidence

DoSubmitNameEvidence { evidence : IdentityNameEvidence }

This action label corresponds to submitting new name evidence.

DoSubmitNameEvidence action effect

This action does the following:

Aspect	Description
State update	If the evidence doesn't already exist and is valid, it's added to the evidenceStore in the local state.
Messages to be sent	A SubmitNameEvidenceResponse message is sent to the requester, confirming the submission or indicating an error if the evidence already exists.
Engines to be spawned	No engines are spawned by this action.
Timer updates	No timers are set or cancelled.

DoQueryNameEvidence

DoQueryNameEvidence { externalIdentity : ExternalIdentity }

This action label corresponds to querying name evidence for a specific external identity.

DoQueryNameEvidence action effect

This action does the following:

Aspect	Description
State update	No change to the local state.
Messages to be sent	A QueryNameEvidenceResponse message is sent to the requester, containing relevant evidence for the specified external identity.
Engines to be spawned	No engines are spawned by this action.
Timer updates	No timers are set or cancelled.

Matchable arguments

type NamingMatchableArgument := ReplyTo (Option EngineID) (Option MailboxID);

ReplyTo

ReplyTo (Option EngineID) (Option MailboxID)

This matchable argument contains the address and mailbox ID of where the response message should be sent.

Precomputation results

The Naming Engine does not require any non-trivial pre-computations.

syntax alias NamingPrecomputation := Unit;

Guards

Auxiliary Juvix code

Type alias for the guard.

NamingGuard : Type :=
  Guard
    NamingLocalState
    NamingMailboxState
    NamingTimerHandle
    NamingMatchableArgument
    NamingActionLabel
    NamingPrecomputation;

NamingGuardOutput : Type :=
  GuardOutput NamingMatchableArgument NamingActionLabel NamingPrecomputation;

resolveNameGuard

flowchart TD
    C{ResolveNameRequest<br>received?}
    C -->|Yes| D[enabled]
    C -->|No| E[not enabled]
    D --> F([DoResolveName])

resolveNameGuard flowchart

resolveNameGuard
  (t : TimestampedTrigger NamingTimerHandle)
  (env : NamingEnvironment)
  : Option NamingGuardOutput :=
  case getMessageFromTimestampedTrigger t of
    | some (MsgNaming (ResolveNameRequest x)) :=
      do {
        sender <- getSenderFromTimestampedTrigger t;
        pure
          mkGuardOutput@{
            matchedArgs := [ReplyTo (some sender) none];
            actionLabel := DoResolveName x;
            precomputationTasks := unit
          };
      }
    | _ := none;

submitNameEvidenceGuard

flowchart TD
    C{SubmitNameEvidenceRequest<br>received?}
    C -->|Yes| D[enabled]
    C -->|No| E[not enabled]
    D --> F([DoSubmitNameEvidence])

submitNameEvidenceGuard flowchart

submitNameEvidenceGuard
  (t : TimestampedTrigger NamingTimerHandle)
  (env : NamingEnvironment)
  : Option NamingGuardOutput :=
  case getMessageFromTimestampedTrigger t of
    | some (MsgNaming (SubmitNameEvidenceRequest x)) :=
      do {
        sender <- getSenderFromTimestampedTrigger t;
        pure
          mkGuardOutput@{
            matchedArgs := [ReplyTo (some sender) none];
            actionLabel := DoSubmitNameEvidence x;
            precomputationTasks := unit
          };
      }
    | _ := none;

queryNameEvidenceGuard

flowchart TD
    C{QueryNameEvidenceRequest<br>received?}
    C -->|Yes| D[enabled]
    C -->|No| E[not enabled]
    D --> F([DoQueryNameEvidence])

queryNameEvidenceGuard flowchart

queryNameEvidenceGuard
  (t : TimestampedTrigger NamingTimerHandle)
  (env : NamingEnvironment)
  : Option NamingGuardOutput :=
  case getMessageFromTimestampedTrigger t of
    | some (MsgNaming (QueryNameEvidenceRequest x)) :=
      do {
        sender <- getSenderFromTimestampedTrigger t;
        pure
          mkGuardOutput@{
            matchedArgs := [ReplyTo (some sender) none];
            actionLabel := DoQueryNameEvidence x;
            precomputationTasks := unit
          };
      }
    | _ := none;

Action function

Auxiliary Juvix code

Type alias for the action function.

NamingActionInput : Type :=
  ActionInput
    NamingLocalState
    NamingMailboxState
    NamingTimerHandle
    NamingMatchableArgument
    NamingActionLabel
    NamingPrecomputation;

NamingActionEffect : Type :=
  ActionEffect
    NamingLocalState
    NamingMailboxState
    NamingTimerHandle
    NamingMatchableArgument
    NamingActionLabel
    NamingPrecomputation;

namingAction (input : NamingActionInput) : NamingActionEffect :=
  let
    env := ActionInput.env input;
    out := ActionInput.guardOutput input;
    localState := EngineEnvironment.localState env;
  in case GuardOutput.actionLabel out of
       | DoResolveName identityName :=
         case GuardOutput.matchedArgs out of {
           | ReplyTo (some whoAsked) _ :: _ :=
             let
               matchingEvidence :=
                 AVLfilter
                   \ {evidence :=
                     isEQ
                       (Ord.cmp
                         (IdentityNameEvidence.identityName evidence)
                         identityName)}
                   (NamingLocalState.evidenceStore localState);
               identities :=
                 fromList
                   (map
                     \ {evidence :=
                       IdentityNameEvidence.externalIdentity evidence}
                     (toList matchingEvidence));
               responseMsg :=
                 ResolveNameResponse@{
                   externalIdentities := identities;
                   err := none
                 };
             in mkActionEffect@{
               newEnv := env;
               producedMessages :=
                 [ mkEngineMessage@{
                   sender := mkPair none (some (EngineEnvironment.name env));
                   target := whoAsked;
                   mailbox := some 0;
                   msg := MsgNaming responseMsg
                 }
                 ];
               timers := [];
               spawnedEngines := []
             }
           | _ :=
             mkActionEffect@{
               newEnv := env;
               producedMessages := [];
               timers := [];
               spawnedEngines := []
             }
         }
       | DoSubmitNameEvidence evidence' :=
         case GuardOutput.matchedArgs out of {
           | ReplyTo (some whoAsked) _ :: _ :=
             let
               evidence := evidence';
               isValid := NamingLocalState.verifyEvidence localState evidence;
             in case isValid of {
                  | false :=
                    let
                      responseMsg :=
                        SubmitNameEvidenceResponse@{
                          err := some "Invalid evidence"
                        };
                    in mkActionEffect@{
                      newEnv := env;
                      producedMessages :=
                        [ mkEngineMessage@{
                          sender :=
                            mkPair none (some (EngineEnvironment.name env));
                          target := whoAsked;
                          mailbox := some 0;
                          msg := MsgNaming responseMsg
                        }
                        ];
                      timers := [];
                      spawnedEngines := []
                    }
                  | true :=
                    let
                      alreadyExists :=
                        elem
                          \ {a b := a && b}
                          true
                          (map
                            \ {e := isEQ (Ord.cmp e evidence)}
                            (toList
                              (NamingLocalState.evidenceStore localState)));
                      newLocalState :=
                        case alreadyExists of
                          | true := localState
                          | false :=
                            let
                              newEvidenceStore :=
                                Set.insert
                                  evidence
                                  (NamingLocalState.evidenceStore localState);
                            in localState@NamingLocalState{evidenceStore := newEvidenceStore};
                      newEnv' :=
                        env@EngineEnvironment{localState := newLocalState};
                      responseMsg :=
                        SubmitNameEvidenceResponse@{
                          err :=
                            case alreadyExists of
                              | true := some "Evidence already exists"
                              | false := none
                        };
                    in mkActionEffect@{
                      newEnv := newEnv';
                      producedMessages :=
                        [ mkEngineMessage@{
                          sender :=
                            mkPair none (some (EngineEnvironment.name env));
                          target := whoAsked;
                          mailbox := some 0;
                          msg := MsgNaming responseMsg
                        }
                        ];
                      timers := [];
                      spawnedEngines := []
                    }
                }
           | _ :=
             mkActionEffect@{
               newEnv := env;
               producedMessages := [];
               timers := [];
               spawnedEngines := []
             }
         }
       | DoQueryNameEvidence externalIdentity' :=
         case GuardOutput.matchedArgs out of
           | ReplyTo (some whoAsked) _ :: _ :=
             let
               relevantEvidence :=
                 AVLfilter
                   \ {evidence :=
                     isEQ
                       (Ord.cmp
                         (IdentityNameEvidence.externalIdentity evidence)
                         externalIdentity')}
                   (NamingLocalState.evidenceStore localState);
               responseMsg :=
                 QueryNameEvidenceResponse@{
                   externalIdentity := externalIdentity';
                   evidence := relevantEvidence;
                   err := none
                 };
             in mkActionEffect@{
               newEnv := env;
               producedMessages :=
                 [ mkEngineMessage@{
                   sender := mkPair none (some (EngineEnvironment.name env));
                   target := whoAsked;
                   mailbox := some 0;
                   msg := MsgNaming responseMsg
                 }
                 ];
               timers := [];
               spawnedEngines := []
             }
           | _ :=
             mkActionEffect@{
               newEnv := env;
               producedMessages := [];
               timers := [];
               spawnedEngines := []
             };

Conflict solver

namingConflictSolver
  : Set NamingMatchableArgument -> List (Set NamingMatchableArgument)
  | _ := [];

NamingBehaviour type

NamingBehaviour : Type :=
  EngineBehaviour
    NamingLocalState
    NamingMailboxState
    NamingTimerHandle
    NamingMatchableArgument
    NamingActionLabel
    NamingPrecomputation;

NamingBehaviour instance

namingBehaviour : NamingBehaviour :=
  mkEngineBehaviour@{
    guards :=
      [resolveNameGuard; submitNameEvidenceGuard; queryNameEvidenceGuard];
    action := namingAction;
    conflictSolver := namingConflictSolver
  };