forked from bai/curriculum-project-hub
hongjr03
f3b087371a
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.
spec —— Lean 语义母本
这是本 monorepo 的契约:产品各部件语义的上游参照,用 Lean 编写。它的定位与约束见仓库根 README.md 的"宪法"5 条——本文件只讲怎么往这份契约里写东西。
现状
刚初始化的 Lean 工程(lake init),目前只有占位内容(Spec/Basic.lean)。实质领域内容(System 平台层、Courseware 产品层)将逐个概念加入,每个都遵循下面的规范。
构建
cd spec
lake build
工具链锁定在 lean-toolchain(leanprover/lean4:v4.31.0)。无外部依赖——Mathlib / Batteries 等留待第一个真正需要它的定理出现时再引入(依赖碰到再加)。
写作规范
双半契约:prose + type
每个 top-level 声明必须带 /-- … -/ doc 注释,用自然语言陈述其语义意图。两半缺一不可:
- prose 半给人读——说清"这在领域里是什么、为什么"。
- type 半给机器读、给 type checker 把关——保证结构无洞。
agent 不得用预训练先验脑补本领域(领域很新,无先验);prose 是 agent 理解语义的唯一权威来源。
标签分类法
在 doc 注释里用以下标签标注每条语义的状态:
PINNED—— 已解决的分歧点,契约在此处权威,双方据此对齐。OPEN—— 故意未规定。双方均不得假设其解;实现遇到时必须 surface 出来讨论,而不是擅自决定。ADR-NNNN—— 链接到根docs/adr/下的对应决策记录(如ADR-0002),交代该语义的决策出处。
分歧点测试(写之前先过一遍)
新增任何概念前,先问:"不写明,开发者与 agent 会不会各自做出不同假设?"
- 会 → 它是分歧点,入契约。
- 不会(显然的东西 / 纯 plumbing / 普通 CRUD 字段)→ 不入。
详见根 README 宪法第 5 条。
不用 sorry
无法陈述清楚的东西,用 OPEN 在 prose 里标注,而不是用 sorry 留一个假装成立的定理。sorry 会让 lake build 仍然变绿,却在契约里埋一个谎——这与"契约自包含、无洞"直接冲突。
命名
- 模块 / 命名空间:PascalCase,对应分层,如
Spec.System.Agent.Run、Spec.Courseware.Validity。 - 类型:PascalCase。
- 谓词 /
Prop:用意图清晰的命名,如Legal…、ValidTransition、Can…。 - 文件粒度:原则上"一个带独立不变式的概念一个文件"。