module arch.node.engines.reads_for_environment;

import prelude open;
import arch.node.types.engine_environment open;
import arch.node.types.identities open;
import arch.node.engines.reads_for_messages open;
import arch.node.types.anoma_message as Anoma open;

Reads For Environment¶

Overview¶

The Reads For Engine environment maintains the state necessary for managing reads_for relationships between identities, including storing evidence submitted by clients.

axiom verifyEvidence : ReadsForEvidence -> Bool;

Mailbox states¶

The Reads For Engine does not require complex mailbox states. We define the mailbox state as Unit.

ReadsForMailboxState¶

syntax alias ReadsForMailboxState := Unit;

Local state¶

The local state of the Reads For Engine includes the evidence for reads_for relationships.

ReadsForLocalState¶

type ReadsForLocalState :=
  mkReadsForLocalState@{evidenceStore : Set ReadsForEvidence};

Timer Handle¶

The Reads For Engine does not require a timer handle type. Therefore, we define the timer handle type as Unit.

ReadsForTimerHandle¶

syntax alias ReadsForTimerHandle := Unit;

The Reads For Environment¶

ReadsForEnv¶

ReadsForEnv : Type :=
  EngineEnv
    ReadsForLocalState
    ReadsForMailboxState
    ReadsForTimerHandle
    Anoma.Msg;

Instantiation¶

readsForEnv : ReadsForEnv :=
  mkEngineEnv@{
    localState :=
      mkReadsForLocalState@{
        evidenceStore := Set.empty;
      };
    mailboxCluster := Map.empty;
    acquaintances := Set.empty;
    timers := [];
  };