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

flowchart TD
    C{CommitRequest<br>received?}
    C -->|Yes| D[enabled]
    C -->|No| E[not enabled]
    D --> F([DoCommit])

commitGuard flowchart

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
  };