module arch.node.engines.local_key_value_storage_environment;

import prelude open;
import arch.node.engines.local_key_value_storage_messages 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;

Local Key-Value Storage Environment¶

Overview¶

The Local Key-Value Storage Engine provides local storage and retrieval of data in a key-value format.

axiom getNotificationTargets : StorageKey -> List EngineID;

axiom advanceTime : EpochTimestamp -> EpochTimestamp;

Mailbox state types¶

LocalKVStorageMailboxState¶

syntax alias LocalKVStorageMailboxState := Unit;

Local state¶

LocalKVStorageLocalState¶

type LocalKVStorageLocalState :=
  mkLocalKVStorageLocalState@{
    storage : Map StorageKey StorageValue;
    localClock : EpochTimestamp;
  };

Timer handles¶

LocalKVStorageTimerHandle¶

syntax alias LocalKVStorageTimerHandle := Unit;

LocalKVStorageTimestampedTrigger¶

LocalKVStorageTimestampedTrigger : Type :=
  TimestampedTrigger LocalKVStorageTimerHandle Anoma.Msg;

The Local Key-Value Storage Environment¶

LocalKVStorageEnv¶

LocalKVStorageEnv : Type :=
  EngineEnv
    LocalKVStorageLocalState
    LocalKVStorageMailboxState
    LocalKVStorageTimerHandle
    Anoma.Msg;

Instantiation¶

localKVStorageEnv : LocalKVStorageEnv :=
  mkEngineEnv@{
    localState :=
      mkLocalKVStorageLocalState@{
        storage := Map.empty;
        localClock := 0;
      };
    mailboxCluster := Map.empty;
    acquaintances := Set.empty;
    timers := [];
  };