Failure

[10 of 15] Compiling arch.node.engines.decryption_environment /home/runner/work/nspec/nspec/docs/arch/node/engines/decryption_environment.juvix.md:79:7-11: error: Unexpected argument node

icon: octicons/gear-16 search: exclude: false categories: - engine-behaviour - juvix-module tags: - decryption - engine-behavior

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 :=
  | -- --8<-- [start:DoDecrypt]
    DoDecrypt {
      data : ByteString
    }
    -- --8<-- [end:DoDecrypt]
;

`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 :=
  | -- --8<-- [start:ReplyTo]
  ReplyTo (Option EngineID) (Option MailboxID)
  -- --8<-- [end:ReplyTo]
;

`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.

-- --8<-- [start:decryption-guard]
DecryptionGuard : Type :=
  Guard
    DecryptionLocalState
    DecryptionMailboxState
    DecryptionTimerHandle
    DecryptionMatchableArgument
    DecryptionActionLabel
    DecryptionPrecomputation;
-- --8<-- [end:decryption-guard]

-- --8<-- [start:decryption-guard-output]
DecryptionGuardOutput : Type :=
  GuardOutput DecryptionMatchableArgument DecryptionActionLabel DecryptionPrecomputation;
-- --8<-- [end:decryption-guard-output]

`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 := EngineEnv.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; -- No state change
            producedMessages := [mkEngineMsg@{
              sender := mkPair none (some (EngineEnv.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;
  };

Decryption Dynamics¶