Juvix imports

module arch.node.engines.decryption_behaviour;

import prelude open;
import arch.node.types.messages open;
import arch.system.identity.identity open;
import arch.node.types.engine_behaviour open;
import arch.node.types.engine_environment open;
import arch.node.engines.decryption_environment open;
import arch.node.engines.decryption_messages open;
import arch.node.types.identities open;
import arch.node.types.anoma_message open;

Decryption Dynamics

Overview

The behavior of the Decryption Engine define how it processes incoming decryption requests and produces the corresponding responses.

Action labels

type DecryptionActionLabel := DoDecrypt {data : ByteString};

DoDecrypt

DoDecrypt { data : ByteString }

This action label corresponds to decrypting the data in the given request.

DoDecrypt action effect

This action does the following:

Aspect	Description
State update	The state remains unchanged.
Messages to be sent	A DecryptResponse 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 DecryptionMatchableArgument := 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 Decryption Engine does not require any non-trivial pre-computations.

syntax alias DecryptionPrecomputation := Unit;

Guards

Auxiliary Juvix code

Type alias for the guard.

DecryptionGuard : Type :=
  Guard
    DecryptionLocalState
    DecryptionMailboxState
    DecryptionTimerHandle
    DecryptionMatchableArgument
    DecryptionActionLabel
    DecryptionPrecomputation;

DecryptionGuardOutput : Type :=
  GuardOutput
    DecryptionMatchableArgument
    DecryptionActionLabel
    DecryptionPrecomputation;

decryptGuard

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

decryptGuard flowchart

decryptGuard
  (t : TimestampedTrigger DecryptionTimerHandle)
  (env : DecryptionEnvironment)
  : Option DecryptionGuardOutput :=
  case getMessageFromTimestampedTrigger t of
    | some (MsgDecryption (DecryptRequest data)) :=
      do {
        sender <- getSenderFromTimestampedTrigger t;
        pure
          mkGuardOutput@{
            matchedArgs := [ReplyTo (some sender) none];
            actionLabel := DoDecrypt data;
            precomputationTasks := unit
          };
      }
    | _ := none;

Action function

Auxiliary Juvix code

Type alias for the action function.

DecryptionActionInput : Type :=
  ActionInput
    DecryptionLocalState
    DecryptionMailboxState
    DecryptionTimerHandle
    DecryptionMatchableArgument
    DecryptionActionLabel
    DecryptionPrecomputation;

DecryptionActionEffect : Type :=
  ActionEffect
    DecryptionLocalState
    DecryptionMailboxState
    DecryptionTimerHandle
    DecryptionMatchableArgument
    DecryptionActionLabel
    DecryptionPrecomputation;

decryptionAction (input : DecryptionActionInput) : DecryptionActionEffect :=
  let
    env := ActionInput.env input;
    out := ActionInput.guardOutput input;
    localState := EngineEnvironment.localState env;
  in case GuardOutput.actionLabel out of
       DoDecrypt data :=
         case GuardOutput.matchedArgs out of
           | ReplyTo (some whoAsked) _ :: _ :=
             let
               decryptedData :=
                 Decryptor.decrypt
                   (DecryptionLocalState.decryptor localState)
                   (DecryptionLocalState.backend localState)
                   data;
               responseMsg :=
                 case decryptedData of
                   | none :=
                     DecryptResponse@{
                       data := emptyByteString;
                       err := some "Decryption Failed"
                     }
                   | some plaintext :=
                     DecryptResponse@{
                       data := plaintext;
                       err := none
                     };
             in mkActionEffect@{
               newEnv := env;
               producedMessages :=
                 [ mkEngineMessage@{
                   sender := mkPair none (some (EngineEnvironment.name env));
                   target := whoAsked;
                   mailbox := some 0;
                   msg := MsgDecryption responseMsg
                 }
                 ];
               timers := [];
               spawnedEngines := []
             }
           | _ :=
             mkActionEffect@{
               newEnv := env;
               producedMessages := [];
               timers := [];
               spawnedEngines := []
             };

Conflict solver

decryptionConflictSolver
  : Set DecryptionMatchableArgument -> List (Set DecryptionMatchableArgument)
  | _ := [];

DecryptionBehaviour type

DecryptionBehaviour : Type :=
  EngineBehaviour
    DecryptionLocalState
    DecryptionMailboxState
    DecryptionTimerHandle
    DecryptionMatchableArgument
    DecryptionActionLabel
    DecryptionPrecomputation;

DecryptionBehaviour instance

decryptionBehaviour : DecryptionBehaviour :=
  mkEngineBehaviour@{
    guards := [decryptGuard];
    action := decryptionAction;
    conflictSolver := decryptionConflictSolver
  };