spec: 钉死 agent 执行面边界(ADR-0018)

ADR-0001/0002/0004 覆盖协作治理到 triggerAgent,但触发后 agent 在执行层
能干什么——读哪些文件、跑什么命令——无 ADR / spec 覆盖。ADR-0017 落地时
采用 bypassPermissions + 全量内置工具,agent 文件/shell 面对宿主无界;
workspace.ts 的 confine() 沙箱意图存在但被 ADR-0017 静默覆盖成死代码。

新增 ADR-0018 + Spec.System.AgentSurface 模块补这一层:
- AgentFileOp(run × path)+ Authorized 谓词(路径必须落在 run 工作区内)
- 与 Lock 正交:Lock 限定并发,Surface 限定波及面,都按 run × project 作用域
- 机制 OPEN(工具包装 / OS 沙箱 / SDK 钩子),契约只钉不变式
- ADR-0017 的 bypassPermissions + workspace.ts 死代码标为偏离契约,对齐为 follow-up

spec/Spec/System.lean

@@ -2,10 +2,10 @@ import Spec.System.ProjectGroup
 import Spec.System.Run
 import Spec.System.Lock
 import Spec.System.Memory
+import Spec.System.AgentSurface
 import Spec.System.Permission
 import Spec.System.PermissionGrant
 import Spec.System.Audit
-
 /-!
 # System —— Hub 平台层契约
 
@@ -17,10 +17,12 @@ import Spec.System.Audit
 - `Run` —— AgentRun 状态与终止判定(状态集合完整性 OPEN)。
 - `Lock` —— 锁 owner=run(ADR-0002),及"持锁者必为非终止 run"的核心不变式。
 - `Memory` —— 按需上下文:锚点类别(ADR-0003)+ MCP 工具按 run/project 上下文授权的不变式。
+- `AgentSurface` —— agent 执行面被 run 的工作区所界定(ADR-0018);与 Lock 正交——
+  Lock 限定并发,Surface 限定波及面。机制 OPEN。
 - `Permission` —— read⊂edit⊂manage 角色格、能力推导、单调性;force-release 在格外。
 - `PermissionGrant` —— grant(resource×principal×role)与 settings(六 policy 旋钮)结构
   (ADR-0004);role-capability 与 settings-policy 的组合规则 OPEN。
 - `Audit` —— 有意从简(内容多为 plumbing,OPEN)。
 
-标识符见 `Spec.Prelude`。决策出处:ADR-0001..0004。
+标识符见 `Spec.Prelude`。决策出处:ADR-0001..0004, 0018。
 -/

spec/Spec/System/AgentSurface.lean

@@ -0,0 +1,44 @@
+import Spec.Prelude
+import Spec.System.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