From 18aac1ff1630b9790d9c57f64509e19ac9ede262 Mon Sep 17 00:00:00 2001 From: Hong Jiarong Date: Mon, 6 Jul 2026 22:30:05 +0800 Subject: [PATCH] =?UTF-8?q?feat(spec):=20System=20=E5=B1=82=E8=A1=A5=20ADR?= =?UTF-8?q?-0001/0003/0004=20=E7=BC=BA=E5=8F=A3=20+=20ADR-0017=20provider-?= =?UTF-8?q?bound=20session?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 绿。 --- .../0017-agent-session-is-provider-bound.md | 47 +++++++++++++ spec/Spec/Prelude.lean | 13 +++- spec/Spec/System.lean | 9 ++- spec/Spec/System/Memory.lean | 51 ++++++++++++++ spec/Spec/System/PermissionGrant.lean | 69 +++++++++++++++++++ spec/Spec/System/ProjectGroup.lean | 40 +++++++++++ 6 files changed, 225 insertions(+), 4 deletions(-) create mode 100644 docs/adr/0017-agent-session-is-provider-bound.md create mode 100644 spec/Spec/System/Memory.lean create mode 100644 spec/Spec/System/PermissionGrant.lean create mode 100644 spec/Spec/System/ProjectGroup.lean diff --git a/docs/adr/0017-agent-session-is-provider-bound.md b/docs/adr/0017-agent-session-is-provider-bound.md new file mode 100644 index 0000000..88ed160 --- /dev/null +++ b/docs/adr/0017-agent-session-is-provider-bound.md @@ -0,0 +1,47 @@ +# ADR 0017: AgentSession Is Provider-Bound + +## Status + +Accepted. + +## Context + +ADR-0002 says a long-lived `AgentSession` can be reused by many runs, but never +addressed the provider/model dimension. The agent layer is provider-agnostic +(ADR-0001..0003 never required Claude specifically; the `@Claude` trigger name +is a product brand, not a provider commitment). In practice the Hub routes +model calls through an OpenAI-compatible client (e.g. OpenRouter), so a run may +target different models — and the motivation for multi-model is **role-based +routing**: drafting, reviewing, and triage suit different models. + +That raises the question ADR-0002 left open: when a teacher switches model +mid-project, does the `AgentSession` carry live context across the switch, or +is it bound to a single provider/model? + +## Decision + +An `AgentSession` is **provider/model-bound**. A model or provider switch +starts a new `AgentSession`. The `AgentSession` does not carry live context +across a switch. + +Cross-session continuity is not the session's job — it is carried by ADR-0003's +project memory and anchors, which the Hub reads on demand when seeding a new +run. This keeps B consistent with ADR-0003 ("the Hub avoids becoming a full +chat history store"): session continuity and history continuity are the same +mechanism, both via memory/anchors, never via a live cross-provider session. + +Per-run model selection (the run carries its model) is the switching point. + +## Consequences + +- Switching model mid-project = new session; the new run seeds from project + memory/anchors (ADR-0003), not the prior session's live context. +- The agent layer is provider-agnostic: the agent loop is ours; model calls go + through an OpenAI-compatible client. No hard dependency on a single-vendor + agent SDK. +- Role-based model routing (different run kinds default to different models) is + a product/admin configuration concern, not a spec invariant. +- "AgentSession reused by many runs" (ADR-0002) holds *within* one + provider/model; it does not span a switch. +- The `@Claude` trigger name remains the product mention brand regardless of the + backing model. diff --git a/spec/Spec/Prelude.lean b/spec/Spec/Prelude.lean index df99553..c21d688 100644 --- a/spec/Spec/Prelude.lean +++ b/spec/Spec/Prelude.lean @@ -1,7 +1,7 @@ /-! # Prelude —— System 层共享标识符 -平台层反复引用一组标识符(项目、run、session、principal)。其内部表示从未被决策 +平台层反复引用一组标识符(项目、run、session、principal、chat)。其内部表示从未被决策 (UUID / 复合键、principal 子类型学),也非分歧点,故收口成 opaque 载体 `Identifiers`,System 各模块在其上参数化——契约谈得了"锁 owner 是哪个 run"这类 **关系**,却不对标识符表示作承诺。 @@ -13,12 +13,19 @@ namespace Spec.System structure Identifiers where /-- 课程项目标识(`OPEN` 表示;聚合根,likec4 `Project`)。 -/ ProjectId : Type - /-- 一次 Claude 任务的标识(`OPEN` 表示;锁的 owner、审计主体,`AgentRun`)。 -/ + /-- 一次 agent 任务的标识(`OPEN` 表示;锁的 owner、审计主体,`AgentRun`。provider 无关, + ADR-0017;`@Claude` 仅为触发品牌,不承诺 provider)。 -/ RunId : Type - /-- 长生命周期 Claude 会话标识(`OPEN` 表示;跨多 run 复用,ADR-0002)。 -/ + /-- 长生命周期 agent 会话标识(`OPEN` 表示;**provider/model 绑定, ADR-0017**——一次 + session 不跨 provider/model;切 model 即新 session,跨 session 连续性由 ADR-0003 项目 + 记忆/锚点重建,不由 session 自带。同 provider/model 内可跨多 run 复用, ADR-0002)。 -/ SessionId : Type /-- 权限主体标识(`OPEN` 表示及其子类型学;ADR-0004 的 user/chat/department/… 子类型学未定且非本层分歧点,纯 plumbing,故只留 opaque 键)。 -/ Principal : Type + /-- 飞书项目群 chat 标识(`OPEN` 表示;ADR-0001 协作空间、ADR-0003 锚点引用、 + ADR-0004 `feishu_chat` principal 三处共用同一实体。独立成载体而非 `Principal` 子 + 类型——principal 子类型学 OPEN 见上,本层不预设"chat 是 principal 的哪种子型")。 -/ + ChatId : Type end Spec.System diff --git a/spec/Spec/System.lean b/spec/Spec/System.lean index d1ae702..f400a98 100644 --- a/spec/Spec/System.lean +++ b/spec/Spec/System.lean @@ -1,18 +1,25 @@ +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 +协作与执行的平台:项目、飞书群、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。 diff --git a/spec/Spec/System/Memory.lean b/spec/Spec/System/Memory.lean new file mode 100644 index 0000000..e550b09 --- /dev/null +++ b/spec/Spec/System/Memory.lean @@ -0,0 +1,51 @@ +import Spec.Prelude + +/-! +# Memory —— 按需上下文:锚点与项目记忆(ADR-0003) + +ADR-0003:Hub **只存锚点与项目记忆**,不存全量飞书消息历史;Claude 需要更多上下文时经 +飞书 API 按需读取。本模块刻画所存锚点的**类别**(ADR 列定,枚举完整性 OPEN——ADR 是 +"例如"式列举,新增类别不违反契约),并钉死一条 likec4 画不出的安全不变式:**MCP 工具 +按 run/project 上下文授权,Claude 不得传任意 chat id**(ADR-0003 Consequences 末条)。 + +"chat id 与 project 绑定"这一锚点类别由 `ProjectGroup.GroupBinding`(ADR-0001)权威承载, +本模块不重复声明,只覆盖其余飞书侧指针(触发消息、状态卡片、回复、线程)。 +-/ + +namespace Spec.System + +variable (I : Identifiers) +variable (MessageId CardId : Type) + +/-- 上下文锚点(`PINNED` 类别, ADR-0003 列定;**枚举完整性 `OPEN`**——ADR 是"例如"式 +列举,实现若需新类别须 surface,不得默认本枚举已穷尽)。承载 Hub 保留的飞书侧最小指针, +而非消息正文。 -/ +inductive Anchor where + /-- 触发某次 run 的消息(`PINNED` 类别, ADR-0003 "trigger message id")。 -/ + | triggerMessage : MessageId → Anchor + /-- 某 run 的状态卡片(`PINNED` 类别, ADR-0003 "run id and status card id")。 -/ + | statusCard : I.RunId → CardId → Anchor + /-- 回复锚点(`PINNED` 类别, ADR-0003 "reply anchors")。 -/ + | reply : MessageId → Anchor + /-- 线程锚点(`PINNED` 类别, ADR-0003 "thread anchors")。 -/ + | thread : MessageId → Anchor + +/-- MCP 读上下文请求:由某 run 发起、指向某 chat(`PINNED` 关系, ADR-0003 "Claude calls +MCP tools to read … through Feishu APIs")。 -/ +structure McpReadRequest where + /-- 发起请求的 run(授权上下文主体, ADR-0003)。 -/ + run : I.RunId + /-- 请求读取的 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 越权读取。 -/ +def McpReadRequest.Authorized + (req : McpReadRequest I) + (runProject : I.RunId → Option I.ProjectId) + (boundChat : I.ProjectId → Option I.ChatId) : Prop := + ∃ p, runProject req.run = some p ∧ boundChat p = some req.chat + +end Spec.System diff --git a/spec/Spec/System/PermissionGrant.lean b/spec/Spec/System/PermissionGrant.lean new file mode 100644 index 0000000..9869049 --- /dev/null +++ b/spec/Spec/System/PermissionGrant.lean @@ -0,0 +1,69 @@ +import Spec.Prelude +import Spec.System.Permission + +/-! +# PermissionGrant —— 授权与设置(ADR-0004) + +ADR-0004 的"飞书云文档式"权限:**grant**(`resource × principal × role`)与 **settings** +(各 policy 旋钮)分离;role 决定"谁能"(能力,见 `Permission`),settings 决定"此资源 +是否开某类操作"(策略)。本模块把 grant/settings 的结构钉死——`Permission` 已落 role 能 +力格,本模块补"授权如何挂到资源/主体上"。 + +principal 子类型学(user/chat/department/…)与各 policy 值域均为 `OPEN`(ADR 未定,非本 +层分歧点)。**role-capability 与 settings-policy 如何组合成最终授权决策**亦 `OPEN`—— +ADR-0004 把二者列为分离的闸,但未明文规定组合规则(AND?settings 能否超出 role?),实现 +须 surface,不得默认。 +-/ + +namespace Spec.System + +variable (I : Identifiers) +variable (ArtifactId Policy : Type) + +/-- 受权限调控的资源(`PINNED` 三类, ADR-0004 `resource_type: project | artifact | +project_group`);每类携带其 id,故 resource_id 由 resource_type 决定(结构无洞)。 -/ +inductive Resource where + /-- 课程项目(`PINNED` 类别, ADR-0004)。 -/ + | project : I.ProjectId → Resource + /-- 教研产物(`PINNED` 类别, ADR-0004;id 表示 `OPEN`,语义向 Courseware 半边对齐)。 -/ + | artifact : ArtifactId → Resource + /-- 飞书项目群(`PINNED` 类别, ADR-0004 `project_group`;chat 标识见 + `Identifiers.ChatId`,绑定见 `ProjectGroup`)。 -/ + | projectGroup : I.ChatId → Resource + +/-- 授权项(`PINNED` 结构, ADR-0004 `PermissionGrant`):把一个 role 授予一个 principal 对 +某个 resource。role 取自 `Permission.Role`(read/edit/manage 累积格)。principal 表示 +`OPEN`(子类型学未定,见 `Identifiers.Principal`)。 -/ +structure PermissionGrant where + /-- 被授权的资源(`PINNED`, ADR-0004 `resource_id`)。 -/ + resource : Resource I ArtifactId + /-- 被授权的主体(`PINNED` 字段/`OPEN` 表示, ADR-0004 `principal_id`;user/chat/ + department/user_group/app 子类型学未定)。 -/ + principal : I.Principal + /-- 授予的角色(`PINNED`, ADR-0004 `role`;read⊂edit⊂manage 见 `Permission.Role`)。 -/ + role : Role + +/-- 资源策略设置(`PINNED` 结构 + 六旋钮, ADR-0004 `PermissionSettings`):与 grant 分离, +控制"此资源是否开某类操作"。六旋钮由 ADR 逐字列名;各旋钮值域 `OPEN`(ADR 未定,非本层 +分歧点)。共享同一 opaque `Policy` 类型:契约只钉死"旋钮存在且相互独立",不钉死"各旋钮 +值域互异"——值域是实现/后续 ADR 的事。 -/ +structure PermissionSettings where + /-- 设置所属资源(`PINNED`, ADR-0004)。 -/ + resource : Resource I ArtifactId + /-- 对外分享策略(`PINNED` 旋钮名, ADR-0004 `external_share_policy`;值域 `OPEN`)。 -/ + externalShare : Policy + /-- 评论策略(`PINNED` 旋钮名, ADR-0004 `comment_policy`;值域 `OPEN`)。 -/ + comment : Policy + /-- 复制/下载策略(`PINNED` 旋钮名, ADR-0004 `copy_download_policy`;值域 `OPEN`)。 -/ + copyDownload : Policy + /-- 协作者管理策略(`PINNED` 旋钮名, ADR-0004 `collaborator_management_policy`; + 值域 `OPEN`)。 -/ + collaboratorMgmt : Policy + /-- agent 触发策略(`PINNED` 旋钮名, ADR-0004 `agent_trigger_policy`;值域 `OPEN`。与 + `agentCancel` 分立——"谁能触发"≠"谁能取消",ADR-0004 故意拆开)。 -/ + agentTrigger : Policy + /-- agent 取消策略(`PINNED` 旋钮名, ADR-0004 `agent_cancel_policy`;值域 `OPEN`。与 + `agentTrigger` 分立,见上)。 -/ + agentCancel : Policy + +end Spec.System diff --git a/spec/Spec/System/ProjectGroup.lean b/spec/Spec/System/ProjectGroup.lean new file mode 100644 index 0000000..5492285 --- /dev/null +++ b/spec/Spec/System/ProjectGroup.lean @@ -0,0 +1,40 @@ +import Spec.Prelude + +/-! +# ProjectGroup —— 飞书项目群作为协作空间(ADR-0001) + +ADR-0001 的核心:一个 project 对应一个**长生命周期**飞书项目群;群是协作空间,**不是锁 +owner**(锁归 `AgentRun`,见 `Lock` / ADR-0002),不是临时处理 session。群可在无 Claude +处理时保持开启;教师离群/静音与项目权限、与 Claude 生命周期相互独立。本模块钉死 +project↔group 的一对一绑定——likec4 画得出"project has group",画不出"恰好一个、且群 +不持锁"。 + +**群失效态与绑定快照(`OPEN`, ADR-0001 Consequences):** 群解散/归档/不可达时, +`GroupBinding` 快照应变为 `none`(解绑、允许 rebind)还是保持 `some` 但指向失效 chat +(悬挂、待管理员干预)未决策。ADR-0001 已点名 "rebinding or group archival needs +explicit product rules";本模块只刻画健康态 1:1 不变式,不臆造失效态语义。实现遇到 +群解散必须 surface,不得默认任一方。 +-/ + +namespace Spec.System + +variable (I : Identifiers) + +/-- 飞书项目群(`PINNED` 长生命周期协作空间, ADR-0001)。承载 project 与飞书 chat 的绑定; +**不是锁 owner**(锁归 `AgentRun`,见 `Lock`);不是临时 session。 -/ +structure ProjectGroup where + /-- 群对应的飞书 chat(`PINNED` 关系, ADR-0001 "one project has one Feishu project + group";chat 标识见 `Identifiers.ChatId`)。 -/ + chat : I.ChatId + +/-- 项目↔群绑定表(`PINNED` 每项目至多一个群, ADR-0001)。`ProjectId → Option ChatId` 的 +结构本身即"一个 project 至多绑一个群"(由 `Option` 自带);良构补另一半——单射。 -/ +def GroupBinding := I.ProjectId → Option I.ChatId + +/-- 绑定良构:**单射**——不同 project 不绑同一 chat(`PINNED` 1:1 的另一半, ADR-0001)。 +"每 project 至多一个群"由 `Option` 结构自带;这条钉死"每群至多属于一个 project"。群 +rebinding/archival 是生命周期事件(ADR-0001 Consequences),不在本快照不变式内。 -/ +def GroupBinding.WellFormed (b : GroupBinding I) : Prop := + ∀ p₁ p₂ c, b p₁ = some c → b p₂ = some c → p₁ = p₂ + +end Spec.System