Repository navigation
MQ-1 PR-1: a caret symbol in value position refuses at the caret instead of lowering to its ^ token - #12392
Merged
Conversation
…ason_caret_symbol_not_lowered) On main every value position (argument, let, body, data/field init, arm body, scrutinee, if-branch, list item, if-condition operand) accepted ^name and lowered it to a bare ^dag_token_caret with the symbol dropped, via body_lower_primary_expr's first-atom fallback. That fallback now refuses the caret shape, anchored at the ^ token, with its own cause. Ownership row added; RFM caret_symbol_has_no_lowered_form records the below-floor instance; new RFM reference_conservation_population_omits_class_stamped_terminals records why the conservation instrument could not see the drop. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…pecheck) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ip the pinned cav claim and the pin Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… of 13 per-claim front-end runs Each claim ran a full tokenize->parse->normalize, far over the new-witness step budget. The thirteen verdicts are now computed once by csv_verdicts, enrolled warm in floor_pure_producer_share as cav_outcomes is; each claim reads its field. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
This was referenced Sep 27, 2026
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.
MQ-1 PR-1 (of two). This fixes a live §5 defect on main: a caret symbol (
^name) in value position lowered silently wrong. This PR makes it refuse, located at the caret. PR-2, the symbol-literal slice (a lexeme stamp plus aLitSymbolatom), flips exactly this refused population to a faithful lowering.What main does today (measured, not inferred)
fierce-gull-556 ran a seed-interpreted probe of tokenize → parse → normalize on main b1b7aea (branch
probe/snappy-swift-136-mq1-caret@ 2349f53 and 0ee714d):body_lowering_reason_operator_operand_unread: a bare operand used as a whole body. Specimens arev2.std.grammarformal_binding_is_free_name_slotandformal_binding_is_lexeme_stamp_slot, andv2.std.compilers.target_modeltarget_model_bundle_core_keep_edge.v2.std.compilers.target_modelordering_predicate_from_wire_symbol(if id == ^ordering_predicate_is_less {..} else if id == ^ordering_predicate_is_less_or_equal {..}). Its tree carries^dag_token_caretand neither symbol, so both conditions becameid == ^: two different symbols, one node.The single cause is the first-atom fallback in
v2.compiler.body_lowering_foldbody_lower_primary_expr, which answered the caret sequenceseq(^, name)with its^token.The change
body_lower_caret_symbol_token_optionalrecognises the caret shape by its left terminal. The first-atom fallback inbody_lower_primary_expr, and only that fallback, now refuses it with a new, distinct causebody_lowering_reason_caret_symbol_not_lowered, anchored at the^token.x == ^symunifies on the new cause. On main it refused asoperator_operand_unread. Its operand now reaches the same fallback, which was measured: a pin asserting the old cause ran red. So every caret refuses with one cause at the caret, and PR-2 flips one countable population.v2.test.claim.namespace_xl0.call_argument_value_resolve_refusala_caret_symbol_operand_refuses_at_normalizeis flipped to the new cause in this PR.v2.workflow.compile_door_cause_ownership: a FatalGrain row for the new cause (laneSharedSelfHostCriticalPath, flip trigger caret lowers to LitSymbol), so the native lane gains no unattributed refusals.caret_symbol_has_no_lowered_formrecords the observed below-floor instance.reference_conservation_population_omits_class_stamped_terminalsexplains why the conservation instrument could not see the drop. Its population admits only atoms whose identity is not a declared token class. The caret's name terminal is class-stamped as^dag_token_ident, so the dropped symbol was never a member. The drop was invisible by construction, not missed by the comparison. The next-rung trigger is PR-2's lexeme stamp.Controls
v2.test.claim.body_lowering.caret_symbol_value_refusalcalls the producers directly (tokenize → parse → normalize) over one declaration each:caret_symbol_not_loweredand is anchored at^dag_token_caret. The if-condition specimen is the realordering_predicate_from_wire_symbol, trimmed to two arms.Population and BASE-vs-HEAD
File census: neat-boar-16 ran it on srv1 with the self-host driver in census mode. Both arms completed. Per-file rows are on srv1 in
~/nb16-tmp/ct_{base,pr}.pf.body_lowering_reason_caret_symbol_not_lowered. No new refusal has any other cause.call_argument_unread234,value_unlowered26,operator_operand_unread23,wrapper_retention_not_normalized4,type_annotation_not_carried1. No other cause relabels.Claim run (base vs head): neat-boar-16 ran it on srv1 with
gunbc run --claim-runover every test fn of 23 claim modules. The modules were found by what they consume (the relabelled causes, the caret shape or cause, the ownership table, conservation, or a normalized fixture containing a caret), not by the files this PR touches.a_caret_symbol_operand_refuses_at_normalizepasses on both: the old cause on base, the new one on head.caret_symbol_value_refusalplus the share-roster row, and that module was rerun: 13/13 PASS (212.9 s wall, 7.8 GB maxrss for the whole load).Ordering with the native frontier ratchet (#12184)
gunbc.native_frontier_ratchethas no declared disposition for new debt: an added refusal is only ever aFrontierLostfinding. Today the roster isRosterUnminted, so this PR edits no roster. The first mint must land after this PR, so these refusals are minted as owned baseline debt. If the mint lands first, the next nightly reads them asFrontierLostwith no admitted path. gentle-koi-724 has told zesty-otter-346 and neat-boar-16. The missing disposition for a correctness flip that grows debt is a gap for that lane to model.Evidence status
floor_class=structural. The cause was inferred, since the logs were unreadable during the GitHub token outage: each of the 13 caret claims ran its own full tokenize → parse → normalize, far over the new-witness step budget. cd51f40 computes the verdicts once in one producer,csv_verdicts, enrolled warm inv2.workflow.floor_pure_producer_sharebesidecav_outcomes. Each claim reads its own field. Assertions are unchanged.gunbc run --source-root dag --source-root src/v2 --entry <module> --claim-run:v2.test.claim.body_lowering.caret_symbol_value_refusal: 13/13 PASS (221 s).v2.test.claim.namespace_xl0.call_argument_value_resolve_refusal: 21/21 PASS (290 s), including the flippeda_caret_symbol_operand_refuses_at_normalize.dag/stdedits, so no stage0 regen.🤖 Generated with Claude Code