Repository navigation
Delete the TestClaim evaluation island; promote orphan claim classes to executing witnesses - #8497
Merged
Merged
Conversation
added 3 commits
August 19, 2026 02:38
…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.
6 tasks
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 19, 2026
…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>
briansrls
added a commit
that referenced
this pull request
Aug 19, 2026
…5 parse-reaching claims declared as residue, not enrolled (#8505) * Delete the TestClaim evaluation island; promote eight orphan claim classes 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. * field_patch_monoid: promote the assertions, not the value-computations 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. * apply_lens_enforce_uses_projection: the fixture was malformed, and executing 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. * Promote 82 orphan TestClaim predicate files to executing witnesses; root-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> * Delete the two orphaned family_receipt aggregates the promotion left 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> * Fix the two floor-only failure classes from run 32225493043 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> * Vacuity finding: witness_fold_source_stops_at_is_done could not have 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> * Vacuity finding: disj_max_claim_holds could not have failed either 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> * Cross-claim memo counters with a consumer; delete the sibling that never 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> * Cross-context memo probe: two arms, one binary, prediction recorded BEFORE 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> * Unpromote the parse-reaching cohort: 35 claims that cannot reach a verdict 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> * Revert the cross-claim memo counters: their consumer was suspended, and 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> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
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.
What executing them found, on the first run that could
apply_lens_enforce_projection_claim_holdsreturnedfalseon a clean tree. An authored assertion that was simply wrong, sitting in the corpus reading as coverage for exactly as long as nothing executed it.Root-caused to the witness, not the lens:
v2.std.node_queryfind_named_childdescends named children only when the connective isConj, and the fixture authored its root as anAtomcarrying aNamededge — a leaf with a child. Sosubterm_atcould never reach the section,apply_lens_enforcerefused at step one, and the claim'sRejected => falsearm answered. Fixed in the fixture;v2.lens.applicationuntouched.That row is the argument for this PR. The rest is the mechanism that surfaced it.
The mechanism
Floor discovery is marker-keyed:
v2.workflow.floor_naming_hygienefloor_discovery_line_starts_test_decladmits a line only if it startstest fnortest dataat column zero, mirrored host-side incli_run.rswitness_file_from_source. TheTestClaimcorpus is type-keyed and marker-free —test data <x>: TestClaimoccurs zero times corpus-wide — so the two populations are disjoint by construction and noTestClaimrow has ever been a floor unit.Measurement grain is grep over column-zero declarations, stated as such: ~686 rows across 170 modules; 180 of the 218 modules naming
TestClaimdeclare no test decl at all; 379 rows are referenced exactly once corpus-wide, their own declaration.The apparatus was inert too
An evaluator exists (
v2.compiler.05_evalrun_test_claim). Its roster,v2.test.manual.manual_corpus_rostermanual_corpus_node_subject_rows, had six members — and the runner plus all fournat_semiringrung-eval modules declared zero test decls, so nothing drove any of it. Six files, 63 top-level declarations, zero references from outside the island, measured by name rather than by import since imports do not bind in this substrate.Deleted with it, as the same weed above the waterline rather than separate finds:
v2.workflow.bootstrap'sBootstrapEvaluatorCorpusHarnessEntry, whose well-formedness witness compared symbol literals to the literals it had just built the record fromv2.workflow.cliin full — a modeled CLI route surface with zero references to any declaration or to its module pathci_layer_rootsstrict-resolve exclusion rows, under that note's own stated trigger: a row that excludes nothing is dead weight, delete itrun_test_claimand its carriers keep many live consumers; nothing is stranded.Eight classes promoted
Each specimen already carried its assertion as a nullary
fn () -> Boolwrapped in a claim that decided nothing. Promotion isfn→test fn, deletion of the_claim_rhsglue and the inert row, an import prune, and the*_test.dagrename the sidecar rule requires. Checked before renaming: none of these module paths joinsgunbc.witness_deferral_freezeorfloor_expected_red.Floor arithmetic: planned 9008 → 9029, executed 9029, +21 promoted rows.
Discrimination receipts, and the protocol that makes them evidence
Executed on
probe/wise-bat-141-discrimination(runs 32209722310, 32209718874): one subject-side mutation per class, with the predicted RED set written into that branch's commit message before the run. That ordering is the point and a reviewer cannot see it from the diff. A mutation result read afterwards can be rationalised into whatever the tree did; read against a prediction it can only agree or embarrass you.Seven of seven target rows RED under mutation. Predicted collateral from inverting
symbolic_cost_dominatesconfirmed:polynomial_dominates_linear(called certain),nested_cost_projectionandnested_complexity_projection(called likely); three predicted-likely rows stayed green for the same-class short-circuit named in the prediction. Two rows red that were not predicted —lens_application_synthesis_gap_polynomialand..._enforce_rejection— which is better evidence the mutated arm is load-bearing than the seven that were called. That branch is deliberately red and is closed unmerged.Two corrections made before landing, not after
Nullary-and-Bool is a shape, not a semantics.
compose_assoc_lhs/compose_assoc_rhsmatch the promotion shape exactly and are not assertions — each returns the applied composed patch value,falseon a clean tree — so promoting them enrolled two rows red on arrival. This is the mirror of the vacuous-green hazard and equally invisible until execution: a CI run reports which rows fail and cannot report which pass vacuously. The real assertions were ten inertdata witness_*: Bool = <expr> == <expr>rows. The two are demoted, the ten promoted. So the sweep is per-file with the predicate read, never a pattern match over the corpus.Population check so that is not overstated: 182 column-zero
data _: Bool =rows exist, 131 in modules with no test decl, but only 14 carry a comparison operator — ten of them in that one file. Most are configuration flags. A small class, not a secondTestClaim.Not established
apply_lens_enforce_projection_claim_holdshas no discrimination receipt. Its mutation was red on both branches because the row was already red for the fixture defect, and a mutant of an already-failing row proves nothing. It earns a mutation in the next sweep, against a green base.Not done here, deliberately
80 predicate-bearing orphan files remain, 256 predicates across 27 classes keyed on the subject under test rather than the directory, since the subject is the axis a discrimination receipt has to range over. Largest are
body_lowering_fold(3 files / 48 predicates),translate(4 / 38),eval(1 / 21),parse(5 / 15),compile(11 / 13). Ten import no non-std module and need their subject identified before they can be classed. Held until each class has an executed receipt under the protocol above; dispatched as its own lane.