v2: lower the where-refined head so resolve binds it; ResolvedTree.resolved_declarations (base for #12407) by gunbai-bot[bot] · Pull Request #12629 · gunb-ai/gunbc

gunbai-bot · 2026-09-29T15:51:31Z

Base for gunbc#12407 (gunbc#12432, which carries ResolvedTree, has landed) (neat-boar-16 ruling: resolved declaration bodies get their own PR).

The boundary, measured

Before this change, the head of type Pos = Int where positive reached v2 resolve as an unlowered dag_surface_qualified_name parse shell, and resolve preserves such a shell unchanged as module metadata (v2.extdeps.languages.dag dag_resolve_preserve_module_metadata_subtree). So the declaration's carrier was never resolved: a carrier nothing declares was accepted silently, and #12407's Widened cast compared a resolved target against an unresolved carrier. Measured on #12407's branch: once lowering hands resolve a plain type atom, the resolved tree holds the carrier as the kernel binding. The repair is at lowering, the root, not a second walk in resolve.

What lands

v2.compiler.body_lowering_fold body_lower_type_variant: the where-refined head is lowered by the one type-expression lowering (body_lower_type_expr_lowered_optional), the same one signatures and cast targets use. An unreadable head refuses at the head (body_lowering_reason_type_annotation_not_carried).
v2.compiler.resolve ResolvedTree: gains resolved_declarations: SymbolIndex, alongside symbol_index, which replaces nothing. It is filled at the Accepted exit (resolved_tree_of) by the same module fold as the pre-resolve index (symbol_index_fill_module_declarations), run over the resolved root. The two facts are stated on the type: symbol_index is the index resolution consulted (declarations as authored); resolved_declarations is declarations with resolved bodies. No reader of symbol_index for a body type is added, so the two never answer one question. Trees that never went through resolve (the ingest bridges, claim_resolved_tree_without_declarations) carry an empty index, and a declaration cut from a program (realization_attempt) carries the program's.
Consumer: gunbc#12407's v2.compiler.infer refinement_declaration switches to resolved_declarations explicitly.

Step-0 census (receipt)

Every where-refined head in the corpus is a plain type name (NonEmptyStr, String, Int, Nat, …), so resolving them introduces no refusal in the corpus. The only fixtures that named an unimported carrier are v2.test.claim.declaration_graft_assemble's (String in module p); they now carry the kernel Int.

Controls

RED: declaration_graft_where_alias_over_an_undeclared_carrier_refuses (type Name = Undeclared where … refuses resolve_reason_unbound_symbol). Its assembly is a producer rostered warm in v2.workflow.floor_pure_producer_share, beside its ten siblings (one front end is more than one claim's budget).
Positive, production route: declaration_graft_where_alias_carrier_is_resolved_in_resolved_declarations. In resolved_declarations, p.Name's carrier is dag_binding_type_int. It is red if the head stayed a shell, or if it were read from symbol_index (the bare spelling).
declaration_graft_assemble 18/18; body_let_annotation 21/21; body_cast_node, compilation_unit_witness, match_arm_binder_frame, declaration_structure_preserved, reference_conservation, where_refinement_clause_parse and d1_declaration_grammar_parse all green. variant_field_lowering has four failures that are pre-existing: the same four fail on the base (v2 resolve: ResolvedTree carries the SymbolIndex resolution consulted (infer's input carrier) #12432 head c90dae33) with this change absent; they read normalized trees, before resolve.

Declared frontier (condition 1)

The alias right-hand side, record field types and variant payload types are the same defect and stay unresolved in this PR. This is filed as gunbc.recurring_failure_mode declaration_body_type_shell_preserved_unresolved, with trigger every declaration-body type position is lowered before resolve. Sibling: quiet-hawk-702's v1 cause 1b (gunbc#12612, v1 Node.declaration), the same std.decl_ref DeclarationRef identity type on the frozen v1 layer, not a second mechanism. The v2 producer is resolved_reference_node (via declaration_reference_node).

🤖 Generated with Claude Code

…; cut every consumer root-first Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

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

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

…parameter_order, reference_closure) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

…red input); retype main's new resolved-tree test sites Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

…ts use the named no-declarations constructor Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

…); typecheck clean over 116 files Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

…ted symbol and reads .root Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

…ResolvedTree and walk .root Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

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

…vedTree.resolved_declarations (neat-boar-16 ruling) The head reached resolve as an unlowered dag_surface_qualified_name shell, which resolve preserves unchanged as module metadata, so a declaration's carrier was never resolved. It is now lowered through the one type-expression lowering; resolve binds it; an undeclared carrier refuses unbound. ResolvedTree gains resolved_declarations, the same module fold over the resolved root, alongside symbol_index (the index resolution consulted). The other declaration-body type positions are a declared frontier (gunbc.recurring_failure_mode declaration_body_type_shell_preserved_unresolved). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

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

…solved_declarations; Pos2 widens one step on the production route Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

…o later stage reads it; #12407 reads resolved_declarations) (review 72652) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

gunbai-bot · 2026-09-29T16:27:42Z

Review 72652's inaccuracy is fixed at f293dcb (comment only). The ResolvedTree comment named #12407's refinement_declaration as a symbol_index consumer, which was true before #12407's rework. It now states one fact: symbol_index is the table resolve resolves against and no later stage reads it; #12407 reads resolved_declarations. The duplicate sentence is removed.
— sent from wise-bat-862

…ex of its own); it moves in the deleting commit Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

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

… binds it; keep this branch's kept where clause on top of it. Graft fixtures take main's Int carriers plus this branch's local brand declaration Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

…come<ResolvedTree> (#12629) The binding claims inspect only accept/refuse, so they retype to Outcome<ResolvedTree>; Node is no longer used. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

…icates as declarations) (#12969) * v2: ground where-refinement predicates as declarations; resolve binds them Each decidable where predicate is a total Bool declaration (std.types string_non_empty, gt_zero, range; std.content_hash lower_hex_16/40/64/128) and brand a declared marker fn. Lowering carries every predicate of a clause, with its arguments, at its own occurrence; v2 resolve binds each by ordinary name lookup and refuses an unbound one as resolve_reason_where_predicate_unbound. non_empty is respelled string_non_empty corpus-wide (v1 parse/infer tables + stage0 regen) and the gate's non_empty_string consolidates onto it. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * v2: home the Char classifier in std.unicode.char_class; fix stale predicate homes; import filter std.string_type pulled into the compiler closure broke self-host emission (string_lex_compare E0308); the classifier moves to its own Unicode module instead. Comments naming std.integer as the home of gt_zero/range now name std.types (review 71649). filesystem_io imports the bare filter the floor refused once the file was touched. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * floor roster: retire filter rows discharged by filesystem_io's filter import filesystem_io now imports v2.std.algebra filter, so every file importing filesystem_io no longer carries its bare filter pair; the floor refused the touched one as RosterStale. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * floor roster: retire v2.std.algebra rows reached through filesystem_io The import closure is module-grained: importing filesystem_io now reaches every v2.std.algebra declaration, so skip/any/length rows on its importers are discharged too. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * where predicates: execute each declaration against the seed's probe values; stop overclaiming one authority Until v1's tables can consult a declaration (feature:where-refinement-predicate-declaration-authority), the declaration and the table are two representations. The vocabulary witness now executes each grounded declaration on the probe value the compiler is observed to refuse, with boundary controls, one claim per predicate; the comments state the fork instead of claiming one authority (review 71681). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * stage0: restore main's v1_rt.rs (a stale-binary regen had reverted it) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * filesystem_io: drop the duplicate filter import (main added the same one; review 71725) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * MQ-1 PR-2 WIP: caret symbol lowers to a symbol literal * MQ-1 PR-2: RFMs, conservation control, symbol-literal frontier control * symbol literal payload read without a nested Edge pattern (emitted Rust holds the label in an Rc) * caret lowering claims: list_snoc_item from v2.std.algebra; declare the generic-ident-class flip * parse probe: caret-site claims read one warm-shared parse (caret_tree_atom_identities) instead of re-parsing each * caret lowering witness: plain recursion instead of fn-lambda call arguments (the witness is about carets, not the lambda frontier) * caret lowering witness: build lists with list literals/concat (seed types a bare Cons as FreeMonoid) * reference_conservation_admission: drop the braces my merge resolution orphaned (floor/generated: unparseable at byte 6129) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * namecheap witnesses: rename the test helper response -> namecheap_api_response #12421 declared a top-level fn response. The bare-reference scanner reads each service operation's response { ... } block (42 files) as a reference to it, so every PR touching one of those files is refused UnimportedBareProvider. The scanner's missing keyword awareness is reported as its own finding. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * v2 resolve: a module's own `type Int` / `type Bool` shadows the kernel spelling instead of being captured Body lowering rewrote every type atom spelled Int or Bool to the kernel binding before any scope existed. A module that declared its own `type Int = | Mine` and wrote `let y: Int = 1` therefore had its annotation replaced by the kernel Int, and infer judged the let matched. The spelling table moves to its language authority (v2.extdeps.languages.dag dag_kernel_type_binding_optional), and resolve_atom consults it only after the scope walk and the symbol index. A hit declared in the referencing module binds that declaration. Imported, foreign, ambiguous and unbound kernel spellings keep the kernel binding, unchanged. Claims (v2.test.claim.body_let_annotation, 5c): the module-declared Int and Bool lets refuse at the annotation, and the annotation is asserted not to be the kernel binding. An undeclared Int/Bool still binds the kernel type. Both shadow rows are red on main 9ce0394 and green here. The rfm row records the residual and its trigger. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * v2 resolve: an imported user Int refuses instead of binding the kernel Int Resolve now reads a kernel spelling by the declaration a door selected. v2.extdeps.languages.dag dag_kernel_type_declaration_binding_optional lists the declarations a kernel spelling denotes. A hit on one of them takes the canonical binding, and the module's own declaration shadows it. Any other declaration, reached through an import or another module, refuses with resolve_reason_kernel_type_spelling_names_a_foreign_declaration. Unbound and ambiguous names keep the spelling fallback. Third RED: bla_imported_user_int_refuses_rather_than_binding_the_kernel_int (a two-module fixture, p imports q's `type Int = | Mine`). All three REDs are F on main and T here, and the controls are T on both. The new specimens are enrolled in floor_pure_producer_share. The rfm row now states rung = refused, with the trigger at capability grain: declaration-keyed binding across every door. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * v2 resolve: an ambiguous kernel spelling refuses unless every candidate is a kernel declaration An ambiguous kernel spelling now binds the kernel type only when every candidate is a kernel declaration of it: v2.std.integer Int beside std.integer Int is one kernel type. Otherwise it refuses with the ordinary resolve_reason_ambiguous_symbol instead of defaulting to the kernel. An unbound name keeps the kernel binding, which is the correct answer when no declaration is in scope. New claims: - RED bla_ambiguous_imported_int_refuses_rather_than_defaulting_to_the_kernel (p imports Int from q and r). F on main, T here. - Control bla_ambiguous_kernel_declarations_bind_the_kernel_type. T on both. The multi-module specimens now share one helper, bla_assemble_with_peers. The rfm residual is now only the kernel-declaration path list. Its trigger is a mark on the kernel declarations themselves. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * wip: infer symbol-literal arm (DagCanonicalSymbolLiteral typed as v2.std.node Symbol) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * test.claim.parse_test_fn_decl_return_clause: lowering carries the authored return-type spelling Three floor blockers on fa8c596. These claims read the positional return clause from body lowering and expected the kernel binding (dag_binding_type_int, bool_node_symbol). Lowering used to produce that binding by rewriting the spelling. That rewrite now happens in v2.compiler.resolve, after the scope walk, so lowering carries `Int` and `Bool` as written, as the generic row already reads `T`. Arm 1 still discriminates: the return type is Bool, not the parameter's Int. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * dag_canonical_literal_from_node: match the symbol-literal optional once review 72280: the symbol arm tested dag_node_is_symbol_literal_atom and then recomputed dag_symbol_literal_name_optional. That was the same optional twice, and the recomputation needed an arm the predicate had already ruled out. The decision now matches the optional once. The remaining Absent arm is a name payload with no atom identity, which is reachable. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * Dissolve dag_node_is_symbol_literal_atom: callers match dag_symbol_literal_name_optional directly (review 72280 on #12549) * identity_captured_navigation: read a caret literal's name from the lexeme-stamped terminal; delete the span/source-text route and its prose note row (review 72294 on #12549) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * Delete the octet-to-scalar index and its lens-slice claims with the lens span route: nothing else consumed them Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * caret_symbol_has_no_lowered_form: the receipt states the literal's type as this PR derives it review 72301: the receipt still said the symbol literal's type stays on the GroundingNotDerived frontier. The arm in this PR makes that false. It now names the derivation route (DagCanonicalSymbolLiteral, infer_literal_type_binding, v2.std.node symbol_type_node) and the two body_let_annotation claims that execute it. Census trigger (a) stays open and the receipt says why: it names the source checker v1.compiler.types, which still types LitSymbol as string_type. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * v2 resolve: the single-tree namespace binds the module's own declarations; ownership reads declared_in GitHub review 5342739525 on #12540. The same-module test compared a declaration's path to ctx.namespace.module_qn, but build_program_namespace (the plain normalize -> resolve route) leaves module_qn Empty and records its owner in declared_in. namespace_owns_declaration now reads declared_in, which is the owner on both namespace routes and the field root_binding_origin reads. Measuring that route found the earlier boundary. build_program_namespace harvested only the root's named edges, and a normalized module keeps its declarations under captured -> <module path>, so none of them were bound. `type Myint` refused as unbound, and a module's own `type Int` fell through to the kernel spelling and was silently bound to the kernel Int. The namespace now also harvests the module body, which it finds by declared_in. Controls on that route (v2.test.claim.body_let_annotation, enrolled share points): - bla_single_tree_module_declared_int_and_bool_bind_the_local_declaration: F before, T now. - bla_single_tree_undeclared_int_binds_the_kernel_type: T on both. The foreign-import refusal and both ambiguity dispositions are unchanged and still hold. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * v2 resolve: select a grafted module body by the graft's mark, never by walking names Review 5343957887 (P2 on b55b8a7). namespace_tree_module_body walked the module path's names and restarted at the root on a missing step. Two leaks followed: - `module m.t` with a root-level record `t` missed `m`, restarted, found `t`, and bound the record's field as a module binding. - `module t` with a record `t` selected it at once. The body is now selected by the producer's own mark. v2.compiler.namespace_graft namespace_graft_module_body_optional descends the containment spine (namespace_graft_spine_segment_edge_optional) until a step is not a segment, never restarts, and answers only when that stop is the marked body (namespace_graft_node_is_module_body). Header and flat representations have no grafted body, so they keep root-only harvesting. The admission reader in v2.compiler.name_resolve already descended the same spine with its own copy (admit_named_exports_body_root and _descend_spine). It now calls the one function in namespace_graft (namespace_graft_module_body_root), so the spine has one reader. Controls (v2.test.claim.resolve.single_tree_module_body): supplied emit-shaped roots, because normalize always emits a well-formed graft and source text cannot author these shapes. - a_record_matching_the_path_suffix_is_not_a_module_body_holds: F on b55b8a7, T here. - a_record_named_like_a_flat_module_is_not_its_body_holds: F on b55b8a7, T here. Each asserts `leaked` is not bound and `t` still is. The local Int/Bool and undeclared-kernel controls still hold. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * v2 resolve: move build_program_namespace's rationale above the declaration The parse phase refused a // annotation inside the fn body (DESIGN section 4c: only module-item grain is modeled). This is the same text, placed above the declaration. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * RFM reference_conservation_population_omits_class_stamped_terminals: the caret WHY is past tense and names its helper as deleted (review 72492) * v2 infer: a literal payload's facts derive for its own family Review 5348050288. infer_literal_edge_diagnostics_derived decided which literal family owned a payload edge, then dropped the family. infer_literal_payload_entries typed every payload atom as a DecimalDigit, so a Symbol literal's name terminal was recorded as a digit. The edge decision is now typed: infer_literal_edge_payload returns InferIntMagnitudePayload, InferSymbolNamePayload or InferNotALiteralPayload, and the payload fold takes that family. - Int magnitude members keep DecimalDigit / FreeMonoid<DecimalDigit>. - A Symbol name payload is one childless atom and derives as v2.std.node Symbol (symbol_type_node). - Any other shape stays on the frontier. Controls read each payload node's recorded resolved_type (v2.test.claim.body_let_annotation 5e): - bla_symbol_literal_payload_is_typed_symbol_not_digit: F at 87a29e4, T here. - bla_int_literal_payload_digits_stay_decimal_digits: T on both (the integer family is unchanged). Both require at least one payload to be seen, so neither can pass vacuously. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * body_let_annotation: share the payload verdicts, not the inferred trees The floor refused at 92389ff: PureProducerShareWarmNotStored for bla_symbol_literal_as_symbol_tree, because the cross-claim store cannot hold a closure (ServeCacheValueNotPortable, path .value.facts.lookup). The shared producers now return the portable projection the claims inspect: bla_symbol_literal_payload_verdict (the symbol-typed and digit-typed Bools) and bla_int_literal_payload_digit_verdict. The trees are built inside those producers and never stored. The claims and their discrimination are unchanged: the Symbol payload control is F without the family-aware fold and T with it. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * 04_infer: the payload comment cites infer_literal_edge_payload, not the deleted predicate Review 72579: the comment above infer_literal_payload_member_type still named infer_literal_edge_diagnostics_derived, which this PR replaced. No definition or reference to it remains. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * Merge origin/main; bla_symbol_literal_as_int returns Outcome<ResolvedTree> (the #12432 assemble type) * Import the std.disposition / v2.std.live_tree names two touched files use bare; retire their now-imported roster rows Main newly declared Disposition and LiveTreeDisposition, so the gate refused both files on this touch as UnimportedBareProvider. Importing the declaring modules also covers SingleAuthority, RealizationDispatch and SubstrateInputsOnly, whose ActiveDebt rows retire as ImportsFixed. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * roster_gate imports Finding (bare channel is off in a file that declares imports) * reference_conservation_admission: KnownDropShape as a one-variant coproduct (leading |), not an alias to StatementLetBinder With one arm left, '= StatementLetBinder' parsed as an alias, so the variant did not exist and two importers refused IMPORT-MEMBER-ABSENT. The corpus form for a one-variant coproduct is '= | Variant' (e.g. SdramSignalingFamily). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * v2: the kernel host-text String, bound only where no String declaration is visible neat-boar-16's ruling after #12549. It mirrors #12549's Symbol pair through the same mechanism. - Declaration: v2.std.node declares the opaque kernel `String` beside Symbol (the kernel-types home), and owns its type node, host_text_type_node. - Binding: v2.extdeps.languages.dag binds the spelling `String` to it, and the declaration table maps v2.std.node.String to it. - Foreign declarations (decision A): String is the one kernel spelling the corpus already declares with another meaning (v2.std.text and std.string_type are FreeMonoid<Char>, imported by 470+ modules), so dag_kernel_type_foreign_declaration types its foreign-declaration disposition as ForeignDeclarationBinds. v2.compiler.resolve then binds the declaration the author reached, and the kernel host text applies only in the unbound arm. Int, Bool and Symbol keep ForeignDeclarationRefuses. - Literal: DagCanonicalStringLiteral is a fourth arm of the one literal decision, typed as host text. Every consumer that matches the literal decision handles it (infer's type binding, branch operand, match-arm body, Bool pattern classify, payload edge, and the undecidable-verdict lens). - No implicit coercion: a host-text literal at a FreeMonoid<Char> position REFUSES. The declared unfold (literal_homomorphism_rows, UnicodeScalarSequenceUnfold) is not reachable yet, because the literal carries no value. That is filed as gunbc.recurring_failure_mode string_literal_lowers_to_one_class_stamped_atom (fix routed to gentle-koi-724's lane). Claims (v2.test.claim.body_let_annotation 5f). The REDs are F with the behavior reverted and T here: - bla_unimported_string_binds_kernel_host_text - bla_string_literal_is_typed_host_text - bla_string_literal_ascribed_int_refuses - bla_host_text_literal_at_structural_string_refuses Controls, T on both: - bla_imported_structural_string_binds_its_declaration - bla_host_text_value_at_structural_string_is_never_matched (no non-literal expression derives host text in v2 yet, so it pins "never a clean admit") - bla_unknown_unimported_type_name_still_refuses The Symbol and #12540 claims are unchanged and still hold. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * carrier_by_spelling: record the v1/v2 String fork and where it resolves (at the importers) royal-newt-820 flagged it and neat-boar-16 ruled. Under decision A, v2 binds `import v2.std.text { String }` to the structural carrier, while v1 keeps the kernel. The fork resolves at the importers: - host-using importers drop String from their imports, in a separate PR ahead of #12760; - structural-using importers are a declared divergence, recorded here, with #12760's census as the instrument. The rung stays at the v1 minimum. Evidence: bla_imported_structural_string_binds_its_declaration. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * dag_canonical_literal_from_node: the string arm matches the atom inline; the is_* predicate is gone Review 73119. dag_node_is_string_literal_atom was a sibling Bool predicate over Node storage, which the literal coproduct exists to replace. That is the same dissolution as dag_node_is_symbol_literal_atom (3fb5d6a, review 72280). The decision matches the atom identity inline. The claim reads DagCanonicalStringLiteral from the decision, and the RFM row cites the decision. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * defork census: the String row names the kernel host-text String as a distinct concept The generated check failed at d9cc153: docs/plans/dag-v2-defork-audit.md drifted, because the census now finds v2.std.node String (#12760) among the String declarations. The derived file list was right, but the authored reading still called every String '= FreeMonoid<Char>, one concept, two declarations'. That is false for the opaque host text. The reading now separates the structural pair from the host-text String, and the projection is regenerated with generated_artifact_gate main_wet. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * kernel String: read #12759's string value; realize v2.std.node String as the host string #12759 landed, so a string literal now carries its decoded value as one named payload. - DagCanonicalStringLiteral { value } reads it through dag_string_literal_value_symbol_optional. A payload-less string atom is now a malformed literal. - The value edge is its own payload family (InferStringValuePayload), typed host text and never a digit, as #12549 did for the Symbol name. bla_string_literal_is_typed_host_text now also requires that. - string_literal_lowers_to_one_class_stamped_atom records the climb by #12759. The remaining literal-at-FreeMonoid<Char> refusal is now blocked only by v2 infer not peeling an alias to its body. emit-build failed at 9b7c07f: the opaque v2.std.node String was emitted as its own struct, so the bare String in v2_std_node.rs (symbol_lexeme's return) stopped meaning the host string (E0308). gunbc.rust_source_type_bindings gains the exact row v2.std.node String -> RustStdString beside Symbol's, and the String checkpoint proof records that the kernel spelling now has one declaration rendering the same carrier. The stage0 mirror is updated to match: claim_executor --required-regen reports first_generation_equal=true over 161 files. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * carrier_by_spelling: the importer census is a named frontier, not an instrument this PR cites Review 73214. The receipt called the importer census '#12760's census' and its instrument, but no classification exists in the tree yet. It now says the population is described, not bounded; names the census and deletion lane that will bound it; and states that #12760 is held as a draft until both land, so the flip cannot precede the cutover. When the census lands, the receipt will cite it by symbol. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * where_predicate_binding: assemble_program_from_ingest now returns Outcome<ResolvedTree> (#12629) The binding claims inspect only accept/refuse, so they retype to Outcome<ResolvedTree>; Node is no longer used. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * v1 emit_rust: an opaque declaration with an exact realization row emits an alias to that row Ruled by deep-bee-18 for gunbc#12760. The emitter emitted every zero-parameter opaque declaration as `pub struct X(PhantomData)` and ignored the declaration-keyed rows in gunbc.rust_source_type_bindings. On #12760, v2.std.node String therefore became a struct, and the kernel's bare `String` render inside v2_std_node.rs meant that struct (E0308 at symbol_lexeme). The rule is general and declaration-keyed: rust_opaque_declaration_has_exact_row joins the existing name-keyed kernel-alias route at all three sites that decide it. An exact row emits `pub type X = <row spelling>`. An ambiguous row, or a row with no realization, renders the located compile_error! that rust_exact_binding_spelling already produces, so there is no silent choice. The phantom struct stays only where no row exists. Stage0: v1_compiler_emit_rust.rs is regenerated. std_types.rs gains `pub type Unit = ();`, because std.types Unit is a bare opaque declaration with an exact row (RustUnit) that the old emitter emitted nothing for. claim_executor --required-regen reports first_generation_equal=true. Controls (test.claim.opaque_exact_row_alias_witness_test, each read from the emitted text): - std.types Unit, reached only by its row, emits `pub type Unit = ();` (absent before this rule); - a row-less opaque declaration keeps its phantom struct; - Symbol keeps its row alias. v1 admission (gunbc.v1_maintenance_standing v1_seed_standing): this serves the v2 self-host program, because the emitted compiler closure must build with the v2.std.node host-text String. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * 04_infer: bind the literal payload family once in the gather Review 73303 on #12809 (finding 2) flagged the pattern this PR introduced: each family arm matched a variant only to rebuild it for infer_gather_literal_payload_step. The gather now binds the family once, with one arm for InferNotALiteralPayload and one for every family (DESIGN section 2). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * carrier_by_spelling: cite the importer census by symbol, and its structural-using population The census is gunbc#12840 (royal-lark-857). Instrument: v2.lens.text_string_importer_census verdict_with_crossings, whose identity join closes (407 = 391 String importers + 16 non-members). The structural-using population, the declared v1/v2 divergence, is 7 modules, named here. It is a lower bound: 120 unclassified and 2 unmeasured importers stay open. #12760 stays a draft until #12840 and the import-deletion PR land. The symbol is cited in prose only, and joins the evidence list once #12840 lands. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * carrier_by_spelling: the structural-using population is 15 (census revision 7b87f99) After neat-boar-16's fixpoint ruling, #12840 classifies 15 structural-using modules. Eight of them are structural only because they pass host text into a module that keeps its import. v2.compiler.tokenize and v2.std.integer are named divergence sites (ruling 1), 10 parse-refused modules keep the import (ruling 4), and 24 remain undecided. The second instrument, text_string_importer_fixpoint, is added. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * floor: the live-tree closure reads the process-shared index (one index for the environment and kernel-types closures) closure_paths_of built a fresh MultiEntryIndex over the live dag root per call. A diff touching std/types.dag asks for both the parse-environment and kernel-types closures, so the same name set was indexed twice and #12765's guard refused the floor (MultiEntryIndexBuiltTwiceForOneNameSet, both sites namespace_baseline.rs closure_paths_of). The revision-tree index in evaluate_owned_item_in is a distinct source set and is left as is. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * Carry one live-tree index to both closures instead of using the thread's shared slot The shared slot holds the floor's own dag+src/v2 index; a dag-only demand there evicted it and the floor refused SharedIndexRebuiltAfterEviction (#12848's own floor). LiveDagIndex is built on first demand by the floor's baseline reconstruction and passed to environment_agreement and kernel_set_serves_both (-> kernel_names_at), so the two closures share one build and the shared slot is untouched. The roundtrip test shares one too. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * string_literal RFM: the literal-at-structural refusal is a stopgap; #12809 is its trigger neat-boar-16's ruling on #12760: since #12759 carries the literal's value, the lawful route is the unfold. The row now cites gunbc#12809 (parked on #12726 PR2 and #12506) as the trigger that flips bla_host_text_literal_at_structural_string_refuses to an unfold control. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * lexing: import unicode_char_code_point from std.unicode.char_class This branch moved it out of std.unicode.types (to break the std.types cycle); main's new v2.std.compilers.lexing imported it from the old module, so the v2-native emit of 00_compile refused (emit-build). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * WIP v2 resolve: lexical references keyed by occurrence; infer/eval/translate/emit read them * legacy_repair_tap witness: import Present/Absent from v2.std.optional The witness matched git_sha1_object_id's Optional result with bare Present/Absent. v2.std.execution_surface also declares Absent | Present (a9388e4, the same commit), so once a closure holds both, the four reads are ambiguous and the floor refuses PureProducerShareRowModuleUnframeable (AmbiguousBareNameRead, sites=4). The value variant Present { value } is v2.std.optional's; execution_surface's carries no field. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * WIP: lift unscoped atom arm; flatten infer pattern * WIP: argument may not begin after a newline * WIP: walk-population fixture mints its bound references, as the parser does * Restore main's text in the gap-analysis plan: its non_empty spellings record measurements taken on the old name (review 73826) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * v2 resolve: a loop carrier is a binder, kept as the atom it names, never a lexical reference * Debt roster: retire (std/content_hash.dag, get) as NotAReference The floor refused RosterStale: content_hash's get is the builtin get(xs:, index:), whose pair came from the whole-pool fallback resolving it to an unrelated pool fn get. be51d1f (bare loader asks per name) removed that, and retired the same builtin-get pairs elsewhere (e.g. extdeps/bootloader/grub.dag) as NotAReference. This branch touches content_hash.dag, so its row is the one this floor judges. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * Review 73872: drop the unused Char classifier; the gate checks its structural strings with v2.std.algebra non_empty - std.unicode.char_class keeps only unicode_char_code_point (consumed by tokenize and lexing). CharClass and char_in_class had no consumer anywhere and are deleted rather than rehomed. - gate's displaced_cost / mechanism_class are v2.std.text String = FreeMonoid<Char>. Passing them to std.types string_non_empty (host text) crossed representations with no declared unfold (DESIGN section 4). The gate now calls v2.std.algebra non_empty, the structural carrier's own check; main's private non_empty_string stays deleted. - The vocabulary comment no longer claims String inhabits no FreeMonoid carrier. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * Arrow-body-form mutation mirrors place the lexical-reference arm, as production does * Integration: real three-way merges of the generated stage0 files; name Filesystem's declaring module at its five bare readers The five bare Filesystem reads (harness_cli, harness_turn, runner_microvm_boot_probe, scm.repository_load, scm.repository_save) call Filesystem.Read/Write/List, the extdeps.filesystem.filesystem_io service that v1.compiler.emit_rust emit_file_call binds, so that module is the import. They were refused AmbiguousBareNameRead once #12381's std.types edit brought them into the floor's prepared closure. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * Integration: thread #12947's lexical field through #12381's where-predicate walk resolve_where_predicate_operator converts resolve_atom's Outcome through the existing resolve_walk_of_outcome (a type's where clause has no lexical binders in scope, and resolve_atom carries no lexical answer), and the unwalked where-set edge carries an empty lexical list. With this, v2.test.claim.parameter_reference's five assembled-program rows (the four the floor failed on #12947 plus pr_named_fn_parameter_is_a_parameter_reference_holds, red on main) return true: #12381's where-predicate binding is what cures main's resolve_unbound_name_is_declared_in_several_modules at the where clause. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * Revert "Merge #12760 (neat-ibex-696/kernel-string) into the integration branch (generated conflicts taken from ours; regenerated below)" This reverts commit 2688462, reversing changes made to d5446f3. * Integration: take #12760 back out (operator option A); regenerate #12760's own carrier_by_spelling row orders it after the String import-deletion PR, which has not started. Its merge is reverted, the source-type binding row it added is re-derived away by claim_executor --regen-round-cost (fixed point, rebuild_packages=0), and the defork audit's String row returns to main's. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * Integration: #12947's occurrence matches take main's OccurrencePending (#12790) A pending occurrence has no id yet, so it is read like a synthetic one: resolved_tree_lexical_binding finds no binding (Absent), and resolve_lexical_reference refuses it as unkeyed (resolve_reason_lexical_reference_unkeyed). emit-build and the generated lane refused both matches as non-exhaustive on bc718d2. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * Integration: main's resolve_arrow_resource_requirements atom arm carries #12947's lexical field Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * Integration: name the declaring module at three bare reads the combined closure made ambiguous extdeps.cloud.gcp.sts and extdeps.tailscale.acl_api read String bare, declared by both std.string_type and v2.std.text; they import it from std.string_type, the dag/extdeps convention (acl_api's std.types import of String bound nothing). gunbc.systemd_property_directive_overlap reads Unit bare, declared by std.types and v2.std.cardinality; it imports std.types Unit. The floor refused these as AmbiguousBareNameRead (CLAIM-SCOPE) on 430d11d. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * Integration: revert #12381's annotation-only edit in an excluded wet receipt; file the floor class it trips The floor selects an annotation-only hunk as a changed witness, contrary to DESIGN section 4c, and refused the head with ChangedWitnessOutsidePreparedSubject for test.manual.command_runner_local_argv_receipt (on the hermetic exclusion list). The annotation correction (non_empty -> string_non_empty) is reverted so the honest edit is not what blocks the integration; the stale annotation and the capability that lets it be restored are rostered as gunbc.recurring_failure_mode annotation_only_edit_selects_a_changed_witness. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * Integration: the two spark get rows keep main's Retired ImportsFixed standing Main (#12954) retired them after fixing those imports; a merge here had carried the older ActiveDebt rows forward, which the floor refuses as RosterRetirementChanged. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>

Brian Searls and others added 16 commits September 27, 2026 16:30

v2 resolve: ResolvedTree carries the SymbolIndex resolution consulted…

03342a3

…; cut every consumer root-first Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

Merge origin/main; migrate the remaining resolved-tree helpers (typec…

179c7f1

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

pick_ingested: the arrow extractor returns the arrow Node (my retype …

95856ef

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

Merge origin/main; retype main's new resolved-tree helpers (declared_…

84d4768

…parameter_order, reference_closure) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

Merge origin/main into the carrier (kinds stays a separate once-prepa…

c12bf6d

…red input); retype main's new resolved-tree test sites Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

Merge origin/main (#12379 landed)

341a092

Merge origin/main (#12379 landed); #12379's new hand-built infer inpu…

0fb011f

…ts use the named no-declarations constructor Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

Merge origin/main (declared_signature moved to v2.std.arrow_signature…

23697f7

…); typecheck clean over 116 files Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

Merge origin/main (#12440 landed)

66c401b

Merge origin/main (5 commits); one_member_cost_probe keeps main's wan…

ec7c3de

…ted symbol and reads .root Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

Merge origin/main

cd88b7d

plain_type_decl_lowering (new from main): its assembly helpers carry …

2b8dc42

…ResolvedTree and walk .root Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

Merge origin/main

3f95faa

Merge origin/main; body_let_annotation (#12540's new rows) carries Re…

c90dae3

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

Merge origin/main (#12432 landed as a squash)

9d653a0

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

resolve: ResolvedTree comment states symbol_index's consumers once (n…

f293dcb

…o later stage reads it; #12407 reads resolved_declarations) (review 72652) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

gunbai-bot Bot pushed a commit that referenced this pull request Sep 29, 2026

Merge #12629 (comment fix)

89074cb

gunbai-bot Bot mentioned this pull request Sep 29, 2026

variant_field_lowering: five claims read what normalize emits now (source-spelled Int, the wildcard form) #12650

Merged

gunbai-bot Bot added this pull request to the merge queue Sep 30, 2026

This was referenced Sep 30, 2026

v2 infer: type a match over a declared (generic) coproduct and its arm binders #12641

Merged

Plan: one resolution of declaration-body types per ingest (namespace + body providers on ResolutionContext) #12726

Merged

github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Sep 30, 2026

gunbai-bot Bot added this pull request to the merge queue Sep 30, 2026

gunbai-bot Bot pushed a commit that referenced this pull request Sep 30, 2026

Plan: smart-newt-725 reads #12629's resolved_declarations (not an ind…

970276c

…ex of its own); it moves in the deleting commit Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

Merged via the queue into main with commit ba19b72 Sep 30, 2026
5 checks passed

gunbai-bot Bot deleted the session/wise-bat-862-resolved-decls branch September 30, 2026 09:18

gunbai-bot Bot mentioned this pull request Sep 30, 2026

v2 infer: a record construct's field values are judged against the fields its record declares #12763

Merged

gunbai-bot Bot pushed a commit that referenced this pull request Sep 30, 2026

Merge origin/main (#12629 landed as a squash)

9ce7fd5

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

gunbai-bot Bot mentioned this pull request Sep 30, 2026

v2 resolve: named-fn parameter references as path-keyed references; infer grounds them through the index #12766

Merged

gunbai-bot Bot pushed a commit that referenced this pull request Sep 30, 2026

Merge origin/main (#12629 landed)

fe05a18

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

gunbai-bot Bot mentioned this pull request Sep 30, 2026

v2: one roster of kernel value types; a declared Bool is judged (dag_binding_type_bool deleted) #12785

Merged

gunbai-bot Bot mentioned this pull request Sep 30, 2026

v2 inhabitance: a String literal meets a structural text type at the one judge, via the declared unfold (stacks on #12760) #12809

Closed

Navigation Menu

v2: lower the where-refined head so resolve binds it; ResolvedTree.resolved_declarations (base for #12407) - #12629

v2: lower the where-refined head so resolve binds it; ResolvedTree.resolved_declarations (base for #12407)#12629
gunbai-bot[bot] merged 17 commits into
mainfrom
session/wise-bat-862-resolved-decls

gunbai-bot Bot commented Sep 29, 2026

Uh oh!

gunbai-bot Bot commented Sep 29, 2026

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

0 participants

Conversation

gunbai-bot Bot commented Sep 29, 2026

The boundary, measured

What lands

Step-0 census (receipt)

Controls

Declared frontier (condition 1)

Uh oh!

gunbai-bot Bot commented Sep 29, 2026

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

0 participants