kimi-code/FormularDefTree/nodes/undo-spine-compaction/node.md

id	parent	status	version
undo_spine_compaction	root	active	0.2.2

undo × spine × compaction Caliber-Identity FormularDef Node

Motivation

"频繁 compact" 诊断(2026-07-13)揭示:undo、spine、compaction 三个域共享一个 隐含不变量——存储历史与模型所见同一(caliber identity)。v1 式 compaction 物理替换历史,不变量自然成立;spine 把存储改为 append-only + 投影折叠, 不变量被打破,而多个旧路径仍按它工作。本节点把 trio 的共享状态、不变量、 以及全部已确认违规形式化,作为后续修复的验收基准。

Snapshot Scope

repo: project
paths:
  - packages/agent-core-v2/src/agent/contextMemory/(contextMemoryService, contextOps).ts
  - packages/agent-core-v2/src/agent/contextSize/(contextSizeService, contextSizeOps).ts
  - packages/agent-core-v2/src/agent/spine/(spineService, spineFold, spineOps).ts
  - packages/agent-core-v2/src/agent/fullCompaction/fullCompactionService.ts
  - packages/agent-core-v2/test/agent/fullCompaction/repro-frequent-compaction.test.ts
status: current

Parent Contract

继承 root I1–I4。本节点是 trio 关系的权威节点;spine_compaction 节点 保留路由设计的细节,其 Gap 与本节点交叉引用。

Quint-Style Kernel

Design kernel(候选,从诊断结论反推,未经用户批准):

module undo_spine_compaction {
  type Msg = { role: Role, origin: Origin }
  type Node = { id: str, openedAt: int, closedAt: int | none, memory: str | none }
  type Gauge = { length: int, tokens: int, kind: {Measured, Estimate} }

  // 三域共享的可观察状态
  type State = {
    history: Seq[Msg],        // contextMemory 拥有(存储)
    tree: { nodes: Node[], epochStartAt: int, epochMemoryAt: int | none },  // spine 拥有
    gauge: Gauge,             // contextSize 拥有(live-only)
    lastObserved: int,        // spine 内存态(findEvidence 起点)
    pending: Transition | none
  }

  type Event =
    | Append(Msg) | Undo(cut: int) | Clear
    | RootCompact(epochStartAt: int) | ApplyCompaction(newHistory: Seq[Msg])
    | StepEnd(toolCallId) | Restore

  // 投影:模型所见 = fold(history, tree);gauge 触发 = gauge.tokens + est(尾部)
  pure def view(s: State): Seq[Msg] = foldSpine(s.history, s.tree)
  pure def triggerSize(s: State): int = s.gauge.tokens + est(s.history[s.gauge.length:])

  pure def inv(s: State): bool =
    // INV-IDX 下标锚定:树内所有下标落在历史范围内
    and {
      forall n in s.tree.nodes: n.openedAt < len(s.history),
      forall n in s.tree.nodes: n.closedAt != none => n.closedAt < len(s.history),
      s.tree.epochStartAt <= len(s.history),
      s.lastObserved <= len(s.history)
    }
    // INV-CAL 口径同一:gauge 的估算值 ≈ 下一次请求的真实成本(投影口径)
    //   est(raw history) ≈ est(view(s)) —— spine 下 raw ≫ view,估算必须走投影
    // INV-VIEW 投影诚实:view 既不复活已截断内容,也不隐藏存活内容
    //   forall e in {Undo, Clear}: view(s') 只含 s'.history 中的消息(除合成 memory/status)
    // INV-SYNC 提交同步:已接受回执 <=> 已提交 op(树 == 模型认知)

  // 反例形状(全部已复现,见 Validation):
  //   破 INV-IDX/INV-VIEW: Undo 切进 closed span -> fold 吐出陈旧 memory 并
  //     跳过越界 closedAt -> 其后全部新消息被吞噬(repro F)
  //   破 INV-IDX(lastObserved): Undo 后下一个 spine 转移 findEvidence 越界
  //     -> null -> 转移丢失(repro E)
  //   破 INV-IDX(epochStartAt): Clear 后 epochStartAt 悬空 -> fold 丢弃全部
  //     重建历史(repro G)
  //   破 INV-CAL: Undo 重定基 = est(原始存活历史) >> est(投影) -> 虚假压缩
  //     (repro D);Resume 后 gauge={0,0} 同理(静态)
}

Design Formular

D(候选,未经批准):
  D1 任何截断/清空历史的事件(Undo/Clear/ApplyCompaction)必须同时:
     (a) 把树内越界下标钳入 [0, len(history')) 或重置受影响节点;
     (b) 把 gauge 重定基为 投影口径 估算;
     (c) 把 lastObserved 钳到 len(history')。
  D2 gauge 的所有估算路径(undo 重定基、resume 回退、compaction 落地)
     统一使用 est(project(history))。
  D3 spine 模式下 compaction 的 summary 输入为当前历元
     (旧历元已由 summary + 归档覆盖);溢出启发式同用投影口径。
  D4 历元边界是 undo 的硬边界(现状,有意的行为对齐)。

Implementation Formular

I(快照 4ade2ee9b,全部 verified):
  Undo:  contextMemoryService.undo (:99-111)
    - 边界: computeUndoCut 遇 compaction_summary 停止 (contextOps.ts:301-320)
    - 级联: sizeOpsForCut (:160-170) —— 仅当 cutIndex < gauge.length 时,
      gauge := est(原始存活前缀)  ← 违反 D1b/D2(spine 下 raw ≫ view)
    - spine 侧: 无任何订阅;lastObserved 不动  ← 违反 D1c;树下标悬空 ← 违反 D1a
  Clear: promptService.clear -> context.clear (:89-97)
    - gauge := {0,0}(诚实);树完全不动  ← 违反 D1a(repro G)
  RootCompact: applyRootCompaction (fullCompactionService.ts:779-832)
    - append-only + gauge := est(summary)(投影口径,正确);树历元推进(正确)
  Summary 输入: originalHistory = 全部存储历史 (:609)  ← 违反 D3
    (实测: 460k / 773k / 1.04M token;repro A: 需 3 次收缩)
  413 启发式: estimateCurrentRequestTokens = 原始历史 (:237-239)  ← 违反 D3
    (repro C: 一个 turn 内 3 次徒劳压缩后硬失败)
  Resume: gauge live-only,重放后 {0,0} (contextSizeOps.ts:30-32),
    get() 回退 est(全部原始历史) (contextSizeService.ts:85)  ← 违反 D2(静态)
  折叠: foldSpine span 不钳制 (spineFold.ts:95-103)  ← 违反 INV-VIEW(repro F)
  提交: findEvidence(from=lastObserved) 不钳制 (spineService.ts:368-374,
    544-565)  ← 违反 INV-SYNC(repro E,每次 undo 丢一个转移)
  分类:
    - RootCompact 路由/历元推进/阻塞时序: intended(test/spine/compaction.test.ts)
    - undo 边界停在 summary: intended(与非 spine 对齐)
    - 上述各违反项: bug(未感知 spine 的存储/视图分离)
    - flag 运行中翻转、异步压缩交错: unknown(非默认路径,未复现)

Refinement Map

alpha_state: (ContextModel, SpineModel, ContextSizeModel, 内存 pending/lastObserved)
           -> (history, tree, gauge, lastObserved, pending)
义务: I 在 {Undo, Clear, Resume, 413} 事件上不 refine D(D1a-c/D2/D3 全部有反例);
      I 在 {RootCompact, 阻塞式自动压缩} 上 refine D(既有测试)。
剩余证明义务: D1a 的"钳制 vs 重置节点"语义需用户拍板(见 Gap 批次 3)。

Gap(D, I) / Known Non-Refinements / Debt

按严重度排序(复现 = test/agent/fullCompaction/repro-frequent-compaction.test.ts,
该 scratch 已删除,场景转为正式回归测试):

P1 [FIXED 2026-07-13] undo 切进 closed span -> 陈旧 memory 吞噬其后全部新消息
   (含用户最新 prompt),模型盲答。spineFold.ts:95-103 不钳制 closedAt。
   修复:spine.truncate_repair op(spineOps.ts)在 undo 截断时持久化修复
   (跨切点 span 钳到 cut-1、全截断 span 作废、open span 重启于切点);
   spineService 订阅 context.spliced 触发。回归:test/spine/spine.test.ts
   "keeps post-undo messages out of a truncated closed span" + 两个 reducer
   测试。
P2 [FIXED 2026-07-13] undo 后 lastObserved 越界 -> 下一个 spine 转移被 drop
   (每次 undo 丢一个,树与模型认知分叉;误报 unexpected error)。
   修复:截断时游标重置为 min(lastObservedIndex, cut)(spineService splice
   订阅)+ commitPending 钳制兜底。回归:"commits a spine transition after
   an undo shrank the history"。
P3 [FIXED 2026-07-13] /clear(尤其历元边界后)-> epochStartAt 悬空 ->
   fold 丢弃全部重建历史,模型只剩 status 行。
   修复:truncate_repair 同时钳 epochStartAt/epochMemoryAt(clear = cut=0
   的同一修复路径,旧历元保留在树中)。回归:"keeps the rebuilt history
   visible after /clear with a dangling epoch boundary"。
P4 [FIXED 2026-07-13] undo 重定基用原始估算 -> gauge 毒化 -> 下一 turn 虚假
   阻塞压缩。"频繁 compact" 主根因;真实会话(mre987c4)3/3 次 auto 压缩
   全部 undo 后触发,真实请求仅 29-46k。
   修复:sizeOpsForCut 改投影口径(contextMemoryService 注入
   contextProjector,try/catch 回退原始估算)。回归:
   fullCompaction.test.ts "does not auto-compact after an undo when the
   folded view is small"。
P5 [FIXED 2026-07-13] summary 输入 = 全部原始历史(实测 77-104 万 token/次,
   5 次合计 335 万);窗口不足时收缩阶梯后仍可能失败,且阈值路径无熔断。
   修复:epochScopedHistory —— 仅当前历元 + 前历元 summary 链入
   (fullCompactionService)。回归:test/spine/compaction.test.ts
   "summarizes only the current epoch and chains the previous epoch summary"。
P6 [FIXED 2026-07-13] 413 启发式按原始估算 -> 3 次徒劳压缩后 CONTEXT_OVERFLOW。
   修复:estimateCurrentRequestTokens 改投影口径。回归:
   "does not treat a provider 413 as context overflow when the projected
   view is small"。
P7 [FIXED 2026-07-13] 非 spine: 压缩后 floor 仍 >= 阈值时每个 turn 重压。
   修复:compactionFutile 抑制器(tokensAfter 仍超阈值则暂停 auto 压缩并
   warn,历史替换/模型降档时解除)+ floor 跨 turn 保留(模型降档/历史
   替换时重置)。回归:"pauses auto compaction when the compacted shape
   still exceeds the threshold"。
P8 [FIXED 2026-07-13] resume 后 gauge 回退 est(全部原始历史)。
   修复:contextSizeService.get() 从未测量时全量估算改投影口径
   (estimateProjected,带重入防护——fold 的 buildStatus 会读回 gauge)。
   注:该重入循环在实现时被测试捕获(空上下文无限递归),防护已入代码。
P9 [open, 静态] 异步压缩模式(compactionTriggerRatio < blockRatio)下
   pending × root_compact 交错:关错节点或 guard 静默 no-op 且审计不可见。
   非默认配置。详见 spine_compaction 节点 G-A。
P10 [debt→缓解] spine 模式下存储历史只增不减:compaction 成本随会话年龄
   增长——P5 修复后 summary 输入改为当前历元,成本有界;undo 够不着旧
   历元(与"历史可追溯"卖点的张力)留作设计讨论(批次 3)。
P11 [open] flag 运行中翻转:pending 不清、lastObserved 不推进,未定义。
P12 [FIXED 2026-07-13] 显示层口径分裂(TUI footer):contextTokens 仅实测
   前缀(不含尾部)、仅在测量时更新;rawContextTokens 仅在 ContextModel
   变更时重算——测量落地不重算 → raw 滞后甚至 raw < projection(生产
   截图实证:raw 549 / projection 28.8k,违背 rawSize 的 >= 设计声明),
   且 resume 后 getStatus()(measured+estimated)与事件(measured-only)
   口径不同。修复:contextSizeService.publishSizes 双订阅
   (ContextModel + ContextSizeModel)统一发布,contextTokens 改发
   get().size(含尾部),op 的 toEvent 移除;12 个快照更新(事件形状
   由 {raw} 变 {contextTokens, rawContextTokens})。

Validation

Validation Choice: scenarios(复现套件)+ review;不上可执行 Quint。
Reason: 全部不变量都有具体反例轨迹,修复为局部钳制/口径替换;缺机制不缺证明。
  升级条件不变:undo 语义重做(批次 3)或异步压缩成为默认时,把 kernel
  落成 .qnt 做交错检查(需用户明确要求)。
Result:
  - 复现套件(A-G)已于修复后转为正式回归测试并全部转绿(2026-07-13):
    A→test/spine/compaction.test.ts;B/C/D→test/agent/fullCompaction/
    fullCompaction.test.ts;E/F/G→test/spine/spine.test.ts;scratch 文件
    已删除。
  - 真实会话取证: wd_kimi-code-bench-analysis/mre987c4(聚合统计,
    未读消息内容): 5 begins / 4 completes / 1 cancel;3 次 auto 全部 undo 后;
    summary 请求 460k/30k(异常,见下)/1.04M/773k。
  - 未解异常: 07-10 19:46 的 summary 请求仅计费 30k(同时段同规模历史
    计费 460k),所有 commit 均为全量输入,疑为当天 WIP build 行为;
    不影响主结论。
  - 修复副作用:既存 7 个快照(loop/plan/tool/config)更新——P8 顺带
    修正了 rawSize 在未测量窗口对 (raw−projected) 的双重计数(旧值
    偏高);新快照值 = 真实 raw 估算。

Code Mapping

undo:      contextMemory/contextMemoryService.ts:89-170, contextOps.ts:301-380
gauge:     contextSize/contextSizeService.ts:70-115, contextSizeOps.ts:60-108
fold:      spine/spineFold.ts:66-118; 提交: spine/spineService.ts:363-470,544-565
compact:   fullCompaction/fullCompactionService.ts:237-275,432-509,604-832
repro:     test/agent/fullCompaction/repro-frequent-compaction.test.ts (A-G)
既有测试:  test/spine/(compaction, fold, archive, spine).test.ts

Evolution Log

2026-07-13 节点创建(频繁 compact 诊断 + undo×spine 复查):
  形式化 trio 共享不变量 INV-IDX/CAL/VIEW/SYNC;P1-P11 全部记录,
  其中 P1-P7 有复现(7 红),P8/P9/P11 静态。快照 4ade2ee9b (spine-v2)。
2026-07-13 (v0.2.0) P1-P8 全部修复并转正式回归测试(全量 3285 测试绿):
  truncate_repair op + splice 订阅(P1/P2/P3)、gauge 投影口径(P4/P8,
  附带 rawSize 双重计数修正与 7 个快照更新)、历元范围 summary 输入
  (P5)、413 投影口径(P6)、compactionFutile + floor 跨 turn(P7)。
  修复期新增发现并堵上 estimateProjected 重入循环(fold buildStatus
  读回 gauge)。P9/P11 保持 open(非默认路径)。scratch 复现文件已删除。
2026-07-13 (v0.2.1) deep review 跟进(外部评审四条):
  F1(声称 undo 越过历元边界致盲)经核验不可达——computeUndoCut 遇
  compaction_summary 即停且不足 count 整体拒绝(contextOps.ts:301-320),
  切点永远 ≥ epochStartAt;仍按建议防御化:anchor 被截则 epochStartAt
  回退 0(无损保守),不再压到 cut。
  F2(升档不清 futile/floor)修复:任何窗口变化即重校准。
  F3(投影估算三处拷贝)收敛为 IAgentContextProjectorService.
  estimateProjectedTokens;重入守卫留在 contextSize 本地包裹。
  F4(splice 隐含尾部截断契约)加不变量注释 + 非等长跳过防御。
2026-07-13 (v0.2.2) P12 显示层口径统一(用户生产截图:raw 549 <
  projection 28.8k):publishSizes 双订阅统一发布,contextTokens 改发
  get().size 含尾部,消除 raw 滞后与 getStatus/事件口径分裂;
  全量 3287 测试绿,12 个快照更新。