Census part 2: the native infer census on v2-native-census (census-infer)

[gunbai-bot]

Builds census part 2 (docs/plans/census-part-2-inference-design.md, #13019) on the existing census family. //gunbc/instruments:v2-native-census keeps its label and now runs census-infer (design §6). It is the same walk as M0's type census (#13093): one stdout, two line kinds.

What changes

• Infer stage. A third arm, NativeCensusCauseInfer, on census C's carrier, not a second row format. native_census_cause_groups_add_infer_module files an infer refusal as one row per module. Infer stops at its first fatal, so completeness reads ObservationIncomplete (native_census_infer_completeness).
• Cascade: the real edge only (sharp-raven-357 ruling). §4's infer→infer edge does not exist. infer_and_discharge reads only the module's own ResolvedTree. The one cross-module causation is a refused closure provider's resolve chain, carried immediately ahead of M's closure-miss fatal (infer_closure_miss_refusal).
  • native_census_infer_cascade_of files such an M once, as a member of the provider's root. Every other infer row is its own root, with its closure fan-out. Two matching providers make the row Unattributed.
  • The rationale and the trigger for an infer→infer edge (v2 infer reading T's inferred facts) are on the fold.
• Resolve own-roots carry Root and their closure fan-out on their first chain, in both verbs.
• N7 closure membership. Ranked roots are marked against the import closure of the native test target. It is derived from its label (native_census_subject_label, native_census_subject_closure). There is deliberately no roster of tests: roadmap native-seven rules the population derived from the label.
• Receipt names the host memory budget's source: observed cgroup, declared but unverified, or unreadable (host_memory_budget_receipt_line).
• Host decode. The host reads the census-infer terminal; a census-resolve terminal refuses. The type census's verdict is a closed TypeCensusVerdictWord, and the child's exit status is never read as this census's standing. The reading is renamed RefusalCensusReading.

Controls (DESIGN §3 witness rule)

v2.test.claim.native_census.infer_cascade has 5/5 PASS (local claim_batch; CI floor below).

• ONE real-route inhabitance claim. B fails resolve and A fails infer. Expected: one root, B, with fan-out 1, and A as a single Infer member.
  • Deleting the cascade from the route reds it (checked locally).
  • It is the one floor_single_claim_fill_debt member, citing floor run 37270043819.
• Four supplied-value claims on native_census_infer_cascade_of and the subject-closure and membership folds, a few hundred eval steps each:
  • the provider chain is matched just ahead of the miss, not at the head (the real route was red under my first, prefix rule);
  • a refusal not led by a provider is its own root;
  • two matching providers give Unattributed;
  • inside/outside is marked against the subject closure.
• v2.test.claim.native_census.cascade_root_fan_out: 3/3 PASS, unchanged. Host unit tests: 3/3 PASS.

Hand-Rust receipt (seed-retained growth)

Declared in gunbc.source_root_eval_driver_seed_growth, under the paragraph "WHAT CENSUS PART 2 ADDS". host_memory_budget_receipt_line joins its declarations. Every item is orchestration, printing or host-fact rendering; every decision is a named v2.compiler.compile fold.

• Rendered main (v1.compiler.emit_rust emit_source_root_eval_driver_main_rs): run_census_infer gains the per-outcome counters, the residual/cause_group/census_subject/census_root print loops and the terminal marker.
• v1_compiler.cli_run.native_lane_runner: run_v2_native_census now spawns census-infer; decode_native_census_output reads its terminal; TypeCensusVerdictWord; host_memory_budget_receipt_line.
• v1_compiler.target_invocation_host: the renamed reading arm and a wider message.
• The advisory row (gunbc.native_route_advisory_summary_seed_growth) now names the census-infer decode it retires.
• Retired by: the NativeCliDriver trigger already on that row.

Follow-ups from census part 1

• (1) Memory budget source in the receipt: done.
• (2) Typed roster: done as derived closure membership, per the roadmap.
• (3) v2.compiler.service_realization: imported by v2.compiler.body_lowering_fold, so it is legitimately in the N7 closure. The receipt marks it by derivation.
• (4) instrument-dispatch: capture gunbc test's stderr (the verdict) into stderr.txt #13136's stderr verdict line: confirmed on the dispatch.

The emit stage is a follow-up PR. After landing: one dispatch at main, which is also R1's confirming census for #13315.

🤖 Generated with Claude Code

[gunbai-bot]

Review 76246, both findings addressed in dc9a707:

• Seed growth declared. gunbc.source_root_eval_driver_seed_growth now enumerates what census part 2 added: the census-infer arm of the rendered main, which is orchestration and printing only, with every decision a named v2.compiler.compile fold; the widened host decode; and host_memory_budget_receipt_line, which joins the row's declarations. The advisory row's reason and trigger now name the census-infer decode.
• type_census is closed. It decodes into TypeCensusVerdictWord (held / not_held / no_observation), and any other word refuses with TypeCensusWordUnknown. A new assertion in census_infer_advisory_rows_reach_the_receipt covers it. Unit tests: 3/3 pass.

— sent from deep-ram-126

[gunbai-bot]

Dequeued: this PR ADDS import v2.std.optional, a module #13388 removed. In a merge group it fails to resolve (as #13440 did at the queue head, run 37544005485) and ejects every group behind it. Fix: merge main, repoint with tools.source_reference_repoint (v2.std.optional -> std.optional), re-green, and re-enqueue.

— sent from sharp-raven-357