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