forked from bai/curriculum-project-hub
hongjr03
18aac1ff16
ADR-0001/0003/0004 已 PINNED 但 spec/System 未落,补三模块: - ProjectGroup: project↔飞书群 1:1 绑定 + 单射良构(ADR-0001);群失效态 OPEN - Memory: 锚点类别 + MCP 读上下文按 run/project 授权不变式(ADR-0003) - PermissionGrant: grant(resource×principal×role)+settings 六旋钮(ADR-0004); role-capability×settings-policy 组合规则 OPEN - Prelude: 新增 ChatId 载体 - ADR-0017: AgentSession provider/model 绑定,切 model 即新 session, 跨 session 连续性由 ADR-0003 记忆/锚点重建;agent 层 provider 无关, @Claude 仅为触发品牌。RunId/SessionId doc 去 provider 暗示。 lake build 28/28 绿。
27 lines
1.2 KiB
Lean4
27 lines
1.2 KiB
Lean4
import Spec.System.ProjectGroup
|
||
import Spec.System.Run
|
||
import Spec.System.Lock
|
||
import Spec.System.Memory
|
||
import Spec.System.Permission
|
||
import Spec.System.PermissionGrant
|
||
import Spec.System.Audit
|
||
|
||
/-!
|
||
# System —— Hub 平台层契约
|
||
|
||
协作与执行的平台:项目、飞书群、AgentRun、锁、权限、审计、按需上下文。likec4
|
||
(`docs/architecture/likec4/`)已画出这一层的**结构**;本层只补 likec4 画不出的
|
||
**语义分歧点**:
|
||
|
||
- `ProjectGroup` —— project↔飞书群 1:1 长生命周期绑定(ADR-0001);群是协作空间,不持锁。
|
||
- `Run` —— AgentRun 状态与终止判定(状态集合完整性 OPEN)。
|
||
- `Lock` —— 锁 owner=run(ADR-0002),及"持锁者必为非终止 run"的核心不变式。
|
||
- `Memory` —— 按需上下文:锚点类别(ADR-0003)+ MCP 工具按 run/project 上下文授权的不变式。
|
||
- `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。
|
||
-/
|