forked from bai/curriculum-project-hub
sjfhsjfh
3ebe4b754d
Remove filler/redundant patterns: 钉死/钉, 本模块, likec4 画不出/画得出, 臆造, 散文, 分歧点测试, 纯 plumbing, 恰好, 留白, 宪法第N条, 刻意. No code definitions changed, only doc comments.
49 lines
2.2 KiB
Lean4
49 lines
2.2 KiB
Lean4
import Spec.Prelude
|
|
|
|
/-!
|
|
# Memory —— 按需上下文:锚点与项目记忆(ADR-0003)
|
|
|
|
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
|
|
|
|
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)。"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
|