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;

Shard Environment¶

Overview¶

The shard environment maintains state about key-value pairs, tracking read and write accesses for each key across different transaction timestamps. It provides multi-version concurrent storage capabilities.

Mailbox states¶

syntax alias ShardMailboxState := Unit;

The shard engine does not require complex mailbox states. Therefore, we define the mailbox state type as Unit.

Local state¶

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

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

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

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

ShardLocalState¶

type ShardLocalState KVSKey KVSDatum :=
  mkShardLocalState@{
    dagStructure : DAGStructure KVSKey KVSDatum;
    anchors : List NarwhalBlock;
  };

Timer handles¶

syntax alias ShardTimerHandle := Unit;

The shard engine does not require timers. Therefore, we define the timer handle type as Unit.

The Shard Environment¶

ShardEnv¶

ShardEnv (KVSKey KVSDatum : Type) : Type :=
  EngineEnv
    (ShardLocalState KVSKey KVSDatum)
    ShardMailboxState
    ShardTimerHandle
    Anoma.Msg;

Instantiation¶

shardEnv : ShardEnv String String :=
  mkEngineEnv@{
    localState :=
      mkShardLocalState@{
        dagStructure :=
          mkDAGStructure@{
            keyAccesses := Map.empty;
            heardAllReads := 0;
            heardAllWrites := 0;
          };
        anchors := [];
      };
    mailboxCluster := Map.empty;
    acquaintances := Set.empty;
    timers := [];
  };