module arch.node.engines.signs_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.signs_for_environment open;
import arch.node.engines.signs_for_messages open;
import arch.node.engines.signs_for_config open;
import arch.node.types.anoma as Anoma open;

Signs For Behaviour¶

Overview¶

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

Action arguments¶

SignsForActionArgumentReplyTo 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:

The engine ID of the requester.

mailbox:

The mailbox ID where the response should be sent.

SignsForActionArgument¶

type SignsForActionArgument := SignsForActionArgumentReplyTo ReplyTo;

SignsForActionArguments¶

SignsForActionArguments : Type := List SignsForActionArgument;

Actions¶

SignsForAction : Type :=
  Action
    SignsForCfg
    SignsForLocalState
    SignsForMailboxState
    SignsForTimerHandle
    SignsForActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

SignsForActionInput : Type :=
  ActionInput
    SignsForCfg
    SignsForLocalState
    SignsForMailboxState
    SignsForTimerHandle
    SignsForActionArguments
    Anoma.Msg;

SignsForActionEffect : Type :=
  ActionEffect
    SignsForLocalState
    SignsForMailboxState
    SignsForTimerHandle
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

SignsForActionExec : Type :=
  ActionExec
    SignsForCfg
    SignsForLocalState
    SignsForMailboxState
    SignsForTimerHandle
    SignsForActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

signsForQueryAction¶

Respond to a signs_for query.

State update

The state remains unchanged.

Messages to be sent

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

signsForQueryAction
  (input : SignsForActionInput) : Option SignsForActionEffect :=
  let
    env := ActionInput.env input;
    cfg := ActionInput.cfg input;
    tt := ActionInput.trigger input;
    localState := EngineEnv.localState env;
  in case getEngineMsgFromTimestampedTrigger tt of
       | some mkEngineMsg@{
                msg := Anoma.MsgSignsFor (MsgSignsForRequest (mkRequestSignsFor externalIdentityA externalIdentityB));
                sender := msgSender;
              } :=
         let
           hasEvidence :=
             isElement
               \{a b := a && b}
               true
               (map
                 \{evidence :=
                   isEqual
                       (Ord.cmp
                         (SignsForEvidence.fromIdentity evidence)
                         externalIdentityA)
                     && isEqual
                       (Ord.cmp
                         (SignsForEvidence.toIdentity evidence)
                         externalIdentityB)}
                 (Set.toList (SignsForLocalState.evidenceStore localState)));
           responseMsg :=
             mkResponseSignsFor@{
               signsFor := hasEvidence;
               err := none;
             };
         in some
           mkActionEffect@{
             env := env;
             msgs :=
               [
                 mkEngineMsg@{
                   sender := getEngineIDFromEngineCfg cfg;
                   target := msgSender;
                   mailbox := some 0;
                   msg := Anoma.MsgSignsFor (MsgSignsForResponse responseMsg);
                 };
               ];
             timers := [];
             engines := [];
           }
       | _ := none;

submitEvidenceAction¶

Submit new signs_for evidence.

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 ResponseSubmitSignsForEvidence 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 : SignsForActionInput) : Option SignsForActionEffect :=
  let
    env := ActionInput.env input;
    cfg := ActionInput.cfg input;
    tt := ActionInput.trigger input;
    localState := EngineEnv.localState env;
  in case getEngineMsgFromTimestampedTrigger tt of
       | some mkEngineMsg@{
                msg := Anoma.MsgSignsFor (MsgSubmitSignsForEvidenceRequest (mkRequestSubmitSignsForEvidence evidence));
                sender := msgSender;
              } :=
         case verifyEvidence evidence of {
           | true :=
             let
               alreadyExists :=
                 isElement
                   \{a b := a && b}
                   true
                   (map
                     \{e := isEqual (Ord.cmp e evidence)}
                     (Set.toList
                       (SignsForLocalState.evidenceStore localState)));
             in case alreadyExists of {
                  | true :=
                    let
                      responseMsg :=
                        mkResponseSubmitSignsForEvidence@{
                          err := some "Evidence already exists.";
                        };
                    in some
                      mkActionEffect@{
                        env := env;
                        msgs :=
                          [
                            mkEngineMsg@{
                              sender := getEngineIDFromEngineCfg cfg;
                              target := msgSender;
                              mailbox := some 0;
                              msg :=
                                Anoma.MsgSignsFor
                                  (MsgSubmitSignsForEvidenceResponse
                                    responseMsg);
                            };
                          ];
                        timers := [];
                        engines := [];
                      }
                  | false :=
                    let
                      newEvidenceStore :=
                        Set.insert
                          evidence
                          (SignsForLocalState.evidenceStore localState);
                      updatedLocalState :=
                        localState@SignsForLocalState{evidenceStore := newEvidenceStore};
                      newEnv := env@EngineEnv{localState := updatedLocalState};
                      responseMsg :=
                        mkResponseSubmitSignsForEvidence@{
                          err := none;
                        };
                    in some
                      mkActionEffect@{
                        env := newEnv;
                        msgs :=
                          [
                            mkEngineMsg@{
                              sender := getEngineIDFromEngineCfg cfg;
                              target := msgSender;
                              mailbox := some 0;
                              msg :=
                                Anoma.MsgSignsFor
                                  (MsgSubmitSignsForEvidenceResponse
                                    responseMsg);
                            };
                          ];
                        timers := [];
                        engines := [];
                      }
                }
           | false :=
             let
               responseMsg :=
                 mkResponseSubmitSignsForEvidence@{
                   err := some "Invalid evidence provided.";
                 };
             in some
               mkActionEffect@{
                 env := env;
                 msgs :=
                   [
                     mkEngineMsg@{
                       sender := getEngineIDFromEngineCfg cfg;
                       target := msgSender;
                       mailbox := some 0;
                       msg :=
                         Anoma.MsgSignsFor
                           (MsgSubmitSignsForEvidenceResponse responseMsg);
                     };
                   ];
                 timers := [];
                 engines := [];
               }
         }
       | _ := none;

queryEvidenceAction¶

Query signs_for evidence for a specific identity.

State update

The state remains unchanged.

Messages to be sent

A ResponseQuerySignsForEvidence 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 : SignsForActionInput) : Option SignsForActionEffect :=
  let
    env := ActionInput.env input;
    cfg := ActionInput.cfg input;
    tt := ActionInput.trigger input;
    localState := EngineEnv.localState env;
  in case getEngineMsgFromTimestampedTrigger tt of
       | some mkEngineMsg@{
                msg := Anoma.MsgSignsFor (MsgQuerySignsForEvidenceRequest (mkRequestQuerySignsForEvidence externalIdentity));
                sender := msgSender;
              } :=
         let
           relevantEvidence :=
             AVLTree.filter
               \{evidence :=
                 isEqual
                     (Ord.cmp
                       (SignsForEvidence.fromIdentity evidence)
                       externalIdentity)
                   || isEqual
                     (Ord.cmp
                       (SignsForEvidence.toIdentity evidence)
                       externalIdentity)}
               (SignsForLocalState.evidenceStore localState);
           responseMsg :=
             mkResponseQuerySignsForEvidence@{
               externalIdentity := externalIdentity;
               evidence := relevantEvidence;
               err := none;
             };
         in some
           mkActionEffect@{
             env := env;
             msgs :=
               [
                 mkEngineMsg@{
                   sender := getEngineIDFromEngineCfg cfg;
                   target := msgSender;
                   mailbox := some 0;
                   msg :=
                     Anoma.MsgSignsFor
                       (MsgQuerySignsForEvidenceResponse responseMsg);
                 };
               ];
             timers := [];
             engines := [];
           }
       | _ := none;

Action Labels¶

signsForQueryActionLabel¶

signsForQueryActionLabel : SignsForActionExec := Seq [signsForQueryAction];

submitEvidenceActionLabel¶

submitEvidenceActionLabel : SignsForActionExec := Seq [submitEvidenceAction];

queryEvidenceActionLabel¶

queryEvidenceActionLabel : SignsForActionExec := Seq [queryEvidenceAction];

Guards¶

SignsForGuard : Type :=
  Guard
    SignsForCfg
    SignsForLocalState
    SignsForMailboxState
    SignsForTimerHandle
    SignsForActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

SignsForGuardOutput : Type :=
  GuardOutput
    SignsForCfg
    SignsForLocalState
    SignsForMailboxState
    SignsForTimerHandle
    SignsForActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

SignsForGuardEval : Type :=
  GuardEval
    SignsForCfg
    SignsForLocalState
    SignsForMailboxState
    SignsForTimerHandle
    SignsForActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

signsForQueryGuard¶

Condition

Message type is MsgSignsForRequest.

signsForQueryGuard
  (tt : TimestampedTrigger SignsForTimerHandle Anoma.Msg)
  (cfg : EngineCfg SignsForCfg)
  (env : SignsForEnv)
  : Option SignsForGuardOutput :=
  case getEngineMsgFromTimestampedTrigger tt of
    | some mkEngineMsg@{msg := Anoma.MsgSignsFor (MsgSignsForRequest _)} :=
      some
        mkGuardOutput@{
          action := signsForQueryActionLabel;
          args := [];
        }
    | _ := none;

submitEvidenceGuard¶

Condition

Message type is MsgSubmitSignsForEvidenceRequest.

submitEvidenceGuard
  (tt : TimestampedTrigger SignsForTimerHandle Anoma.Msg)
  (cfg : EngineCfg SignsForCfg)
  (env : SignsForEnv)
  : Option SignsForGuardOutput :=
  case getEngineMsgFromTimestampedTrigger tt of
    | some mkEngineMsg@{
             msg := Anoma.MsgSignsFor (MsgSubmitSignsForEvidenceRequest _);
           } :=
      some
        mkGuardOutput@{
          action := submitEvidenceActionLabel;
          args := [];
        }
    | _ := none;

queryEvidenceGuard¶

Condition

Message type is MsgQuerySignsForEvidenceRequest.

queryEvidenceGuard
  (tt : TimestampedTrigger SignsForTimerHandle Anoma.Msg)
  (cfg : EngineCfg SignsForCfg)
  (env : SignsForEnv)
  : Option SignsForGuardOutput :=
  case getEngineMsgFromTimestampedTrigger tt of
    | some mkEngineMsg@{
             msg := Anoma.MsgSignsFor (MsgQuerySignsForEvidenceRequest _);
           } :=
      some
        mkGuardOutput@{
          action := queryEvidenceActionLabel;
          args := [];
        }
    | _ := none;

The Signs For Behaviour¶

SignsForBehaviour¶

SignsForBehaviour : Type :=
  EngineBehaviour
    SignsForCfg
    SignsForLocalState
    SignsForMailboxState
    SignsForTimerHandle
    SignsForActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

Instantiation¶

signsForBehaviour : SignsForBehaviour :=
  mkEngineBehaviour@{
    guards :=
      First [signsForQueryGuard; submitEvidenceGuard; queryEvidenceGuard];
  };

Signs For Action Flowcharts¶

signsForQueryAction flowchart¶

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

  G(signsForQueryGuard)
  A(signsForQueryAction)

  C --> G -- *signsForQueryActionLabel* --> A --> E

  subgraph E[Effects]
    EMsg>MsgSignsForResponse<br/>signsFor result]
  end

submitEvidenceAction flowchart¶

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

  G(submitEvidenceGuard)
  A(submitEvidenceAction)

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

  subgraph E[Effects]
    EEnv[(evidenceStore update)]
    EMsg>MsgSubmitSignsForEvidenceResponse]
  end

queryEvidenceAction flowchart¶

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

  G(queryEvidenceGuard)
  A(queryEvidenceAction)

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

  subgraph E[Effects]
    EMsg>MsgQuerySignsForEvidenceResponse<br/>matching evidence]
  end