Juvix imports

module arch.node.engines.reads_for_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.reads_for_messages open;
import arch.node.engines.reads_for_environment open;
import arch.node.types.anoma_message open;

Reads For Dynamics

Overview

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

Action labels

type ReadsForActionLabel :=
  | DoReadsForQuery {
      externalIdentityA : ExternalIdentity;
      externalIdentityB : ExternalIdentity
    }
  | DoSubmitEvidence {evidence : ReadsForEvidence}
  | DoQueryEvidence {externalIdentity : ExternalIdentity};

DoReadsForQuery

DoReadsForQuery { externalIdentityA : ExternalIdentity; externalIdentityB : ExternalIdentity }

This action label corresponds to processing a reads_for query.

DoReadsForQuery action effect

This action does the following:

Aspect	Description
State update	The state remains unchanged.
Messages to be sent	A ReadsForResponse 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 : ReadsForEvidence }

This action label corresponds to submitting new reads_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 SubmitReadsForEvidenceResponse 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 reads_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 QueryReadsForEvidenceResponse 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 ReadsForMatchableArgument := 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 Reads For Engine does not require any non-trivial pre-computations.

syntax alias ReadsForPrecomputation := Unit;

Guards

Auxiliary Juvix code

Type alias for the guard.

ReadsForGuard : Type :=
  Guard
    ReadsForLocalState
    ReadsForMailboxState
    ReadsForTimerHandle
    ReadsForMatchableArgument
    ReadsForActionLabel
    ReadsForPrecomputation;

ReadsForGuardOutput : Type :=
  GuardOutput
    ReadsForMatchableArgument
    ReadsForActionLabel
    ReadsForPrecomputation;

readsForQueryGuard

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

readsForQueryGuard flowchart

readsForQueryGuard
  (t : TimestampedTrigger ReadsForTimerHandle)
  (env : ReadsForEnvironment)
  : Option ReadsForGuardOutput :=
  case getMessageFromTimestampedTrigger t of
    | some (MsgReadsFor (ReadsForRequest x y)) :=
      do {
        sender <- getSenderFromTimestampedTrigger t;
        pure
          mkGuardOutput@{
            matchedArgs := [ReplyTo (some sender) none];
            actionLabel := DoReadsForQuery x y;
            precomputationTasks := unit
          };
      }
    | _ := none;

submitEvidenceGuard

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

submitEvidenceGuard flowchart

submitEvidenceGuard
  (t : TimestampedTrigger ReadsForTimerHandle)
  (env : ReadsForEnvironment)
  : Option ReadsForGuardOutput :=
  case getMessageFromTimestampedTrigger t of
    | some (MsgReadsFor (SubmitReadsForEvidenceRequest x)) :=
      do {
        sender <- getSenderFromTimestampedTrigger t;
        pure
          mkGuardOutput@{
            matchedArgs := [ReplyTo (some sender) none];
            actionLabel := DoSubmitEvidence x;
            precomputationTasks := unit
          };
      }
    | _ := none;

queryEvidenceGuard

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

queryEvidenceGuard flowchart

queryEvidenceGuard
  (t : TimestampedTrigger ReadsForTimerHandle)
  (env : ReadsForEnvironment)
  : Option ReadsForGuardOutput :=
  case getMessageFromTimestampedTrigger t of
    | some (MsgReadsFor (QueryReadsForEvidenceRequest 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.

ReadsForActionInput : Type :=
  ActionInput
    ReadsForLocalState
    ReadsForMailboxState
    ReadsForTimerHandle
    ReadsForMatchableArgument
    ReadsForActionLabel
    ReadsForPrecomputation;

ReadsForActionEffect : Type :=
  ActionEffect
    ReadsForLocalState
    ReadsForMailboxState
    ReadsForTimerHandle
    ReadsForMatchableArgument
    ReadsForActionLabel
    ReadsForPrecomputation;

readsForAction (input : ReadsForActionInput) : ReadsForActionEffect :=
  let
    env := ActionInput.env input;
    out := ActionInput.guardOutput input;
    localState := EngineEnvironment.localState env;
  in case GuardOutput.actionLabel out of
       | DoReadsForQuery externalIdentityA externalIdentityB :=
         case GuardOutput.matchedArgs out of {
           | ReplyTo (some whoAsked) _ :: _ :=
             let
               hasEvidence :=
                 elem
                   \ {a b := a && b}
                   true
                   (map
                     \ {evidence :=
                       isEQ
                           (Ord.cmp
                             (ReadsForEvidence.fromIdentity evidence)
                             externalIdentityA)
                         && isEQ
                           (Ord.cmp
                             (ReadsForEvidence.toIdentity evidence)
                             externalIdentityB)}
                     (toList (ReadsForLocalState.evidenceStore localState)));
               responseMsg :=
                 ReadsForResponse@{
                   readsFor := hasEvidence;
                   err := none
                 };
             in mkActionEffect@{
               newEnv := env;
               producedMessages :=
                 [ mkEngineMessage@{
                   sender := mkPair none (some (EngineEnvironment.name env));
                   target := whoAsked;
                   mailbox := some 0;
                   msg := MsgReadsFor responseMsg
                 }
                 ];
               timers := [];
               spawnedEngines := []
             }
           | _ :=
             mkActionEffect@{
               newEnv := env;
               producedMessages := [];
               timers := [];
               spawnedEngines := []
             }
         }
       | DoSubmitEvidence evidence :=
         case GuardOutput.matchedArgs out of {
           | ReplyTo (some whoAsked) _ :: _ :=
             let
               isValid := ReadsForLocalState.verifyEvidence localState evidence;
             in case isValid of {
                  | true :=
                    let
                      alreadyExists :=
                        elem
                          \ {a b := a && b}
                          true
                          (map
                            \ {e := isEQ (Ord.cmp e evidence)}
                            (toList
                              (ReadsForLocalState.evidenceStore localState)));
                    in case alreadyExists of {
                         | true :=
                           let
                             responseMsg :=
                               SubmitReadsForEvidenceResponse@{
                                 err := some "Evidence already exists."
                               };
                           in mkActionEffect@{
                             newEnv := env;
                             producedMessages :=
                               [ mkEngineMessage@{
                                 sender :=
                                   mkPair
                                     none
                                     (some (EngineEnvironment.name env));
                                 target := whoAsked;
                                 mailbox := some 0;
                                 msg := MsgReadsFor responseMsg
                               }
                               ];
                             timers := [];
                             spawnedEngines := []
                           }
                         | false :=
                           let
                             newEvidenceStore :=
                               Set.insert
                                 evidence
                                 (ReadsForLocalState.evidenceStore localState);
                             updatedLocalState :=
                               localState@ReadsForLocalState{evidenceStore := newEvidenceStore};
                             newEnv' :=
                               env@EngineEnvironment{localState := updatedLocalState};
                             responseMsg :=
                               SubmitReadsForEvidenceResponse@{
                                 err := none
                               };
                           in mkActionEffect@{
                             newEnv := newEnv';
                             producedMessages :=
                               [ mkEngineMessage@{
                                 sender :=
                                   mkPair
                                     none
                                     (some (EngineEnvironment.name env));
                                 target := whoAsked;
                                 mailbox := some 0;
                                 msg := MsgReadsFor responseMsg
                               }
                               ];
                             timers := [];
                             spawnedEngines := []
                           }
                       }
                  | false :=
                    let
                      responseMsg :=
                        SubmitReadsForEvidenceResponse@{
                          err := some "Invalid evidence provided."
                        };
                    in mkActionEffect@{
                      newEnv := env;
                      producedMessages :=
                        [ mkEngineMessage@{
                          sender :=
                            mkPair none (some (EngineEnvironment.name env));
                          target := whoAsked;
                          mailbox := some 0;
                          msg := MsgReadsFor 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
                           (ReadsForEvidence.fromIdentity evidence)
                           externalIdentity')
                       || isEQ
                         (Ord.cmp
                           (ReadsForEvidence.toIdentity evidence)
                           externalIdentity')}
                   (ReadsForLocalState.evidenceStore localState);
               responseMsg :=
                 QueryReadsForEvidenceResponse@{
                   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 := MsgReadsFor responseMsg
                 }
                 ];
               timers := [];
               spawnedEngines := []
             }
           | _ :=
             mkActionEffect@{
               newEnv := env;
               producedMessages := [];
               timers := [];
               spawnedEngines := []
             };

Conflict solver

readsForConflictSolver
  : Set ReadsForMatchableArgument -> List (Set ReadsForMatchableArgument)
  | _ := [];

ReadsForBehaviour type

ReadsForBehaviour : Type :=
  EngineBehaviour
    ReadsForLocalState
    ReadsForMailboxState
    ReadsForTimerHandle
    ReadsForMatchableArgument
    ReadsForActionLabel
    ReadsForPrecomputation;

ReadsForBehaviour instance

readsForBehaviour : ReadsForBehaviour :=
  mkEngineBehaviour@{
    guards := [readsForQueryGuard; submitEvidenceGuard; queryEvidenceGuard];
    action := readsForAction;
    conflictSolver := readsForConflictSolver
  };