module arch.node.engines.signs_for_environment;

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

axiom verifyEvidence : SignsForEvidence -> Bool;

syntax alias SignsForMailboxState := Unit;

type SignsForLocalState :=
  mkSignsForLocalState@{
    evidenceStore : Set SignsForEvidence;
  };

syntax alias SignsForTimerHandle := Unit;

SignsForEnv : Type :=
  EngineEnv
    SignsForLocalState
    SignsForMailboxState
    SignsForTimerHandle
    Anoma.Msg;

module signs_for_environment_example;
  
  signsForEnv : SignsForEnv :=
    mkEngineEnv@{
      localState :=
        mkSignsForLocalState@{
          evidenceStore := Set.empty;
        };
      mailboxCluster := Map.empty;
      acquaintances := Set.empty;
      timers := [];
    };
end;