From 31748c7d633b270973a5b7b6b0a861a581e71f56 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 3 Sep 2026 09:52:50 +0000 Subject: [PATCH 1/2] os.Hostname.Set onto the CLI-invocation substrate: model the invocation, derive the argv (#8467 grain) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The hostnamectl set-hostname vertical's realization was a hand-authored argv row — `transport shell { argv: ["hostnamectl", "set-hostname", "{desired}"] }` — the exact defect the CLI-invocation lane exists to remove: the subcommand and the operand were opaque literals in a transport DSL, so the operation's own flags were hand-typed rather than derived from cited rows. This is the #8467 grain of the shell->dag census's §5.A hostname row: the §5.B grain (call a typed op) landed at #7194; the op's *realization* is what this cut replaces. The shape mirrors the jq vertical exactly: - `hostnamectl_set_hostname_verb` is ONE cited row (freedesktop hostnamectl(1)); every argv derivation reads it, so a differently-spelled subcommand cannot reach argv. - `HostnameSetInvocation { desired }` is what a caller describes — no flag, no argv position. A DnsLabel keeps the operand inside the hostnamectl-safe grammar. - The lowering emits a two-argument surface [set-hostname, desired]: the subcommand as a FixedToken (spelling owned by the lex table), the operand as a BoundToken (spelling carried by the invocation). The executable is the handler's fixed tool name, exactly as jq.Process's transport row spells "jq". - `hostname_set_invocation_process_plan` seals the surface into a sole_constructor plan; `hostname_set_execute_plan` runs it through the new `hostnamectl.Process.Run` handler; `hostname_set_classify_observation` owns the exit contract (0 = applied, nonzero = failed with stderr), so no domain code reads a raw exit code. os.Hostname.Set is deleted with its transport row (the jq precedent: the semantic op with hardwired argv is removed, the invocation layer answers its question). The local leg (`hostname_set_local`) now builds the invocation and executes the sealed plan; the SSH legs' privileged argv (`sudo -n set-hostname `) reads the same cited verb, so the local and remote legs cannot drift. The full-argv projection `hostname_set_argv` is derived (executable + rendered surface) rather than a second authority. Witnesses: a new hermetic lowering witness (hostname_set_invocation_lowering_witness) asserts the exact surface, the full-argv projection, the bound-operand perturbation, and the exit contract; the census and host-identity witnesses are repointed onto the invocation path. The v1 false-refusal rosters and the census ledger note the deletion. Verified locally: build lane clean (regen first_generation_equal=true, generated-artifact 36/36 match), witnesses lane clean (FloorClean, 3515 executed, 0 failed), infer_semantics_witness bin runs clean. --- dag/extdeps/tools/hostname.dag | 190 +++++++++++++++++- dag/gunbc/hostname_set.dag | 44 ++-- ...host_identity_observation_witness_test.dag | 3 +- ...e_set_invocation_lowering_witness_test.dag | 143 +++++++++++++ ...l_dag_census_5a_typed_ops_witness_test.dag | 29 ++- ...-dag-residual-census-and-arc-completion.md | 2 +- src/v1/00_core.dag | 9 +- .../stage0/src/bin/infer_semantics_witness.rs | 10 +- 8 files changed, 388 insertions(+), 42 deletions(-) create mode 100644 dag/test/claim/hostname_set_invocation_lowering_witness_test.dag diff --git a/dag/extdeps/tools/hostname.dag b/dag/extdeps/tools/hostname.dag index 7b7d13f8381..ce34451f1e5 100644 --- a/dag/extdeps/tools/hostname.dag +++ b/dag/extdeps/tools/hostname.dag @@ -1,10 +1,26 @@ module extdeps.tools.hostname -import std.types { String, List, Bool } +import std.types { String, List, Bool, Int, NonEmptyStr } +import std.algebra { Empty } +import v2.std.algebra { fold_list, list_append, list_snoc_item } +import v2.std.collection { Map, empty_map, map_insert } +import v2.std.compilers.cli_surface { + CliArgumentSyntax, + CliSurface, + cli_argument_text, + cli_surface_arguments, + process_argv_expansion, + serialize_cli_arguments +} +import v2.std.compilers.lexing { LexRuleSet, LiteralPattern, ModeledLexRules, TokenRule } +import v2.std.compilers.target_model { BoundToken, FixedToken } +import v2.std.diagnostic { Accepted, Outcome, Rejected, bind_outcome, outcome_accepted } +import v2.std.node { Symbol } import extdeps.external_authority { ExternalAuthority } import extdeps.uri { Uri, Https } import extdeps.exec.command { ArgvCommand, argv_command } import extdeps.dns.domain_name { DnsLabel } +import extdeps.shell.exec { ProcessObservation, process_observation } data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { uri: Uri { @@ -24,10 +40,6 @@ fn hostname_short_read_argv() -> List { ["hostname", "-s"] } -fn hostname_set_argv(desired: DnsLabel) -> List { - ["hostnamectl", "set-hostname", desired as String] -} - service os.Hostname { operation ReadShort { input {} @@ -45,24 +57,180 @@ service os.Hostname { 0 => { value: "localhost", success: true } "hermetic os.Hostname.ReadShort" } } +} + +// --------------------------------------------------------------------------------------------- +// THE HOSTNAMECTL SET-HOSTNAME VERTICAL (CLI-invocation substrate). +// docs/plans/cli-invocation-emission-design.md +// +// `os.Hostname.Set` stood here with a hand-authored argv row: +// transport shell { argv: ["hostnamectl", "set-hostname", "{desired}"] } +// That row is the defect this vertical removes: the subcommand and the operand were opaque +// literals in a transport DSL, so the operation's own realization was a hand-typed flag list -- +// the #8467 grain (op's flags must derive from cited rows). The caller now describes WHAT it +// wants of hostnamectl (a desired label); the subcommand is a cited row and the argv is derived. +// --------------------------------------------------------------------------------------------- + +// THE SUBCOMMAND IS ONE CITED ROW, not a hand-typed literal. The freedesktop hostnamectl(1) +// manual names the set-hostname verb; this row is that name, and every argv derivation reads +// it -- a caller cannot reach argv with a differently-spelled verb. `os.Hostname.Set` IS the +// set-hostname operation, so the verb is the operation's identity and is never a field a caller +// supplies. +data hostnamectl_set_hostname_verb: NonEmptyStr = "set-hostname" as NonEmptyStr + +// THE INVOCATION THE CALLER DESCRIBES. It states the desired label and nothing else: no flag, +// no subcommand, no argv position. A DnsLabel keeps the operand inside the hostnamectl-safe +// grammar (the same bound `deployed_intent_v1` relies on). +type HostnameSetInvocation { desired: DnsLabel } + +// LEVEL ONE of the derivation: the desired label is a BOUND token (its spelling arrives with +// the invocation), the subcommand is a FIXED token (its spelling is the cited row, owned by the +// lex table below). The executable is not a surface token -- the handler fixes it, exactly as +// jq's handler fixes "jq" -- so the surface is [set-hostname, desired], two arguments. +type HostnameSetProcessPlan { + arguments: List + binding_spellings: Map +} - operation Set { - input { desired: DnsLabel } +fn hostname_set_invocation_lower(invocation: HostnameSetInvocation) -> HostnameSetProcessPlan { + HostnameSetProcessPlan { + arguments: [ + CliArgumentSyntax { + fragments: [FixedToken { token_class: ^hostnamectl_set_hostname_subcommand }] + }, + CliArgumentSyntax { + fragments: [BoundToken { token_class: ^hostnamectl_set_hostname_operand, binding: ^hostname_set_desired_text }] + } + ], + binding_spellings: map_insert( + m: empty_map(), + key: ^hostname_set_desired_text, + value: invocation.desired as String + ) + } +} + +// THE LEX TABLE hostnamectl itself authors: one row per token identity, spelling from the cited +// verb row. A caller cannot supply this -- the FixedToken's spelling comes from here, so a +// caller cannot reach argv with a differently-spelled verb through the surface either. +fn hostname_set_cli_lex_rules() -> ModeledLexRules { + ModeledLexRules { + root: LexRuleSet { + rules: [ + TokenRule { + token_class: ^hostnamectl_set_hostname_subcommand, + pattern: LiteralPattern { text: hostnamectl_set_hostname_verb as String } + } + ] + } + } +} + +// THE SEALED PLAN. `sole_constructor` means the only mint is the lowering below: a caller cannot +// hand the handler a surface it authored, so the argv reaching the process is exactly the one +// the row-driven lowering produced. +type HostnameSetAdmittedProcessPlan sole_constructor { surface: CliSurface } + +fn hostname_set_invocation_process_plan(invocation: HostnameSetInvocation) -> Outcome { + let plan = hostname_set_invocation_lower(invocation: invocation) + bind_outcome( + o: serialize_cli_arguments( + arguments: plan.arguments, + lex: hostname_set_cli_lex_rules(), + binding_spellings: plan.binding_spellings + ), + f: fn(surface) { + outcome_accepted(HostnameSetAdmittedProcessPlan { surface: surface }) + } + ) +} + +// The argv-only projection, retained because witnesses assert over it directly. +fn hostname_set_invocation_cli_arguments(invocation: HostnameSetInvocation) -> Outcome { + let plan = hostname_set_invocation_lower(invocation: invocation) + serialize_cli_arguments( + arguments: plan.arguments, + lex: hostname_set_cli_lex_rules(), + binding_spellings: plan.binding_spellings + ) +} + +// THE FULL-ARGV PROJECTION, DERIVED -- kept so a consumer that needs the plain argv vector the +// LOCAL process runs (witnesses) reads the SAME words the handler executes. The executable is +// the handler's fixed tool name (the same literal the hostnamectl.Process.Run transport row +// spells); the subcommand and the operand are the rendered surface, so the verb can never drift +// from the cited row. If the lowering refuses, the projection is empty (fail-closed) rather +// than a fabricated plausible argv. +fn hostname_set_argv(desired: DnsLabel) -> List { + match hostname_set_invocation_cli_arguments(invocation: HostnameSetInvocation { desired: desired }) { + Rejected { diagnostics: _ } => Empty + Accepted { value: surface, diagnostics: _ } => + list_append( + left: ["hostnamectl"], + right: hostname_set_surface_words(surface: surface), + ) + } +} + +fn hostname_set_surface_words(surface: CliSurface) -> List { + fold_list( + xs: cli_surface_arguments(surface: surface), + empty: Empty, + cons: fn(acc, argument) { + list_snoc_item(xs: acc, item: cli_argument_text(argument: argument)) + } + ) +} + +// THE EXECUTION HANDLER. `arguments` arrives already lowered from a sealed plan; the only +// literal is the executable, the same shape as jq.Process's RunWithoutStdin. The argv here is +// NOT a second authority on hostnamectl's flags. +// +// NOT readonly: this executes set-hostname, a host mutation -- the same reason os.Hostname.Set +// carried no readonly marker. The process handler is a realization, not an observation. +service hostnamectl.Process { + operation Run { + input { arguments: ProcessArgvExpansion } output { - success: Bool from "exit_success" + exit_code: Int from "exit_code" + stdout: String from "stdout" stderr: String from "stderr" } - transport shell { argv: ["hostnamectl", "set-hostname", "{desired}"] } + transport shell { argv: ["hostnamectl", arguments] } exit { 0 => Unit - nonzero => String "hostnamectl set-hostname failed" + nonzero => Unit } mock_response { - 0 => { success: true, stderr: "" } "hermetic os.Hostname.Set" + 0 => { exit_code: 0, stdout: "", stderr: "" } "hermetic hostnamectl.Process.Run" } } } +// THE EXIT CONTRACT, ONE ROW. hostnamectl(1) exits 0 when the hostname was set and nonzero +// otherwise; this is the tool's documented contract, not a hand-typed flag. The domain never +// reads a raw exit code -- it consumes HostnameSetOutcome. +type HostnameSetOutcome + = HostnameSetApplied + | HostnameSetFailed { exit_code: Int, stderr: String } + +fn hostname_set_classify_observation(observation: ProcessObservation) -> HostnameSetOutcome { + if observation.exit_code == 0 { + HostnameSetApplied + } else { + HostnameSetFailed { exit_code: observation.exit_code, stderr: observation.stderr } + } +} + +// EXECUTION. The one function a domain module calls to actually run hostnamectl. It takes the +// SEALED plan, so the arguments reaching the process are the ones the row-driven lowering +// produced -- a caller cannot hand it an argv it authored. +fn hostname_set_execute_plan(plan: HostnameSetAdmittedProcessPlan) -> ProcessObservation { + let arguments = process_argv_expansion(surface: plan.surface) + let ran = hostnamectl.Process.Run(arguments: arguments) + process_observation(exit_code: ran.exit_code, stdout: ran.stdout, stderr: ran.stderr) +} + // 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 diff --git a/dag/gunbc/hostname_set.dag b/dag/gunbc/hostname_set.dag index d72ed3fcd0d..34ea43b77da 100644 --- a/dag/gunbc/hostname_set.dag +++ b/dag/gunbc/hostname_set.dag @@ -1,6 +1,7 @@ module gunbc.hostname_set import std.types { String, NonEmptyStr, List, Bool } +import v2.std.diagnostic { Accepted, Rejected } import extdeps.dns.domain_name { DnsLabel } import extdeps.tools.hostname import gunbc.hostname_read { @@ -24,21 +25,16 @@ type HostnameSetCasOutcome | HostnameSetCasBaseMismatch { observed: String, base: DnsLabel } | HostnameSetCasApplyFailed { stderr: String } -fn hostname_set_operation_argv(desired: DnsLabel) -> List { - hostname_set_argv(desired: desired) -} - +// THE PRIVILEGED ARGV, DERIVED. The `sudo -n` wrapper and the ABSOLUTE hostnamectl path are the +// elevation/authority shape a sudoers NOPASSWD rule matches -- they stay here, on the SSH +// realization edge. The VERB is the cited row (hostnamectl_set_hostname_verb), so a hand-typed +// subcommand cannot drift from the one the local leg executes: one verb, one spelling, both +// legs. The desired label is the invocation's operand. fn hostname_set_privileged_operation_argv( hostnamectl_path: NonEmptyStr, desired: DnsLabel, ) -> List { - ["sudo", "-n", hostnamectl_path as String, "set-hostname", desired as String] -} - -fn hostname_set_operation_argv_matches_authority(desired: DnsLabel) -> Bool { - let materialized = hostname_set_operation_argv(desired: desired) - let authority = hostname_set_argv(desired: desired) - join(materialized, " ") == join(authority, " ") + ["sudo", "-n", hostnamectl_path as String, hostnamectl_set_hostname_verb as String, desired as String] } fn hostname_set_privileged_operation_argv_matches_fleet_grant( @@ -54,12 +50,28 @@ fn hostname_set_privileged_operation_argv_matches_fleet_grant( ) } +// THE LOCAL LEG: the caller describes the invocation, the model derives the argv, the handler +// executes it. `os.Hostname.Set`'s hand-authored transport row is deleted with this function's +// migration onto extdeps.tools.hostname's hostname_set_invocation_process_plan -- the argv +// reaching the process is the one the row-driven lowering produced, and the exit contract is +// read by hostname_set_classify_observation, never by a domain-side exit-code comparison. fn hostname_set_local(desired: DnsLabel) -> HostnameSetCasOutcome { - let result = os.Hostname.Set(desired: desired) - if result.success { - HostnameSetCasApplied - } else { - HostnameSetCasApplyFailed { stderr: result.stderr } + match hostname_set_invocation_process_plan(invocation: HostnameSetInvocation { desired: desired }) { + Rejected { diagnostics: _ } => + HostnameSetCasApplyFailed { stderr: "hostname set invocation could not be lowered to a hostnamectl argv" } + Accepted { value: plan, diagnostics: _ } => + hostname_set_cas_from_set_outcome( + outcome: hostname_set_classify_observation( + observation: hostname_set_execute_plan(plan: plan), + ), + ) + } +} + +fn hostname_set_cas_from_set_outcome(outcome: HostnameSetOutcome) -> HostnameSetCasOutcome { + match outcome { + HostnameSetApplied => HostnameSetCasApplied + HostnameSetFailed { exit_code: _, stderr: e } => HostnameSetCasApplyFailed { stderr: e } } } diff --git a/dag/test/claim/host/host_identity_observation_witness_test.dag b/dag/test/claim/host/host_identity_observation_witness_test.dag index 5e18dcadba4..49cb7a98b0d 100644 --- a/dag/test/claim/host/host_identity_observation_witness_test.dag +++ b/dag/test/claim/host/host_identity_observation_witness_test.dag @@ -29,8 +29,7 @@ test fn witness_hostname_read_resolves_typed_cell_not_shell_script() -> Bool { } test fn witness_hostname_set_argv_is_typed_not_concat() -> Bool { - hostname_set_operation_argv_matches_authority(desired: "srv9" as DnsLabel) - && join(hostname_set_operation_argv(desired: "srv9" as DnsLabel), " ") == "hostnamectl set-hostname srv9" + join(hostname_set_argv(desired: "srv9" as DnsLabel), " ") == "hostnamectl set-hostname srv9" } test fn witness_hostname_set_resolves_typed_cell_not_shell_script() -> Bool { diff --git a/dag/test/claim/hostname_set_invocation_lowering_witness_test.dag b/dag/test/claim/hostname_set_invocation_lowering_witness_test.dag new file mode 100644 index 00000000000..90a43addcb9 --- /dev/null +++ b/dag/test/claim/hostname_set_invocation_lowering_witness_test.dag @@ -0,0 +1,143 @@ +module test.claim.hostname_set_invocation_lowering_witness + +import std.algebra { Cons, Empty } +import std.types { Bool, String } +import v2.std.algebra { fold_list, list_snoc_item } +import v2.std.collection { List } +import v2.std.compilers.cli_surface { cli_argument_text, cli_surface_arguments } +import v2.std.diagnostic { Accepted, Rejected } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import extdeps.dns.domain_name { DnsLabel } +import extdeps.shell.exec { process_observation } +import extdeps.tools.hostname { + HostnameSetApplied, + HostnameSetFailed, + HostnameSetInvocation, + hostname_set_argv, + hostname_set_classify_observation, + hostname_set_execute_plan, + hostname_set_invocation_cli_arguments, + hostname_set_invocation_process_plan, + hostnamectl_set_hostname_verb +} + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// THE HOSTNAMECTL SET-HOSTNAME VERTICAL, LOWERED TO ARGV. +// docs/plans/cli-invocation-emission-design.md +// +// The caller describes WHAT it wants of hostnamectl (a desired label); it never names the +// subcommand or an argv position. `set-hostname` is a cited row, and the argv is derived. The +// point of every assertion below is that the caller named no flag. +// +// The surface the model produces is [set-hostname, desired] -- the executable is the handler's +// fixed tool name (hostnamectl.Process.Run's transport row spells it, exactly as jq.Process's +// row spells "jq"). The full argv the local process runs is hostname_set_argv's projection: +// ["hostnamectl", "set-hostname", desired]. + +fn set_invocation(desired: DnsLabel) -> HostnameSetInvocation { + HostnameSetInvocation { desired: desired } +} + +fn surface_words(invocation: HostnameSetInvocation) -> List { + match hostname_set_invocation_cli_arguments(invocation: invocation) { + Accepted { value: surface, diagnostics: _ } => + fold_list( + xs: cli_surface_arguments(surface: surface), + empty: Empty, + cons: fn(acc, a) { list_snoc_item(xs: acc, item: cli_argument_text(argument: a)) } + ) + Rejected { diagnostics: _ } => Empty + } +} + +// THE VERB IS A CITED ROW, READ AS DATA: the argv spelling is the row's spelling. The witness +// reads the row so a rename cannot silently pass every lowering test while the row says +// something else -- the row IS the authority the lowering reads. +test fn set_hostname_verb_is_the_cited_row() -> Bool { + (hostnamectl_set_hostname_verb as String) == "set-hostname" +} + +// The invocation lowers to EXACTLY two surface words: the subcommand and the desired operand. +test fn set_invocation_lowers_to_exact_surface() -> Bool { + match surface_words(invocation: set_invocation(desired: "srv9" as DnsLabel)) { + Empty => false + Cons { head: first, tail: rest } => + match rest { + Empty => false + Cons { head: second, tail: after } => + match after { + Empty => (first == "set-hostname") && (second == "srv9") + Cons { head: _, tail: _ } => false + } + } + } +} + +// The full argv the local process runs is the handler's executable plus the surface -- the same +// words hostnamectl.Process.Run's transport row spells. +test fn set_full_argv_is_executable_plus_surface() -> Bool { + match hostname_set_argv(desired: "srv9" as DnsLabel) { + Empty => false + Cons { head: first, tail: rest } => + match rest { + Empty => false + Cons { head: second, tail: after } => + match after { + Empty => false + Cons { head: third, tail: tail_end } => + match tail_end { + Empty => (first == "hostnamectl") && (second == "set-hostname") && (third == "srv9") + Cons { head: _, tail: _ } => false + } + } + } + } +} + +// PERTURBATION: change the desired label and ONLY the operand changes. This proves the operand +// is a bound token, not a spelling the caller supplies -- the surface keeps its shape. +test fn desired_label_perturbation_changes_only_the_operand() -> Bool { + match surface_words(invocation: set_invocation(desired: "srv2" as DnsLabel)) { + Empty => false + Cons { head: first, tail: rest } => + match rest { + Empty => false + Cons { head: second, tail: after } => + match after { + Empty => (first == "set-hostname") && (second == "srv2") + Cons { head: _, tail: _ } => false + } + } + } +} + +// Hermetic execution: the sealed plan executes against hostnamectl.Process.Run's mock and the +// exit contract reads the result as HostnameSetApplied. The domain never reads an exit code. +test fn set_realizes_hermetically_as_applied() -> Bool { + match hostname_set_invocation_process_plan(invocation: set_invocation(desired: "srv9" as DnsLabel)) { + Rejected { diagnostics: _ } => false + Accepted { value: plan, diagnostics: _ } => + match hostname_set_classify_observation(observation: hostname_set_execute_plan(plan: plan)) { + HostnameSetApplied => true + _ => false + } + } +} + +// THE EXIT CONTRACT: hostnamectl exits 0 when the hostname was set; any nonzero exit is a +// failure carrying the tool's stderr. Two states, never conflated with absence or refusal. +test fn nonzero_exit_is_a_failure_with_stderr() -> Bool { + match hostname_set_classify_observation(observation: process_observation(exit_code: 1, stdout: "", stderr: "Operation failed: not authorized")) { + HostnameSetApplied => false + HostnameSetFailed { exit_code: code, stderr: e } => code == 1 && e == "Operation failed: not authorized" + _ => false + } +} + +test fn zero_exit_is_applied_even_with_verbose_stdout() -> Bool { + match hostname_set_classify_observation(observation: process_observation(exit_code: 0, stdout: " ", stderr: "")) { + HostnameSetApplied => true + _ => false + } +} diff --git a/dag/test/claim/shell_dag_census_5a_typed_ops_witness_test.dag b/dag/test/claim/shell_dag_census_5a_typed_ops_witness_test.dag index 33ea2b9ca60..2bf206d8a5a 100644 --- a/dag/test/claim/shell_dag_census_5a_typed_ops_witness_test.dag +++ b/dag/test/claim/shell_dag_census_5a_typed_ops_witness_test.dag @@ -2,26 +2,43 @@ module test.claim.shell_dag_census_5a_typed_ops_witness import std.types { Bool, List, NonEmptyStr, String } import extdeps.dns.domain_name { DnsLabel } -import extdeps.tools.hostname { hostname_set_argv } +import extdeps.tools.hostname { + HostnameSetApplied, + HostnameSetInvocation, + hostname_set_argv, + hostname_set_classify_observation, + hostname_set_execute_plan, + hostname_set_invocation_process_plan +} import extdeps.systemd.systemctl import extdeps.tools.id +import v2.std.diagnostic { Accepted, Rejected } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // Hermetic witnesses for the shell->dag census §5.A finite new-op list: os.Hostname.Set, // systemd.Systemctl.ListUnits, systemd.Systemctl.Status, extdeps.tools.id (Uid/Gid/Lookup). -// Model-before-implement only (D1) — each op's mock_response proves the typed exit{}/output shape -// realizes hermetically; call-site migration (§5.B) is a separate, later lane. Each op cites its -// upstream authority in its home file's extdeps_external_authority_anchor. +// The hostname-set entry has moved past the §5.A grain: os.Hostname.Set's hand-authored +// transport row is deleted and the invocation-layer path (HostnameSetInvocation -> lowering -> +// hostnamectl.Process.Run) realizes hermetically. The other ops remain model-before-implement +// only (D1) — each op's mock_response proves the typed exit{}/output shape realizes hermetically; +// call-site migration (§5.B) is a separate, later lane. Each op cites its upstream authority in +// its home file's extdeps_external_authority_anchor. test fn witness_hostname_set_argv_is_typed_not_concat() -> Bool { join(hostname_set_argv(desired: "srv9" as DnsLabel), " ") == "hostnamectl set-hostname srv9" } test fn witness_hostname_set_realizes_hermetically() -> Bool { - let r = os.Hostname.Set(desired: "srv9" as DnsLabel) - r.success && r.stderr == "" + match hostname_set_invocation_process_plan(invocation: HostnameSetInvocation { desired: "srv9" as DnsLabel }) { + Rejected { diagnostics: _ } => false + Accepted { value: plan, diagnostics: _ } => + match hostname_set_classify_observation(observation: hostname_set_execute_plan(plan: plan)) { + HostnameSetApplied => true + _ => false + } + } } test fn witness_systemctl_list_units_realizes_hermetically() -> Bool { diff --git a/docs/plans/shell-to-dag-residual-census-and-arc-completion.md b/docs/plans/shell-to-dag-residual-census-and-arc-completion.md index a4f8b980ec3..cec0b906a62 100644 --- a/docs/plans/shell-to-dag-residual-census-and-arc-completion.md +++ b/docs/plans/shell-to-dag-residual-census-and-arc-completion.md @@ -780,7 +780,7 @@ What the trigger does **not** discharge is the **existing** rows: the wall stops | new op | home file | covers verb | consumers | | --- | --- | --- | --- | -| `extdeps.os.hostname` · ~~`Read`~~ **LANDED** + `Set` | `dag/extdeps/os/hostname.dag` (created) | ~~`hostname -s`~~ **done**; `hostnamectl set-hostname` remains | **Read done** — `os.Hostname.ReadShort` realized via typed cell `HostnameReadOnHost` + `gunbc.hostname_read` (LocalShell → op, SshShell → typed argv); both read consumers dissolved: `host_identity_observation` (`HostIdentityShortHostnameRead`, the `host_identity_short_hostname_script` concat DELETED) and `ci_deploy_target_host` (runtime-present read; the GHA preflight *block* stays E-emit). **Set** (`host_effect_hostname` `SetHostnameCas`, its own `host_effect_set_hostname_cas_script` concat) still pending — reuses this op file with a `SetHostname` op. | +| `extdeps.tools.hostname` · ~~`Read`~~ **LANDED** + ~~`Set`~~ **LANDED, then migrated** | `dag/extdeps/tools/hostname.dag` (moved from `dag/extdeps/os/hostname.dag`) | ~~`hostname -s`~~ **done**; ~~`hostnamectl set-hostname`~~ **done** | **Read done** — `os.Hostname.ReadShort` realized via typed cell `HostnameReadOnHost` + `gunbc.hostname_read` (LocalShell → op, SshShell → typed argv); both read consumers dissolved: `host_identity_observation` (`HostIdentityShortHostnameRead`, the `host_identity_short_hostname_script` concat DELETED) and `ci_deploy_target_host` (runtime-present read; the GHA preflight *block* stays E-emit). **Set done at the §5.B grain, then migrated at the #8467 grain** (CLI-invocation lane): `os.Hostname.Set`'s hand-authored `transport shell { argv: ["hostnamectl", "set-hostname", "{desired}"] }` row is **deleted**; the local leg realizes through `extdeps.tools.hostname`'s `HostnameSetInvocation` → `hostname_set_invocation_process_plan` → `hostnamectl.Process.Run` (argv derived from the cited `hostnamectl_set_hostname_verb` row), and the SSH legs' privileged argv reads the same cited verb. | | `systemd.Systemctl.ListUnits` | **add to** `dag/extdeps/os/systemctl.dag` | `systemctl list-units --state=active` | `host_converge_slice1` (was `_enumerate_units_script`; now calls `systemctl_list_units_active_services` at `:287`). *The `fleet_show_effective_read` consumer named here — `fleet_runner_width_count_read_script` — was never migrated: it was superseded and left dead, and is deleted by the 2026-07-26 true-up.* | | `extdeps.os.id` · `Read` (uid/gid/user) | **new** `dag/extdeps/os/id.dag` | `id -u`, `id -g`, `id ` | `host_effect_realize` (ssh probes), `fleet_posix_accounts` (`probe_command`) | | `ssh.Session.ExecArgv` | **add to** `dag/extdeps/diagnostic/ssh.dag` | typed argv over ssh (`ssh host -- argv`) | `host_effect_realize` ssh probes — **IN FLIGHT, C5 #6946** | diff --git a/src/v1/00_core.dag b/src/v1/00_core.dag index 0ec57314f8b..1f685ea4e5f 100644 --- a/src/v1/00_core.dag +++ b/src/v1/00_core.dag @@ -2489,10 +2489,13 @@ fn container_spelling_verdict(name: String) -> ContainerSpellingVerdict { // source index -- and the service path is exactly that: check_service_field_access_node // builds nominal_type_ref(name: "cron.Tab.List"), a LEAF TYPE NODE whose last // segment is a container name and which is not a container. Excluding it by -// authorship rather than by an exception list is what keeps the six known +// authorship rather than by an exception list is what keeps the five known // false-refusals (cron.Tab.List, Filesystem.List, github.Pulls.List, -// tmux.Session.List, os.Hostname.Set, req.Header.Set) out by construction: a -// seventh service operation named after a container needs no edit here. +// tmux.Session.List, req.Header.Set) out by construction: a +// sixth service operation named after a container needs no edit here. +// (os.Hostname.Set left this list with the CLI-invocation migration: the op's +// hand-authored transport row was deleted and the hostnamectl set-hostname +// vertical realizes through hostnamectl.Process.Run.) fn type_node_name_is_authored(node: Node, source_indices: Map) -> Bool { match node.ident_span { Present { value: span } => diff --git a/src/v1/stage0/src/bin/infer_semantics_witness.rs b/src/v1/stage0/src/bin/infer_semantics_witness.rs index c954e6e6cea..b3f7387caeb 100644 --- a/src/v1/stage0/src/bin/infer_semantics_witness.rs +++ b/src/v1/stage0/src/bin/infer_semantics_witness.rs @@ -1733,22 +1733,26 @@ fn type_resolution_verdict_reports_under_resolved_separately_from_refusal() { } } -/// THE SIX KNOWN FALSE-REFUSALS. Each is a service operation whose last segment is +/// THE FIVE KNOWN FALSE-REFUSALS. Each is a service operation whose last segment is /// a container name; `check_service_field_access_node` renders one as a LEAF TYPE /// NODE via `nominal_type_ref`, so each does reach this walk. None is a container, /// so refusing any of them would be wrong, and the fix a refusal asks for — /// declare an arity row — would be the wrong action. /// /// They are excluded by AUTHORSHIP, not by an exception list: a synthesized node -/// carries a `` span that is in no source index. A seventh service +/// carries a `` span that is in no source index. A sixth service /// operation named after a container therefore needs no edit here. +/// +/// (`os.Hostname.Set` left this list with the CLI-invocation migration: the op's +/// hand-authored transport row was deleted and the hostnamectl set-hostname +/// vertical realizes through hostnamectl.Process.Run, whose last segment is not a +/// container name.) fn service_operations_named_after_containers_are_not_refused() { let known_false_refusals = [ "cron.Tab.List", "Filesystem.List", "github.Pulls.List", "tmux.Session.List", - "os.Hostname.Set", "req.Header.Set", ]; for op in known_false_refusals { From 59076bfcec7bfa62de0f61e28f021bb8fe78e964 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 3 Sep 2026 12:47:10 +0000 Subject: [PATCH 2/2] Review fix: hostname_set_argv becomes refusal-carrying instead of widening a lowering refusal to Empty MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Review advisory (PR #10211): the full-argv projection's `Rejected => Empty` arm was a silent widen — a lowering refusal would surface as an empty list a caller could mistake for a real projection, against DESIGN section 5's "a failure arm must refuse, never widen". It was loud-in-practice (the witnesses' `""` join mismatch) but dishonest as a production-module projection. `hostname_set_argv` now returns Outcome>: a lowering refusal is carried as Rejected, and the three witness consumers match the Outcome instead of reading a bare list that has already swallowed the refusal. The jq vertical's own lowering witnesses do the same (their `argv_of` renders Rejected to false), but there the widen lives in the test file; here it was in the production module. --- dag/extdeps/tools/hostname.dag | 27 ++++++++++++------- ...host_identity_observation_witness_test.dag | 6 ++++- ...e_set_invocation_lowering_witness_test.dag | 26 +++++++++++------- ...l_dag_census_5a_typed_ops_witness_test.dag | 6 ++++- 4 files changed, 43 insertions(+), 22 deletions(-) diff --git a/dag/extdeps/tools/hostname.dag b/dag/extdeps/tools/hostname.dag index ce34451f1e5..fef724f9fed 100644 --- a/dag/extdeps/tools/hostname.dag +++ b/dag/extdeps/tools/hostname.dag @@ -159,17 +159,24 @@ fn hostname_set_invocation_cli_arguments(invocation: HostnameSetInvocation) -> O // LOCAL process runs (witnesses) reads the SAME words the handler executes. The executable is // the handler's fixed tool name (the same literal the hostnamectl.Process.Run transport row // spells); the subcommand and the operand are the rendered surface, so the verb can never drift -// from the cited row. If the lowering refuses, the projection is empty (fail-closed) rather -// than a fabricated plausible argv. -fn hostname_set_argv(desired: DnsLabel) -> List { - match hostname_set_invocation_cli_arguments(invocation: HostnameSetInvocation { desired: desired }) { - Rejected { diagnostics: _ } => Empty - Accepted { value: surface, diagnostics: _ } => - list_append( - left: ["hostnamectl"], - right: hostname_set_surface_words(surface: surface), +// from the cited row. +// +// REFUSAL-CARRYING, NOT A WIDEN: a lowering refusal surfaces as Rejected (DESIGN section 5 -- +// a failure arm refuses, it does not widen into an empty argv that a caller could mistake for +// a real projection). Every consumer matches the Outcome; nothing reads a bare list that has +// already swallowed the refusal. +fn hostname_set_argv(desired: DnsLabel) -> Outcome> { + bind_outcome( + o: hostname_set_invocation_cli_arguments(invocation: HostnameSetInvocation { desired: desired }), + f: fn(surface) { + outcome_accepted( + list_append( + left: ["hostnamectl"], + right: hostname_set_surface_words(surface: surface), + ) ) - } + } + ) } fn hostname_set_surface_words(surface: CliSurface) -> List { diff --git a/dag/test/claim/host/host_identity_observation_witness_test.dag b/dag/test/claim/host/host_identity_observation_witness_test.dag index 49cb7a98b0d..f43b4edd8e3 100644 --- a/dag/test/claim/host/host_identity_observation_witness_test.dag +++ b/dag/test/claim/host/host_identity_observation_witness_test.dag @@ -29,7 +29,11 @@ test fn witness_hostname_read_resolves_typed_cell_not_shell_script() -> Bool { } test fn witness_hostname_set_argv_is_typed_not_concat() -> Bool { - join(hostname_set_argv(desired: "srv9" as DnsLabel), " ") == "hostnamectl set-hostname srv9" + match hostname_set_argv(desired: "srv9" as DnsLabel) { + Rejected { diagnostics: _ } => false + Accepted { value: argv, diagnostics: _ } => + join(argv, " ") == "hostnamectl set-hostname srv9" + } } test fn witness_hostname_set_resolves_typed_cell_not_shell_script() -> Bool { diff --git a/dag/test/claim/hostname_set_invocation_lowering_witness_test.dag b/dag/test/claim/hostname_set_invocation_lowering_witness_test.dag index 90a43addcb9..da40a519305 100644 --- a/dag/test/claim/hostname_set_invocation_lowering_witness_test.dag +++ b/dag/test/claim/hostname_set_invocation_lowering_witness_test.dag @@ -75,20 +75,26 @@ test fn set_invocation_lowers_to_exact_surface() -> Bool { } // The full argv the local process runs is the handler's executable plus the surface -- the same -// words hostnamectl.Process.Run's transport row spells. +// words hostnamectl.Process.Run's transport row spells. The projection is refusal-carrying: a +// lowering refusal must surface as Rejected, never as a bare empty list that looks like a real +// projection. test fn set_full_argv_is_executable_plus_surface() -> Bool { match hostname_set_argv(desired: "srv9" as DnsLabel) { - Empty => false - Cons { head: first, tail: rest } => - match rest { + Rejected { diagnostics: _ } => false + Accepted { value: argv, diagnostics: _ } => + match argv { Empty => false - Cons { head: second, tail: after } => - match after { + Cons { head: first, tail: rest } => + match rest { Empty => false - Cons { head: third, tail: tail_end } => - match tail_end { - Empty => (first == "hostnamectl") && (second == "set-hostname") && (third == "srv9") - Cons { head: _, tail: _ } => false + Cons { head: second, tail: after } => + match after { + Empty => false + Cons { head: third, tail: tail_end } => + match tail_end { + Empty => (first == "hostnamectl") && (second == "set-hostname") && (third == "srv9") + Cons { head: _, tail: _ } => false + } } } } diff --git a/dag/test/claim/shell_dag_census_5a_typed_ops_witness_test.dag b/dag/test/claim/shell_dag_census_5a_typed_ops_witness_test.dag index 2bf206d8a5a..c34915c212c 100644 --- a/dag/test/claim/shell_dag_census_5a_typed_ops_witness_test.dag +++ b/dag/test/claim/shell_dag_census_5a_typed_ops_witness_test.dag @@ -27,7 +27,11 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // its home file's extdeps_external_authority_anchor. test fn witness_hostname_set_argv_is_typed_not_concat() -> Bool { - join(hostname_set_argv(desired: "srv9" as DnsLabel), " ") == "hostnamectl set-hostname srv9" + match hostname_set_argv(desired: "srv9" as DnsLabel) { + Rejected { diagnostics: _ } => false + Accepted { value: argv, diagnostics: _ } => + join(argv, " ") == "hostnamectl set-hostname srv9" + } } test fn witness_hostname_set_realizes_hermetically() -> Bool {