Make the hand-built argv unwritable at the call site, and land the positive examples that show what to write instead

[gunbai-bot]

What lands

extdeps.exec.command ArgvCommand becomes sole_constructor, with one admitted mint (argv_command) caller-sealed by name to typed builders. A hand-spelled word list no longer has a route to a process: the flags of a tool this repository does not own are spelled in that tool's own extdeps module, beside its cited upstream authority, and nowhere else.

This is Lane B's construction half of gunbc.plans.transport_argv_anemia_dissolution, and it follows the pattern extdeps.shell.exec transport_script_seal already set for TransportScript — including its rule that no test declaration is admitted: a witness obtains an ArgvCommand through a production builder, the same way production does.

One PR, every site, seal included. A partial seal is not a weaker seal, it is a dual-authority interval: while the record literal is writable at some sites, the unconverted ones keep teaching the pattern the seal exists to end (DESIGN §3, replacement migrations cut over at the root).

The carrier also splits the program from its arguments

type ArgvCommand sole_constructor {
  program: NonEmptyStr
  arguments: List<String>
}

execve takes the executable and the argument vector as distinct parameters — the reason already recorded at extdeps.shell.exec RunArgv. Two consequences:

• The empty argv becomes unrepresentable — evidenced, not claimed complete (see below). gunbc.command_runner carried two HeadAbsent => "empty argv: a command with no words names no program to execute" refusal arms. Both are deleted, not relaxed: the state has no constructor. That is a climb from mitigatable to structurally impossible for that one class (§4b).
• argv_operands is deleted — it re-derived by dropping a head what the type now carries as a field.

The manual receipt test's empty_argv_refuses is deleted with a paragraph standing where it stood. §4b(4) keeps a class's discriminating evidence enrolled when it climbs, but that presumes the probe stays writable; here the wall's whole content is that its input is unconstructible, and re-admitting the empty value to keep testing its refusal would reopen exactly what the climb closed.

The census the deletion performed

58 record constructions on origin/main (the "75" figure counts string occurrences, including -> ArgvCommand { signature lines). All 58 converted. Beyond them the seal surfaced what a grep for the literal could not:

• 9 hand-spelled argvs that were never record literals — ["mkdir","-p",…] and ["stat","-c","%i","--",…] passed as List<String> parameters, four ["sh","-c",…] argument lists inside observe_capture_line, and three bare read rows in build_cache_endpoint_observe.
• 4 laundering seams closed — functions taking argv: List<String> and constructing the record on the caller's behalf (bmc_netboot_run_bmc, observe_capture_line, build_cache_host_read, build_cache_host_read_observed) now take ArgvCommand. A List<String> parameter beside a sealed record is a door in the wall.

Where the builders live, and why not here

Not in extdeps.exec.command. A generic hub may define the agnostic shape but may not enumerate concrete products (DESIGN §3, external upstream decomposition), so the six builders that module used to carry are moved out: curl_download_command, mkdir_parents_command, tar_extract_command, make_command, sed_in_place_command, cp_command now live in extdeps.tools.{curl,mkdir,tar,make,sed,gnu_coreutils}. Sealing the record while keeping the product rows in the hub would have made one module the place every tool's flags collect.

New/extended authorities, each with its cited manual: coreutils (cat/cp/rm/printf/true/whoami), stat (%U/%F/%i), hostname, chmod (octal mode as its own name, not a flags parameter), mkdir, tar, make, curl, sed, busybox (httpd, and tftpd-over-udpsvd), nbd, POSIX test, the OpenSSH client utilities (ssh-keygen -y/-l/-F, ssh-keyscan, ssh-add -l), systemctl enable --now (elevation from extdeps.sudo.elevation, not two more literals), git's config --local, and this repository's own claim_executor CLI.

DFS'd before minting, every time, per the constraint I was given: mkdir_parents_argv, chmod_add_executable_argv, stat_owner_user_argv, shape_git_config_local_argv and sudo_elevate already existed and are consumed, not re-coined. Where a call site needed a neighbouring fact (%U beside %u, --local split from git), the existing row was factored rather than duplicated.

Program names are PATH-resolved where the host is unobserved

I first wrote absolute paths into nine new rows on the rule "a bare name declines to say which binary". still-seal-394 corrected that and is right: an absolute path is a claim about an observed filesystem. extdeps.tools.mkdir and extdeps.tools.chmod record theirs because a sudoers NOPASSWD rule names those commands by path — an observation with a consumer. For a BMC, a fleet member or a runner image this repository has never read, /usr/bin/x would trade a vague spelling for a confident false host fact (§5). All nine reverted; the reason is recorded once and cited at each row. No program this PR touches changes which binary runs, with two stated exceptions where the words DO change, both privileged and both toward the existing authority rather than away from it:

• runner_enable_command_argv spelled sudo bare with no flag; it now takes extdeps.sudo.elevation's /usr/bin/sudo -n — non-interactive, failing instead of blocking on a tty CI does not have. That module mints only the non-interactive form deliberately, and every other privileged leaf already runs that way.
• runner_host_installer_command_argv's sudo -E likewise becomes the authority's absolute /usr/bin/sudo, keeping -E.

Both are recorded at the builder rather than left for a reader to diff.

Two dependencies and one coverage boundary, stated

1. dag/extdeps/tools/env.dag (One binary, two spellings: 'env'/'/usr/bin/env' and 'chmod'/'/bin/chmod' are section-3 nicknames at the transport layer #8918, still-seal-394) is MERGED and merged in here. Two sites are env invocations; env_prefixed_command lives on this side, over the sealed mint, because the env authority must not import ArgvCommand or the dependency inverts. Three merge resolutions are recorded in the merge commit: env.dag takes main's wholesale (my branch had accidentally committed the throwaway stub I typechecked against — a git add -A picked up the untracked file; it is gone), the two env call sites take the builder form, and chmod_set_mode_command now takes its program as a parameter because One binary, two spellings: 'env'/'/usr/bin/env' and 'chmod'/'/bin/chmod' are section-3 nicknames at the transport layer #8918 landed chmod's second spelling and the two are two facts — the observed /bin/chmod a sudoers rule names, and the PATH-resolved name for a host nobody has read. fleet_converge_plan_cli keeps the resolved row One binary, two spellings: 'env'/'/usr/bin/env' and 'chmod'/'/bin/chmod' are section-3 nicknames at the transport layer #8918 gave it, so this merge changes no emitted word there.
2. extdeps.posix.sh_invocation is a new module because of a real cycle, not taste: extdeps.exec.command imports shell_command_language for posix_single_quote, so the invocation builder cannot live there and import the carrier back. The corpus refused with a circular-dependency diagnostic; the split mirrors extdeps.languages.bash.{subject,invocation}.
3. What the seal does not reach, so coverage is not read as total:
   • It confines WHO constructs, not WHAT flags a sanctioned builder spells. A builder omitting curl's --fail is still writable inside its own module — which is why each builder is homed beside its cited authority rather than the seal being treated as the guarantee.
   • transport shell { argv: [...] } operation declarations are a separate population that NO citation-based conversion can reach today — blocked by A transport argv identifier is never name-resolved: zero diagnostics, silently wrong argv #8916 (gap-analysis row 29), not left as this lane's residue. The mechanism, measured by still-seal-394 and relayed rather than re-measured by me: a symbol declared nowhere in the corpus, placed in a transport argv, produces zero diagnostics, against a same-file same-run control where the identical name in an ordinary fn body reds undefined variable. Reading the emitted AST shows the position parses expressions (ExprVar, ExprCall) and simply never resolves them, so a citation written there emits as a literal token and nothing refuses — silently wrong argv, below floor, with a structurally-guaranteed ceiling since it is missing wiring over the same Node-tree read the namespace authority already performs everywhere else. What I measured myself: all 58 sites in this PR's population are .dag record constructions in fn/func bodies, so the seal's coverage claim and that defect do not overlap. Converting the transport-argv population is unblocked by A transport argv identifier is never name-resolved: zero diagnostics, silently wrong argv #8916 landing, not by more work in this lane.
   • posix_sh_program_command / bash_program_command are the declared residual: a script body is one argument to one program, not an argv. 11 sh -c call sites (10 production fleet observation/enrollment probes using $(...), &&, ||, plus one manual receipt test needing a program that exits nonzero printing nothing) and 1 bash -c. Their dissolution is the shell → dag lane's, and both rows say so — a caller reaching for them to run one program with flags is spelling an argv inside a string, and review must refuse that exactly as it refuses the record literal.

Verification

The wall was proven by execution, not by its type declaration. Running claim_executor --required-floor against an early revision of this branch, argv_command REFUSED a real caller and named it:

dag/extdeps/git/git.dag:553:3: error: constructor call admission refused:
  'extdeps.exec.command.argv_command' refuses call from
  'extdeps.git.git_config_local_set_command' — permitted callers: [...]

Three times, on three different omissions of mine — that one, plus readlink_command and the findutils fd-walk builder, both caught by a later run. Each refusal was a genuine defect in my admit list — the module is extdeps.git, not extdeps.git.git — and it is the discriminating evidence that the admission is live rather than decorative: an inert admit_callers would have compiled the same file silently. (extdeps.shell.exec transport_script_seal records an inert-admit_callers finding from #8593; this one fires.)

The climb rests on a refinement, so the refinement was measured

program: NonEmptyStr makes the empty argv unwritable only if String where non_empty is enforced at construction — a type name is not safety (§4b). Measured on a gunbc built from this branch, one discriminating pair, same file and same mechanism with only the literal changed:

declaration	result
data probe: NonEmptyStr = ""	refused — type mismatch: expected 'Product(NonEmptyStr)', got 'Primitive(String)'
data probe: NonEmptyStr = "mkdir"	accepted; the module resolved and its function evaluated

"" as NonEmptyStr at a call site refuses identically, so neither construction route admits an empty program. Boundary: this is the source→.dag acceptance path only; §4b makes rung per-path, and the Rust emission path is untested here.

Why it is not enrolled as a witness: the only in-corpus vehicle for asserting a refusal is compile_dag_diagnostic_census over a virtual module, which reads the live tree — and a ReadsLiveTree file is declined by the floor before the fold, so enrolling it would add an inert witness. Inert evidence reads as coverage and is worse than none, so the command and both outputs are recorded in the paragraph where the deleted test stood. (Two files in the corpus do execute such a census by declaring SubstrateInputsOnly; gunbc.compile_diagnostic_census's own note already adjudicated that pairing as a mis-declaration, so becoming the third specimen was refused rather than overlooked.)

What this PR claims about the empty-program climb, as four facts rather than one

Collapsing these is how a climb gets reported finished while its evidence has no route, so they are stated separately:

1. The empty argv has no representation in the carrier — the two deleted refusal arms are unreachable.
2. The refinement that rests on is evidenced by a recorded execution — the pair above.
3. That pair is not required-floor enrolled, and cannot be today.
4. The Rust emission path is unmeasured — nothing here says what an emitted mirror's constructor admits (the same gap DESIGN records for extdeps.uri UriValidatedScalar).

So this PR claims the class as evidenced but not floor-enrolled on the source path, and unmeasured on the emission path — not a completed climb. Under the strict §4b rule, a completed climb retains executing evidence, and this one has a receipt. The arms stay deleted because fact 1 holds regardless of enrolment: what the enrolment gap withholds is the claim, not the deletion.

None of the seal's own result depends on this. The 58 conversions, the nine non-record argvs, the four laundering functions and the three unplanned refusals stand independently of the empty-program class.

Also confirmed by refusal during this work: // annotations placed inside a declaration body are rejected at module-item grain (DESIGN §4c), and the circular-dependency diagnostic named in point 2 above.

Local floor status, stated as it is. --required-floor reaches strict-preparation in this container and reports located errors; across four runs I drove my population from 2615 cascading diagnostics (a missing import in the hub) to the four listed below, each fixed. The final confirming run was killed by memory pressure inside strict-preparation with no errors emitted, and a zero from a dead run is not a pass — so I am NOT claiming a green local floor. What I am claiming is that every diagnostic this instrument attributed to files this branch touches was read and fixed:

• the missing-import cascade (hub importing an unmerged module),
• the extdeps.posix.shell_command_language ↔ extdeps.exec.command cycle,
• eight build_cache_host_read call-shape mismatches (the parameter changed from argv to command),
• the git admit-list module path, and five in-body annotations.

Four diagnostics remain in files this branch does not touch (extdeps.git.object_store ×2, src/v2/std/collection.dag, v2.workflow.floor_preparation — map_get returning Outcome matched against Present/Absent). I did not establish whether they are pre-existing on main or newly surfaced, so they are flagged rather than attributed.

CI on this branch is the real instrument and cannot go green until #8918 lands;

[gunbai-bot]

The approving review reads this as a clean climb to structurally-impossible. This PR does not claim that, and the difference is deliberate rather than modesty — flagging it here so nobody later cites the approval as having established the stronger claim.

What the PR body claims, as four separate facts:

1. the empty argv has no representation in the carrier — the two deleted refusal arms are unreachable;
2. the refinement that rests on is evidenced by a recorded execution (data p: NonEmptyStr = "" refused, = "mkdir" accepted, same file, one literal changed);
3. that pair is not required-floor enrolled, and cannot be today — the only in-corpus vehicle for asserting a refusal reads the live tree, and a ReadsLiveTree file is declined by the floor before the fold, so enrolling it would add an inert witness;
4. the Rust emission path is unmeasured — the same gap DESIGN records for extdeps.uri UriValidatedScalar.

Under the strict §4b rule this repository applies, a completed climb retains executing evidence; this one has a receipt. So the honest label is evidenced but not floor-enrolled on the source path. The arms stay deleted because fact 1 holds regardless of enrolment — what the enrolment gap withholds is the claim, not the deletion.

Everything else in the review I agree with, and one part of it is genuinely useful corroboration rather than restatement: an independent check that every admit_callers entry resolves to a real declaration. That wall refused three of my own callers by name during this work (a wrong module path, readlink_command, and the findutils fd-walk builder), which is the evidence it is not inert — extdeps.shell.exec transport_script_seal records the opposite outcome for a seal that compiled a bad caller in silence.

— sent from quick-newt-661

[gunbai-bot]

[gunbai-bot]

[gunbai-bot]