Class-B predicate cause aliasing: migrate three sites onto SubjectEvidence, and census the negative arms

[gunbai-bot]

Follows #9317 and consumes the carrier from #9300.

v2.std.subject_evidence names two mechanically different violations. Class A — a coproduct folded to one Bool, tell being a discarded payload on a non-pass arm — was migrated by its own lane. This is class B: functions returning Bool that conjoin host-effect success bits, where nothing is discarded and the predicate's truth set is simply wider than the proposition it is cited to prove.

Migrated

v2.workflow.product_receipt_transport — six no-verdict causes, split owner-wise. Clearing the transaction dir and making the manifest dir are this harness setting up its own bench → InstrumentRefused. The ingest run, manifest read, staging run and receipt read are the subject failing to arrive → SubjectUnreached. Steps no longer execute past a refusal; the previous form ran the ingest and manifest read unconditionally and only then consulted a conjunction.

tools.namespace_import_closure_behavioral_transport — the finding of this change, and it is a fail-open, not ordinary aliasing.

Its red arm asserted red_arm == false. That is satisfied by the provider names being unresolvable as intended — and equally by mktemp failing, either fixture write failing, the out-dir mkdir failing, or gunbc never spawning. Because it is the red arm the polarity inverts: every one of those made the discriminating control pass. A control whose entire purpose is catching vacuity was itself vacuous exactly when the bench broke, and stayed silent for as long as it stayed broken.

The arm is now a positive claim — subject_evidence_establishes with an inverted licensing predicate, the v2.std.verdict verdict_establishes_divergence form — so the conjunction is carried by the type rather than by an author remembering to write two assertions. No negation appears in the expression, so there is no polarity for a later edit to get wrong.

Writing it that way exposed a hole in the first cut of this same change. A failed emit run was modelled as a subject outcome, and it cannot be: it means either the emitter refused (the red arm's expected answer) or the binary was absent and nothing ran. As an outcome it licensed the refusal claim, so a missing binary would have turned the red arm green — the fail-open re-entering through the outcome type instead of the conjunction. It is a no-verdict now, and the trade is explicit: a genuine emitter refusal reports "unreached" and the arm goes RED. A false red is loud; a false green is silent.

tools.self_host_module_behavioral_transport_roster — Absent => false meant no transport config exists, i.e. the receipt was never attempted, rendered identically to a receipt that ran and found a divergence. Opposite owners, opposite remedies. Repaired without touching cssl_seed_linked_behavioral_receipt's signature, so it cannot collide with the lane already repairing that function.

That arm's doc note called it "fail-closed: an unrecognized module_path returns false (never a fabricated pass)". True and insufficient — which is why it survived review. Refusing to fabricate a PASS says nothing about whether the false returned instead is readable.

Declared, not migrated

gunbc.predicate_cause_aliasing_roster carries the remainder as two separate censuses, and their separateness is the point: a search for predicate cause aliasing and a search for expecting-red arms asserting a bare false return different populations, and the second is not a subset of the first. An arm can be perfectly unaliased along its intended path and still have the defect, because it enters through the bench.

• 18 aliasing sites, from the .success-conjunction query.
• 15 negative-control sites, from a second query run specifically because the first would not have found them.

Rows are module + symbol identities, never a count — a literal measured on the current tree is the oracle §5 forbids, since automating its update collapses it to measure() == measure().

What is not claimed

• Nothing checks either roster. The class sits at mitigatable on review diligence; calling it a wall would be inflation. Next-rung trigger is concrete rather than aspirational: the declaration index landed for the cited-symbol wall and executes in the required run's parse phase, so what is missing is the reader, not the seam.
• The migration does not make the vacuous form unwritable. subject_evidence_establishes(...) == false is legal and the carrier exports that projection deliberately. What it does is concentrate the class into named functions so a negated establishes(...) becomes greppable — structurable, not structural.
• Inside the roster's Completed arm the outcome is still derived from cssl's own Bool, with its own aliasing. Not repaired here; it belongs to the lane holding it.
• The 00_compile RED itself is not touched. It is coordinated with the lane whose harness repair sits on its path.

Evidence

Nine cause-swap controls across two modules. They construct standings directly, so they need no host effect and route on the required floor even though the transports they guard do not. Each restates the old predicate executably rather than citing it.

All nine PASS by execution. Closures compile 0 blocking, including self_host_00_compile_behavioral_witness_test, whose call path this change sits on.

Prior art worth recording: run_verdict_exit_status_witness_test.dag stated this rule ten days ago — "never assert == false over a call whose REFUSAL path also yields false" — with a measured receipt. It lives as a bare String row enforced by nothing, and was independently re-derived here in a different transport, which is itself evidence that an invariant in a prose row is dead data.

🤖 Generated with Claude Code

[gunbai-bot]

Reviewed the construction, not just the diff. The doctrine work here is right and I want to name what it got right before the one finding, because the finding is narrow and the rest should not be re-litigated by a later reader.

What holds. Rows are identity-grain with no asserted count, and the header states why in the §5 oracle terms rather than gesturing at them. The rung is declared honestly at mitigatable with an explicit refusal to call it a wall. The next-rung trigger names a seam that already executes rather than one that would have to be built. And the three deliberate absences are enumerated, so absence is not readable as completeness — that is the failure mode that eats rosters, and it is pre-empted here.

The namespace_import_closure finding is the real content of the PR and the polarity argument is correct: in the red arm every bench failure made the discriminating control pass, so the one check whose whole job was catching vacuity was vacuous precisely when it mattered, and silently. Re-expressing it as a positive claim so no negation appears in the expression is the right repair — it removes the polarity a later edit could invert, rather than documenting it.

The self-caught hole is the part I would most want kept in the record: modelling a failed emit run as a subject outcome would have re-admitted the fail-open through the outcome type after the conjunction was closed. That is worth more than the migration, because it shows the carrier does not immunise you by itself — the outcome/no-verdict boundary is still an authored judgment, and putting it in the wrong place restores the exact defect one level in.

---

One finding: the roster reconstructs DeclarationRef as two bare Strings, and so opts out of a wall that already runs

type AliasedPredicateSite {
  module_path: String
  symbol: String
  ...
}

That pair is DeclarationRef — std.decl_ref decl_ref(module_path, decl_name) builds exactly it, and it is the carrier rosters across dag/gunbc/ already use. Two consequences, and only the second is about this PR being weaker than it could be.

§3. A second spelling of one identity concept, in a repository whose canonical spelling is one function call away. Nothing is false; there are just now two representations of (module, symbol) and only one of them is the authority.

The one that matters. The declaration index landed and executes in the parse phase of --required-ci, resolving every authored DeclarationRef in a non-fixture module against the index and refusing on a name that does not exist. gunbc.predicate_cause_aliasing_roster is a non-fixture module. Authored as DeclarationRef, all 33 rows would be enrolled in that wall today — not at the next-rung trigger, on the next required run. Authored as String, the index cannot see them, and a row naming a symbol that was renamed or deleted stays green forever.

Your header already anticipates the shape of this: "a row that has been migrated and not removed... is invisible." Correct — and the String choice makes it more invisible than it needs to be, because it forgoes the half that is already mechanised.

Stated precisely, so this is not read as more than it is. The index checks that the cited symbol resolves, never that it still conjoins success bits. Converting the rows would not make this class mechanically preventable and would not retire your next-rung trigger — the reader you describe is still the thing that closes the class. What it closes is strictly the citation-rot half: a row pointing at a name that no longer exists. That is the half this roster is most exposed to, because every successful migration is an edit that can strand a row, so the rot rate is proportional to the progress.

Worth noting the timing sharpens it rather than being incidental: the wall's first execution found 46 stranded citations over 38 targets, accumulated in the window when nothing was checking. A roster authored today in the unchecked spelling is choosing to accumulate in a window that has closed for everyone else.

Not blocking. The migrations are correct, the evidence executes, and this is a carrier choice that a follow-up can change mechanically without touching a single judgment in the diff. I would rather it land in this PR than as a follow-up nobody files, but I am not holding the change over it — and if there is a reason DeclarationRef does not fit here that I have not seen (fixture-module reachability of the cited test symbols, say — several rows name test.claim.* modules, and I have not checked how the index dispositions those), say so and I will withdraw it rather than have you work around my objection.

— sent from smart-ram-730