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

dag/gunbc/build_cache_endpoint_path.dag

@@ -0,0 +1,160 @@
+module gunbc.build_cache_endpoint_path
+
+import std.types { String, NonEmptyStr, Bool }
+import std.disposition { Disposition, SingleAuthority }
+import gunbc.build_cache_instance {
+  BuildCacheInstance, ProcessIdentity, EndpointObservationUnavailableReason,
+  unavailable_reason_detail,
+}
+import extdeps.cache.sccache { SccacheServerTcpPort, SccacheServerUnixSocket }
+import extdeps.exec.command { ArgvCommand }
+
+data build_cache_endpoint_path_scope_disposition: Disposition = SingleAuthority
+
+data endpoint_path_state_authority_note: String = "WHY THE ENDPOINT PATH NEEDS ITS OWN STATE MACHINE, AND WHY EndpointAbsent WAS NOT ENOUGH. gunbc.build_cache_instance's EndpointAbsent answers one question — is anybody listening — and that is the right question for PLACEMENT, because an endpoint with no listener has no owner whose cgroup could be classified. It is the wrong question for ACTUATION, and srv4 is the specimen that proves it. Observed 2026-08-01: no listener, no process, no unit, a server.sock file present on disk, and an 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 and the whole cache tree holds one file. srv4 has been uncached since roughly 2026-07-26 for this reason alone.\n\nUnder EndpointAbsent, 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. That is a state-space conflation of exactly the kind DESIGN's failure-mode list names, and its cost is measured rather than hypothetical — a host silently uncached for a week.\n\nSO THE PATH IS A SEPARATE AXIS FROM THE OWNER. EndpointPathState answers 'what is at this path', BuildCacheEndpointObservation answers 'who owns this endpoint'. They are not redundant readings of one fact: EndpointStaleSocket and EndpointPathAbsent both project to EndpointAbsent on the ownership axis, which is precisely the distinction the ownership axis is not built to carry."
+
+type EndpointPathState
+  = EndpointPathAbsent
+  | EndpointListening { owner: ProcessIdentity }
+  | EndpointStaleSocket { detail: NonEmptyStr }
+  | EndpointPathConflict { detail: NonEmptyStr }
+  | EndpointPathObservationUnavailable { reason: EndpointObservationUnavailableReason }
+
+data endpoint_path_conflict_note: String = "EndpointPathConflict IS NOT A STALE SOCKET AND MUST NEVER BE UNLINKED. It is the arm for a path that exists and is not a unix socket at all — a regular file, a directory, a symlink into somewhere else, a mount point. Nothing in this lane put it there, so removing it is destroying a stranger's data to make our own bind succeed, which is the widest possible failure arm. It refuses and stays refused; an operator decides what that path is. Keeping it distinct from EndpointStaleSocket is the entire reason the unlink admission can be safe, because 'the path exists but nobody is listening' is true of both and is the predicate an unconditional rm would be written against."
+
+type ObservationCurrency
+  = ObservationCurrent { observed_at_boot: NonEmptyStr }
+  | ObservationStale { detail: NonEmptyStr }
+  | ObservationCurrencyUnknown { detail: NonEmptyStr }
+
+data observation_currency_note: String = "AN UNLINK DECIDED FROM A STALE READ IS A RACE, NOT A DECISION. The four facts that make a socket stale are all observations, and every one of them can be falsified between the read and the write: a server can bind in that window, and the unlink then severs a LIVE server's socket, leaving a running process no client can reach and a cache that appears healthy from the inside. So currency is an input to the admission rather than an assumption of it, and it carries the boot id it was read under, because a reboot invalidates every pid, inode and socket fact at once. ObservationCurrencyUnknown refuses like ObservationStale does — not knowing whether a read is current is not weaker evidence than knowing it is old, it is the same evidence, and an arm that let Unknown through would be the absorbing fallback DESIGN section 5 forbids."
+
+type StaleSocketUnlinkRefusal
+  = PathAlreadyAbsent
+  | PathIsNotASocket { detail: NonEmptyStr }
+  | ListenerPresent { owner: ProcessIdentity }
+  | PathStateUnavailable { detail: NonEmptyStr }
+  | ObservationNotCurrent { detail: NonEmptyStr }
+  | EndpointHasNoSocketPath { detail: NonEmptyStr }
+
+data endpoint_has_no_socket_path_note: String = "A TCP ENDPOINT CANNOT HAVE A STALE SOCKET, AND THAT IS A REFUSAL RATHER THAN AN UNREACHABLE CASE. SccacheServerEndpoint is a two-arm coproduct and only the unix-socket arm names a filesystem path, so an unlink admission over a TCP instance has nothing to unlink. The tempting shapes are both wrong: silently succeeding treats 'there is no file' as 'the file is gone', which is the PathAlreadyAbsent answer to a question that was never askable; and treating the arm as unreachable puts a partial function at an actuation boundary. It refuses positively, so an observer that produced EndpointStaleSocket for a TCP instance — which it should never do — is reported rather than absorbed. Note this refuses at ADMISSION rather than at command construction: deciding it later would mean an Admitted value existed for which no command can be built, and the whole point of the admitted arm is that it licenses the action."
+
+type StaleSocketUnlinkAdmission
+  = StaleSocketUnlinkAdmitted {
+      instance: BuildCacheInstance
+      stale_detail: NonEmptyStr
+      observed_at_boot: NonEmptyStr
+    }
+  | StaleSocketUnlinkRefused {
+      instance: BuildCacheInstance
+      reason: StaleSocketUnlinkRefusal
+    }
+
+data unlink_admission_construction_note: String = "THE ADMISSION IS DERIVED FROM THE OBSERVED STATE, NOT CHECKED AGAINST FLAGS. An earlier shape for this carried a StaleSocketEvidence record of four Bools — path_is_socket, no_listener, no_fd_owner, observation_current — and admitted when all four were true. That is validation wearing construction's clothes: the four Bools are independently writable, an all-true record can be hand-authored with no observation behind it, and the check restates a constraint the observation already decided. It is the same defect the endpoint owner context carried before review 46217 collapsed three independent fields into one coproduct.\n\nSo admit_stale_socket_unlink takes the OBSERVED EndpointPathState and admits only from EndpointStaleSocket. The four facts are not inputs to be re-checked here; they are what the observer must establish in order to produce that arm at all, and they are stated on the observer's contract below rather than re-represented as data. Every other arm is a positively named refusal, so the refusal is typed, located and countable rather than a false Bool.\n\nWhat remains honestly open, and it is the same residual the activation receipt carries: .dag has no visibility modifiers, so a caller can hand-write EndpointStaleSocket with nothing behind it. That is an explicit lie in the source rather than a forgotten check. It closes when node/subtree visibility grants make this constructor private to its observer."
+
+data stale_socket_observer_contract_note: String = "WHAT AN OBSERVER MUST ESTABLISH BEFORE IT MAY RETURN EndpointStaleSocket. All four, in this order, over a single non-mutating read: (1) the path exists and stat reports a SOCKET — anything else is EndpointPathConflict; (2) the exact path does not appear as a listening entry in /proc/net/unix with St==01 — if it does, the state is EndpointListening and the owner is resolvable; (3) no /proc/*/fd entry resolves to the path's inode, which catches a process holding the socket open without listening, the case a /proc/net/unix scan alone misses; (4) the whole read completed under one boot id with no intervening reboot. Failing to read any of them is EndpointPathObservationUnavailable, never a default to stale — an unreadable /proc is exactly when a bind race is most likely, not least.\n\nThe chain is the same non-mutating /proc walk the endpoint-owner observation already uses, and it deliberately invokes no sccache: extdeps.cache.sccache records by measurement that --show-stats does NOT start a server and answers plausibly with no server in existence, so it cannot establish absence, and a real compile WOULD start one, which is a mutation. Neither is admissible evidence here."
+
+fn admit_stale_socket_unlink(
+  instance: BuildCacheInstance,
+  observed: EndpointPathState,
+  currency: ObservationCurrency,
+) -> StaleSocketUnlinkAdmission {
+  match observed {
+    EndpointPathAbsent =>
+      StaleSocketUnlinkRefused { instance: instance, reason: PathAlreadyAbsent }
+    EndpointListening { owner: o } =>
+      StaleSocketUnlinkRefused { instance: instance, reason: ListenerPresent { owner: o } }
+    EndpointPathConflict { detail: d } =>
+      StaleSocketUnlinkRefused { instance: instance, reason: PathIsNotASocket { detail: d } }
+    EndpointPathObservationUnavailable { reason: r } =>
+      StaleSocketUnlinkRefused {
+        instance: instance,
+        reason: PathStateUnavailable { detail: unavailable_reason_detail(reason: r) },
+      }
+    EndpointStaleSocket { detail: d } =>
+      match currency {
+        ObservationCurrent { observed_at_boot: b } =>
+          match instance.endpoint {
+            SccacheServerTcpPort { port: _ } =>
+              StaleSocketUnlinkRefused {
+                instance: instance,
+                reason: EndpointHasNoSocketPath {
+                  detail: "this instance's endpoint is a TCP port, which names no filesystem path, so a stale unix socket is not a state it can be in" as NonEmptyStr,
+                },
+              }
+            SccacheServerUnixSocket { path: _ } =>
+              StaleSocketUnlinkAdmitted {
+                instance: instance,
+                stale_detail: d,
+                observed_at_boot: b,
+              }
+          }
+        ObservationStale { detail: sd } =>
+          StaleSocketUnlinkRefused {
+            instance: instance,
+            reason: ObservationNotCurrent { detail: sd },
+          }
+        ObservationCurrencyUnknown { detail: ud } =>
+          StaleSocketUnlinkRefused {
+            instance: instance,
+            reason: ObservationNotCurrent { detail: ud },
+          }
+      }
+  }
+}
+
+type StaleSocketUnlinkOutcome
+  = StaleSocketUnlinkCommandReady { command: ArgvCommand }
+  | StaleSocketUnlinkCommandRefused { reason: NonEmptyStr }
+
+fn unlink_refusal_detail(reason: StaleSocketUnlinkRefusal) -> NonEmptyStr {
+  match reason {
+    PathAlreadyAbsent =>
+      "endpoint path is already absent; there is nothing to unlink and a unit start needs no precondition here" as NonEmptyStr
+    PathIsNotASocket { detail: d } => d
+    ListenerPresent { owner: _ } =>
+      "a listener holds this endpoint; unlinking would sever a live server's socket and leave it unreachable while it keeps running" as NonEmptyStr
+    PathStateUnavailable { detail: d } => d
+    ObservationNotCurrent { detail: d } => d
+    EndpointHasNoSocketPath { detail: d } => d
+  }
+}
+
+fn stale_socket_unlink_command(admission: StaleSocketUnlinkAdmission) -> StaleSocketUnlinkOutcome {
+  match admission {
+    StaleSocketUnlinkRefused { instance: _, reason: r } =>
+      StaleSocketUnlinkCommandRefused { reason: unlink_refusal_detail(reason: r) }
+    StaleSocketUnlinkAdmitted { instance: i, stale_detail: _, observed_at_boot: _ } =>
+      match i.endpoint {
+        SccacheServerUnixSocket { path: p } =>
+          StaleSocketUnlinkCommandReady {
+            command: ArgvCommand { argv: ["rm", "-f", p as String] },
+          }
+        SccacheServerTcpPort { port: _ } =>
+          StaleSocketUnlinkCommandRefused {
+            reason: "admitted unlink over a TCP endpoint, which names no path; admit_stale_socket_unlink refuses this at admission, so reaching it here means an admitted value was hand-written rather than derived" as NonEmptyStr,
+          }
+      }
+  }
+}
+
+data no_unconditional_execstartpre_note: String = "WHY THE GENERATED UNIT MUST NOT CARRY ExecStartPre=/bin/rm -f server.sock. It is the obvious fix for srv4 and it is an absorbing fallback: it unlinks in EVERY path state rather than the one state where unlinking is correct. Under EndpointPathAbsent it is a harmless no-op, which is what makes it look safe in testing. Under EndpointPathConflict it destroys a file this lane did not create. Under EndpointListening — the state that occurs on every restart of a healthy unit, and on every double-start race — it severs a live server's socket, leaving a running process that no client can reach and that will not be replaced because it is still holding memory and still parenting compiles. The failure is silent in exactly the way the stale socket was silent, so the remedy would recreate the disease one layer up.\n\nThe deficit's frequency would also be zeroed by construction: an unconditional rm never reports that it removed something it should not have, so nobody would ever learn the unit was doing it. Under this admission the same situation produces a typed, located, countable refusal naming which state blocked it, so a host stuck behind a conflict is visible instead of quietly clobbered.\n\nThe unlink is therefore a SEPARATE admitted step that runs before the unit start and can refuse independently of it, not a line inside the unit. runner_activation's readiness receipt is the analogue: the expensive thing is not performing the action, it is performing it without the observation that licenses it."
+
+fn unconditional_unlink_sketch(observed: EndpointPathState) -> Bool {
+  match observed {
+    EndpointPathAbsent => true
+    EndpointListening { owner: _ } => true
+    EndpointStaleSocket { detail: _ } => true
+    EndpointPathConflict { detail: _ } => true
+    EndpointPathObservationUnavailable { reason: _ } => true
+  }
+}
+
+data unconditional_unlink_sketch_note: String = "THE RED CONTROL, KEPT LIVE RATHER THAN DESCRIBED. This is ExecStartPre=rm -f written as a predicate: it answers 'unlink?' with true in all five path states, because that is precisely what the shell line does. It exists so the witnesses can assert the DIFFERENCE between it and admit_stale_socket_unlink on the two states where the difference is destructive — EndpointListening and EndpointPathConflict — rather than asserting the admission's behaviour alone. An assertion that the admission refuses proves nothing about whether the refusal was needed; the contrast is what makes the wall discriminating. It is never called by production code and it is not a scaffold to dissolve: per DESIGN section 4b, a class's discriminating control stays enrolled as the executing evidence that the higher rung stays real."
+
+fn admission_yields_unlink(admission: StaleSocketUnlinkAdmission) -> Bool {
+  match stale_socket_unlink_command(admission: admission) {
+    StaleSocketUnlinkCommandReady { command: _ } => true
+    StaleSocketUnlinkCommandRefused { reason: _ } => false
+  }
+}