feat(spec): add AgentRole, AgentSkill, RoleSkillBinding (ADR-0017/0018)

spec/Spec/System/AgentRole.lean

@@ -0,0 +1,60 @@
+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`。
+-/
+
+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
+
+/-- 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
+
+/-- 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
+
+end Spec.System

spec/Spec/System/Organization.lean

@@ -5,7 +5,8 @@ import Spec.Prelude
 
 组织就是租户。project/team 必须归属且仅归属一个 org;team→project grant 必须同 org。
 组织实体见 `Hierarchy.Organization`;用户见 `Spec.System.User`;平台控制面见
-`PlatformAdministration`(ADR-0023)。凭据信封见 ADR-0024。
+`PlatformAdministration`(ADR-0023)。凭据信封见 ADR-0024。Agent 角色配置见
+`Spec.System.AgentRole`。
 -/
 
 namespace Spec.System