Repository navigation
Name the boundary between shell -> dag and CLI-authority: argv is not the authority, and CLI invocation is not the universal effect model - #8535
Merged
Conversation
…ot the universal effect model gunbc#8467 establishes that an argv array is a serialization, exactly as bash text is a serialization of a bash AST. Accepted. But stated without a boundary it reads as replacing every typed effect with a CLI tree, which moves the authority downward into one realization technology -- the section 3 violation this lane exists to name, one layer below where it usually appears. So the two lanes are one migration program with a named boundary. This lane owns the semantic destination and site routing: the authority stays the typed domain operation or typed HostEffect, and it decides whether a realization is native, REST, filesystem, library, CLI-backed, or necessarily text-emitting. #8467 owns the inside of the CLI-backed cell. A native handler reaches no CLI surface at all. The census also carried a stale unit. Sizing by argv occurrence, then by executable head, then by tool each produced an inflated remainder, because a tool vertical, its site cutovers and its host_effect_apply caller are commonly ONE vertical whose acceptance condition is the old site's deletion. The measured shape, production only: transport shell 236 lines / 48 files -- 230 lines / 45 files in extdeps argv: 457 lines -- 275 extdeps, 172 gunbc, 10 src/v2 bridge calls 48 across 13 files fn *_argv 333, of which ~158 model no tool at all transport shell is overwhelmingly an extdeps population, i.e. beneath already-typed operations. This lane's original job -- getting shell out of the intent -- is substantially done; the remainder is transport depth. Recorded with the caution that a transport shell block is not a shell program at all: the seed executes it as Command::new(&argv[0]).args(&argv[1..]). Two finish lines are therefore named separately, SHELL-DAG and CLI-AUTHORITY, so a row complete against the first but owing the second reads as the boundary working rather than as incomplete work. A SHELL-DAG row is never blocked on CLI-AUTHORITY. One live instance found while verifying: extdeps.exec.command command_over_transport builds append(ssh_exec_prefix, command.argv) -- the exact SSH-as-prefix shape the boundary forbids -- in production, beneath the generic runner, which is the mechanism by which remote argument boundaries are lost. It shares a file with command_runner's argv -> quoted text -> heredoc round trip, whose carrier already declared the repair in command_runner_dissolution_trigger. The runner cut and the SSH target are one vertical. No code changes. DESIGN.md needs no edit and says so in the text: its shell -> intent row already routes runtime-present sites to typed effects and confines emission to foreign executors and bootstrap, so the boundary falsifies no sentence in it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…weaken the sequencing claim Review on #8535 found the first commit did the exact thing this document warns about five times: it appended a corrected boundary beside stale operational text without deleting the text it supersedes. The finding is correct and the stale claim is load-bearing. TransportScript has not been a transparent brand since #7962. It is a sole_constructor record whose single mint transport_script_seal is admit_callers-sealed to two production declarations, and the cast form closed with it -- 04_infer sole_constructor_construction_diags judges a cast into a sealed type. Both documents still asserted, in the present tense and in fourteen places, that the brand is transparent, that `String as TransportScript` is writable from any module, and that direct shell.Exec.Run is guarded by validation rather than construction. All false at this head. Enumerated by claim across both authorities rather than fixing the site under review -- the document's own standing rule, added after the fifth time this class recurred -- and rewrote every occurrence in place: section 3's terminal paragraph, 4.F's heading and three table cells, the 4 dissolution trigger, 5's end-state paragraph, 5.E's heading, premise and ruling block, the wind-down ledger row, the meta-exec row, and both sites in the invariant doc. The leak fixture is reclassified as scan input and historical record; it can no longer be cited as evidence the cast compiles. What actually survives is smaller and different in kind: the two admitted bridges take a bare body String, so arbitrary text still reaches a transport through a counted, reason-bearing, dissolves_to-carrying call. Conspicuous, not impossible, and it dissolves by per-site migration rather than by further wall work. Also from the review, each verified before acting: - The bridge count named no files. Enumerated all 13. Three -- package_delivery, codex_app_server_press, bmc_netboot_serve -- are absent from the section 4 punch-list that still calls itself complete at 78f43c3. Recorded as that snapshot's correction, not as a second census. - A classification question the count concealed: package_delivery (7 calls) and codex_app_server_press (3) route through retained_foreign, whose dissolves_to is the Bash emitter, while both appear to run inside a present gunbc runtime. If so, ten calls declare the wrong destination. Flagged for their owners; the executor window decides it and this document does not own that fact. - "A SHELL-DAG row is never blocked on CLI-AUTHORITY" was true of the homing decision and false as a sequencing rule, with the counter-example named in the same document: command_runner's cutover needs the structured process-argv carrier, and its SSH arm the nested shell-command target. Reworded. - Added an explicit statement that this is a boundary and scoping increment, not a closeout receipt -- neither finish line is met at this commit. Merged main to pick up #8467, now landed, so the cross-PR references describe a merged authority rather than an open branch. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The boundary section asserted DESIGN.md needed no edit BECAUSE its shell -> intent open-thread row already routed runtime-present sites to typed effects. That row is gone: #8476 cut DESIGN to ~9.5k words and removed open-threads wholesale, and this branch merged main two commits ago. The conclusion survives, the reason does not. What the boundary instantiates now is section 3 general paragraph -- interface, realization and policy are three facts, transport is a Realization handler one of N, dispatch sits peripheral -- so a CLI-backed handler is that shape at the tool seam and DESIGN still needs no edit. Caught while verifying the previous commit against the rewritten DESIGN rather than the one the clause was written against, which is the same check the previous commit performed on fourteen other claims. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 19, 2026
…ucture-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>
briansrls
pushed a commit
that referenced
this pull request
Aug 19, 2026
…t two gates that claim enforcement they no longer have (#8549) * 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> --------- 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>
briansrls
pushed a commit
that referenced
this pull request
Aug 20, 2026
…he dead import it names (#8612) * Name the boundary: argv is not the authority, and CLI invocation is not the universal effect model gunbc#8467 establishes that an argv array is a serialization, exactly as bash text is a serialization of a bash AST. Accepted. But stated without a boundary it reads as replacing every typed effect with a CLI tree, which moves the authority downward into one realization technology -- the section 3 violation this lane exists to name, one layer below where it usually appears. So the two lanes are one migration program with a named boundary. This lane owns the semantic destination and site routing: the authority stays the typed domain operation or typed HostEffect, and it decides whether a realization is native, REST, filesystem, library, CLI-backed, or necessarily text-emitting. #8467 owns the inside of the CLI-backed cell. A native handler reaches no CLI surface at all. The census also carried a stale unit. Sizing by argv occurrence, then by executable head, then by tool each produced an inflated remainder, because a tool vertical, its site cutovers and its host_effect_apply caller are commonly ONE vertical whose acceptance condition is the old site's deletion. The measured shape, production only: transport shell 236 lines / 48 files -- 230 lines / 45 files in extdeps argv: 457 lines -- 275 extdeps, 172 gunbc, 10 src/v2 bridge calls 48 across 13 files fn *_argv 333, of which ~158 model no tool at all transport shell is overwhelmingly an extdeps population, i.e. beneath already-typed operations. This lane's original job -- getting shell out of the intent -- is substantially done; the remainder is transport depth. Recorded with the caution that a transport shell block is not a shell program at all: the seed executes it as Command::new(&argv[0]).args(&argv[1..]). Two finish lines are therefore named separately, SHELL-DAG and CLI-AUTHORITY, so a row complete against the first but owing the second reads as the boundary working rather than as incomplete work. A SHELL-DAG row is never blocked on CLI-AUTHORITY. One live instance found while verifying: extdeps.exec.command command_over_transport builds append(ssh_exec_prefix, command.argv) -- the exact SSH-as-prefix shape the boundary forbids -- in production, beneath the generic runner, which is the mechanism by which remote argument boundaries are lost. It shares a file with command_runner's argv -> quoted text -> heredoc round trip, whose carrier already declared the repair in command_runner_dissolution_trigger. The runner cut and the SSH target are one vertical. No code changes. DESIGN.md needs no edit and says so in the text: its shell -> intent row already routes runtime-present sites to typed effects and confines emission to foreign executors and bootstrap, so the boundary falsifies no sentence in it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Delete the refuted transport-wall prose; enumerate the bridge files; weaken the sequencing claim Review on #8535 found the first commit did the exact thing this document warns about five times: it appended a corrected boundary beside stale operational text without deleting the text it supersedes. The finding is correct and the stale claim is load-bearing. TransportScript has not been a transparent brand since #7962. It is a sole_constructor record whose single mint transport_script_seal is admit_callers-sealed to two production declarations, and the cast form closed with it -- 04_infer sole_constructor_construction_diags judges a cast into a sealed type. Both documents still asserted, in the present tense and in fourteen places, that the brand is transparent, that `String as TransportScript` is writable from any module, and that direct shell.Exec.Run is guarded by validation rather than construction. All false at this head. Enumerated by claim across both authorities rather than fixing the site under review -- the document's own standing rule, added after the fifth time this class recurred -- and rewrote every occurrence in place: section 3's terminal paragraph, 4.F's heading and three table cells, the 4 dissolution trigger, 5's end-state paragraph, 5.E's heading, premise and ruling block, the wind-down ledger row, the meta-exec row, and both sites in the invariant doc. The leak fixture is reclassified as scan input and historical record; it can no longer be cited as evidence the cast compiles. What actually survives is smaller and different in kind: the two admitted bridges take a bare body String, so arbitrary text still reaches a transport through a counted, reason-bearing, dissolves_to-carrying call. Conspicuous, not impossible, and it dissolves by per-site migration rather than by further wall work. Also from the review, each verified before acting: - The bridge count named no files. Enumerated all 13. Three -- package_delivery, codex_app_server_press, bmc_netboot_serve -- are absent from the section 4 punch-list that still calls itself complete at 78f43c3. Recorded as that snapshot's correction, not as a second census. - A classification question the count concealed: package_delivery (7 calls) and codex_app_server_press (3) route through retained_foreign, whose dissolves_to is the Bash emitter, while both appear to run inside a present gunbc runtime. If so, ten calls declare the wrong destination. Flagged for their owners; the executor window decides it and this document does not own that fact. - "A SHELL-DAG row is never blocked on CLI-AUTHORITY" was true of the homing decision and false as a sequencing rule, with the counter-example named in the same document: command_runner's cutover needs the structured process-argv carrier, and its SSH arm the nested shell-command target. Reworded. - Added an explicit statement that this is a boundary and scoping increment, not a closeout receipt -- neither finish line is met at this commit. Merged main to pick up #8467, now landed, so the cross-PR references describe a merged authority rather than an open branch. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Fix the DESIGN clause this PR falsified: #8476 cut the row it cited The boundary section asserted DESIGN.md needed no edit BECAUSE its shell -> intent open-thread row already routed runtime-present sites to typed effects. That row is gone: #8476 cut DESIGN to ~9.5k words and removed open-threads wholesale, and this branch merged main two commits ago. The conclusion survives, the reason does not. What the boundary instantiates now is section 3 general paragraph -- interface, realization and policy are three facts, transport is a Realization handler one of N, dispatch sits peripheral -- so a CLI-backed handler is that shape at the tool seam and DESIGN still needs no edit. Caught while verifying the previous commit against the rewritten DESIGN rather than the one the clause was written against, which is the same check the previous commit performed on fourteen other claims. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Settle the census's misfiled-bucket question by measurement, and delete the dead import it names The census flagged three modules as possibly-misfiled -- package_delivery, codex_app_server_press and provider_wire_evidence route through retained_foreign, whose dissolves_to is the Bash emitter (foreign executors and pre-runtime bootstrap), while appearing to run inside a present gunbc runtime. It recorded that as "a question for their owners -- the executor window is the deciding fact and this document does not own it." The question was decidable without them. package_delivery calls shell.Mkdir.Parents and shell.Find.FilesAndSymlinksWithMode -- typed operations that cannot execute without a present runtime -- in the same function bodies that then fall back to retained_foreign. A function that interleaves a typed operation with a retained foreign script is runtime-present by the fact that its first half ran. So the six remaining calls declare the wrong dissolution target. Three corrections fall out, all measured on 98d7147: - provider_wire_evidence has ZERO retained_foreign call sites. Its effects became typed extdeps.shell operations under review 50540; what survived was an unused import, deleted here. It is struck from the bucket, which is 12 rather than 13, struck through rather than dropped -- a census row that vanishes without explanation cannot be told from one that was never measured. - The call counts are stale in the direction the census warns about elsewhere: 5 and 1, not 7 and 3. - package_materialized_tree_observation_note records replacing a find-piped-to-sort string with shell.Find plus in-substrate std sort, because the string form escaped its quoting on a root containing an apostrophe and forked an authority extdeps.shell already owned. That migration landed at ONE site; another instance remains in the same module with the same shape and the same exposure. A carrier that records a fix should name the population it fixed, or the next reader takes the note as coverage. Local whole-corpus compile was started and killed at 15 minutes without terminating, so it is INCONCLUSIVE rather than clean -- stated rather than omitted. The deleted import is verified unreferenced by grep; CI's floor is the census. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls
pushed a commit
that referenced
this pull request
Aug 20, 2026
…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>
briansrls
pushed a commit
that referenced
this pull request
Aug 20, 2026
…ority, not dead code (#8623) * Name the boundary: argv is not the authority, and CLI invocation is not the universal effect model gunbc#8467 establishes that an argv array is a serialization, exactly as bash text is a serialization of a bash AST. Accepted. But stated without a boundary it reads as replacing every typed effect with a CLI tree, which moves the authority downward into one realization technology -- the section 3 violation this lane exists to name, one layer below where it usually appears. So the two lanes are one migration program with a named boundary. This lane owns the semantic destination and site routing: the authority stays the typed domain operation or typed HostEffect, and it decides whether a realization is native, REST, filesystem, library, CLI-backed, or necessarily text-emitting. #8467 owns the inside of the CLI-backed cell. A native handler reaches no CLI surface at all. The census also carried a stale unit. Sizing by argv occurrence, then by executable head, then by tool each produced an inflated remainder, because a tool vertical, its site cutovers and its host_effect_apply caller are commonly ONE vertical whose acceptance condition is the old site's deletion. The measured shape, production only: transport shell 236 lines / 48 files -- 230 lines / 45 files in extdeps argv: 457 lines -- 275 extdeps, 172 gunbc, 10 src/v2 bridge calls 48 across 13 files fn *_argv 333, of which ~158 model no tool at all transport shell is overwhelmingly an extdeps population, i.e. beneath already-typed operations. This lane's original job -- getting shell out of the intent -- is substantially done; the remainder is transport depth. Recorded with the caution that a transport shell block is not a shell program at all: the seed executes it as Command::new(&argv[0]).args(&argv[1..]). Two finish lines are therefore named separately, SHELL-DAG and CLI-AUTHORITY, so a row complete against the first but owing the second reads as the boundary working rather than as incomplete work. A SHELL-DAG row is never blocked on CLI-AUTHORITY. One live instance found while verifying: extdeps.exec.command command_over_transport builds append(ssh_exec_prefix, command.argv) -- the exact SSH-as-prefix shape the boundary forbids -- in production, beneath the generic runner, which is the mechanism by which remote argument boundaries are lost. It shares a file with command_runner's argv -> quoted text -> heredoc round trip, whose carrier already declared the repair in command_runner_dissolution_trigger. The runner cut and the SSH target are one vertical. No code changes. DESIGN.md needs no edit and says so in the text: its shell -> intent row already routes runtime-present sites to typed effects and confines emission to foreign executors and bootstrap, so the boundary falsifies no sentence in it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Delete the refuted transport-wall prose; enumerate the bridge files; weaken the sequencing claim Review on #8535 found the first commit did the exact thing this document warns about five times: it appended a corrected boundary beside stale operational text without deleting the text it supersedes. The finding is correct and the stale claim is load-bearing. TransportScript has not been a transparent brand since #7962. It is a sole_constructor record whose single mint transport_script_seal is admit_callers-sealed to two production declarations, and the cast form closed with it -- 04_infer sole_constructor_construction_diags judges a cast into a sealed type. Both documents still asserted, in the present tense and in fourteen places, that the brand is transparent, that `String as TransportScript` is writable from any module, and that direct shell.Exec.Run is guarded by validation rather than construction. All false at this head. Enumerated by claim across both authorities rather than fixing the site under review -- the document's own standing rule, added after the fifth time this class recurred -- and rewrote every occurrence in place: section 3's terminal paragraph, 4.F's heading and three table cells, the 4 dissolution trigger, 5's end-state paragraph, 5.E's heading, premise and ruling block, the wind-down ledger row, the meta-exec row, and both sites in the invariant doc. The leak fixture is reclassified as scan input and historical record; it can no longer be cited as evidence the cast compiles. What actually survives is smaller and different in kind: the two admitted bridges take a bare body String, so arbitrary text still reaches a transport through a counted, reason-bearing, dissolves_to-carrying call. Conspicuous, not impossible, and it dissolves by per-site migration rather than by further wall work. Also from the review, each verified before acting: - The bridge count named no files. Enumerated all 13. Three -- package_delivery, codex_app_server_press, bmc_netboot_serve -- are absent from the section 4 punch-list that still calls itself complete at 78f43c3. Recorded as that snapshot's correction, not as a second census. - A classification question the count concealed: package_delivery (7 calls) and codex_app_server_press (3) route through retained_foreign, whose dissolves_to is the Bash emitter, while both appear to run inside a present gunbc runtime. If so, ten calls declare the wrong destination. Flagged for their owners; the executor window decides it and this document does not own that fact. - "A SHELL-DAG row is never blocked on CLI-AUTHORITY" was true of the homing decision and false as a sequencing rule, with the counter-example named in the same document: command_runner's cutover needs the structured process-argv carrier, and its SSH arm the nested shell-command target. Reworded. - Added an explicit statement that this is a boundary and scoping increment, not a closeout receipt -- neither finish line is met at this commit. Merged main to pick up #8467, now landed, so the cross-PR references describe a merged authority rather than an open branch. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Fix the DESIGN clause this PR falsified: #8476 cut the row it cited The boundary section asserted DESIGN.md needed no edit BECAUSE its shell -> intent open-thread row already routed runtime-present sites to typed effects. That row is gone: #8476 cut DESIGN to ~9.5k words and removed open-threads wholesale, and this branch merged main two commits ago. The conclusion survives, the reason does not. What the boundary instantiates now is section 3 general paragraph -- interface, realization and policy are three facts, transport is a Realization handler one of N, dispatch sits peripheral -- so a CLI-backed handler is that shape at the tool seam and DESIGN still needs no edit. Caught while verifying the previous commit against the rewritten DESIGN rather than the one the clause was written against, which is the same check the previous commit performed on fourteen other claims. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Settle the census's misfiled-bucket question by measurement, and delete the dead import it names The census flagged three modules as possibly-misfiled -- package_delivery, codex_app_server_press and provider_wire_evidence route through retained_foreign, whose dissolves_to is the Bash emitter (foreign executors and pre-runtime bootstrap), while appearing to run inside a present gunbc runtime. It recorded that as "a question for their owners -- the executor window is the deciding fact and this document does not own it." The question was decidable without them. package_delivery calls shell.Mkdir.Parents and shell.Find.FilesAndSymlinksWithMode -- typed operations that cannot execute without a present runtime -- in the same function bodies that then fall back to retained_foreign. A function that interleaves a typed operation with a retained foreign script is runtime-present by the fact that its first half ran. So the six remaining calls declare the wrong dissolution target. Three corrections fall out, all measured on 98d7147: - provider_wire_evidence has ZERO retained_foreign call sites. Its effects became typed extdeps.shell operations under review 50540; what survived was an unused import, deleted here. It is struck from the bucket, which is 12 rather than 13, struck through rather than dropped -- a census row that vanishes without explanation cannot be told from one that was never measured. - The call counts are stale in the direction the census warns about elsewhere: 5 and 1, not 7 and 3. - package_materialized_tree_observation_note records replacing a find-piped-to-sort string with shell.Find plus in-substrate std sort, because the string form escaped its quoting on a root containing an apostrophe and forked an authority extdeps.shell already owned. That migration landed at ONE site; another instance remains in the same module with the same shape and the same exposure. A carrier that records a fix should name the population it fixed, or the next reader takes the note as coverage. Local whole-corpus compile was started and killed at 15 minutes without terminating, so it is INCONCLUSIVE rather than clean -- stated rather than omitted. The deleted import is verified unreferenced by grep; CI's floor is the census. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Correct the C-note: the fold is an unconsumed authority, not dead code The C-note filed BuildCacheDaemonObservation / provision_build_cache_verdict / placement_verdict / build_cache_provision_gate_accepts as pre-existing dead production code with a deletion plan. I re-ran the census before acting on it. The zero-caller number reproduces exactly: 8 call sites for the gate, all in one witness file; zero production callers for any of the four symbols. The characterization does not. Reading the module's own receipt rather than the grep output, lane_e_srv1_ci_noncompletion_root_cause_receipt names placement_verdict as the FIX AUTHORITY for the stranded-sccache-server incident that killed CI builds at the 15m compile ceiling, and records that class as "INCIDENT CLEARED, NOT REPAIRED". Nine production modules import the module for other declarations, so the symbol-level zero sits inside a live file. That makes this a §4b rung finding, not a §2 redundancy one: the fold is correct and unasked. Green witnesses establish correctness, not that the class is guarded, and reporting them as the latter reads a rung above where the class sits. The deletion would have applied cleanly, taken the witnesses with it, broken nothing, and removed the named remedy for a recurrable CI-capacity incident -- with the witnesses' greenness as the property that made it look safe. Disposition changed from delete to wire-it-up, with the one measurement that could still make it benign named as the first thing to test. No code touched. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Answer the C-note's first test: the path is genuinely ungated for placement The correction said nobody should wire anything before establishing whether the provisioning path is ungated or gated by an equivalent check under another name. Measured on origin/main by reading the three modules involved. There is a check under a different name and it is not equivalent. realize_provision_build_cache gates on provision_build_cache_catalog_gate_verdict, which is pure catalog-id validation in a third module -- unknown id refuses, a non-sccache_local id refuses, otherwise realizable. It never observes placement, principal, unit ownership or lifecycle, so passing it says nothing about the stranded-daemon class the incident receipt names placement_verdict as the fix for. host_effect_realize matches none of the admission symbols. Two unconsumed authorities, not one: build_cache_ensure's admit_ensure_build_cache_instance is in the same state. Both name the same single next consumer, realize_provision_build_cache_body, so this is one wiring job rather than two -- materially smaller than the correction implied. The tree recorded this itself in ensure_effect_grain_migration_note. Verified against the code rather than quoted, since tonight's repeated failure was a correct measurement of a subject that had moved. It has not moved. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Correct the refinement calibration: no predicate is evaluated, on any kernel The guarantee-recovery doc's calibration example read "a nonliteral refined argument is RuntimeBoundaryOnly" -- a check that fires at the runtime boundary rather than at compile time. Measured across all three kernels the refinement family uses, that is true of none of them. String the conversion runs and is the identity. Executed: "" as NonEmptyStr returns "". Int the only conversion refuses every value, so it is never used; values arrive by declaration and no conversion runs. Executed: the cast refuses a valid 5 identically to -1, and -1 reaching an EpochMs-declared parameter comes back unchanged. collection a sound unforgeable wall -- private tuple field, new the only door -- with zero call sites corpus-wide, and zero refinement declarations over any collection base behind it. A gate that passes everything, a gate nobody walks through, and a wall with no door behind it. The Int row most needs stating: "fail-closed by absence of capability" reads as safe and is not, since 74 declared positions against effectively zero casts means the refusing conversion is almost never on the path. This is the document's own section 4b failure rather than a wording slip: one state was recorded for a class whose paths differ, and it was the strongest of them. Each kernel needs a different remedy, so the row cannot be weakened -- it has to be split. Population recorded as a dated measurement with its limits: 3939 across 612 files at a750b67, four pre-committed predicates passing including a by-name planted control, reproduced exactly on separate runners, corroborated by an independent static scan smaller in the predicted direction. The instrument was deleted, so the number is not reproducible without rebuilding it, and it is an unverified-obligation population -- the census cannot distinguish violated from unverified. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Census: retire the stale srv3_join_shell_words citation, record the srv3 deferral measurement Two corrections to the residual census, both measured at origin/main 4cec10f. srv3_join_shell_words has zero definitions and zero mentions on main; it was cited in two places (the §1.C row and the §4.D deferred table) as a live srv3 transport helper. Removed from both. The five sibling symbols cited beside it all still resolve in gunbc.host_effect_realize and are left untouched. The srv3 deferral's premise is refuted by typed refusal: all 22 EmitArtifactThenThinRun arms in gunbc.host_effect_realize refuse, none accept, and the refusal names "reserved for ConvergePlan (host-effect Phase D)." The control widens it past that file -- the variant is realized nowhere in the tree; the three sites that appear to accept it are classifiers returning a Bool or the variant name for totality. So nothing is pending cutover and no srv3 site waits on a Phase D that exists. That settles the premise, not the disposition. Whether the srv* actuator graph survives at all is an operator decision, and migrating 22 call sites in a subgraph slated for deletion by another route is wasted work under a different premise than the original. Recorded as due for re-decision rather than expired. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Census: correct "realized nowhere" — EmitArtifactThenThinRun has exactly one realizer The paragraph committed earlier today claimed EmitArtifactThenThinRun is realized nowhere in the tree and is therefore declared-but-unrealized. That is false, by exactly one path, in the file the claim examined most closely. realize_converge_on_host splits its EmitArtifactThenThinRun arm on gunbc_apply_mode_for_host: FreshStandup refuses as fail-closed Unimplemented, but ExistingHostQuiescentReload calls realize_converge_in_process -- the identical call the LocalShell arm makes. For an existing quiescent host the transport takes the same path as the shell transport. The sibling SshShell and FleetSsh refusals direct the caller to "use EmitArtifactThenThinRun", which points the same way. Two disguises produced the wrong count and each survives a scan written for the other: a refusal shaped as a success-valued record (hostname_set answers HostnameSetCasApplyFailed with the refusal in a stderr field, invisible to a NotConverged scan), and a realizer behind a refusing first sub-arm (the arm above, whose opening lines read as a refusal). Reading all 24 bodies was the only method that survived; the corrected text records both disguises so the next reader does not re-derive them. The srv3 conclusion is unchanged. The realizing path is for HostConverge, not for any srv3 effect -- every Srv3* arm still refuses. Only the supporting sentence changes: not "realized nowhere so nothing is pending" but "exactly one realizer, and srv3 is not on it." Corrected in place rather than annotated beside, per the standing rule against two accounts of one fact. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Census: correct the arm denominator — 36 production arms, not 24 The paragraph recording how the one-realizer finding was measured stated that all 24 arm bodies had been read. That number came from the manual audits and is wrong. Measured at 4cec10f: 41 EmitArtifactThenThinRun occurrences -- 1 variant declaration in gunbc.host_effect, 36 production match arms across 14 modules, 4 in dag/test/claim. Neither manual audit reached 36 and neither mentioned gunbc.host_effect_codex_supervised_turn, whose arm answers CodexSupervisedSessionApplyRefused: a refusal named by its record rather than by a refusal type, which is the same disguise class the paragraph documents. The finding is unchanged -- exactly one arm realizes, realize_converge_on_host under ExistingHostQuiescentReload. What was wrong was the stated size of what had been examined, inside the paragraph about examining carefully. Recorded as a dated measurement at a named SHA for a derived detector to reproduce and reconcile against, explicitly not as a fixed law, since migrations are expected to change it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Census: record v2.lens.effect_reach as prior art to supersede, not extend Answering the census brief's stop condition -- whether existing parsed-body facts can carry the derived census -- surfaced a lens already answering approximately this question, which a later reader could mistake for coverage. v2.lens.effect_reach classifies host-effect sinks and carries a ShellExecRunSink variant. But sink_kind_for_callee selects by name equality against a remembered callee-text list ("Run", "shell.Exec.Run", "Exec.Run", "WitnessBin.Run", "Read"), everything else falling to UnknownHostEffectSink. That is the forbidden seed form -- where we remember doing it rather than what interprets bytes as shell -- and it cannot see sh -c, sh -s on stdin, or a sudo -S sh -s wrapper. It carries the same blind spot this census carried before Spark was found. Two bounds on its weight: it classifies from callee text rather than resolved callee identity, the text-scanning substitution the brief's stop condition forbids; and enforcement_live_witness_test asserts its contract is unbound, the corpus's own record that it has no enrolled consumer. Disposition is supersede rather than extend: a census seeded from interpretation semantics subsumes its whole sink vocabulary, while extending it would inherit its selection principle. Recorded so the derived cut treats it as prior art with a known-narrow frontier, and so its ShellExecRunSink rows are never read as an existing shell-reach population. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls
pushed a commit
that referenced
this pull request
Aug 20, 2026
… 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>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What this is
Documentation only. No
.dagor Rust changes.gunbc#8467 (
sharp-ant-396) establishes that an argv array is a serialization, exactly as bash text is a serialization of a bash AST. That diagnosis is accepted. Stated without a boundary, though, it reads as replacing every typed effect with a CLI tree — which moves the authority downward into one realization technology, the §3 violation this lane exists to name, one layer below where it usually appears.That session asked me to place the boundary while they execute the branch, since two sessions reworking one PR would collide on the same files. This is that half.
The boundary
HostEffect; it decides whether a realization is native, REST, filesystem, library, CLI-backed, or necessarily text-emitting.ArgvCommandandtransport shell { argv: [...] }are migration substrates.The corrected unit
The census carried a stale work unit. Sizing by argv occurrence, then by executable head, then by tool each produced an inflated remainder, because a tool vertical, its site cutovers and its
host_effect_applycaller are commonly one vertical whose acceptance condition is the old site's deletion — not three workstreams.Measured production populations (excluding
/test/,*_test.dag, fixtures):transport shellis overwhelmingly anextdepspopulation — beneath already-typed operations. This lane's original job, getting shell out of the intent, is substantially done; the remainder is transport depth. Recorded with two cautions in the text: thedag/gunbcargv residue is 172 lines across 41 files (real work, and an earlier scoping pass quoted the file count as a line count), and atransport shellblock is not a shell program at all — the seed executes it asCommand::new(&argv[0]).args(&argv[1..]).Two finish lines, named separately
A site can be complete against the first and still owe the second; that is the boundary working, not incomplete work. A SHELL-DAG row is never blocked on CLI-AUTHORITY — stated explicitly because this document has a history of workers routing away from open work on a stale sentence.
One live instance found while verifying
extdeps.exec.commandcommand_over_transportbuildsArgvCommand { argv: append(ssh_exec_prefix(target: t), items: command.argv) }— the exact SSH-as-prefix composition the boundary forbids, since SSH is a nested target whose carrier is one RFC 4254 command string. It is production code beneath the generic runner, so every SSH-transportedArgvCommandflows through it; it is the concrete mechanism by which remote argument boundaries are lost.It shares a file with
gunbc.command_runner'srun_shell_command, which takes a typedArgvCommand, renders it to quoted text viashell_command_render, and posts it throughshell.Exec.Run's heredoc transport — whose carrier already declared the repair incommand_runner_dissolution_trigger. The runner cut and the SSH target are one vertical, and the debt was declared before it was scoped.Verified, not relayed
Every claim asserted here was checked against the tree rather than taken from the conversation that produced it:
push_shell_argv_tokenspushes each evaluated String verbatim; both exec branches areCommand::new(&argv[0]).args(&argv[1..])— no shell, no word splitting, no quoting.command_runner.daground trip and its dissolution trigger.host_effect_plan.dag:39's placeholderShellCommand { script: "" }.Not verified and therefore not asserted: a Git-plumbing design finding ~30 raw argv sites resolving to one
extdeps.gitauthority — no such document is onmain, so it is presumably another session's branch.What is owed, and by whom
JqInvocation,CliSurface,ProcessArgvExpansionor shell target — is owed bysharp-ant-396, who claimed it.cli-invocation-emission-design.md, theirs to place.DESIGN.mdneeds no edit, and the text says so: its shell → intent row already routes runtime-present sites to typed effects and confines emission to foreign executors and bootstrap, so the boundary falsifies no sentence in it. Stated explicitly so a later reader does not "discover" a missing correction and add a second account of one fact.🤖 Generated with Claude Code