From be4260bcd0edc693b2566b8127833fe72c9ce2a4 Mon Sep 17 00:00:00 2001
From: sjfhsjfh <sjfhsjfh@qq.com>
Date: Sun, 12 Jul 2026 18:43:11 +0800
Subject: [PATCH] refactor(spec): move AgentRole/Run/Memory/AgentSurface into
 System/Agent/ subdir

---
 spec/README.md                                 |  2 +-
 spec/Spec/System.lean                          | 10 +++++-----
 spec/Spec/System/{ => Agent}/AgentRole.lean    |  0
 spec/Spec/System/{ => Agent}/AgentSurface.lean |  2 +-
 spec/Spec/System/{ => Agent}/Memory.lean       |  0
 spec/Spec/System/{ => Agent}/Run.lean          |  0
 spec/Spec/System/Lock.lean                     |  2 +-
 spec/Spec/System/Organization.lean             |  2 +-
 8 files changed, 9 insertions(+), 9 deletions(-)
 rename spec/Spec/System/{ => Agent}/AgentRole.lean (100%)
 rename spec/Spec/System/{ => Agent}/AgentSurface.lean (98%)
 rename spec/Spec/System/{ => Agent}/Memory.lean (100%)
 rename spec/Spec/System/{ => Agent}/Run.lean (100%)

diff --git a/spec/README.md b/spec/README.md
index 851b345..b5e8a3a 100644
--- a/spec/README.md
+++ b/spec/README.md
@@ -49,7 +49,7 @@ agent 不得用预训练先验脑补本领域(领域很新,无先验);prose 是
 
 ### 命名
 
-- **模块 / 命名空间**:PascalCase,对应分层,如 `Spec.System.Run`、`Spec.Courseware.Validity`。
+- **模块 / 命名空间**:PascalCase,对应分层,如 `Spec.System.Agent.Run`、`Spec.Courseware.Validity`。
 - **类型**:PascalCase。
 - **谓词 / `Prop`**:用意图清晰的命名,如 `Legal…`、`ValidTransition`、`Can…`。
 - **文件粒度**:原则上"一个带独立不变式的概念一个文件"。
diff --git a/spec/Spec/System.lean b/spec/Spec/System.lean
index 4eb2702..0b9796c 100644
--- a/spec/Spec/System.lean
+++ b/spec/Spec/System.lean
@@ -6,14 +6,14 @@ import Spec.System.Connections
 import Spec.System.ProjectWorkspace
 import Spec.System.Capacity
 import Spec.System.PlatformAdministration
-import Spec.System.Run
+import Spec.System.Agent.Run
+import Spec.System.Agent.AgentRole
+import Spec.System.Agent.Memory
+import Spec.System.Agent.AgentSurface
 import Spec.System.Lock
-import Spec.System.Memory
-import Spec.System.AgentSurface
 import Spec.System.Permission
 import Spec.System.PermissionGrant
 import Spec.System.Audit
-import Spec.System.AgentRole
 /-!
 # System —— Hub 平台层契约
 
@@ -28,13 +28,13 @@ import Spec.System.AgentRole
 - `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 状态和
   平台紧急工作负载制动(ADR-0022)。
 - `PlatformAdministration` —— 独立平台身份/会话、单一管理员角色、绑定邀请、最后管理员
   保护、fail-closed 平台审计与离线 emergency grant(ADR-0023)。
+- `AgentRole` —— org-scoped agent 角色配置 + 技能(ADR-0017/0018)。
 - `Run` —— AgentRun 状态与终止判定(状态集合完整性 OPEN)。
 - `Lock` —— 锁 owner=run(ADR-0002),及"持锁者必为非终止 run"的核心不变式。
 - `Memory` —— 按需上下文:锚点类别(ADR-0003)+ MCP 工具按 run/project 上下文授权的不变式。
diff --git a/spec/Spec/System/AgentRole.lean b/spec/Spec/System/Agent/AgentRole.lean
similarity index 100%
rename from spec/Spec/System/AgentRole.lean
rename to spec/Spec/System/Agent/AgentRole.lean
diff --git a/spec/Spec/System/AgentSurface.lean b/spec/Spec/System/Agent/AgentSurface.lean
similarity index 98%
rename from spec/Spec/System/AgentSurface.lean
rename to spec/Spec/System/Agent/AgentSurface.lean
index 64c215f..7d21568 100644
--- a/spec/Spec/System/AgentSurface.lean
+++ b/spec/Spec/System/Agent/AgentSurface.lean
@@ -1,5 +1,5 @@
 import Spec.Prelude
-import Spec.System.Run
+import Spec.System.Agent.Run
 
 /-!
 # AgentSurface —— Agent 执行面边界(ADR-0018)
diff --git a/spec/Spec/System/Memory.lean b/spec/Spec/System/Agent/Memory.lean
similarity index 100%
rename from spec/Spec/System/Memory.lean
rename to spec/Spec/System/Agent/Memory.lean
diff --git a/spec/Spec/System/Run.lean b/spec/Spec/System/Agent/Run.lean
similarity index 100%
rename from spec/Spec/System/Run.lean
rename to spec/Spec/System/Agent/Run.lean
diff --git a/spec/Spec/System/Lock.lean b/spec/Spec/System/Lock.lean
index 94a0e22..6ddd4cd 100644
--- a/spec/Spec/System/Lock.lean
+++ b/spec/Spec/System/Lock.lean
@@ -1,5 +1,5 @@
 import Spec.Prelude
-import Spec.System.Run
+import Spec.System.Agent.Run
 
 /-!
 # Lock —— 项目锁与排他不变式
diff --git a/spec/Spec/System/Organization.lean b/spec/Spec/System/Organization.lean
index b7d583a..8f29e8d 100644
--- a/spec/Spec/System/Organization.lean
+++ b/spec/Spec/System/Organization.lean
@@ -6,7 +6,7 @@ import Spec.Prelude
 组织就是租户。project/team 必须归属且仅归属一个 org;team→project grant 必须同 org。
 组织实体见 `Hierarchy.Organization`;用户见 `Spec.System.User`;平台控制面见
 `PlatformAdministration`(ADR-0023)。凭据信封见 ADR-0024。Agent 角色配置见
-`Spec.System.AgentRole`。
+`Spec.System.Agent.AgentRole`。
 -/
 
 namespace Spec.System