Skip to content

[PR] kernel: Fix two byte-stability defects uncovered by verif — truncation must actually shorten + BLOCKED binding collision | kernel: 修 verif 挖出的两个字节稳定性缺陷 — 截断必须真变短 + BLOCKED 绑定撞车保护 (#3935, #3945) - #3972

Merged
ranxianglei merged 29 commits into
masterfrom
2026-10-20_3935-3945-verif-fixes
Oct 20, 2026

Conversation

@ranxianglei

Copy link
Copy Markdown
Owner

(ai: zhipuai-lb/glm-5.3)

kernel-change: 收口 #3853 verif 证明挖出的两个 kernel 字节稳定性缺陷(#3938 家族)

Fixes #3935
Fixes #3945
Part of #3938

Stacked on #3956(分支基于 PR-B 头 74eca4e,含 verif 套件与打桩;合并顺序 #3956 → 本 PR,合并后 diff 自动收缩)。

两个缺陷(都是 #3853 符号执行 + 反例回放发现的,PR-B 合同「只动何时不动改什么」故意不碰,按 issue 分开收口)

#3935 截断结果比原文长

truncateLargeToolOutputs 触发条件只有 original.length > keepPrefix + keepSuffix,从不要求替换文本严格更短。4001 字符的工具输出被截成 4064(prefix 2000 + 标记 ~63 + suffix 2000)——重写已被前缀缓存吃下的中途字节,同时还在膨胀上下文、上报正的 savedTokens(solver 见证字符级 saved = -63)。

修法(54bb967):keep 窗口总量被钳到原文在标记下方实际留出的空间(maxKeep = len − marker − 4,floor 64),外加最终 replacement.length >= original.length 拒施保险。大输出(≥4068)保持 2000+2000 满窗口、字节与 #3941 打桩时代完全一致(4066 pin 不变);无空间可留的候选原样跳过。

#3945 重复 id 改写已发送字节

BLOCKED ref 绑定按 id 存取但被同 id 的所有消息共享,保护却是按消息判定的。refs.ts 只要任一同 id 消息失去保护就把绑定迁走(delete + 新铸号),受保护的兄弟消息下一轮渲染凭空多出一个从未有过的 tag——中途改写已发送字节(generic harness Q2 求解器撞出)。

修法(ad90fea):assignRefs 预扫同 id 保护位,任一同 id 消息仍受保护 ⇒ 不迁移(BLOCKED 保持,双方渲染 verbatim);全部解除后才走 #2607 正常迁移。

打桩先行(红测→修→绿)

证明重订基线(修好后判据自动翻转)

验证

  • kernel suite 1367/1367(+10 pins),kernel tsc 绿
  • VERIF_PYTHON 全套 15/15 绿(cvc5 真跑)
  • bili 侧:golden-storage-render + 3769 两件套 + truncation 族 + storage-render + cache-proof + loop-truncation ×3 = 68 绿;basic + cache-friendly + plugin 34 绿;typecheck 绿
  • kernel 0.0.143→0.0.144,双 lock 同步

可见行为交底

  • 4001–4067 字符的截断产物从 4063± 变为 <原文(严格更短);≥4068 字节不变
  • 同 id 受保护+未保护并存时,未保护那条从「迁移重打标」变为「保持 verbatim」,直到全部解除保护

回滚

两个 commit 各自独立可回退(54bb967 / ad90fea)。

ework-agent and others added 29 commits October 20, 2026 17:42
The kernel kept only the newest TWO unmatched compress call+result pairs and hid older ones on EVERY turn, decoupled from real folds. On a third failed compress this deleted the oldest pair mid-history, rewriting an earlier cached prefix at full cost with no fold behind the break.

Replace the keep-two rotation with fold-gated, position-aware, persistent sweeping: orphans stay visible between folds (append-only, cache-friendly); a committed fold stamps pendingOrphanSweepMinRef (earliest new-block startRef) and the next pass hides only orphans at/after that ref, so the sweep rides the fold's own rewrite (cache-free) while earlier orphans (still-cached prefix) survive; swept ids persist in sweptOrphanCallIds (monotonic) so a resumed session never resurrects them.

Bump acp-kernel 0.0.136 -> 0.0.137.
…3769)

The #3769 seam landed in the 'no fold/switch/restart attribution' bucket because the break came from bili's own cleanup of failed-compress records, not a fold. Add an orphan-sweep attribution channel to the cache ledger: detect growth in the session's sweptOrphanCallIds set per sample and, when a mid-history break has no other claimant, label it prov='orphan-sweep' (count + missed tokens) instead of leaving it unexplained. A real fold claims its own break first, so there is no double-counting. New counters normalize through getCacheLedger for persistence compatibility.
types.ts and two kernel test files sit on a prettier-clean master baseline; the #3769 additions landed over-indented by one space. Normalized to the surrounding 2-space style so the diff stays confined to the feature. No behavior change; typecheck + targeted kernel/host suites re-run green.
…eview fix)

Review found a defect in the fold-marker computation: block-boundary specs (tier distillation compresses bN..bM) store startRef="bN" verbatim on the new block, so Number(startRef.replace(/\D/g,"")) parsed a BLOCK number, not the earliest covered MESSAGE ref. In long sessions that marks the sweep far too early: the next hide pass deletes failed pairs sitting in the still-cached prefix before the fold's own divergence point — re-introducing exactly the #3769 mid-history cache break on every tier-distillation fold.

Compute foldStartRef as the min refNum over each new block's effectiveMessageIds via state.messageRefs.byRaw instead; ids missing from the map (pruned) contribute nothing, which only under-sweeps (safe direction). refNum is exported from hide-consumed.ts so both consumers share one "unknown" definition.

Regression test 6 in issue3769-orphan-sweep.test.ts: m-boundary fold then block-boundary fold asserts pendingOrphanSweepMinRef === first covered ref (not the block number) and that the earlier pair stays visible. Verified to fail against the pre-fix code.
Review found the two new kernel state fields were dropped on every session load: buildRecord persists session.state wholesale, but the load path rebuilds it through mergeState's explicit field whitelist, which predated sweptOrphanCallIds / pendingOrphanSweepMinRef. Losing sweptOrphanCallIds resurrects already-cleaned failed pairs after a restart — a mid-history rewrite (cache break) that violates the PR's own persistence acceptance case. Losing the pending marker only defers a sweep by one fold (conservative).

Extend the mergeState whitelist with both fields, degrading to undefined for old persisted states exactly like every other optional field.
…-gated sweeps (#3769)

Three stale pins broke under the approved keep-two -> fold-gated behavior change:

- stub-resubmission-guard (#2749): the fixture applied folds without a call id, unlike production (src/loop/core.ts passes callId), so the resent call classified as orphan and the new sweep hid it. Pass "call-b1" at each first fold; all summary-integrity assertions unchanged. 5/5 green.
- cache-friendly-plugin: the two anthropic geometry subtests pinned the old KEEP_LAST_ORPHANED=2 rotation (oldest pair pruned on later turns). Rewritten to pin the new contract: failed pairs stay visible between folds, every anchor stays stripped while its own pair rides, quiet turns append-stable. A live-server probe plus the passing drop-pair/main-matrix subtests confirm the geometry expected values. Header docs updated to match the new mechanism. 11/11 green.
- storage-render goldens: regenerated via scripts/update-storage-render-goldens.ts. Diff is additive only — the persisted envelope gained lastSweptCount (cache ledger) and the two new kernel state keys (empty digests); state/blockContents/stats section digests unchanged.
Pre-#3769 states persisted the keep-two rotation's hidden set as message refs (hiddenOrphanRefs); the new hide pass ignored it, so upgrading would resurrect rotation-hidden failed pairs mid-history and break the cached prefix again. Honor the legacy set on upgrade; rememberHiddenRef re-records those refs every pass, so the clause self-perpetuates without any state migration.
syncBlocks deep-clones CompressionState with an explicit field list that missed hiddenOrphanRefs / sweptOrphanCallIds / pendingOrphanSweepMinRef. It runs BEFORE the hide-compress-calls node in every processTurn, so all three ledgers were wiped each turn: the fold-gated sweep never fired end-to-end and the legacy upgrade-compat clause was unreachable. Carry them exactly like cloneState does (lastPassIds stays excluded: its only reader runs pre-sync and the field is re-stamped at processTurn exit).
…P0)

Two processTurn-level pins: an upgraded pre-fold-gate state keeps its rotation-hidden orphan hidden across quiet turns (legacy hiddenOrphanRefs clause), and a fold marker set by applyCompression survives the full pipeline to the hide node (sync-blocks carry) so the fold-gated sweep actually fires end-to-end.
applyForkAdoption rebuilds session state from the parent on resume/fork replay; without carrying hiddenOrphanRefs and sweptOrphanCallIds, failed compress pairs already hidden pre-upgrade or already swept would resurface on replay, rewriting mid-history at full cache cost. Both ledgers are monotonic sets re-recorded every pass, so the carry self-perpetuates.
Real-server e2e: drive a session with a failed compress pair, persist it, patch the record back to an old-shape state (hiddenOrphanRefs set, no #3769 fields), reload under a fresh proxy, and assert the previously-hidden pair stays out of the outbound history while new turns append stably.
With the sync-blocks carry in place the sweep fires end-to-end: a failed compress pair appended at a fold step is swept by that step's own model request, so it never rides inbound and its anchor carries the summary for good (zero-carrier fail-safe, #1567). Re-pin the main matrix (all four wires), the swallow/back-to-back geometries (wide fold absorbs the alpha carrier; FOLD_E tail hits the protected zone), the drop-pair subtest (client-side drop is now a wire no-op) and the 3-concurrent-folds pin (carriers stack one per fold, stable thereafter), from observed live-server bodies. Google pair-absence proxy switches from the topic (which the carrier embeds) to the fold-spec refs that only the re-sent functionCall args carry.
…3769/#1567)

The fold-gated sweep hid EVERY orphan-fate compress pair at/after the fold's
start ref — including successful echoes whose call id never matched the
server-minted block id. A re-sent pair quoting an ACTIVE block's range is the
plugin lane's summary carrier (KDD#7), so hiding it strands the summary: the
#1999 double-carrier test, the plugin session-lock e2e, #1426 mode-upgrade
proof and #1638 notification pin all went red.

resolveFate's 'orphan' verdict is id-based and cannot see success; the sweep
branch now additionally requires the call to quote NO active block range
(quotesActiveBlock: both arg shapes — content[] entries and flat top-level
startId/endId — mirroring the host stripKernelSummaries carrier recognition).
Genuinely failed records and dead-block pairs (swallowed by a wider fold)
still sweep at the fold boundary, per the approved #3769 design.
…carrier regime and #3818 full-mode default (#3769 follow-through)

cache-friendly-plugin: the previous rewrite pinned the pre-floor-20 sweep
regime (successful echo pairs hidden at their fold step, anchors carrying).
That contradicts KDD#7 (plugin lane's wire carrier IS the tool call; the
agent view never renders the kernel acp_summary), the approved #3769 scope
(failed-record cleanup only), and the suite's own P6 dsh-rebase subtest,
which already pinned pair-rides/anchor-stripped. Re-pin to the verified
carrier regime across all four wires: pairs ride from their fold turn on
(summary twice per riding pair: args + receipt), SUM_MARKER zero while any
pair rides, drop-pair surfaces exactly its anchor once then stays
append-stable (#1567 fail-safe), dead-block pairs still sweep at the
swallow boundary (#3769), google lane expectations follow the #3159
canon-shift.

issue3769-upgrade-compat: since #3818 flipped the storage default to full,
the unified index row is the load path — patching only the JSON envelope
left a stale row the loader served instead, so the simulated old-kernel
record now goes through the store (loadSync + flushSync dual-writes both
copies). Teardown now closes both proxies even when an assert throws
(previously a mid-test failure hung the runner).
…#3691)

The watermark decision is made once: replaying the latched clip on every
later turn keeps outbound bytes stable when the token estimate fluctuates
across the threshold. Refs are content-bound so edited messages re-judge;
entries retire when their message leaves the view; a successful fold
resets the latch (the clipped originals ride the fold away). Carry
surfaces: sync node, persist mergeState, fork-adoption, plugin fork
prefix-filter, storage ingest.
…dary (#3939 ②, #3805)

The migration (#2607) mints the fresh numeric ref immediately (citable for
decompress bookkeeping) but the carrier message keeps its pre-migration,
UNTAGGED bytes until the next successful fold — stamping the <acp> tag on
the migration turn rewrote an old message mid-history on an otherwise
quiet turn (the #3805 durable-carrier cache breaker). Fold success
releases the deferral; carried across sync/persist/fork/plugin/ingest.

Also fixes the golden regen script missing the BILI_SNAPSHOT_SHADOW=0
parity pin (regenerated goldens red-flipped on the next CI run without
it); storage-render goldens now pin the two new undefined-valued state
keys, wire bodies unchanged.
…ch (#3939 ⑤)

absorb-hide, crush and filter keepLastOnly re-derive their output every
pass from state/context (absorb records growing, crush responding to
token pressure, keep-last-only demotions as new occurrences arrive) —
each change flipped OLD message bytes on an otherwise quiet turn (the
#3805 prefix-cache breaker class). One structural latch now covers all
of them: post-transform bytes are latched per padded ref at first
application and replay verbatim; refreshes ride fold boundaries
(applyCompression resets the map), the absorb action itself (instant-
reclaim contract kept), and config edits (digest release — enable/
disable applies on the edit turn, never silently later). ccr needs no
latch (replace-once-at-arrival, byte-stable by design #1460).

Placed after hide-compress-calls (the #3784 sweep keeps its own gate)
and before recommend/nudge/truncate/render so downstream judges see the
view the model actually sees. Carried across sync/persist/fork/plugin/
ingest; storage-render goldens pin the two new state keys (undefined
valued), wire bodies unchanged.
…eline the #3769 proof to the fold-gated contract (#3939)

- truncate-tools: build truncatedIds in the loop instead of spreading
  Map.keys() — the iterator spread degrades the symbolic translation of the
  3691 harness (verif refuses to certify on degradation).
- hide-consumed: hoist state.hiddenOrphanRefs ?? [] — .includes on a
  possibly-undefined receiver degrades the same way.
- verif/symbolic: fold Number(constString) to its numeric constant; the old
  {kind:any} made Number.isFinite collapse to constant false, silently
  deleting the refNum-gated fold-sweep path from every model (real code
  fires it; the model could not — engine gap, not kernel bug).
- verif-bug3769 harness re-baselined onto the #3784 fold gate: Q1 (append-only
  growth hides r1) is now UNSAT — the fix holds; Q1b proves the sweep is
  still derivable THROUGH the fold marker (judge not vacuous); replay pins
  hidden=0 without a pending fold and newlySwept=[c1,c2,c3] with one.
- kernel 0.0.142 -> 0.0.143 (both locks synced).

verif: 15/15 green with cvc5 (subset-guard, symbolic-smoke, 3691, 3769,
3805, 3676, generic, induction). kernel suite 1357/1357.
The clip trigger only checked original.length > keepPrefix + keepSuffix;
prefix + marker + suffix briefly exceeded the source just above the window
(4001 → 4064), rewriting banked prefix-cache bytes and INFLATING the
context while reporting saved tokens. The keep window is now capped to the
room the original actually leaves below the marker (floor 64 chars, final
strictly-shorter guard), large outputs keep the full 2000+2000 window
byte-identical, and candidates with no room stay verbatim.
…ed (#3945)

A BLOCKED ref binding is keyed by id but shared by every message with
that id, while protection is decided per message — refs.ts migrated the
binding as soon as ONE sibling lost protection, re-tagging a
still-protected sibling's already-sent bytes. assignRefs now
precomputes same-id protection and skips the migration while any sibling
stays protected; verif harnesses re-baselined (generic Q2 UNSAT =
collision theft unreachable; induction gains a protected-append UNSAT
and documents the remaining collision SAT as the legitimate #2607
protection-lift migration).
@ranxianglei ranxianglei changed the title kernel: 修 verif 挖出的两个字节稳定性缺陷 — 截断必须真变短 + BLOCKED 绑定撞车保护 (#3935, #3945) [PR] kernel: Fix two byte-stability defects uncovered by verif — truncation must actually shorten + BLOCKED binding collision | kernel: 修 verif 挖出的两个字节稳定性缺陷 — 截断必须真变短 + BLOCKED 绑定撞车保护 (#3935, #3945) Oct 20, 2026
@ranxianglei
ranxianglei merged commit 805c0a5 into master Oct 20, 2026
@github-actions

Copy link
Copy Markdown
Contributor

📦 Merged Build Published

This merge to master was published as 0.0.678-master.805c0a5 (rolling master tag).

npm install -g billion-context@0.0.678-master.805c0a5  # this exact build
npm install -g billion-context@master  # always the newest merged build

npm view billion-context@master prints the current version at any time.

ranxianglei pushed a commit that referenced this pull request Oct 20, 2026
t.skip() without return lets the async body keep running on solver-less environments: the TAP line renders as "not ok ... # SKIP" (cosmetic, counted as skip) but the post-skip work still executes and any later throw turns into a spurious failure. Same defect class as the guards restored for #3940 CI red; re-introduced by the #3972 wave.
@ranxianglei
ranxianglei deleted the 2026-10-20_3935-3945-verif-fixes branch October 20, 2026 14:21
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment