forked from bai/curriculum-project-hub
refactor(spec): clean prose patterns across all modules
Remove filler/redundant patterns: 钉死/钉, 本模块, likec4 画不出/画得出, 臆造, 散文, 分歧点测试, 纯 plumbing, 恰好, 留白, 宪法第N条, 刻意. No code definitions changed, only doc comments.
This commit is contained in:
@@ -4,19 +4,14 @@ 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)。逃逸即越权,拒绝。
|
||||
|
||||
钉死的不变式:agent 在一次 run 内发起的文件操作,其路径必须落在该 run 所属 project
|
||||
的工作区目录内(ADR-0007:工程文件是目录树;此 ADR 固定"agent 操作落在该树内")。
|
||||
逃逸即越权,拒绝。与 `Lock`(ADR-0002)正交:Lock 限定**并发**(谁在改),Surface
|
||||
限定**波及面**(能改到哪)。二者都按 run × project 作用域。
|
||||
与 `Lock`(ADR-0002)正交:Lock 限定并发(谁在改),Surface 限定波及面(能改到哪)。
|
||||
二者都按 run × project 作用域。
|
||||
|
||||
shell 面的边界(命令的文件效果同样不得逃逸工作区)是同一不变式的推论,但**机制**
|
||||
——路径校验工具包装、OS 级沙箱(bubblewrap/容器)、SDK 权限钩子,或其组合——`OPEN`
|
||||
(ADR-0018)。契约钉死不变式,不钉死机制。
|
||||
shell 面的边界(命令的文件效果同样不得逃逸工作区)是同一不变式的推论。机制
|
||||
——路径校验、OS 级沙箱、SDK 权限钩子,或其组合——`OPEN`(ADR-0018)。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
@@ -24,17 +19,18 @@ namespace Spec.System
|
||||
variable (I : Identifiers) (Path : Type)
|
||||
|
||||
/-- Agent 在一次 run 内发起的文件操作(`PINNED` 关系, ADR-0018)。由某 run 发起、
|
||||
指向某路径;是否越权由下方 `Authorized` 钉死。 -/
|
||||
指向某路径;是否越权由下方 `Authorized` 约束。 -/
|
||||
structure AgentFileOp where
|
||||
/-- 发起操作的 run(授权上下文主体, ADR-0018;与 `Lock` 同作用域 run × project)。 -/
|
||||
run : I.RunId
|
||||
/-- 操作目标路径(`PINNED` 字段, ADR-0018)。 -/
|
||||
/-- 操作目标路径(`PINNED`, ADR-0018)。 -/
|
||||
path : Path
|
||||
|
||||
|
||||
/-- 工作区边界良构:run 的文件操作路径必须落在该 run 所属 project 的工作区目录内
|
||||
(`PINNED` 平台核心安全不变式, ADR-0018)。`runWorkspace` 与 `pathWithin` 均由平台提供
|
||||
(表示 `OPEN`——路径如何表示、"在内"如何判定是纯 plumbing,非本层分歧点);本谓词只
|
||||
钉死"操作路径必须以 run 的工作区为根",杜绝 agent 越权读写宿主任意文件。 -/
|
||||
(`PINNED` 安全不变式, ADR-0018)。`runWorkspace` 与 `pathWithin` 由平台提供
|
||||
(表示 `OPEN`);本谓词约束"操作路径必须以 run 的工作区为根",杜绝 agent 越权读写
|
||||
宿主任意文件。 -/
|
||||
def AgentFileOp.Authorized
|
||||
(op : AgentFileOp I Path)
|
||||
(runWorkspace : I.RunId → Option Path)
|
||||
|
||||
@@ -3,13 +3,13 @@ import Spec.Prelude
|
||||
/-!
|
||||
# Memory —— 按需上下文:锚点与项目记忆(ADR-0003)
|
||||
|
||||
ADR-0003:Hub **只存锚点与项目记忆**,不存全量飞书消息历史;Claude 需要更多上下文时经
|
||||
飞书 API 按需读取。本模块刻画所存锚点的**类别**(ADR 列定,枚举完整性 OPEN——ADR 是
|
||||
"例如"式列举,新增类别不违反契约),并钉死一条 likec4 画不出的安全不变式:**MCP 工具
|
||||
按 run/project 上下文授权,Claude 不得传任意 chat id**(ADR-0003 Consequences 末条)。
|
||||
ADR-0003:Hub 只存锚点与项目记忆,不存全量飞书消息历史;Claude 需要更多上下文时经
|
||||
飞书 API 按需读取。这里刻画所存锚点的类别(ADR 列定,枚举完整性 OPEN),并约束
|
||||
一条安全不变式:MCP 工具按 run/project 上下文授权,Claude 不得传任意 chat id
|
||||
(ADR-0003 Consequences 末条)。
|
||||
|
||||
"chat id 与 project 绑定"这一锚点类别由 `ProjectGroup.GroupBinding`(ADR-0001)权威承载,
|
||||
本模块不重复声明,只覆盖其余飞书侧指针(触发消息、状态卡片、回复、线程)。
|
||||
这里只覆盖其余飞书侧指针(触发消息、状态卡片、回复、线程)。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
@@ -17,9 +17,8 @@ namespace Spec.System
|
||||
variable (I : Identifiers)
|
||||
variable (MessageId CardId : Type)
|
||||
|
||||
/-- 上下文锚点(`PINNED` 类别, ADR-0003 列定;**枚举完整性 `OPEN`**——ADR 是"例如"式
|
||||
列举,实现若需新类别须 surface,不得默认本枚举已穷尽)。承载 Hub 保留的飞书侧最小指针,
|
||||
而非消息正文。 -/
|
||||
/-- 上下文锚点(`PINNED` 类别, ADR-0003;枚举完整性 `OPEN`——ADR 是"例如"式列举,
|
||||
实现若需新类别须 surface)。承载 Hub 保留的飞书侧最小指针,而非消息正文。 -/
|
||||
inductive Anchor where
|
||||
/-- 触发某次 run 的消息(`PINNED` 类别, ADR-0003 "trigger message id")。 -/
|
||||
| triggerMessage : MessageId → Anchor
|
||||
@@ -35,13 +34,11 @@ MCP tools to read … through Feishu APIs")。 -/
|
||||
structure McpReadRequest where
|
||||
/-- 发起请求的 run(授权上下文主体, ADR-0003)。 -/
|
||||
run : I.RunId
|
||||
/-- 请求读取的 chat(是否允许越界由下方 `Authorized` 钉死:不允许)。 -/
|
||||
/-- 请求读取的 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 越权读取。 -/
|
||||
ADR-0003)。"chat 必须匹配 run 的 project 绑定",杜绝 Claude 传任意 chat id。 -/
|
||||
def McpReadRequest.Authorized
|
||||
(req : McpReadRequest I)
|
||||
(runProject : I.RunId → Option I.ProjectId)
|
||||
|
||||
@@ -2,15 +2,15 @@
|
||||
# Run —— AgentRun 状态机
|
||||
|
||||
一次 `@bot` 创建一个 `AgentRun`(ADR-0001),它在终止时释放项目锁(ADR-0002)。
|
||||
合法转移关系在任何 ADR / likec4 散文里都未定下,故本模块只刻画**状态**与**终止
|
||||
判定**(后者是 Lock 排他不变式的依赖),不臆造转移边。
|
||||
转移关系在任何 ADR 里都未定,这里只刻画状态与终止判定(后者是 Lock 排他不变式的
|
||||
依赖),不定义转移边。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
/-- AgentRun 运行状态(状态名 `PINNED`, ADR-0001..0003, ADR-0022 + likec4;
|
||||
**完整性 `OPEN`**——散文从未声明"状态恰好这些";实现若需新状态(如 pending)须
|
||||
surface,不得默认本枚举已穷尽)。终止态见 `RunState.Terminal`。 -/
|
||||
/-- AgentRun 运行状态(状态名 `PINNED`, ADR-0001..0003, ADR-0022;完整性 `OPEN`
|
||||
——ADR 从未声明"状态就是这些";实现若需新状态(如 pending)须 surface)。终止态
|
||||
见 `RunState.Terminal`。 -/
|
||||
inductive RunState where
|
||||
| active
|
||||
| waitingForUser
|
||||
|
||||
@@ -1,21 +1,18 @@
|
||||
import Spec.Prelude
|
||||
|
||||
/-!
|
||||
# Audit —— Project/Run 审计日志(有意从简)
|
||||
# Audit —— Project/Run 审计日志
|
||||
|
||||
likec4 把 `AuditLog` 列为实体(`AgentRun -> AuditLog 'records lifecycle events'`),
|
||||
但**审计记录里装什么**(事件 schema、保留策略、可查询维度)在任何 ADR / 散文里都
|
||||
未决策,且大多是 plumbing——按分歧点测试不入契约。故本模块刻意几乎为空:只固定
|
||||
"审计以 run 为主体记录其生命周期事件"这一条已决策关系,其余 `OPEN`(留白本身是
|
||||
契约的一部分:承诺此处尚无答案、勿填)。
|
||||
审计记录里装什么(事件 schema、保留策略、可查询维度)在任何 ADR 里都未决策,
|
||||
且大多是实现细节。这里只固定"审计以 run 为主体记录其生命周期事件"这一条已决策
|
||||
关系,其余 `OPEN`。ADR-0023 的 Platform Audit 是另一个控制面,见
|
||||
`Spec.System.PlatformAdministration`,不复用本结构。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
/-- 审计条目的最小骨架(关系 `PINNED` / 内容 `OPEN`, likec4)。只承诺"一条审计记录
|
||||
关联到某个 run";事件类型、时间、actor、详情等字段 `OPEN`,待真实分歧点出现时由
|
||||
对应 ADR 落定。ADR-0023 的 Platform Audit 是另一个 fail-closed 控制面,见
|
||||
`Spec.System.PlatformAdministration`,不复用本结构。 -/
|
||||
关联到某个 run";事件类型、时间、actor、详情等字段 `OPEN`。 -/
|
||||
structure AuditEntry (I : Identifiers) where
|
||||
/-- 该审计条目所属的 run(`PINNED` 关系, likec4)。 -/
|
||||
run : I.RunId
|
||||
|
||||
@@ -4,8 +4,8 @@ import Spec.Prelude
|
||||
# Capacity —— SaaS capacity admission and abuse controls (ADR-0022)
|
||||
|
||||
初始生产服务共享有限的单机资源,但不能让一个 Organization 垄断容量或让无界输入拖垮
|
||||
其他租户。ADR-0022 钉死分层限制、持久 admission、显式背压和紧急制动的领域语义;
|
||||
具体数值必须由生产式容量测试校准,因此保持 `OPEN`,不得把未经验证的数字冒充契约。
|
||||
其他租户。ADR-0022 定义分层限制、持久 admission、显式背压和紧急制动;具体数值由
|
||||
生产式容量测试校准,保持 `OPEN`。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
@@ -4,32 +4,29 @@ import Spec.System.Agent.Run
|
||||
/-!
|
||||
# Lock —— 项目锁与排他不变式
|
||||
|
||||
ADR-0002 的核心:防止并发 Claude 同改一个项目,锁的 **owner 是当前 `AgentRun`**
|
||||
(不是 teacher / chat / session)。本模块把这条决策编码进类型,并钉死那条
|
||||
likec4 画不出的语义不变式——**持锁者必为非终止 run**。
|
||||
ADR-0002:防止并发 agent 同改一个项目,锁的 owner 是当前 `AgentRun`(不是
|
||||
teacher / chat / session)。持锁者必为非终止 run。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
variable (I : Identifiers)
|
||||
|
||||
/-- 项目级锁(`PINNED`, ADR-0002)。`owner : RunId`(非 SessionId/Principal)从类型
|
||||
上编码"lock owner = run_id":锁不可能被 session / teacher 持有。 -/
|
||||
/-- 项目级锁(`PINNED`, ADR-0002)。`owner : RunId`从类型上编码"lock owner = run_id":
|
||||
锁不可能被 session / teacher 持有。 -/
|
||||
structure ProjectAgentLock where
|
||||
/-- 作用域:项目级(`PINNED`, ADR-0002 `scope = project_id`)。 -/
|
||||
/-- 作用域:项目级(`PINNED`, ADR-0002)。 -/
|
||||
scope : I.ProjectId
|
||||
/-- 持有者:一个 run(`PINNED`, ADR-0002 `owner = run_id`)。 -/
|
||||
/-- 持有者:一个 run(`PINNED`, ADR-0002)。 -/
|
||||
owner : I.RunId
|
||||
|
||||
/-- 锁表:每项目当前持锁 run(`PINNED` 排他性, ADR-0002)。`ProjectId → Option RunId`
|
||||
的结构**本身**即排他——不可能为同一项目登记两个并发 owner。 -/
|
||||
的结构本身即排他——不可能为同一项目登记两个并发 owner。 -/
|
||||
def LockTable := I.ProjectId → Option I.RunId
|
||||
|
||||
/-- 锁表良构:**持锁者必为非终止 run**(`PINNED` 平台核心不变式, ADR-0002)。
|
||||
/-- 锁表良构:持锁者必为非终止 run(`PINNED`, ADR-0002)。
|
||||
|
||||
"锁在 run 终止时释放"的逻辑等价物:若 `p` 的锁被 `r` 持有,则 `r` 不在终止态。这条
|
||||
把 Lock 与 Run 耦合起来——likec4 能画"run owns lock while running",画不出"终止即
|
||||
必须释放"这个约束;它正是契约相对结构图的增量。 -/
|
||||
若 `p` 的锁被 `r` 持有,则 `r` 不在终止态。锁在 run 终止时释放。 -/
|
||||
def LockTable.WellFormed
|
||||
(lt : LockTable I) (statusOf : I.RunId → RunState) : Prop :=
|
||||
∀ p r, lt p = some r → ¬ (statusOf r).Terminal
|
||||
|
||||
@@ -35,10 +35,9 @@ structure TeamProjectGrantScope where
|
||||
project : I.ProjectId
|
||||
/-- 获得授权的 team principal(`PINNED`, ADR-0020)。 -/
|
||||
team : I.TeamId
|
||||
|
||||
/-- Team-project grant 是良构的 iff project 与 team 解析到同一 organization
|
||||
(`PINNED`, ADR-0020)。`projectOrg`/`teamOrg` 由平台提供(表示 `OPEN`);本谓词钉死
|
||||
跨 org team grant 必须被拒绝。 -/
|
||||
(`PINNED`, ADR-0020)。`projectOrg`/`teamOrg` 由平台提供(表示 `OPEN`);跨 org
|
||||
team grant 必须被拒绝。 -/
|
||||
def TeamProjectGrantScope.WellScoped
|
||||
(grant : TeamProjectGrantScope I)
|
||||
(projectOrg : I.ProjectId → Option I.OrganizationId)
|
||||
@@ -71,7 +70,7 @@ inductive OrganizationConnectionStatus where
|
||||
|
||||
/-- Organization secret version 的信封绑定上下文(`PINNED`, ADR-0024):认证附加数据必须
|
||||
同时绑定 organization、connection、secret version 与 purpose,因此密文不能跨行、跨 org、
|
||||
跨 connection 或跨用途替换。各标识符的数据库表示属于 plumbing,这里保持 opaque。 -/
|
||||
跨 connection 或跨用途替换。各标识符的数据库表示为实现细节,这里保持 opaque。 -/
|
||||
structure OrganizationSecretBinding
|
||||
(OrganizationId ConnectionId SecretVersionId Purpose : Type) where
|
||||
/-- secret 所属 organization(`PINNED`, ADR-0024)。 -/
|
||||
|
||||
@@ -5,8 +5,7 @@ import Spec.Prelude
|
||||
|
||||
ADR-0004:权限走"飞书云文档式"——grant(`resource + principal + role`)与 settings
|
||||
分离;role 取自封闭的 `read / edit / manage`,且 **read ⊂ edit ⊂ manage** 累积赋能;
|
||||
强制释放锁是 **admin-only**,在 role 体系之外。本模块把这套结构与"高 role 含低
|
||||
role 全部能力"的单调性钉死。
|
||||
强制释放锁是 **admin-only**,在 role 体系之外。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
@@ -4,16 +4,14 @@ import Spec.System.Permission
|
||||
/-!
|
||||
# PermissionGrant —— 授权与设置(ADR-0004)
|
||||
|
||||
ADR-0004 的"飞书云文档式"权限:**grant**(`resource × principal × role`)与 **settings**
|
||||
(各 policy 旋钮)分离;role 决定"谁能"(能力,见 `Permission`),settings 决定"此资源
|
||||
是否开某类操作"(策略)。本模块把 grant/settings 的结构钉死——`Permission` 已落 role 能
|
||||
力格,本模块补"授权如何挂到资源/主体上"。
|
||||
ADR-0004 的"飞书云文档式"权限:grant(`resource × principal × role`)与 settings
|
||||
(各 policy 旋钮)分离;role 决定能力(见 `Permission`),settings 决定"此资源是否
|
||||
开某类操作"。
|
||||
|
||||
principal 子类型学(user/chat/department/…)与各 policy 值域均为 `OPEN`(ADR 未定,非本
|
||||
层分歧点)。**role-capability 与 settings-policy 如何组合成最终授权决策**亦 `OPEN`——
|
||||
ADR-0004 把二者列为分离的闸,但未明文规定组合规则(AND?settings 能否超出 role?),实现
|
||||
须 surface,不得默认。ADR-0020 另行钉死 TEAM principal 授权 PROJECT resource 时必须
|
||||
同 organization;该 tenant well-scopedness 见 `Spec.System.Organization`。
|
||||
principal 子类型学(user/chat/department/…)与各 policy 值域 `OPEN`。role-capability
|
||||
与 settings-policy 如何组合成最终授权决策亦 `OPEN`——ADR-0004 把二者列为分离的闸,
|
||||
但未明文规定组合规则。ADR-0020 约束 TEAM principal 授权 PROJECT resource 时必须同
|
||||
organization,见 `Spec.System.Organization`。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
@@ -45,9 +43,8 @@ structure PermissionGrant where
|
||||
role : Role
|
||||
|
||||
/-- 资源策略设置(`PINNED` 结构 + 六旋钮, ADR-0004 `PermissionSettings`):与 grant 分离,
|
||||
控制"此资源是否开某类操作"。六旋钮由 ADR 逐字列名;各旋钮值域 `OPEN`(ADR 未定,非本层
|
||||
分歧点)。共享同一 opaque `Policy` 类型:契约只钉死"旋钮存在且相互独立",不钉死"各旋钮
|
||||
值域互异"——值域是实现/后续 ADR 的事。 -/
|
||||
控制"此资源是否开某类操作"。六旋钮由 ADR 逐字列名;各旋钮值域 `OPEN`(ADR 未定)。
|
||||
共享同一 opaque `Policy` 类型:契约只约束"旋钮存在且相互独立";值域是实现/后续 ADR 的事。 -/
|
||||
structure PermissionSettings where
|
||||
/-- 设置所属资源(`PINNED`, ADR-0004)。 -/
|
||||
resource : Resource I ArtifactId
|
||||
|
||||
@@ -8,8 +8,8 @@ import Spec.Prelude
|
||||
单一平级管理员角色、绑定身份的 invitation、可撤销服务端 session、mutation 与平台审计
|
||||
同成同败、最后管理员保护,以及无常驻账号的双因子离线恢复。
|
||||
|
||||
本模块只钉死这些会导致安全边界分歧的语义。cookie 属性、token hash、具体 TTL、审计
|
||||
字段表示/保留期、recovery key 介质和 CLI/SQL 机制仍为 `OPEN`,由对应实现决策承载。
|
||||
这些安全边界语义见下。cookie 属性、token hash、具体 TTL、审计
|
||||
字段表示/保留期、recovery key 介质和 CLI/SQL 机制 `OPEN`。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
@@ -3,26 +3,23 @@ import Spec.Prelude
|
||||
/-!
|
||||
# ProjectGroup —— 飞书项目群作为协作空间(ADR-0001)
|
||||
|
||||
ADR-0001 的核心:一个 project 对应一个**长生命周期**飞书项目群;群是协作空间,**不是锁
|
||||
owner**(锁归 `AgentRun`,见 `Lock` / ADR-0002),不是临时处理 session。群可在无 Claude
|
||||
处理时保持开启;教师离群/静音与项目权限、与 Claude 生命周期相互独立。本模块钉死
|
||||
project↔group 的**active**一对一绑定——likec4 画得出"project has group",画不出"恰好一个、
|
||||
且群不持锁"。
|
||||
一个 project 对应一个长生命周期飞书项目群;群是协作空间,不持锁(锁归 `AgentRun`,
|
||||
见 `Lock` / ADR-0002)。群可在无 agent 处理时保持开启;教师离群/静音与项目权限、
|
||||
与 agent 生命周期相互独立。
|
||||
|
||||
**绑定历史(`PINNED`, ADR-0021):** active binding 严格 1:1;实现可以保留 archived
|
||||
historical binding rows 供审计/纠错,但 `GroupBinding` 谓词只刻画当前 active 快照。
|
||||
群解散/不可达的自动化处理仍为 `OPEN`;pilot 纠错由 org admin 显式归档绑定。
|
||||
**绑定历史(`PINNED`, ADR-0021):** active binding 严格 1:1;实现可保留 archived
|
||||
historical binding rows 供审计,但 `GroupBinding` 谓词只刻画当前 active 快照。
|
||||
群解散/不可达的自动化处理 `OPEN`;pilot 纠错由 org admin 显式归档绑定。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
variable (I : Identifiers)
|
||||
|
||||
/-- 飞书项目群(`PINNED` 长生命周期协作空间, ADR-0001)。承载 project 与飞书 chat 的绑定;
|
||||
**不是锁 owner**(锁归 `AgentRun`,见 `Lock`);不是临时 session。 -/
|
||||
/-- 飞书项目群(`PINNED` 长生命周期协作空间, ADR-0001)。承载 project 与飞书 chat 的
|
||||
绑定;不持锁(锁归 `AgentRun`,见 `Lock`)。 -/
|
||||
structure ProjectGroup where
|
||||
/-- 群对应的飞书 chat(`PINNED` 关系, ADR-0001 "one project has one Feishu project
|
||||
group";chat 标识见 `Identifiers.ChatId`)。 -/
|
||||
/-- 群对应的飞书 chat(`PINNED` 关系, ADR-0001;chat 标识见 `Identifiers.ChatId`)。 -/
|
||||
chat : I.ChatId
|
||||
|
||||
/-- 项目↔active 群绑定表(`PINNED` 每项目至多一个 active 群, ADR-0001/0021)。
|
||||
@@ -30,9 +27,9 @@ structure ProjectGroup where
|
||||
自带);良构补另一半——单射。 -/
|
||||
def GroupBinding := I.ProjectId → Option I.ChatId
|
||||
|
||||
/-- Active 绑定良构:**单射**——不同 project 不绑同一 active chat(`PINNED` 1:1 的另一半,
|
||||
ADR-0001/0021)。"每 project 至多一个群"由 `Option` 结构自带;这条钉死"每群至多属于一个
|
||||
project"。archived historical bindings 不在本快照不变式内。 -/
|
||||
/-- Active 绑定良构:单射——不同 project 不绑同一 active chat(`PINNED`, ADR-0001/0021)。
|
||||
"每 project 至多一个群"由 `Option` 结构自带;这条约束"每群至多属于一个 project"。
|
||||
archived historical bindings 不在本快照不变式内。 -/
|
||||
def GroupBinding.WellFormed (b : GroupBinding I) : Prop :=
|
||||
∀ p₁ p₂ c, b p₁ = some c → b p₂ = some c → p₁ = p₂
|
||||
|
||||
|
||||
@@ -3,12 +3,11 @@ import Spec.Prelude
|
||||
/-!
|
||||
# ProjectWorkspace —— project explorer 与飞书建项入口(ADR-0021)
|
||||
|
||||
ADR-0021 把 org 后台里的"文件管理器式"项目管理收口为透明 folder + project:
|
||||
folder 只负责导航、排序、层级与用量聚合,当前不是权限资源。project 仍是授权边界。
|
||||
org 后台里的"文件管理器式"项目管理:folder 只负责导航、排序、层级与用量聚合,当前
|
||||
不是权限资源。project 仍是授权边界。
|
||||
|
||||
本模块只钉死会影响实现分歧的不变量:folder/project 同 org、folder 不参与权限、普通成员
|
||||
从飞书群创建 project 必须受 org policy 控制。folder visibility/team policy/继承授权仍为
|
||||
未来扩展,不得在当前实现中半隐式加入。
|
||||
不变量:folder/project 同 org、folder 不参与权限、普通成员从飞书群创建 project 受
|
||||
org policy 控制。folder visibility/team policy/继承授权 `OPEN`。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
@@ -39,7 +38,7 @@ def ProjectFolderPlacement.WellScoped
|
||||
∃ o, projectOrg placement.project = some o ∧ folderOrg placement.folder = some o
|
||||
|
||||
/-- Folder 当前透明(`PINNED`, ADR-0021):folder 不是权限资源,不持有 grants,移动 project
|
||||
不改变 project 自身授权。未来 folder policy 若出现,必须新增显式语义而不是复用本谓词。 -/
|
||||
不改变 project 自身授权。未来 folder policy 若出现,须新增显式语义。 -/
|
||||
structure FolderTransparent where
|
||||
/-- 透明性命题本身;字段存在是为了让 contract 明确可引用(`PINNED`, ADR-0021)。 -/
|
||||
current : True
|
||||
|
||||
@@ -5,7 +5,7 @@ import Spec.Prelude
|
||||
|
||||
用户实体见 `Hierarchy.User`;外部连接见 `Spec.System.Connections`。
|
||||
|
||||
用户创建当前只钉管理员直接创建;飞书自助注册→管理员审批未钉死(`OPEN`)。
|
||||
用户创建当前只定义管理员直接创建;飞书自助注册→管理员审批 `OPEN`。
|
||||
-/
|
||||
|
||||
namespace Spec.System
|
||||
|
||||
Reference in New Issue
Block a user