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;

axiom getNotificationTargets : StorageKey -> List EngineID;

axiom advanceTime : EpochTimestamp -> EpochTimestamp;

syntax alias LocalKVStorageMailboxState := Unit;

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

syntax alias LocalKVStorageTimerHandle := Unit;

LocalKVStorageTimestampedTrigger : Type :=
  TimestampedTrigger LocalKVStorageTimerHandle Anoma.Msg;

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

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