Actuation phase 2: the endpoint-path state machine and the unlink admission

[gunbai-bot]

First slice of the actuation bundle. No host mutation. This lands the model and the wall a later mutating step must pass through. Stacked on #7595 (runner_activation, build_cache_instance); the diff here is two new files.

The defect

srv4, observed 2026-08-01: no listener, no process, no unit, a server.sock on disk, and an sccache error log whose entire contents are Address in use (os error 98). A server born inside a runner cgroup died with that cgroup without unlinking its socket, so every later server fails to bind. The host has been uncached since roughly 2026-07-26 for that reason alone.

BuildCacheEndpointObservation.EndpointAbsent cannot express this. It answers is anybody listening — the right question for placement, the wrong one for actuation. Under it, srv4 and a host that simply has no cache yet are the same state. They are not: one needs a unit started, the other needs a file removed first and then a unit started, and starting the unit without removing the file reproduces error 98 forever. A state-space conflation whose cost is measured rather than hypothetical.

So EndpointPathState is a separate axis from the owner — absent / listening / stale socket / path conflict / unavailable. EndpointStaleSocket and EndpointPathAbsent both project to EndpointAbsent on the ownership axis, which is exactly the distinction that axis is not built to carry.

Why the unlink is admitted rather than an ExecStartPre

The obvious fix is ExecStartPre=/bin/rm -f server.sock, and it is an absorbing fallback — it unlinks in every path state rather than the one where unlinking is correct:

state	what the unconditional rm does
EndpointPathAbsent	harmless no-op — which is what makes it look safe in testing
EndpointPathConflict	destroys a file this lane did not create
EndpointListening	severs a live server's socket — every healthy restart, every double-start race

The listening case leaves a running process no client can reach and that will not be replaced, because it still holds memory and still parents compiles. Silent in exactly the way the stale socket was silent, so the remedy recreates the disease one layer up. And an unconditional rm never reports having removed something it should not have, so the deficit's frequency is zeroed by construction.

admit_stale_socket_unlink admits only from EndpointStaleSocket under ObservationCurrent; every other state is a positively named, located refusal. The unlink is a separate admitted step before the unit start, able to refuse independently of it — never a line inside the unit.

Three shapes deliberately avoided

• The admission takes the observed state, not four Bools. An all-true evidence record is hand-writable and re-checks what the observation already decided — validation wearing construction's clothes, the same defect review 46217 found in the owner context. The four facts an observer must establish are stated as its contract, not re-represented as data.
• ObservationCurrencyUnknown refuses exactly as ObservationStale does. Not knowing whether a read is current is the same evidence as knowing it is old. An arm that graded them would fire precisely when /proc is least readable — which is when a bind race is likeliest.
• A TCP endpoint refuses at admission, not at command construction, so no admitted value exists for which no command can be built.

Test plan

Green by execution — 8 controls, 0 failures:

claim_batch --source-root dag --source-root src/v2 \
  --entry dag/test/claim/build_cache_endpoint_path_test.dag

PASS witness_the_srv4_stale_socket_is_the_one_state_that_unlinks
PASS witness_a_live_listener_is_never_unlinked
PASS witness_a_non_socket_path_is_never_unlinked
PASS witness_an_absent_path_refuses_rather_than_no_ops
PASS witness_an_unreadable_path_does_not_default_to_stale
PASS witness_a_stale_read_cannot_license_an_unlink
PASS witness_a_tcp_endpoint_has_no_stale_socket_state
PASS witness_the_unconditional_sketch_differs_where_it_is_destructive

unconditional_unlink_sketch is the RED control — ExecStartPre=rm -f written as a predicate, answering true in all five states. Two witnesses assert the admission differs from it on the two destructive states rather than merely asserting the admission refuses: a refusal where the naive fix would also have been harmless proves nothing about the wall's worth. Per DESIGN §4b the control stays enrolled rather than retiring once the wall lands.

Honest residual

.dag has no visibility modifiers, so a caller can hand-write EndpointStaleSocket with no observation behind it — an explicit lie in the source rather than a forgotten check, the same residual BuildCacheInstanceReady carries. It closes when node/subtree visibility grants make the constructor private to its observer.

No observer producer ships here. That is deliberate: the observer is a mutating-adjacent host read, and the operator's sequencing holds host work until the generated units, this state machine, captured-base adoption, rollback, and the controlled-load protocol are reviewed together.

[gunbai-bot]

review 46581 — finding 1 is real and now fixed in 8d19c16; finding 2 I'm not acting on, with receipts below.

Finding 1 — the pool receipt was unbound. Correct, and it was my defect.

admit_runner_activation bound the cache receipt to the activation two ways — its instance host against the deploy host, and its managed_unit against the instance's intended_unit — and gated the pool receipt beside it on two Booleans alone. A pool observed on a different host, or a correctly-observed slice with some other name, admitted activation. That is the same unbound-receipt defect the unit comparison exists to prevent, sitting in the sibling field, and the asymmetry is exactly how it survived being written: the receipt that got the attention got the binding.

HostCompilePoolReady now carries its host, and two comparisons gate admission — pool_receipt_is_for_host and pool_receipt_names_intended_pool.

One deliberate choice worth flagging, since your finding named gunbc_managed_compile_pool_slice as the thing to compare against: the slice is compared to BuildCacheInstance.intended_compile_pool instead. Comparing to the global default would make the wall agree with a constant rather than with the instance being activated against — weaker, and visually identical.

Two new controls, green by execution alongside the existing 16:

PASS witness_a_pool_receipt_from_another_host_is_refused
PASS witness_a_pool_receipt_naming_another_slice_is_refused

Both, not just the host case: one receipt is about the wrong machine, the other about the wrong cgroup on the right machine, and a wall catching only the first would still activate a runner whose compiles are charged outside the intended pool.

The finding also pushed the producer to land in the same commit — gunbc.host_compile_pool derives the receipt, so it is no longer purely hand-authored. Its load-bearing witness reads the real gunbc_compile_pool_placement row and asserts false: the row is CompilePoolInRunnerSlots, so activation refuses fleet-wide today. That is the correct answer, and precisely what a hand-written all-true receipt was silently contradicting.

Finding 2 — the hand-rolled-predicate rule. I checked for it and can't find it.

I looked before declining, and three things point the other way:

1. DESIGN.md contains no predicate/walker dissolution rule. The only match in the tree is docs/plans/e0599-implementation-proposal.md §3.0 — an unmerged proposal, not an authority my brief points at.
2. There is no canonical fold to consume. BuildCacheServerPlacement and EndpointPathState have no *Fold surface anywhere in the corpus (unlike ProbeEffectOnSubjectFold, which does exist and which this PR does thread). "Consume the canonical surface" has no referent here.
3. The peer module already does it this way. gunbc.host_build_cache_provision eliminates these same coproducts with direct exhaustive match in verdict_for_placement and provision_build_cache_verdict. Introducing a fold for two five-arm predicates would fork the module's idiom, not converge it — and DESIGN §4 names Match as one of the six closed behaviors, so exhaustive coproduct elimination is the substrate's normal elimination form rather than a simulated relationship.

The lens that does exist in this area targets hand-unrolled folds over lists — a recursion written out by hand — which is a different shape from a total match over a closed coproduct. If there's a specific rule or lens I've missed, point me at the carrier and I'll fix it; I'd rather converge than argue the idiom.

— sent from smart-stag-201

[gunbai-bot]

review 46625 — correct on both counts; fixed in ee51f21.

witness_ready_pool was the third HostCompilePoolReady construction site and 8d19c16e updated only two. Now carries host: srv4_runner_host_deploy.host_label as HostIdentity, and the module is green by execution — all 10 witnesses including the three callers you named:

PASS srv4_enables_five_named_runner_instances
PASS unenrolled_host_cannot_enable_runner_units
PASS red_control_admission_blind_builder_rejected_by_gate
(+7)

And you're right that the previous test plan overclaimed. That run was real — 18 witnesses across host_compile_pool_test and runner_activation_wall_test — but those are the two modules I edited, not the closure of the type I changed, so the third site was never compiled and the "green by execution" line covered less than it read as covering. Worth naming precisely because it's the second time this lane hit the same shape: the ProbeEffectOnSubjectFold literal in claim_evidence_probe_rule.dag was missed the same way earlier, caught then by the compile-clean gate rather than by me. The rule I should have been applying: after changing a record or coproduct, enumerate every construction site of the type, not the files in the diff.

Also in this push:

• review 46621 (non-blocking): the two stale runner_enable_command citations in gunbc.plans.fleet_subsumption_manual_gaps are repointed. Only two of six occurrences were stale — the other four name the deleted symbol as history (the deletion note, the RED control's provenance, the host_standup rationale) and are deliberately left, since a citation of a deleted thing is only rot when it asserts the thing still exists. The B1 row's present-tense claim was repointed; the 2026-07-22 hand-run account now records runner_enable_command as the then-current path rather than being silently rewritten, because the enable it describes is precisely the readiness-blind one that produced this fleet's birth defect and repointing it would erase the receipt.
• origin/main merged (Require managed build-cache readiness before runner activation #7595 landed). The three add/add conflicts were Require managed build-cache readiness before runner activation #7595's squash against this branch's copies; resolved to this branch, verified by diffing each file against origin/main — zero lines from main are absent here, so it is a strict superset rather than a judgement call. mergeable=MERGEABLE at 1a2839c9.

— sent from smart-stag-201

[gunbai-bot]

review 46655 — finding 1 fixed in 4ea52de. Finding 2 I'm still not acting on, but I dug further this round and found more than I reported last time; details below.

Finding 1 — real, and my own fixture was certifying the hole

derive_compile_pool_readiness matched CompilePoolSliceObserved and bound limits: _, discarding the observed ceilings, then reported CompilePoolReady carrying the size derived from the jobserver. The receipt asserted a sized pool on the strength of a number nobody had compared to the host.

Worth being precise about the class: this is fabricated readiness, not a missing check. The observation was already in hand and was thrown away — so it was never a gap awaiting a producer, it was fail-closed inverted at the one carrier whose entire job is deciding whether compiles have a bounded parent. An unbounded ceiling parenting every cache-miss compiler is exactly the defect this lane exists to close, so getting it wrong here specifically is worse than getting it wrong anywhere else in the diff.

Now compares memory_max against the derived size, with a new PoolSliceCannotHoldDerivedSize { required, observed_ceiling } refusal. Against max rather than high deliberately: max is the ceiling that actually bounds the cgroup, while high is a throttling watermark the kernel permits to be exceeded, so sizing against high would admit a slice whose hard limit sits below the compiles it must hold.

And your pointer at host_compile_pool_test.dag:10 is the sharpest part of the finding: observed_slice built all-zero limits and witness_a_declared_and_observed_slice_is_ready passed anyway, so the acceptance set was ratifying the defect rather than catching it. The fixture now carries a ceiling that can hold the derived size, and a new sibling pins the case it used to admit — both halves, because without the positive fixture the derivation could refuse everything and still pass, and without the new one it could admit everything.

PASS witness_a_slice_below_the_derived_size_is_not_ready   (+7)

Finding 2 — I checked harder this time, and I found the mechanism you're pointing at. It doesn't cover these.

Last round I said I could find no such rule. That was under-researched, and two things I've since found are worth putting on the record because they cut partly your way:

• src/v2/lens/non_fold_residue exists and enforces exactly the shape you name — non-fold residue must be rostered, matching DESIGN §6's "a finished stage is one fold; any non-fold residue is either a named irreducible kernel or un-migrated modeling."
• A predicate-level disposition precedent exists: gunbc.fleet_posix_accounts fleet_posix_account_exists_predicate_disposition: Disposition = Scaffold { ... }.

So the discipline is real. What I can't establish is that it reaches these two functions, and one piece of evidence is decisive: main is green, and gunbc.host_build_cache_provision alone carries 13 such arms, with the same shape widespread across dag/gunbc/**. If the lens fired on Bool-returning exhaustive matches in domain modules, main would be red right now. non_fold_residue is a v2.lens roster over compiler-pipeline residue, not a wall over domain-layer coproduct elimination — and DESIGN §4 names Match as one of the six closed behaviors, so exhaustive elimination of a five-arm coproduct is the substrate's normal elimination form.

On the disposition receipt: I'd rather not add one than add a false one. Disposition = Scaffold asserts a thing is temporary with a dissolution trigger. pool_is_declared and admission_yields_unlink are not scaffolds — they're the intended shape — so stamping them as such to clear a review would be a dishonest mark in a repo whose whole discipline is that marks mean what they say.

That leaves a genuine disagreement rather than an oversight, and I'd rather resolve it than keep restating it. If you can point me at either (a) the lens or gate that should fire on these and currently does not, or (b) the canonical fold surface for BuildCacheServerPlacement / StaleSocketUnlinkOutcome that I should be consuming — noting neither type has a *Fold anywhere in the corpus, unlike ProbeEffectOnSubjectFold, which this PR does thread — I'll take the fix immediately. Absent that, converging these two while leaving the hundreds already on main would fork the idiom rather than close it.

— sent from smart-stag-201