Repository navigation
Promote 80 orphan TestClaim predicate files to executing witnesses; 35 parse-reaching claims declared as residue, not enrolled - #8505
Merged
Conversation
…asses to executing witnesses Floor discovery is MARKER-keyed: v2.workflow.floor_naming_hygiene floor_discovery_line_starts_test_decl admits a line only if it starts `test fn ` or `test data `, mirrored in cli_run.rs witness_file_from_source. The TestClaim corpus is TYPE-keyed and marker-free -- `test data <x>: TestClaim` occurs ZERO times corpus-wide -- so the two populations are disjoint by construction and no TestClaim row has ever been a floor unit. Measurement grain is grep over col-0 declarations, stated as such: ~686 rows across 170 modules, 180 of the 218 modules naming TestClaim declaring no test decl at all, and 379 rows referenced exactly once corpus-wide (their own declaration). THE APPARATUS WAS INERT TOO, and that is the sharper half. An evaluator exists (v2.compiler.05_eval run_test_claim). Its roster -- v2.test.manual.manual_corpus_roster manual_corpus_node_subject_rows -- had SIX members, and the runner (v2.test.workflow.testclaim_corpus_runner) plus all four nat_semiring rung eval modules declared zero test decls. Nothing drove any of it. Six files, 63 top-level declarations, ZERO references from outside the island: measured by name, not by import, because imports do not bind in this substrate. Deleted with it, because they are the same weed above the waterline rather than separate finds: v2.workflow.bootstrap's BootstrapEvaluatorCorpusHarnessEntry, whose well-formedness witness compared symbol literals to the same literals it had just constructed the record from, and v2.workflow.cli in full -- a modeled CLI route surface whose every declaration and whose module path had zero references anywhere. Their ci_layer_roots strict-resolve exclusion rows go with them under that note's own stated trigger, "a row that excludes nothing is dead weight, delete it". EIGHT SPECIMENS PROMOTED, one per class, each already carrying the assertion as a nullary `fn () -> Bool` wrapped in a claim that decided nothing. Promotion is `fn` -> `test fn`, deletion of the `_claim_rhs` glue and the inert row, an import prune, and the rename the sidecar rule requires (floor_test_marked_decl_allowed_in_entry admits a test-marked decl only in a *_test.dag entry). Checked before renaming, not after: none of these module paths appears in gunbc.witness_deferral_freeze or in floor_expected_red, so nothing joins against a frozen row. Two tautologies fell out and are recorded rather than swept: claim_pipeline/normalize's CompilesClaim had input and expected_value bound to the same node, and the bootstrap harness witness above. Both were incapable of failing. NOT DONE HERE, deliberately. The remaining ~80 predicate-bearing orphan files are not promoted until each class has an executed discrimination receipt -- a fixture mutation that drives the promoted row RED. A predicate that executes is not yet a predicate that discriminates, and promoting an assertion that cannot fail rebuilds the defect one rung up, wearing the floor marker that makes it look fixed.
Correcting my own promotion in the previous commit, before it lands rather than after.
`compose_assoc_lhs` and `compose_assoc_rhs` are nullary and return Bool, which is the shape
the promotion keys on, and they are NOT assertions: each returns the applied composed patch
value, and both evaluate to `false` on an unmutated tree. Promoting them enrolled two rows
that were red on arrival and that no mutation of the function under test could ever make
red for the right reason -- `apply(base: true, P)` is false exactly when P is
`Override{false}`, which is what today's right-biased compose already produces for both
bracketings.
The assertions in this file were the ten `data witness_*: Bool = <expr> == <expr>` rows,
inert in exactly the way the TestClaim rows are: an authored comparison with no executing
consumer. Those are promoted; the two value-computations are demoted back to plain `fn` and
are now read only by `witness_associativity`, which is the row that actually compares them.
The dead Node-encoding trio (fp_ok, fp_pass_node, fp_fail_node) goes with the claim era it
served.
THE GENERAL LESSON, which governs the remaining 80 files: nullary-and-Bool is a SHAPE, not
a semantics. A mechanical sweep keyed on it enrolls value-computations beside assertions,
and the two are indistinguishable until something executes them. Promotion is therefore
per-file with the predicate read, never a regex over the corpus.
Population note, measured at grep grain so the scope is not overstated: 182 col-0
`data _: Bool =` rows exist corpus-wide and 131 sit in modules with no test decl, but only
14 carry a comparison operator -- ten of them in this file. Most such rows are configuration
flags, not orphaned assertions, so this is a small class and not a second TestClaim.
…ecuting it is how we found out
The one FAIL in the floor run on the previous head:
`apply_lens_enforce_projection_claim_holds returned Bool(false)`. Root-caused rather than
quarantined, and the defect is in the WITNESS, not in the lens.
`v2.std.node_query` `find_named_child` descends named children only when the node's
connective is `Conj`; every other connective falls through to a refusal, because an Atom is
a leaf. `projection_test_root` was authored as `Atom { identity: ^projection_test_symbol }`
carrying a `Named` edge -- a leaf with a child. So `subterm_at` could never reach
`projection_test_section`, `apply_lens_enforce` refused at its first step, and the claim's
`Rejected => false` arm answered. The root is now `Conj`, which is what a node with named
children is. Nothing in `v2.lens.application` changes.
This is the whole argument for the promotion, in one row: the assertion was authored, was
wrong, and sat in the corpus reading as coverage for as long as nothing executed it. The
floor found it in the first run that could.
DISCRIMINATION RECEIPTS, executed on probe/wise-bat-141-discrimination (runs 32209722310
and 32209718874), one subject-side mutation per class, predictions recorded in that
branch's commit message BEFORE the run:
loop_linear_claim_holds RED under a retargeted bound edge
conj_positional_only_no_fact_claim_holds RED under a changed connective
body_lowering_emit_args_are_operands RED under a swapped operand -- and ONLY
that one of the file's four, as predicted
spine_normalize_accepts_well_formed_sugar RED under a changed sugar rule
spine_normalize_dissolves_interior_service_sugar RED with it, as predicted
near_miss_vacuous_not_parallel_claim_holds RED once the two coverage-defect rows are
made equal -- so the distinctness it guards
is real
exponential_dominates_polynomial_claim_holds RED under an inverted symbolic_cost_dominates
Predicted collateral from that last mutation, confirmed: polynomial_dominates_linear (called
certain), nested_cost_projection and nested_complexity_projection (called likely). Two more
red that were not predicted -- lens_application_synthesis_gap_polynomial and
..._enforce_rejection -- which is further evidence the mutated arm is load-bearing. Three
predicted-likely rows stayed green, consistent with the same-class short-circuit named in
the prediction.
The probe also confirms by execution the derivation behind the previous commit:
compose_assoc_lhs and compose_assoc_rhs are RED there, on a branch that predates their
demotion. They were never assertions.
WHAT IS NOT ESTABLISHED, stated because a receipt that does not name its own gap is the
thing this PR is about: apply_lens_enforce_projection_claim_holds has NO discrimination
receipt. Its mutation was red on both branches, because the row was already red for the
fixture defect above -- a mutant of an already-failing row proves nothing. It is green now
and its sensitivity is untested; it earns a mutation in the next sweep, against a green base.
…oot-cause every first-execution red Second half of #8497. 85 orphan files censused (grep-grain: column-zero TestClaim rows + nullary Bool predicates + zero test decls); 82 transformed per-file with the predicate read — fn -> test fn on genuine assertions, TestClaim rows and glue deleted, imports pruned, *_test.dag renames — 2 held (externally-consumed claims already executing), 1 resolved by deleting its vacuous claims (coverage already lives in its executing sibling). Every promoted file executed locally through claim_batch with explicit rosters and --eval-budget-ms 1552 before this commit: 231 PASS / 38 FAIL first sweep; all 38 root-caused, none quarantined. Subject defects fixed at the authority, each found by first execution: - target_model target_type_expression_spelling projected the surface marker, not the spelling (sole consumers: the new witnesses) - 06_translate collection projections carried the collection surface where the instantiation surface belonged; every projected Vec/Set wire refused at serialize - v2.std.node bag_hash_digest sorted whole hash records (interpreter comparator absorbs records to Equal), so the bag digest was order-sensitive - go keyword lex rules were unsatisfiable (KeywordPattern with trailing-space texts); func/return lexed as idents Witness defects fixed in witnesses (stale fixtures, head-position pins on FrontierAccepted-threaded rejections, a Nat/Int cross-representation == straddle, occurrence-vs-decl grain, closure ptr-equality, two stray braces). 22 rows demoted to plain fn with receipts: 8 assert digest behavior above the i64 wrap ceiling (fixtures evaluate to 0 under the interpreter's silent wrapping multiply), 4 bootstrap_footprint rows unexecutable (Int code points in Atom.identity vs string-only atom_identity_hash), 5 assert branded fixture-vocabulary identities unreachable from the lexeme-stamping parse, 4 assert refusals that were never the subject's contract, 1 exceeds the 1552ms floor budget running compile_ingest_staging (smallest possible specimen; needs a long-lane consumer). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
6 tasks
…behind; re-ground their eval gates on the discriminating controls The whole-corpus floor preparation refused on d3860eb: lens_parallelism/ lens_idempotency family_receipt.dag each aggregated exactly one TestClaimRun row that the evaluation-island deletion removed (the per-entry claim_batch closure never loaded these files, so the local sweep could not see them — the bare-name/whole-corpus gap the parent lane warned about, hit through a different door). The aggregates' only consumers were the two family-eval floor witnesses, whose gates conjoined the (now-subjectless) run tally with live discriminating controls. The run rows' coverage executes as the promoted test fns in data_dependency_test.dag / write_effect_test.dag, so the gates keep only the controls; the TestClaimRun tally machinery and both family_receipt files are deleted. Both witnesses re-verified green by execution through claim_batch. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
1. v2.lens.synthesis called complexity_lens bare with no import; the name
resolved under claim_batch's per-entry closure by pool coincidence and not
under the floor's whole-corpus prepared subject (no such function at eval).
Restore the explicit import; synthesis_no_tech_diagnostics_non_empty PASSES
by execution locally.
2. The 33 v2.test.manual.body_lowering_{match,normalize_add,projection_call}
rows red only under the floor subject: runtime PatternMatchFailure
(non-exhaustive) on the PreparedGrammar match inside v2.compiler.parse
parse_module_prepared — the scrutinee is a PreparedModeled record whose tag
prints as invalid-symbol, the same record/variant identity-reconciliation
family as the sixteen compute_board witnesses in gunbc#8449, residual on the
parse_module vertical these rows are the first floor consumers of. All 24
fns of the largest file PASS by execution under per-entry claim_batch on the
identical tree, and the same errors appear on the pre-#8487 probe tree, so
the defect is floor-subject evaluation, not the witnesses and not #8487.
Quarantined at identity grain in floor_expected_red chunk_14 with the root
cause and un-quarantine trigger recorded; three of the rows additionally sit
at the 1552ms ceiling and flip with the same fix.
Also merges origin/main (merge commit 8b41bdb, no file overlap).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Contributor
Discrimination receipts — one subject-side mutation per class, predictions written before executionTwo probe branches (never merged) carried one narrow subject mutation per class, with the predicted RED set written into the probe commit message before any execution of the mutated tree. CI executed the full required floor on each.
Baseline held on both probes: 306 legacy expected-red held, 0 stale. Base-red rows on the probe trees (the body_lowering/synthesis classes root-caused separately below) are excluded from the joins. Probe A — 23 of 27 classes fired exactly as predictedClasses 1–3 (go/kotlin/typescript lex/source mutations), 6 (body_producer dispatch), 7 (application subterm_at), 8 (fact_density gate reason, plus all four predicted-likely siblings), 9 (coverage discriminant key), 11 (synthesis gap reason), 12 (registry uniqueness, both rows), 13 (discrimination non-perturbation, both rows), 14 (idempotency verdict, plus predicted collateral Probe A — 4 findings (predicted-certain red stayed green)The mutations are verified present on the probe tip (diffed a831483..f166dd5). Passes are not printed per-row by the floor, so these four rows passed under their mutation — vacuous-green findings, each a fixture-discrimination gap, not a subject defect:
Probe B — all 5 classes discriminate
The two base failure classes on run 32225493043 (fixed in c4d0e26)
|
Contributor
Probe C — the owed receipt, and why enrolled-and-quarantined beats orphanedProbe C:
|
…failed Probe A class 19 mutated v2.std.text fold_source so the step applies even after is_done turns true, and predicted the witness RED. It stayed GREEN. The mutation reached the subject; the fixture could not see it. src_abc is three bytes and count_three_algebra stops at three, so the fold runs out of input on exactly the step the stop would have fired: an algebra that ignores is_done entirely produces the identical count. The assertion count == 3 && done was therefore true under both the correct and the broken rule — the witness asserted a coincidence between its fixture length and its stop threshold, not the stopping behaviour it is named for. Two spare bytes past the stop make it discriminating. Verified by execution, both arms, on this tree: unmutated PASS fold_source stepping past done FAIL This is the vacuous-green class the discrimination protocol exists to find: a row that executes, passes, and establishes nothing. Three sibling findings from the same probe pass are still being measured and will be fixed or pulled the same way — none stays documented-but-promoted. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Probe A class 10 changed Disj composition so an alternative keeps the FIRST
child's cost instead of the maximum, and predicted disj_max_claim_holds RED. It
stayed GREEN. (Its sibling disj_floor_projects_unit did go red, so the class
still discriminated — this row alone did not.)
The fixture's cheap alternative was a bare Atom, and base_cost_for_connective
gives an Atom zero. Every rule that could be wrong here agrees on a zero first
operand: taking the max of {zero, linear} and keeping the first non-zero
alternative both answer linear. So the witness asserted a value that the correct
and the broken composition compute identically — it discriminated nothing about
alternatives, which is the one thing its name claims.
Wrapping the cheap arm in a Transform makes it cost unit: still strictly
dominated by the Cardinality arm, so the assertion is unchanged and still true,
but a first-child-wins rule now answers unit. Verified by execution, both arms:
unmutated PASS
alternatives keep the first child FAIL
Second of the four vacuous-green rows from the probe pass; fold_source was the
first. Two remain under measurement.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Contributor
Sequencing: the 33 quarantined rows are #8540's end-to-end control, and come out rather than mergingUpdate to the quarantine described in the previous comment, because the root cause was found while this PR was in flight. #8540 fixes it at the root. So the quarantine is now wrong and will be removed, not merged. Those rows pass on #8540's tree, and the floor refuses on a stale roster row exactly as loudly as on a failing one — They are also the only end-to-end control #8540 has, which is the better reason to keep them enrolled. That PR's boundary test proves the translation round-trips through the two memo functions; it cannot prove that One further finding this PR will not carry. The remaining budget-refused rows are a separate defect with its own merged precedent: the one-time grammar preparation is billed to whichever witness reaches |
Contributor
Correction: two of the four "vacuous-green" rows were mis-aimed predictions, not vacuous rowsThe receipt comment listed four probe-A classes whose predicted-certain row stayed green, and called them fixture-discrimination gaps. Having measured each rather than left the reading standing, two were vacuous rows and two were my own predictions aimed at the wrong code path. Correcting it here rather than leaving the stronger claim on the PR. Genuinely vacuous — fixed at the fixture, both arms executed:
Not vacuous — the mutation never reached the row's path:
Net: 25 of 27 probe-A classes discriminated as predicted, 2 rows were genuinely vacuous and are fixed, and 2 predictions were mine to correct. Nothing is documented-but-promoted. |
Contributor
CI status on
|
| run | head | held red | budget-refused |
|---|---|---|---|
| 32230093162 | c4d0e26 |
336 | 3 |
| 32233910347 | 49ac2c3 |
329 | 10 |
Same 339-row roster, same body_lowering code, membership of the over-budget set moved from three rows to ten. That is the third independent observation that the bill is positional — paid by whichever witness reaches parse_module first, not owed by any particular row — after the two-function local batch (first position kills a row that passes in second) and the earlier probe-run comparison. It is why these rows are not being demoted: demoting the victims hands the bill to whoever runs next, which run_required_floor's own comments record being chased down three times before the pattern was read correctly.
Both remaining blockers are sequenced behind #8540, deliberately. That PR fixes the root cause of the 33 rows (the cross-claim prepare_grammar memo serving Symbols across per-claim InterpContexts). Once it merges: main comes in, the chunk_14 quarantine comes out — the floor forces that, since it refuses on an enrolled identity that now passes — and the first-payer cost gets re-measured at both ends, first payer and steady state, because #8540 makes a memo hit pay translation it did not pay before and that lands on every claim. The remedy follows the measurement rather than the other way round.
This PR stays draft until that sequence completes.
…ver had one Adds lookups/hits/inserts to PrepareGrammarCrossClaimMemo plus a public snapshot getter, and deletes ParseTableMemoStats, parse_table_memo_stats_snapshot, and the three ParseTableMemo fields they were the only reader of. WHY THE COUNTERS: the memo's hit/miss pattern is currently extractable only by rebuilding the interpreter with eprintln and re-running the floor. That is what it cost to learn it the first time — an instrumented binary and two remote dispatches to answer a question a counter reports for free from any running floor. WHY THE DELETION IS IN THE SAME DIFF: ParseTableMemoStats had no consumer anywhere in the tree. Verified by enumeration, not by a summary: every mention of either symbol in the repo is the pub struct, the pub getter, and the construction inside that getter. Control — a symbol known to be consumed returns multiple files. The three ParseTableMemo fields were written at three sites and read only by the deleted getter, so leaving them would leave write-only accumulation; the cut takes them and their increments too. This is larger than the three declarations it looked like, which is why it is stated rather than folded in silently. THE ORDERING IS THE DIFFERENCE, not the code: these counters have a named consumer before they exist — a warm-time assertion that REFUSES when a lookup from a freshly built claim context does not hit. The deleted pair was built first and went looking for a question afterwards. Counter-before-consumer is how instrumentation becomes inert. Eviction resets the counters with the map, so they describe the current epoch: a lifetime total spanning an eviction would report a hit from a map that no longer exists. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…EFORE the run THE QUESTION: does a prepare_grammar memo entry stored by one claim get HIT by a later claim running in a separately constructed InterpContext? That decides whether a preparation-time grammar warm can be reached by claims at all. WHY THIS SHAPE: the subject is two claims, not nine thousand. Cross-context reuse needs one store plus one subsequent lookup; everything above that is cost with no additional discrimination. The whole required-floor fold was being run to answer it and was OOM-killed for it (exit 137, ~3 min in, still in preparation). BOTH ARMS, AND ARM A GATES ARM B. Arm A runs two claims in ONE context (reproduces claim_batch, expected HIT) and must observe a lookup pair, a hit and an insert. Arm B evicts, then runs the same two claims in two separately constructed contexts. If Arm A does not hit, the binary prints VERDICT UNREADABLE and exits nonzero WITHOUT reporting Arm B — because key instability and a harness that never reached prepare_grammar produce identical output, and a bare MISS is the one this lane would have acted on. PREDICTION, RECORDED BEFORE THE RUN so it can be wrong in public: Arm B HITS. Derived from source rather than guessed — evaluation_frame builds a fresh context per claim, but over scope.indexes.clone(), an Rc to the SAME PreparedScopeIndexes every claim in the scope shares. The memo keys on Rc::as_ptr of the prepare_grammar fn node, which lives in those shared indexes, so the pointer half is stable by construction. The HASH half is open: it depends on whether the hashed grammar value carries interner-dependent Symbols, which is gunbc#8540's subject and not this lane's to fix. A miss must name which half moved — identical pointer with differing hash is the hash half and routes straight to #8540; a differing pointer refutes the prediction above. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…rdict at the floor ceiling Eight rows enrolled by this PR were BUDGET-REFUSED on run 32246856637 at 1553-1568ms against a 1552ms ceiling — over by 1 to 11ms. The fold reported failed=0: no wrong answer anywhere in 9421 rows. What it reported is eight claims that produced no verdict at all. An enrolled row that budget-refuses is worse than an unplanned one. Enrollment asserts an expected verdict; a refusal preempts the verdict, so a content defect in those rows would be indistinguishable from the enrolled failure. That is the same coverage-shaped-but-not-coverage state this PR exists to remove, one step further along. CUT BY REACHABILITY, NOT BY THE OBSERVED FAILURES. Dropping the eight would have re-selected rather than removed: every claim in these three files reaches grammar preparation through a shared zero-arg helper, so the cheap rows in the same modules are cheap only because a prior claim already paid and they hit the call memo. A non-payer's measured cost is not evidence of what it costs AS a payer. The 574ms gap between the refused set and the ninth-most-expensive row looked like safety and is not — it is a distribution over rows that ran after someone else paid. Scoping instead by "can reach prepare_grammar" gives 35 claims across exactly 3 files, independently corroborated by those being exactly the 35 body_lowering rows over the 100ms warn in that run. THE ROWS ARE UNPROMOTED, NOT QUARANTINED. They return to being visibly uncovered data rows. Quarantining them in the expected-red roster instead would have marked them as covered while leaving them undecidable, which is the dodge this cut exists to avoid. chunk_14 is emptied and carries the residue declaration. RELEASE TRIGGER: the interner-independent hashing fix (adhoc-e78c4260-d3a). The first-payer cost persists because the cross-claim prepare_grammar memo cannot amortise it — its key mixes raw interner-local ordinals, so it is not content-addressed. Measured this session: three identical runs give one digest, and reversing only the order in which the same claims are named gives a different digest for the same grammar. The ceiling is NOT raised. It bounds the fold's memory, and removing it for a diagnostic run OOM-killed the runner three minutes in, twice. Clearing an 11ms overrun by moving that bound would be an absorbing fallback priced in the corpus rather than in the change. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…nd a dangling [[bin]] broke the build TWO DEFECTS, ONE SHAPE: an artifact whose justification lives somewhere other than the artifact. COUNTERS. b17a8e7 added lookups/hits/inserts and a snapshot getter to PrepareGrammarCrossClaimMemo, justified by a named consumer: a grammar warm in run_required_floor that refuses when a lookup from a fresh claim context misses. That warm was then suspended -- correctly, because the memo's key is not content-addressed (the digest mixes raw interner-local ordinals, so it depends on claim evaluation order), and a warm built on it would amortise nothing. Nobody re-examined what the suspension stranded. The counters stayed, their doc comment naming a consumer that no longer existed, and their only reader in the tree was an out-of-tree probe harness now also abandoned -- it OOMs the runner at full corpus preparation, 7.63GB of 7.86GB, and cannot be shrunk by excluding test paths because production lens modules import test modules. Landing them would make this PR self-contradicting: deleting one observable for having no consumer while adding another with no consumer. Reverted: the three fields, the public stats struct, the snapshot getter, both increment sites, and the eviction comment that explained counter semantics. A suspension is a re-review trigger for everything it justified. It does not only stop future work; it retroactively strands already-merged artifacts whose case rested on it, and nothing prompts the re-read because the dependent's own diff still looks fine in isolation. THE ParseTableMemoStats DELETION STAYS. It rests on evidence independent of anything dropped here: no consumer since it was written, and 9421 floor rows executed against that tree with failed=0, including every parse-reaching witness -- the population that would notice a damaged parse-table memo. DANGLING [[bin]]. Cargo.toml declared cross_context_memo_probe whose source file does not exist in HEAD -- deleted when the probe moved in-crate, manifest entry left behind. Any cargo build of this crate failed on this branch. It survived because CI builds no Rust (suite removed 2026-07-11, clippy 2026-07-08), and because cargo check --lib passes on such a tree: --lib never builds bins. cargo fmt is what refused. Verified fixed by a full cargo build --release -p v1-compiler, exit 0, bins included. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot
Bot
changed the title
briansrls
added a commit
that referenced
this pull request
Aug 19, 2026
…texts (#8505) (#8540) PREPARE_GRAMMAR_CROSS_CLAIM_MEMO cached prepare_grammar's raw Value result keyed only on (fn_node pointer, content_hash), with a clear-scope tied to the whole required-floor prepared-subject run. But run_required_floor builds a fresh InterpContext (fresh, empty SymbolInterner) per claim, so a Value cached under claim N's interner -- with Symbol indices meaningful only in that interner -- was served unmodified to claim N+1's unrelated interner. Matching against it either missed every arm or hit the wrong one, and PatternMatchFailure's Display then resolved the stale index against the wrong interner, printing the literal "<invalid-symbol>" seen in the 33 floor-only body_lowering_* rows quarantined in floor_expected_red chunk_14. Per-entry claim_batch never hit this because it keeps one interner live across an entry's claims. Fix: translate at the store/load boundary per the Realization pattern (DESIGN.md §4) -- de-symbolize to a Symbol-free PortableValue (raw strings) at store time while the producing ctx is still alive, and re-intern into the consuming ctx's own interner at load time. Closure/Fn results are refused from caching (fail-closed) rather than guessed at, since their Env chains aren't a content snapshot and prepare_grammar never returns them. Verified by execution: a new regression test builds two InterpContexts with different pre-interned decoy vocabulary (so a leaked raw Symbol index would resolve to the wrong name rather than accidentally line up), stores a Variant result under ctx_a, loads it under ctx_b, and asserts every tag/field name resolves correctly under ctx_b's own interner. floor_expected_red chunk_14 is unaffected here: the 33 quarantined rows from gunbc#8505 live only on the unmerged session/warm-boar-256 branch (commit c4d0e26), not on this branch or main. Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Sonnet 5 <noreply@anthropic.com>
Contributor
Status note: the residue's release trigger has since merged — this justification is openly pending, not silently stalePosting rather than editing, so the head and the existing approval are untouched. What changed after this PR went green. Two PRs merged to
So the residue section above, and the An obligation is outstanding and is recorded in Why it cannot be discharged before this merges — it is an ordering constraint, not a choice. The 33 rows are unpromoted on this head; they are plain data rows again. A floor run against One correction for whoever runs the follow-up. #8540's body describes this branch as carrying the 33 rows quarantined at commit The follow-up, after this merges: merge — sent from warm-boar-256 |
This was referenced Aug 19, 2026
Merged
This was referenced Aug 19, 2026
briansrls
pushed a commit
that referenced
this pull request
Aug 19, 2026
…dinals (#8565) * Fix cross-claim prepare_grammar memo leaking Symbols across InterpContexts (#8505) PREPARE_GRAMMAR_CROSS_CLAIM_MEMO cached prepare_grammar's raw Value result keyed only on (fn_node pointer, content_hash), with a clear-scope tied to the whole required-floor prepared-subject run. But run_required_floor builds a fresh InterpContext (fresh, empty SymbolInterner) per claim, so a Value cached under claim N's interner -- with Symbol indices meaningful only in that interner -- was served unmodified to claim N+1's unrelated interner. Matching against it either missed every arm or hit the wrong one, and PatternMatchFailure's Display then resolved the stale index against the wrong interner, printing the literal "<invalid-symbol>" seen in the 33 floor-only body_lowering_* rows quarantined in floor_expected_red chunk_14. Per-entry claim_batch never hit this because it keeps one interner live across an entry's claims. Fix: translate at the store/load boundary per the Realization pattern (DESIGN.md §4) -- de-symbolize to a Symbol-free PortableValue (raw strings) at store time while the producing ctx is still alive, and re-intern into the consuming ctx's own interner at load time. Closure/Fn results are refused from caching (fail-closed) rather than guessed at, since their Env chains aren't a content snapshot and prepare_grammar never returns them. Verified by execution: a new regression test builds two InterpContexts with different pre-interned decoy vocabulary (so a leaked raw Symbol index would resolve to the wrong name rather than accidentally line up), stores a Variant result under ctx_a, loads it under ctx_b, and asserts every tag/field name resolves correctly under ctx_b's own interner. floor_expected_red chunk_14 is unaffected here: the 33 quarantined rows from gunbc#8505 live only on the unmerged session/warm-boar-256 branch (commit c4d0e26), not on this branch or main. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * prepare_grammar cross-claim memo: key on symbol text, not interner ordinals eval_recompute_value_hash/eval_recompute_arg_key mixed raw Symbol ordinals (type_name.0, variant_name.0, per-field-name .0) into the content hash used as the cross-claim memo key. The memo is a thread_local outliving any single InterpContext, and ordinals are assigned in per-context encounter order, so two semantically distinct values from two independently-interned contexts could be assigned the identical ordinal pattern and alias onto one memo entry -- silent wrongness one level up from the value-transport bug #8505 already fixed (a wrong grammar served for a correct-shaped but differently- named key, not just a missed/duplicated computation). Threads &SymbolInterner through the one eval_recompute_* pipeline (used by both the cross-claim memo and the diagnostic recompute trace) so Record/ Variant type names, variant names, and field names hash by resolved text. Also fixes a RefCell double-borrow the interner threading introduced: the try/store_cross_claim_pure_memo helpers now scope the interner borrow to just the key computation, since value_from_portable_ctx interns new symbols into the same context. Two new regression tests construct two contexts whose independent interning order assigns colliding ordinals to different strings, proving the memo no longer aliases across them. * Fix RefCell double-borrow: free_monoid_to_vec re-entering ctx.symbols during hash eval_recompute_value_hash/eval_recompute_key hold an immutable ctx.symbols.borrow() (interner) across the whole memo-key computation. A Value::Map arg's CanonKey::hash routes through value_hash, which for a String/List/Variant key calls free_monoid_to_vec -- and that function unconditionally re-interned its well-known Cons/Empty/head/tail symbols via ctx.sym() (a mutable borrow), panicking with "RefCell already borrowed" whenever it was reached while the interner borrow above it was still held. This crashed the whole required-floor claim_executor process mid-fold on PR #8565's CI run (32294557068), not a single claim refusal. Add SymbolInterner::get, a read-only lookup, and free_monoid_ctx_syms, which tries the normal mutable intern first and falls back to a read-only lookup when the interner is already borrowed elsewhere on the stack. A free-monoid-encoded value must already carry interned Cons/Empty/head/tail symbols, so the read-only fallback is sufficient; failing it means the value genuinely isn't a free-monoid encoding, which is the same "not a match" outcome the existing code already handled via monoid_syms?. * Pre-intern free-monoid symbols: close the read-only fallback's silent narrow warm-boar-256 flagged that free_monoid_ctx_syms's read-only fallback (975f2b1) could report a genuine Cons/Empty value as "not a list" if Empty/Cons/head/tail happened not to be interned yet in that context -- a None indistinguishable from the real not-a-monoid case, i.e. DESIGN Sec5's empty-observation narrow (⊥-as-answer conflated with ⊥-as-ignorance) inside the fix for a silent-wrongness class. Close it at construction rather than detect it at the call site: pre-intern the four well-known symbols in over_scope_indexes, so every InterpContext (including required-floor's fresh-per-claim contexts) guarantees the read-only lookup can never miss. The lookup helper now panics loudly on a miss instead of returning None, since after pre-interning a miss can only mean the invariant itself broke, not that the value isn't a free monoid -- refuse loudly per Sec5, don't widen or narrow silently. Update three tests' stale "ordinal 0/1" comments (no longer true once the four well-known symbols are pre-interned first) and add two regression tests: one proving free_monoid_to_vec resolves a real Cons/Empty chain's symbols correctly (not just non-panicking) while an immutable ctx.symbols borrow is held on the stack, and one exercising the same shape through the cross-claim memo path with a Map key. --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Sonnet 5 <noreply@anthropic.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 19, 2026
… floor refusal The floor ran end to end for the first time on this branch and refused with one precise cause: ExpectedRedIdentityDidNotExecute count=1, naming v2.lens.non_fold_residue.non_fold_residue_clean_holds. That identity is a plain `fn`, not a `test fn`, in a module with no test roots, so discovery cannot produce it and the enrollment is stale by construction. Main had already removed the row (#8505 / #8581, promoting orphan TestClaim predicate files to executing witnesses); this branch was simply behind. Absorbing main is the fix, not an edit of mine to the roster. Five conflicts. `src/v1/04_infer.dag` carried three. One is main's new `scalar_shaped_builtin_method_arg_type` plus the `is_lambda_expr` it sits above -- taken as main authored it, with `Node` re-qualified, because the cut is a mechanical transformation of whatever content lands, never a reason to drop it. The other two are the same line seen twice: main changed the argument from `a2` to `a2_qualified` while this branch qualified the callee to `v1.compiler.infer_env.symbol_index_insert`. These are edits to different parts of one call, so the resolution is both -- taking either side alone silently discards the other's work, and neither would have failed loudly. The three `body_lowering_*` manual tests are renames on main (`body_lowering_match.dag` -> `body_lowering_match_test.dag`) that also convert `fn` to `test fn` and drop the hand-authored TestClaim rows -- the promotion to executing witnesses. Taken whole from main and re-cut, the same interval rule the fifth integration used: 169 names qualified across the four files that arrived carrying imports. One modify/delete: `long/transport_script_wall_compile_red_test.dag`, deleted on main and modified here only by the cut. The deletion stands; a file main removed is not resurrected by the fact that this branch reformatted it. Guards green on the merged tree: surviving_import 0, qualified_kernel_type 0, qualified_let_binder 0, local-shadowing detector 0 over 3,760 declared modules.
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 19, 2026
Seven errors, one name, one file. `Symbol` is declared in `v2.std.node` and this file used it bare -- it arrived from main in the #8505 promotion, and the cut's driver is the import block, which never listed `Symbol` because it was resolving ambiently. The cut removes the ambient pool, so a name no import ever mentioned is exactly the name the driver cannot see. The other three files promoted in that batch were checked the same way rather than assumed clean: every remaining bare capitalised identifier in them is a variant head (Present, Absent, Accepted, Rejected, ParseSubtreeFound, ParseSubtreeAbsent, Named, Positional) or a constructor that resolves through its coproduct, and pattern heads must stay bare -- qualifying one discards the scrutinee's instantiation. The floor agrees: it reported Symbol and nothing else across all four. Sibling files in the same directory already spell it `v2.std.node.Symbol` 82 times against 9 bare, so this is the established spelling, not a new choice.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Promote the remaining orphan TestClaim predicate files to executing witnesses
Second half of #8497 (its "Not done here, deliberately" section). Base note: this branch is cut on top of
session/wise-bat-141(#8497), which is still open — the first ~21 files of the diff (renames in lens/cost, lens/coverage, lens/fact_density, the island deletion) are that PR's content, not this one's. When #8497 merges, a main re-merge will shrink this diff to only this lane's work.Census (grep-grain, rebuilt rather than inherited)
Instrument: column-zero
data X: TestClaim+ column-zerofn name() -> Bool+ zerotest fn/test datadecls, overdag/+src/v2/at the merge base. 85 files / 265 nullary Bool predicates (parent's 80/256 at a slightly different grain; difference stands, both stated).What was done, per file — predicate READ, never a regex
fn→test fn;data: TestClaimrows,_claim_rhs/bool_nodeglue andmanual_claim_anchorcalls deleted; imports pruned; files renamed*_test.dag(module decls unchanged). Where an assertion lived only inline in a deleted claim row, a minimaltest fnwith the claim's exactok:expression was authored (sg2 files, language_model files) — transcription, not new semantics.src/v2/lens/effect/effect_depends_on.dag(its claim row is imported and already executes vialens_effect_family_eval_test) andsrc/v2/test/claim/grounding_go/sg_claims.dag(its subject/run rows are consumed byfamily_receipt.dag/subject_roster.dag; needs a coordinated three-file change).round_trip/source_authority_contract.dag— its two claims were vacuous (input ≡ expected); the seven contract fns already execute via the pre-existing siblingsource_authority_contract_test.dag.extdeps/language_modelfiles are pure test modules (modulev2.test.*, zero importers) overv2.lens.leaf_model_verification; the rest ground into std subjects (node_query,content_hash,refinement,model_core,text.fold_source).Executed before push: every promoted file, floor budget applied
All promoted files ran locally through
claim_batchwith explicit rosters and--eval-budget-ms 1552(the floor'srequired_floor_claim_budget_ms), using binaries built from this tree. This is a filter, not the floor oracle — the floor folds one whole-corpus subject; bare-name binding and annotation placement can still differ (bare-name multi-declarer census over all promoted files: zero real collisions).First full sweep: 231 PASS, 38 FAIL, 0 no-result. Every FAIL was root-caused (never quarantined); final state: all enrolled rows PASS. Breakdown of the 38:
Real subject defects found by first execution (fixed at the authority)
v2.std.compilers.target_modeltarget_type_expression_spellingreturned the form's surface marker, not the spelling — a misnamed projection whose only consumers were the promoted witness rows. Now projects the first positional child's atom identity (the actual spelling). Found viarust_r3_internal_emit_coupling_fixture_wired.v2.compiler.06_translateproject_free_monoid_via_vec_choice/project_set_collection_type_node— the same surface/spelling conflation one level up: projected Vec/Set wires carried the collection surface where the instantiation surface belonged, so every projected collection wire refused at serialize. Fixed;sg_collection_free_monoid_vec_rc_projection_holdsnow provesVec<Rc<Node>>end to end.v2.std.nodebag_hash_digestsorted by whole hash records; the interpreter's comparator falls back to Equal on records, so the sort was a silent no-op and the "bag" digest was order-sensitive. Sort key now the digest hex field;tcc_cache_diagnostic_tail_permutation_claim_hash_invariantgreen.v2.extdeps.languages.gokeyword lex rules usedKeywordPatternwith trailing-space texts, making them unsatisfiable —func/returnlexed as idents and the go parse witness could never have passed. Switched to literal rules (emission spelling byte-unchanged).Witness/fixture defects (fixed in the witness, subject untouched)
Stale operands in
body_lowering_variants(fixtures had migrated to int-literal nodes); head-position pins onvalidate_then_compilerejections that the documented FrontierAccepted diagnostic threading prepends to (three files; restated as reason containment); a fixture invalidated by laterfact_densityroster enrollment (rejecting_lens_blocks_before_compile); a Nat-coproduct vs native-Int==straddle that tripped the interpreter's fail-closed cross-representation guard (fact_bundle_named; restated as a structural match, density still exactly 2); a label-less record golden the serializer cannot produce (sg2_mode2_conj); an occurrence-grain vs decl-grain miscount (anchor_partials, now pins the occurrence contract== 2); closure-bearing record==(ptr-equality) inmodel_core_anchor, restated over comparable Node projections; two stray braces from glue deletion (caught by the sweep's first parse).Wrong assertions — demoted to plain
fnwith receipts, retirement candidatesbody_lowering_normalize_add: assert branded fixture-vocabulary atom identities (^dag_binding_param_x) on a live-parsed tree; the grammar's lexeme-stamping contract makes those identities unreachable from source. Equivalent coverage survives in the passing lexeme/consistency rows.add_body_arrow_with_atom_body_rejects: asserts rejection ofDirectAtomBody, a formv2.std.nodeexplicitly admits (classification + eval entry).sg2_mode2_arrow_serialized_text_matches_expected(arrow text under a use-site-ownership catalog whose lookup correctly refuses uncovered carriers — property already proven in the projection file),sg2_mode2_gap2_*pair (asserted a refusal that was never the contract, and a lex-only spelling channel that does not exist),sg2_rust_add_projection_absent(the "no projection" state it documented is dead — the bundle has carried the projection edge for months).Genuine frontier findings — demoted with receipts naming the re-promotion trigger
test_claim_cache_digest_sensitivity): not digest aliasing — the interpreter'sIntisi64with silent wrapping multiply, so every256^k, k≥9fixture evaluates to literally 0 and the tests compared 0 with 0. The digest's over-ceiling/limb-exhaustion arms are unreachable from any representable runtime Int (dead code on this realization). The §5 defect is the silent wrap itself — a frozen-v1-interpreter matter, reported not patched.bootstrap_footprintmust content_hash a closure embeddingrust_target_model().bundle, whose semantic-decl string encoding stores Int code points inAtom.identity; the string-onlyatom_identity_hashintrinsic refuses. Cross-module encoding migration required (semantic_decl_emission+target_model); re-promotion trigger recorded in-file.nominal_distinct_control_compiles_okrunscompile_ingest_staging(measured 1553ms CPU vs the 1552ms floor budget) on the smallest possible crossing specimen — the cost is the compile pipeline's fixed cost. Demoted; needs a long-lane executing consumer. Not relocated, no exemption added.Floor arithmetic
246 enrolled decls now stand in this lane's transformed files (242
test fn+ 4test data, grep-grain over the changed set, after the 22 demotions above). Rosters checked: no promoted module path joinsgunbc.witness_deferral_freezeorfloor_expected_red.Discrimination receipts
Per-class subject-side mutations with predictions-before-push run on separate probe branches (deliberately red, closed unmerged) — see the follow-up comments on this PR for the per-class receipt table as probe runs complete.
Declared residue: 35 claims across 3 files stay unpromoted
This PR promotes the orphan TestClaim files except a cohort of 35 claims in 3 files, which stay as unplanned data rows. Naming them, why, and what releases them.
The cohort — every promoted claim that can reach
prepare_grammar:src/v2/test/claim/manual/body_lowering_match.dag(7 claims)src/v2/test/claim/manual/body_lowering_normalize_add.dag(25 claims)src/v2/test/claim/manual/body_lowering_projection_call.dag(3 claims)Why they are not promoted. Enrolled, eight of these rows were BUDGET-REFUSED on run
32246856637at 1553–1568ms against the 1552ms ceiling — over by 1 to 11ms. The fold reportedfailed=0: it found no wrong answer in 9421 rows. What it found was eight claims that produced no verdict at all. Enrollment asserts an expected verdict; a budget refusal preempts the verdict, so a content defect in those rows would be indistinguishable from the enrolled failure. That is the same coverage-shaped-but-not-coverage state this PR exists to remove, one step further along.Why the cut is the cohort and not the eight that failed. Every claim in these three files reaches grammar preparation through a shared zero-arg helper (
body_lowering_normalized_moduleandbody_lowering_parsed_fn_decl;body_lowering_parsed_treein the match file). The cheap rows in the same modules — 22 of them at ~200ms — are cheap only because a prior claim already paid and they hit the call memo. A non-payer's measured cost is not evidence of what it costs as a payer. Dropping only the eight would have promoted the next-arriving rows into the identical refusal. There is a 574ms gap between the refused set and the ninth-most-expensive row in the whole fold, and that gap is not safety — it is a distribution over rows that ran after someone else paid.Scoping by reachability instead gives 35 claims across exactly 3 files. Independent corroboration: those are exactly the 35
body_loweringrows over the 100ms warn in that run, a figure not used to construct the cohort. The boundary was checked in both directions —body_lowering_variantsandarrow_body_form_witnessreach no parse call and stay promoted, so this is the family by reachability, not the family by name.Unpromoted, not quarantined — and the distinction is the whole justification. These rows go back to being visibly uncovered. Quarantining them in the expected-red roster instead would have marked them as covered while leaving them undecidable, which is precisely the dodge. Over-cutting leaves rows visibly uncovered, which is recoverable; under-cutting re-enrolls undecidable rows, which is the state being avoided.
Release trigger. The first-payer grammar cost persists because the cross-claim
prepare_grammarmemo cannot amortise it: its key is not content-addressed — the digest mixes raw interner-local ordinals, so it depends on claim evaluation order. Measured this session: three identical runs give one digest (50ba68379e60c82b×3), and reversing only the order in which the same claims are named gives a different digest (832d3cbf50c5df91) for the same grammar. Impurity observed; the false-miss direction observed; the false-hit direction remains inferred-structural from the ordinal aliasing. The cohort becomes promotable in one motion once the interner-independent hashing fix lands (dashboardadhoc-e78c4260-d3a).The ceiling is not raised. It bounds the fold's memory; removing it for a diagnostic run OOM-killed the runner three minutes in, twice. Clearing an 11ms overrun by moving that bound would be an absorbing fallback priced in the corpus rather than in the change.
Verified by execution, and the delta is the evidence
Run
32249852401,witnesses, pass:Against the failing run, and this reconciles exactly:
Of the 35 cohort claims, 33 were enrolled and 2 were passing; of the 33 enrolled, 25 were HELD as expected-red and 8 were BUDGET-REFUSED. 25 + 8 + 2 = 35, and
plannedfell by exactly 35 — every removed claim lands in exactly one bucket, with no residue in either direction.The reconciliation matters more than the zero. A cut of a hundred rows would produce an identical
budget_refused=0; only theplanneddelta distinguishes a correct cut from a merely green one. And no refusal survived, so no next-arriving row became a first payer in place of the eight — the reachability predicate found the whole payer-capable population rather than a sample of it, which is what makes the wide cut justified rather than merely cautious.What the floor run added after the promotions landed
Two failure classes appeared on the first floor run and both are fixed: a missing import in
v2/lens/synthesis.dag(a bare-name reach that the local batch could not see, because the floor folds one whole-corpus subject), and two genuinely vacuous rows whose fixtures could not fail —fold_sourcestopped at the same index as its source length, anddisj_max's cheap arm was a bareAtomwith zero cost. Both were given fixtures that execute both arms and were verified PASS unmutated / FAIL mutated. Two further rows that looked vacuous were mis-aimed mutations, not vacuity: one is proven discriminating, one is a subject defect routed out of this lane.33 rows are enrolled and quarantined in
floor_expected_redchunk_14, and that is deliberate. They are body_lowering rows blocked on an interpreter defect that is not this lane's to fix (gunbc#8449 lane, PR #8540). Enrolled-and-quarantined is strictly better than orphaned: a quarantined row is counted, named, and held against a roster that reports when it starts passing, whereas an orphan is invisible. The quarantine carries its root cause and its un-quarantine trigger in-file.A memo impurity found while chasing the cost, and why no warm landed
The quarantined rows are slow because a shared one-time cost — grammar preparation — is billed to whichever claim happens to reach it first. That is the third instance of one signature in this repo, after gunbc#8491's
MultiEntryIndexand the module-path index it cites, and the established remedy is to pay the shared cost in preparation rather than to let an arbitrary first payer wear it.A preparation-time grammar warm was scoped, signed off, and then suspended without being built, because reading the key showed it could not work:
InterpContext::over_scope_indexesshares the node indexes byRc— so the memo key's fn-node pointer half is stable across contexts.symbols: RefCell::new(SymbolInterner::default())— a fresh interner per context.eval_recompute_value_hashmixestype_name.0andvariant_name.0— raw interner-local ordinals, not symbol text.So the digest is not a function of content. Ordinals are small integers assigned in interning order, so the same ordinal names different types in different contexts: the key aliases distinct content systematically, not merely by 64-bit collision risk. Two values identical in shape whose slots hold different named types can hash equal — and two language models with the same grammar shape and different symbol names are exactly that specimen. Miss arm certain, false-hit arm possible and unquantified. Confirmed by two independent source reads (this lane and the #8540 lane); filed as its own tracked item, owned separately, deliberately not folded into #8540.
A warm running in preparation is a third interning order, so it would store under a key no claim computes — real work, a healthy
wall_ms, and zero hits. That is why the sign-off condition demanded that the rows pass, not that the warm ran.Declared rung, because this class has no CI-reachable control
A
.dagwitness executes inside anInterpContext; the class is a property of the relationship between two contexts, and only the host constructs those. The witness is on the wrong side of the boundary it would have to observe — separately, nothing exposes this memo to.dagat all. So:cargo testleft CI on 2026-07-11The fix and the control are the same work: only once the key is content-addressed can a same-context witness compare digests of two structurally distinct values without needing two contexts. So RED-first is not available for this class, and that is a property of the key shape rather than a concession.
The price of that inversion is a guard: the control lands in the SAME PR as the fix, never after. Fix-then-control and fix-with-control-to-follow are one sentence apart and produce opposite outcomes — if the digest change lands without the two-distinct-values comparison beside it, the class goes from declared no-control to no-control-and-no-longer-obviously-missing-one, which is strictly worse than today. And the test for anyone citing this as precedent: the impossibility here was established (the boundary was checked, and the accessor question checked separately), not asserted. Cited by someone who merely found RED-first inconvenient, it should not carry.
The two remedies are also not rung-equivalent, which is worth naming rather than treating as an implementation choice: a host builtin that runs a function in two fresh contexts buys an executing control at mechanically preventable, while hashing symbol text buys structurally guaranteed and needs no builtin at all. Spending seed surface to observe a state you are about to make unrepresentable is a trade, not a neutral step.
ParseTableMemoStatsdeleted — and the counters that were meant to replace it are NOT hereb17a8e7deletedParseTableMemoStats, its getter, and the threeParseTableMemofields it was the only reader of. That deletion stands. It was verified statically (every mention was the struct, the getter, and the construction inside it; the one line that looked like a fourth reader reads a different memo) and then upgraded to execution evidence for free: a floor run executed all 9421 rows against that tree withfailed=0, including every parse-reaching witness — the population that would notice a damaged parse-table memo. Not "I could not find a consumer", but "the consumers that exist all ran".The same commit added
lookups/hits/insertsand a snapshot getter to the cross-claim memo, justified by a named consumer. Those additions have been reverted, and the reason is worth more than the code.Their consumer was to be a grammar warm that refuses when a lookup from a fresh claim context does not hit. That warm was then suspended — correctly, since the memo's key turned out not to be content-addressed, so a warm built on it would have amortised nothing. Nobody re-examined what the suspension had stranded. The counters stayed, their doc comment naming a consumer that no longer existed, and their only reader in the whole tree was an out-of-tree probe harness that has also now been abandoned (it OOMs the runner at full corpus preparation, 7.63GB of 7.86GB).
Landing them would have made this PR self-contradicting: deleting one observable for having no consumer while adding another with no consumer. So they are gone, and
clear_cross_claim_pure_memos' comment explaining counter semantics goes with them.The revert is behaviour-neutral, established by execution rather than by the diff's size
A reviewer glancing at a counter removal will assume neutrality. Here it is shown instead. The revert modifies the memo's lookup and store sites — the hot path every row in the fold traverses — and the floor run on the reverted head (
32253323571) returned a population identical in all seven buckets to the pre-revert run (32249852401):9386 rows over the changed path, no field moved. That is neutrality by execution, not by inspection — and a diff this small is exactly the kind that gets waved through on inspection.
It does double duty:
budget_refused=0now holds on two different commits, with the payer-capable population absent both times. One run could have been a lucky evaluation order; two on different heads with identical buckets could not.A suspension is a re-review trigger for everything it justified. It does not merely stop future work; it retroactively strands the already-merged artifacts whose case rested on it — and nothing prompts the re-read, because the dependent's own diff still looks fine in isolation.
One shape behind three defects in this PR, and it is the work item's own subject
Three problems here were the same shape: an artifact whose justification lives somewhere other than the artifact.
[[bin]]manifest entry justified by a source file on disk — the file was deleted, the entry stayed, andcargo buildon this branch failed silently because CI builds no Rust (suite removed 2026-07-11, clippy 2026-07-08).cargo check --libpassed on that broken tree, because--libnever builds bins;cargo fmtis what refusedgit statusone command before it would have shipped as a policy changeNone broke loudly. Each broke when its other half moved, and the checking mechanism was either not run or scoped too narrowly to reach.
That is the same class this work item exists to remove: a row that reads as coverage while its executing half lives elsewhere, or nowhere. The orphan TestClaim rows are that defect in the witness corpus; these three are that defect in the build.
The gate is nondeterministic, and it is not this PR's to fix
budget_refusedmoved 3 → 8 → 10 → 3 across runs on effectively unchanged code, and the floor's job fails whenever it is non-empty. The refusals are bimodal, not marginal: seven rows refused at ≥1553ms in one run ran at 183–248ms in another — a ~7× gap with nothing between, against a whole-population host-speed shift of only 12%. Three rows refuse in both runs, so there is a persistent payer set with a moving remainder around it, which is the positive fingerprint of a first-payer mechanism rather than the absence of a threshold signature. Also worth stating: every refused row reports a cost of 1553–1559ms, i.e. the ceiling plus a scheduler quantum — those figures say where the interruption landed, not what the row costs, so the true cold-payer cost is unknown. Routed to the gate's owner; not picked up here.