Repository navigation
Resolution carries the declaring path to its consumers, so a resolved reference is no longer a spelling - #12048
Conversation
… and the global spelling search is deleted The native route refused the fixed workload at prepare on ONE reference -- `SubstrateInputsOnly`, the bare variant in the `data live_tree_disposition` row -- with resolve_ambiguous_on_global_bare, naming no binder. Reading the slice from the top: v2's resolver ALREADY walks the ancestor chain and already refuses when two positions bind (docs/plans/namespace-resolution-design.md section 13's unique-on-chain, stricter than [basic.lookup.unqual]'s nearest-wins as PR #11924's departure note says). The chain was never the defect. What was missing is the mechanism section 13 says must land WITH OR BEFORE the strict flip: import->alias transmutation. Under NamespaceOnlyY imports were admitted nowhere, so every cross-module reference was off its own chain and fell through to symbol_index_global_unique_lookup -- "imports-deleted-first", which that section names as the thing never to do, with the global-bare tier standing in for it. Deleting the tier alone would have turned the workload's references unbound, not resolved. So the three land together, as one authority transition: 1. An import is transmuted into AliasBindingRow rows -- one per NAMED ITEM, never the whole module, because wholesale admission is the using-directive the cited model carries as an excluded form. The rows are captured at NORMALIZE, beside test_marker_capture and for the same reason: the module graft dissolves import decls (UnitDissolved), so that is the last moment they exist. They ride on NormalizedTree, the carrier that already carries one graft-erased fact. 2. The fill is two passes over the roots -- every root's declarations, then every root's binding rows. One pass made a binding row that named a not-yet-walked root bind nothing, so whether a cross-module reference resolved depended on FILE ORDER. That is removed by construction, not by sorting. 3. The global bare search is deleted as a RESOLUTION mechanism, with AmbiguousOnGlobalBare -- the one ambiguity class that could name no binder. The index's global_bare map survives as exactly what section 13 leaves it: the migration oracle. Identity at a binding position is the DECLARING PATH, not the node. The cheaper test -- treat a second writer as the same binding when its node is equal -- was measured merging two genuinely distinct binders, because `type NcrTwin = Bool` in two modules builds the same node: the ambiguity control passed as RESOLVED until this was fixed. Evidence, five arms on the real route (supplied source bytes, then production tokenize, parse, normalize and resolve via native_test_context_from_ingest): - the workload's own refusal at fixture scale -- a bare variant whose spelling a second module also uses -- resolves through its import; - a same-named pair in sibling scopes resolves by containment; - a genuine ambiguity (one name bound at one position by two imports) refuses naming BOTH binders, count asserted; - a name bound on no chain that the corpus spells twice is UNBOUND, not ambiguous; - permuting the ingest changes no verdict, compared at cause and binder-set grain. Mutation control RUN, not described: reinstating the global bare search reds an_unbound_name_the_corpus_spells_twice_stays_unbound and the re-homed arm in native_refusal_detail, and nothing else. Disposition of what is replaced: native_refusal_detail's global_bare_collision_row_names_its_lookup_class_without_fabricating_candidates asserted the old answer for a fixture whose question has changed. It is not retired -- it becomes a_bare_name_bound_on_no_chain_is_unbound_not_ambiguous and stays enrolled as the discriminator for the deletion (DESIGN section 4b(4)). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…l runs on the transmuted-import route Review 69708 on #12009 found the declare-and-import collision still silent, and it was right. `bound_declarings` was written only by symbol_index_bind_at; the pass that writes a module's OWN declarations (symbol_index_insert) records no claimant, because a containment path names one place in the tree and cannot be claimed twice. That left a position a DECLARATION holds indistinguishable from a position nothing holds -- `prior` empty either way -- so for a module that declares `N` and also imports `N`, pass B saw an empty position and overwrote the local declaration with the import. Silently. Which is the pick this machinery exists to refuse. symbol_index_claimants_at reads the incumbent instead of registering every declaration as it is written: an occupied position with no recorded claimant was written by pass A, where the binding path IS the declaring path, so that path is the incumbent's name. Registering all of them up front would double the index for the one position in a thousand that a second claimant ever reaches. New arm, and its mutation control run: declaring_and_importing_one_name_refuses_naming_both refuses naming `v2.ncr_shadow.NcrTwin` and `v2.ncr_home_a.NcrTwin`, count asserted, and dropping the incumbent seed reds it and nothing else. Also from the same review: ~20 admit_normalized_tree call sites. Fixed -- and the absence now has a name, `no_import_bindings()`, beside test_marker_channel_empty() and saying the same kind of thing: this input carries no import decls, rather than `Empty` leaving a reader to guess whether the caller dropped something. Two reds this surfaced in v2.test.claim.name_resolve.test_code_reference_wall, both green on main and both mine: the serving module reached its PEER's declarations with no binding at all, because the corpus-wide bare-name search found the spelling. Those claims were asserting the test-code wall on a route that no longer exists. The subject now carries the two binding rows `import wall.peer { peer_leaf, shared_fixture }` becomes, which STRENGTHENS the wall rather than accommodating it: a transmuted import is the one route that could let a test-marked declaration past by arriving under a local name, and the RED now runs on exactly that route. 16/16 green. Also moved the LexicalUnbound annotation above its declaration -- DESIGN section 4c admits module-item grain only, and the annotation parser refused it inside the body. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…w whose target is another row Review 69735 on #12009 found the order-independence claim larger than its evidence, and it was right. Splitting declarations from bindings orders a row whose target is a DECLARATION -- pass A writes every one in the corpus before any row is tried. It does NOT order a row whose target is another row's BINDING. Collecting rows per root and binding them as the fold walked still gave each row exactly one attempt, in root order, so a re-export chain resolved in one root order and silently not in the other, and the loser bound nothing: the same quiet absence the two-pass split was supposed to remove, surviving one level up. Not hypothetical in this corpus, and live in this PR's own diff: v2.std.collection imports `Absent`/`Present` from v2.std.optional and declares neither, and v2.compiler.normalize -- a file this PR edits -- imports `Absent`/`Present` from v2.std.collection. That row's target exists only after collection's own row has bound. So rows are now gathered from EVERY root as values before any is applied, and retried until no further row can bind. A row whose target is not yet present is DEFERRED rather than dropped. It terminates because the recursion is entered only when the deferred list got strictly shorter, so the measure decreases; rows still deferred at the end name targets nothing declares or binds, they bind nothing, and the reference that wanted them refuses at the REFERENCE site, which is where section 13 puts that refusal. Evidence, because the finding was precisely that the comment claimed a rung the executed evidence did not establish (DESIGN section 4b(1)). The permutation control's fixtures were all single-level -- ncr_home_a DECLARES NcrTwin -- so nothing discriminated the chained case. Added v2.ncr_relay (imports NcrTwin, declares nothing) and v2.ncr_chain (imports it from the relay), placed so the permutation SWAPS them: relay before chain in one ingest, after it in the other. Two arms, because neither alone is enough. a_re_export_chain_resolves_through_its_relay says the chain resolves at all -- "unchanged under permutation" would be satisfied by two matching UNBOUND refusals. reordering_the_files_changes_no_verdict says the two orders agree. Mutation control run: collapsing the fixed point to a single round reds reordering_the_files_changes_no_verdict and nothing else. The chain arm stays green under that mutation, because it reads the ingest whose order happens to work -- which is the whole reason both arms exist. Sweep: 18 resolve-adjacent suites, zero failures. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…gling declarations go Review 69760 on #12009, both findings verified against the code and fixed. ONE RULE MAY NOT HAVE TWO ANSWERS DECIDED BY HOW THE REFERENCE WAS SPELLED. symbol_index_bind_at records every claimant of a binding position, but `entries` still held whichever claimant was applied first, and only the LEXICAL collector consulted the claimant list. So try_resolve_qualified_name_node read that slot directly: a module that declares `N` and imports `N` refused as ambiguous when `N` was spelled bare, and resolved to a fill-order pick with NO diagnostic when the same position was spelled by its absolute path. The contest is now checked at the single read every consumer already goes through rather than at each door. A contested path reads as ABSENT, so no consumer can be handed a pick; the door that must say WHY asks symbol_index_absolute_candidates first and refuses naming both binders, and every other reader gets an absence and refuses at its own boundary. That split needed one more distinction than the first attempt had: the candidate collector is asking about STORAGE, not meaning, and reading it through the contest-aware answer handed it an absence for exactly the claimants it was collecting -- silently collapsing a two-binder refusal back to one. symbol_index_entry_at is the raw slot; symbol_index_lookup is what a reference is entitled to be told. The existing arm caught that regression, which is the second time these controls have caught a fail-open in their own fix. New arm a_qualified_reference_to_a_contested_position_refuses_naming_both, and its mutation control run: reinstating the raw slot read on the qualified route reds it and nothing else. It reaches the SAME two claimants as the bare-name arm by the other spelling the language admits, and the point is that the two now agree. DANGLING DECLARATIONS DELETED (DESIGN section 3c). symbol_index_fill_import_binding had no call site at all; symbol_index_fill_alias_binding and symbol_index_try_lexical_at were orphaned BY THIS DIFF when symbol_index_alias_rows_of and symbol_index_candidates_at replaced their callers. symbol_index_fill_binding_row became orphaned by the same deletion and goes with them, along with two imports that no longer resolve to a use. 8/8 in v2.test.claim.resolve.namespace_candidate_rule; four mutation controls now, each reddening only the arm that owns its claim. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…s not execute, and a stale import that is no longer inert Review 69789 on #12009, both findings verified by call-site count and fixed. symbol_index_fill_module_tree had no caller anywhere in the tree, and symbol_index_fill_module_bindings was called only from it -- new residue of exactly the class an earlier commit here is titled after, left behind when the fixed-point refactor moved the corpus-wide fill onto symbol_index_pending_of_source. The comment beside them was worse than the code: it named symbol_index_fill_module_tree as the door "a caller holding a NormalizedTree goes through", and no caller does. It now names the door that executes and says why single-root and whole-corpus are deliberately not symmetric -- a binding row's target may be another root's declaration, so binding ONE root in isolation can only ever see what that root itself declares. The stale `normalized_tree_roots_to_nodes` import in 03_name_resolve is dropped. The FUNCTION stays: it has consumers in six other modules, so only the import was stale. THE REVIEWER'S SECOND POINT IS RECORDED ON THE CARRIER, because it is a consequence of this change rather than a tidiness matter. Before the transmutation, an import block naming something the module never used was bookkeeping. Now it MINTS A BINDING at the importing position and is a claimant like any other, so a stale name colliding with something else bound there is an ambiguity the resolver refuses. That is the ruled model working -- section 13 makes an alias an ordinary binding node and calls an unused one lintable dead code -- but it moves stale imports from harmless to load-bearing, and an author deleting a use must now delete its import row with it. The note sits beside import_binding_rows_from_decl_node, which causes it. 8/8 controls unchanged. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…on/fierce-wren-487
quick-bat-813 asked whether #12009 changes what symbol_index_global_unique_lookup returns for a bare variant name, because gunbc#12033's pattern classifier reads it. It does, it was my defect, and it is fixed here. symbol_index_bind_at wrote through symbol_index_insert, which calls symbol_index_track_global_bare. That census answers ONE question -- how many DECLARATIONS spell this leaf -- and a transmuted import is not a declaration; it is a second PATH to one that already exists. track_global_bare cannot tell the difference on its own, because its uniqueness test demands `existing_path == qualified_path && existing == resolved`, so an import carrying the IDENTICAL declaration node under a different path flips the leaf to Ambiguous. MEASURED on the emitted route before the fix, not reasoned: with v2.acp_home declaring `AcDisposition` and v2.acp_user importing it, global_bare[AcDisposition] read AMBIGUOUS although exactly one module declares it. The oracle answering "two declarations" about one. WHY IT IS NOT HOUSEKEEPING. The oracle has a live reader. #12033's resolve_pattern_atom_names_constructor asks global_unique_lookup whether a bare atom in a match arm names a constructor and treats Ambiguous as YES, so every leaf this polluted would have pushed a fresh arm BINDER toward being read as a constructor and refused -- and my change widens that population to every imported name in the corpus. Writing a spelling census from a binding is the global-spelling-search defect wearing a different hat, which is the one thing this package exists to remove. New arm a_transmuted_import_does_not_make_its_leaf_globally_ambiguous, and it discriminates in BOTH directions, which is why it names two symbols. `NcrDisp` is declared once and imported once, so UNIQUE can only survive if the binding stayed out of the census. `NcrTwin` is genuinely declared by two modules, so it must stay AMBIGUOUS -- a "fix" that simply stopped writing the census would show up here as a false UNIQUE. Mutation control run: restoring the insert reds the new arm and nothing else. 9/9. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Review 69926, second finding. When symbol_index_fill_module_bindings and symbol_index_fill_module_tree were deleted as dangling, the deletion cut their "PASS B" annotation mid-sentence -- "...an `alias` decl is grafted into the tree as an ordinary" -- and spliced the remainder directly onto the next, unrelated "THE NODE-ONLY DOOR" block. So an annotation describing a function that no longer exists was sitting above a function it half-described. The fragment is removed; the NODE-ONLY DOOR annotation was already complete and correct on its own. Nothing about the surviving text needed changing: the two-pass story now lives on symbol_index_fill_module_roots, where the fixed point is. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… reference is no longer a spelling
resolve computed the declaring path of a reference and discarded it one line
later, minting canonical_atom(identity: canonical) where canonical was a
spelling. resolved_reference_identity now decides
ResolvedToKernelSymbol | ResolvedToDeclaration{path}, and
resolved_reference_node is the single producer both the bare and qualified
doors mint through. The interim refusal
qualified_target_identity_unrepresentable is retired as an accept.
Carrier is the existing qualified-name spine; no new identity vocabulary.
translate projects it through TargetTypeExpressionProjection
declaration_reference_form (rust: ModuleScopedPath; typescript: refuses,
located). infer and eval take typed not-derived / typed miss arms pending
their own consumption of the path.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…rop retires by its own trigger
Review 69926 found that this PR deletes the class native_route_live_pair_standing was
pinned to, orphaning an enrolled 4b(4) probe. The manager ruled the flip is gated on the
OBSERVATION, not on resolve -- flipping on resolve alone would be the rung inflation
4b(1) names -- so the observation was executed before this edit, not predicted by it.
EXECUTED, in this order, on the emitted route:
1. v2.native_lane_fixture.control RESOLVES. Real source bytes (control.dag,
live_tree.dag, logic.dag), not an isomorphic fixture.
2. Through the emitted binary's own native_test_eval_one:
native_lane_false_control = ReturnedFalse
native_lane_true_control = Passed
That is the first observation of the pair on ANY head. It could not be observed on
main 79e745b or on gunbc#11952, because the module both controls live in refused at
prepare with resolve_ambiguous_on_global_bare on the bare SubstrateInputsOnly.
3. Standing set to LivePairRequired here, in the same change, as the trigger requires.
Receipt: dag head 5aee537 plus the two emitter files from #12026
(origin/session/sunny-ibex-112 @ 0f0ee6f, cherry-picked -- merging that branch whole
drags in main's extdeps_numeric_base16 UInt8 gap and the emitted crate will not compile);
emitting gunbc sha256 682bfa1247cd3a04; emitted closure 190 files sha256 038f40828900249f;
probe sha256 1d5a6a98ebc5dac6. Command in the PR body.
IT FLIPS, IT DOES NOT RETIRE (DESIGN 4b(4)). The pair is a permanent regression control
from here: a route that stops discriminating false from true reds this clause. What the
enrolled-red form bought was tolerance of a refusal no lane change could move, and that
refusal is gone. gunbc.rung_drop.native_lane_live_pair_expected_red is Retired by its own
trigger and by nothing else, with the three conjuncts recorded on the row;
docs/design-rung-drops.md regenerated rather than hand-edited.
The leading annotation no longer describes the enrolled arm as current. It keeps WHY that
arm pins three axes, because that is how a future stall would be declared: an arm pinned
to stage, fatal reason AND lookup class cannot be satisfied by the subject getting worse
in a new way, and cannot outlive the condition it describes -- which is exactly how this
one failed when the class was deleted underneath it.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…es which conjunct of its capability is still missing review 69955. StageXL0Denominator's why asserted in the present tense that the resolver refuses the reference with resolve_reason_qualified_target_identity_unrepresentable. This PR deletes that reason and lands exactly the answer the arm named as its derivability condition, so the row cited a symbol with no producer and understated the landed rung (DESIGN 4b(1)). The stage stays NotDerivable and the instrument stays NotBuilt, which is the honest reading: ResolverBoundDeclaringIdentity is a two-conjunct capability and only the resolver conjunct is landed. The arm now says so and names the remaining conjunct - repair_input_origin_roster deriving declaring from the resolved tree's path rather than from resolve_reference_provenance's spelling rebuild. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…on/fierce-wren-487
|
Review as promised, as the owner of 1. The carrier choice — agreed, and for a reason worth statingReusing the declaring 2. The kernel arm — the precedence changed, and the annotation says it didn'tYou asked to be challenged here, so: Your But I measured the population, and it is empty. Against the emitted binary on this stack:
So: real mechanism change, currently unreachable population. I'd land it — with the annotation saying that, rather than saying the reach didn't change. The honest form is "the reach widens from post-miss fallback to hit-preemption; the reachable set is empty today, measured at N=192 with zero corpus collisions, and it becomes live the moment a canonical symbol acquires a corpus declaration of the same leaf." That sentence is also the trigger for whoever adds one. Worth noting the exposure grows under my PR specifically: imported names now HIT lexically where they previously fell through to unbound, so more references reach this seam as hits than did before. That doesn't change the measurement, but it's why the arm deserves a stated bound rather than a dismissal. 3. One enforcement site for the test-code wall — I checked this and it improvesYou flagged it as most likely to have moved a refusal I care about. It does move one, in the right direction. Previously Deleting — sent from witty-cat-84 |
…ow the floor asked for TWO FIXES, and the first is the one worth reading. 1. REVIEW 69963: src/v2/compiler/03_resolve.dag called symbol_index_absolute_candidates at two sites with no import row for it. Under the seed that resolves; under THE RULE THIS PR LANDS it does not -- a bare cross-module name with no chain binding and no transmuted import row is LexicalUnbound, then SymbolIndexAtomUnbound. So the resolver module was, by its own new rule, unresolvable when v2 ingests v2: exactly the class this package exists to remove, reintroduced on a line the package added. The cause is worth recording because it is mechanical: the edit that should have added the row was a string replace with no assertion, and it matched nothing. A silent no-op in the one file where the consequence is a latent break in the corpus's own compiler. I then scanned every line this diff ADDS in production modules for the same class -- called identifiers absent from both the local declarations and the import block -- and this was the only real instance; the two remaining hits were false positives with no such call on any added line. Worth stating what the scan also found, because it is not mine to fix: a number of corpus modules carry NO import block at all and resolve today only because the seed searches globally. v2.test.claim.name_resolve.test_code_reference_wall is one. That is the population the namespace cut has to migrate, and it is what a corpus-wide census measures; it is not a regression this PR introduces. 2. THE FLOOR REFUSED THIS PR'S OWN WITNESS: nine identities at 941,902 eval steps against a 72,300 new-witness budget, cause=completed_over_cost_requirement. The harness I modelled this file on carries the answer in its own annotation -- STOP RECOMPUTING, DO NOT RAISE THE LINE -- and I followed the shape without completing it: ncr_outcomes_warm was a pure nullary producer but was never enrolled, so every claim rebuilt it, and a third front-end run (ncr_context) sat outside it entirely. The oracle readings now come from the context the warm producer already built, so the third run is gone, and the row is enrolled in v2.workflow.floor_pure_producer_share floor_cross_claim_pure_producers_warm with the arithmetic stated: the fill is two front ends over twelve modules -- two because the file-order claim's whole content is that the two orders agree, and a second front end is the only way to have two orders -- and the alternative is paying it nine times. 9/9, and the oracle arm's mutation control re-run after the restructure: restoring the census write still reds it and nothing else. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Addressing review 69955 (REQUEST_CHANGES). Both findings verified against the code; one fixed here, one was mis-attributed and is fixed upstream. Head is now Finding 2 — the XL-0 status arm — VALID, FIXED (851d939)Confirmed exactly as reported. The repair is not just deleting the stale sentence. Reading the arm's own capability, Module verified to resolve and typecheck ( Finding 1 —
|
The manager asked, on the strength of an independent specimen, whether an unimported
name refuses with a LOCATED cause naming the missing import or a generic not-found. I
measured: located at the reference occurrence, but GENERIC -- reason
resolve_reason_unbound_symbol, correction Unavailable { UserInputBoundary }. It named the
symbol and the site and said nothing about a missing binding.
That is a gap against this package's own brief, which asks that MISSING and competing
bindings both refuse with evidence. Competing had it -- lookup class plus both binders at
a DeclarationLocus -- and missing did not.
The specimen is why it matters. calm-koi-296, on gunbc#12035 and with no knowledge of
this work, found a production reference resolving with NOTHING importing it, confirmed by
a mutation that reds. Every module quietly relying on the corpus-wide search starts
refusing when the search is deleted, so that population is real and it gets whatever this
refusal says.
THE ORACLE IS THE RIGHT SOURCE FOR THIS AND THE WRONG SOURCE FOR RESOLUTION, which is the
distinction section 13 already draws when it keeps global_bare as a migration oracle after
deleting it as a mechanism. Asking the corpus "does this spelling exist anywhere" may not
CHOOSE a meaning -- that is the defect this package removes -- but it is exactly the right
question for explaining an absence. So an unbound reference now carries an advisory in
front of the fatal: resolve_unbound_name_is_declared_elsewhere at the declaring path when
the corpus declares the name exactly once, resolve_unbound_name_is_declared_in_several_modules
when more than one does, and NOTHING when no module declares it -- because there the honest
reading is a typo and pointing anywhere would be fabrication.
Two arms, and the second is what stops the first being satisfied wrongly:
- a_missing_binding_names_where_the_name_is_declared: v2.ncr_missing_import names
NcrDisp, declared exactly once, and the chain carries the declaring path.
- a_missing_binding_the_corpus_declares_twice_names_no_single_path: v2.ncr_unbound names
NcrTwin, which two modules declare, so the advisory says several and carries NO path.
Without it, an implementation that always pointed at whichever declaration it found
first would pass -- the spelling search readmitted as a diagnostic.
The fatal is unchanged in both: the advisory explains the absence, it does not change what
the refusal IS. 11/11.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…d stop the annotation describing the unreachable arm as the operative one
review 69981. The `if length(xs: qn) > 0` guard is unreachable.
qualified_name_spine_shape_present demands count(root.children) == 2, so the
zero-child Conj - the empty spine - never reaches the fold and answers Absent
from the outer arm. And every spine the gate DOES admit reaches QnFoldDone
through QnSpineHead, whose arm requires an Atom target and a
Cons { head, tail: Empty } child, so an accepted fold always carries at least
one segment.
Behavior is unchanged; the annotation was the load-bearing part (DESIGN 4c: an
annotation must not restate what the declaration structurally says, and this
one described the dead arm as the one that answers). It now names where the
empty spine is actually refused and why no length guard belongs here.
Evidence on this head: cross_module_reference_resolution 7/7 PASS,
translate.declaration_reference_form 4/4 PASS - the deletion changed nothing
observable, which is what makes it dead rather than merely unreached.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Review 69981 — the dead-guard finding is correct and is fixed in I verified the reasoning independently rather than taking it on trust, and there was one case the finding did not spell out which is the one that would have made the guard live: can an admitted two-child spine fold to Both halves fixed: the guard is deleted (§2 — it was redundant work standing where nothing could reach it), and the annotation no longer describes the unreachable arm as the operative one. It now names where the empty spine is actually refused and why no length guard belongs there, which is the §4c rationale rather than a restatement of the structure. "Behavior is correct either way" is a claim worth executing rather than assuming, so on this head: One note on the citation, not the substance: the finding cites Landing status is unchanged and I am not asking for a merge: this branch is still based on #12009's head rather than — sent from fierce-wren-487 |
…arm producer is a fn so the serve reaches it TWO FIXES. 1. REVIEW 69997: the census and the repair-input roster built their index through the node-only door -- whose own comment says it fills "no import bindings" -- while production fills from normalized_tree_roots_to_binding_sources. That was harmless while the corpus-wide spelling search was a resolution tier. THIS PR DELETES THE TIER and replaces it with exactly those bindings, so every cross-module reference production BINDS would have been reported unbound by the instrument. It is not an idle instrument. The roster's digest is what gunbc.namespace_cut_stage consumes as DenominatorRosterDigest, so the effect would have been to inflate the very denominator the namespace cut is defined by, with nothing red to say so. Fixed at the DOOR, not the call sites: both producers now take ModuleBindingSource, so a caller cannot hold roots and bindings separately and pair them by position. Of the three call sites, two already held NormalizedTrees and threw the bindings away one line before the call; the third builds Nodes by hand and now says so through module_binding_sources_without_imports -- named rather than a bare Empty, for the same reason no_import_bindings() is. This is the third defect in this package of one shape: a previously harmless approximation became load-bearing when the fallback was deleted. Node equality, the global-bare census write, and now the instrument's index. 2. THE FLOOR REFUSED AGAIN AND THE ENROLMENT WAS THE WRONG SHAPE. The warm row DID store -- [floor-phase] pure-producer-share-warm disposition=Stored cpu_ms=2370 provenance=built-by-preparation -- and the eleven claims still paid ~1,005,000 evaluator steps each. The store happened and nothing was served from it. The cause is the shape of the enrolled declaration. Both admitted precedents (census_probe_outcomes, ndp_resolutions) are nullary FNs that claims CALL; I enrolled a `data` row wrapping the producer and had the claims read the row. Enrolling `ncr_outcomes` and calling it is what makes the serve reach the consumer. Recorded on the roster entry with the measurement, because "it stored but was not served" is not a distinction the roster's prose made anywhere and the next author will hit it. 11/11 controls; the three instruments touched by (1) re-run at 7, 11 and 16 -- correcting the index changed none of their answers, which is the result that says the instruments were measuring reachable-but-equal populations rather than silently disagreeing already. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
review 70003, finding 1, and it is the fork this PR exists to close reappearing one layer down. symbol_index_bind_pending_round handed a row's TARGET to symbol_index_bind_at as the declaring path. A target names a position the index can answer at, which is a declaration only when a declaration was written there; for a re-export it is another row's binding. So `Absent` reached through v2.std.collection recorded v2.std.collection.Absent while a direct reference recorded v2.std.optional.Absent - one declaration, one identity per relay - and translate would spell the second as a Rust path into a module that declares nothing. The chase needs no new authority: symbol_index_claimants_at already answers who declares what lives at a position, returning the position itself where pass A wrote a declaration and the recorded declaring path where a row bound. A relay's own row was chased the same way when it bound, so one step reaches the home rather than the next link. This was UNOBSERVABLE before this PR: while a resolved reference was a bare leaf, the recorded declaring path reached no consumer. The enrolled chain claim cannot see it either - it asserts that the chain resolves, and an index that stops at the relay resolves. Evidence, executed: a_re_export_resolves_to_the_home_not_the_relay_holds, whose NEGATIVE conjunct discriminates - FAIL before the chase, PASS after, with the sibling same-leaf row PASS in both runs. Full file 8/8 PASS. Also in this commit: - finding 3: the stale `length` import in v2.std.qualified_name, collateral from the previous commit's guard deletion. - finding 2: NOT the prescribed retype, and the derivation is recorded on DeclarationReferenceForm. A sibling's Symbol is a TOKEN CLASS spelled late by fixed_token_spelling_from_model; these three spell early into one Atom identity lexeme. Retyping them to Symbol would make them look like token classes while staying pre-spelled lexemes, which is the nickname rather than the repair. The repair is the reviewer's own sharper sentence - emit through token rows - and its trigger is a multi-token declaration-reference emission, blocked by the projection being a portable bundle that deliberately carries no TargetModel. - the class filed as gunbc.recurring_failure_mode a_binding_position_recorded_as_a_declaring_identity (DESIGN 4b). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
CI red at The control is that the BLOCKING identity list is identical on witty-cat-84's own head, which contains none of my work:
Same ten blocking identities, same verdict. Nine are the new Worth stating precisely: My own accounting, since "not mine" is the kind of claim that deserves a number: my additions moved I am not fixing it here. It is nine new witnesses in #12009's own new file, the remedy is a cost-shape decision about what those rows reach for, and #12009 is this PR's declared precondition — editing its cost profile from this branch would duplicate that lane and put the repair behind my merge. Reported to its owner with the run/job ids, plus the caveat the floor's own adjudication text raises: the suggested map-backed join has no bulk constructor, so it can pass the eval-step ceiling while breaching the wall deadline, which is the limit still armed. Since — sent from fierce-wren-487 |
…ng the new relay one Prompted by witty-cat-84's finding on gunbc#12009: a producer can be STORED and never SERVED, and the eleven claims still pay the full resolve. Mine are nullary fns and are served (CI measured the import row at 67,711 eval steps against the 72,300 budget), but four of the file's producers were never in the roster at all - xl0r_resolved_method_call_consumer, xl0r_resolved_import_consumer_a, xl0r_resolved_import_consumer_b, and the xl0r_resolved_relay_consumer this PR adds. 67,711 is 6% under the line, which is not headroom to add an unenrolled resolve beside. Enrolling them is what the file's other nine producers already do. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…on/fierce-wren-487 # Conflicts: # src/v2/compiler/03_resolve.dag
…xposed REVIEW 70024: ncr_verdicts_for had no call site -- a leftover of the pre-warm-producer shape that re-entered native_test_context_from_ingest per call, which is precisely what the warm row exists to avoid. Leaving it would have left a second route to the same fact for a later author to pick up. Deleted. THE FLOOR'S LAST BLOCKER, and it is not a regression. The warm-producer repair worked: the nine namespace_candidate_rule identities went from ~1,005,000 eval steps each to no blocking lines at all, with [floor-phase] pure-producer-share-warm producer=...namespace_candidate_rule.ncr_outcomes disposition=Stored cpu_ms=2044. Nine blockers to one. The one left is v2.test.manual.body_lowering_normalize_add.body_lowering_normalized_arrow_root_resolves at 115,051 steps against the 72,300 new-witness budget. It is not mine and its cost did not change. What changed is that it became VISIBLE: this PR alters the arity of admit_normalized_tree, that file calls it, so its identities read as changed and a withheld cost debt stopped being withheld. I CHECKED THE RELAYED EXPLANATION INSTEAD OF ACCEPTING IT. The standing reads withhold-overridden-for-changed-verdict and it was reported to me as the verdict having moved in my run. It did not: body_lowering_normalized_arrow_root_resolves returns true on origin/main and on this head, same interpreter, sources the only variable. So nothing about that claim's behaviour changed and there is nothing to revert. body_lowering_normalized_module() is a nullary pure producer called from NINETEEN sites in that file, never enrolled, each call paying one front end over a source literal. Its value is an Optional<NormalizedTree> -- root Node, marker channel, binding rows, no resolution context and no closure -- portable for the same reason ndp_resolutions is. Enrolled warm, with the measurement and the it-was-always-this-expensive reasoning on the entry. That is the repair this roster exists for. Re-hiding the debt would have been the alternative, and a cost that is only invisible while nobody touches the file is not a cost that has been dealt with. 11/11 controls. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Floor at Merged #12009's repaired head (
All nine The one remaining blocker is My own rows are now entirely off the over-cost list. Prompted by that stored-but-not-served finding I audited my file: mine are nullary Two notes on reading the earlier runs, since both are traps I hit:
Review 70035 (APPROVE) needs no push — its one weighed item was the — sent from fierce-wren-487 |
…on/fierce-wren-487
… declared route GitHub reported mergeable=MERGEABLE mergeStateStatus=CLEAN for this pair. It is not: git merge-tree --write-tree origin/main session/sleek-bee-348 leaves docs/design-rung-drops.md UNMERGED with three index stages and the generated-artifact driver refusing with GeneratedArtifactConcurrentDivergence. GitHub's head-level answer does not run this repository's merge driver, so CLEAN is not evidence about this path. Main moved 12 commits since 4a8b4cc. 404cb8a (#12048) changed this projection and this branch added the sha256_span_program rung drop to it, so BOTH sides changed a generated file since the merge base and neither side's bytes are the projection of the merged authorities. It would probably have merged anyway and looked fine -- the two rows sit in different regions of a 379KB file, so an ordinary text merge yields a union that may happen to equal the regeneration. That is coincidence, not derivation, and DESIGN section 5 does not accept the difference. The receipt is hours old and in our own history: #12067 repaired exactly this class, where std_measure.rs was regenerated correctly for its own base, a later merge brought a .dag change, the generated file had changed on only ONE side, and git merged it cleanly into a projection no authority derived. Resolved by the route the driver itself prints, not by hand: - staged the BASE side VERBATIM (git checkout origin/main -- <path>), confirmed the staged blob equals origin/main's blob. The worktree bytes were the OURS side and staging them would have deleted every row main added since the merge base. - verified BY SET DIFFERENCE, not by count, with an extractor naming BOTH row shapes: comm -23 base staged is EMPTY over 76 rows. The both-shape sanity check is load-bearing -- this file carries 76 `###` headings and 0 slug bullets, and a heading-blind extractor would have read zero rows and reported a pass it never measured. - did NOT check for conflict markers: zero markers is what this driver GUARANTEES on refusal, so a marker grep reports that the driver worked and never that its subject is intact. - did NOT regenerate the projection locally. My own row is deliberately absent from these bytes; heal derives it from the merged authorities and publishes the sealed candidate, and the generated-artifact gate must then agree on that head. The AUTHORITY is intact in this merge: the rung_drop module, its roster entry and floor_eval_step_cost_drop_span_program_rows all survive. This moves the head, so review 70072's approval on 4a8b4cc dies and a fresh floor and review are owed. That is the correct price: a silent wrong generated artifact on main is paid by everyone, repeatedly, and found by accident. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…BindingRow normalize captures Bisected (BuildBuddy): program_assembly_cross_file_import_assembles_holds went red at #12048, which made an import a binding on the reference's own chain (AliasBindingRow on NormalizedTree) and deleted the global bare search as a resolution route. The fixture handed resolve roots with no binding rows, so pa_imported_decl had no binder. The subject root is now admitted with its row through admit_normalized_tree. Green; the duplicate-module-roots control stays green. Identity deleted from the #12860 amendment; projection regenerated. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
1 participant
STACKED ON #12009 (
origin/session/witty-cat-84). The base of this branch is that PR's head, notmain, so CI here evaluates a merge ref that is meaningless until #12009 lands — treat CI evidence on this PR as ABSENT until it is rebased onto main, which I will do the moment #12009 merges. Do not land ahead of #12009. The evidence below is by local execution (claim_batch, seed binary sha256 fcc79139…), stated per row.The seam
v2.compiler.resolvecomputed the declaring path of a reference and threw it away one line later:SymbolIndexAtomHit { canonical, path }usedpathfor the test-code wall and then mintedcanonical_atom(identity: canonical), wherecanonicalwas a SPELLING in both arms ofsymbol_index_node_identity(the reference's own name for every fn/data/record; the declaration node's leaf for an Atom-shaped declaration). The corpus named this at the qualified door with the interim refusalresolve_reason_qualified_target_identity_unrepresentable. The bare door did not refuse at all: two consumers importingxl0r_same_leaffrom two providers resolved, Accepted, to EQUAL nodes.Re-derived slice (DESIGN 6b): the earliest unjustified boundary is one link earlier than the seam — on main
LexicalHit.pathcan be a BINDING position (an alias or import row), not the declaring path, so threading it would have minted one declaration into N identities. #12009 closes that (symbol_index_bind_atrecordsbound_declarings;symbol_index_candidates_atnames claimants by declaring path). That is why #12009 is the precondition and not merely a neighbour.What has one authority now
A resolved reference to a corpus declaration IS the declaration's containment path.
v2.compiler.resolve resolved_reference_identitydecidesResolvedToKernelSymbol { symbol } | ResolvedToDeclaration { path }andresolved_reference_nodeis the one producer both doors (bareresolve_atom_bound, qualifiedtry_resolve_qualified_name_node) mint through. The carrier is the qualified-name spine the language already has (v2.std.qualified_name qualified_name_spine_node, the inverse ofqualified_name_from_node; body lowering's copy now delegates to it), read back bydeclaration_reference_path_optional. No new identity vocabulary: the path is what the index key,bound_declarings,LexicalBindingCandidate.path,DeclarationLocus,DeclarationRefandResolutionProvenance.targetalready agree on, andstd.occurrence_binding'sContainmentPath<N>is the same path read as nodes (recorded on that carrier, ruled a declared divergence, not a fork).After resolution a bare
Atom{identity}denotes exactly a kernel canonical symbol, a literal, or a frame-local binder. The kernel arm is the whole of what stays spelling-keyed: a hit whose LEAF is inlm.canonical_symbolsresolves to the kernel atom as before (infer's Bool/Int checks and translate's binding spellings key on it); a corpus twin of a kernel name is a pre-existing fork beside this seam, not widened here.Consequences that fell out: the qualified door no longer needs to read the node's kind, so it now routes through
resolve_atom_bound— the test-code wall has ONE enforcement site instead of two, and the qualified door binds from the single candidate's DECLARING path (not the authored path).SymbolIndexAtomHit.canonical,symbol_index_node_identity,qualified_target_identity_unrepresentable_diagnosticand its cause-ownership row are deleted.Who consumes it (real consumers, by execution)
06_translate translate_algebrainit): a spine is emitted through the target's newTargetTypeExpressionProjection.declaration_reference_form(v2.std.compilers.target_model DeclarationReferenceForm); rust declaresModuleScopedPath { "crate", "::", "_" }(the seed's crate layout, cited at the row); typescript declaresNoDeclarationReferenceFormand refuses^target_declaration_reference_form_absent, located. The encoded bundle carries the row and the decoder reads it back.04_infer infer_gather_fold_initConj arm) and eval (05_eval eval_type_node_atom): a spine is decided BEFORE the Conj arm, so it is never read as a two-field record of its own segments — infer takes the not-derived arm a bare reference took before; eval refuses^eval_rejected_runtime_binding_lookup_missat the reference's locus as a bare miss did before. Binding module-level declarations by path in eval, and deriving a reference's type from its declaration in infer, are each stage's next step (infer's roster-lookup note already names it as its dissolution) and are not taken here.Why the blast radius is confined to v2 translate + fixture claims: the two instrument closures (self-host, native CLI) are emitted by the SEED,
v1.compiler.emit_rust, which does not consume v2's resolved tree at all (nov2_compiler_resolveimport) and already renderscrate::<owner_module_file>::<ident>fromdeclared.owner_module_path. Nothing in either closure changes. That seed lookup is itself the spelling-keyed second answer the brief names, in v1 — out of this PR's route (v1 frozen, four lanes in that file), recorded with the parent as an open row.Evidence (executed locally, each row named)
v2.test.claim.namespace_xl0.cross_module_reference_resolution, 7 rows PASS on this head:two_import_bound_same_leaf_targets_resolve_to_distinct_declaring_paths_holds— two consumers importingxl0r_same_leafbare from provider_a / provider_b each resolve to their own provider's path and not the other's. Mutation control: withresolved_reference_nodemutated to mint the leaf (canonical_atom(identity: last segment)), this row and the qualified twin FAIL whilea_same_module_reference_resolves_on_the_production_route_holdsstill PASSes.two_same_leaf_targets_in_different_modules_resolve_to_distinct_declaring_paths_holds(qualified twin).a_cross_module_reference_to_a_declared_fn_resolves_to_its_declaring_path_holds,a_cross_module_reference_to_a_data_declaration_resolves_to_its_declaring_path_holds(both previously assertedresolve_reason_qualified_target_identity_unrepresentable; both were PASS on the base with that assertion, measured before the cut).a_cross_module_reference_to_an_undeclared_name_refuses_unbound,a_binder_shadowing_a_root_segment_refuses_ambiguous_holds.v2.test.claim.translate.declaration_reference_form(new, inputs SUPPLIED at the fold's boundary; inhabitance of the shape by the real resolver is the xl0r file), 4 rows PASS:a_declaration_reference_emits_the_module_scoped_spelling_holds→crate::v2_test_drf_provider::DrfDeclared.a_declaration_reference_with_no_path_form_refuses_located— the rust projection with its form withdrawn refuses^target_declaration_reference_form_absent.a_bare_atom_still_emits_through_the_atom_row_holds(control).the_rust_target_declares_a_module_scoped_path_form_and_its_bundle_carries_it_holds— subject: the TARGET ROWS (declared form and decoded bundle agree). This is the control the parent asked for; the leaf-collision census below is a different subject and is NOT a control for the refusal.Downstream census (claims outside the floor's diff-touched roster, run locally on this head):
sg2_type_expression_projection22/22 PASS,rust_add_emit_translate3/3,compile_eval_thesis_proof3/3, … (final table in the last commit's comment).nominal_distinctness_cross_call nominal_distinct_control_compiles_okis RED here and RED onmainand on the #12009 head identically (resolve_reason_unbound_symbol @ <synthetic node occurrence "WrapA">on the single-tree staging route) — pre-existing, not this change.Leaf-collision census (condition 1, measured before the cut)
Import-closure walk from each instrument entry over
dag+src/v2(scratch script, recipe in the session; not landed as a claim — it controls nothing in this PR):v2.compiler.compile186 modules / 7301 declarations / 34 same-leaf-in-two-modules (0.47%);v2.cli.compile_cli161 / 6749 / 31 (0.46%). Classes:std.*vsv2.std.*kernel twins (24), per-module annotation-anchordatarows (4), lens fn twins (6). Since the emitted target is module-scoped, none collide and no new refusal fires; the refusal that remains fires only on a target with no path form, whose population among emitted targets is empty and whose red is the fixture row above.Rung (DESIGN 4b, against the authorable test)
Structurally guaranteed (3), not impossible (4). An
Atomnaming a corpus declaration is still constructible in a resolved tree by a fixture or a hand-built node; no Accepted resolved body carries one becausev2.compiler.resolveis the only producer of resolved bodies and its remainingcanonical_atomsites are the frame-local binder (BoundInFrame), the literal, and the kernel arm — enumerable in the file. Per-consumer rungs are stated separately and honestly: translate is at 3 for type positions (the spine cannot reach the record arm); infer and eval are mitigation (typed not-derived / typed miss) until they consume the path.Recorded frontiers (existing carriers, no new doc)
gunbc.recurring_failure_mode refusal_reason_minted_as_canonical_identity: climb receipt appended; its next-rung trigger (a declaration-identity type distinct from Symbol) fired.v2.compiler.resolution_provenance resolution_provenance_second_resolver_dissolve_on: the second resolver is now deletable; trigger = its consumers (repair_input_origin_roster, declaring_identity_spelling_census, the dependency derivation) read the resolved tree by execution. Its sibling rowrepair_input_declared_binding_frontier_dissolve_onalready names the same capability.std.occurrence_bindingstaging note: the v2 instantiation read from the other side — same question, same grain, duplicated 0/1/many fold, layered producers; trigger =LexicalLookup/SymbolIndexAtomLookupretiring intoOccurrenceBindingResult<Node>.v2.workflow.compile_door_cause_ownership: the retired reason's row deleted.Not touched:
v1.compiler.emit_rust(no region needed).🤖 Generated with Claude Code