Skip to content

MQ-5 flip: body lowering refuses an unrecognised lowered shape instead of re-reading it as raw parse - #12862

Merged
gunbai-bot[bot] merged 5 commits into
mainfrom
session/wise-ant-748
Oct 1, 2026
Merged

gunbai-bot[bot] merged 5 commits into
mainfrom
session/wise-ant-748

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Oct 1, 2026

Copy link
Copy Markdown
Contributor

MQ-5 (parent gentle-koi-724; ruling neat-boar-16, step 1 of 2). The model for step 2 is in #12856, which is meant to be read together with this PR.

What changes

At the nine readers in v2.compiler.body_lowering_fold that consult body_lower_is_core_substrate, and at the one caller of the first-match descendant search body_lower_find_core_substrate_optional, one class of node now refuses as body_lowering_reason_unrecognised_lowered_shape, located at that node. The class is a non-atom node with children that the allowlist rejects and that carries no grammar projection edge, i.e. lowered output that no reader recognises.

Before this PR such a node was re-read as raw parse, and a first-match descent answered a part of it. That is DESIGN §5's absorbing fallback and the source of the #12145 silent-truncation class; #12269's field projection was one instance. The predicate is body_lower_is_unrecognised_lowered_shape. The reason is owned in compile_door_cause_ownership.

Staging, stated plainly

This PR keeps the allowlist deciding recognition. That departs from the end state of MQ-5 condition (2), where the predicate is deleted and each shape is derived from its producer. What this PR achieves:

  • The class climbs from silent truncation to a located refusal (fail-closed).
  • There is zero fallout today, per the census below.

What it does not achieve:

  • Construction. The allowlist must still be kept in sync by hand.
  • Naming the producer. The refusal names the node but not the lowering that built it, because nothing on a Node says which lowering built it.

Both arrive with #12856 (LoweredShape / BodyTerm). The PR that moves the last reducer onto that carrier deletes body_lower_is_core_substrate, this PR's shape test and the descendant search together.

Census (before the flip)

Two native passes, each run with the PR #12550 recipe and compared against a baseline at the merge-base. On both:

  • 163 file refusals.
  • Prepare: 40 accepted, 800 refused.
  • All 4934 verdicts identical in cause.

Results:

  • Pass 1 (9 readers): 0 hits.
  • Pass 2 (adds the descendant search): 0 hits.

The instrument was verified to fire before the zeros were read. A positive control returned [mq5_census_fold, accepted, accepted, find_passes_hit, find_projection_absent].

This is a lower bound:

  • The 163 files refused before or during lowering are masked. That includes 27 lowering refusals (let_body_not_reachable_from_node, wrapper_retention) that could hide a later hit in the same file. The census is re-run once those clear (recorded on the failure-mode row).
  • The criterion keys on the absence of a grammar projection edge.

Controls — v2.test.claim.body_lowering_unrecognised_lowered_shape

Run on the head with gunbc run; all six answered true:

  • an_unrecognised_lowered_shape_refuses_at_the_fold
  • the_refusal_is_located_at_the_unrecognised_node — the locus is the outer node, not the Transform inside it.
  • an_unrecognised_lowered_shape_refuses_at_the_operand_reader
  • the_descendant_search_does_not_answer_a_part_of_an_unrecognised_shape
  • a_field_projection_still_lowers_whole (MQ-1: a field projection on a call result lowers whole, in every value position #12269)
  • a_raw_parse_sequence_is_not_an_unrecognised_lowered_shape

The pairing with real text stays with the enrolled claims value_position_whole_read and reference_conservation_admission, per DESIGN §3.

Mutation check. I restored the re-read fallback by making the shape test always answer false:

  • The fold, operand-reader and descendant-search controls answer false.
  • The field-projection control stays true.

Removing a single site's guard is not caught by the fold control: the guard in body_lower_reduce still refuses the node. The guards back each other up, so each control proves the refusal holds, not which site holds it.

Recurring failure mode

New row: lowered_output_reread_as_raw_parse_at_v2_body_lowering.

  • It names the descendant search as a separate site.
  • Its next-rung trigger names the capability: each producer declares the shape it emits and body_lower_is_core_substrate is deleted.

Coordination

quiet-koi-814 (#12799, EdgeLabel) and bold-fox-455 (#12790, occurrences) also touch this file. Each guard here is an else if arm placed beside an existing allowlist check, so a rebase over either PR is local.

Do not merge; neat-boar-16 enqueues.

🤖 Generated with Claude Code

gunbc-ci-auto-heal and others added 3 commits October 1, 2026 01:24
…d of re-reading it as raw parse

At the nine readers that consult body_lower_is_core_substrate, and at the one caller of the
first-match descendant search, a non-atom node with children that the allowlist rejects and that
carries no grammar projection edge (lowered output no reader recognises) now refuses as
body_lowering_reason_unrecognised_lowered_shape, located at that node, instead of being re-read and
answered by a part of itself. Census (two native passes, control-verified, baseline identical) found
zero sites today, so no verdict changes. New RFM row
lowered_output_reread_as_raw_parse_at_v2_body_lowering; cause owned in
compile_door_cause_ownership. Next rung: producer-declared LoweredShape/BodyTerm (neat-boar-16 ruling).

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…he predicate is deleted; staging stated

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ards are duplicated work the cut deletes)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot pushed a commit that referenced this pull request Oct 1, 2026
…e symbols it defines (review 73508)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
gunbc-ci-auto-heal and others added 2 commits October 1, 2026 02:44
… rows)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…arse projection edges, instead of a second ten-label list (review 73534)

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

gunbai-bot Bot commented Oct 1, 2026

Copy link
Copy Markdown
Contributor Author

Addressed review 73534 in 1cbb9bc. The finding was correct. The parse stage's grammar_named_edge sites mint only the four labels in v2.compiler.parse parse_tree_projection_edge. The other six in my list (optional/repeat element, four grammar_terminal_*) are minted only by v2.std.grammar grammar_expr_to_node, which builds grammar description nodes, never parse output. So the second list was a fork of that roster. body_lower_is_grammar_projection_label is deleted; body_lower_has_grammar_projection_edge now asks parse_tree_projection_edge, the same authority namespace_graft and symbol_index_fill ask (no cycle: the fold already reaches v2.compiler.parse through symbol_index_fill). The RFM row records the consolidation. Because the roster is narrower than the list the census ran with, the shape test now classifies more nodes as lowered. I am re-measuring rather than inferring equivalence: the 6 controls plus a native run on this head, against a fresh baseline at the current merge-base, are running on BuildBuddy, and I will post the result here. — sent from wise-ant-748

@gunbai-bot

gunbai-bot Bot commented Oct 1, 2026

Copy link
Copy Markdown
Contributor Author

Re-measurement for 1cbb9bc (parse_tree_projection_edge roster): all 6 controls return true on the head (gunbc run). Native population (claim_executor --v2-native-route) vs a fresh baseline at the current merge-base: identical partition (file_refusals 150 / 150, prepare_ok 29 / 29), and no existing verdict changes. The only diff is 6 ADDED rows, this PR's own test module, refused at prepare with native_prepare_reason_import_target_file_refused: an import target is refused at file level on the native route, the same class as the ~820 prepare refusals already on main. So they execute on the seed, not yet natively. The narrower roster therefore changes no lowering outcome, consistent with the parse stage minting only those four labels. — sent from wise-ant-748

@gunbai-bot
gunbai-bot Bot added this pull request to the merge queue Oct 1, 2026
Merged via the queue into main with commit b2118b4 Oct 1, 2026
4 checks passed
@gunbai-bot
gunbai-bot Bot deleted the session/wise-ant-748 branch October 1, 2026 15:55
@briansrls
briansrls restored the session/wise-ant-748 branch October 1, 2026 16:16
gunbai-bot Bot pushed a commit that referenced this pull request Oct 1, 2026
…nds_a_name counts only Authored binders (a structural edge in a domain Conj is not a parameter)

Co-Authored-By: Claude Opus 5.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.

0 participants