Skip to content

D1 A: parse type-alias where refinements - #10946

Merged
briansrls merged 14 commits into
mainfrom
session/witty-boar-671
Sep 11, 2026
Merged

briansrls merged 14 commits into
mainfrom
session/witty-boar-671

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Sep 10, 2026 •

Copy link
Copy Markdown
Contributor

Summary

  • v2 dag grammar now parses a type-alias where clause (type A = T where brand("A")) by attaching the clause to dag_production_type_variant, not to every type_expr.
  • Empty where still refuses. Later D1 causes (G, K+L, E, M, J) are not in this PR — each will be a separate PR based on main.

Test plan

D1 acceptance bar: cause A is gone from every attributed subject; no previously accepted member regresses; newly exposed causes are recorded; the where structure survives parse and normalize in its intended modeled form. Never “the file leaves the refusing set”.

Required CI is build + floor. The head-bound srv2 167-member cause-relative closure receipt is the required native semantic evidence: it establishes the self-host compiler closure and this PR’s cause-relative delta, not whole-v2.test.* native admission, and does not retire v2_native_route_off_the_merge_path.

Current receipt (eager-raven-113, head 5da6623579 overlaid on main 0423c33770, 167-member closure, controls-only): 68 → 67, zero regressions — identical to 195f41f4, bound to this head.

file outcome
dag/std/cache_identity.dag RefusalCleared
src/v2/std/compilers/target_model.dag AdvancedToNewCause → match-arm (cause D, #10967)
dag/std/cache_interface.dag still parse, co-occurring cause O (not A)
dag/std/content_hash.dag still parse, co-occurring G, H, K, M (not A)
dag/std/integer.dag still parse, co-occurring cause J (not A)

Lands after #10988 → D2 → D3. Emitter class / native-route drop are unchanged.

@gunbai-bot gunbai-bot Bot changed the title Parse and carry v2 where-refinement clauses D1: declaration-level dag grammar (where, eq-fn, sole_constructor, variants, numeric type args) Sep 10, 2026
v2 had no production for a type-alias `where` refinement, so the six closure files never entered the tree. Attach the clause to the variant (the alias RHS), not to every type_expr, so fn return types stay the shape body-lowering already lowers. Empty `where` still refuses. Later D1 causes are not in this PR.

Co-authored-by: Cursor <cursoragent@cursor.com>
@gunbai-bot
gunbai-bot Bot force-pushed the session/witty-boar-671 branch from d9d395d to 9e4bb2f Compare September 10, 2026 17:13
@gunbai-bot
gunbai-bot Bot marked this pull request as draft September 10, 2026 17:14
@gunbai-bot gunbai-bot Bot changed the title D1: declaration-level dag grammar (where, eq-fn, sole_constructor, variants, numeric type args) D1 A: parse type-alias where refinements Sep 10, 2026
@gunbai-bot

gunbai-bot Bot commented Sep 10, 2026

Copy link
Copy Markdown
Contributor Author

review 63162 asked to keep = expr off the shared fn_body production (block / if / fn-literal consumers; DESIGN §3; D1 vs D5).

Verified on current head 9e4bb2f5bc4: dag_grammar_fn_body_expr is brace-only (lbrace / stmt_seq / rbrace). Formal productions for dag_production_fn_body are the same two brace forms. fn_decl still consumes that braced fn_body. There is no = expr arm on this PR.

That = expr hung on fn_body on an earlier stacked commit that is no longer on the branch. #10946 is cause A only. Cause G will be a later PR based on main, with = expr only on dag_grammar_fn_decl_expr (or a decl-only production), leaving fn_body braced for block/if/literal.

— sent from witty-boar-671

Floor CI refused the changed parse identities with no verdict: they rebuilt
the grammar inside the 500ms claim budget. Use dag_prepared_grammar instead.

Co-authored-by: Cursor <cursoragent@cursor.com>
@gunbai-bot

gunbai-bot Bot commented Sep 10, 2026

Copy link
Copy Markdown
Contributor Author

Fixture receipt at 9e4bb2f5bc4 (srv2 aarch64, cargo 1.93.0, claim_batch --claim-run, 48 GB scope, RUSTC_WRAPPER unset; seed built from this sha in 7m46s).

src/v2/test/claim/parse/d1_declaration_grammar_parse_test.dag — exit 1

PASS cause_a_where_refinement_clause_parses_holds
PASS cause_a_where_clause_parse_tree_carries_holds
PASS cause_a_where_control_normalizes_holds
PASS cause_a_where_reproducer_normalizes_holds
FAIL cause_a_where_clause_survives_normalize_holds
PASS cause_a_empty_where_clause_refuses_holds

src/v2/test/claim/parse/where_refinement_clause_parse_test.dag — exit 1

PASS where_refinement_clause_parses_and_is_carried_holds
FAIL where_refinement_clause_survives_normalize_graft_holds
PASS where_refinement_empty_clause_is_refused_holds

Reading: the clause is parsed and present on the parse tree, and the empty-where red refuses; it does not survive normalize/graft on either entry. That is the accept-then-erase shape the brief rules out (DESIGN §5 absorbing fallback), so this head is not yet the repair. The 167-file closure run waits for a head where both survives_normalize* arms pass.

Graft unfolds `_node_projection` shells at the module body, so a preserved
where production was dissolved after an Accepted normalize. Attach the clause
as a named child so both survives_normalize arms can still find it.

Co-authored-by: Cursor <cursoragent@cursor.com>
@gunbai-bot

gunbai-bot Bot commented Sep 10, 2026

Copy link
Copy Markdown
Contributor Author

Fixture receipt at 66008cf0f92 (same rig: srv2, claim_batch --claim-run, 48 GB scope, RUSTC_WRAPPER unset; seed 7m36s).

Identical tally to 9e4bb2f5bc4: 7 PASS / 2 FAIL — cause_a_where_clause_survives_normalize_holds and where_refinement_clause_survives_normalize_graft_holds still FAIL (549 ms, subject cbc73b1988668690). The rehome onto dag_surface_where_refinement_clause did not change the outcome on the admitted tree. The witnesses are Bool, so the receipt carries no locus; see the lane note for the ask.

Brian Searls and others added 6 commits September 10, 2026 17:48
A Named where-edge whose target was still a production shell stayed
transparent to graft. Wrap the clause so the kept target is not all
_node_projection children, and return Witness<Node> (Suggested host)
when the production is absent from the admitted tree.

Co-authored-by: Cursor <cursoragent@cursor.com>
The if-then Present { value: root } arm typed as Node against the else
fold's Optional<Node>, so neither entry resolved.

Co-authored-by: Cursor <cursoragent@cursor.com>
--claim-run entries must return Bool. The Witness<Node> form is
cause_a_where_clause_survives_normalize_locus and
where_refinement_clause_survives_normalize_locus for gunbc run --function.

Co-authored-by: Cursor <cursoragent@cursor.com>
gunbc run renders String and not Witness<Node>. Claim-run survives
arms stay Bool; the companions join edge labels and find=true/false.

Co-authored-by: Cursor <cursoragent@cursor.com>
Kernel join builds ExitFailure.reason (std.process has reason, not
message). ExitSuccess when parse_subtree_find still sees the clause.

Co-authored-by: Cursor <cursoragent@cursor.com>
The companion only ran the brand fixture; the Bool arm also required
bare `where non_empty`. where_refinement Bool now uses the same file
symbol as its companion.

Co-authored-by: Cursor <cursoragent@cursor.com>
@gunbai-bot

gunbai-bot Bot commented Sep 10, 2026

Copy link
Copy Markdown
Contributor Author

Fixture receipt at 85324204b98 (srv2, claim_batch --claim-run, 48 GB scope, RUSTC_WRAPPER unset): 9/9 PASS, both entries exit 0.

PASS cause_a_where_refinement_clause_parses_holds
PASS cause_a_where_clause_parse_tree_carries_holds
PASS cause_a_where_control_normalizes_holds
PASS cause_a_where_reproducer_normalizes_holds
PASS cause_a_where_clause_survives_normalize_holds
PASS cause_a_empty_where_clause_refuses_holds
PASS where_refinement_clause_parses_and_is_carried_holds
PASS where_refinement_clause_survives_normalize_graft_holds
PASS where_refinement_empty_clause_is_refused_holds

The clause is parsed, carried on the parse tree, and survives normalize + graft on the admitted tree; the empty-where red still refuses. Next: the 167-file closure before/after at the PR head (209def17), posted here when it lands.

@gunbai-bot

gunbai-bot Bot commented Sep 10, 2026

Copy link
Copy Markdown
Contributor Author

Closure before/after for cause A — measured on a local, unpushed merge of #10882 head 25d1c7973bc + this PR at 209def17cc5 (main's emitted closure does not compile without #10882's 285b02eed29; merge-tree clean). srv2 aarch64, seed 7m21s, lane emit 172 files (closure 528a7cb7d1c7…), emitted driver folded over a root holding exactly the 167 closure files with a controls-only universe: [wall 275.61s rss 1228000kB], {"_terminal":"complete","file_refusals":68,"rows":2}.

68 → 68. Zero files left the refusing set, zero entered. Terminal causes by class: graft 25 (unchanged), parse 24 (was 26), match-arm 9 (was 8), lexer 8 (unchanged), wrapper-retention 1 (unchanged), normalize_reason_post_normalize_not_well_formed 1 (new).

Per-file terminal-cause changes (before = #10943 carrier at 2fb67b411a):

  • dag/std/cache_identity.dag: parse_g0_tokens_remain → normalize_reason_post_normalize_not_well_formed — the where clause now parses, but the carried refinement node fails the post-normalize well-formedness law. This is a D1 defect to close before un-draft: the carrier must be a shape normalized_tree admits.
  • src/v2/std/compilers/target_model.dag: parse_g0_tokens_remain → body_lowering_reason_match_arm_navigation_refused — progressed to its next cause (D, single-arm match), as expected.
  • The other A-carrying files (cache_interface.dag etc.) still stop at parse_g0_tokens_remain because they carry a second parse cause (co-occurrence per the carrier).

Reading: the grammar repair is correct and regression-free at closure grain; acceptance for this PR is the cache_identity.dag row leaving normalize_reason_post_normalize_not_well_formed.

Brian Searls and others added 4 commits September 10, 2026 20:10
Grammar-prepare fill exceeds required_floor_claim_cpu_safety_limit_ms, so
enrolling them as test fn witnesses interrupted before verdict and blocked
the floor lane. They stay claim_batch functions.

Co-authored-by: Cursor <cursoragent@cursor.com>
De-enrolling made the predicates undiscoverable; interpreted-floor
interrupted_before_verdict stays a runner-capacity problem, not an
enrollment waiver.

Co-authored-by: Cursor <cursoragent@cursor.com>
Two brand-refined aliases failed post-normalize well_formed because graft
unpacked duplicate where edges onto one Conj. Each alias is now Named by
its lexeme, and the clause is a production-shaped Conj over a predicate Atom
rather than the parse shell.

Co-authored-by: Cursor <cursoragent@cursor.com>
…native.

#10882 is on main; keep a merge commit (no rebase).
@gunbai-bot

gunbai-bot Bot commented Sep 10, 2026

Copy link
Copy Markdown
Contributor Author

Closure before/after for #10946 at head 195f41f42f, overlaid on main 0006e0aabd (PR diff from merge-base 077b771c3f applied, no unmerged paths; srv2, emitted driver over the 167-member closure root, controls-only universe, {"_terminal":"complete","file_refusals":67}, wall 286 s, rss 1.2 GB). Baseline: the #10943 carrier at 2fb67b411a, 68 refusals.

68 → 67. Zero regressions (no previously accepted module refuses; no non-A file changed cause). Cause A is discharged on every file the carrier attributes to it:

file carrier causes outcome
dag/std/cache_identity.dag A RefusalCleared (was parse_g0_tokens_remain, then normalize_reason_post_normalize_not_well_formed at the previous head; now accepted)
src/v2/std/compilers/target_model.dag A AdvancedToNewCause → body_lowering_reason_match_arm_navigation_refused (cause D, owned by #10967)
dag/std/cache_interface.dag A, O still parse_g0_tokens_remain — the co-occurring cause O speaks next; A cannot be observed separately at the terminal grain
dag/std/content_hash.dag A, G, H, K, M still parse_g0_tokens_remain — co-occurring causes
dag/std/integer.dag A, J still parse_g0_tokens_remain — co-occurring cause J

The two sole-A files are the discriminating evidence: both left cause A, one to acceptance and one to its next cause. The three multi-cause files are StillBlocked by a cause this PR does not own, not by A. Terminal-cause histogram after: graft 25, parse 24, match-arm 9, lexer 8, wrapper-retention 1.

This satisfies the cause-relative acceptance (A ceases on every attributed file; each accepts or advances to a typed cause; no accepted member regresses). Ready to leave draft once the PR body states that bar instead of "six files leave the refusing set".

… authority.

Keep a merge commit (no rebase). A required-v2-native 180-minute kill is not this PR's red.
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review September 10, 2026 21:27
@gunbai-bot

gunbai-bot Bot commented Sep 10, 2026

Copy link
Copy Markdown
Contributor Author

Refreshed closure receipt for #10946 at head 5da6623579 (PR diff from merge-base a4b21cb8e4 overlaid on main 0423c33770; srv2 private base clone; emitted driver over the 167-member closure root, controls-only universe; {"_terminal":"complete","file_refusals":67}, wall 308 s, rss 1.2 GB; instrument digest 815a9684d69a0651). Baseline: #10943 carrier at 2fb67b411a, 68 refusals.

Identical to the 195f41f4 result: 68 → 67, zero regressions. Cause A: dag/std/cache_identity.dag RefusalCleared; src/v2/std/compilers/target_model.dag AdvancedToNewCause → body_lowering_reason_match_arm_navigation_refused; cache_interface / content_hash / integer still stop at parse on their co-occurring causes (O / G,H,K,M / J). No accepted module regressed; nothing earlier-stage. Histogram after: graft 25, parse 24, match-arm 9, lexer 8, wrapper-retention 1.

This receipt binds to 5da6623579. Landing position: third, after #10963 and #10969.

@briansrls
briansrls merged commit c176027 into main Sep 11, 2026
2 of 5 checks passed
@briansrls
briansrls deleted the session/witty-boar-671 branch September 11, 2026 02:51
briansrls pushed a commit that referenced this pull request Sep 11, 2026
…, and share the parse-witness fixture trees warm (#11032)

SYMPTOM: main's required floor is red -- ten identities INTERRUPTED-BEFORE-VERDICT at
the 500ms per-claim CPU ceiling (cpu_at_least=506-610ms, right-censored) since #10946
and #10961 landed: the seven where-clause rows of
v2.test.parse.d1_declaration_grammar_parse, the two carried/graft rows of
v2.test.parse.where_refinement_clause_parse,
v2.test.claim.body_lowering.declaration_structure_preserved
.where_refinement_clause_interior_is_not_retained_holds, and
v2.test.parse.expression_bodied_fn_decl_parse.braced_fn_decl_survives_normalize_holds
(runs 34556215902, 34556223550, 34560949186). No floor run has ever reached their
verdict.

COST SHAPE, measured not inferred. Uncensored (claim_batch, uncontended amd64 host)
the ten complete at 318-523ms; the eight file-mate rows that DID complete in run
34556223550 put the lane's runner at 1.4-2.1x that host, so the real cost was
~510-840ms -- structurally over, not marginal. The run's own cross-claim demand census
names the halves: parse_grammar_digest at claims=19 evals=19 (~128ms per claim) plus
two grammar_to_node walks per claim, every one keyed on the warm-shared prepared
grammar -- a once-per-grammar invariant rebuilt on every parse call, the finding
#10992's write-up flagged for a separate lane -- and, under it, one module-constant
source tokenized and parsed by two to four claims of one file, once per claim frame.
Same class as #10992 (a shared precondition re-derived per claim frame), third
instance.

REPAIR, at both homes, never the line:
- v2.compiler.parse: GrammarFirstAnalysis now carries grammar_digest and
  productions_by_name, computed once in compute_grammar_first_analysis_given (so once
  per prepare_grammar) and read by parse_table_for_production_analyzed; the grammar's
  own locus, read only by the rejection arm that carries no diagnostic of its own, is
  derived on that arm alone. Every claim that parses .dag text inherits this.
- The three parse-witness files share each multi-consumer source at the parse tree
  through nullary producers enrolled WARM in v2.workflow.floor_pure_producer_share
  (eight rows); normalize stays per claim. Single-consumer sources are not shared, and
  the one three-source conjunction is split into three rows.

Measured on the uncontended amd64 host after the parser repair alone (before the
share): 101-460ms per claim, every row under the line; the share then removes the
remaining per-claim tokenize+parse (~130-170ms each) from the multi-consumer rows.
Positive control by execution: with the where clause removed from type_variant and
the `= expr` arm removed from fn_decl, the where-carrying rows of all three
where-families and the four expression-bodied rows FAIL while their controls PASS;
grammar restored byte-identical. No assertion deleted or weakened; no ceiling change.


Claude-Session: https://claude.ai/code/session_01YApoxsmnC96ad2nWpRJdja

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant