Converge refuses srv5/srv6 by name instead of failing to match them

[gunbai-bot]

The hazard

gunbc.spark.serving_desired asserts one realization for every host holding SparkServingCell: an Ollama runtime serving a DeepSeek GGUF artifact. The serving-cell roster is srv5 and srv6 — and those two hosts are currently running a vLLM tensor-parallel deployment that no desired state in this corpus models.

So a wet convergence today would not fail to find its target — it would find it and assert the wrong thing: install Ollama over a working tensor-parallel pair and report success. Every part of that behaves as specified, which is what makes it destructive.

Why a refusal rather than leaving them off a roster

A non-match is not a refusal. It holds only while the manifest happens not to match, emits no diagnostic when it stops holding, and one edit to spark_serving_desired_manifest silently turns it back into an actuation. This lands the refusal as a modelled fact: subject, cause, discharge condition.

Where it sits

spark_serving_role_scoped_desired_members_in, before role dispatch, through the SparkServingRoleScopedDesiredRefused channel the module already has. That function is the sole production constructor of serving desired members — spark_serving_desired_members has no other non-test caller — and serving_converge_slice_wet reaches it via spark_serving_axis_for_observation → spark_serving_full_membership_plan. There is no second door.

The reason is a typed coproduct, not a sentence, because the arms discharge differently. RunsARealizationNoDesiredStateModels ends when the corpus grows a vLLM realization and desired state selects it — a modelling act with an observable completion. HeldByOperatorDecision ends only when the operator says so. One string would make a hold a PR can lift look identical to one it cannot.

The withholding roster is a parameter, for the same reason spark_cell_role_in takes one: an arm's evidence must not depend on which machines are withheld today, or the wall's own witnesses go red on the day the wall is deliberately removed.

Executed evidence, not a typecheck

Full witnesses lane with the wall live: verdict=FloorClean, claims_failed=0, unexpected_failures=0, planned=executed=3539. The fail-closed census found nothing else standing on the old premise.

Then the discriminating RED — wall disabled in place, same five claims re-run through claim_batch:

FAIL w_a_withheld_host_refuses_although_its_role_admits_serving
FAIL w_an_operator_hold_withholds_the_same_way
PASS w_withholding_one_host_leaves_the_others_planning
PASS w_the_production_roster_reaches_the_arm_its_withholding_selects
PASS w_the_planner_scopes_desired_state_by_role

The three passes matter as much as the two failures: the mutation broke the wall, not the module.

One honest caveat: w_the_production_roster_reaches_the_arm_its_withholding_selects passes under mutation by construction — it reads the same predicate on both sides, so it is a fixture-vs-production drift check, not the wall's evidence. The wall's evidence is the fixture claim, discriminating because its host holds SparkServingCell: every role check passes, the planner is one step from building seven members, and it is still refused.

One rewritten claim

w_the_production_roster_reaches_the_serving_arm asserted that every production serving cell reaches the seven-member arm. That stopped being true when the wall landed — not from a planner regression, but because a wall landed in front of it. Written that way it would need editing every time the withholding list moves, making it a change detector. It now states the invariant: a withheld production serving cell refuses; one that is not reaches seven. Both arms stay meaningful whether the list is full, partial or empty.

Discharge

Read the running deployment back into a vLLM realization — parallel degree, KV dtype, max model len, max num seqs, worker population, image identity — and have desired state select it. These rows come out then, and not before.

🤖 Generated with Claude Code

https://claude.ai/code/session_01U397y4s3dSBof7vGPAX87G

[gunbai-bot]

Thanks — taking both nits, neither as a change, and one of them because it's wrong in a way worth recording.

The "; also " joiner. It never appears in the single-reason case: join over a one-element list emits no separator, so one row renders as just its reason sentence. The joiner is reachable only when two rows name the same host, which is the case the annotation above it is about. So there's no awkward single-reason rendering to fix.

But the fact that it read as though there were is worth keeping, because it's the honest cost of the design choice directly above it: I deliberately did not mint an ambiguity arm for duplicate rows. The neighbouring spark_cell_role_in has one, and needs it — two rows there can name two different roles, so the roster genuinely fails to decide what the host is. Here every row says the same thing about the decision (withheld) and differs only in why, so an ambiguity arm would be a variant for a state that changes no outcome. The joiner is what that choice costs: a rendering path that only exists for a case the model doesn't otherwise distinguish.

The 0 - 1 sentinel. Agreed it reads awkwardly, and it's pre-existing — w_role_scoped_count already used it before this diff, as the "refused" encoding for a function whose green values are member counts. I kept it rather than introducing a second spelling in the same file for the same idea; changing it is a separate cleanup over every use, not a rider on a safety wall.

Worth flagging one thing the review's framing gets slightly generous, since I'd rather it be on the record than accepted: the summary credits the tests with exercising the "roster changes don't silently break the check" property via the parameterized _in form. That's true of the fixture claims. The production claim (w_the_production_roster_reaches_the_arm_its_withholding_selects) does not discriminate — it reads the same withholding predicate on both sides of the match, so it passes whether the wall fires or is inert. I verified that by disabling the wall in place: it stays green while the two fixture claims go red. It's a fixture-vs-production drift check, not evidence the wall works, and the PR body says so.

— sent from eager-pike-541