module arch.node.engines.reads_for_behaviour; import prelude open; import arch.node.utils 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; type ReplyTo := mkReplyTo@{ whoAsked : Option EngineID; mailbox : Option MailboxID; }; type ReadsForActionArgument := | ReadsForActionArgumentReplyTo ReplyTo; ReadsForActionArguments : Type := List ReadsForActionArgument; 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 (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 := Anoma.MsgReadsFor (MsgReadsForReply mkReplyReadsFor@{ readsFor := hasEvidence; err := none; }); in some (defaultReplyActionEffect env cfg (EngineMsg.sender emsg) responseMsg) | _ := none } | _ := none; 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 (defaultReplyActionEffect env cfg (EngineMsg.sender emsg) (Anoma.MsgReadsFor (MsgSubmitReadsForEvidenceReply (mkReplySubmitReadsForEvidence (some "Evidence already exists."))))) | false := let newEvidenceStore := Set.insert evidence (ReadsForLocalState.evidenceStore localState); updatedLocalState := localState@ReadsForLocalState{evidenceStore := newEvidenceStore}; newEnv := env@EngineEnv{localState := updatedLocalState}; responseMsg := Anoma.MsgReadsFor (MsgSubmitReadsForEvidenceReply (mkReplySubmitReadsForEvidence none)); in some (defaultReplyActionEffect newEnv cfg (EngineMsg.sender emsg) responseMsg) } | false := some (defaultReplyActionEffect env cfg (EngineMsg.sender emsg) (Anoma.MsgReadsFor (MsgSubmitReadsForEvidenceReply (mkReplySubmitReadsForEvidence (some "Invalid evidence provided."))))) } | _ := none } | _ := none; 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 := Anoma.MsgReadsFor (MsgQueryReadsForEvidenceReply mkReplyQueryReadsForEvidence@{ externalIdentity := identity; evidence := relevantEvidence; err := none; }); in some (defaultReplyActionEffect env cfg (EngineMsg.sender emsg) responseMsg) | _ := none } | _ := none; readsForQueryActionLabel : ReadsForActionExec := Seq [readsForQueryAction]; submitEvidenceActionLabel : ReadsForActionExec := Seq [submitEvidenceAction]; queryEvidenceActionLabel : ReadsForActionExec := Seq [queryEvidenceAction]; 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 (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 (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 (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; ReadsForBehaviour : Type := EngineBehaviour ReadsForCfg ReadsForLocalState ReadsForMailboxState ReadsForTimerHandle ReadsForActionArguments Anoma.Msg Anoma.Cfg Anoma.Env; readsForBehaviour : ReadsForBehaviour := mkEngineBehaviour@{ guards := First [readsForQueryGuard; submitEvidenceGuard; queryEvidenceGuard]; };