module arch.node.net.storage_environment;

import arch.node.net.storage_messages open;
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;

Storage Environment¶

Overview¶

The Engine environment of the engine.

Mailbox state¶

StorageMailboxState¶

StorageMailboxState : Type := Unit;

Local state¶

StorageLocalState¶

type StorageLocalState := mkStorageLocalState;

Timer handles¶

StorageTimerHandle¶

StorageTimerHandle : Type := Unit;

StorageTimestampedTrigger¶

StorageTimestampedTrigger : Type :=
  TimestampedTrigger StorageTimerHandle Anoma.Msg;

Engine Environment¶

StorageEnv¶

StorageEnv : Type :=
  EngineEnv StorageLocalState StorageMailboxState StorageTimerHandle Anoma.Msg;

Instantiation¶

exStorageEnv : StorageEnv :=
  mkEngineEnv@{
    localState := mkStorageLocalState;
    mailboxCluster := Map.empty;
    acquaintances := Set.empty;
    timers := [];
  };