Seal srv3's execution surface so no other module can name it

dag/extdeps/posix/identity.dag

@@ -0,0 +1,102 @@
+module extdeps.posix.identity
+
+import std.types { String, Int, Bool }
+import extdeps.external_authority { ExternalAuthority }
+import extdeps.uri { Uri, Https }
+import v2.std.optional { Optional, Present, Absent }
+import v2.std.integer { integer_lexeme_to_int_optional, integer_nat_to_decimal_string }
+import std.algebra { trim }
+
+data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
+  uri: Uri {
+    scheme: Https
+    locator: "pubs.opengroup.org/onlinepubs/9699919799/basedefs/sys_types.h.html"
+  }
+}
+
+// POSIX OWNS THESE TYPES; `id(1)` MERELY PRINTS THEM. extdeps.tools.id is the coreutils tool that
+// reports a uid and a gid, and this module is the standard those values belong to -- a separate
+// upstream with its own governance, per the external-upstream decomposition rule. A uid observed
+// through `id -u` and a uid read from a passwd row are the same concept, and only one of them is
+// about coreutils.
+//
+// uid_t and gid_t are integer types in POSIX. They are modeled as Int here rather than as the
+// decimal text a probe happens to print, which is the whole point of the module: the corpus was
+// carrying `uid + ":" + gid` as a String composed from two raw stdout captures, so an `id` that
+// printed a warning banner, an empty line, or nothing at all still produced a syntactically
+// plausible owner argument for a privileged chown. There was no state in which that could be
+// noticed -- the concatenation always succeeds.
+
+// NOT A SECOND SPELLING OF extdeps.access.posix_effective_principal. That module models the
+// effective principal's NAME as whoami(1) reports it -- an opaque NonEmptyStr, deliberately not a
+// number. These are the numeric ids, which is what chown's owner argument takes and what a name
+// cannot be substituted for. Same subject, two facts POSIX itself keeps apart (getpwnam maps one
+// to the other, and nothing here pretends that mapping is free).
+type PosixUserId { value: Int }
+
+type PosixGroupId { value: Int }
+
+// The owner argument chown(1) takes is a PAIR, and this is the only place its ":" separator is
+// spelled. Composing it at each call site is the same fact written twice.
+type PosixOwnerSpec {
+  user: PosixUserId
+  group: PosixGroupId
+}
+
+// DECODING IS PARTIAL AND SAYS SO. Text that is not a decimal integer yields Absent, so a caller
+// must answer for it; the previous shape made "1000", "" and "id: cannot find name for user ID"
+// equally acceptable owners.
+// EMPTY AND NEGATIVE ARE REFUSED HERE RATHER THAN DELEGATED. Measured, not assumed: a witness
+// asserting that empty text does not decode came back FALSE, because integer_lexeme_to_int_optional
+// answers Present { value: 0 } for "". Zero is uid 0 -- root -- so an `id` that printed nothing
+// would have decoded to the most privileged principal on the host and been chowned to. The
+// predecessor's String concatenation had the same hole from the other direction (an empty capture
+// produced the owner ":1000"); decoding does not remove a fabrication unless the decoder's own
+// empty case is answered.
+//
+// POSIX ids are non-negative, so a negative lexeme is refused for the same reason: it decodes
+// cleanly and means nothing.
+fn posix_id_value_from_text(text: String) -> Optional<Int> {
+  let lexeme = trim(s: text)
+  match lexeme == "" {
+    true => Absent
+    false =>
+      match integer_lexeme_to_int_optional(lexeme: lexeme) {
+        Absent => Absent
+        Present { value: n } =>
+          match n < 0 {
+            true => Absent
+            false => Present { value: n }
+          }
+      }
+  }
+}
+
+fn posix_user_id_from_text(text: String) -> Optional<PosixUserId> {
+  match posix_id_value_from_text(text: text) {
+    Absent => Absent
+    Present { value: n } => Present { value: PosixUserId { value: n } }
+  }
+}
+
+fn posix_group_id_from_text(text: String) -> Optional<PosixGroupId> {
+  match posix_id_value_from_text(text: text) {
+    Absent => Absent
+    Present { value: n } => Present { value: PosixGroupId { value: n } }
+  }
+}
+
+fn posix_user_id_text(user: PosixUserId) -> String {
+  integer_nat_to_decimal_string(value: user.value)
+}
+
+fn posix_group_id_text(group: PosixGroupId) -> String {
+  integer_nat_to_decimal_string(value: group.value)
+}
+
+fn posix_owner_spec_text(spec: PosixOwnerSpec) -> String {
+  concat(
+    posix_user_id_text(user: spec.user),
+    concat(":", posix_group_id_text(group: spec.group)),
+  )
+}

dag/extdeps/posix/path_ownership.dag

@@ -0,0 +1,152 @@
+module extdeps.posix.path_ownership
+
+import std.types { String, Bool }
+import extdeps.external_authority { ExternalAuthority }
+import extdeps.uri { Uri, Https }
+import extdeps.posix.identity { PosixOwnerSpec, posix_owner_spec_text }
+
+data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
+  uri: Uri {
+    scheme: Https
+    locator: "pubs.opengroup.org/onlinepubs/9699919799/functions/chown.html"
+  }
+}
+
+// OWNERSHIP CONVERGENCE, MODELED AS A DECISION RATHER THAN AS A PROCESS EXIT.
+//
+// A successful chown process is not evidence that a path is owned. It is evidence that one
+// invocation of one utility exited zero -- which is a claim about the utility, not about the
+// filesystem. The two come apart in ordinary ways: a chown that silently followed a symlink
+// changed something else, a chown on a path that a concurrent process replaced changed the old
+// inode, and a chown under a sudoers rule that permits the binary but not the target can exit zero
+// having done nothing on some configurations. Treating exit status as convergence is the
+// fabricated-plausible-output failure at the actuation boundary.
+//
+// So the ensure is: observe, decide, mutate only if needed, observe again independently, and let
+// the SECOND observation decide the verdict. The mutation's own exit status is not consulted for
+// the verdict at all -- it can only cause the readback to disagree.
+
+type PathOwnershipIntent {
+  path: String
+  owner: PosixOwnerSpec
+}
+
+// AN UNOBSERVED OWNER IS NOT AN UNOWNED PATH. `stat` refusing and `stat` reporting a different
+// owner are different states with opposite actuations: the first must not chown at all (the host
+// was never asked), the second must. Collapsing them is the empty-observation narrow pointed at a
+// privileged mutation.
+type PathOwnershipObservation
+  = PathOwnerObserved { owner: PosixOwnerSpec }
+  | PathOwnerUnobserved { reason: String }
+
+// THE PRE-MUTATION DECISION. Separated from the ensure itself so it is decidable without a host:
+// the whole point of the readback design is that the interesting logic is pure and the effects are
+// three calls at the edges.
+type PathOwnershipDecision
+  = OwnershipAlreadySatisfied { owner: PosixOwnerSpec }
+  | OwnershipMutationRequired { current: PosixOwnerSpec, desired: PosixOwnerSpec }
+  | OwnershipDecisionRefused { reason: String }
+
+// THE MUTATION IS EVIDENCE EVEN THOUGH IT IS NOT AUTHORITY. An earlier revision of this module
+// fused "not authoritative for state" with "not evidence at all": the verdict took only the
+// readback, so what the chown reported was discarded entirely. That is wrong in the other
+// direction -- the attempt establishes whether a mutation was dispatched at all and what the
+// actuator said, which is what an operator needs when the readback also disagrees (side-chat
+// review of #8760).
+//
+// WHAT IT DOES NOT CARRY YET, stated rather than implied: exit code, stdout and stderr. The
+// transport surface these arms are reached through projects a process result to a three-valued
+// predicate before this module sees it, so the cause an operator most wants -- chown's own stderr
+// -- is already gone by here. NEXT-RUNG TRIGGER: a transport read that returns the process result
+// rather than a predicate. Until then this carrier is honest about being coarse instead of
+// pretending the distinction it can draw is the whole one.
+type ChownAttemptObservation
+  = ChownNotDispatched { cause: String }
+  | ChownReportedSuccess
+  | ChownReportedFailure
+
+type PathOwnershipEnsureOutcome
+  = PathAlreadyOwned { owner: PosixOwnerSpec }
+  | PathOwnershipConvergedAfterAttempt {
+      owner: PosixOwnerSpec
+      attempt: ChownAttemptObservation
+    }
+  | PathOwnershipEnsureRefused { reason: String }
+
+fn posix_owner_spec_equal(left: PosixOwnerSpec, right: PosixOwnerSpec) -> Bool {
+  left.user.value == right.user.value && left.group.value == right.group.value
+}
+
+// SKIPPING AN UNNECESSARY CHOWN IS A SAFETY PROPERTY, NOT AN OPTIMIZATION. The mutation requires
+// elevation; not performing it is one fewer privileged invocation on the host, and on the common
+// path -- a converge that has already run -- it is the only invocation the ensure would have made.
+fn path_ownership_decision(
+  desired: PosixOwnerSpec,
+  observed: PathOwnershipObservation,
+) -> PathOwnershipDecision {
+  match observed {
+    PathOwnerUnobserved { reason: why } =>
+      OwnershipDecisionRefused {
+        reason: concat("path ownership: the current owner could not be observed, so no chown is authorized: ", why),
+      }
+    PathOwnerObserved { owner: current } =>
+      match posix_owner_spec_equal(left: current, right: desired) {
+        true => OwnershipAlreadySatisfied { owner: current }
+        false => OwnershipMutationRequired { current: current, desired: desired }
+      }
+  }
+}
+
+// THE STATE COMES FROM THE READBACK AND FROM NOTHING ELSE, and the structure says so: `attempt`
+// reaches the outcome only as a field of the receipt, never as a match subject deciding whether
+// convergence happened. Every arm here dispatches on `readback`. So a caller cannot report
+// convergence from a process result -- not because the value is absent, but because no branch
+// consults it.
+//
+// The refusal on a mismatch names both owners AND what the chown reported. "The chown did not
+// take" and "the chown took, to the wrong owner" are the same shape here and are distinguished by
+// the values, not by an arm -- what matters to the caller is that the path is not owned as
+// intended, and what the actuator said is the cause they will look for next.
+fn path_ownership_verdict(
+  desired: PosixOwnerSpec,
+  attempt: ChownAttemptObservation,
+  readback: PathOwnershipObservation,
+) -> PathOwnershipEnsureOutcome {
+  match readback {
+    PathOwnerUnobserved { reason: why } =>
+      PathOwnershipEnsureRefused {
+        reason: concat(
+          concat("path ownership: the owner could not be read back after the chown ", chown_attempt_text(attempt: attempt)),
+          concat(", so convergence is not established: ", why),
+        ),
+      }
+    PathOwnerObserved { owner: after } =>
+      match posix_owner_spec_equal(left: after, right: desired) {
+        true => PathOwnershipConvergedAfterAttempt { owner: after, attempt: attempt }
+        false =>
+          PathOwnershipEnsureRefused {
+            reason: concat(
+              concat(
+                concat("path ownership: after the chown ", chown_attempt_text(attempt: attempt)),
+                concat(" the path is owned by ", posix_owner_spec_text(spec: after)),
+              ),
+              concat(", not ", posix_owner_spec_text(spec: desired)),
+            ),
+          }
+      }
+  }
+}
+
+// THE OUTCOME IS "CONVERGED AFTER AN ATTEMPT", NOT "THIS CHOWN CHANGED IT", and the difference is
+// the third row of the matrix: a chown that REPORTED FAILURE followed by a readback showing the
+// desired owner establishes that the desired state now exists, and does NOT establish that our
+// mutation produced it. A concurrent actor may have, or the utility may have acted partially
+// before returning nonzero. The old name PathOwnershipChanged asserted the causal claim the
+// evidence does not support.
+fn chown_attempt_text(attempt: ChownAttemptObservation) -> String {
+  match attempt {
+    ChownNotDispatched { cause: why } => concat("was not dispatched (", concat(why, ")"))
+    ChownReportedSuccess => "reported success"
+    ChownReportedFailure => "reported failure"
+  }
+}

dag/extdeps/sudo/elevation.dag

@@ -0,0 +1,56 @@
+module extdeps.sudo.elevation
+
+import std.types { String, NonEmptyStr, List }
+import extdeps.external_authority { ExternalAuthority }
+import extdeps.uri { Uri, Https }
+import v2.std.algebra { list_append }
+
+data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
+  uri: Uri {
+    scheme: Https
+    locator: "www.sudo.ws/docs/man/sudo.man/"
+  }
+}
+
+data sudo_binary_path: NonEmptyStr = "/usr/bin/sudo"
+
+// ELEVATION IS A FACT ABOUT AN INVOCATION, AND IT WAS BEING SPELLED FOUR TIMES AS TWO LITERALS.
+// Every privileged leaf in gunbc.host_effect_realize carried `bin_path: "/usr/bin/sudo"` beside an
+// args list whose first element was a bare "-n", so sudo's own calling convention -- which binary,
+// which flag, in which position -- was duplicated into each caller's argv, and the flag's meaning
+// (never prompt; fail instead of blocking on a tty that CI does not have) survived only as two
+// characters at the head of a list.
+//
+// THERE IS NO MODE PARAMETER, AND THAT IS THE MODEL RATHER THAN AN OMISSION. An earlier draft of
+// this module carried a SudoElevation type with one variant, so every caller passed the same value
+// and no arm ever discriminated -- a type with a single inhabitant that nothing matches on is
+// vocabulary, not information (DESIGN section 2). What it was reaching for is real: interactive
+// sudo must be unreachable here. That is achieved by this module minting only the non-interactive
+// form, which is strictly stronger than a parameter a caller could someday be given another value
+// for. If a second mode is ever genuinely needed, it arrives as a variant WITH a call site that
+// distinguishes it, not as a placeholder waiting for one.
+// A COMMAND THAT HAS BEEN ELEVATED, addressed the way the host effect surface takes it: a binary to
+// execute and the argv tail that follows it.
+type ElevatedInvocation {
+  bin_path: String
+  args: List<String>
+}
+
+// -n: never prompt. sudo fails instead of blocking on a tty, which is what makes a missing
+// NOPASSWD grant a refusal the caller can observe rather than a job that hangs until it is killed.
+data sudo_non_interactive_flag: NonEmptyStr = "-n"
+
+// `command` is the full argv of the program being elevated, binary first -- the same shape that
+// would run unelevated. Elevation is therefore a transformation OF an invocation, not a separate
+// spelling of one, so a caller cannot elevate a command it could not otherwise name.
+// ONE APPEND, NOT A SNOC PER ELEMENT. The fold this replaces walked `command` appending to a
+// growing accumulator, which is quadratic in argv length. DESIGN section 6's bare-minimum-cost rule
+// fixes a proven cost shape regardless of the realized n, precisely because "n is small here" is
+// not time-stable -- this function is the one place every privileged invocation in the repository
+// is assembled, so its n is whatever a future caller's argv turns out to be.
+fn sudo_elevate(command: List<String>) -> ElevatedInvocation {
+  ElevatedInvocation {
+    bin_path: sudo_binary_path as String,
+    args: list_append(left: [sudo_non_interactive_flag as String], right: command),
+  }
+}

dag/extdeps/tools/chmod.dag

@@ -0,0 +1,27 @@
+module extdeps.tools.chmod
+
+import std.types { String, NonEmptyStr, List }
+import extdeps.external_authority { ExternalAuthority }
+import extdeps.uri { Uri, Https }
+
+data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
+  uri: Uri {
+    scheme: Https
+    locator: "pubs.opengroup.org/onlinepubs/9699919799/utilities/chmod.html"
+  }
+}
+
+// The absolute path exists for the same reason it does in extdeps.tools.chown and
+// extdeps.tools.mkdir: a sudoers NOPASSWD rule names a command by path. chmod sits at /bin rather
+// than /usr/bin on the hosts this actuator targets, and that is a fact about those hosts recorded
+// here rather than assumed at a call site.
+data chmod_binary_path: NonEmptyStr = "/bin/chmod"
+
+// THE SYMBOLIC MODE, NOT AN OCTAL LITERAL. `+x` adds the execute bit to whatever permissions the
+// file already carries; an octal mode REPLACES them, so the two are not interchangeable spellings
+// of "make it executable" -- one preserves the other bits and one silently decides them. POSIX
+// specifies both forms; this module offers the one whose meaning is additive, because that is what
+// an ensure means.
+fn chmod_add_executable_argv(path: String) -> List<String> {
+  [chmod_binary_path as String, "+x", path]
+}

dag/extdeps/tools/chown.dag

@@ -0,0 +1,23 @@
+module extdeps.tools.chown
+
+import std.types { String, NonEmptyStr, List }
+import extdeps.external_authority { ExternalAuthority }
+import extdeps.uri { Uri, Https }
+import extdeps.posix.identity { PosixOwnerSpec, posix_owner_spec_text }
+
+data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
+  uri: Uri {
+    scheme: Https
+    locator: "man7.org/linux/man-pages/man1/chown.1.html"
+  }
+}
+
+data chown_binary_path: NonEmptyStr = "/usr/bin/chown"
+
+// THE OWNER ARGUMENT IS A TYPED PAIR, NOT A STRING THE CALLER ASSEMBLED. Callers used to pass an
+// `owner: String` built as uid + ":" + gid at the call site, which put chown's argument grammar in
+// the caller and left every caller free to get it wrong silently. Here the ":" form is produced
+// once, from a PosixOwnerSpec that could only be constructed from decoded ids.
+fn chown_argv(owner: PosixOwnerSpec, path: String) -> List<String> {
+  [chown_binary_path as String, posix_owner_spec_text(spec: owner), path]
+}

dag/extdeps/tools/id.dag

@@ -11,6 +11,12 @@ data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
   }
 }
 
+// THE ABSOLUTE PATH IS LOAD-BEARING, NOT PEDANTRY. The argv rows above name `id` bare and resolve
+// through PATH, which is right for a remote shell. A sudoers NOPASSWD rule matches on the command
+// PATH, so a privileged invocation that names the binary bare is a different subject from the one
+// the grant authorizes -- and gunbc.host_effect_realize needs both spellings for the same tool.
+data id_binary_path: NonEmptyStr = "/usr/bin/id"
+
 fn id_uid_argv() -> List<String> {
   ["id", "-u"]
 }