module arch.node.engines.shard_environment;

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

syntax alias ShardMailboxState := Unit;

type ReadStatus :=
  mkReadStatus@{
    hasBeenRead : Bool;
    isEager : Bool;
    executor : EngineID;
  };

type WriteStatus :=
  mkWriteStatus@{
    data : Option KVSDatum;
    mayWrite : Bool;
  };

type KeyAccess :=
  mkKeyAccess@{
    readStatus : Option ReadStatus;
    writeStatus : Option WriteStatus;
  };

type DAGStructure :=
  mkDAGStructure@{
    keyAccesses : Map KVSKey (Map TxFingerprint KeyAccess);
    heardAllReads : TxFingerprint;
    heardAllWrites : TxFingerprint;
  };

type ShardLocalState :=
  mk@{
    dagStructure : DAGStructure;
    anchors : List NarwhalBlock;
  };

syntax alias ShardTimerHandle := Unit;

ShardEnv : Type :=
  EngineEnv ShardLocalState ShardMailboxState ShardTimerHandle Anoma.Msg;

module shard_environment_example;
  
  shardEnv : ShardEnv :=
    EngineEnv.mk@{
      localState :=
        ShardLocalState.mk@{
          dagStructure :=
            DAGStructure.mkDAGStructure@{
              keyAccesses := Map.empty;
              heardAllReads := 0;
              heardAllWrites := 0;
            };
          anchors := [];
        };
      mailboxCluster := Map.empty;
      acquaintances := Set.empty;
      timers := [];
    };
end;