import Spec.Prelude

/-!
# AgentRole —— Agent 角色与技能配置 (ADR-0017, ADR-0018)

AgentRole 是 org-scoped 运行时配置:system prompt、tool allowlist、default model
和 skill 绑定。通过 CLI 管理,不需重启进程生效。

Role 的执行面(model/prompt/tools/skill 内容)变更时,该 role 的 active sessions
归档——下次 run 不能在旧指令下创建的 provider context 上恢复。
仅 label/排序变更不影响会话连续性(ADR-0017)。

Run 时只读加载 role 选中的 skill 不可变版本到 run-scoped 目录,
run 结束后删除(ADR-0018)。Skill 管理是 org-scoped;存储机制 `OPEN`。

管理面分组:skill 与 role 共用一棵 org 内可嵌套 folder 树(ADR-0028)。folder 是透明
组织节点——只做后台导航/分组,不进入身份、解析与授权;name/roleId 唯一性、role→skill
绑定、run 加载与 slash 命令均与 folder 无关。
-/

namespace Spec.System

variable (I : Identifiers)

/-- Agent 角色(`PINNED`, org-scoped, ADR-0017)。 -/
structure AgentRole where
  /-- 所属组织(`PINNED`)。 -/
  organization : I.OrganizationId
  /-- 斜杠命令名(`OPEN` 表示;如 /draft)。 -/
  roleId : String
  /-- system prompt(`PINNED`)。 -/
  systemPrompt : String
  /-- tool allowlist(`PINNED`;tool 标识集合 `OPEN`)。 -/
  tools : List String
  /-- 默认 model(`PINNED`;model ID 表示 `OPEN`)。 -/
  defaultModel : String
  /-- 管理面分组 folder(`PINNED`, ADR-0028;`none` 表示未分类)。透明节点,见
  `AgentConfigFolder`——不进入 role 的身份与解析,roleId 仍 org 内唯一。 -/
  folder : Option I.AgentConfigFolderId

/-- Agent 技能(`PINNED`, org-scoped, ADR-0017/0018)。 -/
structure AgentSkill where
  /-- 所属组织(`PINNED`)。 -/
  organization : I.OrganizationId
  /-- 名称(`PINNED`)。 -/
  name : String
  /-- 版本(`PINNED`)。 -/
  version : String
  /-- 内容摘要(`PINNED`;SHA-256 content-addressed)。 -/
  contentDigest : String
  /-- 描述(`OPEN`)。 -/
  description : String
  /-- 管理面分组 folder(`PINNED`, ADR-0028;`none` 表示未分类)。透明节点,见
  `AgentConfigFolder`——不进入 skill 的身份与解析,name 仍 org 内唯一。 -/
  folder : Option I.AgentConfigFolderId

/-- Role-Skill 绑定(`PINNED`, ADR-0017)。一个 role 可绑定零或多个 skill。 -/
structure AgentRoleSkillBinding where
  /-- 所属组织(`PINNED`)。 -/
  organization : I.OrganizationId
  /-- 绑定的 role(`PINNED`)。 -/
  roleId : String
  /-- skill 名称(`PINNED`)。 -/
  skillName : String
  /-- skill 版本(`PINNED`)。 -/
  skillVersion : String
  /-- 排序(`PINNED`)。 -/
  sortOrder : Nat

/-- Agent 配置 folder(`PINNED`, org-scoped, ADR-0028):skill 与 role **共用**的一棵
可嵌套 folder 树的节点,仅承担管理面的导航与分组。它是透明组织节点(与 ADR-0021
project Folder 同例):不是权限资源、不持有 grants;不进入 skill name / roleId 的身份
与解析——name/roleId 仍在 org 内唯一、与 folder 无关;role→skill 绑定、run 的 skill
快照加载与飞书 slash 命令均不引用 folder。folder 归属变更是 label 类变更
(ADR-0017),不归档会话。folder 仅在为空(无子 folder、无挂载的 skill/role)时可删
(`PINNED`)——挂载物的级动归置规则未定,故先禁止。 -/
structure AgentConfigFolder where
  /-- 所属组织(`PINNED`)。 -/
  organization : I.OrganizationId
  /-- folder 标识(`OPEN` 表示)。 -/
  id : I.AgentConfigFolderId
  /-- 父 folder;`none` 为根层(`PINNED`,可嵌套)。 -/
  parent : Option I.AgentConfigFolderId

/-- Skill/role 的 folder 归属良构性(`PINNED`, ADR-0028):每个 skill/role 至多归属于
一个 folder,且只能归属于与其**同 org** 的 folder;`none`(未分类)总是良构。
移动 skill/role 进出 folder 不改变其自身授权与解析。 -/
def AgentConfigFolderPlacement.WellScoped
    (organization : I.OrganizationId)
    (placement : Option I.AgentConfigFolderId)
    (folderOrg : I.AgentConfigFolderId → Option I.OrganizationId) : Prop :=
  ∀ folderId, placement = some folderId → folderOrg folderId = some organization

end Spec.System