module arch.node.engines.verification_behaviour; import prelude open; import arch.node.types.messages open; import arch.system.identity.identity open hiding {ExternalIdentity}; import arch.node.utils open; import arch.node.types.engine open; import arch.node.engines.verification_config open; import arch.node.engines.verification_environment open; import arch.node.engines.verification_messages open; import arch.node.engines.signs_for_messages open; import arch.node.types.crypto open; import arch.node.types.identities open; import arch.node.types.anoma as Anoma open; type ReplyTo := mkReplyTo@{ whoAsked : Option EngineID; mailbox : Option MailboxID; }; type VerificationActionArgument := | VerificationActionArgumentReplyTo ReplyTo; VerificationActionArguments : Type := List VerificationActionArgument; VerificationAction : Type := Action VerificationCfg VerificationLocalState VerificationMailboxState VerificationTimerHandle VerificationActionArguments Anoma.Msg Anoma.Cfg Anoma.Env; VerificationActionInput : Type := ActionInput VerificationCfg VerificationLocalState VerificationMailboxState VerificationTimerHandle VerificationActionArguments Anoma.Msg; VerificationActionEffect : Type := ActionEffect VerificationLocalState VerificationMailboxState VerificationTimerHandle Anoma.Msg Anoma.Cfg Anoma.Env; VerificationActionExec : Type := ActionExec VerificationCfg VerificationLocalState VerificationMailboxState VerificationTimerHandle VerificationActionArguments Anoma.Msg Anoma.Cfg Anoma.Env; verifyAction (input : VerificationActionInput) : Option VerificationActionEffect := let env := ActionInput.env input; cfg := ActionInput.cfg input; tt := ActionInput.trigger input; localState := EngineEnv.localState env; in case getEngineMsgFromTimestampedTrigger tt of | some emsg := case emsg of { | mkEngineMsg@{ msg := Anoma.MsgVerification (MsgVerificationRequest (mkRequestVerification data commitment externalIdentity useSignsFor)); } := case useSignsFor of { | false := let responseMsg := Anoma.MsgVerification (MsgVerificationReply (mkReplyVerification (Verifier.verify (VerificationCfg.verifier (EngineCfg.cfg cfg) Set.empty externalIdentity) (VerificationCfg.backend (EngineCfg.cfg cfg)) data commitment) none)); in some (defaultReplyActionEffect env cfg (EngineMsg.sender emsg) responseMsg) | true := let existingRequests := Map.lookup externalIdentity (VerificationLocalState.pendingRequests localState); newPendingList := case existingRequests of | some reqs := reqs ++ [ mkPair (EngineMsg.sender emsg) (mkPair data commitment); ] | none := [ mkPair (EngineMsg.sender emsg) (mkPair data commitment); ]; newPendingRequests := Map.insert externalIdentity newPendingList (VerificationLocalState.pendingRequests localState); newLocalState := localState@VerificationLocalState{pendingRequests := newPendingRequests}; newEnv := env@EngineEnv{localState := newLocalState}; responseMsg := Anoma.MsgSignsFor (MsgQuerySignsForEvidenceRequest (mkRequestQuerySignsForEvidence externalIdentity)); in some (defaultReplyActionEffect env cfg (VerificationCfg.signsForEngineAddress (EngineCfg.cfg cfg)) responseMsg) } | _ := none } | _ := none; signsForReplyAction (input : VerificationActionInput) : Option VerificationActionEffect := let env := ActionInput.env input; cfg := ActionInput.cfg input; tt := ActionInput.trigger input; localState := EngineEnv.localState env; in case getEngineMsgFromTimestampedTrigger tt of | some emsg := case emsg of { | mkEngineMsg@{ msg := Anoma.MsgSignsFor (MsgQuerySignsForEvidenceReply (mkReplyQuerySignsForEvidence externalIdentity evidence err)); } := case Map.lookup externalIdentity (VerificationLocalState.pendingRequests localState) of { | some reqs := let newPendingRequests := Map.delete externalIdentity (VerificationLocalState.pendingRequests localState); newLocalState := localState@VerificationLocalState{pendingRequests := newPendingRequests}; newEnv := env@EngineEnv{localState := newLocalState}; in some mkActionEffect@{ env := newEnv; msgs := map \{req := let whoAsked := fst req; data := fst (snd req); commitment := snd (snd req); responseMsg := Anoma.MsgVerification (MsgVerificationReply (mkReplyVerification (Verifier.verify (VerificationCfg.verifier (EngineCfg.cfg cfg) evidence externalIdentity) (VerificationCfg.backend (EngineCfg.cfg cfg)) data commitment) none)); in defaultReplyMsg cfg whoAsked responseMsg} reqs; timers := []; engines := []; } | none := some mkActionEffect@{ env := env; msgs := []; timers := []; engines := []; } } | _ := none } | _ := none; verifyActionLabel : VerificationActionExec := Seq [verifyAction]; signsForReplyActionLabel : VerificationActionExec := Seq [signsForReplyAction]; VerificationGuard : Type := Guard VerificationCfg VerificationLocalState VerificationMailboxState VerificationTimerHandle VerificationActionArguments Anoma.Msg Anoma.Cfg Anoma.Env; VerificationGuardOutput : Type := GuardOutput VerificationCfg VerificationLocalState VerificationMailboxState VerificationTimerHandle VerificationActionArguments Anoma.Msg Anoma.Cfg Anoma.Env; VerificationGuardEval : Type := GuardEval VerificationCfg VerificationLocalState VerificationMailboxState VerificationTimerHandle VerificationActionArguments Anoma.Msg Anoma.Cfg Anoma.Env; verifyGuard (tt : TimestampedTrigger VerificationTimerHandle Anoma.Msg) (cfg : EngineCfg VerificationCfg) (env : VerificationEnv) : Option VerificationGuardOutput := case getEngineMsgFromTimestampedTrigger tt of | some mkEngineMsg@{ msg := Anoma.MsgVerification (MsgVerificationRequest _); } := some mkGuardOutput@{ action := verifyActionLabel; args := []; } | _ := none; signsForReplyGuard (tt : TimestampedTrigger VerificationTimerHandle Anoma.Msg) (cfg : EngineCfg VerificationCfg) (env : VerificationEnv) : Option VerificationGuardOutput := case getEngineMsgFromTimestampedTrigger tt of | some emsg := case emsg of { | mkEngineMsg@{ msg := Anoma.MsgSignsFor (MsgQuerySignsForEvidenceReply _); sender := sender; } := case isEqual (Ord.cmp sender (VerificationCfg.signsForEngineAddress (EngineCfg.cfg cfg))) of { | true := some mkGuardOutput@{ action := signsForReplyActionLabel; args := []; } | false := none } | _ := none } | none := none; VerificationBehaviour : Type := EngineBehaviour VerificationCfg VerificationLocalState VerificationMailboxState VerificationTimerHandle VerificationActionArguments Anoma.Msg Anoma.Cfg Anoma.Env; verificationBehaviour : VerificationBehaviour := mkEngineBehaviour@{ guards := First [verifyGuard; signsForReplyGuard]; };