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 :=
  mk@{
    evidenceStore : Set SignsForEvidence;
  };

syntax alias SignsForTimerHandle := Unit;

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

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