Files
curriculum-project-hub/spec/Spec/System.lean
T
hongjr03 f3b087371a feat(hub): usage fact ledger for run-scoped cost attribution (ADR-0026)
Replace the single-scalar cost model on AgentRun with an append-only
UsageFact ledger. One AgentRun owns zero or more UsageFact rows; each
records one billable consumption event (model completion, external
capability, or tool proxy) with its own provider/model/tokens/quantity/
cost. AgentRun.costUsd/inputTokens/outputTokens become a derived rollup
cache.

This unblocks external capabilities (PDF->MD bundle, audio/video->text)
that bill in non-token units (pages, seconds) through a different
provider than the main agent loop, without per-capability schema changes
or nested AgentRuns (which would pollute lock/admission/session
semantics).

Contract:
- spec/Spec/System/Agent/Usage.lean pins UsageFact, UsageFactKind,
  CostSource and three invariants: append-only; belongs to one run,
  never holds a lock; missing cost != zero (ADR-0022).
- ADR-0026 records the decision, the rejected nested-Run alternative,
  the rollup cache strategy, and the deferred capability registry /
  pricebook / post-hoc correction flows.

Schema:
- UsageFact model with indexes on (runId, occurredAt), (runId, kind),
  (provider, model, occurredAt), (capabilityId, occurredAt).
- Migration backfills one synthetic model_completion fact per existing
  run with recorded cost/tokens (correlationId = runId marks backfill);
  truly unrecorded runs stay runsWithoutCost per ADR-0022.

Write path (trigger finish):
- Write the UsageFact first, then mirror it onto AgentRun as two
  separate statements (not one transaction). The fact is the truth so it
  goes first; the cache is derived so it goes second. A crash between
  them leaves the cache stale but the usage service re-reads facts
  directly, so this is recoverable; the reverse order would lose the
  truth. Separate statements also avoid an AgentRun row lock held across
  the insert's FK ShareLock, which deadlocked concurrent workspace
  teardown under the Organization->Project->AgentRun->UsageFact cascade.

Read paths:
- org/usage.ts aggregates from UsageFact, ignoring the AgentRun cache.
- slash /usage buckets by (fact.provider, fact.model); a run with a
  main loop + an external call lands in two buckets.
- session detail exposes usageFacts[] + costSource for future per-run
  cost-breakdown UI.

Tests:
- usage.test.ts: 6 integration tests pin fact aggregation, missing-cost-
  !=-zero, multi-fact-per-run, empty-run, project-level, empty-org.
- trigger.test.ts: existing /usage assertion ($0.0023,
  openrouter / mock-model) passes on the fact path.
- feishu-reactions mock prisma gains usageFact.create.
2026-07-18 14:44:23 +08:00

54 lines
3.0 KiB
Lean4
Raw Blame History

This file contains ambiguous Unicode characters
This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.
import Spec.System.Hierarchy
import Spec.System.ProjectGroup
import Spec.System.Organization
import Spec.System.User
import Spec.System.Connections
import Spec.System.ProjectWorkspace
import Spec.System.Capacity
import Spec.System.PlatformAdministration
import Spec.System.Agent.Run
import Spec.System.Agent.AgentRole
import Spec.System.Agent.Memory
import Spec.System.Agent.AgentSurface
import Spec.System.Agent.Usage
import Spec.System.Lock
import Spec.System.Permission
import Spec.System.PermissionGrant
import Spec.System.Audit
/-!
# System —— Hub 平台层契约
协作与执行的平台:项目、飞书群、AgentRun、锁、权限、审计、按需上下文。
likec4 已画出结构;这里补语义:
- `Hierarchy` —— 三层主体:平台 → 组织 → 用户。
- `User` —— 用户创建路径(管理员直接创建;飞书注册 `OPEN`)。
- `Connections` —— 外部连接:提供商枚举(当前仅飞书) + 绑定/信息类型。
- `ProjectGroup` —— project↔飞书群 1:1 长生命周期绑定(ADR-0001);群是协作空间,不持锁。
- `Organization` —— SaaS 租户(ADR-0020);project/team 单归属,TEAM grant 不跨 org;
connection secret 信封与 fail-closed resolver(ADR-0024);
owner/admin/member(`OrganizationRole`)及其管理规则(最后所有者保护)。
- `ProjectWorkspace` —— org 后台 project explorer:folder 是透明组织节点,project 仍是权限边界
(ADR-0021)。
- `Capacity` —— platform ceiling 与 org policy 的分层限制、持久 admission request 状态和
平台紧急工作负载制动(ADR-0022)。
- `PlatformAdministration` —— 独立平台身份/会话、单一管理员角色、绑定邀请、最后管理员
保护、fail-closed 平台审计与离线 emergency grant(ADR-0023)。
- `AgentRole` —— org-scoped agent 角色配置 + 技能(ADR-0017/0018)。
- `Run` —— AgentRun 状态与终止判定(状态集合完整性 OPEN)。
- `Lock` —— 锁 owner=run(ADR-0002),及"持锁者必为非终止 run"的核心不变式。
- `Memory` —— 按需上下文:锚点类别(ADR-0003)+ MCP 工具按 run/project 上下文授权。
- `AgentSurface` —— agent 执行面被 run 的工作区所界定(ADR-0018);与 Lock 正交——
Lock 限定并发,Surface 限定波及面。机制 OPEN。
- `Usage` —— Run 内 append-only 用量计量事实账本(ADR-0026);主模型 completion、
外部能力调用、代理网关旁路共用同一账本。fact 不持锁、不跨 run;`costUsd = none`
表示未知而非零(ADR-0022)。Run 上的 cost/token 标量是其 rollup cache。
- `Permission` —— read⊂edit⊂manage 角色体系、能力推导、单调性;force-release 在格外。
- `PermissionGrant` —— grant(resource×principal×role)与 settings(六 policy 旋钮)
(ADR-0004);组合规则 OPEN。
- `Audit` —— customer Project/Run 审计从简(内容 OPEN);Platform Audit 由
`PlatformAdministration` 独立承载。
标识符见 `Spec.Prelude`。决策出处:ADR-0001..0004, 0018, 0020..0026。
-/