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;

Naming Environment¶

Overview¶

The Naming Engine maintains the state necessary for managing associations between IdentityNames and ExternalIdentitys, including storing evidence submitted by clients.

axiom verifyEvidence : IdentityNameEvidence -> Bool;

Mailbox states¶

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

NamingMailboxState¶

syntax alias NamingMailboxState := Unit;

Local state¶

The local state of the Naming Engine includes the evidence for name associations.

NamingLocalState¶

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

Timer Handle¶

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

NamingTimerHandle¶

syntax alias NamingTimerHandle := Unit;

The Naming Environment¶

NamingEnv¶

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

Instantiation¶

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