Guarantee probe observation surface: compile_dag_diagnostic_census, and the first floor-class measurement

[briansrls]

The observation surface ladder-probe-corpus needs before any wall control can migrate, plus the first floor-class measurement it makes possible. Scope amended by the lane owner (2026-08-01) to admit exactly this one surface — see "Why a compiler change was authorized" below.

The problem this closes

The only .dag-callable v1 compile was compile_dag_rust_emit_check: it counts diagnostics passing compile_clean_diagnostic_is_hard and returns false when that count is nonzero. Everything else is discarded inside the host. Measured against the tests Stage 1a is supposed to migrate, that costs three specific things:

1. Class identity. The Rust RED asserts CallArgumentNameUnknown specifically. At Bool grain a probe refusing for any hard reason — a typo in the probe source included — reads as the wall firing. That is the proxy-assertion fail-open.
2. Blocking severity, and this one is a live regression hole. The filter is is_interpreter_blocking_diagnostic, so demoting a landed wall from blocking to advisory turns its migrated RED silently GREEN. ct_call_shape_wall_witness_test pins exactly this in its second assert; a Bool-grain migration would delete that assertion.
3. Advisories entirely, so a positive control cannot state zero-diagnostics-of-any-severity — the assertion review 45357 added after an advisory MethodExistenceUndecided passed unnoticed as a green control.

It is structural, not stylistic: Stage 0's ProbeObservation carries RefusedTyped { diagnostic_class, count } and AcceptedCounted { diagnostic_class, count }, and neither is inhabitable from a Bool. The Stage-0 vocabulary was uninhabitable on every v1 path.

What lands

• gunbc.compile_diagnostic_census — CompileDiagnosticCensusRow { diagnostic_class, subject_name, blocking, count } and the coproduct CensusObserved | CensusNotRunnable, with pure row selectors. No arm judges acceptance.

• compile_dag_diagnostic_census — one measurement-only builtin. Same compile path as its sibling; (class, name) is compile_clean_diagnostic_histogram_key (§3 projection, not a second diagnostic vocabulary); blocking is the existing compile_clean_diagnostic_is_hard delegation carried as data, so the severity policy keeps one home. Nothing is filtered — callers filter. Aggregation keys on (class, name, blocking) deliberately: folding severities together would hide the very demotion this surface exists to keep visible.

• CensusNotRunnable as a distinct arm, never an empty row list. An empty census is byte-identical to a clean compile, so could-not-measure would read as the subject passing (DESIGN §5, ⊤-as-answer vs ⊤-as-ignorance). Preserving the split at the host seam is what lets the probe layer map it to ProbeNotRunnable without guessing. A host panic is caught at the boundary and lands here with its cause.

• dag/test/claim/compile_diagnostic_census_witness_test.dag — green by execution: class identity, blocking severity (the demotion detector — it reds if a wall is softened to advisory), occurrence counts rather than presence flags, a clean-source control proving the harness is not uniformly refusing, and the NotRunnable vs empty-observation split.

  Both severity directions have live specimens, and the route there involved two corrections, both recorded rather than tidied away. I first concluded no advisory specimen could be produced synthetically — three candidates each either compiled silent or refused blocking. Corpus prevalence said otherwise (the whole-tree census carries 1,981 where-refinement advisories), so the class was demonstrably reachable and a probe finding none was evidence against the probe. A working specimen followed, and AcceptedCounted gained a producer.

  I then attributed the original failure to the closure — fixture-only compiles carry no std. A discriminating control refuted that too, and a 2×2 finally pinned the real axis, which was neither thing guessed. Crossing declaration site (a locally-declared alias vs std's brand — structurally identical: type NonEmptyStr = String where non_empty and type Tight = String where non_empty) against cast subject (literal vs unknown parameter):

	literal subject	parameter subject
local alias	silent	fires
std brand	silent	fires

Declaration site is irrelevant — a user-declared refinement alias is judged exactly as std's brand is. The axis is literal vs non-literal, and the diagnostic names it: "where-refinement unenforced: predicate non_empty on Product(Tight) — non-literal value at refined position". So the original probe's silence is correct behaviour: it cast the literal "x", and a literal at a refined position is deliberately exempt (the ladder working — construction deciding what validation would otherwise check). No census row is filed for it; doing so would have seeded the wall-implementer population with a below-floor claim against correct behaviour. It becomes the dead-probe worked example instead — the failure mode in its least obvious dress, since the probe does cast, at a fn boundary, against a properly declared refinement.

Mandate adopted as lane policy on the strength of this record: every below-floor or silent-class row the baseline stage produces carries a probe-adequacy receipt — closure and shape and the prevalence cross-check where a population exists — required, not advisory. Three consecutive mechanism explanations here were refuted while the conclusions they explained kept surviving; mechanism stories do not survive contact, executed discriminating controls do. Every superseded claim is kept in the gap analysis rather than overwritten, because the sequence is the lesson.

Probe-adequacy receipts for the four below-floor findings

The rule above applies first to the rows that prompted it. All four were originally measured under a fixture-only closure and have been re-run under the full dag + src/v2 pool, with the refined-brand cast as the discriminating control proving that harness can surface a diagnostic — so a zero there is the compiler's silence, not the harness's.

Finding	Closure	Result	Verdict
Generic instantiation	full pool	0 diagnostics	unchanged
Field through generics	full pool	0 diagnostics	unchanged
Parse: list separator	full pool	0 diagnostics	unchanged
Exhaustiveness, type-variable scrutinee	full pool	0 diagnostics	unchanged

All four declare only local types over kernel scalars, so the wider pool adds no machinery they depend on — but that is now measured rather than argued.

The measurement it makes possible

Six floor classes as probe pairs (deliberately-bad input plus legitimate control), v1 pipeline → Rust target, synthetic single module. Every control compiles clean.

Class	Bad input	Observed	Control
Generic instantiation	Boxed { inner: "not an int" } at Boxed<Int>	silent, 0 diagnostics	clean
Field through generics	fn get_field<T>(t: T) -> Int { t.no_such_field }	silent, 0 diagnostics	clean
Parse: list separator dropped	three elements, one comma missing	silent, 0 diagnostics	clean
Exhaustiveness, type-variable scrutinee	match t { Red => 1 } on T	silent, 0 diagnostics	clean
Exhaustiveness, coproduct scrutinee	missing arm on declared closed variant	refuses NonExhaustiveMatch, blocking	clean
Record completeness	record literal omitting a required field	refuses MissingField, blocking	clean

Two §1c census rows corrected by execution, both in the direction the census's Unknown default protects against:

• Record completeness was carried as Unknown — unmeasured; it measures R2.
• Closed-match exhaustiveness is not one rung — it splits by scrutinee path. And the row's attribution of the silence to PatternLookupBlocked => [] is wrong on the carrier: pattern_subject_from_node reaches that arm only where the scrutinee's inferred type is_compiler_error, i.e. where a diagnostic already exists. The silent arm is PatternDynamic { span: _ } => []. PatternLookupBlocked's own silence is not established by these probes and is not asserted as though it were.

Why a compiler change was authorized

The brief's scope said no compiler change. I stopped and escalated rather than improvising, because the alternative readings differ materially: migrating at Bool grain would be a declared rung lowering that deletes landed assertions (DESIGN §4b meta-obligation 3), and deferring would stall the node's highest-risk slice. The lane owner amended scope to admit exactly this surface, under five guardrails: one measurement-only builtin, projection of existing authorities only, fail-closed at the host seam, a registry row carrying its sibling's dissolution trigger, and evidence parity before any ct_ deletion.

On the contested ground: builtin_function_registry is itself a §3 fork awaiting the PrimitiveDefinition identity join, per gunbc.plans.compile_clean_forcecheck. The new row carries a note binding it to exactly its sibling's dissolution — when the join dissolves the registry, the two migrate together. One additive row is linear cost against that dissolution; the alternative was a schema no v1 probe could inhabit. The 04_method.dag diff is one row plus that note, nothing else.

Not in this PR

No wall lands and no wall is strengthened — probes measure. No ct_ test is deleted here: guardrail 5 requires the migrated probe to reach assertion parity in the same PR that removes the original, and that is slice 1, which also needs gunbc.guarantee_measurement (gunbc#7572) on main for the class/path identities. Nothing here builds against a copied schema.

🤖 Generated with Claude Code

[cursor]

Bugbot is not enabled for your account, so this pull request was not reviewed.

Enable Bugbot in the Cursor dashboard to get automatic reviews on future PRs.

[gunbai-bot]

Both findings in review 46144 are real and are fixed by construction rather than argued down. Pushed, not just replied.

Finding 1 — the exported projection reintroduced the fail-open. Correct, and it is worse than the review states: the module whose entire purpose is keeping could-not-measure distinct from observed-nothing reintroduced exactly that conflation at its own API boundary. The prose caution I attached ("a caller asking whether the subject was accepted must match the coproduct itself, never read a zero out of these") is validation standing precisely where construction was available — and the NotRunnable witness encoded the fail-open as an assertion (count(census_rows(not_runnable)) == 0), so the test suite was pinning the defect in place.

Fixed structurally: census_blocking_rows, census_advisory_rows, and census_rows_of_class now take List<CompileDiagnosticCensusRow>, so obtaining rows requires matching the coproduct. census_rows(c: CompileDiagnosticCensus) and its collapsing arm are deleted — the bad read is unwritable, not warned against. The caution deleted with the accessor rather than surviving beside it (§4b: a warning about a state that can no longer be written is dead text). Every witness now matches, with NotRunnable => false, so could-not-measure fails a witness instead of passing it.

Finding 2 — no qualifying hand-Rust receipt. Also correct, and the distinction you drew is the right one: the 04_method.dag note covers the registry row and inherits its sibling's PrimitiveDefinition identity-join trigger, which does not reach the Rust projection at all. Added a registered Disposition = Scaffold row with its own trigger, following the convention gunbc.compile_clean_diagnostic_policy already uses for its census transport. It dissolves when the substrate can read v1 diagnostics without a host transport — v2 self-hosting far enough for a probe to call the modeled compile, or a floor-enrolled diagnostic lens subsuming the projection — and explicitly not merely when the registry is replaced, since the projection is the scaffold and the registry row is only its type declaration.

Receipts: 6/6 witnesses PASS by execution, exit 0; whole-tree compile census re-running against the changed signatures.

Worth noting for the record: three prior approving reviews passed over finding 1. It was caught here, and it was the defect this PR was least entitled to ship.

— sent from snappy-eagle-314

[gunbai-bot]

Thanks — taking the note-duplication finding seriously, but I'm not acting on it, and here's the measured reason.

src/v1/stage0/src/v1_compiler_infer_method.rs is a generated file. Line 1 reads // Generated by v1 compiler -- do not edit. — it is produced from src/v1/04_method.dag by regen_stage0. So compile_dag_diagnostic_census_row_note() is not a hand-authored second copy of the note; it is the emitter's uniform projection of the single .dag data row into its Rust realization.

The precedent is in the same file and pre-dates this PR: filesystem_read_result_type_note() sits at line 23 on origin/main, generated the same way from data filesystem_read_result_type_note: String in 04_method.dag. Every prose data ... : String row in that module renders as a zero-arg function; mine is the second, not the first.

That makes this DESIGN §7 rather than §3. The .dag graph is the authority and Rust is one realization of it — a generated projection of a single authority is not a fork, or the whole seed would be one. There is exactly one place to edit this note, and it is the .dag row.

Both suggested remedies would be net-negative:

• Deleting the Rust function by hand edits a generated artifact, so regen_stage0 --verify would report divergence and red RegenVerifyGate — and the next regen would restore it anyway.
• Dropping the .dag-side note would delete the actual authority, and the generated function would disappear with it, taking the row's rationale out of the tree entirely.

The "no callers" observation is accurate and is also true of the sibling — these rows are documentation carried on the carrier per DESIGN §6 ("let the mark on the carrier be the authority; no parallel-ledger docs"), which is exactly why the note lives beside the registry row it explains rather than in a doc.

Non-blocking either way, and the rest of the review matches my own receipts. Leaving the diff as-is.

— sent from snappy-eagle-314

[gunbai-bot]

review 46306 is correct, and it caught the sharpest possible version of this lane's own failure mode. Fixed in 139f074c.

The four §1c rows listed ladder-probe-corpus probe pair, v1 CompileAccept in their Evidence column. That reads as a probe that exists and runs. It does not — those probe pairs are this node's future slice work. Compare the parse-separator row two lines down, which cites tidy-deer-730 probe on gunbc#7484 + review 45347: a landed, enrolled probe. Mine were forward-looking citations sitting in an evidence column, which is rung inflation in the canonical authority, filed by the lane whose entire purpose is to prevent it. Exactly four occurrences, exactly the rows named.

I did not take either of the two suggested remedies verbatim, because reverting to UnknownUnmeasured would throw away a real result. Those measurements were executed — via compile_dag_diagnostic_census, with the source snippets and outputs recorded in the §10 eighth-pass ledger, and they are reproducible today. What they are not is enrolled. So the honest state is neither "unmeasured" nor "probe pair exists"; it is measured-but-not-enrolled, and each Evidence cell now says precisely that: a one-off execution, NOT ENROLLED, nothing re-runs it, nothing reds if the behaviour changes. That is §4b meta-obligation 4 stated against my own rows rather than about someone else's.

I filed §11 item 10 for the enrollment obligation rather than folding it into item 9. They look similar and are not: item 9 migrates REDs that exist but run dark, while these four classes have no probe at all. One is a move, the other is authorship, and sizing them together would hide the difference. Item 10 also carries the bound while it stands — a rung whose only evidence is an unenrolled measurement is honest about the past and silent about the present, so it must not be cited as durable evidence — and its dissolution condition is each of the four carrying a probe pair on the class/path identities, at which point the Evidence cells name the executing probe the way the parse-separator row already does.

One scope note on what I deliberately did not touch: the misspelled-label row (§1c, the landed call-shape wall) cites probe pair pre 0 diagnostics → post two located refusals. That evidence is real but rides the dark Rust suite, which is a different defect with a different remedy — it is item 9's migration, and it is the first slice of this node. Rewriting it here would have conflated the two gaps your finding just correctly separated.

— sent from snappy-eagle-314