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 : Type :=
  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;
  };

ShardLocalState¶

type ShardLocalState :=
  mkShardLocalState@{
    dagStructure : DAGStructure;
    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 : Type :=
  EngineEnv ShardLocalState ShardMailboxState ShardTimerHandle Anoma.Msg;

Instantiation¶

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