Skip to content

Native parse of the workload closure: the dag grammar gains the leading-pipe coproduct and the positional variant payload - #11998

Closed
gunbai-bot[bot] wants to merge 9 commits into
mainfrom
session/gentle-tern-521
Closed

gunbai-bot[bot] wants to merge 9 commits into
mainfrom
session/gentle-tern-521

Conversation

@gunbai-bot

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

Copy link
Copy Markdown
Contributor

Subject

The native adjudicate of //v2/test/parse/expression_bodied_fn_decl_parse:all (133 modules, universe 7) on the integration branch (#11952). Before this PR, the native front end refused dag/std/content_hash.dag and other closure files with parse_g0_tokens_remain. Note that the originally briefed spelling //v2/test/parse:expression_bodied_fn_decl_parse names no declaration under #11919, which is why it selected 13 std modules and universe 0.

Boundary

The single dag grammar, v2.extdeps.languages.dag, which the native front end and the seed-run v2 parser both read. No second parser, and no edits to corpus files to dodge the parser. Each construct was found by bisecting with the v2 parser under the seed.

  1. A coproduct opening with | (type H =\n | A\n | B). The separator gets its own production, dag_grammar_type_alias_rhs_lead_expr, placed before the type_alias_rhs nonterminal. The sugar rule sugar_rule_type_alias_rhs_lead lowers it to the rhs, and body_lower_is_structure_preserved_emitted treats it as structure. As a result, = | A | B and = A | B normalize to the same provenance-free tree. A lone | with nothing after it is still refused.
  2. A variant with a positional payload (Fnv1a64(Fnv1a64Structural)). A new production, positional_variant_payload, is offered beside field_decl_block, and only in a variant's field slot. As in v1, arity is one, so A(X, Z) and type R(X) are still refused. The two consumers that classify fielded variants now name it too: namespace_graft_type_decl_is_fielded (a single predicate now shared by both former copies of the check) and body_lower_is_structure_preserved_emitted.

Parity, declared: fields and binders are unlowered for both spellings

Positional and record variants are equally unlowered today. No v2 stage lowers variant fields into declared field identities for either A { v: T } or A(T). The match-arm lowering keeps only a pattern's constructor, so binders are dropped for both spellings (confirmed with a probe). In the normal case the loss is loud, because resolve refuses the unbound name. It is silent in one case: a match binder dropped on the native route that shadows an outer name silently uses the outer value. Per the manager's ruling (declare and defer; building the shadow check here would add a throwaway tree shape that Pkg11c replaces), this is declared in ONE rung drop, gunbc.rung_drop variant_fields_unlowered_on_the_native_route:

  • Population: the native lane.
  • Trigger: Pkg11c lowers match binders.
  • Evidence rule: until it fires, no native test PASS through a dropped-binder arm is evidence.

docs/design-rung-drops.md is regenerated. Pkg11c (quick-bat-813) is building the lowering.

Controls

The witness module is v2.test.parse.coproduct_leading_pipe_and_positional_payload_parse. It runs on the prepared-grammar parse and normalize, 9 claims:

  • Leading pipe: a multi-line sum parses and normalizes; the single-line form parses; a bare | refuses; = | A | B and = A | B give an equal provenance-free tree; and A | B vs A | C must differ (the discriminating half of that equality).
  • Positional: type C = A(X) | B { n: Int } | D (no leading pipe) parses and normalizes; A(X, Z) refuses; type R(X) refuses; A(_) => (binds nothing, loses nothing) normalizes.
  • Independent mutations, each run with the other rows present:
    • Removing only the leading-pipe row: every leading-pipe claim goes red; the positional claims stay green.
    • Removing only the positional row: only the positional claims go red.
    • Removing only the lead sugar rule: only the equality claim goes red.

Workload rerun (native, local, integ b52c7b5 + this PR)

  • Last full run was at 34ae973. It predates the removal of the binder refusal.
    • 15 file refusals. One was std/content_hash.dag, refused by the positional binder refusal that has since been removed. I have not rerun the lane since the removal.
    • All 7 workload tests reach prepare and refuse at resolve: resolve_ambiguous_on_global_bare on SubstrateInputsOnly. That is past parse and outside grammar.
  • The remaining classes are reported to the manager as follow-on work:
    • Parse: return, an int literal as a generic arg, the keyword module used as a param name or arg label, and an anonymous record alias.
    • Postfix: call-result .field in tail position, and module-qualified record construction. Both go to Pkg11c.

Disposition

This PR replaces nothing; it adds rows that were missing. It does not overlap #11911 (expression choice order) or #11114 (removes dag_formal_productions; this PR adds no formal-productions rows).

🤖 Generated with Claude Code

gunbc-ci-auto-heal and others added 9 commits September 21, 2026 19:00
…e frontier for unlowered variant fields

Side-chat hold on 318a377: the leading | now has its own production
(type_alias_rhs_lead) lowered by sugar to its rhs, so '= | A | B' and
'= A | B' normalize to the same provenance-free tree. Positional match
binders, which the match-arm lowering silently dropped, are a typed
refusal (body_lowering_reason_positional_pattern_binder_unlowered, cause
row in compile_door_cause_ownership). Record and positional variant
fields are equally unlowered on the native route; one rung drop,
variant_fields_unlowered_on_the_native_route, names that frontier.
Witness grows a construction specimen, the refusal, a braced control,
the equality and its discriminating negative.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… loses nothing and lowers

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…g it; witness cites the lead production by its real name (review 69768)

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… the type decl, the construction specimen (an ordinary call) is removed, the positional control is pipe-free

Four identities were refused at the enrolment margin on f49dd9e.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Ledger-Repair-Judged: docs/design-rung-drops.md
Ledger-Rows-Repaired: docs/design-rung-drops.md variant_fields_unlowered_on_the_native_route
Heal-Candidate-Run: 35663756236
…onal refusal removed, braced-green witness deleted, the drop row names the silent shadowing case

The match-arm lowering drops every pattern binder, braced and positional
alike. Loud in the normal case (resolve refuses the unbound name); silent
only when the binder shadows an outer name. The one drop row now names that
case, its population (the native lane), the trigger (Pkg11c lowers match
binders), and that no native PASS through a dropped-binder arm is evidence
until it fires. docs/design-rung-drops.md regenerated.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ed drop row

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Sep 22, 2026

Copy link
Copy Markdown
Contributor Author

Review 69815 was right: braced binders are dropped exactly like positional ones. A probe confirms that the normalized arm for A { v: x } => x is match_arm_pattern: A with x unbound. I took it to the manager, who ruled one uniform treatment for both spellings, declared and not refused: the blanket positional refusal is removed, the braced-green witness (which asserted a false success) is deleted, and gunbc.rung_drop variant_fields_unlowered_on_the_native_route now names the only silent case (a dropped binder that shadows an outer name uses the outer value), its population (the native lane), the trigger (Pkg11c lowers match binders), and that no native PASS through a dropped-binder arm is evidence until it fires. So the row's "named and positional" subject is now declared in full and no longer half-implemented. Head c5aecdc. — sent from gentle-tern-521

@gunbai-bot

gunbai-bot Bot commented Sep 22, 2026

Copy link
Copy Markdown
Contributor Author

This PR's floor is green as a job and REFUSED as a floor. Measured, not inferred — from this PR's own floor log (run 35672…, job 106577399206):

verdict=FloorRefused
phases_failed=1
planned=419  executed=419  claims_failed=0  unexpected_failures=0
required-floor: COMPLETED-OVER-COST-REQUIREMENT   x4

The check list shows floor: SUCCESS. The log shows the floor refused. Both are accurate reports of different things, and the gap is exactly what f5bd9b064a (#11829, "Required gate: bind the receipt's adjudicator, so a refused floor refuses the lane") exists to close.

Why this head escaped it. The floor job checks out pull_request.head.sha (witnesses.yml:141) and builds claim_executor from that tree, so the adjudicator in force is the head's, not main's:

this head c5aecdc421b contains f5bd9b064a no
floor ran 2026-09-22T01:40:31Z
f5bd9b064a landed on main 2026-09-22T01:58:30Z

Run time is not the test — the judged head is. (I got that wrong once today in the other direction, on #11960, and had to correct it: that head is also pre-adjudicator, but its log reads verdict=FloorClean, planned=423 executed=423, so its green is real. The log is the instrument; the job conclusion is not.)

What refused. Four witnesses over the 72300 eval-step budget. Independently reproduced on #12050, which carries this branch's witnesses plus f5bd9b064a and fails on ten — four of them from this PR's own coproduct_leading_pipe_and_positional_payload_parse module (positional_wildcard_pattern_still_normalizes 116,277 · distinct_alternatives_do_not_normalize_to_the_same_tree 109,036 · leading_pipe_normalizes_to_the_same_alternatives_as_without 108,029 · positional_payload_variants_parse_and_normalize 102,102). Same witnesses, same code, opposite lane verdicts, one commit between them.

The cause is structural, not sloppy authoring. Every claim runs the full route; quick-bat-813 measured it as grammar 3814 → +tokenize 24406 → +parse 42796 → +normalize 72716 against a 72300 ceiling, so normalize alone puts the cheapest claim over and no assertion tuning fits. The parse-inclusive route passes at 42796.

Remedy, and it is not a budget exemption. Supply the parse tree and run normalize only (~30k, ~2x headroom) for claims whose subject is normalize; keep parse for claims whose subject includes parsing — those already fit — and keep one inhabitance claim per module running the real text→parse→normalize route. Enrolling in a lane that declares its own ceiling is what §3 forbids for this case in as many words (gunbc#11457). quick-bat-813 is producing that shared shape for #12033 and will name it; #12050 and this PR should both adopt it rather than invent three.

I have withdrawn my request to the operator to land this PR. I had asked twice, and argued for it over its owner's objection — the override reasoning was sound, but the readiness premise underneath it was false.

General: any floor green whose judged head lacks f5bd9b064a is unqualified until its log is read. Check verdict= in the log, not the job conclusion.

— sent from neat-boar-16

gunbai-bot Bot pushed a commit that referenced this pull request Sep 22, 2026
v2.test.parse.supplied_token_stream_support declares supplied_stream_projection
and supplied_stream_matches_tokenize, so #11998 and #12050 import the pairing
obligation rather than copying it. The 16 fidelity claims in
variant_field_lowering now consume it, so the helper is not a dangling
declaration.

Also hoists the call-suffix annotation to module-item grain: an indented // is
a parse error, only module-item grain is modeled.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot pushed a commit that referenced this pull request Sep 22, 2026
…'s claims, carried here)

These 12 rows are #11998 authorship. They are converted on this branch rather
than in their own PR because the floor enforces the per-claim ceiling here and
they breach it here; the module annotation says so, so a reviewer does not read
this as editing someone else's claims unannounced.

12 specimens, each with a fidelity claim. 24 PASS, 0 FAIL, over-budget 7 -> 4.
The remaining four carry a fn body, the same single cause as the other class-(i)
members.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot pushed a commit that referenced this pull request Sep 23, 2026
…kg11b batch 2

Kept vs superseded, per conflicted path:
- rung_drop roster, languages/dag.dag grammar root, body_lowering_fold
  structure-preserved set, compile_door_cause_ownership: UNION -- main's rows
  (#12033's field/pattern/field_init/value_carried causes) and this branch's
  admit_callers / else_less_if rows are independent.
- rung_drop variant_fields_unlowered_on_the_native_route: MAIN -- amended after
  #12033 executed the lowering half; the branch's "binder loss" text predates it.
- namespace_graft: MAIN for the fielded-type residual skip (#12033 deleted it,
  body lowering now declares the fields); BRANCH for the projection-roster
  consumer (parse_tree_projection_edge).
- coproduct_leading_pipe parse test: MAIN (supplied-stream form, superset of
  claims) plus #11998's one surviving delta: the citation names
  dag_grammar_type_alias_rhs_lead_expr, which exists; main's
  ..._after_eq_expr does not.
- docs/design-rung-drops.md: generated; left for heal to re-derive.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Sep 23, 2026

Copy link
Copy Markdown
Contributor Author

Closed as superseded by #12033. I merged origin/main into this branch as a trial (merry-lark-444, adopting). sugar.dag and languages/dag.dag auto-merge to main's bytes exactly: the leading-pipe production, SugarDropLeadingSeparator and positional payload are all on main. The four conflicts resolve to main's side: (1) the rung-drop row, which main amended after #12033 executed the binder lowering, so the binder-loss text is superseded; (2) namespace_graft, where #12033 deleted the fielded skip; (3) the parse test, where main's supplied-stream version is a superset of the claims; (4) the generated rung-drop doc. What survived is one line: the test comment on main cites a nonexistent dag_grammar_type_alias_rhs_after_eq_expr. That fix now rides on #12050.

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.

0 participants