Repository navigation
v2: carry the test marker and refuse references to test code - #11882
Closed
gunbai-bot[bot] wants to merge 91 commits into
Closed
gunbai-bot[bot] wants to merge 91 commits into
gunbai-bot[bot] wants to merge 91 commits into
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>
…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>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
dag_symbol_map_put was a second name for grammar_symbol_map_put. Nested puts become one fold over a symbol list. Co-authored-by: Cursor <cursoragent@cursor.com>
…-test-ref-refusal
…ule: resolution consumes it Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The atom walk inserts into the Map as it goes, so there is one authority and no quadratic list concat. grammar_carries_symbol no longer has a second fold. Co-authored-by: Cursor <cursoragent@cursor.com>
… fixture Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
# Conflicts: # src/v2/workflow/floor_pure_producer_share.dag
…-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
…lve-on is met by this channel Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
# Conflicts: # src/v2/compiler/03_resolve.dag # src/v2/workflow/floor_pure_producer_share.dag
…eBinding; check test code before the qualified target's shape Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…new-witness step budget after main moved Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…est-ref-refusal # Conflicts: # src/v2/workflow/floor_pure_producer_share.dag
…e line scan at its real trigger Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…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).
… 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.
Contributor
Author
|
Duplicate: this is branch — sent from snappy-koi-46 |
6 tasks
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
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.
Auto-opened by session-dashboard for session
snappy-koi-46.Pushing to
v2-test-ref-refusaladvances this PR.Worker attestation
Before flipping this PR to ready for review, confirm each item:
npm test,cargo test) and the result.Closes #Ndirective.Summary
TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.
Test plan