Skip to content

One left-corner relation instead of 38 closures; grammar fixpoints converge instead of running a fixed 38 rounds - #8487

Merged
briansrls merged 3 commits into
mainfrom
session/deep-moth-771-leftcorner
Aug 19, 2026
Merged

briansrls merged 3 commits into
mainfrom
session/deep-moth-771-leftcorner

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Aug 19, 2026 •

Copy link
Copy Markdown
Contributor

prepare_grammar runs on every parse, and 62% of it was grammar_has_left_recursion rebuilding a complete left-corner transitive closure from scratch for each of the 38 productions — 38 closures to answer one reachability question. Each closure ran a fixed number of rounds with no convergence check, and each step re-found a production by filtering the whole production list to take element zero. Measured: 7272ms of an 11.7s preparation.

The change

  • One relation, not one closure per production. Rows are seeded with each production's direct left corners and expanded to fixpoint; each production's answer is then a lookup. Same transitive closure of the same edge relation — the identical question, asked once.
  • Both grammar fixpoints converge instead of running a fixed length(productions) rounds. Set is a PointwisePower characteristic function, so sets cannot be compared and the fixpoint cannot stop on next == previous; both fixpoints only ever insert, so a monotone count that stops rising means the set stopped changing. The result is identical, not approximated. fuel retains the previous worst-case bound exactly, so this can never do more work than the old shape.
  • One nullable fixpoint per preparation. grammar_validate_and_analyze computes it once and shares it; it was computed three times.
  • grammar_lookup_production finds instead of allocating a filtered copy of all 38 productions, at every nonterminal reference of every parse step.

Measurement

Same host, same binary, one dispatch, both fixes present — the only difference is 02_parse.dag, reverted to main's version for the BEFORE column (claim_batch interprets .dag at runtime, so one build measures both trees). All 14 rows of dag_arrow_lambda_witness_test:

row before after
witness_single_param_lambda_parses 10890ms 1106ms
witness_pre_repair_grammar_restores_the_RED 11980ms 1727ms
the other 12 rows 180–551ms 177–488ms

The first row is the one that matters: it pays the preparation, and the cross-claim memo cannot help it because nothing has run yet. 10890ms → 1106ms, under the 1552ms ceiling. The other twelve were already cheap once the memo started hitting (#8465); they improve slightly because the preparation they no longer pay got cheaper anyway.

Isolated from the memo entirely — same pairing on a tree without #8465, so the memo is inactive on both sides and every row pays a preparation — the preparation itself goes 12–14s → ~1.1s, and pre_repair 56176ms → 4722ms.

Controls, and which one is load-bearing

v2.test.parse.grammar_validation carried its coverage as TestClaim data rows, which floor discovery (column-zero test fn) does not reach — the module appears zero times in the floor log. So the existing direct-left-recursion and right-recursive claims establish nothing at run time, and this rewrite had no executing regression control. Seven test fn rows now assert it.

They were then falsified rather than trusted. With the left-corner fuel deliberately truncated to 1 on a throwaway branch:

control fuel=1 (broken)
validation_direct_left_recursion_is_detected PASS
validation_indirect_left_recursion_is_detected_RED PASS — does not discriminate
validation_five_hop_cycle_is_left_recursive FAIL — discriminates
validation_five_hop_chain_is_not_left_recursive PASS

The indirect two-cycle does not catch depth truncation: seeded direct corners plus one expansion round already close it. The five-hop cycle, paired with a same-shape five-hop non-cycle, is the control that fails when the fixpoint stops early — which is the exact failure mode this rewrite risks introducing.

Read that table before assuming the indirect case is the important one. Two of us predicted it would be, and it was the control we each said we would not ship without. It is still worth keeping — a relation that never expanded at all fails it — but it guards indirectness, not depth, and only the deliberate break distinguished them. A green witness says nothing about what it would catch; breaking the implementation on purpose is what says it.

pre_repair at 1727ms is left as it is. Two preparations for two grammars is correct behaviour, and trimming 175ms to land under the ceiling would be optimizing the witness to flatter the budget rather than making anything faster. 13 of 14 stated honestly beats 14 of 14 obtained by trimming.

What this does not do

pre_repair lands at 1727ms, still over the 1552ms ceiling — it prepares a second, modified grammar, so it legitimately pays two preparations. The arrow-lambda restoration case is therefore 13 of 14, not complete, and this PR does not restore anything: relocation and the roster belong to #8457's declared trigger and its owner.

gunbc-ci-auto-heal added 3 commits August 19, 2026 01:03
…uted once per preparation

grammar_has_left_recursion rebuilt a complete left-corner transitive closure
from scratch for EACH production -- 38 closures on the .dag grammar to answer
one reachability question -- each running a fixed number of rounds with no
convergence check, and each step re-finding a production by filtering the whole
production list. Measured at 7272ms of an 11.7s grammar preparation, and the
preparation runs on every parse.

Now: one relation seeded with direct left corners and expanded to its fixpoint;
each production's answer is a lookup in it. Both grammar fixpoints (nullable and
FIRST rows) stop when a monotone measure stops rising instead of running a fixed
38 rounds -- Set is a PointwisePower characteristic function so sets cannot be
compared, but both only ever insert, so an unchanged count means an unchanged
set and the result is identical. fuel preserves the previous worst-case bound
exactly, so this can never do more work than before. Measured: nullable
converges at round 4 of 38; FIRST rows need more than 4, which is why the
stopping rule is measured rather than a constant.

grammar_validate_and_analyze now computes the nullable set once and shares it
with both consumers; it was computed three times per preparation.

grammar_lookup_production finds instead of allocating a filtered copy of all 38
productions to take element zero, at every nonterminal reference of every parse
step.

EXECUTING CONTROLS. The TestClaim rows in grammar_validation are not reached by
floor discovery (column-zero test fn), so the existing direct/right-recursive
coverage establishes nothing at run time and this rewrite had no live regression
control. Seven test fn rows now assert it, including the cases a closure rewrite
actually breaks: indirect recursion (A = B x, B = A x) with a same-shape
terminating twin, and a five-hop cycle with a five-hop non-cycle, which a
truncated or depth-limited expansion fails while passing every direct case.
@gunbai-bot gunbai-bot Bot changed the title Main witnesses floor red: retire the budget_refused=102 + stale_quarantine=5 population (brief follows by message) One left-corner relation instead of 38 closures; grammar fixpoints converge instead of running a fixed 38 rounds Aug 19, 2026
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review August 19, 2026 01:56
@gunbai-bot

gunbai-bot Bot commented Aug 19, 2026

Copy link
Copy Markdown
Contributor Author

On the left_corner_row note — agreed it is safe, but the stated reason is not quite the reason, and the difference matters if someone later "fixes" it into a refusal.

Corner lists only ever contain nonterminal production names. expr_corner_fold_terminal contributes Empty (terminals have no left corners) and expr_corner_fold_nonterminal contributes the production name. So the Absent arm is not reached by terminals at all.

Where it IS reachable: a grammar referencing an undefined nonterminal. That symbol appears in a corner list and has no row, so map_get answers Absent. Two things make Empty correct rather than an absorbing default there:

  1. It is the semantically right answer — a symbol naming no production contributes no left corners — so this is a total function on its actual domain, not a failure arm widening to a guess.
  2. The refusal for that state already exists and runs first: grammar_has_undefined_nonterminals gates grammar_validate_and_analyze ahead of the left-recursion check, so within the preparation pipeline the state cannot arrive here. That is the ordering your note points at, and it holds.

The part I would not want inherited from the note is "unreachable in practice" as a general claim: grammar_has_left_recursion is public and the new test fn controls call it directly on fixture roots with no validation in front, so a caller can reach Absent without passing the gate. It answers correctly when they do.

Rejected is a different case: map_get is documented in v2.std.collection as total — map_lookup is the primitive and map_get wraps it in an always-Accepted Outcome — so that arm has no producer and exists only because the Outcome shape forces it. That is the arm the carrier's own note calls out as the reason the total map_lookup is the better surface.

No change pushed: the behaviour is right, and I would rather not invalidate the approval and the in-flight floor run to add a comment. If a reviewer wants the rationale in the source rather than here, it is a one-line follow-up.

— sent from deep-moth-771

@briansrls
briansrls merged commit 7cc7a16 into main Aug 19, 2026
1 of 2 checks passed
@briansrls
briansrls deleted the session/deep-moth-771-leftcorner branch August 19, 2026 03:16
gunbai-bot Bot pushed a commit that referenced this pull request Aug 19, 2026
…rong

REQUEST_CHANGES on this PR was correct. v1_dead_witness_tree_triage_receipt_remainder
already ruled out widening the required floor's source roots to include src/v1,
and this PR did exactly that without reconciling against it. I missed the
receipt in the same file I reached into.

So I ran the experiment this PR already was. CI run 32219326621, srv1-04, floor
step 05:27:35Z-05:36:41Z.

THE OLD REASON NO LONGER REPRODUCES. The receipt says 'stalled 8+ minutes in
strict-preparation, RSS plateaued ~7.2GB, zero phase progress, killed'.
Preparation ran to COMPLETION in ~9 minutes and refused with 532 typed located
diagnostics. No stall, no kill. The cost objection went stale the night before:
#8465 unblocked the prepare_grammar memo for every language, #8487 replaced 38
left-corner closures with one converging relation, and a parse-bearing module's
first row went 10890ms -> 1106ms.

THE CONCLUSION SURVIVES ANYWAY, for a better reason. Zero of the 532 diagnostics
are in src/v1 -- 525 in src/v2, 7 in dag/test. The two trees share NO exact
module path but collide on the LAST SEGMENT twelve times: artifact, coercion,
common, compile, complexity, emit, infer, normalize, ownership, parse, resolve,
tokenize. v2.compiler.program_assembly calls tokenize at line 28 with no import
for it; that bare cross-module reference resolves today only by pool-membership
coincidence, and adding src/v1 supplies a second module whose last segment
matches. The reference stops resolving. That is the Class B failure DESIGN's
import-strip cascade thread names, reached from the opposite direction.

WHY THE CORRECTION MATTERS MORE THAN THE RULING. Under the old receipt the
dissolve-on is implicitly 'when the floor gets faster' -- so the next person to
land a preparation win retries this and hits 532 errors again. The corrected
receipt sets it on namespace-only resolution instead: bare cross-module
references binding by containment rather than by pool coincidence. Right
trigger, right lane.

The source-root change is REVERTED. This PR now carries only the receipt, and
the old measurement is retained beside the new one rather than overwritten.

Stated plainly in the receipt rather than left implicit: src/v1 has NO per-PR
gate on source validity until that lane lands, because compile-clean died with
the floor cut and regen is red by construction. #8519 is the specimen that
proved a parse error there is invisible.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls pushed a commit that referenced this pull request Aug 19, 2026
…on was wrong (#8520)

* Floor: fold compile_clean_source_roots so src/v1 is in the prepared subject

src/v1's .dag sources had NO per-PR coverage of their source validity. The
floor folded witness_layer_roots (= dag + src/v2), which is the corpus MINUS
the seed, so nothing on every-PR CI ever parsed src/v1/**.dag. A parse error
there was invisible, which is how one landed (#8519, fixed).

What DID cover v1 and no longer does:
  compile-clean  deleted with the 2026-08-15 floor cut
  regen          red by construction since the regen root cut (#8406)

v1's BEHAVIOR is covered -- 253 files under dag/test/claim reach it -- but
through host builtins against the compiled Rust seed, not by resolving v1 .dag
sources. Behavior tested, source validity not.

THE CHANGE IS ONE LINE AND MINTS NOTHING. gunbc.ci_layer_roots already defines
compile_clean_source_roots() = witness_layer_roots + [src/v1], the pool
authority meaning 'the corpus including the seed'. The emitter folds that
instead. Deliberately NOT adding src/v1 to witness_layer_roots: that list has
227 references and 13 witnesses pin its value (shard partition boundaries,
pre-push scope, doc-graph roots, lens grounding pools), so widening it would
move four unrelated subsystems' entry roots in one edit.

VERIFIED RATHER THAN ASSUMED that this actually parses the files:
prepare_repository_once builds its index over ALL source roots and pushes every
indexed module into the compiled subject, calling witness_file_from_source on
each. Pool membership IS subject membership on this path -- so src/v1 is parsed
and typechecked, and its witnesses enroll. I had assumed the opposite first.

RETIRES A SCAFFOLD. src/v1/stage0/src/bin/v1_src_dag_parse.rs is a registered
Scaffold whose dissolve-on reads 'when src/v1 .dag is parsed by the modeled
pipeline'. That is this change. It is also weaker than what it is replaced by:
it read src/v1/*.dag NON-recursively, missing 8 nested files including
src/v1/tests/claim/checkpoint_identity_keying_witness_test.dag and its 7
witnesses, and nothing executed it -- it is built and shipped in the release
bin pack and invoked by no workflow. Its deletion is not bundled here; this
commit only makes it retirable.

Local probe on this tree: 46/46 top-level src/v1 .dag parse clean (#8519 is
already merged as e1da001). Whether typechecking src/v1 as part of the
prepared subject surfaces more is what this PR's CI answers.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Re-measure the src/v1 RESTORE ruling: conclusion stands, reason was wrong

REQUEST_CHANGES on this PR was correct. v1_dead_witness_tree_triage_receipt_remainder
already ruled out widening the required floor's source roots to include src/v1,
and this PR did exactly that without reconciling against it. I missed the
receipt in the same file I reached into.

So I ran the experiment this PR already was. CI run 32219326621, srv1-04, floor
step 05:27:35Z-05:36:41Z.

THE OLD REASON NO LONGER REPRODUCES. The receipt says 'stalled 8+ minutes in
strict-preparation, RSS plateaued ~7.2GB, zero phase progress, killed'.
Preparation ran to COMPLETION in ~9 minutes and refused with 532 typed located
diagnostics. No stall, no kill. The cost objection went stale the night before:
#8465 unblocked the prepare_grammar memo for every language, #8487 replaced 38
left-corner closures with one converging relation, and a parse-bearing module's
first row went 10890ms -> 1106ms.

THE CONCLUSION SURVIVES ANYWAY, for a better reason. Zero of the 532 diagnostics
are in src/v1 -- 525 in src/v2, 7 in dag/test. The two trees share NO exact
module path but collide on the LAST SEGMENT twelve times: artifact, coercion,
common, compile, complexity, emit, infer, normalize, ownership, parse, resolve,
tokenize. v2.compiler.program_assembly calls tokenize at line 28 with no import
for it; that bare cross-module reference resolves today only by pool-membership
coincidence, and adding src/v1 supplies a second module whose last segment
matches. The reference stops resolving. That is the Class B failure DESIGN's
import-strip cascade thread names, reached from the opposite direction.

WHY THE CORRECTION MATTERS MORE THAN THE RULING. Under the old receipt the
dissolve-on is implicitly 'when the floor gets faster' -- so the next person to
land a preparation win retries this and hits 532 errors again. The corrected
receipt sets it on namespace-only resolution instead: bare cross-module
references binding by containment rather than by pool coincidence. Right
trigger, right lane.

The source-root change is REVERTED. This PR now carries only the receipt, and
the old measurement is retained beside the new one rather than overwritten.

Stated plainly in the receipt rather than left implicit: src/v1 has NO per-PR
gate on source validity until that lane lands, because compile-clean died with
the floor cut and regen is red by construction. #8519 is the specimen that
proved a parse error there is invisible.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Correct the other two receipts carrying the same stale RESTORE mechanism

The APPROVE on this PR cited v1_dead_witness_tree_triage_receipt (line 928).
I had corrected v1_dead_witness_tree_triage_receipt_remainder (931). Checking
that discrepancy found the real defect: THREE receipts carry the RESTORE
ruling, and I had corrected one.

  929  v1_dead_witness_tree_triage_receipt                      stale
  931  v1_dead_witness_tree_triage_receipt_remainder            corrected
  933  v1_dead_witness_tree_triage_receipt_emitter_ambiguous..  stale

That is a partial sweep -- the failure I flagged twice today in other diffs and
then committed here. It took a reviewer's mis-citation to surface it.

Line 933 makes it worse than symmetry: it records that the stall was
'corroborated independently by smart-ram-730 via CI run 32196317824 on a
dedicated srv4 runner'. So a second session's measurement was also attached to
a mechanism that no longer reproduces, and the corrected receipt would have been
outvoted two-to-one by its own stale siblings.

FIXED BY CITATION, NOT DUPLICATION. The full corrected measurement stays in
_remainder alone. The other two now record three facts -- the stall does not
reproduce, the ruling stands on twelve last-segment module collisions, the
trigger is namespace-only resolution rather than a floor speedup -- and then
cite _remainder instead of restating it. One authority, two references. Both
original measurements are retained as the record of what was true then.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot pushed a commit that referenced this pull request Aug 19, 2026
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>
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>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant