module arch.node.engines.transport_protocol_environment;

import arch.node.types.basics open;
import arch.node.types.engine open;
import arch.node.types.messages open;
import arch.node.types.identities open;
import arch.node.types.anoma_message as Anoma open;

Transport Protocol Environment¶

Overview¶

The Engine environment of the engine.

Mailbox states¶

syntax alias TransportProtocolMailboxState := Unit;

Local state¶

type TransportProtocolLocalState := mk;

Timer Handle¶

TransportProtocolTimerHandle : Type := Unit;

The TransportProtocol does not require a timer handle type. Therefore, we define the timer handle type as Unit.

Timestamped Trigger¶

TransportProtocolTimestampedTrigger : Type :=
  TimestampedTrigger TransportProtocolTimerHandle Anoma.Msg;

The Transport Protocol Environment¶

TransportProtocolEnv¶

TransportProtocolEnv : Type :=
  EngineEnv
    TransportProtocolLocalState
    TransportProtocolMailboxState
    TransportProtocolTimerHandle
    Anoma.Msg;

Instantiation¶

exTransportProtocolEnv : TransportProtocolEnv :=
  EngineEnv.mk@{
    localState := TransportProtocolLocalState.mk;
    mailboxCluster := Map.empty;
    acquaintances := Set.empty;
    timers := [];
  };