Juvix imports
module arch.node.engines.commitment_behaviour;
import prelude open;
import arch.system.identity.identity open;
import arch.node.engines.commitment_messages open;
import arch.node.engines.commitment_environment open;
import arch.node.types.anoma_message open;
import arch.node.types.engine_behaviour open;
import arch.node.types.engine_environment open;
import arch.node.types.identities open;
import arch.node.types.messages open;
Commitment
Dynamics¶
Overview¶
The behavior of the Commitment
Engine define how it processes incoming commitment requests and produces the corresponding responses.
Action labels¶
type CommitmentActionLabel := DoCommit {data : Signable};
DoCommit
¶
DoCommit { data : Signable }
This action label corresponds to generating a commitment (signature) for the given request.
DoCommit
action effect
This action does the following:
Aspect | Description |
---|---|
State update | The state remains unchanged. |
Messages to be sent | A CommitResponse 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. |
Matchable arguments¶
type CommitmentMatchableArgument := ReplyTo (Option EngineID) (Option MailboxID);
ReplyTo
¶
ReplyTo (Option EngineID) (Option MailboxID)
This matchable argument contains the address and mailbox ID of where the response message should be sent.
Precomputation results¶
The Commitment Engine does not require any non-trivial pre-computations.
syntax alias CommitmentPrecomputation := Unit;
Guards¶
Auxiliary Juvix code
Type alias for the guard.
CommitmentGuard : Type :=
Guard
CommitmentLocalState
CommitmentMailboxState
CommitmentTimerHandle
CommitmentMatchableArgument
CommitmentActionLabel
CommitmentPrecomputation;
CommitmentGuardOutput : Type :=
GuardOutput
CommitmentMatchableArgument
CommitmentActionLabel
CommitmentPrecomputation;
commitGuard
¶
commitGuard
(t : TimestampedTrigger CommitmentTimerHandle)
(env : CommitmentEnvironment)
: Option CommitmentGuardOutput :=
case getMessageFromTimestampedTrigger t of
| some (MsgCommitment (CommitRequest data)) :=
do {
sender <- getSenderFromTimestampedTrigger t;
pure
mkGuardOutput@{
matchedArgs := [ReplyTo (some sender) none];
actionLabel := DoCommit data;
precomputationTasks := unit
};
}
| _ := none;
Action function¶
Auxiliary Juvix code
Type alias for the action function.
CommitmentActionInput : Type :=
ActionInput
CommitmentLocalState
CommitmentMailboxState
CommitmentTimerHandle
CommitmentMatchableArgument
CommitmentActionLabel
CommitmentPrecomputation;
CommitmentActionEffect : Type :=
ActionEffect
CommitmentLocalState
CommitmentMailboxState
CommitmentTimerHandle
CommitmentMatchableArgument
CommitmentActionLabel
CommitmentPrecomputation;
commitmentAction (input : CommitmentActionInput) : CommitmentActionEffect :=
let
env := ActionInput.env input;
out := ActionInput.guardOutput input;
localState := EngineEnvironment.localState env;
in case GuardOutput.actionLabel out of
DoCommit data :=
case GuardOutput.matchedArgs out of
| ReplyTo (some whoAsked) _ :: _ :=
let
signedData :=
Signer.sign
(CommitmentLocalState.signer localState)
(CommitmentLocalState.backend localState)
data;
responseMsg :=
CommitResponse@{
commitment := signedData;
err := none
};
in mkActionEffect@{
newEnv := env;
producedMessages :=
[ mkEngineMessage@{
sender := mkPair none (some (EngineEnvironment.name env));
target := whoAsked;
mailbox := some 0;
msg := MsgCommitment responseMsg
}
];
timers := [];
spawnedEngines := []
}
| _ :=
mkActionEffect@{
newEnv := env;
producedMessages := [];
timers := [];
spawnedEngines := []
};
Conflict solver¶
commitmentConflictSolver
: Set CommitmentMatchableArgument -> List (Set CommitmentMatchableArgument)
| _ := [];
CommitmentBehaviour type¶
CommitmentBehaviour : Type :=
EngineBehaviour
CommitmentLocalState
CommitmentMailboxState
CommitmentTimerHandle
CommitmentMatchableArgument
CommitmentActionLabel
CommitmentPrecomputation;
CommitmentBehaviour instance¶
commitmentBehaviour : CommitmentBehaviour :=
mkEngineBehaviour@{
guards := [commitGuard];
action := commitmentAction;
conflictSolver := commitmentConflictSolver
};