forked from EduCraft/curriculum-project-hub
hongjr03
8df8156969
Introduces the External Capability abstraction: platform-registered, org-enabled document/media transform services invoked as side effects of an AgentRun. The first concrete capability is pdf_to_md_bundle backed by MinerU. This lands the contract, schema, adapter interface, and a fully mock-tested adapter; the real MinerU HTTP client is deferred until credentials and pricing are confirmed. Contract: - spec/Spec/System/Agent/Capability.lean pins ExternalCapability, OrganizationCapabilityConnection (reuses ADR-0024 envelope, distinct from model-provider connection), and CapabilityInvocation.Authorized (workspace containment predicate, ADR-0018). lake build green (41 jobs). - ADR-0027 records why capability credentials are a separate connection type (MinerU/Whisper have their own auth shape, not OpenRouter /v1/models), the adapter seam, and what is deferred (capability invocation record, pricebook, agent-facing tool discovery). Schema: - OrganizationCapabilityConnection + CapabilityCredentialVersion, mirroring the Feishu Application Connection shape. Unique by (organizationId, capabilityId). Migration 20260718130000 applied. Adapter (hub/src/capability): - types.ts: CapabilityId, CapabilityAdapter interface, secret payload, CapabilityConnectionUnavailable. - mineruClient.ts: MineruClient interface + MineruParseResult + errors. Real HTTP client deferred; the interface is the seam. - capabilityConnections.ts: resolveCapabilityCredential — org-scoped, fail-closed, reuses LocalSecretEnvelope with purpose="capability". - pdfToMdBundle.ts: adapter that resolves credential, confines input/output to the run workspace (ADR-0018), calls MineruClient, writes md + images into workspace, and writes a UsageFact (kind=external_capability, quantity=pages, costSource=provider_reported|unknown per ADR-0022). Tests (7, all green): - md + images written to workspace, UsageFact attributes pages + cost - costUsd null -> costSource=unknown (missing cost != zero, ADR-0022) - no ACTIVE connection -> fail-closed, no fact written - input/output path escape -> CapabilityPathEscape - MinerU client error propagates, no fact written - empty markdown -> parse failure Deferred (needs operator): MinerU account/API key/pricing, real MineruClient HTTP implementation, org admin UI for capability connection management, agent-facing tool exposure (MCP vs built-in).
105 lines
4.8 KiB
Lean4
105 lines
4.8 KiB
Lean4
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
|