module arch.node.engines.naming_environment;

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

axiom verifyEvidence : IdentityNameEvidence -> Bool;

syntax alias NamingMailboxState := Unit;

type NamingLocalState :=
  mkNamingLocalState@{
    evidenceStore : Set IdentityNameEvidence;
  };

syntax alias NamingTimerHandle := Unit;

NamingEnv : Type :=
  EngineEnv NamingLocalState NamingMailboxState NamingTimerHandle Anoma.Msg;

module naming_environment_example;
  
  namingEnv : NamingEnv :=
    mkEngineEnv@{
      localState :=
        mkNamingLocalState@{
          evidenceStore := Set.empty;
        };
      mailboxCluster := Map.empty;
      acquaintances := Set.empty;
      timers := [];
    };
end;