forked from EduCraft/curriculum-project-hub
sjfhsjfh
3ebe4b754d
Remove filler/redundant patterns: 钉死/钉, 本模块, likec4 画不出/画得出, 臆造, 散文, 分歧点测试, 纯 plumbing, 恰好, 留白, 宪法第N条, 刻意. No code definitions changed, only doc comments.
41 lines
1.6 KiB
Lean4
41 lines
1.6 KiB
Lean4
import Spec.Prelude
|
||
import Spec.System.Agent.Run
|
||
|
||
/-!
|
||
# AgentSurface —— Agent 执行面边界(ADR-0018)
|
||
|
||
Agent 在一次 run 内发起的文件操作,其路径必须落在该 run 所属 project 的工作区目录内
|
||
(ADR-0007)。逃逸即越权,拒绝。
|
||
|
||
与 `Lock`(ADR-0002)正交:Lock 限定并发(谁在改),Surface 限定波及面(能改到哪)。
|
||
二者都按 run × project 作用域。
|
||
|
||
shell 面的边界(命令的文件效果同样不得逃逸工作区)是同一不变式的推论。机制
|
||
——路径校验、OS 级沙箱、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`);本谓词约束"操作路径必须以 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
|