Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
22 commits
Select commit Hold shift + click to select a range
69daabe
Make the hand-built argv unwritable: seal ArgvCommand, and land the b…
Aug 22, 2026
09a9c6b
Program spelling is an observation claim: one authority paragraph, on…
Aug 22, 2026
80beb08
Five more hand-spelled argvs the seal surfaced: /proc reads and the f…
Aug 22, 2026
5cf5c0e
Cast the two NonEmptyStr literals at their call sites
Aug 22, 2026
1e3eb3d
Admit two builders the wall caught, and measure the NonEmptyStr refin…
Aug 22, 2026
0015c4f
Count the sh -c residual instead of estimating it: eleven, not six
Aug 22, 2026
1e187f0
The nbd programs do not both run on the BMC: correct the note that sa…
Aug 22, 2026
9452129
State the two privileged word changes at the builder that makes them
Aug 22, 2026
5f28e5a
Name the two concrete products the hub still carries, and why the rul…
Aug 22, 2026
e45c546
The transport-argv population is blocked by a floor defect, not this …
Aug 22, 2026
6702821
State the empty-program climb as four facts, not one claim
Aug 22, 2026
4e076dc
Merge main: extdeps.tools.env (#8918) lands the authority this branch…
Aug 22, 2026
859de9d
The bracket-form regression control follows its builder's rename
Aug 22, 2026
fcd7fe5
Merge main: the census caught a new hand-built argv that landed while…
Aug 22, 2026
5074fe4
Merge remote-tracking branch 'origin/main' into session/quick-newt-661
Aug 23, 2026
a04964d
Merge main: install(1) and this branch's coreutils builders are addit…
Aug 23, 2026
3306f74
One name, two operations: qualify the ten live-deploy references the …
Aug 23, 2026
9aa4d37
Merge remote-tracking branch 'origin/main' into session/quick-newt-661
Aug 23, 2026
7ef4aa3
Merge remote-tracking branch 'origin/main' into session/quick-newt-661
Aug 23, 2026
0876160
Merge main (§4c annotation fix, #8989) and align the one over-indente…
Aug 23, 2026
bf52dfb
Two witnesses caught the spelling migration going both ways, and only…
Aug 23, 2026
6c191fe
Merge remote-tracking branch 'origin/main' into session/quick-newt-661
Aug 23, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
202 changes: 146 additions & 56 deletions dag/extdeps/exec/command.dag

Large diffs are not rendered by default.

21 changes: 20 additions & 1 deletion dag/extdeps/git/git.dag
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ module extdeps.git

import extdeps.external_authority { ExternalAuthority }
import extdeps.uri { Uri, Https }
import extdeps.exec.command { ArgvCommand, argv_command }
import std.measure { Percent, percent }
import std.types { Bool, CommitSha, Email, FilePath, GitRef, Int, List, NonEmptyStr, Seconds, Timestamp }
import v2.std.algebra { length, skip }
Expand Down Expand Up @@ -522,6 +523,8 @@ fn shape_git_add_argv() -> List<String> {
["git", "add"]
}

data git_binary_name: NonEmptyStr = "git"

fn shape_git_commit_no_verify_no_edit_argv() -> List<String> {
["git", "commit", "--no-verify", "--no-edit"]
}
Expand All @@ -530,8 +533,24 @@ fn shape_git_config_argv(key: String, value: String) -> List<String> {
["git", "config", key, value]
}

// THE PROGRAM AND ITS OPERANDS, NAMED SEPARATELY, so the two addressings of one fact derive from
// one row instead of agreeing by coincidence: the actuator wants the whole word list, the hook
// emitter wants a command it can render, and `--local` is spelled once for both.
//
// `git` is deliberately NOT an absolute path here, unlike every other binary row in extdeps. These
// words are emitted into a repository-local hook script that runs in a developer's own checkout,
// where the git that resolves through PATH is the git that clone is being managed by; pinning
// /usr/bin/git would name a different program than the one the developer is running.
fn git_config_local_set_args(key: String, value: String) -> List<String> {
["config", "--local", key, value]
}

fn shape_git_config_local_argv(key: String, value: String) -> List<String> {
["git", "config", "--local", key, value]
append([git_binary_name as String], items: git_config_local_set_args(key: key, value: value))
}

fn git_config_local_set_command(key: String, value: String) -> ArgvCommand {
argv_command(program: git_binary_name, arguments: git_config_local_set_args(key: key, value: value))
}

fn shape_git_config_get_argv(key: String) -> List<String> {
Expand Down
42 changes: 42 additions & 0 deletions dag/extdeps/languages/bash/invocation.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,42 @@
module extdeps.languages.bash.invocation

import std.types { String, NonEmptyStr }
import extdeps.external_authority { ExternalAuthority }
import extdeps.uri { Uri, Https }
import extdeps.exec.command { ArgvCommand, argv_command }

data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
uri: Uri {
scheme: Https
locator: "www.gnu.org/software/bash/manual/bash.html"
}
}

// BASH IS NOT `sh`, AND THE CALLER PICKED IT DELIBERATELY. extdeps.posix.shell_command_language
// posix_sh_program_command runs a program against the POSIX specification; this runs one against GNU
// Bash, whose grammar is a superset. A site using `[[`, arrays, `local`, or process substitution is
// making a Bash-specific request, and silently routing it through /bin/sh -- which on some hosts IS
// bash and on others is dash -- is how a script that works on one host fails on the next. The two
// builders exist separately so that choice is recorded rather than inherited from the host.
//
// The subject this cites is declared at extdeps.languages.bash.subject; this module is one surface
// over it (an invocation shape), not a second Bash.
// PATH-resolved program name, deliberately: this repository has made no filesystem observation of
// the host this command runs on, and an absolute path is a claim about one. The full reasoning, the
// criterion for climbing to an absolute row, and the counter-example that makes the distinction
// load-bearing are recorded once at extdeps.exec.command program_spelling_is_an_observation_claim.
data bash_program_name: NonEmptyStr = "bash"

// Same residual-class standing as the POSIX sibling: the script TEXT is modeling debt owned by the
// shell -> dag lane, and this builder is not a route for spelling a program's argv inside a string.
// One call site at the seal: gunbc.fleet_converge_plan_cli's locked apply script.
fn bash_program_command(script: String) -> ArgvCommand {
argv_command(program: bash_program_name, arguments: ["-c", script])
}

// A SCRIPT FILE IS NOT A SCRIPT STRING. `bash <path>` reads the program from a file, so nothing
// about the text passes through this repository's own quoting at all -- which is why this form has
// no residual-class standing beside the one above: there is no embedded program here, only a path.
fn bash_script_argv(script_path: String) -> List<String> {
[bash_program_name as String, script_path]
}
54 changes: 54 additions & 0 deletions dag/extdeps/posix/sh_invocation.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,54 @@
module extdeps.posix.sh_invocation

import std.types { String, NonEmptyStr }
import extdeps.external_authority { ExternalAuthority }
import extdeps.uri { Uri, Https }
import extdeps.exec.command { ArgvCommand, argv_command }

data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
uri: Uri {
scheme: Https
locator: "pubs.opengroup.org/onlinepubs/9699919799/utilities/sh.html"
}
}

// WHY THIS IS A SEPARATE MODULE FROM extdeps.posix.shell_command_language, AND IT IS A CYCLE, NOT A
// PREFERENCE. The invocation builder was authored inside that module and the corpus refused with a
// circular dependency: extdeps.exec.command imports it for posix_single_quote, so it cannot import
// extdeps.exec.command back for the ArgvCommand carrier. The subject module owns the SPECIFICATION
// (the shell command language, its quoting rules); this module owns one INVOCATION SHAPE over the
// utility that implements it, and depends on the carrier -- exactly the split
// extdeps.languages.bash.invocation has from extdeps.languages.bash.subject, for the same reason.

// THE `sh -c` INVOCATION, AND IT IS THE RESIDUAL CLASS OF THIS SEAL RATHER THAN A HOLE IN IT.
//
// What the ArgvCommand wall makes unwritable is a hand-spelled WORD LIST: the flags of a tool this
// repository does not own, typed at a call site where nothing can check them. That is a different
// class from a shell PROGRAM, which is one argument to one program (`sh`) whose own contract is
// "interpret this text". A builder that took a script and returned an argv is not a place a flag can
// be dropped -- there are no flags to drop -- so sealing the record does not and should not make a
// shell program unwritable. The text itself is modeling debt, and it is the shell -> dag lane's
// debt: gunbc.retained_shell_script and extdeps.shell.exec TransportScript already own the route by
// which a script body becomes a modeled program, and the sites that reach for this builder are the
// ones that have not yet been carried through it.
//
// POPULATION AT THE SEAL, counted rather than estimated: eleven call sites. Ten are production host
// probes in the fleet observation and enrollment path (gunbc.fleet_probe_identity_observe x6,
// gunbc.fleet_host_key_enrollment x4) whose bodies use $(...), && and || -- genuine shell
// composition, not an argv wearing a costume. The eleventh is a manual receipt test that needs a
// program which exits nonzero while printing nothing, and reaches for `sh -c "exit 3"` because no
// utility has that as its contract.
//
// DISSOLVE-ON: those bodies become modeled programs through the shell -> dag route, at which
// point this builder loses its last caller and is deleted with them. It is NOT an escape hatch for a
// new argv: a caller reaching for it to run a single program with flags is spelling that program's
// argv inside a string, which review must refuse exactly as it refuses the record literal.
fn posix_sh_program_command(script: String) -> ArgvCommand {
argv_command(program: posix_sh_program, arguments: ["-c", script])
}

// PATH-resolved program name, deliberately: this repository has made no filesystem observation of
// the host this command runs on, and an absolute path is a claim about one. The full reasoning, the
// criterion for climbing to an absolute row, and the counter-example that makes the distinction
// load-bearing are recorded once at extdeps.exec.command program_spelling_is_an_observation_claim.
data posix_sh_program: NonEmptyStr = "sh"
32 changes: 32 additions & 0 deletions dag/extdeps/posix/test_utility.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
module extdeps.posix.test_utility

import std.types { String, NonEmptyStr }
import extdeps.external_authority { ExternalAuthority }
import extdeps.uri { Uri, Https }
import extdeps.exec.command { ArgvCommand, argv_command }

data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
uri: Uri {
scheme: Https
locator: "pubs.opengroup.org/onlinepubs/9699919799/utilities/test.html"
}
}

// THE STANDALONE UTILITY, NOT THE SHELL BUILTIN, and that is why this module exists at all rather
// than the question being answered by a shell fragment. Every shell also implements `test` as a
// builtin, so a caller that reaches for a shell to ask it pays for a shell parse and inherits that
// shell's own quoting rules. Spawning the utility asks the same question of a real program with a
// real argv, which is exactly what this repository's ArgvCommand carrier is for.
// PATH-resolved program name, deliberately: this repository has made no filesystem observation of
// the host this command runs on, and an absolute path is a claim about one. The full reasoning, the
// criterion for climbing to an absolute row, and the counter-example that makes the distinction
// load-bearing are recorded once at extdeps.exec.command program_spelling_is_an_observation_claim.
data test_program: NonEmptyStr = "test"

// -f IS "EXISTS AND IS A REGULAR FILE", which is a stronger claim than -e ("exists"): a directory, a
// socket or a dangling symlink at that path answers false here and true under -e. The two are not
// interchangeable and this builder commits to the one its callers mean -- a unit file that turned
// out to be a directory is not present, it is broken.
fn test_regular_file_command(path: String) -> ArgvCommand {
argv_command(program: test_program, arguments: ["-f", path])
}
82 changes: 82 additions & 0 deletions dag/extdeps/ssh/openssh_client_commands.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,82 @@
module extdeps.ssh.openssh_client_commands

import std.types { String, NonEmptyStr, Int }
import extdeps.external_authority { ExternalAuthority }
import extdeps.uri { Uri, Https }
import extdeps.exec.command { ArgvCommand, argv_command }

data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
uri: Uri {
scheme: Https
locator: "man.openbsd.org/ssh-keygen.1"
}
}

data ssh_keyscan_external_authority_anchor: ExternalAuthority = ExternalAuthority {
uri: Uri {
scheme: Https
locator: "man.openbsd.org/ssh-keyscan.1"
}
}

data ssh_add_external_authority_anchor: ExternalAuthority = ExternalAuthority {
uri: Uri {
scheme: Https
locator: "man.openbsd.org/ssh-add.1"
}
}

// THE OPENSSH CLIENT UTILITIES THIS REPOSITORY INVOKES AS PROCESSES, one module because they are one
// upstream (the OpenSSH portable distribution ships all three from one release), with a citation per
// utility because they are three separate manual pages making three separate contracts.
//
// These builders were previously hand-spelled at their call sites in gunbc.fleet_host_key_enrollment
// and gunbc.fleet_ssh_credential_verify -- five bare word lists in which the flags of a security
// tool lived beside the code that read its output.
// PATH-resolved program name, deliberately: this repository has made no filesystem observation of
// the host this command runs on, and an absolute path is a claim about one. The full reasoning, the
// criterion for climbing to an absolute row, and the counter-example that makes the distinction
// load-bearing are recorded once at extdeps.exec.command program_spelling_is_an_observation_claim.
data ssh_keygen_program: NonEmptyStr = "ssh-keygen"
data ssh_keyscan_program: NonEmptyStr = "ssh-keyscan"
data ssh_add_program: NonEmptyStr = "ssh-add"

// -y DERIVES the public key from a private key file and prints it. It reads the private half, which
// is why the caller supplying the path is asserting it holds one -- this is not a public-key reader.
fn ssh_keygen_public_key_command(identity_file: String) -> ArgvCommand {
argv_command(program: ssh_keygen_program, arguments: ["-y", "-f", identity_file])
}

// -l prints the FINGERPRINT of the key in the named file, rather than the key. A fingerprint is what
// a human compares and what a receipt records; the key itself is what gets installed. Two different
// products, so two different builders.
fn ssh_keygen_fingerprint_command(key_file: String) -> ArgvCommand {
argv_command(program: ssh_keygen_program, arguments: ["-l", "-f", key_file])
}

// -F SEARCHES a known-hosts file for a host and exits nonzero when it is absent, which is what makes
// it a presence probe rather than a reader. The file is named explicitly (-f) because the point of
// the probe is to ask about a SPECIFIC staged fragment, not about whatever known_hosts the invoking
// user happens to have.
fn ssh_keygen_known_hosts_find_command(host: String, known_hosts_file: String) -> ArgvCommand {
argv_command(program: ssh_keygen_program, arguments: ["-F", host, "-f", known_hosts_file])
}

// THE TIMEOUT IS A PARAMETER AND IS NOT OPTIONAL, because ssh-keyscan's default is to wait, and a
// converge that waits on an unreachable host has turned a refusal into a hang. -t names the key type
// so the scan returns one algorithm's key rather than whatever set the far side advertises -- a
// caller pinning a host key must say which key it is pinning.
fn ssh_keyscan_command(host: String, key_type: String, timeout_seconds: Int) -> ArgvCommand {
argv_command(
program: ssh_keyscan_program,
arguments: ["-T", to_string(timeout_seconds), "-t", key_type, host],
)
}

// -l LISTS the identities the agent currently holds, by fingerprint. It contacts the agent named by
// SSH_AUTH_SOCK in the process environment -- which is an ENVIRONMENT fact and deliberately not an
// argument here: this builder models ssh-add's argv, and how the caller arranges the agent socket is
// the caller's own realization concern.
fn ssh_add_list_identities_command() -> ArgvCommand {
argv_command(program: ssh_add_program, arguments: ["-l"])
}
27 changes: 16 additions & 11 deletions dag/extdeps/storage/nbd.dag
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ import std.decl_ref { decl_ref }
import std.types { NonEmptyStr, String, Int, Bool, List, Port }
import extdeps.external_authority { ExternalAuthority }
import extdeps.uri { Uri, Https }
import extdeps.exec.command { ArgvCommand }
import extdeps.exec.command { ArgvCommand, argv_command }

data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
uri: Uri {
Expand Down Expand Up @@ -54,10 +54,17 @@ fn nbd_server_config_text(export: NbdExport) -> String {
)
}

// PATH-RESOLVED, AND THE TWO PROGRAMS RUN IN DIFFERENT PLACES, which is worth stating because a
// single "the BMC" would be wrong about half of it: nbd-server runs on the host serving the image
// and nbd-client attaches on the BMC (gunbc.bmc_virtual_media renders both to text for an operator).
// This repository has read neither filesystem. An absolute path for either would be a guess whose
// failure mode is a hard spawn error on hardware nobody is watching, so the spelling stays exactly
// what the call sites used before this conversion and the not-knowing stays visible.
data nbd_server_program: NonEmptyStr = "nbd-server"
data nbd_client_program: NonEmptyStr = "nbd-client"

fn nbd_server_command(config_path: NonEmptyStr) -> ArgvCommand {
ArgvCommand {
argv: ["nbd-server", "-C", config_path as String],
}
argv_command(program: nbd_server_program, arguments: ["-C", config_path as String])
}

type NbdClientAttach {
Expand All @@ -68,19 +75,17 @@ type NbdClientAttach {
}

fn nbd_client_attach_command(attach: NbdClientAttach) -> ArgvCommand {
ArgvCommand {
argv: [
"nbd-client",
argv_command(
program: nbd_client_program,
arguments: [
"-N", attach.export_name as String,
attach.server as String,
to_string(attach.port),
attach.device as String,
],
}
)
}

fn nbd_client_disconnect_command(device: NonEmptyStr) -> ArgvCommand {
ArgvCommand {
argv: ["nbd-client", "-d", device as String],
}
argv_command(program: nbd_client_program, arguments: ["-d", device as String])
}
29 changes: 29 additions & 0 deletions dag/extdeps/sudo/elevation.dag
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ import std.types { String, NonEmptyStr, List }
import extdeps.external_authority { ExternalAuthority }
import extdeps.uri { Uri, Https }
import v2.std.algebra { list_append }
import extdeps.exec.command { ArgvCommand, argv_command }

data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
uri: Uri {
Expand All @@ -12,6 +13,15 @@ data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
}
}

// THE ABSOLUTE PATH IS THE CLAIM THIS ONE BINARY MUST MAKE, and callers that previously spelled a
// bare `sudo` now render this row -- a real change in the emitted words, stated here because the
// -E row below states its own delta and this one was left implicit until review 55022 asked.
// extdeps.exec.command program_spelling_is_an_observation_claim is the general authority: an
// absolute path asserts a filesystem someone read, and a bare name declines to. sudo is the case
// where declining is the WORSE claim, because a sudoers rule matches on the absolute path -- a
// PATH-resolved spelling would let the caller's own PATH decide which binary crosses the privilege
// boundary, which is the opposite of what elevation is for. It is also the spelling sudo_elevate
// above already used, so the alternative was two spellings of one binary inside one module.
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.
Expand Down Expand Up @@ -54,3 +64,22 @@ fn sudo_elevate(command: List<String>) -> ElevatedInvocation {
args: list_append(left: [sudo_non_interactive_flag as String], right: command),
}
}

// -E PRESERVES THE INVOKING ENVIRONMENT, and it is a SEPARATE row from sudo_elevate rather than a
// flag on it, because the two make different security claims: the default drops the caller's
// environment, and -E carries it across the privilege boundary. A caller that needs variables set
// before sudo to survive it must say so; a caller that does not must not silently get it.
//
// IT DOES NOT ADD -n, AND THAT IS PRESERVED RATHER THAN CHOSEN. Its one caller
// (gunbc.runner_host_deploy) emits an operator-run installer command that has always been able to
// prompt on a tty. Adding non-interactive refusal here would be a live behaviour change shipped
// inside an argv refactor, which is exactly what this lane refuses to do silently; if that command
// should fail instead of prompting, that is its own change with its own witness.
data sudo_preserve_environment_flag: NonEmptyStr = "-E"

fn sudo_preserve_environment_command(command: List<String>) -> ArgvCommand {
argv_command(
program: sudo_binary_path,
arguments: list_append(left: [sudo_preserve_environment_flag as String], right: command),
)
}
Loading
Loading