Juvix imports

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;

Naming Environment

Overview

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

Mailbox states

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

syntax alias NamingMailboxState := Unit;

Local state

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

type NamingLocalState :=
  mkNamingLocalState {
    evidenceStore : Set IdentityNameEvidence;
    verifyEvidence : IdentityNameEvidence -> Bool
  };

Timer Handle

syntax alias NamingTimerHandle := Unit;

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

Environment summary

NamingEnvironment : Type :=
  EngineEnvironment NamingLocalState NamingMailboxState NamingTimerHandle;

Example of a Naming environment

namingEnvironmentExample : NamingEnvironment :=
  mkEngineEnvironment@{
    name := "naming";
    localState :=
      mkNamingLocalState@{
        evidenceStore := Set.empty;
        verifyEvidence := \ {_ := true}
      };
    mailboxCluster := Map.empty;
    acquaintances := Set.empty;
    timers := []
  };