module arch.node.engines.reads_for_behaviour;

import prelude open;
import arch.node.types.messages open;
import arch.node.types.engine open;
import arch.node.types.identities open;
import arch.node.engines.reads_for_messages open;
import arch.node.engines.reads_for_config open;
import arch.node.engines.reads_for_environment open;
import arch.node.types.anoma as Anoma open;

Reads For Behaviour¶

Overview¶

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

Action arguments¶

ReadsForActionArgumentReplyTo ReplyTo¶

type ReplyTo :=
  mkReplyTo@{
    whoAsked : Option EngineID;
    mailbox : Option MailboxID;
  };

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

whoAsked:

is the address of the engine that sent the message.

mailbox:

is the mailbox ID where the response should be sent.

ReadsForActionArgument¶

type ReadsForActionArgument := ReadsForActionArgumentReplyTo ReplyTo;

ReadsForActionArguments¶

ReadsForActionArguments : Type := List ReadsForActionArgument;

Actions¶

ReadsForAction : Type :=
  Action
    ReadsForCfg
    ReadsForLocalState
    ReadsForMailboxState
    ReadsForTimerHandle
    ReadsForActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

ReadsForActionInput : Type :=
  ActionInput
    ReadsForCfg
    ReadsForLocalState
    ReadsForMailboxState
    ReadsForTimerHandle
    ReadsForActionArguments
    Anoma.Msg;

ReadsForActionEffect : Type :=
  ActionEffect
    ReadsForLocalState
    ReadsForMailboxState
    ReadsForTimerHandle
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

ReadsForActionExec : Type :=
  ActionExec
    ReadsForCfg
    ReadsForLocalState
    ReadsForMailboxState
    ReadsForTimerHandle
    ReadsForActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

readsForQueryAction¶

Process a reads for query and respond with whether the relationship exists.

State update

The state remains unchanged.

Messages to be sent

A ResponseReadsFor 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.

readsForQueryAction
  (input : ReadsForActionInput) : Option ReadsForActionEffect :=
  let
    env := ActionInput.env input;
    tt := ActionInput.trigger input;
    cfg := ActionInput.cfg input;
    localState := EngineEnv.localState env;
  in case getEngineMsgFromTimestampedTrigger tt of
       | some emsg :=
         case emsg of {
           | mkEngineMsg@{
               msg := Anoma.MsgReadsFor (MsgReadsForRequest (mkRequestReadsFor identityA identityB));
             } :=
             let
               hasEvidence :=
                 isElement
                   \{a b := a && b}
                   true
                   (map
                     \{evidence :=
                       isEqual
                           (Ord.cmp
                             (ReadsForEvidence.fromIdentity evidence)
                             identityA)
                         && isEqual
                           (Ord.cmp
                             (ReadsForEvidence.toIdentity evidence)
                             identityB)}
                     (Set.toList
                       (ReadsForLocalState.evidenceStore localState)));
               responseMsg :=
                 mkResponseReadsFor@{
                   readsFor := hasEvidence;
                   err := none;
                 };
             in some
               mkActionEffect@{
                 env := env;
                 msgs :=
                   [
                     mkEngineMsg@{
                       sender := getEngineIDFromEngineCfg cfg;
                       target := EngineMsg.sender emsg;
                       mailbox := some 0;
                       msg :=
                         Anoma.MsgReadsFor (MsgReadsForResponse responseMsg);
                     };
                   ];
                 timers := [];
                 engines := [];
               }
           | _ := none
         }
       | _ := none;

submitEvidenceAction¶

Process submission of new reads for evidence.

State update

If the evidence is valid and doesn't exist, it's added to the evidence store.

Messages to be sent

A ResponseSubmitReadsForEvidence 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.

submitEvidenceAction
  (input : ReadsForActionInput) : Option ReadsForActionEffect :=
  let
    env := ActionInput.env input;
    tt := ActionInput.trigger input;
    cfg := ActionInput.cfg input;
    localState := EngineEnv.localState env;
  in case getEngineMsgFromTimestampedTrigger tt of
       | some emsg :=
         case emsg of {
           | mkEngineMsg@{
               msg := Anoma.MsgReadsFor (MsgSubmitReadsForEvidenceRequest (mkRequestSubmitReadsForEvidence evidence));
             } :=
             case verifyEvidence evidence of {
               | true :=
                 case
                   isElement
                     \{a b := a && b}
                     true
                     (map
                       \{e := isEqual (Ord.cmp e evidence)}
                       (Set.toList
                         (ReadsForLocalState.evidenceStore localState)))
                 of {
                   | true :=
                     some
                       mkActionEffect@{
                         env := env;
                         msgs :=
                           [
                             mkEngineMsg@{
                               sender := getEngineIDFromEngineCfg cfg;
                               target := EngineMsg.sender emsg;
                               mailbox := some 0;
                               msg :=
                                 Anoma.MsgReadsFor
                                   (MsgSubmitReadsForEvidenceResponse
                                     (mkResponseSubmitReadsForEvidence
                                       (some "Evidence already exists.")));
                             };
                           ];
                         timers := [];
                         engines := [];
                       }
                   | false :=
                     let
                       newEvidenceStore :=
                         Set.insert
                           evidence
                           (ReadsForLocalState.evidenceStore localState);
                       updatedLocalState :=
                         localState@ReadsForLocalState{evidenceStore := newEvidenceStore};
                       newEnv := env@EngineEnv{localState := updatedLocalState};
                     in some
                       mkActionEffect@{
                         env := newEnv;
                         msgs :=
                           [
                             mkEngineMsg@{
                               sender := getEngineIDFromEngineCfg cfg;
                               target := EngineMsg.sender emsg;
                               mailbox := some 0;
                               msg :=
                                 Anoma.MsgReadsFor
                                   (MsgSubmitReadsForEvidenceResponse
                                     (mkResponseSubmitReadsForEvidence none));
                             };
                           ];
                         timers := [];
                         engines := [];
                       }
                 }
               | false :=
                 some
                   mkActionEffect@{
                     env := env;
                     msgs :=
                       [
                         mkEngineMsg@{
                           sender := getEngineIDFromEngineCfg cfg;
                           target := EngineMsg.sender emsg;
                           mailbox := some 0;
                           msg :=
                             Anoma.MsgReadsFor
                               (MsgSubmitReadsForEvidenceResponse
                                 (mkResponseSubmitReadsForEvidence
                                   (some "Invalid evidence provided.")));
                         };
                       ];
                     timers := [];
                     engines := [];
                   }
             }
           | _ := none
         }
       | _ := none;

queryEvidenceAction¶

Query all evidence related to a specific identity.

State update

The state remains unchanged.

Messages to be sent

A ResponseQueryReadsForEvidence 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.

queryEvidenceAction
  (input : ReadsForActionInput) : Option ReadsForActionEffect :=
  let
    env := ActionInput.env input;
    tt := ActionInput.trigger input;
    cfg := ActionInput.cfg input;
    localState := EngineEnv.localState env;
  in case getEngineMsgFromTimestampedTrigger tt of
       | some emsg :=
         case emsg of {
           | mkEngineMsg@{
               msg := Anoma.MsgReadsFor (MsgQueryReadsForEvidenceRequest (mkRequestQueryReadsForEvidence identity));
             } :=
             let
               relevantEvidence :=
                 AVLTree.filter
                   \{evidence :=
                     isEqual
                         (Ord.cmp
                           (ReadsForEvidence.fromIdentity evidence)
                           identity)
                       || isEqual
                         (Ord.cmp
                           (ReadsForEvidence.toIdentity evidence)
                           identity)}
                   (ReadsForLocalState.evidenceStore localState);
               responseMsg :=
                 mkResponseQueryReadsForEvidence@{
                   externalIdentity := identity;
                   evidence := relevantEvidence;
                   err := none;
                 };
             in some
               mkActionEffect@{
                 env := env;
                 msgs :=
                   [
                     mkEngineMsg@{
                       sender := getEngineIDFromEngineCfg cfg;
                       target := EngineMsg.sender emsg;
                       mailbox := some 0;
                       msg :=
                         Anoma.MsgReadsFor
                           (MsgQueryReadsForEvidenceResponse responseMsg);
                     };
                   ];
                 timers := [];
                 engines := [];
               }
           | _ := none
         }
       | _ := none;

Action Labels¶

readsForQueryActionLabel¶

readsForQueryActionLabel : ReadsForActionExec := Seq [readsForQueryAction];

submitEvidenceActionLabel¶

submitEvidenceActionLabel : ReadsForActionExec := Seq [submitEvidenceAction];

queryEvidenceActionLabel¶

queryEvidenceActionLabel : ReadsForActionExec := Seq [queryEvidenceAction];

Guards¶

ReadsForGuard : Type :=
  Guard
    ReadsForCfg
    ReadsForLocalState
    ReadsForMailboxState
    ReadsForTimerHandle
    ReadsForActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

ReadsForGuardOutput : Type :=
  GuardOutput
    ReadsForCfg
    ReadsForLocalState
    ReadsForMailboxState
    ReadsForTimerHandle
    ReadsForActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

ReadsForGuardEval : Type :=
  GuardEval
    ReadsForCfg
    ReadsForLocalState
    ReadsForMailboxState
    ReadsForTimerHandle
    ReadsForActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

readsForQueryGuard¶

Condition

Message type is MsgReadsForRequest.

readsForQueryGuard
  (tt : TimestampedTrigger ReadsForTimerHandle Anoma.Msg)
  (cfg : EngineCfg ReadsForCfg)
  (env : ReadsForEnv)
  : Option ReadsForGuardOutput :=
  case getEngineMsgFromTimestampedTrigger tt of
    | some mkEngineMsg@{msg := Anoma.MsgReadsFor (MsgReadsForRequest _)} :=
      some
        mkGuardOutput@{
          action := readsForQueryActionLabel;
          args := [];
        }
    | _ := none;

submitEvidenceGuard¶

Condition

Message type is MsgSubmitReadsForEvidenceRequest.

submitEvidenceGuard
  (tt : TimestampedTrigger ReadsForTimerHandle Anoma.Msg)
  (cfg : EngineCfg ReadsForCfg)
  (env : ReadsForEnv)
  : Option ReadsForGuardOutput :=
  case getEngineMsgFromTimestampedTrigger tt of
    | some mkEngineMsg@{
             msg := Anoma.MsgReadsFor (MsgSubmitReadsForEvidenceRequest _);
           } :=
      some
        mkGuardOutput@{
          action := submitEvidenceActionLabel;
          args := [];
        }
    | _ := none;

queryEvidenceGuard¶

Condition

Message type is MsgQueryReadsForEvidenceRequest.

queryEvidenceGuard
  (tt : TimestampedTrigger ReadsForTimerHandle Anoma.Msg)
  (cfg : EngineCfg ReadsForCfg)
  (env : ReadsForEnv)
  : Option ReadsForGuardOutput :=
  case getEngineMsgFromTimestampedTrigger tt of
    | some mkEngineMsg@{
             msg := Anoma.MsgReadsFor (MsgQueryReadsForEvidenceRequest _);
           } :=
      some
        mkGuardOutput@{
          action := queryEvidenceActionLabel;
          args := [];
        }
    | _ := none;

The Reads For Behaviour¶

ReadsForBehaviour¶

ReadsForBehaviour : Type :=
  EngineBehaviour
    ReadsForCfg
    ReadsForLocalState
    ReadsForMailboxState
    ReadsForTimerHandle
    ReadsForActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

Instantiation¶

readsForBehaviour : ReadsForBehaviour :=
  mkEngineBehaviour@{
    guards :=
      First [readsForQueryGuard; submitEvidenceGuard; queryEvidenceGuard];
  };

Reads For Action Flowcharts¶

readsForQueryAction flowchart¶

flowchart TD
  subgraph C[Conditions]
    CMsg>MsgReadsForRequest]
  end

  G(readsForQueryGuard)
  A(readsForQueryAction)

  C --> G -- *readsForQueryActionLabel* --> A --> E

  subgraph E[Effects]
    EMsg>ResponseReadsFor<br/>readsFor]
  end

submitEvidenceAction flowchart¶

flowchart TD
  subgraph C[Conditions]
    CMsg>MsgSubmitReadsForEvidenceRequest]
  end

  G(submitEvidenceGuard)
  A(submitEvidenceAction)

  C --> G -- *submitEvidenceActionLabel* --> A --> E

  subgraph E[Effects]
    EEnv[(evidenceStore update)]
    EMsg>ResponseSubmitReadsForEvidence<br/>error]
  end

queryEvidenceAction flowchart¶

flowchart TD
  subgraph C[Conditions]
    CMsg>MsgQueryReadsForEvidenceRequest]
  end

  G(queryEvidenceGuard)
  A(queryEvidenceAction)

  C --> G -- *queryEvidenceActionLabel* --> A --> E

  subgraph E[Effects]
    EMsg>ResponseQueryReadsForEvidence<br/>evidence list]
  end