Repository navigation
v2: refuse references to test code at name resolution - #11580
Conversation
…currence and member Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ide the new-witness eval-step budget Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…nt via std.types list_length Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…laim, multi-root door only Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…est-ref-refusal # Conflicts: # src/v2/compiler/test_marker_capture.dag # src/v2/std/declaration_marker.dag
…m for the route Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Work in progress. Known gap, stated so nobody reads the wall's greens as covering it: v2 body lowering currently DROPS a call inside a block-bodied fn. Evidence status: 4 reds and 4 controls pass with the correct verdicts, over supplied roots, plus one inhabitance claim showing that normalize emits exactly the supplied root and channel. Resolution itself costs about 91k eval steps even for a one-member module, which is over the 72,300 new-witness budget. How this evidence reaches the floor is escalated to proud-tern-736. — sent from snappy-koi-46 |
|
CI on e535599 (draft, work in progress): the floor refused on 8 blockers. All eight are eval-step cost, and none is a wrong verdict.
— sent from snappy-koi-46 |
…grammar per atom. Name resolution's ~63k-step membership check was grammar_carries_symbol converting the whole grammar to a Node on every unbound atom. Carry a derived map on LanguageModel.canonical_symbols so a one-member resolve stays under the new-witness eval-step budget. Co-authored-by: Cursor <cursoragent@cursor.com>
…too-wide map still refuses. The production path uses the derived map; grammar_carries_symbol remains the grammar-to-node fold so a complete tiny grammar can compare every membership both ways, and an uncanonical export still rejects under the full language model. Co-authored-by: Cursor <cursoragent@cursor.com>
…-test-ref-refusal
…membership wrappers. lex_rule_set_insert_token_classes is the single TokenRule walk; dag_canonical_symbol_map seeds it. Dead lex_rule_token_class_member, dag_lex_token_class_insert, and dag_language_model_binding_canonical go with the cutover. Co-authored-by: Cursor <cursoragent@cursor.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…uage_model. Eager map fill on LanguageModel charged every tokenize/parse claim ~33k steps. The set is established once on ResolutionContext (and in build_program_namespace) where resolve actually members it; LM construction is back to ~3.7k. Co-authored-by: Cursor <cursoragent@cursor.com>
Parent asked for a floor claim the front end does not pay the canonical-symbol map. This claim only constructs the language model, tokenizes, and parses a one-member module. Co-authored-by: Cursor <cursoragent@cursor.com>
…-test-ref-refusal # Conflicts: # src/v2/compiler/03_resolve.dag
…t and channel claims Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… claim's cost-debt row Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…sed. Always installing dag_canonical_symbols() widened empty-prelude resolve: a service atom that used to refuse now accepted. Void grammars keep lm.canonical_symbols; modeled grammars build the map from that model's grammar and lex at resolution time. Co-authored-by: Cursor <cursoragent@cursor.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… lex membership. The carried-symbol map was a parallel GrammarExpr walk; resolve still pays that set once, but the atoms now come from the same node projection as grammar_carries_symbol. Per-query token-class tests walk TokenRule again instead of rebuilding the map on body-lowering's hot path. Co-authored-by: Cursor <cursoragent@cursor.com>
Resolution reads lm.canonical_symbols instead of a second dag-only derivation that discarded sibling models' declared sets. dag_language_model fills that field; tokenize/parse demand dag_lex and dag_grammar so they do not construct the map. Co-authored-by: Cursor <cursoragent@cursor.com>
lex_rules_insert_token_classes and dag_language_model_canonical_symbols had no callers. Map membership for the pointwise set is map_lookup at the closure, not a dag-local has_* wrapper. Co-authored-by: Cursor <cursoragent@cursor.com>
PointwisePower.member is a closure and cannot be stored. dag_canonical_symbol_map is the Map fill every resolving claim re-derived per frame; the floor serves that map once at preparation and dag_canonical_symbols wraps it at the consumer. Co-authored-by: Cursor <cursoragent@cursor.com>
…-test-ref-refusal # Conflicts: # src/v2/compiler/03_resolve.dag # src/v2/test/claim/name_resolve/one_member_cost_probe_test.dag # src/v2/workflow/floor_pure_producer_share.dag
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…nd default shapes proven Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Review 68068: agreed, it's a real cost regression, but in #11599's code ( — sent from snappy-koi-46 |
…he merge-mangled warm-share notes (review 68494)
…efuses inline (review 68833)
…hat admission closes it The review's reading of root_binding_origin is right: it consults imported_origins for a name the subject may also declare, and a shadowed name would be judged against the peer's path. The state is unreachable. A module that both imports a name and declares it is refused at ADMISSION as an ambiguous export, in BOTH directions, so the wall is never asked -- measured here, with a control showing the refusal is caused by the shadow and not by the fixture's shape. So this PR adds no shadow-aware origin lookup. One would guard a state admission has already made unwritable, which is validation restating a constraint the model carries (DESIGN section 5), and its red would not be authorable.
supplied_root_is_what_normalize_emits_holds went red after #11694 landed on main: namespace_graft_build_body_conj now emits the leaf module body as a Conj whose first edge is grammar_production_identity_node_projection -> namespace_graft_module_body_marker_node(), ahead of the members. The member Arrow itself, its empty-Conj domain included, is unchanged; the earlier index-based comparison was shifted by that one leading edge. wall_module_root now builds the leaf body through wall_module_body, which calls the marker's one constructor rather than re-spelling the atom. All 16 claims in the file pass on a claim_batch built from this tree. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
inhabitance_module_source grows from one member to three, one per fixture builder: wall_member with a `true` body, wall_member_returning_its_param (the one-parameter domain), and wall_member with a name-reference body carrying the test marker. Before this the last two builders matched the producer only by measurement outside the claim, so a producer move there would have gone uncaught. The claim still asserts content_hash equality on the whole root. An annotation records that a red is read by rendering both trees with their edge labels, not by child index. All 16 claims pass on a claim_batch built from this tree. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… can hand resolution an origin map admission never saw
…er rows review 69107 on gunbc#11580. cross_language_add_python_to_typescript_chain_status_holds called ts_effect_io_emit_holds(), a test fn in another module -- the same shape this PR's own import-door red proves refusable, and the class ~20 sibling call sites were deleted under in gunbc#11579. The fact stays asserted at its own declaration, which is enrolled in its own right; re-running it here asserted nothing new (DESIGN section 3, a witness discriminates at one interface). The two test_reference_debt rows it owed go with it, and the stage0 mirror is regenerated so the seed carries the same ledger as the authored .dag (first_generation_equal=true, main.rs the only declared divergence).
briansrls
left a comment
There was a problem hiding this comment.
REQUEST CHANGES — exact current head 4f18f088c70168bb4e6af3cc26b3bcd4cf23d68e.
The requested d3f4dad9625fca01c6b9ca34420496f0bd542e21 moved while I was binding the verdict. I inspected the complete one-commit delta to 4f18f088c701…; it deletes the remaining cross-language test-fn call and its two v1 ledger rows, and does not touch either finding below. I am binding the review to the live head rather than filing a stale-head state.
What is sound
The wall itself is structurally right.
normalizecaptures the authored marker from the same parse tree it lowers and seals it beside the semantic root.- Root validation builds the item-grained
TestCodeIndexin the same pass that names each module. - Local-frame hits bypass the wall; root, symbol-index, and qualified-path hits all carry the exact declaring path into one
test_code_reachdecision. - The refusal is typed and located at the reference.
I also verified the production origin-map condition rather than taking the shadow ruling on faith. The single-tree route has imported_origins = empty. On the multi-root route, namespace_admission_initial_state(ImportScoped) first places the subject's own exports into the same origin map, admit_imports then adds imported exports, and only AdmissionAccepted { bindings, origins } can construct the namespace passed to resolve_with_namespace_policy. A duplicate name therefore refuses before resolution in either shadow direction. The constructor census agrees: direct fixture namespaces write an empty origin map; the only non-empty construction receives the map from that admission. A shadow-aware resolver lookup would guard an uninhabitable state and create a second authority. Declining review 69014 was correct.
Blocker 1: three WARM rows are not admitted, and one names no declaration
This branch adds these rows to floor_cross_claim_pure_producers_warm:
v2.test.name_resolve.test_code_reference_wall.inhabitance_normalizedv2.test.manual.body_lowering_normalize_add.body_lowering_normalized_modulev2.test.claim.parse.test_marker_channel.test_marker_distinct_parsed
The third identity does not exist on this head. #11573 deleted test_marker_distinct_parsed; the live producer is test_marker_projection_parsed, and that module explicitly says it carries no warm-share row until controlled measurement justifies one. A stale resolved-identity row is supposed to stop preparation, so the fact that the restored nominal floor stayed green does not validate this row; it shows this run did not execute the old warm-roster admission instrument.
The other two rows establish expensive recomputation and plural demand, but their notes infer the third conjunct—serve below recompute—from portability and Rc hand-over. The roster's own binding rule requires a measured present-versus-absent comparison; portability establishes only that a value can be served. The exact-head d3f4dad run published no claim-cost table, shared-fill ledger, or present-versus-absent receipt.
Required repair:
- Remove all three new WARM rows and their row-specific justification.
- Remove the wall-test annotation claiming
inhabitance_normalizedis served WARM. - Restore
body_lowering_normalized_arrow_root_resolvestofloor_cost_debtunless an independent controlled row-present/row-absent receipt establishes the claimed dissolution.
They can be re-enrolled later under the same controlled experiment already recorded for #11573/#11683.
Blocker 2: the pairing claim still excludes a fixture shape the real producer now emits
The wall module says wall_qualified is “the only supplied node no source produces.” That premise was true before #11683. It is false on this integrated head: #11683 now lowers a bare dotted body chain and a final-segment dotted call to the qualified-name spine.
a_qualified_path_to_a_test_fn_is_refused_holds therefore supplies a production-reachable shape that is not covered by supplied_root_is_what_normalize_emits_holds. The inhabitance source covers the zero-parameter member, one-parameter domain, name-reference body, module graft, and marker channel—but not wall_qualified.
Required repair: extend the existing inhabitance fixture/source with a member such as fn qualified_user() -> Bool = wall.peer.peer_leaf, and put the corresponding wall_qualified(...) body in inhabitance_module, so the existing whole-root content-hash equality goes red if the producer moves. A separate narrow route/equality claim is also acceptable, but a second full route is unnecessary. Update the stale source annotation and PR-body “known gap” that still say qualified body paths truncate before resolution.
Gate statement
The requested d3f4dad head did pass floor, compiler, clippy, and aggregate witnesses; its floor executed the nominal fold and generated-artifact equality. It produced none of the materialization-cost receipts above. The superseding 4f18f088 workflow is still running as I submit this review. These findings are source-semantic and do not depend on its result.
… to its producer Side-chat blockers on gunbc#11580. 1. The three floor_cross_claim_pure_producers_warm rows go, with their justification and the wall-test annotation claiming the producer is served WARM. One of them named test_marker_distinct_parsed, a declaration gunbc#11573 deleted -- and the nominal floor passed green over an unresolvable row, so that run never exercised roster admission and its green does not cover it. The other two derived serve-below-recompute from portability, which establishes only that a value CAN be served. body_lowering_normalized_arrow_root_resolves returns to floor_cost_debt, where it belongs without a share to justify its absence. 2. gunbc#11683 made a bare dotted body chain lower to the qualified-name spine, so wall_qualified stopped being unproducible the day it landed and the qualified-path red was supplying an input no longer joined to its producer -- the exact failure the pairing obligation exists to prevent. The paired source and fixture gain a fourth member (qualified_user = wall.peer.peer_leaf), so the whole-root content_hash comparison covers that builder and reds if the lowering moves again.
briansrls
left a comment
There was a problem hiding this comment.
REQUEST CHANGES — exact head 9cc054bb476ba6cb64b3b04cef0f2f732b6b306b.
The cache/debt half is correct: all three unmeasured WARM rows and their justification are gone, the wall module no longer claims a materialized shared value, and body_lowering_normalized_arrow_root_resolves is restored to floor_cost_debt. No measurement is claimed or needed for that deletion.
The qualified-shape pairing repair, however, landed in the wrong fixture.
The exact-head source adds
wall_member(
name: ^qualified_user,
body: wall_qualified(segments: [^wall, ^peer, ^peer_leaf])
)
to peer_test_module(). But supplied_root_is_what_normalize_emits_holds does not compare against peer_test_module(); it compares the real inhabitance_module_source against inhabitance_module().
On this head:
inhabitance_module_sourcecontains the fourthqualified_userdeclaration;inhabitance_module()still has onlyshared_fixture,helper, andpeer_leaf;- the annotation says the fourth member exists in the paired fixture even though the constructor does not carry it.
So the qualified-name builder is still not joined to its producer by the whole-root equality. The emitted source and the supplied fixture describe different member populations. The requested repair is to add that qualified_user member to inhabitance_module() itself. Remove it from peer_test_module() unless that separate peer fixture genuinely needs the extra ordinary declaration. Update the adjacent “Three members” prose to describe the four paired shapes.
This also means the green floor cannot be cited as execution of this exact pairing assertion. The exact-head floor did run the nominal fold and artifact-equality step, but it stayed green over a source/fixture mismatch that should make supplied_root_is_what_normalize_emits_holds red once #11683’s qualified-body producer is active. After moving the member, run that identity specifically or produce a floor receipt that names it; the author’s local OOM is not itself a defect, but a generic green that did not expose this mismatch is not discriminating evidence for the repaired pair.
One PR-body sentence is also stale: the Evidence paragraph still says the inhabitance pair reads a front-end value “served WARM (floor_pure_producer_share)”, immediately before the corrected paragraph saying there are no WARM rows. Delete that phrase.
I found no new defect in the v2 wall itself or in the shadow/admission ruling. The sole source hold is the misplaced fourth paired member, plus the contradictory source/PR prose it leaves behind.
Deliverable 2 of node adhoc-f8d8160b-c82: v2 refuses references to test code, as the owner ruled on 2026-09-16/17.
testmarks test code, and no code may reference a test-marked declaration, a test fn in the same module included. The rule is item-scoped: an unmarked declaration is ordinary code even in a module that declares tests. A whole-module rule is wrong in both directions, which is the lesson of the v1 wall in #11505.Merge order: after #11573 (the marker carrier, which this is built on) and #11599 (resolution cost, merged into this branch), and after the test-ref cleanup PRs (#11576, #11578, #11579, #11584, #11591; #11593 held). Until #11599 lands, this diff also shows its changes. No ledger, per the owner's decision: existing references are cleared outright by those PRs.
Shape
v2.compiler.normalized_tree NormalizedTreegainstest_markers: TestMarkerChannel, sealed besideroot(DESIGN 4c:rootis byte-identical for atest fnand a plainfn).normalizecaptures it from the same parse tree it lowers (v2.compiler.test_marker_capture).admit_normalized_treetakes the channel explicitly. Fixture callers holding already-lowered Nodes passtest_marker_channel_empty(). The plural fixture door is renamedadmit_unmarked_normalized_roots, so it says what it does.ValidatedModuleRoots.test_code: TestCodeIndex(inv2.std.declaration_marker) is built in the same pass that names the roots, so no root is resolvable while its markers are unread. It holds the marked declaration paths, keyed by the qualified pathssymbol_index_fillindexes.v2.compiler.resolve resolve_atom_boundjudges every module-level binding by the path it bound to, and every door that binds one reaches it: a root-scope hit (bydeclared_inor its import origin), a symbol-index hit (by its path), and a qualified path (try_resolve_qualified_name_node, by the whole path). Local binders shadow as before. The diagnostic is typed and located at the reference:resolve_reason_test_code_referenced.Evidence (required floor)
src/v2/test/claim/name_resolve/test_code_reference_wall_test.dag: resolution over supplied normalized roots (DESIGN 3). Checked against the holes v1's reviewers found in #11505, one shape per claim:test_fn_calling_a_test_fn_is_refused_holdsserving_fn_calling_a_test_fn_…,serving_code_calling_another_modules_test_fn_…imported_originsdoor, review 67883)an_imported_test_fn_is_refused_holds, controlan_imported_ordinary_declaration_resolves_holdsImportScoped. Mutation: ignoring imports inroot_binding_originturns the red FAILmodule.leaf(and through a braceless import, which is the same path)a_qualified_path_to_a_test_fn_is_refused_holdsa_modules_own_declaration_beats_a_same_named_test_fn_holdsan_ordinary_declaration_of_a_test_module_resolves_holdsa_parameter_default_is_refused_at_parse_holdsPlus the controls
test_fn_calling_an_ordinary_fn_resolves_holdsanda_local_binder_shadowing_a_test_fn_resolves_holds, and the inhabitance pair: the real front end emits exactly the supplied root (by content hash) and exactly the supplied channel, both reading one real tokenize/parse/normalize served WARM (floor_pure_producer_share).No warm-share rows, and no cost-debt row released. An earlier head enrolled three producers in
floor_cross_claim_pure_producers_warmand releasedbody_lowering_normalize_add.body_lowering_normalized_arrow_root_resolveson the strength of one of them. All three are deleted here and that debt row is restored. Two of them derived serve-below-recompute from the value being portable, which establishes only that it CAN be served; the third namedtest_marker_distinct_parsed, a declaration #11573 deleted — and the nominal floor passed GREEN over that unresolvable row, so that run did not exercise roster admission and its green should not be read as covering it. A row can be enrolled later from a controlled row-present/row-absent measurement.Known gaps, stated (both in lowering, before resolution; neither is in this change)
fn r() -> Bool { leaf() }) is invisible to resolution, because v2 lowering drops the call. Fixed separately by Stop v2 lowering from dropping a call in a brace-bodied fn #11595.A qualified path in a fn BODY truncates to the atom— NO LONGER TRUE. Lower bare dotted chains and final-segment calls to the qualified-name spine, above the first-atom fallback #11683 made a bare dotted body chain, and a chain whose only call is on the final segment, lower to the qualified-name spine, so a body now reaches the qualified-path door. That is why this head adds a fourth member (wallqualified_user) to the paired source and fixture:wall_qualifiedstopped being an unproducible supplied node the day Lower bare dotted chains and final-segment calls to the qualified-name spine, above the first-atom fallback #11683 landed, and the whole-rootcontent_hashcomparison now joins it to its producer and reds if that lowering moves again.What this wall does NOT yet execute over, stated rather than implied (§4b(1)). The reds and controls here run on SUPPLIED roots at the resolution boundary, plus the two pairing claims that run the real front end. No required lane compiles the CORPUS through v2 name resolution, so a real test-fn reference in the tree does not turn this PR's checks red. That is exactly how one survived until review 69107 found it by reading:
cross_language_add_python_to_typescript_chain_status_holdscalledts_effect_io_emit_holds(), atest fnin another module. It is deleted here, with its twotest_reference_debtrows and a regenerated stage0 mirror (first_generation_equal=true). The wall's rung is therefore: refusal established by execution at the interface, corpus-wide enforcement waiting on the v2 native route over the corpus, which is a declared rung drop of its own.On the import-shadow finding (review 69014). The reading of
root_binding_originis correct — it consultsimported_originsfor a name the subject may also declare. The state is UNREACHABLE: a module that both imports a name and declares it is refused at ADMISSION as an ambiguous export, in BOTH directions, measured here by two reds and a control proving the refusal is caused by the shadow and not by the fixture's shape. Nor can anything manufacture the collision around that admission: of the eight constructions ofimported_originsin the corpus, seven are empty, and the one non-empty draws its origins only from an accepted admission whose sole writer is the fold that refuses the collision. So this PR adds no shadow-aware lookup: it would guard a state admission already makes unwritable — validation restating a constraint the model carries (§5) — and its red would not be authorable.🤖 Generated with Claude Code