Juvix imports
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.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;
Verification Behaviour¶
Overview¶
The behavior of the Verification Engine defines how it processes incoming verification requests and produces the corresponding responses.
Action arguments¶
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.
VerificationActionArgument¶
type VerificationActionArgument := VerificationActionArgumentReplyTo ReplyTo;
VerificationActionArguments¶
VerificationActionArguments : Type := List VerificationActionArgument;
Actions¶
Auxiliary Juvix code
VerificationAction¶
VerificationAction : Type :=
Action
VerificationCfg
VerificationLocalState
VerificationMailboxState
VerificationTimerHandle
VerificationActionArguments
Anoma.Msg
Anoma.Cfg
Anoma.Env;
VerificationActionInput¶
VerificationActionInput : Type :=
ActionInput
VerificationCfg
VerificationLocalState
VerificationMailboxState
VerificationTimerHandle
VerificationActionArguments
Anoma.Msg;
VerificationActionEffect¶
VerificationActionEffect : Type :=
ActionEffect
VerificationLocalState
VerificationMailboxState
VerificationTimerHandle
Anoma.Msg
Anoma.Cfg
Anoma.Env;
VerificationActionExec¶
VerificationActionExec : Type :=
ActionExec
VerificationCfg
VerificationLocalState
VerificationMailboxState
VerificationTimerHandle
VerificationActionArguments
Anoma.Msg
Anoma.Cfg
Anoma.Env;
verifyAction¶
Verify a commitment.
- State update
- If
useSignsForis true, the state is updated to store pending requests. Otherwise, the state remains unchanged. - Messages to be sent
- If
useSignsForis false, aResponseVerificationmessage is sent back to the requester. IfuseSignsForis true and it's the first request for this identity, aQuerySignsForEvidenceRequestis sent to the SignsFor Engine. - Engines to be spawned
- No engines are created by this action.
- Timer updates
- No timers are set or cancelled.
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 :=
some
mkActionEffect@{
env := env;
msgs :=
[
mkEngineMsg@{
sender := getEngineIDFromEngineCfg cfg;
target := EngineMsg.sender emsg;
mailbox := some 0;
msg :=
Anoma.MsgVerification
(MsgVerificationResponse
(mkResponseVerification
(Verifier.verify
(VerificationCfg.verifier
(EngineCfg.cfg cfg)
Set.empty
externalIdentity)
(VerificationCfg.backend
(EngineCfg.cfg cfg))
data
commitment)
none));
};
];
timers := [];
engines := [];
}
| 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};
in some
mkActionEffect@{
env := newEnv;
msgs :=
case existingRequests of
| some _ := []
| none :=
[
mkEngineMsg@{
sender := getEngineIDFromEngineCfg cfg;
target :=
VerificationCfg.signsForEngineAddress
(EngineCfg.cfg cfg);
mailbox := some 0;
msg :=
Anoma.MsgSignsFor
(MsgQuerySignsForEvidenceRequest
(mkRequestQuerySignsForEvidence
externalIdentity));
};
];
timers := [];
engines := [];
}
}
| _ := none
}
| _ := none;
handleSignsForResponseAction¶
Process a signs-for response and handle pending requests.
- State update
- The state is updated to remove the processed pending requests for the given external identity.
- Messages to be sent
ResponseVerificationmessages are sent to all requesters who were waiting for this SignsFor evidence.- Engines to be spawned
- No engines are created by this action.
- Timer updates
- No timers are set or cancelled.
handleSignsForResponseAction
(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 (MsgQuerySignsForEvidenceResponse (mkResponseQuerySignsForEvidence 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);
in mkEngineMsg@{
sender := getEngineIDFromEngineCfg cfg;
target := whoAsked;
mailbox := some 0;
msg :=
Anoma.MsgVerification
(MsgVerificationResponse
(mkResponseVerification
(Verifier.verify
(VerificationCfg.verifier
(EngineCfg.cfg cfg)
evidence
externalIdentity)
(VerificationCfg.backend
(EngineCfg.cfg cfg))
data
commitment)
none));
}}
reqs;
timers := [];
engines := [];
}
| none :=
some
mkActionEffect@{
env := env;
msgs := [];
timers := [];
engines := [];
}
}
| _ := none
}
| _ := none;
Action Labels¶
verifyActionLabel¶
verifyActionLabel : VerificationActionExec := Seq [verifyAction];
handleSignsForResponseActionLabel¶
handleSignsForResponseActionLabel : VerificationActionExec :=
Seq [handleSignsForResponseAction];
Guards¶
Auxiliary Juvix code
VerificationGuard¶
VerificationGuard : Type :=
Guard
VerificationCfg
VerificationLocalState
VerificationMailboxState
VerificationTimerHandle
VerificationActionArguments
Anoma.Msg
Anoma.Cfg
Anoma.Env;
VerificationGuardOutput¶
VerificationGuardOutput : Type :=
GuardOutput
VerificationCfg
VerificationLocalState
VerificationMailboxState
VerificationTimerHandle
VerificationActionArguments
Anoma.Msg
Anoma.Cfg
Anoma.Env;
VerificationGuardEval¶
VerificationGuardEval : Type :=
GuardEval
VerificationCfg
VerificationLocalState
VerificationMailboxState
VerificationTimerHandle
VerificationActionArguments
Anoma.Msg
Anoma.Cfg
Anoma.Env;
verifyGuard¶
- Condition
- Message type is
VerificationRequest.
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;
signsForResponseGuard¶
- Condition
- Message is a signs-for response from the SignsFor engine.
signsForResponseGuard
(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 (MsgQuerySignsForEvidenceResponse _);
sender := sender;
} :=
case
isEqual
(Ord.cmp
sender
(VerificationCfg.signsForEngineAddress (EngineCfg.cfg cfg)))
of {
| true :=
some
mkGuardOutput@{
action := handleSignsForResponseActionLabel;
args := [];
}
| false := none
}
| _ := none
}
| none := none;
The Verification Behaviour¶
VerificationBehaviour¶
VerificationBehaviour : Type :=
EngineBehaviour
VerificationCfg
VerificationLocalState
VerificationMailboxState
VerificationTimerHandle
VerificationActionArguments
Anoma.Msg
Anoma.Cfg
Anoma.Env;
Instantiation¶
verificationBehaviour : VerificationBehaviour :=
mkEngineBehaviour@{
guards := First [verifyGuard; signsForResponseGuard];
};
Verification Action Flowchart¶
verifyAction flowchart¶
flowchart TD
CM>MsgVerificationRequest]
SC{useSignsFor?}
ES[(Update pending requests)]
MSG1>Response to requester]
MSG2>Request to SignsFor Engine]
CM --verifyGuard--> SC
SC --false --> MSG1
SC --true--> ES
ES --> MSG2verifyAction flowchart
handleSignsForResponseAction flowchart¶
flowchart TD
CM>MsgQuerySignsForEvidenceResponse]
ES[(Remove pending requests)]
MSG>Responses to requesters]
CM --signsForResponseGuard--> ES --> MSGhandleSignsForResponseAction flowchart