Skip to content
Juvix imports 

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.

Auxiliary Juvix code 

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;
  };
Arguments
backend:
The backend associated with this identity.
capabilities:
The capabilities available to this identity.
commitmentEngine:
Optional reference to the commitment engine for this identity.
decryptionEngine:
Optional reference to the decryption engine for this identity.

IdentityManagementLocalState

type IdentityManagementLocalState :=
  mkIdentityManagementLocalState@{
    identities : Map EngineID IdentityInfo;
  };
Arguments
identities:
Map of engine IDs to their corresponding identity information.

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 := [];
  };