M0: //gunbc/instruments:type-declaration-use-census — resolved type-declaration and cast census (nominal-type plan)

[gunbai-bot]

M0 of the nominal-type plan (gunbc#13024, docs/plans/nominal-type-declaration-plan.md §2). Stacked on #13026 (deep-badger-684's native census row), which should land first. The precursor #13033 has already landed.

Status: lands as an instrument, with NO M2 sizing (operator ruling 2026-10-03). The nominal migration is parked until native resolve and infer coverage grow. Re-running this instrument is how that is decided.

The receipt: coverage verdict

• Run: instrument-dispatch 37119024146, label //gunbc/instruments:type-declaration-use-census, revision 163bb59. The receipt lines are in that run's job log, because the artifact's stdout.txt came back empty; that capture defect is filed as work item adhoc-82107088-798.
• Controls held: the fixture root's rows identity-joined in both directions, and the unindexed root refused with status 2.
• Whole tree: NO OBSERVATION (exit 2). Re-run the instrument for every figure; none is transcribed here (DESIGN §6). The frontier breaks down in two parts:
  • Unreached modules (no reference index, so their declarations and casts are unknown). Most of the corpus is in this state, in three groups:
    • Native resolve: dominated by resolve_reason_unbound_symbol, then resolve_reason_ambiguous_symbol. This is the namespace-cut and native-resolve frontier.
    • Front end: files the context refused.
    • A residue of other resolve reasons: construct_tag_not_a_constructor, anonymous-record typing, binder hiding, realized-declaration mismatch, an unbound where predicate, and an unlowered float literal.
  • Casts in modules that did resolve: every one is OperandTypeUndecided, and none is decided. In each case the module did not infer. That is the N7 native-infer frontier, led by find_witness_reason_no_candidate (a cast into an alias or refinement) and infer_grounding_not_derived. A module refuses infer on its first fatal, so one undecidable cast undecides all of its casts.
• What would make the census size M2: native resolve for the unbound and ambiguous population, and native infer admitting a cast into an alias or refinement. Neither needs a census change.
• Typecase-shaped sites (D3): none observable, because no cast was decided.
• §2 table findings: bodyless declarations without nominal_opaque; one-field records; Opaque's second disjunct; encoding pending S2. These are recorded as open items in the plan's Parked note (PLAN: one nominal type-declaration model; delete refinements #13024 head 1666a95), not as code.

What it is

• gunbc test //gunbc/instruments:type-declaration-use-census is one more row in the native census family. V2NativeCensusProducer now carries a reading (ResolveRefusalReading for the existing row, TypeDeclarationUseReading for this one), so it is not a second registration pattern (sharp-raven-357's ruling).
• The walk: census-infer. A new native-driver verb that resolves and then infers every ingested module. Its per-module step, v2.compiler.compile native_census_module_inference, is the same infer the native lane demands (native_test_infer_resolved). It is shared with census part 2: quiet-boar-260's Design: census part 2 — inference/emit census below resolve #13019 §2a reads the refused arm. One infer walk, not two. census-resolve keeps its cost and meaning.
• The folds (gunbc.instruments.type_declaration_use_census) read the resolved and inferred trees, never text:
  • Declarations: the form comes from emission's own authority (v2.compiler.emit_produced module_member_class). Refinement carrier and predicates are read through v2.compiler.infer refinement_declaration_of_node, split out from refinement_declaration so the census has no second reader. Modifiers come from v2: carry the type-declaration modifier slot on NormalizedTree (M0 precursor) #13033's carrier.
  • as sites: the target is the declaration the cast resolves to. The operand's type comes from infer's own reader (infer_branch_operand_resolved_type_in_tree). The immediate parent supplies the evidence: compare, order, add, a call (by callee path plus the declared parameter type), or the fn's declared return.
• The receipt: a cross-module join. Every row carries {module, symbol | enclosing@occurrence, form, class, witness, evidence}.
  • A declaration nothing references is UNCONSUMED before any other class.
  • A strip with neither workaround nor declared-position evidence is an EXCEPTION (plan M3 list), never NominalProjection (ruling from the plan's author).
  • A cast whose module did not infer, or whose operand infer left on its frontier, is OperandTypeUndecided, with its cause.
  • A module with no reference index (front-end or resolve refusal), or a declaration whose form is undecided, makes the run refuse with exit 2.
• Out-of-gate list: the binary prints affected <module>. The host reader (gunbc.instruments.type_declaration_use_census_reading) filters those through v2.workflow.required_floor required_gate_admits into out_of_gate lines for M2's PR body. The gate is read host-side, so the emitted compiler's closure does not carry a workflow roster.

Controls

• Receipt interface (test.claim.type_declaration_use_census_witness_test, 18 claims, all PASS remotely at 9fee458). The rows are supplied: one declaration and one cast of each class, the mutation control (introduction rewritten as projection changes class), and an unindexed module refusing with no observation.
  • These were written after the classifier, so their discriminating reds were shown by planting the two defects each guards against, at the same head. Classing an unevidenced strip as NominalProjection turned exactly a_strip_with_no_parent_evidence_is_an_exception_not_a_projection_holds red. Dropping the UNCONSUMED check turned exactly an_unreferenced_declaration_is_unconsumed_not_alias_holds red.
• Real route, run by the instrument before the whole tree:
  • Fixture root (type_census_fixture_files): an identity join in both directions against the expected rows.
  • Unindexed root: must exit 2.
• Verb plan: native_driver_plan_test has a new claim that census-infer plans as its own word, and its pinned usage strings are updated.
• Stage0 mirror: v1_compiler_emit_rust.rs was regenerated remotely. The second --required-regen reported no drift.

Findings and departures, stated rather than hidden

1. Introductions are mostly undecided today. A cast into an alias or refinement (n as Port) makes native infer refuse its whole module (find_witness_reason_no_candidate, the N7 frontier). Those modules' casts come back OperandTypeUndecided, so NominalIntroduction coverage is low until native infer admits the crossing. The real-route fixture pins that cast as undecided, so it goes red when infer improves. Whether coverage is enough to size M2 is reported with the receipt, not assumed.
2. Classes the §2 table has no row for:
   • Bodyless: a declaration without a body and without nominal_opaque (type MachineWidth<bits>) is BodylessUnclassified.
   • Resource: a resource declaration is ResourceUnclassified.
   • One-field records: classed UnconstrainedNominal (a public raw constructor over its field).
     The table may want rows for these. Reported, not invented into the plan.
3. Opaque, second disjunct: "a nominal whose view no consumer outside its module reads" is not computed. Only nominal_opaque decides Opaque. Computing the rest needs view-read evidence.
4. Encoding: casts stripped to encode cannot be classed OperationWorkaround:encode because encoding has no capability home yet (§9 S2). An encode-shaped call lands in the exception list, with the callee named in its evidence.
5. Field and let positions: these give no NominalProjection evidence yet. Only call parameters and fn returns do, so those sites are exceptions.
6. Seed template change: the verb's loop is hand-written Rust in the seed's driver template (src/v1/05_emit_rust.dag), beside census and census-resolve, following their precedent. Every decision in it is a .dag fold. It is admitted under the v1 purpose test as v2-instrument plumbing.

Hand-written seed Rust receipt

• What is new hand Rust:
  • target_invocation_host run_type_declaration_use_census and fixture_file_rows.
  • cli_run::native_lane_runner run_census_infer_with and run_type_declaration_use_census_runs, plus the V2NativeCensus { reading } field.
  • run_v2_native_census is census A: native census refusals grouped by fatal reason; //gunbc/instruments:v2-native-census #13026's, carried in by the stack, and is not added here.
• Named lane that executes it: gunbc test //gunbc/instruments:type-declaration-use-census. This is the instrument seam DESIGN "Building & checks" prescribes ("a row in instrument_registry and an arm here"). Every decision it makes is a .dag fold: type_declaration_use_census_standing, the fixture rows, and the receipt in gunbc.instruments.type_declaration_use_census. The host writes files, spawns the binary and passes values.
• Admission: gunbc.v1_maintenance_standing v1_seed_standing purpose test. The Rust is v2-instrument plumbing (the census measures v2's own resolved and inferred trees). No seed semantics change.

🤖 Generated with Claude Code

[gunbai-bot]

On the hand-written seed Rust advisory (review 74687, and 74636 before it): the receipt is in the PR body under Hand-written seed Rust receipt. It is a deferral that names its lane: gunbc test //gunbc/instruments:type-declaration-use-census executes the new host Rust. The section also cites the admission (gunbc.v1_maintenance_standing v1_seed_standing purpose test). Every decision is a .dag fold; the host writes files, spawns the binary and passes values. run_v2_native_census comes from #13026, which this PR is stacked on, and is not new here.

— sent from tidy-koi-264

[gunbai-bot]

M0 whole-tree receipt. The run is instrument-dispatch 37119024146 at 163bb59, label //gunbc/instruments:type-declaration-use-census. The receipt lines are in the job log; the uploaded stdout.txt artifact came back empty, which is a capture gap in the dispatch workflow, not in the census.

Controls held. The fixture root matched its expected rows by identity in both directions, and the unindexed root refused with status 2. The whole tree's verdict is no observation (exit 2), as designed, because modules are unreached.

Coverage: too low to size M2. I am not shipping the sizing.

• Unreached modules: 6097 of 7426 ingested modules never produce a resolved tree on the native route. That breaks down as:

  fatal reason	modules
  resolve_reason_unbound_symbol	4748
  resolve_reason_ambiguous_symbol	923
  front-end file refusals	373
  other resolve reasons (construct_tag_not_a_constructor and 7 more)	53

  They have no reference index, so their declarations and casts are unknown. Those are the namespace-cut and native-resolve frontiers, not census defects.

• Casts: in the 1329 modules that did resolve, all 1200 as sites are OperandTypeUndecided, and 0 are decided. In every case the module did not infer: find_witness_reason_no_candidate 861, infer_grounding_not_derived 154, and the rest are spread over field, return and argument inhabitance refusals. This is the N7 infer frontier: a module refuses on its first fatal, so one cast it cannot cross undecides all of them.

Declaration totals, over the 1329 resolved modules only. These are a lower bound by construction:

class	count	note
Sum	846
MultiFieldRecord	469
UNCONSUMED	247
UnconstrainedNominal	157	108 one-field records, 49 brand-only refinements
TrueAlias	37
BodylessUnclassified	28
Opaque	1	extdeps.access.posix_effective_principal EffectivePosixPrincipalName
CheckedConstructionStage	1	extdeps.network.ipv6 Hextet

Most refinements sit in modules that do not resolve, which is why the last two rows are so small. The affected and out-of-gate lists each have 334 entries.

Typecase-shaped sites (would reopen D3): none observable, because no cast was decided.

§2 table findings:

1. BodylessUnclassified (28): bodyless declarations without nominal_opaque (type MachineWidth<bits> and similar) have no row in the table.
2. One-field records (108): these are in UnconstrainedNominal. The table does not say whether a one-field record is a nominal or its own class.
3. Opaque's second disjunct: "view read by no outside consumer" is not computed. Only the modifier decides it.
4. OperationWorkaround:encode: not classifiable until S2 names encoding's home.

What would make the census size M2: native resolve for the unbound and ambiguous population, plus native infer admitting a cast into an alias or refinement (the find_witness_reason_no_candidate arm). Re-running the instrument after those land re-derives everything above; no census change is needed.