Sequence the websocat install so a failed step stops the chain, and witness what ran

[gunbai-bot]

The defect

srv3_ensure_websocat ran four host mutations — mkdir, chown, curl, chmod — plus a readback, with no step gated on the outcome of the one before it. A failed mkdir was followed by a download into a directory that does not exist, a chmod of a file that was never written, and a readback of that.

The returned Srv3HostPredicate was correct in every one of those cases. That is why no witness in the file could see it: the value was right and the execution was wrong. Only an action trace can catch that class.

This is the same shape as the eager-argument regression fixed in #8695 — in a strict language, moving an effectful call from a branch into an argument position changes when it runs, with no signature change and no type error.

The cut

The sequence is now modeled rather than implied by evaluation order:

• WebsocatStage — the seven stages, named.
• websocat_after(stage, outcome) -> WebsocatStep — the sole transition authority.
• websocat_advance(outcome, next) — Holds continues; Fails and Unobserved both stop, and stop distinguishably. "The chown failed" and "the host was never asked" authorize the same non-action for different reasons, and collapsing them would be the empty-observation narrow pointed at a privileged mutation.

Every effect now sits inside a match arm. No effectful call is in an argument position or a let that precedes its own guard.

Two design errors I caught and rewrote before this was measurable: the trace initially re-derived the stage order, putting the sequence in two places (§3 fork) — it now reads websocat_after; and it used a _ => wildcard, which the non-fold-residue floor forbids.

Evidence — measured by mutation, not by reading

Mutation: websocat_advance rewritten to never stop, reproducing the pre-cut behaviour.

witness	base	mutated	restored
already_installed_runs_observe_only	true	true	true
unobservable_observation_runs_observe_only	true	true	true
a_failed_directory_ensure_stops_before_download	true	false	true
an_unobservable_ownership_ensure_stops_before_download	true	false	true
a_failed_download_stops_before_chmod	true	false	true
the_readback_never_runs_after_a_failed_step	true	false	true
a_fully_successful_install_runs_the_complete_chain_then_reads_back	true	true	true

The two observe-only witnesses staying green is correct, not a hole: they route through the ObserveInstalled arm of websocat_after, which this mutation does not touch. The positive control staying green is what stops the other four from passing on a walk that never runs anything.

One witness could not carry its own name, and the first mutation run proved it

the_readback_never_runs_after_a_failed_step was green under the mutation on the first run. Its five traces supplied six outcomes for a seven-stage chain, so under a never-stopping advance the walk simply ran out of outcomes at stage six and stopped short of readback anyway. It passed against exactly the defect it is named for.

That is the same off-by-one I had already caught in the positive control, present a second time. Fixed by supplying seven outcomes per trace; the table above is the re-run.

I am reporting this rather than quietly fixing it because it is the instrument failing, and a witness that cannot go red for its class is evidence of nothing — this file exists specifically because the previous witnesses were of that kind.

Merge

Main's witness floor is red from #8701 (fleet_desired_admission non-exhaustive over the split FleetDesiredRevision); #8738 fixes it. This branch is off e9e42f2f24 and will show that failure until #8738 lands.