feat(hub): external capability registry for PDF/ASR transforms (ADR-0027) (#5)

Co-authored-by: Hong Jiarong <me@jrhim.com>
Co-committed-by: Hong Jiarong <me@jrhim.com>

spec/Spec/System/Agent/Capability.lean

@@ -0,0 +1,104 @@
+import Spec.Prelude
+import Spec.System.Agent.Run
+import Spec.System.Agent.Usage
+
+/-!
+# Capability —— 外部能力注册与调用(ADR-0027)
+
+`AgentRun` 内可能调用**外部能力**:PDF→MD bundle、音视频→文本、OCR 等。这些能力
+不是主 agent loop 的模型 completion,不持项目锁,不占 session 语义(ADR-0026 已拒绝
+nested Run)。它们是 Run 内的副作用:读 workspace 输入、调外部服务、产物落 workspace、
+写一条 `UsageFact`。
+
+本模块 pin 三件事:
+
+1. **ExternalCapability** —— 平台注册的、org 启用的文档/媒体转换服务,由稳定
+   `capabilityId` 标识。
+2. **CapabilityConnection** —— org-scoped 凭证连接,复用 ADR-0024 信封机制但独立于
+   model-provider connection。只有 `active` connection 可被 resolver 使用。
+3. **CapabilityInvocation 良构** —— 调用的输入/输出必须落在 run 的 workspace 内
+   (ADR-0018 `AgentSurface`),且调用产生的消耗必须以 `UsageFact` 记录。
+
+凭证不经 Agent 子进程:Agent 只通过 capability adapter 间接调用,adapter 在 Hub 侧
+解析 org-scoped 凭证并调用外部服务(ADR-0024 resolver boundary)。这与 model-provider
+的 loopback proxy 是不同的机制——capability 调用不走 agent 的网络面,走 Hub 直连。
+
+不变式(`PINNED`, ADR-0027):
+
+- **凭证隔离** —— capability credential 不进 Agent 进程环境;adapter 在 Hub 侧解析。
+- **workspace 边界** —— 输入路径与输出目录都必须落在 run 的 workspace 内(ADR-0018)。
+- **必记 fact** —— 一次成功调用必须产生 ≥1 条 `UsageFact`(`kind = externalCapability`),
+  即使 `costUsd = none`(unknown ≠ 零,ADR-0022/0026)。
+
+`CapabilityInvocation` 作为一等持久记录(status/retries/partial output)在 pilot 不做;
+`UsageFact` 的 `capabilityId + correlationId` 是唯一可追溯痕迹(ADR-0027 Deferred)。
+-/
+
+namespace Spec.System.Agent
+
+variable (I : Identifiers) (Path : Type)
+
+/-- 外部能力的输入种类(`PINNED`, ADR-0027)。集合 `OPEN`——新增 kind 须 surface。 -/
+inductive CapabilityInputKind where
+  /-- PDF 文档(`PINNED`)。 -/
+  | pdf
+  /-- 图片(`PINNED`)。 -/
+  | image
+  /-- 音频(`PINNED`)。 -/
+  | audio
+  /-- 视频(`PINNED`)。 -/
+  | video
+
+/-- 外部能力(`PINNED`, ADR-0027)。平台注册的文档/媒体转换服务,由 org 启用。
+
+一个 capability 由稳定 `capabilityId` 标识(如 `pdf_to_md_bundle`),声明接受的输入
+种类与计量单位。org 通过 `CapabilityConnection` 启用它;adapter 是平台侧实现。 -/
+structure ExternalCapability where
+  /-- 稳定能力标识(`PINNED`;如 `pdf_to_md_bundle`、`audio_video_to_text`)。 -/
+  capabilityId : String
+  /-- 接受的输入种类(`PINNED`, ADR-0027)。 -/
+  inputKind : CapabilityInputKind
+  /-- 计量单位(`OPEN`;如 `"pages"`、`"audio_seconds"`)。与 UsageFact.unit 对齐。 -/
+  meteringUnit : String
+
+/-- capability connection 的运行态(`PINNED`, ADR-0024/0027):与 model-provider /
+Feishu connection 同构,只有 `active` 可被 resolver 使用。 -/
+inductive CapabilityConnectionStatus where
+  | draft
+  | active
+  | disabled
+
+/-- Organization 的外部能力凭证连接(`PINNED`, ADR-0027)。复用 ADR-0024 信封机制
+但独立于 model-provider connection:capability 服务(如 MinerU、Whisper)有自己的 auth
+形状与 readiness probe,不走 OpenRouter `/v1/models`。唯一性键为
+`(organization, capabilityId)`。 -/
+structure OrganizationCapabilityConnection where
+  /-- connection 所属 organization(`PINNED`, ADR-0027)。 -/
+  organization : I.OrganizationId
+  /-- 该 connection 启用的 capability(`PINNED`, ADR-0027)。 -/
+  capability : ExternalCapability
+  /-- 运行态(`PINNED`, ADR-0024/0027)。 -/
+  status : CapabilityConnectionStatus
+
+/-- 一次 capability 调用的良构约束(`PINNED`, ADR-0027)。输入路径与输出目录都必须落在
+发起 run 的 workspace 内(ADR-0018 `AgentSurface`);`runWorkspace` 与 `pathWithin`
+由平台提供(表示 `OPEN`)。逃逸即越权,拒绝。 -/
+structure CapabilityInvocation where
+  /-- 发起调用的 run(`PINNED`;调用是 Run 内副作用,不跨 run,ADR-0026/0027)。 -/
+  run : I.RunId
+  /-- 被调用的 capability(`PINNED`)。 -/
+  capability : ExternalCapability
+  /-- 输入路径(workspace 内,`PINNED`, ADR-0018)。 -/
+  inputPath : Path
+  /-- 输出目录(workspace 内,`PINNED`, ADR-0018)。 -/
+  outputDir : Path
+
+/-- capability 调用良构:输入与输出路径都落在 run 的 workspace 内(`PINNED`,
+ADR-0018/0027)。这是 `AgentFileOp.Authorized` 在 capability 调用上的对应物。 -/
+def CapabilityInvocation.Authorized
+    (inv : CapabilityInvocation I Path)
+    (runWorkspace : I.RunId → Option Path)
+    (pathWithin : Path → Path → Prop) : Prop :=
+  ∃ w, runWorkspace inv.run = some w ∧ pathWithin inv.inputPath w ∧ pathWithin inv.outputDir w
+
+end Spec.System.Agent