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