Model the SSH nested command-string target: argv -> shell -> one RFC 4254 command string by gunbai-bot[bot] · Pull Request #8596 · gunb-ai/gunbc

gunbai-bot · 2026-08-19T22:54:42Z

Summary

Adds gunbc.remote_shell_command: a minimal, fully-decidable shell simple-command grammar (single-quoted words joined by single spaces) whose shell_parse is the structural inverse of emit_remote_shell, reusing bash_single_quote (v2.extdeps.languages.bash) for escaping rather than re-deriving it (DESIGN §2/§3).
Models RemoteExecCommandInterpretation — the RFC 4254 §6.5 (one string-typed command field, no shell mandate) vs. OpenSSH/OpenBMC-Dropbear (deployment fact: both invoke a POSIX-conformant shell) split. Unknown refuses rather than assumes (DESIGN §5 construction-over-validation).
remote_exec_command_string produces the composed command as its own typed NonEmptyStr output — never a suffixed argv appended to an ssh prefix — for a caller to hand to ssh.Session.Exec's command field. Two targets composed, never concatenated.
Does NOT wire into gunbc.typed_argv_exec, extdeps.exec.command's SshExec branch, or ssh.Session.Exec — that composition is a separate step (the SshExec branch is a contested seam).
Carries remote_exec_command_live_confirmation as a declared, unexecuted receipt with a trigger (DESIGN §4b "no untracked stall") — CI has no live BMC, so the remote half is never folded into the hermetic green.

Test plan

13 witnesses in dag/test/claim/remote_shell_command_witness_test.dag, all PASS by remote execution (claim_batch), proving shell_parse(emit_remote_shell(simple_command(argv))) == argv hermetically — including fixtures for a single-quote word, a space word, and a shell-metacharacter word, plus Unknown-interpretation refusal and empty-argv refusal.
Live-SSH confirmation against a real OpenSSH host and an OpenBMC/Dropbear BMC — declared unexecuted, no live BMC in CI.

🤖 Generated with Claude Code

… command_runner bmc_netboot_run_bmc and bmc_netboot_put_path each hand-rolled their own shell.Exec.Run + retained_runtime + shell_exec_via_bash heredoc glue around command_over_transport/scp_command — two independent copies of the same bridge pattern (§2/§3). gunbc.command_runner already carries this exact pattern as a single authority (run_shell_command), with its own declared dissolution obligation for the heredoc bridge, and busybox_bmc_build.dag already consumes it the same way. Route both call sites through it instead of forking a second copy, and fold the local dissolution-trigger prose to describe the surviving debt: the SSH-transport space-joined-argv posture in extdeps.exec.command.command_over_transport, out of scope for this change per the parent session's brief (repairing it needs the nested shell-command target, a separate migration whose receipt cannot execute in CI today). No behavior change: command_over_transport(cmd, LocalExec) is identity, so both refactored call sites render byte-identical commands to before. All 9 existing witnesses (bmc_netboot_serve_witness_test, bmc_netboot_shell_boot_witness_test) pass unchanged via claim_batch. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

…and tree -> one RFC 4254 command string Adds gunbc.remote_shell_command: a minimal, fully-decidable simple-command grammar (single-quoted words joined by single spaces) whose shell_parse is the structural inverse of emit_remote_shell, reusing bash_single_quote for escaping rather than re-deriving it. RemoteExecCommandInterpretation models the RFC 4254 vs OpenSSH/Dropbear protocol-vs-deployment split, refusing Unknown rather than assuming a shell. remote_exec_command_string produces one command string as its own typed output -- never a suffixed argv -- for a caller to hand to ssh.Session.Exec's command field. Not wired into gunbc.typed_argv_exec, extdeps.exec.command's SshExec branch, or ssh.Session.Exec by this change; that composition is separate. 13 witnesses in dag/test/claim/remote_shell_command_witness_test.dag prove shell_parse(emit_remote_shell(simple_command(argv))) == argv hermetically, including single-quote, space, and shell-metacharacter fixtures, plus Unknown-interpretation refusal. The live-SSH half (does the far side agree) is carried as a declared, unexecuted receipt with a trigger -- CI has no live BMC, so it is never folded into the hermetic green. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

…e encoding proof The prior design proved shell_parse(emit_remote_shell(x)) == x, but this module authored both halves -- a self-consistent oracle, green by construction, that would stay green under one shared wrong quoting rule (exactly the failure mode quoting invites). IEEE 1003.1-2017 section 2.2.2 gives a complete correctness proof for the encoding directly: inside single quotes every byte is literal, and a single quote cannot occur within single quotes. So wrapping each word in single quotes and escaping an embedded quote as the four-character quote-backslash-quote-quote sequence is correct for every byte sequence, by that one cited clause -- no parser, no metacharacter table, no word-expansion model required. This is a property of the module's own output (every byte sits inside a single-quote span), checkable without modeling a reader -- construction, not validation. shell_parse and its supporting types are removed: once the correctness argument no longer needs a reader model, a hand-rolled inverse parser is residue with no consumer. Witnesses become exact-string structural checks against the cited encoding rather than round trips, and the fixture set shrinks: single-quote, space, and metacharacter words all collapse to the same trivial or single-escape case under single-quote wrapping. RemoteExecCommandInterpretation's Unknown-refuses vocabulary and the declared-unexecuted live-confirmation receipt are unchanged -- both already carried the right honesty about the external (far-side-shell) assumption, which this change narrows but does not remove. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

gunbai-bot · 2026-08-19T23:11:15Z

Design change, superseding the round-trip-parser approach claude/claude-opus-4-7 reviewed above (now stale).

Parent review found the original correctness proof — shell_parse(emit_remote_shell(argv)) == argv — was a self-consistent oracle: both emit_remote_shell and shell_parse were authored by this module, so the round trip proves only internal agreement, not that either side matches real shell semantics. It would stay green under one shared wrong quoting rule, which is exactly the failure mode quoting invites.

Replaced with a citation-grounded structural proof: IEEE 1003.1-2017 §2.2.2 states that inside single quotes every byte is literal and a single quote cannot occur within single quotes. That one clause is a complete correctness proof for wrap-in-single-quotes-and-escape-embedded-quotes, for every byte sequence — no grammar, no parser, no metacharacter table. shell_quote_word now cites the clause directly. This is a property of the emitter's own output (every byte sits inside a single-quote span), checkable without modeling a reader at all — construction over validation.

shell_parse and its supporting types are removed as residue: once the emitter is restricted to the cited form, there is no remaining consumer for a hand-rolled inverse parser. The witness suite shrank from 13 round-trip tests to 10 exact-string structural checks — three fixtures (quote, space, metacharacter) collapse under single-quote wrapping since it's uniform across all of them.

emit_remote_shell's actual logic did not change (it already only wrapped in single quotes via bash_single_quote); only the correctness argument and test strategy changed. Nothing broke in the general form.

All 10 rewritten witnesses verified PASS by remote execution.

— sent from vivid-bee-590

The encoding was named bash_single_quote and lived in v2.extdeps.languages.bash, but gunbc.remote_shell_command cites IEEE 1003.1-2017 section 2.2.2 (POSIX shell command language) for its correctness -- a fact about POSIX, not about Bash specifically. GNU Bash and this SSH command emitter cited the same clause for the same encoding while the function itself lived under one of the two citing modules, so a bash-specific change to that emitter could silently invalidate a POSIX claim made outside it. posix_single_quote now lives in extdeps.posix.shell_command_language, the citation anchor both call sites already pointed at. bash.dag's token-class dispatch table and its echo-escaping helper (bash_single_quote_spaced) call the imported function directly rather than through a bash-local wrapper -- no re-derivation, one authority. The encoding itself is unchanged (same two-line concat/replace), so this is a pure relocation: verified by executing both consumers' witness suites against the new import -- all 10 remote_shell_command_witness_test witnesses and all 61 bash_command_fold_test witnesses pass, 0 failures. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

gunbai-bot · 2026-08-19T23:42:46Z

Follow-up authority move, addressing a finding from parent review: the claude/claude-opus-4-7 APPROVE above (and my prior comment) describe this module as reusing v2.extdeps.languages.bash.bash_single_quote — that's now stale.

The single-quote encoding was named bash_single_quote and lived in the bash emitter module, but the correctness claim is cited against IEEE 1003.1-2017 §2.2.2 (POSIX shell command language) — a fact about POSIX, not Bash specifically. Two modules (GNU Bash's emitter and this one) were citing the same clause for the same encoding while the function itself lived under only one of the two citing modules; a bash-specific change to that emitter could have silently invalidated a POSIX claim made outside it.

Moved the function to extdeps.posix.shell_command_language as posix_single_quote — the citation anchor both call sites already pointed at. bash.dag's token-class dispatch table and its echo-escaping helper now import and call it directly. The encoding itself is byte-identical (same two-line concat/replace); this is a pure relocation, verified by executing both consumers' witness suites against the new import: all 10 remote_shell_command_witness_test witnesses and all 61 bash_command_fold_test witnesses pass, 0 failures.

— sent from vivid-bee-590

The SshExec arm previously composed ssh_exec_prefix ++ argv as a flat suffix -- wrong in kind, since RFC 4254 carries the remote program as one command string, not a suffixed argv. It now folds the inner ArgvCommand through gunbc.remote_shell_command remote_exec_command_string into that one string (cited to IEEE 1003.1-2017 2.2.2), and refuses on an Unknown RemoteExecCommandInterpretation instead of guessing. command_over_transport now returns a typed CommandOverTransportOutcome, so every consumer (command_runner's run_shell_command / run_shell_command_capture, bmc_netboot_serve's serve-command builder) threads the refusal instead of assuming success. bmc_transport names openbmc_dropbear_interpretation explicitly, since the OpenBMC/Dropbear fleet's interpretation is a determined deployment fact, not Unknown. 17/17 witnesses pass by execution (remote_shell_command_witness_test, bmc_netboot_serve_witness_test). Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

gunbai-bot · 2026-08-20T00:07:54Z

Follow-up on the earlier APPROVE review, which noted the SshExec wiring was deferred to the parent-lane's job: that wiring has now landed on this branch (commit 087b82e). extdeps.exec.command command_over_transport's SshExec branch no longer composes ssh_exec_prefix ++ argv as a flat suffix -- it folds the inner ArgvCommand through remote_exec_command_string into one RFC-4254 command string, and command_over_transport now returns a typed CommandOverTransportOutcome that every consumer (command_runner, bmc_netboot_serve) threads instead of assuming success. bmc_transport names openbmc_dropbear_interpretation explicitly for the OpenBMC/Dropbear fleet.

17/17 witnesses pass by execution (remote_shell_command_witness_test, bmc_netboot_serve_witness_test), including the composition-shape assertions (serve_command_one_shape_two_transports etc.).

CI's required-floor frontend refused: DESIGN §4c annotations parse only as standalone leading `//` blocks attached to module-scope declarations, not inside a declaration body. serve_command_one_shape_two_transports carried its explanatory comment between two && clauses; moved it above the test fn instead. No behavior change -- 17/17 witnesses still pass. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

gunbai-bot · 2026-08-20T00:42:52Z

Looked at both minor observations from review 53898; neither needs a code change here.

a as NonEmptyStr on an empty argv element: confirmed by reading eval_cast/cast_identity_result in v1_interpreter.rs -- a cast to any refinement whose underlying kernel is String (which is NonEmptyStr's kernel) is an unchecked identity cast at runtime; the non_empty predicate is never evaluated on the cast path. This is a corpus-wide, pre-existing ceiling (every "x" as NonEmptyStr site in the tree has the same gap), not something this diff introduces or could locally close without a forked one-site fix for a systemic issue (DESIGN §6: root-cause at the language layer, not a local patch). It's also functionally inert here: posix_single_quote renders an empty-string word as '', which is the correct POSIX encoding for an empty positional argument, so a fabricated-but-empty NonEmptyStr produces correct shell output regardless. Not fixing.

extdeps.exec.command importing gunbc.remote_shell_command: the review itself notes this is allowed under §3 (folders are browsing conventions; the only structural law is acyclicity), and remote_shell_command_scope_note in that module already documents the direction and why. Nothing to add.

— sent from vivid-bee-590

…-remote-shell-command # Conflicts: # dag/gunbc/bmc_netboot_serve.dag

…ain's command_over_transport refusal coproduct TWO SEPARATE THINGS, both landing here because CI surfaced them together. (1) THE §4c REFUSAL, 29 sites across four files. I put per-site rationale where the explanation belongs conceptually -- beside the line it explains -- which is exactly the position the language refuses. Hoisted every block to a consolidated leading annotation on the declaration. WHAT I ACTUALLY GOT WRONG, since I had already hit this twice: I fixed ONE block earlier and reported it as fixed. I repaired the instance the error named instead of the class the RULE names. The sweep this time is the whole branch and then the whole corpus -- both now zero indented `//`. The refusal is correct and I am not routing around it. It is fail-closed at the source boundary, typed, located to the byte, and it stopped the line rather than silently dropping the prose. The corpus already tried the alternative: `//` as an outright parse error made comment SYNTAX unwritable without making commentary unwritable, and prose migrated into `data ...: String` rows where intent is mechanically indistinguishable from program data. (2) THE MERGE, which was NOT a text conflict to pick a side on. main landed the command_over_transport refusal coproduct (Built | Refused, #8596) while this branch replaced the capture return type. Both arms of both functions had to be rebuilt, not chosen: run_shell_command SSH arm: Refused -> exit_failure with the rendered cause run_shell_command_capture SSH arm: Refused -> ProcessRefused, NOT the deleted ShellCaptureResult main still constructed there Taking either side whole would have been wrong in a way that still compiles on one of them: ours drops main's new refusal handling, theirs resurrects a deleted type. So I took ours and re-applied main's additions explicitly -- the imports, command_over_transport_refusal_reason and its note, and both refusal arms. Note the refusal now composes rather than collapsing: an SSH command that cannot even be BUILT is a ProcessRefused with a stated cause, distinct from one that ran and failed. That is the same distinction this branch exists to make, arriving from main's side of the merge. The LocalExec arm is untouched by the merge and still routes through RunArgv. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

…tion — and a check that finds this class The floor refused with `no such function: v2.workflow.required_floor.required_floor_expected_red_roster`. Neither this branch nor main declares it, and yet this branch's `cli_run.rs` calls it -- which is the shape I have now hit three times tonight, so I stopped fixing it and looked for the rest. It was MINE. Commit 5fb26a1 ("Restore the floor's edge to the expected-red roster as a qualified reference") added it, and the eighth integration deleted it by taking main's side on `required_floor.dag`. Main never had the function, so there was nothing on main's side to preserve it; taking main's file whole discarded it, and git has recorded that file settled ever since. The delegating edge is not decoration. `cli_run.rs` evaluates the roster inside the policy module's own frame, and the frame's scope IS that module's closure -- a name `required_floor` does not reference is not in the world the frame was built from. Main reaches `v2.workflow.floor_expected_red.floor_expected_red_roster` directly because main's frame differs; on this branch the edge is what makes the name reachable. SO I WROTE THE CHECK RATHER THAN PROMISING TO BE CAREFUL. `dropcheck.py` compares declaration names between a pre-integration commit and HEAD, keeps those that main also lacks, and reports them -- BY CONTENT, never by git's merge state, which is precisely the record a wholesale take corrupts. Over the eighth integration it found eight candidates. Four are main's own deletions (#8598, #8596, #8527 -- confirmed by finding each name in main's history rather than by assuming), one is main superseding my interim `scalar_shaped_builtin_method_arg_type`, and one is this. Over the ninth integration it reports zero. That is the difference between a rule and a mechanism: I wrote "verify the discarded side by content, not by git status" into my own notes two integrations ago, and then dropped this function anyway.

…llers finding (#8593) * Correct two gates that describe per-PR enforcement in the present tense while not running Measured 2026-08-19: dag/tools carries 12 gate modules and ZERO are referenced by any workflow. .github/workflows/ holds two files, and witnesses.yml's only executing step is claim_executor --required-floor. tools.extdeps_scope_placement_gate calls itself a "server-side per-PR wall" that "refuses any dag/extdeps .dag file added by THIS CHANGE"; tools.prose_row_introduction_gate opens with "THE PER-PR WALL". Neither is standing. DESIGN is already honest about this -- its "Building & checks" section declares the 2026-08-15 floor cut as a bounded rung drop and names the effect gates among what is unguarded until the re-add queue closes. What was never updated is the module-level prose, and that is the copy a session actually opens. A wall described in the present tense is a premise the next plan gets built on. PROSE ONLY. No enforcement is re-added, no gate deleted, no roster touched. Only the description is corrected to match the mechanism, citing DESIGN as the authority rather than restating its contents. tools.rust_stage0_gates was checked and needs no correction: it says per-PR execution is "gated on #6239", which states the wall is blocked rather than asserting it stands. RECORDED WITH IT, because it is what made the gap invisible and it generalises past these files: THE .dag CALL GRAPH IS NOT THE EXECUTION GRAPH. Any claim of the form "this runs in CI" is decided by .github/workflows/ and the fold those workflows invoke, never by who calls whom in .dag. Two sessions independently traced the .dag callers of git.Core.DiffUnified0, both concluded it was on a path CI walks every run, and both were wrong -- agreeing was not a second observation, because both had read the same artifact. The finding is stronger than "these two gates are dormant". In hermetic mode eval_mock_response replays the operation RESULT off the declaration's mock_response and never touches argv, so no argv is CONSTRUCTED in the mode CI runs. No argv defect of any kind is observable there. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Refuse the argv representation ambiguity instead of silently resolving it A free monoid whose elements are Strings satisfies BOTH readings at an argv position: value_as_host_string folds it into one concatenated word (its `Value::Str(s) => out.push_str(&s)` arm), and free_monoid_to_vec splices it into N words. The value records no choice between them, and push_shell_argv_tokens tried the concatenating reader first -- so one declared List<String> produced ONE argv word when it arrived monoid-encoded and N words when it arrived as a native list. Same type, same declaration, opposite arity, decided by a representation the author never selected. This is a state-space conflation, not a missing wall, which is why no branch ordering could have been correct: "one argument whose text is the concatenation" and "N arguments" are different states with different remedies. The position now raises a typed, located diagnostic naming the argv index and both readings. MEASURED SPECIMEN: extdeps.git.git git_diff_range_argv returns [base, head] on its TwoDot arm, spliced into `git diff -U0 <range>`. Monoid-encoded that reaches the process as `mainHEAD`. The failure is not that git errors -- on any pair whose concatenation names a real object it produces a successful diff of the WRONG RANGE, which is fabricated plausible output rather than a crash. DELIBERATELY UNCHANGED: Int-element monoids stay char-decoded (unambiguous under one reading only); native Value::List keeps its N-word expansion; ProcessArgvExpansion stays authoritative; and value_as_host_string itself is untouched -- value_to_host_string wraps it for general use, and narrowing a shared helper to fix one caller is the forked-logic trap this lane exists to remove. The empty monoid keeps its current empty-string reading, called out in-code as a deliberate narrow choice rather than left implicit. EVIDENCE, and the RED is unit-level by necessity rather than convenience: in hermetic mode eval_mock_response replays an operation's RESULT off its declaration and never touches argv, so no argv is CONSTRUCTED in the mode CI runs and there is no execution to assert against. Three assertions build the representations directly. Proven discriminating by disabling the refusal and re-running: native list of two strings -> 2 argv words (holds both ways: control) monoid-encoded, refusal enabled -> refuses monoid-encoded, refusal disabled -> FAILED, argv ["mainHEAD"] codepoint monoid -> 1 word (holds both ways: control) NO FROZEN ROSTER, because the refusal IS the census: whatever breaks was relying on the concatenation, and that is exactly the population worth enumerating. Each will be fixed from first principles -- either a latent instance of this defect, or a site that genuinely wants one word and should say so with an explicit join. No arm restoring the old behaviour will be added for sites that complain. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Open the vocabulary axis of realization_vocabulary_containment; falsify the REST/CLI boundary The argv lane keeps asserting in prose that a Redfish/REST path constructs no process invocation. Prose cannot be contradicted by the tree. This makes it a row that reds. NO SECOND LENS WAS MINTED. v2.lens.realization_vocabulary_containment already answers "does module X reach construction vocabulary from set V". The obstacle was that V was a literal: the importer-path axis was already threaded as a parameter through scan_facts_for_leaks_under, while module_is_target_ast_vocab was welded into the predicate. A second lens for a second V would have been the section 3 duplication this lens exists to detect, so the vocabulary axis was opened instead -- the section 2 horizontal move, one axis rather than N copies. RealizationVocabularySet + module_is_in_vocab + is_vocab_leak_in / scan_facts_for_leaks_in / vocab_leak_count_in / vocab_leak_count_live_in. target_ast_vocabulary() DERIVES from the existing target_ast_vocab_modules and target_ast_vocab_module_prefixes rows rather than replacing them, because gunbc.realization_vocab_confinement_census consumes those rows directly and has live claims against them. THE OLD ENTRY POINTS DELEGATE, they do not keep a parallel copy. Leaving the original fold beside the general one would have been one predicate with two implementations -- the fork this lens detects, one level down. The exempt population is a PARAMETER rather than a global roster read, so "this vocabulary has zero admitted exceptions" is a stated fact instead of an accident of the target-AST roster happening to name no CLI module. TWO SITES LEFT TARGET-AST-ONLY, DELIBERATELY, with the reason in-file: the two projections feeding the grandfathered-roster staleness check, whose roster rows are target-AST debt by construction (RealizationVocabDebtClass has no other inhabitant). A second vocabulary arrives with an empty exempt population and so has no roster to be stale against; parameterizing them now would answer a staleness question about a population that does not exist. Trigger recorded. THE FALSIFIER'S SUBJECT IS NOT AN EMPTY UNIVERSE, which is how a negative claim usually turns vacuous. dag/extdeps/bmc contains a module that legitimately reaches this vocabulary -- openbmc_fan_control, the module this lane routes through jq -- beside redfish.dag, which does not. So the scan discriminates WITHIN the population, and the RED control is live corpus data rather than a planted fixture: withdraw the one admitted edge and the count must become 1. Without that assertion a clean result is indistinguishable from a scan that read nothing, which is the empty-observation narrow. The admitted edge is named at exact (importer_path, vocab_module) grain, so a SECOND jq-reaching module anywhere in the scanned roots reds rather than being absorbed by a pattern broad enough to cover it. EXECUTED: all three witnesses return true, including the discrimination control at exactly 1. The pre-existing lens witnesses (planted_leak, discriminators, roster_soundness) return true unchanged. SCOPE, STATED RATHER THAN IMPLIED: the witness is floor-discovered -- neither long/-homed nor in floor_prepared_subject_exclusions -- and reads the live tree, but only the two named directories. A module outside those roots reaching CLI vocabulary is not seen here, and no green from this file may be read as whole-corpus coverage. That lens's whole-corpus half is enrolled on a cadence that does not currently run, which is a fact about the cadence rather than about this witness. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Widen the CLI-vocabulary falsifier root by root; every clean root carries its own control The boundary was enforced in two directories and prose everywhere else. That was the whole of its limitation, so this widens it -- one root per assertion rather than one widened list, so a failure names the root that broke instead of reporting that something, somewhere, reaches CLI vocabulary. ROOTS ADDED, each landing in a stated state rather than behind one green: dag/extdeps entirely -- one admitted edge (the fan control jq edge, already named) plus the jq definition site on the edge roster. Clean otherwise. src/v2/{std,compiler,lens,workflow} -- ZERO admissions. The compiler substrate constructs no process invocation at all. If any of it ever needs a CLI surface, that is an architectural event and it reds here first. A CLEAN ROOT AND AN UNREAD ROOT BOTH REPORT ZERO, and those are different states -- bottom-as-answer against bottom-as-ignorance. Three controls separate them, because the widened roots have no known edge to withdraw: vocab_scan_fact_count_live asserts each scan acquired real facts, so a zero is a finding rather than a silence. Withdrawing the admission under the WIDE root must still surface the fan control edge at exactly 1. A nonzero fact count proves the extdeps scan read something; it does NOT prove it descended into bmc/ where the only known edge lives, so without this "dag/extdeps is clean" could be clean because the one dirty subtree was never reached. Dropping the definition-edge roster must make the count RISE, which proves that roster admits a real edge rather than naming a path the scan never had a fact for. THE TWO ROSTERS ARE DELIBERATELY DIFFERENT SHAPES. The jq definition site is a PATH prefix because constructing a CLI surface is what that location is for; the fan control admission is an EXACT (importer_path, vocab_module) pair because it is one consumer that happens to need the vocabulary and must not silently become two. EXECUTED: 8 of 8 green, including all four controls. STILL NOT COVERED, stated rather than implied: dag/gunbc carries six modules reaching extdeps.shell.exec (the host-effect and transport layer) and dag/test carries the witnesses that exercise this vocabulary deliberately. Neither is added here. Whether dag/gunbc's shell reach is a realization edge or admitted debt is a policy question about the boundary itself, not a mechanical widening, and it is not this change's to decide. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Close the last roots: the #8535 boundary now reds, stated as infrastructure-vs-consumer THE BOUNDARY, in the form that fails rather than the paragraph: Realization infrastructure may reach transport vocabulary; consumers may not, except by exact named admission. #8535's prose says CLI-backed handlers are one realization cell. This says which modules ARE that cell and refuses the rest by name. dag/gunbc's six extdeps.shell.exec reaches are two different things, split by what the module IS rather than by what it imports: PATH-ROSTERED AS REALIZATION EDGES -- retained_shell_script (defines the counted bridges, calls transport_script_seal), bash_materialized_transport (the only other admit_callers-sealed caller of that seal), host_effect_realize (the realization core, reaching through retained_srvn). Reaching transport vocabulary is what these locations are FOR, which is the same reason jq's definition site is path-rostered. ADMITTED AS EXACT PAIRS -- package_delivery, codex_app_server_press, provider_wire_evidence. Exact, so a SEVENTH consumer reds instead of being absorbed by a prefix broad enough to cover it. THE REASON ON THOSE THREE IS THE FINDING, NOT A JUSTIFICATION. All three reach through retained_foreign, whose declared dissolves_to is the bash emitter -- the destination for foreign executors and pre-runtime bootstrap -- while all three appear to run inside a present gunbc runtime, which would make their real destination typed effects. The roster records a bucket that is probably wrong rather than laundering it, so fixing the bucket takes the admission OFF instead of re-justifying it. That population was reached TWICE INDEPENDENTLY: by a retained_foreign call census and by this import-graph scan, which additionally separated out provider_wire_evidence. Two routes landing on one set is why these are named rather than guessed. dag/test is path-rostered and said so: these are the witnesses that exercise this vocabulary deliberately, including the ones proving the argv refusal itself. A test that could not import the thing it tests would be a test of nothing. Stated as a roster rather than left unscanned, so the exclusion is visible instead of implied by absence. THE GENERAL RULE, written into the file because the next person widening a root will reach for the inherited control and it will pass while proving nothing: RE-ESTABLISH DISCRIMINATION AT THE NEW SCOPE. DO NOT INHERIT IT. A narrow root's RED proves the scan discriminates over THAT root. Widen it and it proves nothing about the new subtrees -- a nonzero fact count shows the scan read something, not that it descended where the dirty modules live. Caught here under a green: dag/extdeps reported clean and would have reported clean had bmc/ never been reached at all. So every root carries, at its own scope, a withdrawal control with an exact expected count and a roster-drop control asserting the count RISES, the latter because an edge roster no fact matches is indistinguishable from a correct one. EXECUTED: 12 of 12 green, six of them controls. The gunbc withdrawal returns exactly 3, which is what establishes the split is real rather than fitted to produce a pass. CONTEXT A READER NEEDS FIRST: only 13 files in the whole corpus reach CLI construction vocabulary. The boundary was substantially intact before anyone described it; this confirms and pins a property the tree mostly has rather than negotiating one into existence. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Model the local process-argv seam; fix the trailing-annotation refusal my own edit introduced TWO THINGS, and the second is a defect I caused and did not catch. 1. shell.Exec.RunArgv -- the local process-argv execution seam. Run is argv ["bash", "-s"] with the script on stdin, so every local ArgvCommand in the corpus renders its argv to quoted TEXT and hands it to a shell that parses it back into an argument vector. The seed does Command::new(&argv[0]) at the far end regardless, so the round trip buys nothing and costs exactly what argv-as-serialization exists to stop: a re-parse where argument boundaries are inferred from text instead of carried. THE PROGRAM IS A SEPARATE INPUT, not the first element of the expansion. execve takes the executable and the argument vector as distinct parameters, and with the program separate as NonEmptyStr an EMPTY argv becomes unconstructible -- the unspawnable empty vector has no representation rather than being refused after the fact. NO success: Bool FIELD. `success` is not an observation, it is a POLICY judgement about one -- jq exits 4 to mean "no output" and 1 to mean "false result", neither of which is failure. A Bool beside stdout makes every caller re-derive that from a field that already discarded the information, and lets a refusal read as empty output. So the wire carries the honest triple and the typed outcome is decoded immediately above it against a caller-declared policy. THAT DECODER IS NOT NEW VOCABULARY. It is the pattern already landed for jq (jq_classify_observation / JqExitPolicy / JqOutcome), so ProcessOutcome and ProcessExitPolicy generalize it and the module records what is owed: jq's types are the specialization, its 4-means-absent rule is the missing third policy variant, and they dissolve into these on the first migrated consumer. Named rather than left to be discovered, and deliberately not done here -- jq's classifier is landed and consumed, so folding it in belongs with the migration that motivates it. Local only, per the standing constraint: no SSH arm. command_over_transport's SshExec prefix-append stays where it is. 2. THE REFUSAL I INTRODUCED. Adding the operation left two block comments trailing at end-of-file with no declaration after them -- in the witness, and in exec.dag, where deleting a `data ... : String` prose row (correctly, per section 4c) orphaned the annotation that had described it. Source annotations attach to a FOLLOWING module item; a trailing block names no subject and the substrate refuses it. Both moved above the declarations they govern, and every .dag this branch touches swept for a trailing `//`. WHY 12 OF 12 GREEN DID NOT CATCH IT, which is the part worth carrying: `gunbc run --function` accepted the file the floor refused. The two paths do not agree on annotation validation, so a per-function green is not evidence that the floor will prepare the same file. My verification loop was reading the weaker path and reporting it as though it were the stronger one. The witness assertions themselves are unaffected and still green, including the new definition-edge roster entry -- which exists because THIS change tripped the falsifier: exec.dag reaching cli_surface is a CLI-vocabulary edge inside dag/extdeps, a root the witness asserts is clean. The module is itself a member of cli_process_vocab_modules, so the reach is vocabulary-internal, on the same footing as jq's module. A roster entry added because a real scan refused is a different thing from one added in anticipation, and the file says so. CI is the verifying consumer for the annotation fix: the refusal reproduces on the floor's preparation path, which is not reachable from any local invocation I could find, so I am not claiming a local green I did not get. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Move seam rationale to module-item grain; annotations are not admitted inside declaration bodies Second refusal from the same root cause, and the constraint is stated in DESIGN section 4c rather than being discovered here: the .dag realization admits only standalone leading // blocks attached to MODULE-SCOPE declarations. Trailing, body, unattached and block-comment forms refuse until separately modeled. I wrote the seam's rationale inside the operation body, which is body grain, so every one of those lines refused. Moved to one consolidated module-scope block above the service declaration -- which is also why the pre-existing operations in this file carry their notes as module-scope rows rather than inline: the language has never admitted the inline form, and I should have read that as the constraint it is instead of as a stylistic accident. Also fixed a comment inside a list literal in the witness. My first sweep counted brace depth and missed it, because a list body is bracket-delimited; the sweep now counts both and the branch is clean under it. NOTHING SEMANTIC CHANGED IN THIS COMMIT. The operation, its inputs, its output shape and the decoder are byte-identical in meaning to the previous commit; only the position of prose moved. Recorded explicitly so the next reader does not have to diff it to find out whether the seam was redesigned under cover of a formatting fix. WHAT THIS COST AND WHY IT RECURRED: I pushed the first annotation fix without local verification, saying CI was the verifying consumer because the refusal is raised on the floor's preparation path and gunbc run --function does not raise it. That was honest but it was also one class at a time -- I fixed the trailing form, pushed, and only then learned the body form refuses too, because CI reports the first failing class and stops being informative about the rest. Reading section 4c's own sentence would have given me both forms at once, and a sweep derived from the RULE rather than from the error message is what I should have run the first time. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * File the finding: admit_callers on a service operation is accepted and inert THE CLASS. admit_callers is the repository's construction wall -- a declaration names who may call it, and anyone else is refused. On a fn it works. On a service operation the same syntax PARSES, RESOLVES CLEAN, and DOES NOTHING. WHY THAT IS WORSE THAN THE WALL BEING ABSENT. An absent wall is visible: you look, find nothing, and know where you stand. This one is invisible while reading as present -- an author seals an operation, a reviewer reads the roster as a boundary, and it admits everyone. It is the inert-lens failure at CONSTRUCTION grain, which is the worst place for it, because a construction refusal is the rung people stop checking behind. Measured evidence that the illusion works: I was one step from reporting "the wall is available" after watching the declaration parse, and the reviewing session says it would have believed me. TWO INDEPENDENT ROUTES, deliberately not two readings of one artifact. BY EXECUTION: admit_callers added to the real shell.Exec.Run naming only gunbc.command_runner, after which the unadmitted gunbc.package_delivery -- which calls Run five times -- resolved byte-identically to the unsealed baseline captured first. BY SOURCE (the other session, independently): enforcement lives at exactly one seed site, gated on an exact-constructor-declaration lookup reading the fn admission list; an operation invocation is not a constructor-declaration lookup, so it never reaches that arm, and no operation-call analogue exists. BLAST RADIUS TODAY: ZERO. No operation in the corpus carries admit_callers -- all 21 occurrences across dag/ and src/v2/ attach to a fn or a sealed type. So this is a LATENT TRAP, not a live hole, and the distinction is stated because the first author to reach for it is the one who gets hurt and will have no reason to doubt it. THE PAIR IS ONE ARTIFACT, which is the point rather than a convenience. The positive control (fn form refuses, green today) and the finding (operation form does not, red today) run through one invocation over sources compiled as DATA via the guarantee probe corpus. Split into two files they would be two observations; together they are a discrimination, and the discrimination is the finding. Without the control, a red could equally mean the mechanism is inert or that this file cannot compile a probe at all -- different states, different remedies. Compiling the sources as data is also what makes the pair possible: a refusal here is a resolve error, so an unadmitted call written directly into this module would take the whole file down with it. EXECUTED: fn form returns true, operation form returns false, same file, same run. ENROLLED AS KNOWN-RED rather than left to fail. A bare red takes the floor down and gets triaged as breakage by someone who does not know why it is there. Per DESIGN 4b it does NOT get deleted when the resolver gains operation-grain enforcement -- it flips to a permanent regression control, because deleting the evidence on the climb recreates specification-without-execution one rung up. The roster's own coherence witness passes with the identity added. RUNG, HONESTLY: not mitigatable but BELOW it, because no mitigation occurs -- nothing refuses, nothing counts, nothing is logged. Attainable ceiling: structurally guaranteed, since the class is decidable and fully modeled and only implementation stands between here and there. NEXT-RUNG TRIGGER: an operation-grain construction refusal exists, verified by a correctly-imported unadmitted caller. The trigger is stated in its VERIFIED form because its first two attempted verifications were inconclusive for reasons unrelated to the seal -- a missing import, then a fixture whose service did not resolve at all. A trigger already mis-measured twice should carry how to measure it. NOT FIXED HERE. The resolver change is substrate work with its own owner and its own review bar; routing around the defect or following it into infer would both be the wrong move from this lane. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Retarget the admission control onto the sealed fixture: 54.9s over a 10s ceiling CI caught a cost defect in my own control, and the floor's summary is what identified it: failed=0, known_red_held=307 (my expected-red enrollment took, 306 -> 307), and completed_over_cost_requirement=1. Nothing was broken; one witness was too expensive. THE ROW: fn_form_admission_refuses_unadmitted_caller took 54940ms against the floor's 10000ms per-witness ceiling and grew RSS by 0.99GB. Its forged source imported extdeps.shell.exec to reach transport_script_seal, so compiling it dragged the whole shell/extdeps closure through the diagnostic census. The operation-form probe beside it cost 516ms for exactly the inverse reason: it imports only std.types. THE FIX is to change the control's SUBJECT, not to raise a ceiling or split the file. test.fixture.sole_constructor_sealed.definer exists precisely to exercise caller admission on a minimal closure -- it is the fixture the corpus already uses for this mechanism -- so the control now forges an unadmitted caller of mint_sealed_local. Same mechanism, same refusal class, two orders of magnitude less work, and it moves the control off a production module it never needed to depend on. DISCRIMINATION RE-VERIFIED AFTER THE CHANGE, not assumed from it: fn form returns true, operation form returns false. A cheaper control that stopped discriminating would be worse than the expensive one. WHAT I COULD NOT MEASURE LOCALLY, said rather than implied: every gunbc run pays a whole-corpus typecheck, so both probes report ~58s wall from this session and the witness-level cost the floor meters is invisible from here. The 54.9s and 516ms figures are the floor's own per-witness numbers, and CI is what will confirm the retarget landed under the ceiling. I am not claiming a local measurement I did not get. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Cut command_runner's local path onto shell.Exec.RunArgv: argv stops round-tripping through a shell THE CHAIN THAT IS NOW GONE from the local arm: render the argv to quoted text, wrap it in a bash heredoc, hand it to a shell, let the shell split it back into an argument vector -- to reach a seed that ends in Command::new(argv[0]).args(argv[1..]) regardless. Every step existed only to undo the step before it. On LocalExec command_over_transport is the IDENTITY, so the render had nothing to transform either. Deleted from that path rather than routed around. MEASURED FIRST, because the assignment's census was stale by construction: 22 live call sites across 5 modules (not 25 across 6), 17 of them run_shell_command_capture. ALL 22 PASS LocalExec -- zero use SshExec -- so the entire live population moves in this cut. The callers are untouched: the change is internal to command_runner and both signatures are preserved. THE ONE ENABLER, and it is the part worth reviewing hardest. ArgvCommand.argv is a runtime List<String>; CliSurface is sole_constructor and its only construction route is through CliArgumentSyntax fragments, which carry declared token classes and bindings. Fragments structurally CANNOT express a word that does not exist until the program runs -- a filesystem path, a hostname. So cli_surface_of_literal_words was added to v2.std.compilers.cli_surface. WHY THAT IS NOT THE AMBIGUITY THE CARRIER EXISTS TO CLOSE: the refused state is a List<String> arriving at an argv position with NO declared role, where "one word whose text is the concatenation" and "N separate words" are both well-formed and the realization must guess. This constructor IS the declaration -- its name says each element is exactly one argv word. It is the same resolution the interpreter refusal I landed earlier tells authors to reach for. The file states what it does not license: an argument whose spelling is known at authoring time belongs in fragments, and reaching for this instead is modeling debt. EMPTY ARGV REFUSES rather than defaulting -- a command with no words names no program, and inventing one is fabricated output. THE SSH ARM IS UNTOUCHED, deliberately. Its prefix-append shape is wrong in kind (RFC 4254 carries one string, so the inner command is a nested serialization target, not a concatenation) and that target belongs to another lane. Two sessions editing one contested branch is worse than either fix. It also carries no traffic through this module today, which is why leaving it cost nothing. THE success FIELD is derived through a NAMED policy -- process_exit_is_admitted(ExitZeroSucceeds) -- rather than a bare exit_code == 0, so the convention this runner applies is something a caller can change rather than a literal to discover. WHAT STILL COLLAPSES, named and not fixed here: "ran and exited nonzero" and "could not be executed at all" both arrive as success: false. Under the old bash hop those were genuinely indistinguishable -- a missing binary became the shell's exit 127, which claims a process ran when it never existed. Going direct removes the shell that fabricated that code, so the distinction is now AVAILABLE at the transport even though ShellCaptureResult cannot express it. Not repaired in this cut because it is not free: 17 call sites read that record and the destination is the ProcessOutcome coproduct one module away, so the repair belongs with the sites it changes. THE DISCRIMINATING RECEIPT, executed wet against a real process: argv ["printf", "%s|", "a b"] direct exec -> one operand "a b" -> stdout "a b|" OBSERVED via a shell -> two operands -> stdout "a|b|" asserted absent All three assertions pass. A green that would still be green with the bash hop restored would prove nothing about what changed, which is why the subject is an argument the two paths DISAGREE about rather than a command that merely succeeds. IT IS WET AND EXCLUDED, for a reason that is structural rather than convenient: hermetic evaluation replays an operation's declared mock_response and never constructs an argv at all, so "the words reached the process unsplit" is not observable hermetically. A hermetic version could only assert the mock, which is specification-without-execution. Excluded exactly as the prior argv receipt is, and the file says so. DIVERGENCE FROM THE RECORDED TRIGGER, stated rather than left for a reader to notice: command_runner_dissolution_trigger names host_effect_apply binding ArgvCommand execution as a typed transport handler. This cut routes command_runner directly at shell.Exec.RunArgv instead. The trigger's second clause -- retire the shell_exec_via_bash glue -- is satisfied for the local arm and NOT for the SSH arm, so the trigger is not yet discharged and I have left it in place rather than claiming it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Restrict the literal-words mint to its two callers; state what CI does not guard; correct the trigger Three review items, all taken. The first is the one that mattered and my semantic defence of it was insufficient. 1. THE MINT IS NOW admit_callers-RESTRICTED. My argument was that a constructor whose name says "each element is one argv word" IS the declaration the refused state lacks, and that stands -- but the declaration was UNBOUNDED. Anyone could make it, about anything, which left the interpreter's argv refusal one import away from being routed around: not defeated, just satisfied by an intent nobody checked was true. Nominal wall, not structural. The admitted population is TWO -- run_shell_command and run_shell_command_capture -- which is what makes the restriction honest rather than aspirational. A third caller is an edit to the list in the declaring module: a counted review event rather than an import written elsewhere. VERIFIED BY EXECUTION, with a discriminating RED rather than by reading the declaration -- which matters more than usual here, because I spent this session proving that this exact mechanism is ACCEPTED AND INERT at operation grain. An unadmitted module calling it is refused: constructor call admission refused: 'v2.std.compilers.cli_surface.cli_surface_of_literal_words' refuses call from 'test.fixture.mint_admit_probe.intruder.unadmitted_mint' — permitted callers: [gunbc.command_runner.run_shell_command, gunbc.command_runner.run_shell_command_capture] Located, names the caller, lists the roster. The admitted callers still work: the wet receipt passes unchanged. This is a fn, which is the grain where the mechanism is verified to fire. The file's note that authoring-time spelling belongs in fragments carries no enforcement, and now says so rather than reading as a wall. 2. WHAT GUARDS THIS CUT, AND WHAT DOES NOT, written where the next author stands. The property "the local path reaches no shell" is established wet and the receipt is FLOOR-EXCLUDED, so CI does not run it and someone reintroducing a render-and-bash hop gets no signal. The exclusion is structural -- hermetic evaluation replays mock_response and never constructs an argv, so a hermetic version could only assert the mock -- but the consequence is a real gap and the module now states it: rung mitigatable, next-rung trigger a wet lane that executes floor-excluded receipts. A green test that nothing runs is exactly the inert evidence DESIGN calls a lie, and the file should not read as enforced. 3. THE TRIGGER NAMED A MODULE THAT WAS NEVER BUILT. Asked whether I had created PARALLEL AUTHORITY rather than whether I matched wording, I measured: there is no host_effect_apply production module (it exists only as a witness test), and host_effect_realize never mentions ArgvCommand. command_runner is the ONLY module that turns an ArgvCommand into a local process. The other ArgvCommand consumers reach shell_command_render, which serializes argv into TEXT for emission (githooks) or for the SSH leg -- a different destination, not a second local-exec route. So this did not diverge from the trigger; it satisfied a better version of one that named a binding nobody wrote, and satisfying it literally would have meant building the second route DESIGN forbids. The row is rewritten to name the condition that actually remains: the SSH arm, which needs the nested command-string target another lane owns, and at which point shell_exec_via_bash and retained_runtime leave this module entirely. Also fixed in passing: my own trigger rewrite wrote a \\U escape into the .dag string instead of the literal character, which made the module unparseable. Caught by resolving the file rather than by reading the diff. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Correct a false premise in the trigger I just rewrote: host_effect_apply exists The conclusion was right and one clause of its evidence was false, which is worse than usual here because it sits in a REPLACEMENT trigger -- the row exists to stop the next author re-deriving the question, and a false premise makes them do it anyway. WHAT I WROTE: no host_effect_apply production module exists, witness test only. WHY I GOT IT WRONG: I searched for a FILE named host_effect_apply*.dag and found only the witness test. It is a FUNCTION. gunbc.host_effect_realize declares host_effect_apply and host_effect_apply_gated and both are production. That is the third scope error of this session in one family -- a limited view read as the population -- and the specific lesson is narrower than the earlier two: searching for a filename does not answer a question about a symbol. WHAT ACTUALLY CARRIES THE ARGUMENT, verified independently rather than taken from the correction: host_effect_realize contains ZERO occurrences of ArgvCommand and does not appear among that type's consumers. So host_effect_apply exists and dispatches effects, but it never reaches an ArgvCommand and is therefore not a second route from an ArgvCommand to a process. command_runner remains the sole one, there is no parallel authority, and satisfying the original trigger literally would still have meant BUILDING the second route rather than finding it. The row now says that, and records the correction in place rather than quietly overwriting it, so a reader who saw the earlier claim learns it was wrong instead of wondering which revision to believe. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Replace ShellCaptureResult with ProcessOutcome across every capture site THE CONFLATION, corrected from how we first described it. I claimed in the previous commit that removing the shell's fabricated 127 made "could not be executed at all" available beside "ran and exited nonzero". I TESTED THAT AND IT IS FALSE: a missing program does not produce a result record at all, it REFUSES the evaluation -- failed to execute 'no_such_binary': No such file or directory (os error 2) -- so spawn failure was already fail-closed one rung above the record, and the RED first proposed for this work would have passed against the old record too. The real conflation is one step over and it was live at EIGHT sites: ran and FAILED, printing nothing -> success=false, stdout="" ran and SUCCEEDED, printing nothing -> success=true, stdout="" Both are stdout == "". Those eight read stdout without consulting success, so a failed probe and an empty result were the same value. THE EIGHT, AND WHAT EACH NOW DOES: fleet_host_key_enrollment.check -- THE WORST ONE. Tested trim(stdout)=="present" with no success check, so a probe that FAILED produced "" != "present" and fell through to the branch that APPLIES. A refusal to read authorized_keys was indistinguishable from the key being absent, and the remedies are opposite. Now: refusal refuses and does not mutate the file. fleet_host_key_enrollment.verify -- did concat("outcome=", trim(stdout)), so a refused verify wrote the literal receipt line "outcome=" into a file someone would later read as fact. Now: outcome=UNKNOWN with the cause. fleet_host_key_enrollment.{user,hostname} -- display only. Routed through process_outcome_receipt_text, which renders the three arms to three DISTINCT strings; a refusal can no longer read as empty. fleet_probe_identity_observe.user -- display only, same route. fleet_probe_identity_observe.{passwd_home,job_home} -- USED AS PATHS, not just printed, so they match the arms directly: "(refused: ...)" is fine to print and catastrophic to open. An unreadable home now skips the probe with a stated not-probed line instead of reading .ssh/authorized_keys off a fabricated root. fleet_converge_plan_cli hostname -s -- SURFACED, NOT CLOSED, and said so in file. A `-> String` function has no way to refuse; the honest repair changes the return type and cascades into converge plan subject identity. It now returns a value that CANNOT be mistaken for a hostname rather than a plausible "", so a plan keyed on it is visibly wrong instead of silently wrong. Rung: mitigatable, with the next-rung trigger named. SITES THAT GENUINELY DO NOT NEED THE DISTINCTION, stated rather than left silent: fleet_converge_plan_cli test -f -- exit status IS the product, no stdout anyone wants. Asks process_outcome_admitted directly. Forcing it through an output-bearing variant would add a field it cannot answer. ssh-keygen -F readback -- same shape, same treatment. fleet_ssh_credential_verify x2 -- decompose into a classifier that consumes all three values TOGETHER, so the correlation was already performed. The match adds exhaustiveness and names ProcessOutputAbsent, previously indistinguishable from a failure with empty stdout. DELETED, not kept beside: type ShellCaptureResult is gone. Its one fabricated construction is gone too -- fleet_host_key_enrollment built a ShellCaptureResult to stand in for a FILESYSTEM write failure, inventing success:false for something that was never a process. The coproduct makes that unwritable. scan_host_key_lines shows why the type fits: `scan.success && trim(stdout) != ""` IS ProcessOutputPresent, so a hand-written correlation became a variant. And ssh-keyscan exiting 0 with no key is now a named outcome rather than being reported as a refusal with an empty cause. DISCRIMINATING RED, executed wet, six of six green: nonzero-exit-printing-nothing must be Refused and zero-exit-printing-nothing must be Absent. Both go red if ShellCaptureResult is restored, because then both are stdout == "". The file also records what is NOT tested and why -- the nonexistent-program case is already distinguishable via transport refusal, so asserting it would prove nothing. Recorded on the carrier: spawn failure is fail-closed at the transport, therefore A CALLER CANNOT PROBE FOR A BINARY'S EXISTENCE BY TRYING TO RUN IT -- the attempt stops the line instead of answering. Presence must be asked of something that exists. That is why a separate presence probe has to exist, and it is why no fourth "not spawned" variant was added: it would be an uninhabited arm every consumer must handle and none can reach. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Site 8: the poison IS persisted, and it defeats the guard — second row Checked rather than argued, and the answer is worse than "it might reach a receipt". fleet_converge_plan_wet WRITES host_short verbatim to fleet_converge_plan_subject_host_path, coerces it to NonEmptyStr as the plan's subject host, and folds it into the member-set fingerprint and the plan content hash. An unobserved hostname is persisted as a receipt that later reads as fact. AND IT DEFEATS THE GUARD BUILT FOR THIS EXACT CASE. fleet_converge_apply_wet re-observes the host and refuses on SubjectHostMismatch when observed != planned. Two consecutive refusals produce the SAME string, so the comparison SUCCEEDS and apply proceeds. The check whose entire purpose is to stop a plan being applied on the wrong host is satisfied by two non-observations agreeing with each other -- the empty-observation narrow relocated to the guard: bottom == bottom read as "same host". Making the marker unique per call would NOT repair it; it converts a false match into a false mismatch, which is a different wrong answer, not an observation. NOT INTRODUCED HERE, stated precisely: the prior code persisted "" and compared "" == "", which passed identically. This migration does not repair the defect -- it makes the persisted evidence legible instead of blank. Filed as a SECOND row rather than folded into the first, because the first row's claim (visibly wrong rather than plausibly empty) says nothing about reachability and this row is entirely about reachability. Both mitigatable; different next-rung triggers. This one's: the subject-host comparison consumes an outcome rather than a String, so unobserved-vs-unobserved is a REFUSAL to compare, not an equality. The block is hoisted to module scope as a leading annotation on the declaration (§4c), not left inside the func body. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Hoist 29 body annotations to module-item grain (§4c), and integrate main's command_over_transport refusal coproduct TWO SEPARATE THINGS, both landing here because CI surfaced them together. (1) THE §4c REFUSAL, 29 sites across four files. I put per-site rationale where the explanation belongs conceptually -- beside the line it explains -- which is exactly the position the language refuses. Hoisted every block to a consolidated leading annotation on the declaration. WHAT I ACTUALLY GOT WRONG, since I had already hit this twice: I fixed ONE block earlier and reported it as fixed. I repaired the instance the error named instead of the class the RULE names. The sweep this time is the whole branch and then the whole corpus -- both now zero indented `//`. The refusal is correct and I am not routing around it. It is fail-closed at the source boundary, typed, located to the byte, and it stopped the line rather than silently dropping the prose. The corpus already tried the alternative: `//` as an outright parse error made comment SYNTAX unwritable without making commentary unwritable, and prose migrated into `data ...: String` rows where intent is mechanically indistinguishable from program data. (2) THE MERGE, which was NOT a text conflict to pick a side on. main landed the command_over_transport refusal coproduct (Built | Refused, #8596) while this branch replaced the capture return type. Both arms of both functions had to be rebuilt, not chosen: run_shell_command SSH arm: Refused -> exit_failure with the rendered cause run_shell_command_capture SSH arm: Refused -> ProcessRefused, NOT the deleted ShellCaptureResult main still constructed there Taking either side whole would have been wrong in a way that still compiles on one of them: ours drops main's new refusal handling, theirs resurrects a deleted type. So I took ours and re-applied main's additions explicitly -- the imports, command_over_transport_refusal_reason and its note, and both refusal arms. Note the refusal now composes rather than collapsing: an SSH command that cannot even be BUILT is a ProcessRefused with a stated cause, distinct from one that ran and failed. That is the same distinction this branch exists to make, arriving from main's side of the merge. The LocalExec arm is untouched by the merge and still routes through RunArgv. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Take main's optional-hostname repair and re-express it on ProcessOutcome; DELETE my two mitigatable rows because they are no longer true MAIN FIXED THE DEFECT WHILE THIS BRANCH WAS OPEN, and it fixed it at the rung this lane named as the trigger rather than at the one I settled for. mine: -> String, returning a marker that cannot be mistaken for a hostname. Legible, still not a refusal. Two rows at mitigatable. main: -> NonEmptyStr?, Absent when the probe did not succeed. Plan AND apply refuse outright on Absent, and the subject comparison routes through fleet_converge_apply_subject_host_matches over two NonEmptyStr values instead of a bare String equality. That closes BOTH rows. Row 1 (the value is visibly wrong rather than plausibly empty) is obsolete because there is no longer a value. Row 2 (the poison is persisted, and two non-observations comparing equal DEFEAT the SubjectHostMismatch guard) is obsolete because Absent never reaches the comparison at all. SO I DELETED BOTH ANNOTATIONS RATHER THAN KEEPING THEM. A rung row that describes a defect the tree no longer has is not harmless documentation -- it is a false claim in the file that owns the fact, and the next reader plans against it. That is the stale-citation class this repo already pays for, and the cost is worse for a row asserting a LIVE SAFETY DEFECT than for a stale line number: someone would have re-escalated a fixed bug. WHAT I ACTUALLY CHANGED is only the probe's input shape. main derived Absent from `!run.success || trimmed == ""`, reading the record this branch deletes. The same judgment now reads the arms of ProcessOutcome, and the mapping is exact rather than re-decided: ProcessRefused -> none (did not observe) ProcessOutputAbsent -> none (ran, said nothing) ProcessOutputPresent, trims empty -> none (wrote bytes that do not name a host) ProcessOutputPresent, trims nonempty-> Present The third arm is the one worth stating: ProcessOutputPresent means the process WROTE BYTES, not that those bytes name a host, so the empty-after-trim guard main had is preserved rather than assumed away by the richer type. Also migrated this file's `test -f` site off `.success` onto process_outcome_admitted -- exit status IS the product there, which is why it takes the admitted projection rather than matching arms. CONVERGENCE WORTH NAMING: main's repair and this branch's migration are the same argument from two directions. Main gave the RESULT somewhere to say "not observed"; this branch gave the OBSERVATION somewhere to say it. Neither is redundant with the other, and the merged form is stronger than either -- which is why this resolution takes main's shape rather than defending mine. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>

…onto transport-agnostic command_over_transport (inherits vivid-bee-590's design) (#8628) * command_runner: collapse the transport match at the run site onto command_over_transport command_over_transport already resolves both CommandTransport arms into one plain, directly-executable outer ArgvCommand (LocalExec is the identity; SshExec folds the inner command into one RFC 4254 command string, landed in #8596). Re-deciding the transport at command_runner's run site duplicated that dispatch at its consumer. run_shell_command and run_shell_command_capture now ask command_over_transport once, decompose the resulting argv into program + operands, and hand both straight to shell.Exec.RunArgv -- no bash heredoc, no shell re-parse, no per-transport match, for either transport. Empty argv refuses rather than defaulting. Adds cli_surface_of_literal_words, the one sanctioned route from a runtime List<String> to a CliSurface, and a wet discriminating receipt proving the words reach the process unsplit (excluded from the hermetic floor since the property isn't observable without a real process). Corrects two now-stale claims about command_runner's heredoc path in bmc_netboot_serve.dag and the shell-to-dag residual census doc. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * command_runner: file the ssh exit-255 conflation as its own typed DissolutionCondition Records the four vivid-bee-590 design points durably in the tree rather than only in review discussion: the Built/Refused distinction and the LocalExec redesign latitude were already covered in prior comment blocks; this adds a dedicated ssh_exit_255_conflation_dissolution row (rung: mitigatable, next- rung trigger: an SshExec-typed 255 ProcessOutcome variant, gated on a real retry consumer) alongside the existing command_runner_dissolution_trigger, and trims the run-site comment to point at it instead of duplicating the same facts as prose the compiler cannot read as evidence. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Sonnet 5 <noreply@anthropic.com>

… measured, not claimed (#8655) * Correct two gates that describe per-PR enforcement in the present tense while not running Measured 2026-08-19: dag/tools carries 12 gate modules and ZERO are referenced by any workflow. .github/workflows/ holds two files, and witnesses.yml's only executing step is claim_executor --required-floor. tools.extdeps_scope_placement_gate calls itself a "server-side per-PR wall" that "refuses any dag/extdeps .dag file added by THIS CHANGE"; tools.prose_row_introduction_gate opens with "THE PER-PR WALL". Neither is standing. DESIGN is already honest about this -- its "Building & checks" section declares the 2026-08-15 floor cut as a bounded rung drop and names the effect gates among what is unguarded until the re-add queue closes. What was never updated is the module-level prose, and that is the copy a session actually opens. A wall described in the present tense is a premise the next plan gets built on. PROSE ONLY. No enforcement is re-added, no gate deleted, no roster touched. Only the description is corrected to match the mechanism, citing DESIGN as the authority rather than restating its contents. tools.rust_stage0_gates was checked and needs no correction: it says per-PR execution is "gated on #6239", which states the wall is blocked rather than asserting it stands. RECORDED WITH IT, because it is what made the gap invisible and it generalises past these files: THE .dag CALL GRAPH IS NOT THE EXECUTION GRAPH. Any claim of the form "this runs in CI" is decided by .github/workflows/ and the fold those workflows invoke, never by who calls whom in .dag. Two sessions independently traced the .dag callers of git.Core.DiffUnified0, both concluded it was on a path CI walks every run, and both were wrong -- agreeing was not a second observation, because both had read the same artifact. The finding is stronger than "these two gates are dormant". In hermetic mode eval_mock_response replays the operation RESULT off the declaration's mock_response and never touches argv, so no argv is CONSTRUCTED in the mode CI runs. No argv defect of any kind is observable there. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Refuse the argv representation ambiguity instead of silently resolving it A free monoid whose elements are Strings satisfies BOTH readings at an argv position: value_as_host_string folds it into one concatenated word (its `Value::Str(s) => out.push_str(&s)` arm), and free_monoid_to_vec splices it into N words. The value records no choice between them, and push_shell_argv_tokens tried the concatenating reader first -- so one declared List<String> produced ONE argv word when it arrived monoid-encoded and N words when it arrived as a native list. Same type, same declaration, opposite arity, decided by a representation the author never selected. This is a state-space conflation, not a missing wall, which is why no branch ordering could have been correct: "one argument whose text is the concatenation" and "N arguments" are different states with different remedies. The position now raises a typed, located diagnostic naming the argv index and both readings. MEASURED SPECIMEN: extdeps.git.git git_diff_range_argv returns [base, head] on its TwoDot arm, spliced into `git diff -U0 <range>`. Monoid-encoded that reaches the process as `mainHEAD`. The failure is not that git errors -- on any pair whose concatenation names a real object it produces a successful diff of the WRONG RANGE, which is fabricated plausible output rather than a crash. DELIBERATELY UNCHANGED: Int-element monoids stay char-decoded (unambiguous under one reading only); native Value::List keeps its N-word expansion; ProcessArgvExpansion stays authoritative; and value_as_host_string itself is untouched -- value_to_host_string wraps it for general use, and narrowing a shared helper to fix one caller is the forked-logic trap this lane exists to remove. The empty monoid keeps its current empty-string reading, called out in-code as a deliberate narrow choice rather than left implicit. EVIDENCE, and the RED is unit-level by necessity rather than convenience: in hermetic mode eval_mock_response replays an operation's RESULT off its declaration and never touches argv, so no argv is CONSTRUCTED in the mode CI runs and there is no execution to assert against. Three assertions build the representations directly. Proven discriminating by disabling the refusal and re-running: native list of two strings -> 2 argv words (holds both ways: control) monoid-encoded, refusal enabled -> refuses monoid-encoded, refusal disabled -> FAILED, argv ["mainHEAD"] codepoint monoid -> 1 word (holds both ways: control) NO FROZEN ROSTER, because the refusal IS the census: whatever breaks was relying on the concatenation, and that is exactly the population worth enumerating. Each will be fixed from first principles -- either a latent instance of this defect, or a site that genuinely wants one word and should say so with an explicit join. No arm restoring the old behaviour will be added for sites that complain. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Open the vocabulary axis of realization_vocabulary_containment; falsify the REST/CLI boundary The argv lane keeps asserting in prose that a Redfish/REST path constructs no process invocation. Prose cannot be contradicted by the tree. This makes it a row that reds. NO SECOND LENS WAS MINTED. v2.lens.realization_vocabulary_containment already answers "does module X reach construction vocabulary from set V". The obstacle was that V was a literal: the importer-path axis was already threaded as a parameter through scan_facts_for_leaks_under, while module_is_target_ast_vocab was welded into the predicate. A second lens for a second V would have been the section 3 duplication this lens exists to detect, so the vocabulary axis was opened instead -- the section 2 horizontal move, one axis rather than N copies. RealizationVocabularySet + module_is_in_vocab + is_vocab_leak_in / scan_facts_for_leaks_in / vocab_leak_count_in / vocab_leak_count_live_in. target_ast_vocabulary() DERIVES from the existing target_ast_vocab_modules and target_ast_vocab_module_prefixes rows rather than replacing them, because gunbc.realization_vocab_confinement_census consumes those rows directly and has live claims against them. THE OLD ENTRY POINTS DELEGATE, they do not keep a parallel copy. Leaving the original fold beside the general one would have been one predicate with two implementations -- the fork this lens detects, one level down. The exempt population is a PARAMETER rather than a global roster read, so "this vocabulary has zero admitted exceptions" is a stated fact instead of an accident of the target-AST roster happening to name no CLI module. TWO SITES LEFT TARGET-AST-ONLY, DELIBERATELY, with the reason in-file: the two projections feeding the grandfathered-roster staleness check, whose roster rows are target-AST debt by construction (RealizationVocabDebtClass has no other inhabitant). A second vocabulary arrives with an empty exempt population and so has no roster to be stale against; parameterizing them now would answer a staleness question about a population that does not exist. Trigger recorded. THE FALSIFIER'S SUBJECT IS NOT AN EMPTY UNIVERSE, which is how a negative claim usually turns vacuous. dag/extdeps/bmc contains a module that legitimately reaches this vocabulary -- openbmc_fan_control, the module this lane routes through jq -- beside redfish.dag, which does not. So the scan discriminates WITHIN the population, and the RED control is live corpus data rather than a planted fixture: withdraw the one admitted edge and the count must become 1. Without that assertion a clean result is indistinguishable from a scan that read nothing, which is the empty-observation narrow. The admitted edge is named at exact (importer_path, vocab_module) grain, so a SECOND jq-reaching module anywhere in the scanned roots reds rather than being absorbed by a pattern broad enough to cover it. EXECUTED: all three witnesses return true, including the discrimination control at exactly 1. The pre-existing lens witnesses (planted_leak, discriminators, roster_soundness) return true unchanged. SCOPE, STATED RATHER THAN IMPLIED: the witness is floor-discovered -- neither long/-homed nor in floor_prepared_subject_exclusions -- and reads the live tree, but only the two named directories. A module outside those roots reaching CLI vocabulary is not seen here, and no green from this file may be read as whole-corpus coverage. That lens's whole-corpus half is enrolled on a cadence that does not currently run, which is a fact about the cadence rather than about this witness. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Widen the CLI-vocabulary falsifier root by root; every clean root carries its own control The boundary was enforced in two directories and prose everywhere else. That was the whole of its limitation, so this widens it -- one root per assertion rather than one widened list, so a failure names the root that broke instead of reporting that something, somewhere, reaches CLI vocabulary. ROOTS ADDED, each landing in a stated state rather than behind one green: dag/extdeps entirely -- one admitted edge (the fan control jq edge, already named) plus the jq definition site on the edge roster. Clean otherwise. src/v2/{std,compiler,lens,workflow} -- ZERO admissions. The compiler substrate constructs no process invocation at all. If any of it ever needs a CLI surface, that is an architectural event and it reds here first. A CLEAN ROOT AND AN UNREAD ROOT BOTH REPORT ZERO, and those are different states -- bottom-as-answer against bottom-as-ignorance. Three controls separate them, because the widened roots have no known edge to withdraw: vocab_scan_fact_count_live asserts each scan acquired real facts, so a zero is a finding rather than a silence. Withdrawing the admission under the WIDE root must still surface the fan control edge at exactly 1. A nonzero fact count proves the extdeps scan read something; it does NOT prove it descended into bmc/ where the only known edge lives, so without this "dag/extdeps is clean" could be clean because the one dirty subtree was never reached. Dropping the definition-edge roster must make the count RISE, which proves that roster admits a real edge rather than naming a path the scan never had a fact for. THE TWO ROSTERS ARE DELIBERATELY DIFFERENT SHAPES. The jq definition site is a PATH prefix because constructing a CLI surface is what that location is for; the fan control admission is an EXACT (importer_path, vocab_module) pair because it is one consumer that happens to need the vocabulary and must not silently become two. EXECUTED: 8 of 8 green, including all four controls. STILL NOT COVERED, stated rather than implied: dag/gunbc carries six modules reaching extdeps.shell.exec (the host-effect and transport layer) and dag/test carries the witnesses that exercise this vocabulary deliberately. Neither is added here. Whether dag/gunbc's shell reach is a realization edge or admitted debt is a policy question about the boundary itself, not a mechanical widening, and it is not this change's to decide. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Close the last roots: the #8535 boundary now reds, stated as infrastructure-vs-consumer THE BOUNDARY, in the form that fails rather than the paragraph: Realization infrastructure may reach transport vocabulary; consumers may not, except by exact named admission. #8535's prose says CLI-backed handlers are one realization cell. This says which modules ARE that cell and refuses the rest by name. dag/gunbc's six extdeps.shell.exec reaches are two different things, split by what the module IS rather than by what it imports: PATH-ROSTERED AS REALIZATION EDGES -- retained_shell_script (defines the counted bridges, calls transport_script_seal), bash_materialized_transport (the only other admit_callers-sealed caller of that seal), host_effect_realize (the realization core, reaching through retained_srvn). Reaching transport vocabulary is what these locations are FOR, which is the same reason jq's definition site is path-rostered. ADMITTED AS EXACT PAIRS -- package_delivery, codex_app_server_press, provider_wire_evidence. Exact, so a SEVENTH consumer reds instead of being absorbed by a prefix broad enough to cover it. THE REASON ON THOSE THREE IS THE FINDING, NOT A JUSTIFICATION. All three reach through retained_foreign, whose declared dissolves_to is the bash emitter -- the destination for foreign executors and pre-runtime bootstrap -- while all three appear to run inside a present gunbc runtime, which would make their real destination typed effects. The roster records a bucket that is probably wrong rather than laundering it, so fixing the bucket takes the admission OFF instead of re-justifying it. That population was reached TWICE INDEPENDENTLY: by a retained_foreign call census and by this import-graph scan, which additionally separated out provider_wire_evidence. Two routes landing on one set is why these are named rather than guessed. dag/test is path-rostered and said so: these are the witnesses that exercise this vocabulary deliberately, including the ones proving the argv refusal itself. A test that could not import the thing it tests would be a test of nothing. Stated as a roster rather than left unscanned, so the exclusion is visible instead of implied by absence. THE GENERAL RULE, written into the file because the next person widening a root will reach for the inherited control and it will pass while proving nothing: RE-ESTABLISH DISCRIMINATION AT THE NEW SCOPE. DO NOT INHERIT IT. A narrow root's RED proves the scan discriminates over THAT root. Widen it and it proves nothing about the new subtrees -- a nonzero fact count shows the scan read something, not that it descended where the dirty modules live. Caught here under a green: dag/extdeps reported clean and would have reported clean had bmc/ never been reached at all. So every root carries, at its own scope, a withdrawal control with an exact expected count and a roster-drop control asserting the count RISES, the latter because an edge roster no fact matches is indistinguishable from a correct one. EXECUTED: 12 of 12 green, six of them controls. The gunbc withdrawal returns exactly 3, which is what establishes the split is real rather than fitted to produce a pass. CONTEXT A READER NEEDS FIRST: only 13 files in the whole corpus reach CLI construction vocabulary. The boundary was substantially intact before anyone described it; this confirms and pins a property the tree mostly has rather than negotiating one into existence. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Model the local process-argv seam; fix the trailing-annotation refusal my own edit introduced TWO THINGS, and the second is a defect I caused and did not catch. 1. shell.Exec.RunArgv -- the local process-argv execution seam. Run is argv ["bash", "-s"] with the script on stdin, so every local ArgvCommand in the corpus renders its argv to quoted TEXT and hands it to a shell that parses it back into an argument vector. The seed does Command::new(&argv[0]) at the far end regardless, so the round trip buys nothing and costs exactly what argv-as-serialization exists to stop: a re-parse where argument boundaries are inferred from text instead of carried. THE PROGRAM IS A SEPARATE INPUT, not the first element of the expansion. execve takes the executable and the argument vector as distinct parameters, and with the program separate as NonEmptyStr an EMPTY argv becomes unconstructible -- the unspawnable empty vector has no representation rather than being refused after the fact. NO success: Bool FIELD. `success` is not an observation, it is a POLICY judgement about one -- jq exits 4 to mean "no output" and 1 to mean "false result", neither of which is failure. A Bool beside stdout makes every caller re-derive that from a field that already discarded the information, and lets a refusal read as empty output. So the wire carries the honest triple and the typed outcome is decoded immediately above it against a caller-declared policy. THAT DECODER IS NOT NEW VOCABULARY. It is the pattern already landed for jq (jq_classify_observation / JqExitPolicy / JqOutcome), so ProcessOutcome and ProcessExitPolicy generalize it and the module records what is owed: jq's types are the specialization, its 4-means-absent rule is the missing third policy variant, and they dissolve into these on the first migrated consumer. Named rather than left to be discovered, and deliberately not done here -- jq's classifier is landed and consumed, so folding it in belongs with the migration that motivates it. Local only, per the standing constraint: no SSH arm. command_over_transport's SshExec prefix-append stays where it is. 2. THE REFUSAL I INTRODUCED. Adding the operation left two block comments trailing at end-of-file with no declaration after them -- in the witness, and in exec.dag, where deleting a `data ... : String` prose row (correctly, per section 4c) orphaned the annotation that had described it. Source annotations attach to a FOLLOWING module item; a trailing block names no subject and the substrate refuses it. Both moved above the declarations they govern, and every .dag this branch touches swept for a trailing `//`. WHY 12 OF 12 GREEN DID NOT CATCH IT, which is the part worth carrying: `gunbc run --function` accepted the file the floor refused. The two paths do not agree on annotation validation, so a per-function green is not evidence that the floor will prepare the same file. My verification loop was reading the weaker path and reporting it as though it were the stronger one. The witness assertions themselves are unaffected and still green, including the new definition-edge roster entry -- which exists because THIS change tripped the falsifier: exec.dag reaching cli_surface is a CLI-vocabulary edge inside dag/extdeps, a root the witness asserts is clean. The module is itself a member of cli_process_vocab_modules, so the reach is vocabulary-internal, on the same footing as jq's module. A roster entry added because a real scan refused is a different thing from one added in anticipation, and the file says so. CI is the verifying consumer for the annotation fix: the refusal reproduces on the floor's preparation path, which is not reachable from any local invocation I could find, so I am not claiming a local green I did not get. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Move seam rationale to module-item grain; annotations are not admitted inside declaration bodies Second refusal from the same root cause, and the constraint is stated in DESIGN section 4c rather than being discovered here: the .dag realization admits only standalone leading // blocks attached to MODULE-SCOPE declarations. Trailing, body, unattached and block-comment forms refuse until separately modeled. I wrote the seam's rationale inside the operation body, which is body grain, so every one of those lines refused. Moved to one consolidated module-scope block above the service declaration -- which is also why the pre-existing operations in this file carry their notes as module-scope rows rather than inline: the language has never admitted the inline form, and I should have read that as the constraint it is instead of as a stylistic accident. Also fixed a comment inside a list literal in the witness. My first sweep counted brace depth and missed it, because a list body is bracket-delimited; the sweep now counts both and the branch is clean under it. NOTHING SEMANTIC CHANGED IN THIS COMMIT. The operation, its inputs, its output shape and the decoder are byte-identical in meaning to the previous commit; only the position of prose moved. Recorded explicitly so the next reader does not have to diff it to find out whether the seam was redesigned under cover of a formatting fix. WHAT THIS COST AND WHY IT RECURRED: I pushed the first annotation fix without local verification, saying CI was the verifying consumer because the refusal is raised on the floor's preparation path and gunbc run --function does not raise it. That was honest but it was also one class at a time -- I fixed the trailing form, pushed, and only then learned the body form refuses too, because CI reports the first failing class and stops being informative about the rest. Reading section 4c's own sentence would have given me both forms at once, and a sweep derived from the RULE rather than from the error message is what I should have run the first time. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * File the finding: admit_callers on a service operation is accepted and inert THE CLASS. admit_callers is the repository's construction wall -- a declaration names who may call it, and anyone else is refused. On a fn it works. On a service operation the same syntax PARSES, RESOLVES CLEAN, and DOES NOTHING. WHY THAT IS WORSE THAN THE WALL BEING ABSENT. An absent wall is visible: you look, find nothing, and know where you stand. This one is invisible while reading as present -- an author seals an operation, a reviewer reads the roster as a boundary, and it admits everyone. It is the inert-lens failure at CONSTRUCTION grain, which is the worst place for it, because a construction refusal is the rung people stop checking behind. Measured evidence that the illusion works: I was one step from reporting "the wall is available" after watching the declaration parse, and the reviewing session says it would have believed me. TWO INDEPENDENT ROUTES, deliberately not two readings of one artifact. BY EXECUTION: admit_callers added to the real shell.Exec.Run naming only gunbc.command_runner, after which the unadmitted gunbc.package_delivery -- which calls Run five times -- resolved byte-identically to the unsealed baseline captured first. BY SOURCE (the other session, independently): enforcement lives at exactly one seed site, gated on an exact-constructor-declaration lookup reading the fn admission list; an operation invocation is not a constructor-declaration lookup, so it never reaches that arm, and no operation-call analogue exists. BLAST RADIUS TODAY: ZERO. No operation in the corpus carries admit_callers -- all 21 occurrences across dag/ and src/v2/ attach to a fn or a sealed type. So this is a LATENT TRAP, not a live hole, and the distinction is stated because the first author to reach for it is the one who gets hurt and will have no reason to doubt it. THE PAIR IS ONE ARTIFACT, which is the point rather than a convenience. The positive control (fn form refuses, green today) and the finding (operation form does not, red today) run through one invocation over sources compiled as DATA via the guarantee probe corpus. Split into two files they would be two observations; together they are a discrimination, and the discrimination is the finding. Without the control, a red could equally mean the mechanism is inert or that this file cannot compile a probe at all -- different states, different remedies. Compiling the sources as data is also what makes the pair possible: a refusal here is a resolve error, so an unadmitted call written directly into this module would take the whole file down with it. EXECUTED: fn form returns true, operation form returns false, same file, same run. ENROLLED AS KNOWN-RED rather than left to fail. A bare red takes the floor down and gets triaged as breakage by someone who does not know why it is there. Per DESIGN 4b it does NOT get deleted when the resolver gains operation-grain enforcement -- it flips to a permanent regression control, because deleting the evidence on the climb recreates specification-without-execution one rung up. The roster's own coherence witness passes with the identity added. RUNG, HONESTLY: not mitigatable but BELOW it, because no mitigation occurs -- nothing refuses, nothing counts, nothing is logged. Attainable ceiling: structurally guaranteed, since the class is decidable and fully modeled and only implementation stands between here and there. NEXT-RUNG TRIGGER: an operation-grain construction refusal exists, verified by a correctly-imported unadmitted caller. The trigger is stated in its VERIFIED form because its first two attempted verifications were inconclusive for reasons unrelated to the seal -- a missing import, then a fixture whose service did not resolve at all. A trigger already mis-measured twice should carry how to measure it. NOT FIXED HERE. The resolver change is substrate work with its own owner and its own review bar; routing around the defect or following it into infer would both be the wrong move from this lane. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Retarget the admission control onto the sealed fixture: 54.9s over a 10s ceiling CI caught a cost defect in my own control, and the floor's summary is what identified it: failed=0, known_red_held=307 (my expected-red enrollment took, 306 -> 307), and completed_over_cost_requirement=1. Nothing was broken; one witness was too expensive. THE ROW: fn_form_admission_refuses_unadmitted_caller took 54940ms against the floor's 10000ms per-witness ceiling and grew RSS by 0.99GB. Its forged source imported extdeps.shell.exec to reach transport_script_seal, so compiling it dragged the whole shell/extdeps closure through the diagnostic census. The operation-form probe beside it cost 516ms for exactly the inverse reason: it imports only std.types. THE FIX is to change the control's SUBJECT, not to raise a ceiling or split the file. test.fixture.sole_constructor_sealed.definer exists precisely to exercise caller admission on a minimal closure -- it is the fixture the corpus already uses for this mechanism -- so the control now forges an unadmitted caller of mint_sealed_local. Same mechanism, same refusal class, two orders of magnitude less work, and it moves the control off a production module it never needed to depend on. DISCRIMINATION RE-VERIFIED AFTER THE CHANGE, not assumed from it: fn form returns true, operation form returns false. A cheaper control that stopped discriminating would be worse than the expensive one. WHAT I COULD NOT MEASURE LOCALLY, said rather than implied: every gunbc run pays a whole-corpus typecheck, so both probes report ~58s wall from this session and the witness-level cost the floor meters is invisible from here. The 54.9s and 516ms figures are the floor's own per-witness numbers, and CI is what will confirm the retarget landed under the ceiling. I am not claiming a local measurement I did not get. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Cut command_runner's local path onto shell.Exec.RunArgv: argv stops round-tripping through a shell THE CHAIN THAT IS NOW GONE from the local arm: render the argv to quoted text, wrap it in a bash heredoc, hand it to a shell, let the shell split it back into an argument vector -- to reach a seed that ends in Command::new(argv[0]).args(argv[1..]) regardless. Every step existed only to undo the step before it. On LocalExec command_over_transport is the IDENTITY, so the render had nothing to transform either. Deleted from that path rather than routed around. MEASURED FIRST, because the assignment's census was stale by construction: 22 live call sites across 5 modules (not 25 across 6), 17 of them run_shell_command_capture. ALL 22 PASS LocalExec -- zero use SshExec -- so the entire live population moves in this cut. The callers are untouched: the change is internal to command_runner and both signatures are preserved. THE ONE ENABLER, and it is the part worth reviewing hardest. ArgvCommand.argv is a runtime List<String>; CliSurface is sole_constructor and its only construction route is through CliArgumentSyntax fragments, which carry declared token classes and bindings. Fragments structurally CANNOT express a word that does not exist until the program runs -- a filesystem path, a hostname. So cli_surface_of_literal_words was added to v2.std.compilers.cli_surface. WHY THAT IS NOT THE AMBIGUITY THE CARRIER EXISTS TO CLOSE: the refused state is a List<String> arriving at an argv position with NO declared role, where "one word whose text is the concatenation" and "N separate words" are both well-formed and the realization must guess. This constructor IS the declaration -- its name says each element is exactly one argv word. It is the same resolution the interpreter refusal I landed earlier tells authors to reach for. The file states what it does not license: an argument whose spelling is known at authoring time belongs in fragments, and reaching for this instead is modeling debt. EMPTY ARGV REFUSES rather than defaulting -- a command with no words names no program, and inventing one is fabricated output. THE SSH ARM IS UNTOUCHED, deliberately. Its prefix-append shape is wrong in kind (RFC 4254 carries one string, so the inner command is a nested serialization target, not a concatenation) and that target belongs to another lane. Two sessions editing one contested branch is worse than either fix. It also carries no traffic through this module today, which is why leaving it cost nothing. THE success FIELD is derived through a NAMED policy -- process_exit_is_admitted(ExitZeroSucceeds) -- rather than a bare exit_code == 0, so the convention this runner applies is something a caller can change rather than a literal to discover. WHAT STILL COLLAPSES, named and not fixed here: "ran and exited nonzero" and "could not be executed at all" both arrive as success: false. Under the old bash hop those were genuinely indistinguishable -- a missing binary became the shell's exit 127, which claims a process ran when it never existed. Going direct removes the shell that fabricated that code, so the distinction is now AVAILABLE at the transport even though ShellCaptureResult cannot express it. Not repaired in this cut because it is not free: 17 call sites read that record and the destination is the ProcessOutcome coproduct one module away, so the repair belongs with the sites it changes. THE DISCRIMINATING RECEIPT, executed wet against a real process: argv ["printf", "%s|", "a b"] direct exec -> one operand "a b" -> stdout "a b|" OBSERVED via a shell -> two operands -> stdout "a|b|" asserted absent All three assertions pass. A green that would still be green with the bash hop restored would prove nothing about what changed, which is why the subject is an argument the two paths DISAGREE about rather than a command that merely succeeds. IT IS WET AND EXCLUDED, for a reason that is structural rather than convenient: hermetic evaluation replays an operation's declared mock_response and never constructs an argv at all, so "the words reached the process unsplit" is not observable hermetically. A hermetic version could only assert the mock, which is specification-without-execution. Excluded exactly as the prior argv receipt is, and the file says so. DIVERGENCE FROM THE RECORDED TRIGGER, stated rather than left for a reader to notice: command_runner_dissolution_trigger names host_effect_apply binding ArgvCommand execution as a typed transport handler. This cut routes command_runner directly at shell.Exec.RunArgv instead. The trigger's second clause -- retire the shell_exec_via_bash glue -- is satisfied for the local arm and NOT for the SSH arm, so the trigger is not yet discharged and I have left it in place rather than claiming it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Restrict the literal-words mint to its two callers; state what CI does not guard; correct the trigger Three review items, all taken. The first is the one that mattered and my semantic defence of it was insufficient. 1. THE MINT IS NOW admit_callers-RESTRICTED. My argument was that a constructor whose name says "each element is one argv word" IS the declaration the refused state lacks, and that stands -- but the declaration was UNBOUNDED. Anyone could make it, about anything, which left the interpreter's argv refusal one import away from being routed around: not defeated, just satisfied by an intent nobody checked was true. Nominal wall, not structural. The admitted population is TWO -- run_shell_command and run_shell_command_capture -- which is what makes the restriction honest rather than aspirational. A third caller is an edit to the list in the declaring module: a counted review event rather than an import written elsewhere. VERIFIED BY EXECUTION, with a discriminating RED rather than by reading the declaration -- which matters more than usual here, because I spent this session proving that this exact mechanism is ACCEPTED AND INERT at operation grain. An unadmitted module calling it is refused: constructor call admission refused: 'v2.std.compilers.cli_surface.cli_surface_of_literal_words' refuses call from 'test.fixture.mint_admit_probe.intruder.unadmitted_mint' — permitted callers: [gunbc.command_runner.run_shell_command, gunbc.command_runner.run_shell_command_capture] Located, names the caller, lists the roster. The admitted callers still work: the wet receipt passes unchanged. This is a fn, which is the grain where the mechanism is verified to fire. The file's note that authoring-time spelling belongs in fragments carries no enforcement, and now says so rather than reading as a wall. 2. WHAT GUARDS THIS CUT, AND WHAT DOES NOT, written where the next author stands. The property "the local path reaches no shell" is established wet and the receipt is FLOOR-EXCLUDED, so CI does not run it and someone reintroducing a render-and-bash hop gets no signal. The exclusion is structural -- hermetic evaluation replays mock_response and never constructs an argv, so a hermetic version could only assert the mock -- but the consequence is a real gap and the module now states it: rung mitigatable, next-rung trigger a wet lane that executes floor-excluded receipts. A green test that nothing runs is exactly the inert evidence DESIGN calls a lie, and the file should not read as enforced. 3. THE TRIGGER NAMED A MODULE THAT WAS NEVER BUILT. Asked whether I had created PARALLEL AUTHORITY rather than whether I matched wording, I measured: there is no host_effect_apply production module (it exists only as a witness test), and host_effect_realize never mentions ArgvCommand. command_runner is the ONLY module that turns an ArgvCommand into a local process. The other ArgvCommand consumers reach shell_command_render, which serializes argv into TEXT for emission (githooks) or for the SSH leg -- a different destination, not a second local-exec route. So this did not diverge from the trigger; it satisfied a better version of one that named a binding nobody wrote, and satisfying it literally would have meant building the second route DESIGN forbids. The row is rewritten to name the condition that actually remains: the SSH arm, which needs the nested command-string target another lane owns, and at which point shell_exec_via_bash and retained_runtime leave this module entirely. Also fixed in passing: my own trigger rewrite wrote a \\U escape into the .dag string instead of the literal character, which made the module unparseable. Caught by resolving the file rather than by reading the diff. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Correct a false premise in the trigger I just rewrote: host_effect_apply exists The conclusion was right and one clause of its evidence was false, which is worse than usual here because it sits in a REPLACEMENT trigger -- the row exists to stop the next author re-deriving the question, and a false premise makes them do it anyway. WHAT I WROTE: no host_effect_apply production module exists, witness test only. WHY I GOT IT WRONG: I searched for a FILE named host_effect_apply*.dag and found only the witness test. It is a FUNCTION. gunbc.host_effect_realize declares host_effect_apply and host_effect_apply_gated and both are production. That is the third scope error of this session in one family -- a limited view read as the population -- and the specific lesson is narrower than the earlier two: searching for a filename does not answer a question about a symbol. WHAT ACTUALLY CARRIES THE ARGUMENT, verified independently rather than taken from the correction: host_effect_realize contains ZERO occurrences of ArgvCommand and does not appear among that type's consumers. So host_effect_apply exists and dispatches effects, but it never reaches an ArgvCommand and is therefore not a second route from an ArgvCommand to a process. command_runner remains the sole one, there is no parallel authority, and satisfying the original trigger literally would still have meant BUILDING the second route rather than finding it. The row now says that, and records the correction in place rather than quietly overwriting it, so a reader who saw the earlier claim learns it was wrong instead of wondering which revision to believe. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Replace ShellCaptureResult with ProcessOutcome across every capture site THE CONFLATION, corrected from how we first described it. I claimed in the previous commit that removing the shell's fabricated 127 made "could not be executed at all" available beside "ran and exited nonzero". I TESTED THAT AND IT IS FALSE: a missing program does not produce a result record at all, it REFUSES the evaluation -- failed to execute 'no_such_binary': No such file or directory (os error 2) -- so spawn failure was already fail-closed one rung above the record, and the RED first proposed for this work would have passed against the old record too. The real conflation is one step over and it was live at EIGHT sites: ran and FAILED, printing nothing -> success=false, stdout="" ran and SUCCEEDED, printing nothing -> success=true, stdout="" Both are stdout == "". Those eight read stdout without consulting success, so a failed probe and an empty result were the same value. THE EIGHT, AND WHAT EACH NOW DOES: fleet_host_key_enrollment.check -- THE WORST ONE. Tested trim(stdout)=="present" with no success check, so a probe that FAILED produced "" != "present" and fell through to the branch that APPLIES. A refusal to read authorized_keys was indistinguishable from the key being absent, and the remedies are opposite. Now: refusal refuses and does not mutate the file. fleet_host_key_enrollment.verify -- did concat("outcome=", trim(stdout)), so a refused verify wrote the literal receipt line "outcome=" into a file someone would later read as fact. Now: outcome=UNKNOWN with the cause. fleet_host_key_enrollment.{user,hostname} -- display only. Routed through process_outcome_receipt_text, which renders the three arms to three DISTINCT strings; a refusal can no longer read as empty. fleet_probe_identity_observe.user -- display only, same route. fleet_probe_identity_observe.{passwd_home,job_home} -- USED AS PATHS, not just printed, so they match the arms directly: "(refused: ...)" is fine to print and catastrophic to open. An unreadable home now skips the probe with a stated not-probed line instead of reading .ssh/authorized_keys off a fabricated root. fleet_converge_plan_cli hostname -s -- SURFACED, NOT CLOSED, and said so in file. A `-> String` function has no way to refuse; the honest repair changes the return type and cascades into converge plan subject identity. It now returns a value that CANNOT be mistaken for a hostname rather than a plausible "", so a plan keyed on it is visibly wrong instead of silently wrong. Rung: mitigatable, with the next-rung trigger named. SITES THAT GENUINELY DO NOT NEED THE DISTINCTION, stated rather than left silent: fleet_converge_plan_cli test -f -- exit status IS the product, no stdout anyone wants. Asks process_outcome_admitted directly. Forcing it through an output-bearing variant would add a field it cannot answer. ssh-keygen -F readback -- same shape, same treatment. fleet_ssh_credential_verify x2 -- decompose into a classifier that consumes all three values TOGETHER, so the correlation was already performed. The match adds exhaustiveness and names ProcessOutputAbsent, previously indistinguishable from a failure with empty stdout. DELETED, not kept beside: type ShellCaptureResult is gone. Its one fabricated construction is gone too -- fleet_host_key_enrollment built a ShellCaptureResult to stand in for a FILESYSTEM write failure, inventing success:false for something that was never a process. The coproduct makes that unwritable. scan_host_key_lines shows why the type fits: `scan.success && trim(stdout) != ""` IS ProcessOutputPresent, so a hand-written correlation became a variant. And ssh-keyscan exiting 0 with no key is now a named outcome rather than being reported as a refusal with an empty cause. DISCRIMINATING RED, executed wet, six of six green: nonzero-exit-printing-nothing must be Refused and zero-exit-printing-nothing must be Absent. Both go red if ShellCaptureResult is restored, because then both are stdout == "". The file also records what is NOT tested and why -- the nonexistent-program case is already distinguishable via transport refusal, so asserting it would prove nothing. Recorded on the carrier: spawn failure is fail-closed at the transport, therefore A CALLER CANNOT PROBE FOR A BINARY'S EXISTENCE BY TRYING TO RUN IT -- the attempt stops the line instead of answering. Presence must be asked of something that exists. That is why a separate presence probe has to exist, and it is why no fourth "not spawned" variant was added: it would be an uninhabited arm every consumer must handle and none can reach. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Site 8: the poison IS persisted, and it defeats the guard — second row Checked rather than argued, and the answer is worse than "it might reach a receipt". fleet_converge_plan_wet WRITES host_short verbatim to fleet_converge_plan_subject_host_path, coerces it to NonEmptyStr as the plan's subject host, and folds it into the member-set fingerprint and the plan content hash. An unobserved hostname is persisted as a receipt that later reads as fact. AND IT DEFEATS THE GUARD BUILT FOR THIS EXACT CASE. fleet_converge_apply_wet re-observes the host and refuses on SubjectHostMismatch when observed != planned. Two consecutive refusals produce the SAME string, so the comparison SUCCEEDS and apply proceeds. The check whose entire purpose is to stop a plan being applied on the wrong host is satisfied by two non-observations agreeing with each other -- the empty-observation narrow relocated to the guard: bottom == bottom read as "same host". Making the marker unique per call would NOT repair it; it converts a false match into a false mismatch, which is a different wrong answer, not an observation. NOT INTRODUCED HERE, stated precisely: the prior code persisted "" and compared "" == "", which passed identically. This migration does not repair the defect -- it makes the persisted evidence legible instead of blank. Filed as a SECOND row rather than folded into the first, because the first row's claim (visibly wrong rather than plausibly empty) says nothing about reachability and this row is entirely about reachability. Both mitigatable; different next-rung triggers. This one's: the subject-host comparison consumes an outcome rather than a String, so unobserved-vs-unobserved is a REFUSAL to compare, not an equality. The block is hoisted to module scope as a leading annotation on the declaration (§4c), not left inside the func body. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Hoist 29 body annotations to module-item grain (§4c), and integrate main's command_over_transport refusal coproduct TWO SEPARATE THINGS, both landing here because CI surfaced them together. (1) THE §4c REFUSAL, 29 sites across four files. I put per-site rationale where the explanation belongs conceptually -- beside the line it explains -- which is exactly the position the language refuses. Hoisted every block to a consolidated leading annotation on the declaration. WHAT I ACTUALLY GOT WRONG, since I had already hit this twice: I fixed ONE block earlier and reported it as fixed. I repaired the instance the error named instead of the class the RULE names. The sweep this time is the whole branch and then the whole corpus -- both now zero indented `//`. The refusal is correct and I am not routing around it. It is fail-closed at the source boundary, typed, located to the byte, and it stopped the line rather than silently dropping the prose. The corpus already tried the alternative: `//` as an outright parse error made comment SYNTAX unwritable without making commentary unwritable, and prose migrated into `data ...: String` rows where intent is mechanically indistinguishable from program data. (2) THE MERGE, which was NOT a text conflict to pick a side on. main landed the command_over_transport refusal coproduct (Built | Refused, #8596) while this branch replaced the capture return type. Both arms of both functions had to be rebuilt, not chosen: run_shell_command SSH arm: Refused -> exit_failure with the rendered cause run_shell_command_capture SSH arm: Refused -> ProcessRefused, NOT the deleted ShellCaptureResult main still constructed there Taking either side whole would have been wrong in a way that still compiles on one of them: ours drops main's new refusal handling, theirs resurrects a deleted type. So I took ours and re-applied main's additions explicitly -- the imports, command_over_transport_refusal_reason and its note, and both refusal arms. Note the refusal now composes rather than collapsing: an SSH command that cannot even be BUILT is a ProcessRefused with a stated cause, distinct from one that ran and failed. That is the same distinction this branch exists to make, arriving from main's side of the merge. The LocalExec arm is untouched by the merge and still routes through RunArgv. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Take main's optional-hostname repair and re-express it on ProcessOutcome; DELETE my two mitigatable rows because they are no longer true MAIN FIXED THE DEFECT WHILE THIS BRANCH WAS OPEN, and it fixed it at the rung this lane named as the trigger rather than at the one I settled for. mine: -> String, returning a marker that cannot be mistaken for a hostname. Legible, still not a refusal. Two rows at mitigatable. main: -> NonEmptyStr?, Absent when the probe did not succeed. Plan AND apply refuse outright on Absent, and the subject comparison routes through fleet_converge_apply_subject_host_matches over two NonEmptyStr values instead of a bare String equality. That closes BOTH rows. Row 1 (the value is visibly wrong rather than plausibly empty) is obsolete because there is no longer a value. Row 2 (the poison is persisted, and two non-observations comparing equal DEFEAT the SubjectHostMismatch guard) is obsolete because Absent never reaches the comparison at all. SO I DELETED BOTH ANNOTATIONS RATHER THAN KEEPING THEM. A rung row that describes a defect the tree no longer has is not harmless documentation -- it is a false claim in the file that owns the fact, and the next reader plans against it. That is the stale-citation class this repo already pays for, and the cost is worse for a row asserting a LIVE SAFETY DEFECT than for a stale line number: someone would have re-escalated a fixed bug. WHAT I ACTUALLY CHANGED is only the probe's input shape. main derived Absent from `!run.success || trimmed == ""`, reading the record this branch deletes. The same judgment now reads the arms of ProcessOutcome, and the mapping is exact rather than re-decided: ProcessRefused -> none (did not observe) ProcessOutputAbsent -> none (ran, said nothing) ProcessOutputPresent, trims empty -> none (wrote bytes that do not name a host) ProcessOutputPresent, trims nonempty-> Present The third arm is the one worth stating: ProcessOutputPresent means the process WROTE BYTES, not that those bytes name a host, so the empty-after-trim guard main had is preserved rather than assumed away by the richer type. Also migrated this file's `test -f` site off `.success` onto process_outcome_admitted -- exit status IS the product there, which is why it takes the admitted projection rather than matching arms. CONVERGENCE WORTH NAMING: main's repair and this branch's migration are the same argument from two directions. Main gave the RESULT somewhere to say "not observed"; this branch gave the OBSERVATION somewhere to say it. Neither is redundant with the other, and the merged form is stronger than either -- which is why this resolution takes main's shape rather than defending mine. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * HealthzEffectiveRead becomes the coproduct it always was, and the rung is measured rather than claimed The carrier was { body: String, probe_error: String }, and all 20 of its constructions set exactly one field -- never both, because there is no such observation: a probe either landed and produced a body or refused and produced a reason. The empty string was doing the work of a tag, in a type that also admits the empty string as a legitimate body. It is now HealthzBodyRead | HealthzProbeRefused. ground_service_ready_from_healthz_with_bundle's probe check was the first clause of an if-chain; it is now a match, and the four stages below it split into ground_service_ready_from_healthz_body, which can only ever be reached with a body in hand. THE RUNG, PROBED IN BOTH DIRECTIONS, AND IT IS TWO RUNGS: FIELD ACCESS IS STRUCTURAL. A probe reaching read.body off a refusal made the floor refuse during strict-preparation -- 'no field body on type HealthzEffectiveRead', located, at modules_resolved=3729, before a single witness executed. THE BARE RECORD LITERAL IS NOT. A literal naming the coproduct with no variant tag still resolves and still constructs; it is refused only at the match, at evaluation. Measured: that probe PASSED pre-change (planned=9784, failed=0) and became a per-witness runtime FAIL post-change with the corpus fully executed, not a preparation refusal. So the construction half sits at mechanically preventable, not structurally impossible, and the carrier says so. Next-rung trigger is a compiler capability, named on the declaration: a record literal naming a coproduct type with no variant tag should refuse at resolve, where field access already does. readiness_check_order_note shrank from five ordered stages to four. PROBE left it because it is no longer ordered by anything; the other four remain ordering-by-discipline and the note says which and why. Floor: planned=9783 executed=9783 passed=9475 known_red_held=304 failed=0, against a pre-change baseline of 9784/9476/304/0 -- the delta is exactly the deleted probe. The 4 stale-quarantine rows are identical in both runs and are inherited from main, not from this change. * File the argv fabrication finding: real in the code, unreachable at declared grain, NOT admitted push_shell_argv_tokens ends in two arms that push the format! Display rendering of a value as a host argv word. Null becomes the word 'null', Map and Set become brace-wrapped renderings, Record becomes its type name plus fields -- fabricated plausible output in argv position rather than a crash. For Int, Float and Bool the same arm is correct and wanted, so deleting the fallback would break the good half. REACHABILITY: no declared argv site in the tree can carry a structured value there. All 258 shell-transport operations enumerated, every argv element classified -- 889 string literals, idents typed List<String> / ProcessArgvExpansion / String / NonEmptyStr / FilePath, and calls each returning List<String> or String. Nothing else. Both production callers draw from that population. cargo_build Build does declare env: Map of String to String inside a shell-transport operation, but it is an env input, never an argv element -- a probe matching on the operation rather than on the argv list would have reported a fabricator that cannot execute. The claim is unreachable-at-DECLARED-grain, not unreachable: declared types are not construction-enforced (3939 WhereRefinementUnenforced, no refinement predicate evaluated on any kernel). NOT ADMITTED, failing the standing in both directions: it is not DefectRepairDiagnosticsMayMove because that class needs a behavior the seed exhibits today and an unreachable arm exhibits nothing; and it fails the 2026-08-20 purpose test because hardening a dead seed arm serves v1, not the v2 self-host program. Refusal dominates, so it is recorded rather than fixed, with the one thing that would make it admissible named: a reachable specimen. Floor unchanged: planned=9783 executed=9783 passed=9475 known_red_held=304 failed=0, no errors, no refusals. * Sharpen the next-rung trigger: the decision procedure exists, the refusal does not The trigger read 'a compiler capability', which implies infrastructure to be built. That is not what is missing. v1.compiler.types is_coproduct_type answers the question in one expression -- n.connective == Disj -- and record-literal inference already resolves the literal's named type and already reasons about coproduct membership on the neighbouring path (lookup_variant_parent_enum, variant_owner_node, record_lit_variant_from_expected, record_lit_expected_coproduct). What is absent is the judgment, not the fact. Stated at the reach measured: those symbols answer the VARIANT-named literal (this name is an arm, whose parent is X); the failing case is the PARENT-named literal, which is a different question, and the refusal is neither built nor tested here. So the row moves from DESIGN 4b's second category (can climb after one grounding) to its third (can climb now but unbuilt). Also records the trap for whoever builds it: is_coproduct_type is sufficient for the direct, exactly-resolved specimen; a generalization must apply it to the RESOLVED STRUCTURAL declaration rather than assume every authored alias node carries Disj, or it would silently admit the construction it exists to refuse. Floor: planned=9783 executed=9783 passed=9475 known_red_held=304 failed=0, no errors, no refusals. --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>

Brian Searls and others added 3 commits August 19, 2026 22:24

gunbai-bot Bot force-pushed the session/vivid-bee-590-remote-shell-command branch from 2f66f1d to 087b82e Compare August 20, 2026 00:07

Merge remote-tracking branch 'origin/main' into session/vivid-bee-590…

cb16055

…-remote-shell-command # Conflicts: # dag/gunbc/bmc_netboot_serve.dag

briansrls merged commit 7a23610 into main Aug 20, 2026
1 check passed

briansrls deleted the session/vivid-bee-590-remote-shell-command branch August 20, 2026 01:53

gunbai-bot Bot mentioned this pull request Aug 20, 2026

SHELL-DAG: collapse command_runner's transport match at the run site onto transport-agnostic command_over_transport (inherits vivid-bee-590's design) #8628

Merged

Navigation Menu

Repository navigation

Model the SSH nested command-string target: argv -> shell -> one RFC 4254 command string - #8596

Model the SSH nested command-string target: argv -> shell -> one RFC 4254 command string#8596
briansrls merged 7 commits into
mainfrom
session/vivid-bee-590-remote-shell-command

gunbai-bot Bot commented Aug 19, 2026

Uh oh!

gunbai-bot Bot commented Aug 19, 2026

Uh oh!

gunbai-bot Bot commented Aug 19, 2026

Uh oh!

gunbai-bot Bot commented Aug 20, 2026

Uh oh!

gunbai-bot Bot commented Aug 20, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

gunbai-bot Bot commented Aug 19, 2026

Summary

Test plan

Uh oh!

gunbai-bot Bot commented Aug 19, 2026

Uh oh!

gunbai-bot Bot commented Aug 19, 2026

Uh oh!

gunbai-bot Bot commented Aug 20, 2026

Uh oh!

gunbai-bot Bot commented Aug 20, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant