PR A: model Cargo execution placement; make the roster-bijection outcome typed

[gunbai-bot]

First of the falsifier-recovery series. Subject: interpreter_dispatch_bijection_real_roster_red_holds, the last remaining batch-2 failure.

Why this PR exists in this shape

The falsifier's component receipt for run 31703924598's predecessor (31685755058) reports the witness as:

interpreter_dispatch_bijection_real_roster_red_holds (...) returned Bool(false)

That is the entire diagnosis available after ten days red. The transport ended in run.success, so cargo was missing, the clone failed, the tests ran and disagreed, and — the one that matters most — the compile SUCCEEDED where this test requires it to refuse were all indistinguishable. An untriageable failure cannot be ranked, and an unranked failure is one nobody owns. So this PR does not begin by guessing the cause; it makes the cause reportable.

What landed

gunbc.cargo_execution_placement — placement as its own axis. extdeps.rust.cargo_build owns the intent; nothing owned which executable runs it, where, so consumers expressed it the only way left: a path literal inside a shell string. This transport hardcoded /opt/cargo/bin/cargo twice, and its own note said why — the modeled cargo.Build.Test spells argv ["cargo", ...], which resolves through PATH, and PATH's cargo here is a shim that dispatches to a remote builder. A local-workspace subject cannot run remotely, so the transport routed around the model instead of the model carrying the distinction.

decide_cargo_placement is total, and a remote builder serving a RequiresLocalWorkspace subject refuses before execution rather than being attempted and diagnosed from a nonzero exit.

Typed outcome. CargoInvocationOutcome keeps not attempted (an environment obligation) apart from failed (a subject finding) — different remedies, so different arms, even though both answer false.

The declared limit — please read this rather than the diff

Only cargo's existence is observed. shell.Which.Check also declares path: FilePath?, and that field is deliberately not consumed: under wet execution it returns a bare stdout String rather than an Optional, so match Present/Absent raises a non-exhaustive match on the path itself. That is the Value::Null / Optional straddle DESIGN already carries as an open thread, sitting at the service-output boundary.

So: the hardcoded literal is gone and the invocation now works on any host whose cargo lives elsewhere — but locality is not established. A PATH cargo that is itself a remote-dispatching shim still satisfies the admitted arm. The placement decision is modeled and its refusal arm is real and witnessed; what is missing is the observation that would let the decision be made about a named executable instead of a name. A dissolve-on sits at the call site, triggered by the Value::Null split.

I would rather land the triage fix with that boundary stated than consume a known-unreliable field to claim a wall I do not have.

Evidence

Five hermetic claims, green by execution, and the discrimination is measured: regressing decide_cargo_placement to admit the remote arm reds remote_builder_refuses_a_local_workspace_subject.

Not claimed: that the wet witness turns green. It needs a runner with a local cargo and ~11 GiB for its clone-and-build — a cadence job, not a session job. What this PR guarantees is that the next cadence run reports why rather than Bool(false).

Note: hermetically the witness now refuses with no mock_response for operation Check. shell.Which.Check declares no mock; that refusal is fail-closed rather than fabricated, and the witness is ReadsLiveTree (deferred from per-PR discovery, run wet by the cadence). Adding a mock would change hermetic answers for every Which.Check consumer, which is a wider change than this PR should make.

Context

Two of batch-2's three failures were retired by #8222 and I verified both wet on merged main: self_host_logic_behavioral_receipt_holds and namespace_import_closure_receipt_holds both return true, the latter with four green arms and its red arm correctly refusing. This is the third.

[gunbai-bot]

Both items from review 51730 verified against the code. The first was a real defect I introduced; fixed in 74c823102a1.

Finding 1 — fixed. You are right, and the diagnosis is exact: RelocatableSubject × RemoteBuilder was answered with RemoteBuilderCannotServeLocalWorkspace, a cause label that flatly contradicts its own arm, leaving RemoteBuilder with no admitting path and no way to say why. That is the §3 state-space conflation this file's own header warns about, reproduced inside the function written to remove it.

The two remote refusals are now distinct causes because their remedies differ. RemoteBuilderCannotServeLocalWorkspace is permanent — the subject is bound to the machine holding the workspace, and the remedy is to stop asking. RemoteBuilderRealizationUnbound is a missing capability — a relocatable subject genuinely could use a remote builder, but nothing in this repository binds one, so there is no executable to name. Collapsing them made the capability gap unreportable.

I chose the honest-cause option over your first alternative deliberately: admitting the relocatable arm needs a path on RemoteBuilder, and I am not going to invent a remote-builder realization that has no consumer just to give a variant an admitting path — that would be modeling for symmetry rather than for a fact.

Two new controls, green by execution: relocatable_subject_refuses_for_an_unbound_realization_not_locality pins the cause identity, and the_two_remote_refusals_read_differently asserts the projections diverge — so re-collapsing them reds a witness rather than passing silently. Seven claims now pass.

Finding 2 — confirmed, not fixed here, and homed rather than hand-waved. You are right that until a consumer reads _outcome(), the receipt keeps saying Bool(false) and the stated benefit does not land. I checked what it would take: a witness test fn returns Bool, and the only text the component receipt carries besides that is an interpreter runtime error (that is why the batch-6 rows could say failed to execute 'npm' while this one could not). There is no witness-side refusal primitive. So the options are to change what the claim runner carries from a witness, or to raise a runtime error deliberately — and the second is abusing an error path to smuggle a diagnostic.

That wiring belongs in PR C of this series, whose subject is exactly the receipt surface (FloorRunProgress vs FloorTerminalReceipt, and making noncompletion legible). I would rather land it there, with the receipt change, than bolt a diagnostic channel onto this transport. Scoped and tracked, not deferred indefinitely.

— sent from silent-bee-502

[gunbai-bot]

CI red here is inherited, not caused by this PR. The failing gate names dag/extdeps/programmable_logic/ice40/supply.dag:

compile-clean: source annotation sits inside a declaration body. Only module-item
grain is modeled; move it above the declaration it describes.

This PR touches three files — gunbc.cargo_execution_placement, its witness, and the roster-bijection transport — and none of them is that one. The file arrived with #8214, after this branch was cut, and PR CI evaluates the merge ref, so the failure rides in from main rather than from the diff.

Fix is up as #8235 against main (the annotation moves to module-item grain; the prose is preserved because it carries a real modelling fact about why the NVCM arm answers none). Once that lands I will merge main into this branch to pick it up and re-run.

Not asking for this to be waved through: build, regen and heal_generated_artifacts are green on 74c8231, and the only red is the inherited compile-clean gate.

— sent from silent-bee-502

[gunbai-bot]

Correcting my own overstatement about this PR, before it merges.

I wrote in a status summary that this PR means "the failure that reported Bool(false) for ten days will report a cause." That is wrong, and it contradicts what I told review 51730 in this very thread: until a consumer reads run_interpreter_dispatch_bijection_real_roster_outcome(), the receipt keeps saying Bool(false). The production entry point still returns Bool.

The accurate claim is narrower: this PR makes the cause representable and preserves it through the transport. It does not make production report it. The live consumer is #8239. Asserting otherwise is the producer-without-consumer class this series exists to remove, so I would rather correct it here than let it stand in a summary.

Rescoping the acceptance honestly, rather than treating approvals as discharging it:

• A1 — what this PR delivers: placement modeled as its own axis; a total decision with a witnessed pre-execution refusal; the two remote refusals distinguished by remedy; typed CargoInvocationOutcome replacing the exit-code Bool; both hardcoded /opt/cargo/bin/cargo literals gone. CI-green, two approvals, discriminating RED measured.
• A2 — still open: binding the invocation to an exact LOCAL cargo artifact. This PR resolves by existence only and passes the bare name through PATH, so a PATH cargo that is itself a remote-dispatching shim still satisfies it. Blocked on the Value::Null / Optional straddle at the service-output boundary, declared in the module and at the call site with a dissolve-on.

A2 is not discharged by A1 having approvals. It is a separate obligation and it stays open.

— sent from silent-bee-502