Repository navigation
Fix cross-claim prepare_grammar memo leaking Symbols across InterpContexts (#8505) - #8540
Merged
Merged
Conversation
…texts (#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>
gunbai-bot
Bot
changed the title
briansrls
pushed a commit
that referenced
this pull request
Aug 19, 2026
…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>
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>
4 tasks done
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.
Summary
Root-cause fix for the floor-subject-only
PatternMatchFailureresidual of gunbc#8449: thePreparedGrammarmatch inv2.compiler.parseparse_module_preparedreds with<invalid-symbol>tags under the whole-corpus prepared subject (gunbc#8505, specimen: the 33 quarantined rows infloor_expected_redchunk_14, run 32225493043).Root cause:
PREPARE_GRAMMAR_CROSS_CLAIM_MEMO(v1_interpreter.rs) cachesprepare_grammar's resultValue-- which embedsSymbols local to the producingInterpContext'sSymbolInterner-- keyed only on(fn_node pointer, content_hash), with a clear-scope tied to the whole required-floor prepared-subject run (register_floor_prepared_authority/clear_floor_prepared_authority).run_required_floor's claim-evaluation fold builds a genuinely freshInterpContext(fresh, empty interner) per claim by design. A value cached under claim N's interner, served unmodified to claim N+1's interner, produces non-exhaustive pattern-match failures, andPatternMatchFailure'sDisplaythen resolves the stale index against the wrong interner, printing the literal"<invalid-symbol>"-- matching every observed detail (floor-subject-only; the exact error text; thePreparedModeled -> PreparedModeledGrammar -> GrammarFirstAnalysisshape; per-entryclaim_batchnever hitting it because it keeps one interner live across an entry's claims).Fix: boundary translation per the Realization pattern (DESIGN.md §4) -- de-symbolize to a
Symbol-freePortableValue(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/Fnresults are refused from caching (fail-closed) rather than guessed at, since theirEnvchains aren't a content snapshot andprepare_grammarnever returns them.Roster note:
floor_expected_redchunk_14's 33 quarantined rows live only on the unmergedsession/warm-boar-256branch (commitc4d0e2676f), not on this branch ormain-- so there is nothing to remove here. That commit should not be merged, since these rows will pass once this fix lands.Test plan
ctrl-build --remote -- cargo check -p v1-compiler --lib-- compiles cleancross_claim_memo_survives_a_fresh_consuming_context: builds twoInterpContexts with different pre-interned decoy vocabulary (so a leaked rawSymbolindex would resolve to the wrong name rather than accidentally lining up), stores aVariantresult underctx_a, loads it underctx_b, asserts every tag/field name resolves correctly underctx_b's own interner -- green by execution viactrl-build --remote -- cargo test -p v1-compiler --lib cross_claim_memo_survives_a_fresh_consuming_contextcargo fmt -p v1-compiler -- --checkclean🤖 Generated with Claude Code
Scope of the regression test, and a falsifiable end-to-end prediction
cross_claim_memo_survives_a_fresh_consuming_contextproves thePortableValuetranslation round-trips correctly throughstore_cross_claim_pure_memo/try_cross_claim_pure_memo-- it does not prove thatrun_required_floor's real per-claim context path actually routes through those two functions. If a second store/load path were ever added, or the floor stopped consulting this memo, that test would keep passing while the property it protects was gone.The end-to-end control for that is the 33
body_lowering_*rows this bug produced (gunbc#8505, run 32225493043, currently quarantined on the unmergedsession/warm-boar-256branch, not on this PR ormain). They fail today through the realrun_required_floorper-claim path with no test scaffolding: 30PatternMatchFailure+ 3budget_refused. Correction: this PR's own CI run (32233599135, planned=9179) does NOT exercise those 33 rows -- they are not on the roster this branch's floor executes (session/warm-boar-256's row-promotion work, 242 test-fn rows, is not onmainand not on this branch either), so their absence from this run's failures is not evidence they now pass; it is evidence the rows never ran. What this CI run does establish: the fix does not regress the existing 9179-row floor, and none of the 306 enrolled expected-red rows flip to now-PASS. The 33-row prediction is confirmed or falsified separately, aftersession/warm-boar-256mergesmainon top of this fix and re-runs required-floor -- that session will post the resulting numbers (pass or fail) once it does.