module arch.node.engines.identity_management_environment;

import prelude open;
import arch.node.types.messages open;
import arch.node.types.crypto open;
import arch.node.types.identities open;
import arch.node.types.engine_environment open;
import arch.node.engines.identity_management_messages open;
import arch.node.types.anoma_message as Anoma open;
import arch.system.identity.identity open hiding {ExternalIdentity};

Identity Management Environment¶

Overview¶

The Identity Management Engine's environment maintains the state necessary for managing identities, including information about connected identities, backends, and capabilities.

axiom genDecryptor : Backend -> Decryptor Backend Plaintext Ciphertext;

axiom genSigner : Backend -> Signer Backend Signable Commitment;

Mailbox states¶

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

IdentityManagementMailboxState¶

syntax alias IdentityManagementMailboxState := Unit;

Local state¶

The local state of the Identity Management Engine includes information about the identities it manages.

IdentityInfo¶

type IdentityInfo :=
  mkIdentityInfo@{
    backend : Backend;
    capabilities : Capabilities;
    commitmentEngine : Option EngineID;
    decryptionEngine : Option EngineID;
  };

IdentityManagementLocalState¶

type IdentityManagementLocalState :=
  mkIdentityManagementLocalState@{identities : Map EngineID IdentityInfo};

Timer Handle¶

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

IdentityManagementTimerHandle¶

syntax alias IdentityManagementTimerHandle := Unit;

The Identity Management Environment¶

IdentityManagementEnv¶

IdentityManagementEnv : Type :=
  EngineEnv
    IdentityManagementLocalState
    IdentityManagementMailboxState
    IdentityManagementTimerHandle
    Anoma.Msg;

Instantiation¶

identityManagementEnv : IdentityManagementEnv :=
  mkEngineEnv@{
    localState :=
      mkIdentityManagementLocalState@{
        identities := Map.empty;
      };
    mailboxCluster := Map.empty;
    acquaintances := Set.empty;
    timers := [];
  };