Repository navigation
PROBE (do not merge): #13168 overlaid with #13361 for the floor acceptance comparison - #13362
Closed
gunbai-bot[bot] wants to merge 56 commits into
Closed
gunbai-bot[bot] wants to merge 56 commits into
gunbai-bot[bot] wants to merge 56 commits into
Conversation
…pr row
body_lower_if_else_capture_optional searched the if's capture and, at any left
element that was not `else`, recursed LEFT before right. For
`if b { if c { X } else { Y } } else { Z }` it entered the then-arm and answered
the nested if's `else { Y }` as the outer else: Z was dropped, Y lowered twice,
and normalize ACCEPTED the module (silent wrongness, DESIGN §5). It was loud only
when Y held a function value, whose binder occurrence then appeared twice:
dag/std/materialization_ladder.dag value_materialization refused as
normalize_reason_minted_occurrence_duplicated, one of the native seven's file
refusals. body_lower_if_then_arm_optional searched the same way.
Both arm readers are now projections of body_lower_if_row_arms_optional, which
reads the two if_expr grammar rows by position (block: if cond fn_body else
(if_expr | fn_body); then-form: if cond then expr else expr) and answers Absent
for any other capture. The dead searching helper
body_lower_if_fn_body_capture_optional is deleted. The arm contract is
unchanged: an `else if` is answered as its if_expr shell, any other arm as its
production's captured child.
Claims: v2.test.claim.body_lowering.if_arm_position (an atom count over the
normalized tree, plus the function-value forms). Row: the capture side is filed
on gunbc.recurring_failure_mode else_arm_lowered_as_an_if_nested_inside_it.
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
The first floor run (37073686904) refused all four claims over the new-witness enrolment margin (353k-687k eval steps against 72300): each claim frame paid its own tokenize -> parse -> normalize. iap_verdicts computes the four verdicts once into four Bools (portable: no Node, no closure), each claim reads its field, and the producer is enrolled WARM in v2.workflow.floor_pure_producer_share beside eam_outcomes, the same ground. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
`if false { if true {1} else {2} } else {3}` is 3. The searching else reader took
the nested `else { 2 }` as the outer else, so a body lowered through it answers 2.
The mirror (`if true { if false {1} else {2} } else {3}` is 2) holds under either
reader and is the control. The module is import-free: the floor evaluates it
through the seed, and the native lane through the emitted compiler's own body
lowering, where it is the discriminating red. It is not yet merge-blocking
evidence for the v2 reader, since the native lane is not a required lane.
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…dicate guards A FIRST-overlap row is now removed only when the declared lookahead (k=2) proves the alternatives disjoint. A leading not-predicate subtracts the prefixes it is proved to cover, and only when the guard is plain (a finite token-string set whose PEG success is membership). A guard naming one word of a class narrows that position to class-less-word (the k=1 op_requires shape). Every undecidable arm keeps the row. Roster 51 -> 48: stmt return-vs-bare-assignment, let_expr let-vs-bare, let_sugar node-vs-bare are disjoint at k=2. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… retire its debt row
Touching the file put its bare references under the unimported-provider
gate. Both names are now imported, so the SubstrateInputsOnly row moves
ActiveDebt -> Retired { ImportsFixed }.
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…fix; no wildcard arms The ruling's direction: a pair of prefixes is disjoint when one side's prefix is covered by the other side's proved-plain guard, whatever length the guarded side's own prefix has (name: e | !(name :) e, whose positional side can be one token). Guards ride the prefixes they head and survive extension. The three GrammarExpr matches are written out arm by arm (NonFoldResidueRosterDiverged). Two controls added for the short-side case. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…in not-predicates arg: positional is !(name :) expr. stmt: the expression alternative is !(name = | 'node' name) expr. expr: binary_expr is !(name =>) binary. Each guard captures nothing, so trees are unchanged; the overlap proof clears dag_production_arg and stmt's ident-led row. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
The expression body was a second alternative sharing every expression-led input with the statement body. It is the one-statement case; body_lower_match_arm_body_lowered already lowers a statement body through body_lower_stmt_spine, whose last statement is the value. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ator ruling 2026-10-03, this case only) if_expr := if expr ( then expr else expr | block (else (if|block))? ). The else_less_if_stmt production is deleted; stmt no longer offers it. With-else trees are unchanged (a present optional and a choice pass through). Lowering reads an else-less if through one positional reader, body_lower_else_less_if_parts_optional: at statement position a block ending in return is the admitted guard; the exit walk and the if value reader refuse every other else-less if as else_less_if_unlowered, at it. Controls (v2.test.parse.else_less_if_value_category): the guard is accepted; the value position refuses at the if; both parse to the one else-less if_expr route. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…(LetInExpressionDropped) Per the 2026-10-02 zero-ambiguity decisions (statement let only, let-in dropped). The in-form alternative shared 'let name = value' with the statement form. A statement let's value followed by 'in' now refuses by name at the 'in' (a not-predicate over refuse_on_match, so a statement let's tree is unchanged). The six in-form lowering readers are deleted; no non-test source used the form. Test sources that used it are moved to the statement form or dropped where the statement form was already covered; let_in_form_refuses_at_the_in_holds is the refusal control. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…guard (base 2, cap 3) Every candidate site is read at depth 2; one that still overlaps is read again only as deep as its longest proved-plain leading guard, capped at 3. Measured on the dag grammar: a global k=3 tripled the roster run (114s -> 371s); guard-driven depth costs 138s. Controls: a three-token guard clears its row at its own depth; the near miss keeps it. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… empty arm body is its own production
expr: block_expr is !('{' '}' | '{' name ':' | '{' string ':') block_expr,
so '{}' in expression position is the empty brace literal (operator ruling
2026-10-03, A); binary_expr is !(name '=>' | '(' name ',') binary. Both
three-token heads are read at their guards' own depth.
match arm: body is empty_block_body ('{' '}') | !('{' '}') stmt body, so
the forty 'X => {}' arms stay empty blocks; it lowers as an empty block
always did (statement_spine_headless, at the body).
Route controls: v2.test.parse.brace_and_lambda_head_route.
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…e slot as IfRowNoElse On #13029's positional reader. The block form's else slot is seq(else, ..) or the empty node of an absent optional; the empty node answers IfRowNoElse, said rather than searched for or read as a value. The else-less guard reads its condition and arm from the same row reader. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…0-p2 # Conflicts: # src/v2/compiler/body_lowering_fold.dag
…he parsed node DESIGN section 3 witness rule (floor refused five new claims on cost). else_less_if_value_category: the conjunction is split into one claim per input; the guard and value claims parse once and hand the node to body_lower_admitted_guard_optional / body_lower_if_expr instead of a whole normalize. The real path stays executed by closure_parse_batch_two an_early_return_guard_parses_and_lowers_holds. brace_and_lambda_head_route: one data declaration per source, one parse per claim. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ly at a site's own alternatives Review 74631: the ingested bind fixtures now use statement let; the round-trip instrument's let_in case is retired (let_statement covers the form), and its derived drop population and projection follow. The bind family spec waits on the target-model separator change (its own PR). Cost (floor fill 26.5s against main's ~5s): a not-predicate narrows prefixes only where it heads one of the site's own alternatives; nested guards inside expanded productions are read as the empty prefix they consume, which only keeps rows. Measured remotely: the proof was ~8s of ~9s preparation. Also fixes the if-arm Optional typing in else_less_if_value_category. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…0-p2 # Conflicts: # docs/design-rung-drops.md
…101k against 72.3k) The value position is a one-line data initializer; the guard keeps the shortest fn with a statement after it. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…0-p2 # Conflicts: # docs/design-rung-drops.md # src/v2/extdeps/languages/dag.dag # src/v2/std/parse_refusal_reason.dag # src/v2/test/claim/parse/newline_dual_role_operator_mutation_test.dag
…okens Floor fill was 26s against main's ~5s. Measured remotely (startup subtracted): grammar preparation 8.6s at depth cap 3, 3.5s at cap 2, 2.3s with the proof off -- the escalation re-walked every head of the site, so the expr site re-expanded every identifier-led binary expression at depth 3. A prefix whose first token begins no pair that overlapped at the shallower depth cannot overlap deeper, so the deeper read is restricted to those tokens. After: 2.5s. Roster at this head: 0 rows. All 12 analyzer controls and 8 route claims pass. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Floor: the two guard claims were 89-91k against 72.3k; parsing the body as the fn_body production drops the module and signature tokens. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
elif_verdicts and bhr_verdicts compute every claim's Bool from one parse per source and are enrolled in floor_pure_producer_share; each claim reads its field (the claims had measured at the new-witness budget's edge, refused on enrolment margin). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Measured with claim_batch (prepare wall, 3 runs each, spread <0.3s): main
grammar 2.5s; this head before 6.8s; depth cap 2 3.3s; proof off 2.2s. The
depth-3 read of the expr site's '{' row walked every statement form after
the brace with depth 2 left. A prefix whose first two tokens begin no pair
that overlapped at the shallower depth cannot overlap deeper, so the
second position is restricted to those pairs' second tokens (unless a
pair has a prefix shorter than two). After: 5.0s. Roster 0; all 12
analyzer controls pass.
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ough IfRowElse #13051 (now on main) read IfRowArms.else_part, which this branch replaced with else_slot: IfRowElse. The census's new-reader else now answers through body_lower_if_row_else_part_optional (IfRowNoElse -> Absent), the same explicit no-else the lowering readers use. emit-build at 7668231 refused 'no field else_part on type IfRowArms'. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…0-p2 # Conflicts: # src/v2/workflow/floor_pure_producer_share.dag
Resolved per region. floor_pure_producer_share.dag: main's bns_verdicts row (this branch adds no roster rows). dag.dag: the import keeps KeywordAsValueName; the let_sugar head guard is main's (#13133's three-token node head); dag_grammar_field_pattern_expr takes main's body with this branch's two binder guards re-applied, and main's new if rows (optional else) are kept intact. seed_admits_a_keyword_as_a_pattern_binder: both receipts kept (main's SECOND SHAPE, this branch's specimen relabelled THIRD). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Taking main's side of the field_pattern hunk also brought main's three new if rows (dag_grammar_if_else_tail_expr / _if_block_form_expr / _if_then_form_expr), which the common text after the hunk already declares; the seed refused the duplicate declarations. The removed copies were byte-identical to the kept ones. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… loop repository_convergence_witness_test.dag carried a second 'let alias' in another fn, surfaced by the census once the first was renamed. The bare NAME= claim subject used 'then', a clause keyword that ends the statement sequence before the binder is reached; 'loop' heads an expression, which the statement guard excludes before '=', so the NAME= sugar's guard is what refuses. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…uses unnamed (measured) Statement alternatives dispatch by FIRST set and a not-predicate guard is transparent to it, so the bare NAME= let_sugar alternative is never reached for a keyword: the guard there was unreachable (loop = 1 and then = 1 both refuse as parse_g0_tokens_remain at the keyword, measured with the locate probe). The dead guard is removed; the binder reads the reference production, so a keyword is still never accepted. The claim subject moves to the reachable node NAME = form, a floor claim holds the bare form to 'refuses', and the RFM row states the rung and its trigger. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Each fixture is cut to the smallest source that exercises its position (no type declarations, one match arm, no second field), and the label control is split into a record-init/projection label and a field-declaration label. Measured with claim_batch eval_steps: 42k-116k, from 93k-185k. Seven claims still exceed the 72300 new-witness budget because the position itself needs a match or a two-binder fn; per the floor freeze (calm-boar-904) their identities go to royal-deer-478 for the single-claim fill debt rather than to a roster row here. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…it the contextual control A match position is exercised from a data initializer instead of an fn body, which drops the fn-header parse; the contextual control is split into a parameter half and a pattern-binder half, and node-then-if drops its parameters. claim_batch eval_steps 42k-103k (from 42k-116k), 13/13 PASS. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…rim two arms The node-then-if control is the same fixture as #13133's enrolled v2.test.parse.bare_node_statement_route bare_node_statement_before_an_if_takes_the_expression_route; repeating it here was duplicated evidence (and the claim the floor priced highest, 95797 steps). The bool-literal and contextual pattern-binder controls now end their single arm in '=> 0'. The floor's own measurement on 49d1886 put only these three over the 72300 new-witness budget. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…rp-raven-357 kvn_bool_literal_pattern_control_holds (76109 steps) and kvn_contextual_pattern_binder_control_holds (77441 steps) on the floor of record, run 37167363297 at head 2c91990, against the 72300 new-witness budget. Two rows, not folded. Reason: each subject is already the minimal construct and the cost is the interpreted tokenize/parse floor. Trigger: per-source tokenize/parse cost below the budget, or parse claims evaluated on the native route. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…'s parse The chunk list was already balanced (its closing brace is the fn's own line); the extra '}' ended floor_cost_debt_proven_chunks early and every lane refused the module as unparseable (src/v2/workflow/floor_cost_debt.dag:122723). v1_src_dag_parse: 7601 files parse-clean. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ance claim The floor's enrolment margin (302ms) refused seven kvn claims: each re-ran tokenize for a subject that is the grammar's binder guard. Per the §3 witness rule, every claim but kvn_param now parses a supplied stream; kvn_param stays on the real text route and asserts the located KeywordAsValueName fatal (the route, not only the answer). Each supplied stream owes a fidelity claim against the real tokenizer, comparing class, lexeme, positions and layout digest. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ness budget on supplied streams Floor at 0b89edf measured kvn_bool_literal_pattern_control_holds at 48755 steps (was 76109) and kvn_contextual_pattern_binder_control_holds at 49815 (was 77441), both admitted inside the enrolment margin, so the ruled debt rows no longer apply. File restored to origin/main's bytes. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…rdAsValueName
dag_grammar_field_pattern_expr is 'name [":" pattern]', so R { true } is an
implicit value binder named true, not a literal pattern. The field-pattern
guard now takes admit_bool_literals: false at the pun/outer-name position
and true after ':', where a pattern reads true/false as literals. Claims:
R { true } and R { false } refuse at the keyword; R { true: x } and
R { ok: true } still parse.
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
roadmap_component: take main's widened account-slot condition with the then_stmt label, and rename main's two new ts_if then: labels to then_stmt. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
parse_refusal_reason: keep both new variants (KeywordAsValueName from this branch, TokenStartsNotIncreasing from main) in the comment, the coproduct and the symbol match; the mutation test's exhaustive match keeps both arms. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…t_alias alias is a keyword; this PR refuses it as a value binder (KeywordAsValueName). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
roadmap_allocation_client: take main's rewritten intent block. Main's new js_branch parameter 'then' is renamed then_arm (a keyword is not a value binder), and its ts_if then: labels become then_stmt, matching ts_if's renamed parameter. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
#13305 landed the service_realization 'then' -> 'proceed' rename, so this branch's hunk there is dropped (file is main's bytes). The RFM row keeps main's THIRD SPECIMEN (#13305's parameter shape) and renumbers this branch's binder/reference receipt to FOURTH. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
roadmap_component / roadmap_inline_assignment_client / roadmap_issue_sort:
this branch's change there was only the ts_if then: -> then_stmt: label
rename (verified: identical modulo that rename), so take main's rewritten
files and reapply it. Main's new dag/gunbc/site/{controls,choice_client,
mention_client}.dag ts_if call sites get the same label rename.
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ontext reads it by instance Each floor claim runs in a fresh InterpContext whose content-hash memo is empty, so the first call in each claim that took a tier-served value (or a part of it, e.g. a prepared grammar's prepared_exprs) as an argument re-hashed the whole value natively: a per-claim cost proportional to the served value's size, outside the step budget (calm-tern-13, wise-ant-549, tidy-raven-393's 0b89edf vs b72b994 cost diff). The hash reads only content and process-canonical spellings, so it is a fact about the instance: it is now computed once at publication into CROSS_CLAIM_SERVED_HASH_MEMO and consulted by Rc pointer, used only while the allocation is alive (the tier retains it for its lifetime). Instance identity is the join, never a digest; serving still verifies arguments, so the memo decides only the cost of a key. Cleared with the tier. Control: a_fresh_context_keys_a_served_value_and_its_parts_without_rehashing. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…r's justification Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Contributor
Author
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.
Measurement-only draft. It is #13168 (cfa31bb) merged with royal-deer-478's #13361 (1d89f4e), so the floor can measure the kvn/nfbcp parse rows and the
[cross-claim-demand] parse_module_preparedline against b72b994, as #13361's acceptance control. It will be closed once the floor reports. Do not review or merge.🤖 Generated with Claude Code