Repository navigation
TransportScript is a sole-constructor record: close the meta-exec construction half, and the cast form of sole_constructor with it - #7962
Conversation
…struction half, and the cast form of sole_constructor with it
`extdeps.shell.exec` declared `type TransportScript = String where
brand("TransportScript")` — a TRANSPARENT brand, so `as TransportScript`
was writable from any module and the class was lens-guarded, not
construction-walled (DESIGN shell-to-intent row, corrected 2026-07-27).
TransportScript is now a `sole_constructor` record with a `body: String`
field. `transport_script_seal` is the single mint, `admit_callers`-sealed
to exactly two production decls — `gunbc.retained_shell_script`
`retained_shell_script_to_transport` and the new
`gunbc.bash_materialized_transport` `bash_materialized_transport`. No
test declaration is admitted; the execution witness obtains its
TransportScript through the production adapter.
Two things had to be established rather than assumed.
The transport projection (the spike). Dotted-field interpolation into
argv had precedent; routing a record field to `stdin:` had NONE — every
`stdin:` in the corpus was a bare identifier. Proven by execution in a
detached scratch worktree: `stdin: script.body` compiles and delivers
exact bytes through `cat` (including tabs, braces, dollars and both
quote kinds), `bash -s` fed the same way executes and returns stdout and
stderr, and `argv: ["sh","-c","{command.body}"]` discriminates
`test 1 -eq 1` from `test 1 -eq 2`.
The language hole. `sole_constructor` was enforced at the record literal
only, and `std.coercion` `dag_cast_rules` judges a cast only when source
AND target both sit in the primitive cast domain — so a cast into a
sealed record was entirely unjudged, and the wall would have leaked at
exactly the form this change must refuse. `src/v1/04_infer.dag`
`sole_constructor_construction_diags` is now the one authority both
construction forms consult. Corpus census before landing: zero
`as <sealed type>` casts exist across all 17 sole_constructor types, so
the form closed without refusing any existing site.
Verified by execution: whole-tree compile-clean 0 blocking errors;
guarantee-probe suite 5/5 PASS (cast red, unadmitted-caller red,
admitted-caller green, forged-literal red, sanctioned-mint green);
`regen_stage0 --verify` divergence 0. Mutation-tested — unwiring only
the cast diagnostic concat reds `sole_constructor_cross_module_cast_red_refuses`
while both controls stay green, so the wall does the work.
Three production `shell.Exec.Run` sites move onto `retained_runtime`
with declared reasons. The `host_language_transport_script` lens is
reclassified in prose as a regression control per DESIGN 4b(4), not
deleted.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The wall's gating fact is now executed rather than reasoned. transport_script_stdin_byte_fidelity_witness_test runs wet through the production bridge and asserts a payload carrying an embedded tab, an unexpanded dollar and embedded double quotes returns byte-identical from stdout. The frontier line records shell.Exec.Run=3, so three real dispatches occurred and the pass cannot be vacuous. The second control runs the same shape with and without a terminal newline, which attributes the earlier spike round-trip mismatch to the RETURN side (the runtime's stdout layer) rather than to the transport -- the difference between an ambiguity and an attributed fact. The five other reds were all consequences of this change, fixed at their causes rather than by relaxing an assertion: - two witnesses still cast a now-record TransportScript `as String`, which renders the record rather than its body; they project `.body` (review finding, verified against the tree before fixing) - the DESIGN paragraph asserted the construction half both closed and open; both ends now say the same thing, and name the String-bridge residue that IS still open one rung lower - the six sole-constructor probe rows are in lexicographic id order - the dark-suite law gained an honest third arm for the probes that are dag-native rather than disposed or a named gap, plus a partition check so the arms cannot overlap - the roadmap capability-audit brief fits the 100-word budget - the argv expression residue is pinned at 8, not 7: Check's argv element went from a bound name to a field access when TransportScript became a record, which materialization refuses as ArgvExpressionUnsupported. The increment is recorded with its cause and dissolve-on rather than absorbed. Widening Check's input back to a bare String would have deleted the wall to satisfy a census, which DESIGN forbids outright. The live path is unaffected: dispatch_shell evaluates argv expressions. Executed locally on a worktree build, not the stale baked binary: guarantee_probe_corpus 45/45, operation_argv_corpus 9/9, retained_shell_script 2/2, stdin byte fidelity 2/2 wet. DESIGN.md and ROADMAP.md regenerated (ExitSuccess). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Two conflicts, both in the shell-to-intent row and its generated projection. Resolved by NAME, not by side. dag/gunbc/design_document.dag: both sides edited the same row, neither side empty. Main recorded BoundedPoll's deletion (2026-08-07, Node-tree constructor census) in three sentences; this branch rewrote the meta-exec confinement paragraph to say the TransportScript construction half is closed. The edits are disjoint, so the resolution takes this branch's line and applies main's three edits onto it, asserting for each that the target text was present before replacing and absent after. Verified by name afterward rather than by count: all three of main's facts present, both of this branch's present, and the stale claim that TransportScript is a transparent brand over String absent. DESIGN.md: a generated projection. Neither side's bytes are the projection of the merged authorities, so it was regenerated from the resolved authority rather than resolved by hand, per the merge driver's own instruction. ExitSuccess, zero markers, same five facts verified by name in the output. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Both controls execute a real shell through the transport, so dry discovery ran them and both compared false (the 2-of-7767 red on beec1bd). The fix is enrollment, not a weaker assertion: a dry-satisfiable version of this witness would assert nothing about byte delivery, which is the one fact the wall rests on. Same shape as effect_plan_bash_materialize_real_execution_witness_test: LiveTreeDisposition = ReadsLiveTree on the witness module, a BinWitnessWet exclusion row from dry discovery, and two bin_wet roster rows. Green by execution, wet: both controls PASS with [expectation-frontier] shell.Exec.Run=3 -- three real dispatches, not a vacuous pass. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
design_document.dag: one row edited by both sides, disjoint within the row (mine the meta-exec confinement clause, main's the ci_floor_peak/While clause). Resolved by word-grain three-way merge, then verified by NAME that markers from both sides survive and that each side's deleted base phrases are gone -- never by count. v1_compiler_infer.rs is a generated seed and was NOT hand-merged. main deleted the FuncSigLookup variant FuncSigCallerNotAdmitted from 04_sigs.dag, so the ours-side seed was the stale party -- it was the only thing left in the tree referencing a variant no .dag declares. Took main's seed as compilable input and regenerated from the merged .dag authority. DESIGN.md regenerated, not resolved by hand. Seed obligation discharged in the prescribed order: main_wet ExitSuccess, regen_stage0, then a FRESH rebuild before --verify (one pass can self-verify for the wrong reason on a binary predating its own change): regen_divergence_count=0, committed stage0 matches fresh self-compile. My cast wiring survived in the authority: sole_constructor_construction_diags is still defined in 04_infer.dag and still wired at both construction forms. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
review 49822 — both findings fixed, and the caveat it flagged is now discharged by executionBoth findings were repaired in the tree before this comment; this reply is the owed acknowledgement plus the receipt the review asked for.
The stdin caveat is no longer a caveatThe PR body carried one honest caveat: the strict round-trip returned
Those digests are the post-enrollment values and differ from the ones measured during the spike, because the witness module gained a The CI red on
|
…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 authority, and CLI invocation is not the universal effect model (#8535) * 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> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
…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>
…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>
What this closes
extdeps.shell.execdeclaredtype TransportScript = String where brand("TransportScript")— a transparent brand, soas TransportScriptwas writable from any module. DESIGN's shell → intent row said so plainly (correction of 2026-07-27,review 43600): theShellOnHostroute was construction-walled, butshell.Exec.Run's own transport was lens-guarded only, and closing it was named as the meta-exec confinement milestone.TransportScriptis now asole_constructorrecord with abody: Stringfield.transport_script_sealis the single mint,admit_callers-sealed to exactly two production decls:gunbc.retained_shell_scriptretained_shell_script_to_transportgunbc.bash_materialized_transportbash_materialized_transport(new — the Bash-materialization adapter)No test declaration is admitted. The execution witness obtains its
TransportScriptthrough the production adapter. The adapter takes the materialization, not itssourcetext, so no caller can launder self-built text through it, and it refuses withAbsentrather than an empty script (§5 — no fabricated plausible output).The spike (the gating unknown), by execution
Dotted-field interpolation into argv had precedent. Routing a record field to stdin had none — every
stdin:in the corpus was a bare identifier, and inferring stdin support from dotted argv is exactly what this spike existed to not do. Run in a detached, branchless scratch worktree with no remote publication; removed afterward, nothing committed or pushed from it.Established:
stdin: script.bodycompiles, and exact bytes arrive —alpha\nbeta\ttab {brace} $dollar 'sq' "dq" endechoed throughcat.bash -sfed the same way executes and returns stdoutspike-out/ stderrspike-err.argv: ["sh", "-c", "{command.body}"]discriminates:test 1 -eq 1→true,test 1 -eq 2→false.The caveat is discharged. An earlier revision of this section recorded that the strict echo round-trip returned
falseand attributed it to the transport's trailing-newline trim — reasoned, not executed. That attribution has been replaced by a witness rather than by a better argument:dag/test/claim/transport_script_stdin_byte_fidelity_witness_test.dagruns two wet controls through the production bridge and both PASS —transport_script_stdin_delivers_exact_bytes(tab, unexpanded dollar, embedded double quotes; bytes back == bytes in) — subject digest898c66066ad4a8b6transport_script_stdin_fidelity_is_independent_of_terminal_newline(same shape with and without a terminal newline, pinning the difference to the RETURN side) — subject digestbd9eebc35c6f2d49with
[expectation-frontier] shell.Exec.Run=3, three real dispatches, so the pass is not vacuous. Both controls execute a real shell, so they are enrolled wet (LiveTreeDisposition = ReadsLiveTree, aBinWitnessWetexclusion from dry discovery, twobin_wetroster rows) — a dry-satisfiable version would assert nothing about byte delivery, which is the one fact the wall rests on.The language hole this uncovered
sole_constructorwas enforced at the record literal only.std.coerciondag_cast_rulesjudges a cast only when source AND target both sit in the primitive cast domain, so a cast into a sealed record was entirely unjudged — the wall would have leaked at exactly the form the change must refuse.src/v1/04_infer.dagsole_constructor_construction_diagsis now the one authority both construction forms consult (infer_record_litand theExprCastarm). This touches a load-bearing pipeline stage, so:as <sealed type>casts exist across all 17sole_constructortypes — the form closed without refusing any existing site.regen_stage0 --verify→regen_divergence_count=0, committed stage0 matches fresh self-compile.Evidence
--target dag)regen_stage0 --verifyProbes (three new rows in
gunbc.guarantee_probe_corpus, each with an executing witness):sole_ctor_cast_red_probe→ExpectBlockingRefusal{SoleConstructorViolation}— sourceIntis a cast-domain type and the target is not, so only the sole-constructor check can refuse itsole_ctor_unadmitted_caller_red_probe→ExpectBlockingRefusal{ConstructorCallAdmissionRefused}sole_ctor_admitted_caller_green_probe→ExpectZeroDiagnosticsplus the pre-existing forged-literal red and sanctioned-mint green controls.
Mutation test (per the standing rule that a green witness is not a working wall): unwiring only the
cast_sole_ctor_diagsconcat, regenerating and rebuilding, givesFAIL sole_constructor_cross_module_cast_red_refuseswhilePASS forged_literal_red_refusesandPASS admitted_caller_green_controlhold — the hole was real, the mutation was surgical, and the wall does the work. Wall restored from saved copies and probes re-confirmed 5/5 on the restored binaries.Callers moved
Three production
shell.Exec.Runsites route throughretained_runtimewith declared reasons:gunbc.command_runner(generic ArgvCommand heredoc transport, pending the typedhost_effect_applyargv handler) and twogunbc.bmc_netboot_servesites (pre-runtime bootstrap window).Ladder disposition
This class climbs from mechanically preventable (a lens that reds a new raw literal) to structurally impossible for both writable forms: a cross-module record literal and an
as TransportScriptcast now have no constructor. Per DESIGN §4b(4) the discriminating REDs and positive controls stay enrolled as the evidence the higher rung is real. Thehost_language_transport_scriptlens is reclassified in prose as a regression control rather than deleted — it stays deliberately green onComputedApplication, so it still backstops a class construction does not own.DESIGN.md / ROADMAP.md are regenerated from their
.dagauthorities (gunbc.design_document,gunbc.roadmap_authority); the roadmap capability-audit row is narrowed, not closed — the cast form and caller admission are audited, while generics, coproduct variants, default values andmodule_skips_direct_call_arg_checkremain unverified, so that node stays open.Standing gap, named accurately
The
.dag⇄Rust transport seam's execution suite (v1-compiler-tests) does not run in CI. Two things this is not:.github/workflows/ci.ymlrunscargo test -p v1-compiler-tests --release --no-runas a compile-contract gate on every run — the third amendment tocommit_gate_rust_suite_removed_disposition(operator ruling, 2026-07-31, on the Typecheck perf: sink the where-refinement peel, wire the once-per-closure variant base, share the process index #7490 repair). The compile half of the seam is gated on this PR.Terminaland repo-wide: nextest was removed 2026-07-11 by operator ruling (non-required, red on main, ~37 GiB — the fleet's largest CI memory job), and the record says the suite runs locally only. Every PR touching this seam has had exactly this gap since. It leaves with the v1 seed at the DESIGN §7 collapse.An earlier revision of this section claimed the seam had "no CI coverage" and named
cargo test -p v1-compileras the run that would close it. Both were wrong: the compile half is gated, andv1-compilerandv1-compiler-testsare distinct workspace members, so that command resolves and runs the compiler crate's own unit tests rather than the seam suite. A green from it would not have supported the claim it was offered for.