refactor(spec): move AgentRole/Run/Memory/AgentSurface into System/Agent/ subdir

2026-07-12 18:43:11 +08:00
parent a4449f03c4
commit be4260bcd0
8 changed files with 9 additions and 9 deletions
@@ -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
@@ -0,0 +1,44 @@
+import Spec.Prelude
+import Spec.System.Agent.Run
+
+/-!
+# AgentSurface —— Agent 执行面边界(ADR-0018)
+
+ADR-0001/0002/0004 覆盖"协作治理"直到 `triggerAgent`:谁能触发一次 run。但触发之后
+agent 在执行层面能干什么——读哪些文件、跑什么命令——任何 ADR / 散文都未定。ADR-0017
+落地时采用 Claude Code SDK 的 `bypassPermissions` + 全量 Read/Write/Bash/Glob/Grep,
+agent 的文件与 shell 面对宿主**无界**:spec 与 ADR 均未钉死边界。本模块补这一层。
+
+钉死的不变式:agent 在一次 run 内发起的文件操作,其路径必须落在该 run 所属 project
+的工作区目录内(ADR-0007:工程文件是目录树;此 ADR 固定"agent 操作落在该树内")。
+逃逸即越权,拒绝。与 `Lock`(ADR-0002)正交:Lock 限定**并发**(谁在改),Surface
+限定**波及面**(能改到哪)。二者都按 run × project 作用域。
+
+shell 面的边界(命令的文件效果同样不得逃逸工作区)是同一不变式的推论,但**机制**
+——路径校验工具包装、OS 级沙箱(bubblewrap/容器)、SDK 权限钩子,或其组合——`OPEN`
+(ADR-0018)。契约钉死不变式,不钉死机制。
+-/
+
+namespace Spec.System
+
+variable (I : Identifiers) (Path : Type)
+
+/-- Agent 在一次 run 内发起的文件操作(`PINNED` 关系, ADR-0018)。由某 run 发起、
+指向某路径;是否越权由下方 `Authorized` 钉死。 -/
+structure AgentFileOp where
+  /-- 发起操作的 run(授权上下文主体, ADR-0018;与 `Lock` 同作用域 run × project)。 -/
+  run : I.RunId
+  /-- 操作目标路径(`PINNED` 字段, ADR-0018)。 -/
+  path : Path
+
+/-- 工作区边界良构:run 的文件操作路径必须落在该 run 所属 project 的工作区目录内
+(`PINNED` 平台核心安全不变式, ADR-0018)。`runWorkspace` 与 `pathWithin` 均由平台提供
+(表示 `OPEN`——路径如何表示、"在内"如何判定是纯 plumbing,非本层分歧点);本谓词只
+钉死"操作路径必须以 run 的工作区为根",杜绝 agent 越权读写宿主任意文件。 -/
+def AgentFileOp.Authorized
+    (op : AgentFileOp I Path)
+    (runWorkspace : I.RunId → Option Path)
+    (pathWithin : Path → Path → Prop) : Prop :=
+  ∃ w, runWorkspace op.run = some w ∧ pathWithin op.path w
+
+end Spec.System
@@ -0,0 +1,51 @@
+import Spec.Prelude
+
+/-!
+# Memory —— 按需上下文:锚点与项目记忆(ADR-0003)
+
+ADR-0003:Hub **只存锚点与项目记忆**,不存全量飞书消息历史;Claude 需要更多上下文时经
+飞书 API 按需读取。本模块刻画所存锚点的**类别**(ADR 列定,枚举完整性 OPEN——ADR 是
+"例如"式列举,新增类别不违反契约),并钉死一条 likec4 画不出的安全不变式:**MCP 工具
+按 run/project 上下文授权,Claude 不得传任意 chat id**(ADR-0003 Consequences 末条)。
+
+"chat id 与 project 绑定"这一锚点类别由 `ProjectGroup.GroupBinding`(ADR-0001)权威承载,
+本模块不重复声明,只覆盖其余飞书侧指针(触发消息、状态卡片、回复、线程)。
+-/
+
+namespace Spec.System
+
+variable (I : Identifiers)
+variable (MessageId CardId : Type)
+
+/-- 上下文锚点(`PINNED` 类别, ADR-0003 列定;**枚举完整性 `OPEN`**——ADR 是"例如"式
+列举,实现若需新类别须 surface,不得默认本枚举已穷尽)。承载 Hub 保留的飞书侧最小指针,
+而非消息正文。 -/
+inductive Anchor where
+  /-- 触发某次 run 的消息(`PINNED` 类别, ADR-0003 "trigger message id")。 -/
+  | triggerMessage : MessageId → Anchor
+  /-- 某 run 的状态卡片(`PINNED` 类别, ADR-0003 "run id and status card id")。 -/
+  | statusCard : I.RunId → CardId → Anchor
+  /-- 回复锚点(`PINNED` 类别, ADR-0003 "reply anchors")。 -/
+  | reply : MessageId → Anchor
+  /-- 线程锚点(`PINNED` 类别, ADR-0003 "thread anchors")。 -/
+  | thread : MessageId → Anchor
+
+/-- MCP 读上下文请求:由某 run 发起、指向某 chat(`PINNED` 关系, ADR-0003 "Claude calls
+MCP tools to read … through Feishu APIs")。 -/
+structure McpReadRequest where
+  /-- 发起请求的 run(授权上下文主体, ADR-0003)。 -/
+  run : I.RunId
+  /-- 请求读取的 chat(是否允许越界由下方 `Authorized` 钉死:不允许)。 -/
+  chat : I.ChatId
+
+/-- 请求获授权:其 chat 必须等于该 run 所属 project 的绑定群(`PINNED` 安全不变式,
+ADR-0003 Consequences "MCP tools must authorize by run/project context; Claude cannot
+pass arbitrary chat ids")。`runProject`/`boundChat` 由平台提供(表示 `OPEN`);本谓词只
+钉死"chat 必须匹配 run 的 project 绑定",杜绝 Claude 传任意 chat id 越权读取。 -/
+def McpReadRequest.Authorized
+    (req : McpReadRequest I)
+    (runProject : I.RunId → Option I.ProjectId)
+    (boundChat : I.ProjectId → Option I.ChatId) : Prop :=
+  ∃ p, runProject req.run = some p ∧ boundChat p = some req.chat
+
+end Spec.System
@@ -0,0 +1,30 @@
+/-!
+# Run —— AgentRun 状态机
+
+一次 `@Claude` 创建一个 `AgentRun`(ADR-0001),它在终止时释放项目锁(ADR-0002)。
+合法转移关系在任何 ADR / likec4 散文里都未定下,故本模块只刻画**状态**与**终止
+判定**(后者是 Lock 排他不变式的依赖),不臆造转移边。
+-/
+
+namespace Spec.System
+
+/-- AgentRun 运行状态(状态名 `PINNED`, ADR-0001..0003, ADR-0022 + likec4;
+**完整性 `OPEN`**——散文从未声明"状态恰好这些";实现若需新状态(如 pending)须
+surface,不得默认本枚举已穷尽)。终止态见 `RunState.Terminal`。 -/
+inductive RunState where
+  | active
+  | waitingForUser
+  | completed
+  | failed
+  | timedOut
+  | limitExceeded
+  | canceled
+
+/-- run 处于**终止态**(`PINNED`, ADR-0002, ADR-0022:锁在 completes/fails/
+timesOut/limitExceeded/canceled 时释放)。`active`/`waitingForUser` 非终止——后者仍
+占用项目(锁未释放)。 -/
+def RunState.Terminal : RunState → Prop
+  | .completed | .failed | .timedOut | .limitExceeded | .canceled => True
+  | .active | .waitingForUser => False
+
+end Spec.System