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;

axiom verifyEvidence : ReadsForEvidence -> Bool;

syntax alias ReadsForMailboxState := Unit;

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

syntax alias ReadsForTimerHandle := Unit;

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

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