DeclarationRetires: the trigger shape the corpus writes in prose because no variant could hold it

[gunbai-bot]

The finding

std.dissolution modeled exactly one trigger shape:

type DissolutionTrigger = DeclarationAppears { ref: DeclarationRef }

It fires when the named declaration is found, so every trigger built from it is a forward reference to a carrier that does not exist yet.

That is the wrong shape for the retirement this corpus actually records. Read the corpus and the dissolve-on: marker names the subject — the declaration that must go away — not a carrier that must arrive:

• sol_console_send_script — "…retires its concat-built transport"
• configfs_op_line — "…removing the shell leaf"
• nbd_server_config_text — "…renders NbdExport structurally instead of the inline join"
• and their kin: "or the crate deletes", "the directory dissolves into generated emit", "delete this module … together"

With only the forward shape available an author had exactly two moves: bind forward to a symbol nobody has declared — which gunbc.runner_spec_from_offer refuses by name as the DESIGN §3 fabricated-citation class — or write the condition into a description string. The second move won. A description is unreadable to dissolution_status by construction, so the debt's retirement condition became something no mechanism can see.

The missing variant is the defect, not the authors. This is the arity finding: a fork downstream of a row indicting the row's arity rather than its value.

The change

DeclarationRetires { ref } fires when the named declaration is absent, over exactly the same present_decls evidence the forward shape already consumes. Presence discharges the forward trigger; absence discharges the retirement trigger — one dissolution_trigger_fired fn, the only place the two shapes differ.

It has a property its sibling lacks: its ref names something that exists today, so it is verifiable at the moment it is written rather than a promise about a name someone may or may not choose later. That is what makes it usable for this population without fabricating symbols.

Three production conditions migrate from unbound_dissolution to retires_dissolution — extdeps.bmc.serial_console, extdeps.linux.usb_gadget, extdeps.storage.nbd. Their irreducible rationale moves to // annotations (DESIGN §4c); the condition is now a trigger, so dissolution_is_bound is TRUE for all three where it was FALSE before.

Evidence — green by execution, with a discriminating RED

Subject: this branch. Ref: 4c05db315f (base 6c3fbeb960). Producer: ./target/release/gunbc run --source-root dag --source-root src/v2 --entry dag/test/claim/dissolution_census_mechanism_witness_test.dag --function <fn>, locally built v1-compiler.

function	result
a_retirement_trigger_is_pending_while_its_declaration_is_present	true
a_retirement_trigger_fires_once_its_declaration_is_gone	true
migrated_production_retirement_conditions_are_bound	true
supplying_a_bound_rows_declaration_reds_the_gate (pre-existing)	true
unbound_rows_stay_unbound_under_any_present_decls (pre-existing)	true

RED control — invert the DeclarationRetires arm of dissolution_trigger_fired to present (the pre-change behaviour) and re-run:

function	result under inversion
a_retirement_trigger_is_pending_while_its_declaration_is_present	false
a_retirement_trigger_fires_once_its_declaration_is_gone	false
supplying_a_bound_rows_declaration_reds_the_gate	true (unchanged)

Both new assertions flip while the forward-trigger sibling holds, so the perturbation discriminates the retirement arm specifically rather than breaking the fold globally. The inversion was reverted; the file is unchanged from the committed form.

required-regen: first_generation_equal=true planned=131 executed=131 (the declared_divergent=1 [main.rs] row is pre-existing). cargo fmt --all --check clean. The stage0 mirror src/v1/stage0/src/std_dissolution.rs is the emitter's own candidate output, copied from target/stage0-regen-candidate/src/, not hand-authored.

Measured population (subject: dag/, ref 6c3fbeb960, producer: a row-grain python scanner over module-scope data NAME: String|NonEmptyStr declarations)

• 388 rows whose value states a retirement condition, in 252 files
• of those, 308 rows in 214 files sit in a module with no typed dissolution carrier at all
• corpus-wide, unbound_dissolution( appears at 772 sites against 5 bound_dissolution(ref sites

A caution about the cut, because it is the part that cannot be automated: I tried to classify the 308 by whether the token after dissolve-on: resolves to exactly one live declaration. It yields 16 candidates, and reading them shows most are ordinary English words (carrier, named, witness, eval) that happen to collide with a declaration name. The marker is free prose and a mechanical bind is not sound over it — which is itself the argument against a sweep. What is always available is the direction this PR adds: the subject a debt row describes is a live declaration, so DeclarationRetires on that subject is expressible for this whole population without naming anything that does not exist.

What this does NOT claim

It does not make prose dissolve-on unwritable. It removes the reason the corpus wrote prose — there was no expressible typed form for the retirement direction — but the wall against new prose rows is still tools.prose_row_introduction_gate, still path-scoped by gunbc.prose_row_frontier prose_row_migration_scope, and none of these three modules is in that scope. Nor does it wire the migrated rows into gunbc.census_closure_frontier: that roster is folded against present_decls: [], under which every retirement trigger reports DissolutionFired by construction, so enrolling retirement rows there requires the census to be given the live declaration population first. That is a separate change and is named here rather than left to be rediscovered.