Juvix imports

module arch.node.engines.encryption_behaviour;

import prelude open;
import Stdlib.Data.List.Base open;
import Stdlib.Trait.Ord as Ord;
import arch.system.identity.identity open hiding {ExternalIdentity};
import arch.node.engines.encryption_environment open;
import arch.node.engines.encryption_messages open;
import arch.node.engines.reads_for_messages 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;

`Encryption` Dynamics¶

Overview¶

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

Action labels¶

type EncryptionActionLabel :=
  | DoEncrypt {
      data : Plaintext;
      externalIdentity : ExternalIdentity;
      useReadsFor : Bool
    }
  | DoHandleReadsForResponse {
      externalIdentity : ExternalIdentity;
      readsForEvidence : Set ReadsForEvidence
    };

`DoEncrypt`¶

DoEncrypt { data : Plaintext; externalIdentity : ExternalIdentity; useReadsFor : Bool }

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

DoEncrypt action effect

This action does the following:

Aspect	Description
State update	If `useReadsFor` is true, the state is updated to store pending requests. Otherwise, the state remains unchanged.
Messages to be sent	If `useReadsFor` is false, an `EncryptResponse` message is sent back to the requester. If `useReadsFor` is true and it's the first request for this identity, a `QueryReadsForEvidenceRequest` is sent to the ReadsFor Engine.
Engines to be spawned	No engines are created by this action.
Timer updates	No timers are set or cancelled.

`DoHandleReadsForResponse`¶

DoHandleReadsForResponse { externalIdentity : ExternalIdentity; readsForEvidence : Set ReadsForEvidence };

This action label corresponds to receiving reads for evidence and using it to address relevant pending requests.

DoHandleReadsForResponse action effect

This action does the following:

Aspect	Description
State update	The state is updated to remove the processed pending requests for the given external identity.
Messages to be sent	`EncryptResponse` messages are sent to all requesters who were waiting for this ReadsFor evidence.
Engines to be spawned	No engines are created by this action.
Timer updates	No timers are set or cancelled.

Matchable arguments¶

type EncryptionMatchableArgument := 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 Encryption Engine does not require any non-trivial pre-computations.

syntax alias EncryptionPrecomputation := Unit;

Guards¶

Auxiliary Juvix code

Type alias for the guard.

EncryptionGuard : Type :=
  Guard
    EncryptionLocalState
    EncryptionMailboxState
    EncryptionTimerHandle
    EncryptionMatchableArgument
    EncryptionActionLabel
    EncryptionPrecomputation;

EncryptionGuardOutput : Type :=
  GuardOutput
    EncryptionMatchableArgument
    EncryptionActionLabel
    EncryptionPrecomputation;

`encryptGuard`¶

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

encryptGuard flowchart

encryptGuard
  (t : TimestampedTrigger EncryptionTimerHandle)
  (env : EncryptionEnvironment)
  : Option EncryptionGuardOutput :=
  case getMessageFromTimestampedTrigger t of
    | some (MsgEncryption (EncryptRequest data externalIdentity useReadsFor)) :=
      do {
        sender <- getSenderFromTimestampedTrigger t;
        pure
          mkGuardOutput@{
            matchedArgs := [ReplyTo (some sender) none];
            actionLabel := DoEncrypt data externalIdentity useReadsFor;
            precomputationTasks := unit
          };
      }
    | _ := none;

`readsForResponseGuard`¶

readsForResponseGuard
  (t : TimestampedTrigger EncryptionTimerHandle)
  (env : EncryptionEnvironment)
  : Option EncryptionGuardOutput :=
  case getMessageFromTimestampedTrigger t of
    | some (MsgReadsFor (QueryReadsForEvidenceResponse externalIdentity evidence err)) :=
      case getSenderFromTimestampedTrigger t of {
        | some sender :=
          case
            Ord.isEQ
              (Ord.cmp
                sender
                (EncryptionLocalState.readsForEngineAddress
                  (EngineEnvironment.localState env)))
          of {
            | true :=
              some
                mkGuardOutput@{
                  matchedArgs := [];
                  actionLabel :=
                    DoHandleReadsForResponse externalIdentity evidence;
                  precomputationTasks := unit
                }
            | false := none
          }
        | none := none
      }
    | _ := none;

Action function¶

Auxiliary Juvix code

Type alias for the action function.

EncryptionActionInput : Type :=
  ActionInput
    EncryptionLocalState
    EncryptionMailboxState
    EncryptionTimerHandle
    EncryptionMatchableArgument
    EncryptionActionLabel
    EncryptionPrecomputation;

EncryptionActionEffect : Type :=
  ActionEffect
    EncryptionLocalState
    EncryptionMailboxState
    EncryptionTimerHandle
    EncryptionMatchableArgument
    EncryptionActionLabel
    EncryptionPrecomputation;

encryptResponse
  (externalIdentity : ExternalIdentity)
  (env : EncryptionEnvironment)
  (evidence : Set ReadsForEvidence)
  (req : Pair EngineID Plaintext)
  : EngineMessage :=
  let
    localState := EngineEnvironment.localState env;
    whoAsked := fst req;
    data := snd req;
    encryptedData :=
      Encryptor.encrypt
        (EncryptionLocalState.encryptor localState evidence externalIdentity)
        (EncryptionLocalState.backend localState)
        data;
    responseMsg :=
      EncryptResponse@{
        ciphertext := encryptedData;
        err := none
      };
    envelope :=
      mkEngineMessage@{
        sender := mkPair none (some (EngineEnvironment.name env));
        target := whoAsked;
        mailbox := some 0;
        msg := MsgEncryption responseMsg
      };
  in envelope;

encryptionAction (input : EncryptionActionInput) : EncryptionActionEffect :=
  let
    env := ActionInput.env input;
    out := ActionInput.guardOutput input;
    localState := EngineEnvironment.localState env;
  in case GuardOutput.actionLabel out of
       | DoEncrypt data externalIdentity' useReadsFor :=
         case GuardOutput.matchedArgs out of {
           | ReplyTo (some whoAsked) _ :: _ :=
             case useReadsFor of {
               | false :=
                 let
                   envelope :=
                     encryptResponse
                       externalIdentity'
                       env
                       Set.empty
                       (mkPair whoAsked data);
                 in mkActionEffect@{
                   newEnv := env;
                   producedMessages := [envelope];
                   timers := [];
                   spawnedEngines := []
                 }
               | true :=
                 let
                   existingRequests :=
                     Map.lookup
                       externalIdentity'
                       (EncryptionLocalState.pendingRequests localState);
                   newPendingList :=
                     case existingRequests of
                       | some reqs := reqs ++ [mkPair whoAsked data]
                       | none := [mkPair whoAsked data];
                   newPendingRequests :=
                     Map.insert
                       externalIdentity'
                       newPendingList
                       (EncryptionLocalState.pendingRequests localState);
                   newLocalState :=
                     localState@EncryptionLocalState{pendingRequests := newPendingRequests};
                   newEnv' :=
                     env@EngineEnvironment{localState := newLocalState};
                   messagesToSend :=
                     case existingRequests of
                       | some _ := []
                       | none :=
                         let
                           requestMsg :=
                             QueryReadsForEvidenceRequest@{
                               externalIdentity := externalIdentity'
                             };
                           envelope :=
                             mkEngineMessage@{
                               sender :=
                                 mkPair
                                   none
                                   (some (EngineEnvironment.name env));
                               target :=
                                 EncryptionLocalState.readsForEngineAddress
                                   localState;
                               mailbox := some 0;
                               msg := MsgReadsFor requestMsg
                             };
                         in [envelope];
                 in mkActionEffect@{
                   newEnv := newEnv';
                   producedMessages := messagesToSend;
                   timers := [];
                   spawnedEngines := []
                 }
             }
           | _ :=
             mkActionEffect@{
               newEnv := env;
               producedMessages := [];
               timers := [];
               spawnedEngines := []
             }
         }
       | DoHandleReadsForResponse externalIdentity evidence :=
         case
           Map.lookup
             externalIdentity
             (EncryptionLocalState.pendingRequests localState)
         of
           | some reqs :=
             let
               messages :=
                 map (encryptResponse externalIdentity env evidence) reqs;
               newPendingRequests :=
                 Map.delete
                   externalIdentity
                   (EncryptionLocalState.pendingRequests localState);
               newLocalState :=
                 localState@EncryptionLocalState{pendingRequests := newPendingRequests};
               newEnv' := env@EngineEnvironment{localState := newLocalState};
             in mkActionEffect@{
               newEnv := newEnv';
               producedMessages := messages;
               timers := [];
               spawnedEngines := []
             }
           | none :=
             mkActionEffect@{
               newEnv := env;
               producedMessages := [];
               timers := [];
               spawnedEngines := []
             };

Conflict solver¶

encryptionConflictSolver
  : Set EncryptionMatchableArgument -> List (Set EncryptionMatchableArgument)
  | _ := [];

EncryptionBehaviour type¶

EncryptionBehaviour : Type :=
  EngineBehaviour
    EncryptionLocalState
    EncryptionMailboxState
    EncryptionTimerHandle
    EncryptionMatchableArgument
    EncryptionActionLabel
    EncryptionPrecomputation;

EncryptionBehaviour instance¶

encryptionBehaviour : EncryptionBehaviour :=
  mkEngineBehaviour@{
    guards := [encryptGuard; readsForResponseGuard];
    action := encryptionAction;
    conflictSolver := encryptionConflictSolver
  };

Encryption Dynamics¶