From 01bc20d25fdc8a8c495447a28692ae3e077878b0 Mon Sep 17 00:00:00 2001
From: sjfhsjfh <sjfhsjfh@qq.com>
Date: Sun, 12 Jul 2026 18:38:17 +0800
Subject: [PATCH] feat(spec): add AgentRole, AgentSkill, RoleSkillBinding
 (ADR-0017/0018)

---
 spec/Spec/System.lean              |  2 +
 spec/Spec/System/AgentRole.lean    | 60 ++++++++++++++++++++++++++++++
 spec/Spec/System/Organization.lean |  3 +-
 3 files changed, 64 insertions(+), 1 deletion(-)
 create mode 100644 spec/Spec/System/AgentRole.lean

diff --git a/spec/Spec/System.lean b/spec/Spec/System.lean
index 3a4db08..4eb2702 100644
--- a/spec/Spec/System.lean
+++ b/spec/Spec/System.lean
@@ -13,6 +13,7 @@ import Spec.System.AgentSurface
 import Spec.System.Permission
 import Spec.System.PermissionGrant
 import Spec.System.Audit
+import Spec.System.AgentRole
 /-!
 # System —— Hub 平台层契约
 
@@ -27,6 +28,7 @@ import Spec.System.Audit
 - `Organization` —— SaaS 租户(ADR-0020);project/team 单归属,TEAM grant 不跨 org;
   connection secret 信封与 fail-closed resolver(ADR-0024);
   owner/admin/member(`OrganizationRole`)及其管理规则(最后所有者保护)。
+- `AgentRole` —— org-scoped agent 角色配置 + 技能(ADR-0017/0018)。
 - `ProjectWorkspace` —— org 后台 project explorer:folder 是透明组织节点,project 仍是权限边界
   (ADR-0021)。
 - `Capacity` —— platform ceiling 与 org policy 的分层限制、持久 admission request 状态和
diff --git a/spec/Spec/System/AgentRole.lean b/spec/Spec/System/AgentRole.lean
new file mode 100644
index 0000000..70aeedd
--- /dev/null
+++ b/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
diff --git a/spec/Spec/System/Organization.lean b/spec/Spec/System/Organization.lean
index 972c0a8..b7d583a 100644
--- a/spec/Spec/System/Organization.lean
+++ b/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