module arch.node.types.engine_behaviour;

import arch.node.types.basics open;
import arch.node.types.messages open;
import arch.node.types.identities open;
import arch.node.types.engine_config open;
import arch.node.types.engine_environment open;

Engine behaviour¶

Each engine processes only one message at a time. The behaviour of an engine is specified by a finite set of guards and an action function, which both determine how engine instances react to received messages or timer notifications.

Guards¶

Guards are terms of type Guard, which is a function type, where the trigger of type TimestampedTrigger H AM is a term that captures the message received with a timestamp or a clock notification about timers that have elapsed during the engine's operation. Guards return data of type GuardOutput A if the precondition of the action that they are guarding is met.

Recall that the behaviour is described by a set of guards and an action function. The guard is a function that evaluates conditions in the engine environment to determine what action should be performed; for this, each guard creates an action label, that then is "interpreted" by the action function.

The guard function receives:

• the timestamped trigger that caused guard evaluation,
• the environment of the engine instance, and
• an optional time reference for the starting point of the evaluation of all guards.

Given these inputs, the guard function computes an action label, which encodes

• all information necessary to infer how the engine will react
• additional information on how this action contributes to properties of the Anoma protocol instance the engine is part of.

The action function then computes the effects of the action label; besides changes to the engine environment, an action effect comprises sending messages, creating new engine instances, and updating timers.

Actions¶

Action¶

The input of the action function is parameterised by the types for:

• C: engine configuration,
• S: local state,
• B: mailbox state,
• H: timer handles,
• A: action arguments,
• AM: type for all engine messages (Msg),
• AC: type for all engine configurations (Cfg), and
• AE: type for all engine environments (Env).

The Action function receives as argument the ActionInput, and returns the ActionEffect.

{-# isabelle-ignore: true #-}
Action (C S B H A AM AC AE : Type) : Type :=
  (input : ActionInput C S B H A AM) -> Option (ActionEffect S B H AM AC AE);

If the guard does not give a result, this means that none of its guarded actions are triggered.

Trigger H AM -> EngineEnv S B H AM -> Bool;

ActionInput¶

The ActionInput contains:

• the action arguments,
• the engine configuration,
• the engine environment, and
• the timestamped trigger that caused the guard evaluation.

type ActionInput (C S B H A AM : Type) :=
  mkActionInput@{
    args : A;
    cfg : EngineCfg C;
    env : EngineEnv S B H AM;
    trigger : TimestampedTrigger H AM;
  };

ActionEffect¶

The ActionEffect S B H AM AC AE type defines the effects produced by the action. The action can perform any of the following:

• Update the engine environment.
• Produce a set of messages to be sent to other engine instances.
• Set, discard, or supersede timers.
• Define new engine instances to be created.

type ActionEffect (S B H AM AC AE : Type) :=
  mkActionEffect@{
    env : EngineEnv S B H AM;
    msgs : List (EngineMsg AM);
    timers : List (Timer H);
    engines : List (Pair AC AE);
  };

ActionExec¶

type ActionExec (C S B H A AM AC AE : Type) :=
  Seq (List (Action C S B H A AM AC AE));

Guard¶

{-# isabelle-ignore: true #-}
Guard (C S B H A AM AC AE : Type) : Type :=
  (trigger : TimestampedTrigger H AM)
    -> (cfg : EngineCfg C)
    -> (env : EngineEnv S B H AM)
    -> Option (GuardOutput C S B H A AM AC AE);

GuardOutput¶

The guard output defines an action sequence, the programmatic action to be performed, and action arguments.

type GuardOutput (C S B H A AM AC AE : Type) :=
  mkGuardOutput@{
    action : ActionExec C S B H A AM AC AE;
    args : A;
  };

GuardEval¶

type GuardEval (C S B H A AM AC AE : Type) :=
  | First (List (Guard C S B H A AM AC AE))
  | Any (List (Guard C S B H A AM AC AE));

The GuardEval type defines the criteria for evaluating actions associated with guards inside the given list. The evaluation strategies are as follows:

• With First, we say that the first guard in the provided list that holds, i.e., yields a result, upon sequential evaluation is selected, its associated action is performed, and the evaluation stops.
• With Any, we say that any guard in the provided list that holds upon sequential evaluation is selected, their associated actions are performed, and the evaluation stops.

The type for engine behaviours¶

The EngineBehaviour type encapsulates the concept of behaviours within Anoma. Each engine is associated with a specific term of type EngineBehaviour that defines its core dynamics and operational characteristics. The behaviour determines how the engine processes inputs, manages state, and interacts with other components. As defined, it clears up that engines are essentially a collection of guarded state-transition functions. Using the terminology introduced earlier, an EngineBehaviour is a set of guards and an action function.

type EngineBehaviour (C S B H A AM AC AE : Type) :=
  mkEngineBehaviour@{guards : GuardEval C S B H A AM AC AE};