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};

axiom genDecryptor : Backend -> Decryptor Backend Plaintext Ciphertext;

axiom genSigner : Backend -> Signer Backend Signable Commitment;

syntax alias IdentityManagementMailboxState := Unit;

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

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

syntax alias IdentityManagementTimerHandle := Unit;

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

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