module arch.node.engines.identity_management_behaviour; import prelude open; import arch.node.engines.commitment_config open; import arch.node.engines.decryption_config open; import arch.node.engines.commitment_environment open; import arch.node.engines.decryption_environment open; import arch.node.engines.identity_management_environment open; import arch.node.engines.identity_management_messages open; import arch.node.engines.identity_management_config open; import arch.node.types.anoma as Anoma open; import arch.node.types.engine open; import arch.node.types.engine_environment open; import arch.node.types.identities open; import arch.node.types.messages open; import arch.system.identity.identity open hiding {ExternalIdentity}; type MessageFrom := mkMessageFrom@{ whoAsked : Option EngineID; mailbox : Option MailboxID; }; type IdentityManagementActionArgument := | IdentityManagementActionArgumentMessageFrom MessageFrom; IdentityManagementActionArguments : Type := List IdentityManagementActionArgument; IdentityManagementAction : Type := Action IdentityManagementCfg IdentityManagementLocalState IdentityManagementMailboxState IdentityManagementTimerHandle IdentityManagementActionArguments Anoma.Msg Anoma.Cfg Anoma.Env; IdentityManagementActionInput : Type := ActionInput IdentityManagementCfg IdentityManagementLocalState IdentityManagementMailboxState IdentityManagementTimerHandle IdentityManagementActionArguments Anoma.Msg; IdentityManagementActionEffect : Type := ActionEffect IdentityManagementLocalState IdentityManagementMailboxState IdentityManagementTimerHandle Anoma.Msg Anoma.Cfg Anoma.Env; IdentityManagementActionExec : Type := ActionExec IdentityManagementCfg IdentityManagementLocalState IdentityManagementMailboxState IdentityManagementTimerHandle IdentityManagementActionArguments Anoma.Msg Anoma.Cfg Anoma.Env; hasCommitCapability (capabilities : Capabilities) : Bool := case capabilities of | Capabilities.Commit := true | Capabilities.CommitAndDecrypt := true | _ := false; hasDecryptCapability (capabilities : Capabilities) : Bool := case capabilities of | Capabilities.Decrypt := true | Capabilities.CommitAndDecrypt := true | _ := false; isSubsetCapabilities (requested : Capabilities) (available : Capabilities) : Bool := (not (hasCommitCapability requested) || hasCommitCapability available) && not (hasDecryptCapability requested) || hasDecryptCapability available; updateIdentityAndSpawnEngines (env : IdentityManagementEnv) (backend' : Backend) (whoAsked : EngineID) (identityInfo : IdentityInfo) (capabilities' : Capabilities) : Pair IdentityInfo (List (Pair Cfg Env)) := let decryptionConfig : DecryptionCfg := DecryptionCfg.mk@{ decryptor := genDecryptor backend'; backend := backend'; }; decryptionEnv : DecryptionEnv := EngineEnv.mk@{ localState := unit; mailboxCluster := Map.empty; acquaintances := Set.empty; timers := []; }; decryptionEng : Pair Cfg Env := mkPair (PreCfg.CfgDecryption decryptionConfig) (PreEnv.EnvDecryption decryptionEnv); commitmentConfig : CommitmentCfg := CommitmentCfg.mk@{ signer := genSigner backend'; backend := backend'; }; commitmentEnv : CommitmentEnv := EngineEnv.mk@{ localState := unit; mailboxCluster := Map.empty; acquaintances := Set.empty; timers := []; }; commitmentEng : Pair Cfg Env := mkPair (PreCfg.CfgCommitment commitmentConfig) (PreEnv.EnvCommitment commitmentEnv); in case capabilities' of | Capabilities.CommitAndDecrypt := let spawnedEngines := [decryptionEng; commitmentEng]; commitmentEngineName := nameGen "committer" (snd whoAsked) whoAsked; decryptionEngineName := nameGen "decryptor" (snd whoAsked) whoAsked; updatedIdentityInfo1 := identityInfo@IdentityInfo{ commitmentEngine := some (mkPair none commitmentEngineName); decryptionEngine := some (mkPair none decryptionEngineName); }; in mkPair updatedIdentityInfo1 spawnedEngines | Capabilities.Commit := let spawnedEngines := [commitmentEng]; commitmentEngineName := nameGen "committer" (snd whoAsked) whoAsked; updatedIdentityInfo1 := identityInfo@IdentityInfo{commitmentEngine := some (mkPair none commitmentEngineName)}; in mkPair updatedIdentityInfo1 spawnedEngines | Capabilities.Decrypt := let spawnedEngines := [decryptionEng]; decryptionEngineName := nameGen "decryptor" (snd whoAsked) whoAsked; updatedIdentityInfo1 := identityInfo@IdentityInfo{decryptionEngine := some (mkPair none decryptionEngineName)}; in mkPair updatedIdentityInfo1 spawnedEngines; copyEnginesForCapabilities (env : IdentityManagementEnv) (whoAsked : EngineID) (externalIdentityInfo : IdentityInfo) (requestedCapabilities : Capabilities) : IdentityInfo := let newIdentityInfo := IdentityInfo.mkIdentityInfo@{ backend := IdentityInfo.backend externalIdentityInfo; capabilities := requestedCapabilities; commitmentEngine := case hasCommitCapability requestedCapabilities of | true := IdentityInfo.commitmentEngine externalIdentityInfo | false := none; decryptionEngine := case hasDecryptCapability requestedCapabilities of | true := IdentityInfo.decryptionEngine externalIdentityInfo | false := none; }; in newIdentityInfo; generateIdentityAction (input : IdentityManagementActionInput) : Option IdentityManagementActionEffect := let env := ActionInput.env input; local := EngineEnv.localState env; identities := IdentityManagementLocalState.identities local; trigger := ActionInput.trigger input; in case getEngineMsgFromTimestampedTrigger trigger of | some emsg := let whoAsked := EngineMsg.sender emsg; in case Map.lookup whoAsked identities of { | some _ := some ActionEffect.mk@{ env := env; msgs := [ EngineMsg.mk@{ sender := getEngineIDFromEngineCfg (ActionInput.cfg input); target := whoAsked; mailbox := some 0; msg := PreMsg.MsgIdentityManagement (IdentityManagementMsg.GenerateIdentityReply ReplyGenerateIdentity.mkReplyGenerateIdentity@{ commitmentEngine := none; decryptionEngine := none; externalIdentity := whoAsked; err := some "Identity already exists"; }); }; ]; timers := []; engines := []; } | none := case emsg of { | EngineMsg.mk@{ msg := Anoma.PreMsg.MsgIdentityManagement (IdentityManagementMsg.GenerateIdentityRequest (RequestGenerateIdentity.mkRequestGenerateIdentity backend' params' capabilities')); } := let identityInfo := IdentityInfo.mkIdentityInfo@{ backend := backend'; capabilities := capabilities'; commitmentEngine := none; decryptionEngine := none; }; pair' := updateIdentityAndSpawnEngines env backend' whoAsked identityInfo capabilities'; updatedIdentityInfo := fst pair'; spawnedEnginesFinal := snd pair'; updatedIdentities := Map.insert whoAsked updatedIdentityInfo identities; newLocalState := local@IdentityManagementLocalState{identities := updatedIdentities}; newEnv' := env@EngineEnv{localState := newLocalState}; in some ActionEffect.mk@{ env := newEnv'; msgs := [ EngineMsg.mk@{ sender := getEngineIDFromEngineCfg (ActionInput.cfg input); target := whoAsked; mailbox := some 0; msg := PreMsg.MsgIdentityManagement (IdentityManagementMsg.GenerateIdentityReply ReplyGenerateIdentity.mkReplyGenerateIdentity@{ commitmentEngine := IdentityInfo.commitmentEngine updatedIdentityInfo; decryptionEngine := IdentityInfo.decryptionEngine updatedIdentityInfo; externalIdentity := whoAsked; err := none; }); }; ]; timers := []; engines := spawnedEnginesFinal; } | _ := none } } | _ := none; connectIdentityAction (input : IdentityManagementActionInput) : Option IdentityManagementActionEffect := let env := ActionInput.env input; local := EngineEnv.localState env; identities := IdentityManagementLocalState.identities local; trigger := ActionInput.trigger input; in case getEngineMsgFromTimestampedTrigger trigger of | some emsg := let whoAsked := EngineMsg.sender emsg; in case Map.lookup whoAsked identities of { | some _ := some ActionEffect.mk@{ env := env; msgs := [ EngineMsg.mk@{ sender := getEngineIDFromEngineCfg (ActionInput.cfg input); target := whoAsked; mailbox := some 0; msg := PreMsg.MsgIdentityManagement (IdentityManagementMsg.ConnectIdentityReply ReplyConnectIdentity.mkReplyConnectIdentity@{ commitmentEngine := none; decryptionEngine := none; err := some "Identity already exists"; }); }; ]; timers := []; engines := []; } | none := case emsg of { | EngineMsg.mk@{ msg := Anoma.PreMsg.MsgIdentityManagement (IdentityManagementMsg.ConnectIdentityRequest (RequestConnectIdentity.mkRequestConnectIdentity externalIdentity' backend' capabilities')); } := case Map.lookup externalIdentity' identities of { | none := some ActionEffect.mk@{ env := env; msgs := [ EngineMsg.mk@{ sender := getEngineIDFromEngineCfg (ActionInput.cfg input); target := whoAsked; mailbox := some 0; msg := PreMsg.MsgIdentityManagement (IdentityManagementMsg.ConnectIdentityReply ReplyConnectIdentity.mkReplyConnectIdentity@{ commitmentEngine := none; decryptionEngine := none; err := some "External identity not found"; }); }; ]; timers := []; engines := []; } | some externalIdentityInfo := if | isSubsetCapabilities capabilities' (IdentityInfo.capabilities externalIdentityInfo) := let newIdentityInfo := copyEnginesForCapabilities env whoAsked externalIdentityInfo capabilities'; updatedIdentities := Map.insert whoAsked newIdentityInfo identities; newLocalState := local@IdentityManagementLocalState{identities := updatedIdentities}; newEnv' := env@EngineEnv{localState := newLocalState}; in some ActionEffect.mk@{ env := newEnv'; msgs := [ EngineMsg.mk@{ sender := getEngineIDFromEngineCfg (ActionInput.cfg input); target := whoAsked; mailbox := some 0; msg := PreMsg.MsgIdentityManagement (IdentityManagementMsg.ConnectIdentityReply ReplyConnectIdentity.mkReplyConnectIdentity@{ commitmentEngine := IdentityInfo.commitmentEngine newIdentityInfo; decryptionEngine := IdentityInfo.decryptionEngine newIdentityInfo; err := none; }); }; ]; timers := []; engines := []; } | else := some ActionEffect.mk@{ env := env; msgs := [ EngineMsg.mk@{ sender := getEngineIDFromEngineCfg (ActionInput.cfg input); target := whoAsked; mailbox := some 0; msg := PreMsg.MsgIdentityManagement (IdentityManagementMsg.ConnectIdentityReply ReplyConnectIdentity.mkReplyConnectIdentity@{ commitmentEngine := none; decryptionEngine := none; err := some "Capabilities not available"; }); }; ]; timers := []; engines := []; } } | _ := none } } | _ := none; deleteIdentityAction (input : IdentityManagementActionInput) : Option IdentityManagementActionEffect := let env := ActionInput.env input; local := EngineEnv.localState env; identities := IdentityManagementLocalState.identities local; trigger := ActionInput.trigger input; in case getEngineMsgFromTimestampedTrigger trigger of | some emsg := let whoAsked := EngineMsg.sender emsg; in case emsg of { | EngineMsg.mk@{ msg := Anoma.PreMsg.MsgIdentityManagement (IdentityManagementMsg.DeleteIdentityRequest (RequestDeleteIdentity.mkRequestDeleteIdentity externalIdentity backend')); } := case Map.lookup externalIdentity identities of { | none := some ActionEffect.mk@{ env := env; msgs := [ EngineMsg.mk@{ sender := getEngineIDFromEngineCfg (ActionInput.cfg input); target := whoAsked; mailbox := some 0; msg := PreMsg.MsgIdentityManagement (IdentityManagementMsg.DeleteIdentityReply ReplyDeleteIdentity.mkReplyDeleteIdentity@{ err := some "Identity does not exist"; }); }; ]; timers := []; engines := []; } | some _ := let updatedIdentities := Map.delete externalIdentity identities; newLocalState := local@IdentityManagementLocalState{identities := updatedIdentities}; newEnv' := env@EngineEnv{localState := newLocalState}; in some ActionEffect.mk@{ env := newEnv'; msgs := [ EngineMsg.mk@{ sender := getEngineIDFromEngineCfg (ActionInput.cfg input); target := whoAsked; mailbox := some 0; msg := PreMsg.MsgIdentityManagement (IdentityManagementMsg.DeleteIdentityReply ReplyDeleteIdentity.mkReplyDeleteIdentity@{ err := none; }); }; ]; timers := []; engines := []; } } | _ := none } | _ := none; generateIdentityActionLabel : IdentityManagementActionExec := ActionExec.Seq [generateIdentityAction]; connectIdentityActionLabel : IdentityManagementActionExec := ActionExec.Seq [connectIdentityAction]; deleteIdentityActionLabel : IdentityManagementActionExec := ActionExec.Seq [deleteIdentityAction]; IdentityManagementGuard : Type := Guard IdentityManagementCfg IdentityManagementLocalState IdentityManagementMailboxState IdentityManagementTimerHandle IdentityManagementActionArguments Anoma.Msg Anoma.Cfg Anoma.Env; IdentityManagementGuardOutput : Type := GuardOutput IdentityManagementCfg IdentityManagementLocalState IdentityManagementMailboxState IdentityManagementTimerHandle IdentityManagementActionArguments Anoma.Msg Anoma.Cfg Anoma.Env; IdentityManagementGuardEval : Type := GuardEval IdentityManagementCfg IdentityManagementLocalState IdentityManagementMailboxState IdentityManagementTimerHandle IdentityManagementActionArguments Anoma.Msg Anoma.Cfg Anoma.Env; generateIdentityGuard (trigger : TimestampedTrigger IdentityManagementTimerHandle Anoma.Msg) (cfg : EngineCfg IdentityManagementCfg) (env : IdentityManagementEnv) : Option IdentityManagementGuardOutput := case getEngineMsgFromTimestampedTrigger trigger of | some EngineMsg.mk@{ msg := Anoma.PreMsg.MsgIdentityManagement (IdentityManagementMsg.GenerateIdentityRequest _); } := some GuardOutput.mk@{ action := generateIdentityActionLabel; args := []; } | _ := none; connectIdentityGuard (trigger : TimestampedTrigger IdentityManagementTimerHandle Anoma.Msg) (cfg : EngineCfg IdentityManagementCfg) (env : IdentityManagementEnv) : Option IdentityManagementGuardOutput := case getEngineMsgFromTimestampedTrigger trigger of | some EngineMsg.mk@{ msg := Anoma.PreMsg.MsgIdentityManagement (IdentityManagementMsg.ConnectIdentityRequest _); } := some GuardOutput.mk@{ action := connectIdentityActionLabel; args := []; } | _ := none; deleteIdentityGuard (trigger : TimestampedTrigger IdentityManagementTimerHandle Anoma.Msg) (cfg : EngineCfg IdentityManagementCfg) (env : IdentityManagementEnv) : Option IdentityManagementGuardOutput := case getEngineMsgFromTimestampedTrigger trigger of | some EngineMsg.mk@{ msg := Anoma.PreMsg.MsgIdentityManagement (IdentityManagementMsg.DeleteIdentityRequest _); } := some GuardOutput.mk@{ action := deleteIdentityActionLabel; args := []; } | _ := none; IdentityManagementBehaviour : Type := EngineBehaviour IdentityManagementCfg IdentityManagementLocalState IdentityManagementMailboxState IdentityManagementTimerHandle IdentityManagementActionArguments Anoma.Msg Anoma.Cfg Anoma.Env; identityManagementBehaviour : IdentityManagementBehaviour := EngineBehaviour.mk@{ guards := GuardEval.First [generateIdentityGuard; connectIdentityGuard; deleteIdentityGuard]; };