test(formal): advance the kernel witness monitor per step and bound the pilot's generation ratio

[lan17]

Slice 4 of the #165 pilot. #171's own measurement said the kernel views could not generate at parity: at the pinned 2,000 × 40 workload they took 4 to 7 times as long as the original profiles with invariants and 9 to 13 times without. The cause was the witness design, not the kernel: cache-kernel.qnt kept var history and recomputed the label set by refolding the whole history at every step, so witness cost grew with history length and the history itself was emitted in every ITF state. This PR makes the monitor incremental, bounds the kernel's sampling cost in the same job, measures the generation lane's own command for both models, and pins the pilot inventory. No profile, driver or production code changes.

The pilot's "generate at parity" criterion is not met, and this PR now says so in its report. Under the generation lane's real command (512 traces per profile, --mbt) both kernel views exhaust Node's default heap before writing a trace; the effects view needs about 7 GB of memory and 2.3× the original's wall time to finish when given a 12 GB heap, because the kernel's exported state is 2.7× the original's per ITF state. The sampling-cost bound below passes, but it is not the #165 generation budget; the report records generationParity: false until the exported state shrinks or the lane's configuration for kernel-based profiles changes. This was found by the review described at the end.

The monitor advances one value per step

lifecycle_witnesses now exposes advance(monitor, step, heldEffects, budget); the kernel records var monitor: Witness::Monitor and sets monitor' = Witness::advance(monitor, { input, observation }, ...) in commit, and from emptyMonitor in initialize. The credited labels live in monitor.labels; the separate witnesses variable and the retained history are gone. The four whole-history prefix predicates (future-frame refill and the three tracked-layers boundaries) became data: a Script fixes the public input order and, per step, the observation fields that establish the consequence (Expect = Any | Exactly(int), ExpectCalls = AnyCalls | ExactlyCalls(List[int])). The monitor keeps one cursor per script: the matched prefix length, -1 once a history departs, complete once it reaches the script length. A departed history can never earn the label; a completed prefix keeps it.

reached(history, heldEffects, budget) remains as the fold of advance over a history and is what the monitor's own controls exercise, so the incremental form and the whole-history form agree by construction. All 13 existing positive and negative controls pass unchanged against the new monitor. Two controls are added, each checked to fail on the mutant it targets: a history that departs from a script at step 1 earns nothing even when the complete script follows (a cursor that restarted on mismatch would credit it), and each script earns nothing under the other view (removing the view gate would credit it). An independent differential run during review compared the old whole-history reached with the new fold over every prefix of every control fixture, all single and double point mutants of those fixtures, and 4,000 random 16-step histories under both views and both budgets, with no disagreement.

The witness-isolation lint now names the single witness variable ((^|::)monitor$) and requires exactly one. The runner reads K::monitor from the kernel trace and projects its labels set as the trace's pilotWitnesses; a monitor without a label set is rejected rather than reconstructed.

Two kernel invariants made linear

With the refold gone, the kernel's own invariants were the next cost: oneRegisteredFlightPerIdentity compared every pair of executions and registeredExecutionsHavePendingCallers searched the calls for every execution, so at 80 steps the pilot's five properties cost more than the original layers profile's nine. Both are restated with the same meaning in linear form: the registered shared executions have as many distinct instance/key identities as members, and every unfinished execution's owner is in the set of owners with a pending call. The challenge checks that use them still fail at their declared steps. oneRegisteredFlightPerIdentity had no fault that only it detects, so one is added: a kernel that never lets a second caller join the registered process flight fails the property at the second call in both shared-source histories, and the unmodified kernel passes every step of both. Every pilot property except the closed-scope memo rule now has such a fault, and the tests pin that.

Sampling-cost bound and the generation-lane measurement

For each profile the runner samples the original's generation bounds from execution.json (layers 2,048 samples of 80 steps, effects 4,096 of 60; pinned seed, one thread, no trace output) in both models with their own invariants, twice each with the two models alternating, and fails when the kernel view's fastest wall time exceeds exploration.maxRatio in pilot.json, set to 2.5, times the original's fastest. A violation is recorded and raised only after the history differentials, native replays and fault checks have run, so a slow week still yields the correctness evidence. Three records locate the remaining cost and are not gated: the same pairing without invariants; the kernel view with its monitor assignment replaced by monitor' = monitor, whose difference to the full view is the monitor's cost; and each side's property cost (gated run minus plain run), because the originals pay about twice as much for their nine invariants as the kernel does for its five, which flatters the gated ratio.

Separately, the runner issues the generation lane's own command for both models (--mbt, the original's 512 traces, ITF output to a scratch directory removed after counting) and records each model's exit status, wall time, traces and bytes, plus generationParity. The original must complete; the kernel view's failure is recorded rather than failing the check, so the weekly job keeps producing evidence while the state-size work happens.

Faster of two runs, wall time including CLI startup (about 1 s per run locally, 2 to 3 s hosted); the hosted column is the kernel-pilot job of run 34902237253:

Pairing (generation bounds)	Original, local	Kernel, local	Ratio, local	Ratio, hosted	Bound
layers, with invariants	8.0 s	8.5 s	1.06×	1.20×	2.5×
layers, without invariants	2.8 s	5.4 s	1.88×	1.95×	recorded
layers, kernel with frozen monitor	8.0 s	6.1 s	0.76×		recorded
effects, with invariants	7.0 s	11.4 s	1.63×	1.76×	2.5×
effects, without invariants	2.5 s	8.7 s	3.53×	3.41×	recorded
effects, kernel with frozen monitor	7.0 s	7.3 s	1.05×		recorded
layers, generation lane (512 traces)	14.7 s, 175 MB	heap exhausted, 0 traces			recorded
effects, generation lane (512 traces)	10.9 s, 112 MB	heap exhausted, 0 traces			recorded

The bound started at 2; the first hosted measurement left effects 12% under it, too little for a required weekly job on runners that vary, so it is 2.5. Two more hosted runs measured 1.12× and 1.60× (34904430717, on a slower runner: 17 s for the layers original against 13.7 s the first time) and 1.19× and 1.78× (34906552607). The bound still fails on the 4 to 7× of the refolding monitor. If a later slice brings the effects view down, the bound should follow.

For reference, before this PR at 2,000 × 40 the same pairs were 4.1× and 8.8× (layers) and 6.7× and 13.1× (effects). The frozen-monitor rows say where the rest is: with the monitor frozen the kernel views sit at or below the originals with invariants, so nearly all of the remaining wall-time difference is the monitor's per-step bookkeeping (about 13 to 17 µs per step, linear in the view's bounded call count, no longer in history length), not the kernel's state. Making the monitor cheaper is the next parity work item for sampling cost. The generation-lane rows say the other half: the kernel's exported state, not its speed, is what blocks the actual corpus, and that is exported-state size work.

Pins

test/formal-kernel-pilot.test.ts pins the inventory that the #171 review left unpinned: 12 histories (5 layers, 7 effects), 11 distinct labels, 6 faults with 9 checks covering 4 of the 5 properties, 5 properties, 15 Quint monitor controls, 2 exploration repetitions, and the 4 scripts with their labels. The catalog validator requires the exploration bound.

Evidence

• Local node formal/kernel-pilot.mjs check at ac03fd1: passed and complete in 341 s (189 s at test(formal): add shared lifecycle kernel pilot #171's head; the difference is the added timing, frozen-monitor and generation-lane measurements); 12 histories agree step by step with the originals and replay in both ports, all 9 fault checks fail at their declared checkpoints, 17 monitor controls pass, gated ratios 1.02× (layers) and 1.67× (effects) against the 2.5× bound, frozen-monitor 0.77× and 1.09×, property-cost ratio 0.57 and 0.59, generation lane: originals complete (14.0 s, 12.1 s), kernel views abort on heap exhaustion (SIGABRT, zero traces) under Node v24.20.0 with a 4.5 GB heap limit, generationParity: false. Kernel raw traces are 1.9 to 3.5× the originals' size for the twelve histories.
• Full formal run on fe7a87f: https://github.com/lan17/DialCache/actions/runs/34902237253. check-models, generate, symbolic and kernel-pilot passed (hosted pilot 468 s, all histories, replays and faults); the TypeScript mutation, parity and merge lanes failed on a formal/README.md wording change that tripped the source audit, reverted in 4801d1d. Run on 4fd8101: https://github.com/lan17/DialCache/actions/runs/34904430717, every lane green (check-models, generate, symbolic, kernel-pilot, both parities, all six mutation shards and both merges) except TypeScript parity, which hit the 5 s flake fixed above. Run on 174807e: https://github.com/lan17/DialCache/actions/runs/34906552607, green in all 15 jobs including the aggregate. Run on a9cee75 (after the report-mode review): https://github.com/lan17/DialCache/actions/runs/34916911057, green in all 15 jobs. Its kernel-pilot job took 15 minutes (852 s in the runner, against 7 to 9 minutes before): the generation-lane measurement costs about 30 s per original and 80 s per kernel view on the hosted runner before the heap is exhausted. Hosted numbers there: gated 1.19× and 1.76×, frozen-monitor 0.87× and 1.11×, property-cost ratio 0.68 and 0.66, generationParity: false. Run on the final head ac03fd1 (after the until-clean rounds): https://github.com/lan17/DialCache/actions/runs/34995257291, green in all 15 jobs; kernel-pilot 846 s (about 15 minutes), gated 1.18× and 1.74×, frozen-monitor 0.86× and 1.09×, property-cost ratio 0.69 and 0.66, kernel attempts aborting on heap exhaustion at 79 s and 82 s under 150 s timeouts, with the runner's node v24.20.0, 4 GB heap limit and 17 GB of memory recorded, generationParity: false.
• tsc --noEmit, the whole vitest suite (3,075 tests) and quint test of the monitor controls pass.

One pre-existing flake fixed in passing

test/formal-effects.test.ts's witness gate evaluates about 550 histories synchronously under vitest's default 5 s per-test timeout and has taken 3.0 to 5.2 s on hosted runners; it failed main's scheduled run 34833641404 and this branch's run 34904430717 with no semantic difference. The features gate already had a 30 s budget; the effects and local-clock gates now have the same. Two lines, no assertion changed.

Review before Codex

Two targeted local reviewers ran on the first head (a Quint reviewer that built an old-versus-new reached differential over every prefix of every control fixture, all single and double mutants, and 4,000 random traces with no disagreement, and a runner reviewer that caught the check-lane-versus-generation-lane mislabel and the startup masking). Then review-loop ran in report mode with seven lanes plus a two-stage holistic audit on 174807e. Its accepted findings and what changed:

• holistic-1 (defect, high): the gate omitted trace output and passed while the kernel views cannot run the lane's real command. Reproduced independently (rc 134, heap out of memory, zero traces; 7 GB peak with a 12 GB heap). Now measured and recorded as described above; the parity claim is withdrawn.
• holistic-2, architecture-1, reliability-1: a ratio violation aborted the pilot before any correctness evidence. Now recorded and raised at the end.
• performance-1 (medium): the README attributed the remaining cost to kernel state; the frozen-monitor measurement shows it is the monitor. Attribution corrected and measured every run.
• holistic-3 (medium): the gated ratio is flattered by a 2× property-cost asymmetry. Property cost per side is now recorded and the README quantifies it.
• simplicity-2: the echo-only invariants option is gone; each side carries the invariants its runs used.
• tests-1: nothing exercised a step after a script completes. A control and a one-step extension of the tracked-layers history now do, in both ports.
• Interleaved repetitions, a README note on which direction the witness lint enforces, a fixture comment on non-shrinking call lists, and the kernel-pilot job timeout raised to 30 minutes for the added measurements.
• simplicity-1 (replace the scripts with a capped 10-step prefix) was declined: same measured cost, +3.5% ITF per state in exactly the dimension holistic-1 identifies as the blocker, and the scripts keep each input next to its expectation. The README no longer justifies them by speed.

Then review-loop ran in until-clean mode on the result, three rounds of seven fresh lanes each plus the two-stage holistic audit and a plan critic per round (about 1.3M subagent tokens and 30 minutes per round):

• Round 1 (a9cee75 → 0eaea8f): the pilot's copy of the lane command had drifted (no --verbosity, hard-coded threads), so run-models.mjs now exports the builder both use, pinned literally; every cost measurement's failure is recorded and raised only after the correctness evidence; a generation attempt records how it ended (completed, violation by Quint's own marker, aborted, failed) and its timeout; parity requires time and bytes within generation.maxRatio; the frozen-monitor record reuses the pairing comparison; the two witness expectation types became one polymorphic Expect; report schema 2; job timeout raised.
• Round 2 (0eaea8f → 7370a49): I had documented a "lane's 600 s ceiling" that does not exist (the lane has only its job timeout) and derived a worst case the per-process timeouts cannot give; both corrected, the kernel attempt's timeout capped at the original's ceiling. Sampling violations name their run and report; the heavy measurements moved after the histories, replays and fault checks; the frozen-monitor run is interleaved with the gated pairing; three controls close test gaps (label accumulation, the writes expectation, the parity time arm); dead optionality removed; README numbers all from one recorded check.
• Round 3 (7370a49 → ac03fd1): three low improvements, fixed without a fourth review by your choice: generateHistory restores the model it rewrites instead of two call sites doing it; the generation record probes the node that quint runs under (version, heap limit, memory, options) so a parity flip is attributable to state shrink rather than a runner change; the witness checkpoints assert every credited label is still recorded at the final state; three README sentences tightened.

Correctness and tests came back clean in rounds 1 and 3; performance, reliability and contracts were clean in round 3. Two follow-ups were filed outside this PR: the witness gate re-parses its corpus three times (the cause of the 5 s flake), and the memory note for formal/README.md, which sits in the source-audit ledger.

Not in this slice

Shrinking the kernel's exported state (or changing the lane's configuration for kernel-based profiles) so the generation command completes; carrying the originals' properties in the kernel views; making the monitor's per-step bookkeeping cheaper; preserved-corpus replay through the kernel views; routing deadline judgments through cache-rules; moving the layers encodings out of the kernel; the eight dropped layers invariants; and the receipt-based independent fence check. The first three are new #165 work items from this review; the rest are slices 5 and 6 of the sequence in #165.