Skip to content
Juvix imports 

module arch.node.engines.encryption_behaviour;

import prelude open;
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.encryption_config open;
import arch.node.engines.reads_for_messages open;
import arch.node.types.anoma as Anoma open;
import arch.node.types.engine open;
import arch.node.types.identities open;
import arch.node.types.messages open;

Encryption Behaviour

Overview

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

Action arguments

EncryptionActionArgumentReplyTo 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:
is the address of the engine that sent the message.
mailbox:
is the mailbox ID where the response message should be sent.

EncryptionActionArgument

type EncryptionActionArgument := EncryptionActionArgumentReplyTo ReplyTo;

EncryptionActionArguments

EncryptionActionArguments : Type := List EncryptionActionArgument;

Actions

Auxiliary Juvix code

EncryptionAction

EncryptionAction : Type :=
  Action
    EncryptionCfg
    EncryptionLocalState
    EncryptionMailboxState
    EncryptionTimerHandle
    EncryptionActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

EncryptionActionInput

EncryptionActionInput : Type :=
  ActionInput
    EncryptionCfg
    EncryptionLocalState
    EncryptionMailboxState
    EncryptionTimerHandle
    EncryptionActionArguments
    Anoma.Msg;

EncryptionActionEffect

EncryptionActionEffect : Type :=
  ActionEffect
    EncryptionLocalState
    EncryptionMailboxState
    EncryptionTimerHandle
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

EncryptionActionExec

EncryptionActionExec : Type :=
  ActionExec
    EncryptionCfg
    EncryptionLocalState
    EncryptionMailboxState
    EncryptionTimerHandle
    EncryptionActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

encryptAction

Process an encryption request.

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, a ResponseEncrypt 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.
encryptAction (input : EncryptionActionInput) : Option EncryptionActionEffect :=
  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 EngineMsg.msg emsg of {
           | Anoma.MsgEncryption (MsgEncryptionRequest (mkRequestEncrypt data externalIdentity useReadsFor)) :=
             case useReadsFor of {
               | false :=
                 some
                   mkActionEffect@{
                     env := env;
                     msgs :=
                       [
                         mkEngineMsg@{
                           sender := getEngineIDFromEngineCfg cfg;
                           target := EngineMsg.sender emsg;
                           mailbox := some 0;
                           msg :=
                             Anoma.MsgEncryption
                               (MsgEncryptionResponse
                                 mkResponseEncrypt@{
                                   ciphertext :=
                                     Encryptor.encrypt
                                       (EncryptionCfg.encryptor
                                         (EngineCfg.cfg cfg)
                                         Set.empty
                                         externalIdentity)
                                       (EncryptionCfg.backend
                                         (EngineCfg.cfg cfg))
                                       data;
                                   err := none;
                                 });
                         };
                       ];
                     timers := [];
                     engines := [];
                   }
               | true :=
                 let
                   existingRequests :=
                     Map.lookup
                       externalIdentity
                       (EncryptionLocalState.pendingRequests localState);
                   newPendingList :=
                     case existingRequests of
                       | some reqs :=
                         reqs ++ [mkPair (EngineMsg.sender emsg) data]
                       | none := [mkPair (EngineMsg.sender emsg) data];
                   newLocalState :=
                     localState@EncryptionLocalState{pendingRequests := Map.insert
                       externalIdentity
                       newPendingList
                       (EncryptionLocalState.pendingRequests localState)};
                 in some
                   mkActionEffect@{
                     env := env@EngineEnv{localState := newLocalState};
                     msgs :=
                       case existingRequests of
                         | some _ := []
                         | none :=
                           [
                             mkEngineMsg@{
                               sender := getEngineIDFromEngineCfg cfg;
                               target :=
                                 EncryptionCfg.readsForEngineAddress
                                   (EngineCfg.cfg cfg);
                               mailbox := some 0;
                               msg :=
                                 Anoma.MsgReadsFor
                                   (MsgQueryReadsForEvidenceRequest
                                     mkRequestQueryReadsForEvidence@{
                                       externalIdentity := externalIdentity;
                                     });
                             };
                           ];
                     timers := [];
                     engines := [];
                   }
             }
           | _ := none
         }
       | _ := none;

handleReadsForResponseAction

Process reads-for evidence response.

State update
The state is updated to remove processed pending requests.
Messages to be sent
ResponseEncrypt 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.
handleReadsForResponseAction
  (input : EncryptionActionInput) : Option EncryptionActionEffect :=
  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 EngineMsg.msg emsg of {
           | Anoma.MsgReadsFor (MsgQueryReadsForEvidenceResponse (mkResponseQueryReadsForEvidence externalIdentity evidence err)) :=
             case
               Map.lookup
                 externalIdentity
                 (EncryptionLocalState.pendingRequests localState)
             of {
               | some reqs :=
                 let
                   newLocalState :=
                     localState@EncryptionLocalState{pendingRequests := Map.delete
                       externalIdentity
                       (EncryptionLocalState.pendingRequests localState)};
                 in some
                   mkActionEffect@{
                     env := env@EngineEnv{localState := newLocalState};
                     msgs :=
                       map
                         \{req :=
                           let
                             whoAsked := fst req;
                             data := snd req;
                           in mkEngineMsg@{
                                sender := getEngineIDFromEngineCfg cfg;
                                target := whoAsked;
                                mailbox := some 0;
                                msg :=
                                  Anoma.MsgEncryption
                                    (MsgEncryptionResponse
                                      mkResponseEncrypt@{
                                        ciphertext :=
                                          Encryptor.encrypt
                                            (EncryptionCfg.encryptor
                                              (EngineCfg.cfg cfg)
                                              evidence
                                              externalIdentity)
                                            (EncryptionCfg.backend
                                              (EngineCfg.cfg cfg))
                                            data;
                                        err := none;
                                      });
                              }}
                         reqs;
                     timers := [];
                     engines := [];
                   }
               | none := none
             }
           | _ := none
         }
       | _ := none;

Action Labels

encryptActionLabel

encryptActionLabel : EncryptionActionExec := Seq [encryptAction];

handleReadsForResponseActionLabel

handleReadsForResponseActionLabel : EncryptionActionExec :=
  Seq [handleReadsForResponseAction];

Guards

Auxiliary Juvix code

EncryptionGuard

EncryptionGuard : Type :=
  Guard
    EncryptionCfg
    EncryptionLocalState
    EncryptionMailboxState
    EncryptionTimerHandle
    EncryptionActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

EncryptionGuardOutput

EncryptionGuardOutput : Type :=
  GuardOutput
    EncryptionCfg
    EncryptionLocalState
    EncryptionMailboxState
    EncryptionTimerHandle
    EncryptionActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

encryptGuard

Condition
Message type is MsgEncryptionRequest.
encryptGuard
  (tt : TimestampedTrigger EncryptionTimerHandle Anoma.Msg)
  (cfg : EngineCfg EncryptionCfg)
  (env : EncryptionEnv)
  : Option EncryptionGuardOutput :=
  case getEngineMsgFromTimestampedTrigger tt of
    | some mkEngineMsg@{msg := Anoma.MsgEncryption (MsgEncryptionRequest _)} :=
      some
        mkGuardOutput@{
          action := encryptActionLabel;
          args := [];
        }
    | _ := none;

readsForResponseGuard

readsForResponseGuard
  (tt : TimestampedTrigger EncryptionTimerHandle Anoma.Msg)
  (cfg : EngineCfg EncryptionCfg)
  (env : EncryptionEnv)
  : Option EncryptionGuardOutput :=
  case getEngineMsgFromTimestampedTrigger tt of
    | some emsg :=
      case EngineMsg.msg emsg of {
        | Anoma.MsgReadsFor (MsgQueryReadsForEvidenceResponse _) :=
          case
            isEqual
              (Ord.cmp
                (EngineMsg.sender emsg)
                (EncryptionCfg.readsForEngineAddress (EngineCfg.cfg cfg)))
          of {
            | true :=
              some
                mkGuardOutput@{
                  action := handleReadsForResponseActionLabel;
                  args := [];
                }
            | false := none
          }
        | _ := none
      }
    | _ := none;

The Encryption Behaviour

EncryptionBehaviour

EncryptionBehaviour : Type :=
  EngineBehaviour
    EncryptionCfg
    EncryptionLocalState
    EncryptionMailboxState
    EncryptionTimerHandle
    EncryptionActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

Instantiation

encryptionBehaviour : EncryptionBehaviour :=
  mkEngineBehaviour@{
    guards := First [encryptGuard; readsForResponseGuard];
  };

Encryption Action Flowcharts

encryptAction flowchart

flowchart TD
  subgraph C [Conditions]
    CMsg[MsgEncryptionRequest]
  end

  G[encryptGuard]
  A[encryptAction]

  C --> G -->|encryptActionLabel| A --> E

  subgraph E [Effects]
    direction TB
    E1[(Update pending requests)]
    E2[Send encrypted response]
  end
encryptAction flowchart

handleReadsForResponseAction flowchart

flowchart TD
  subgraph C [Conditions]
    CMsg[MsgQueryReadsForEvidenceResponse]
  end

  G[readsForResponseGuard]
  A[handleReadsForResponseAction]

  C --> G -->|handleReadsForResponseActionLabel| A --> E

  subgraph E [Effects]
    direction TB
    E1[(Remove pending requests)]
    E2[Send encrypted responses]
  end
handleReadsForResponseAction flowchart