Juvix imports

module arch.node.engines.signs_for_behaviour;

import prelude open;
import Stdlib.Data.List.Base open;
import Data.Set.AVL open;
import Stdlib.Trait.Ord open;
import Stdlib.Data.Bool.Base open;
import arch.node.types.messages 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.signs_for_environment open;
import arch.node.engines.signs_for_messages open;
import arch.node.types.anoma_message open;

Signs For Dynamics

Overview

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

Action labels

type SignsForActionLabel :=
  | DoSignsForQuery {
      externalIdentityA : ExternalIdentity;
      externalIdentityB : ExternalIdentity
    }
  | DoSubmitEvidence {evidence : SignsForEvidence}
  | DoQueryEvidence {externalIdentity : ExternalIdentity};

DoSignsForQuery

DoSignsForQuery { externalIdentityA : ExternalIdentity; externalIdentityB : ExternalIdentity }

This action label corresponds to processing a signs_for query.

DoSignsForQuery action effect

This action does the following:

Aspect	Description
State update	The state remains unchanged.
Messages to be sent	A SignsForResponse message is sent back to the requester.
Engines to be spawned	No engine is created by this action.
Timer updates	No timers are set or cancelled.

DoSubmitEvidence

DoSubmitEvidence { evidence : SignsForEvidence }

This action label corresponds to submitting new signs_for evidence.

DoSubmitEvidence 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 SubmitSignsForEvidenceResponse message is sent back to the requester.
Engines to be spawned	No engine is created by this action.
Timer updates	No timers are set or cancelled.

DoQueryEvidence

DoQueryEvidence { externalIdentity : ExternalIdentity }

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

DoQueryEvidence action effect

This action does the following:

Aspect	Description
State update	The state remains unchanged.
Messages to be sent	A QuerySignsForEvidenceResponse message is sent back to the requester.
Engines to be spawned	No engine is created by this action.
Timer updates	No timers are set or cancelled.

Matchable arguments

type SignsForMatchableArgument := 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 Signs For Engine does not require any non-trivial pre-computations.

syntax alias SignsForPrecomputation := Unit;

Guards

Auxiliary Juvix code

Type alias for the guard.

SignsForGuard : Type :=
  Guard
    SignsForLocalState
    SignsForMailboxState
    SignsForTimerHandle
    SignsForMatchableArgument
    SignsForActionLabel
    SignsForPrecomputation;

SignsForGuardOutput : Type :=
  GuardOutput
    SignsForMatchableArgument
    SignsForActionLabel
    SignsForPrecomputation;

signsForQueryGuard

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

signsForQueryGuard flowchart

signsForQueryGuard
  (t : TimestampedTrigger SignsForTimerHandle)
  (env : SignsForEnvironment)
  : Option SignsForGuardOutput :=
  case getMessageFromTimestampedTrigger t of
    | some (MsgSignsFor (SignsForRequest x y)) :=
      do {
        sender <- getSenderFromTimestampedTrigger t;
        pure
          mkGuardOutput@{
            matchedArgs := [ReplyTo (some sender) none];
            actionLabel := DoSignsForQuery x y;
            precomputationTasks := unit
          };
      }
    | _ := none;

submitEvidenceGuard

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

submitEvidenceGuard flowchart

submitEvidenceGuard
  (t : TimestampedTrigger SignsForTimerHandle)
  (env : SignsForEnvironment)
  : Option SignsForGuardOutput :=
  case getMessageFromTimestampedTrigger t of
    | some (MsgSignsFor (SubmitSignsForEvidenceRequest x)) :=
      do {
        sender <- getSenderFromTimestampedTrigger t;
        pure
          mkGuardOutput@{
            matchedArgs := [ReplyTo (some sender) none];
            actionLabel := DoSubmitEvidence x;
            precomputationTasks := unit
          };
      }
    | _ := none;

queryEvidenceGuard

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

queryEvidenceGuard flowchart

queryEvidenceGuard
  (t : TimestampedTrigger SignsForTimerHandle)
  (env : SignsForEnvironment)
  : Option SignsForGuardOutput :=
  case getMessageFromTimestampedTrigger t of
    | some (MsgSignsFor (QuerySignsForEvidenceRequest x)) :=
      do {
        sender <- getSenderFromTimestampedTrigger t;
        pure
          mkGuardOutput@{
            matchedArgs := [ReplyTo (some sender) none];
            actionLabel := DoQueryEvidence x;
            precomputationTasks := unit
          };
      }
    | _ := none;

Action function

Auxiliary Juvix code

Type alias for the action function.

SignsForActionInput : Type :=
  ActionInput
    SignsForLocalState
    SignsForMailboxState
    SignsForTimerHandle
    SignsForMatchableArgument
    SignsForActionLabel
    SignsForPrecomputation;

SignsForActionEffect : Type :=
  ActionEffect
    SignsForLocalState
    SignsForMailboxState
    SignsForTimerHandle
    SignsForMatchableArgument
    SignsForActionLabel
    SignsForPrecomputation;

signsForAction (input : SignsForActionInput) : SignsForActionEffect :=
  let
    env := ActionInput.env input;
    out := ActionInput.guardOutput input;
    localState := EngineEnvironment.localState env;
  in case GuardOutput.actionLabel out of
       | DoSignsForQuery externalIdentityA externalIdentityB :=
         case GuardOutput.matchedArgs out of {
           | ReplyTo (some whoAsked) _ :: _ :=
             let
               hasEvidence :=
                 elem
                   \ {a b := a && b}
                   true
                   (map
                     \ {evidence :=
                       isEQ
                           (Ord.cmp
                             (SignsForEvidence.fromIdentity evidence)
                             externalIdentityA)
                         && isEQ
                           (Ord.cmp
                             (SignsForEvidence.toIdentity evidence)
                             externalIdentityB)}
                     (toList (SignsForLocalState.evidenceStore localState)));
               responseMsg :=
                 SignsForResponse@{
                   signsFor := hasEvidence;
                   err := none
                 };
             in mkActionEffect@{
               newEnv := env;
               producedMessages :=
                 [ mkEngineMessage@{
                   sender := mkPair none (some (EngineEnvironment.name env));
                   target := whoAsked;
                   mailbox := some 0;
                   msg := MsgSignsFor responseMsg
                 }
                 ];
               timers := [];
               spawnedEngines := []
             }
           | _ :=
             mkActionEffect@{
               newEnv := env;
               producedMessages := [];
               timers := [];
               spawnedEngines := []
             }
         }
       | DoSubmitEvidence evidence :=
         case GuardOutput.matchedArgs out of {
           | ReplyTo (some whoAsked) _ :: _ :=
             let
               isValid := SignsForLocalState.verifyEvidence localState evidence;
             in case isValid of {
                  | true :=
                    let
                      alreadyExists :=
                        elem
                          \ {a b := a && b}
                          true
                          (map
                            \ {e := isEQ (Ord.cmp e evidence)}
                            (toList
                              (SignsForLocalState.evidenceStore localState)));
                    in case alreadyExists of {
                         | true :=
                           let
                             responseMsg :=
                               SubmitSignsForEvidenceResponse@{
                                 err := some "Evidence already exists."
                               };
                           in mkActionEffect@{
                             newEnv := env;
                             producedMessages :=
                               [ mkEngineMessage@{
                                 sender :=
                                   mkPair
                                     none
                                     (some (EngineEnvironment.name env));
                                 target := whoAsked;
                                 mailbox := some 0;
                                 msg := MsgSignsFor responseMsg
                               }
                               ];
                             timers := [];
                             spawnedEngines := []
                           }
                         | false :=
                           let
                             newEvidenceStore :=
                               Set.insert
                                 evidence
                                 (SignsForLocalState.evidenceStore localState);
                             updatedLocalState :=
                               localState@SignsForLocalState{evidenceStore := newEvidenceStore};
                             newEnv' :=
                               env@EngineEnvironment{localState := updatedLocalState};
                             responseMsg :=
                               SubmitSignsForEvidenceResponse@{
                                 err := none
                               };
                           in mkActionEffect@{
                             newEnv := newEnv';
                             producedMessages :=
                               [ mkEngineMessage@{
                                 sender :=
                                   mkPair
                                     none
                                     (some (EngineEnvironment.name env));
                                 target := whoAsked;
                                 mailbox := some 0;
                                 msg := MsgSignsFor responseMsg
                               }
                               ];
                             timers := [];
                             spawnedEngines := []
                           }
                       }
                  | false :=
                    let
                      responseMsg :=
                        SubmitSignsForEvidenceResponse@{
                          err := some "Invalid evidence provided."
                        };
                    in mkActionEffect@{
                      newEnv := env;
                      producedMessages :=
                        [ mkEngineMessage@{
                          sender :=
                            mkPair none (some (EngineEnvironment.name env));
                          target := whoAsked;
                          mailbox := some 0;
                          msg := MsgSignsFor responseMsg
                        }
                        ];
                      timers := [];
                      spawnedEngines := []
                    }
                }
           | _ :=
             mkActionEffect@{
               newEnv := env;
               producedMessages := [];
               timers := [];
               spawnedEngines := []
             }
         }
       | DoQueryEvidence externalIdentity' :=
         case GuardOutput.matchedArgs out of
           | ReplyTo (some whoAsked) _ :: _ :=
             let
               relevantEvidence :=
                 AVLfilter
                   \ {evidence :=
                     isEQ
                         (Ord.cmp
                           (SignsForEvidence.fromIdentity evidence)
                           externalIdentity')
                       || isEQ
                         (Ord.cmp
                           (SignsForEvidence.toIdentity evidence)
                           externalIdentity')}
                   (SignsForLocalState.evidenceStore localState);
               responseMsg :=
                 QuerySignsForEvidenceResponse@{
                   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 := MsgSignsFor responseMsg
                 }
                 ];
               timers := [];
               spawnedEngines := []
             }
           | _ :=
             mkActionEffect@{
               newEnv := env;
               producedMessages := [];
               timers := [];
               spawnedEngines := []
             };

Conflict solver

signsForConflictSolver
  : Set SignsForMatchableArgument -> List (Set SignsForMatchableArgument)
  | _ := [];

SignsForBehaviour type

SignsForBehaviour : Type :=
  EngineBehaviour
    SignsForLocalState
    SignsForMailboxState
    SignsForTimerHandle
    SignsForMatchableArgument
    SignsForActionLabel
    SignsForPrecomputation;

SignsForBehaviour instance

signsForBehaviour : SignsForBehaviour :=
  mkEngineBehaviour@{
    guards := [signsForQueryGuard; submitEvidenceGuard; queryEvidenceGuard];
    action := signsForAction;
    conflictSolver := signsForConflictSolver
  };