feat(hub): usage fact ledger for run-scoped cost attribution (ADR-0026) (#4)

Co-authored-by: Hong Jiarong <me@jrhim.com> Co-committed-by: Hong Jiarong <me@jrhim.com>
2026-07-18 14:46:41 +08:00
parent 97f7972cc5
commit aaa098bb8b
11 changed files with 760 additions and 46 deletions
@@ -0,0 +1,92 @@
+import Spec.Prelude
+
+/-!
+# Usage —— Run 内用量计量事实账本(ADR-0026)
+
+一次 `AgentRun` 内可能产生**多条**可计费消耗:主模型 completion、外部能力调用
+(PDF→MD bundle、音视频转写等)、或代理网关侧旁路调用。这些消耗**不**是子 Run——
+它们不持项目锁、不占 session 语义、不复用 `AgentRun` 状态机。它们是 Run 内的
+append-only **计量事实**(`UsageFact`)。
+
+`AgentRun` 上的 cost/token 标量是 facts 的派生 rollup cache,不是真相来源;真相在
+`UsageFact` 行。这一层抽象让"主模型"与"外部能力"两类消耗共享同一账本,而非给后者
+各开一种特化字段或 nested Run。
+
+核心不变式(`PINNED`, ADR-0022 + ADR-0026):
+
+- **append-only** —— fact 一旦写入只读不更不删;`costUsd` 修正走新 fact,不改旧行。
+- **`costUsd = none` 表示"未知",不是"零成本"** —— ADR-0022:missing provider cost
+  remains unknown rather than zero。聚合时不得把 none 当 0 求和。
+- **fact 不持锁、不跨 run** —— 它是 Run 内的副作用账本,不是又一次 `@bot` 生命周期。
+  外部能力调用亦同:它的语义边界是 `capabilityId` + `correlationId`,不是 `RunId`。
+- **价目回算是派生** —— `costSource = pricebookDerived` 时,`costUsd` 由
+  `occurredAt × (provider, model)` 查价目表派生;provider 实报(`providerReported`)
+  优先于派生。无价目可查时 `costSource = unknown`,`costUsd = none`。
+
+外部能力(capability)注册表、价目表(pricebook)、商业结算均 `OPEN`,pilot 不做
+(ADR-0021 仍 defer commercial billing)。本模块只 pin **账本结构与不变式**。
+-/
+
+namespace Spec.System.Agent
+
+variable (I : Identifiers) (Time Cost Quantity : Type)
+
+/-- 计量事实类型(`PINNED`, ADR-0026)。集合完整性 `OPEN`——新增 kind 须 surface,
+不得静默把外部消耗塞进既有 kind。 -/
+inductive UsageFactKind where
+  /-- 主 agent loop 的模型 completion(`PINNED`)。 -/
+  | modelCompletion
+  /-- 外部能力调用(`PINNED`;如 pdf_to_md_bundle、audio_video_to_text)。 -/
+  | externalCapability
+  /-- 代理网关侧旁路调用(`PINNED`;非主 loop 的模型调用,如嵌入工具内的子请求)。 -/
+  | toolProxy
+
+/-- 成本来源(`PINNED`, ADR-0026)。优先级:provider 实报 > 价目派生 > unknown。 -/
+inductive CostSource where
+  /-- provider/gateway 实报(`PINNED`)。 -/
+  | providerReported
+  /-- 用 `occurredAt × (provider, model)` 价目表派生(`PINNED`)。 -/
+  | pricebookDerived
+  /-- 缺失,而非零(`PINNED`;ADR-0022 missing cost ≠ zero)。 -/
+  | unknown
+
+/-- 一次可计费消耗的计量事实(`PINNED`, ADR-0026)。append-only;一次 run ≥0 条。
+
+字段分两组:**归属与时间**(run/occurredAt/kind)用于聚合与价目回算;
+**计量与成本**(tokens/quantity/unit/costUsd/costSource)用于账目本身。
+非 token 计量(页/秒/次)走 `quantity + unit`,与 token 并存而非取代。 -/
+structure UsageFact where
+  /-- 所属 run(`PINNED`;fact 不跨 run,fact 不持锁,ADR-0026)。 -/
+  run : I.RunId
+  /-- 消耗发生时刻(`PINNED`);价目回算依赖此字段而非 run.finishedAt,
+  因为外部能力可能早于 run 结束。 -/
+  occurredAt : Time
+  /-- 事实类型(`PINNED`, ADR-0026)。 -/
+  kind : UsageFactKind
+  /-- provider 标识(`PINNED`;如 openrouter、mineru、openai_whisper)。 -/
+  provider : String
+  /-- 模型标识(`OPEN`;非模型计费可为 none)。 -/
+  model : Option String
+  /-- 输入 tokens(`OPEN`;非 token 计量可为 none)。 -/
+  inputTokens : Option Nat
+  /-- 输出 tokens(`OPEN`)。 -/
+  outputTokens : Option Nat
+  /-- 非 token 计量数值(`OPEN`;如页数、音频秒数)。与 tokens 并存。 -/
+  quantity : Option Quantity
+  /-- 计量单位(`OPEN`;如 "pages"、"audio_seconds"、"invocations")。 -/
+  unit : Option String
+  /-- 成本(`PINNED`;none = 未知,非零,ADR-0022)。 -/
+  costUsd : Option Cost
+  /-- 成本来源(`PINNED`;costUsd ≠ none 时必填,costUsd = none 时为 `unknown`)。 -/
+  costSource : CostSource
+  /-- 外部能力标识(`OPEN`;kind = externalCapability 时填,如 pdf_to_md_bundle)。 -/
+  capabilityId : Option String
+  /-- 外部请求关联 id(`OPEN`;对账/幂等用,不参与聚合)。 -/
+  correlationId : Option String
+
+/-- Fact 的成本是否**已知**(`PINNED`, ADR-0026)。聚合 rollup 时,只对已知成本求和;
+未知成本的 fact 不贡献 0,而是让汇总保持未知(若所有 fact 均未知)或部分未知。 -/
+def UsageFact.HasKnownCost (fact : UsageFact I Time Cost Quantity) : Prop :=
+  fact.costUsd ≠ none
+
+end Spec.System.Agent