Skip to content

CLI invocation emission: design note + Wave 0 carrier probe (argument boundaries survive the grammar fold, proven by execution) - #8467

Merged
briansrls merged 24 commits into
mainfrom
session/sharp-ant-396
Aug 19, 2026
Merged

briansrls merged 24 commits into
mainfrom
session/sharp-ant-396

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Aug 18, 2026 •

Copy link
Copy Markdown
Contributor

What this is

An argv array is a serialization, the way bash text is a serialization of a bash AST. Both
carriers in this repo store the serialized form and treat it as the authority: the declarative
transport shell { argv: [...] } blocks and the value-level builders. That is why the same
defect class keeps recurring — a dropped flag, a bespoke spelling, an embedded language in a
leaf — and why fixing each occurrence never generalizes.

This PR lands the design authority plus the first two executed increments. Nothing is cut over:
no consumer is rewired and no transport argv is deleted.

Measured census (the plan's own numbers were stale by ~2.3x)

argv: lines                                    597 across 129 files
transport shell blocks                         250
operation declarations                         322
success: Bool from "exit_success"              173
exit_code: Int from "exit_code"                 69
literal argv heads                             282
  ...of those, wrappers not tools               78
sh -c / bash -c embedded-language leaves        14

Wave 0 — the argument/fragment algebra

Concatenation is correct within an argument (--color=never, -er) and destructive
across arguments. The algebra is List<List<ConcreteSyntaxToken>>, so CliArgumentSyntax
preserves the grouping a tool's projection selected.

Wave 1A — the jq semantic layer

The domain states what it wants of jq; argv is derived. Two-level derivation closes both defect
classes at their own level: semantic property -> option identity prevents omission, option
identity -> canonical spelling prevents bespoke spelling. Option rows carry raw-output, not
--raw-output: the dashes belong to the grammar. JqCliSelection is a coproduct, not an
Optional, because no option is required and no answer are different states.

Unlowered axes (bindings, file input) are typed refusals, not plausible guesses.

Executed receipts

All nine return true on the real acceptance path. A nonexistent-function control refuses with
NoSuchFunction, so a silent no-run cannot read as a pass — a false-green that did occur earlier
in this lane.

W0  joined_fragments_render_one_argument
W0  separated_fragments_render_three_arguments
W0  both_groupings_flatten_to_the_same_text
W0  keystone_flat_text_is_nonempty
W1A sensor_invocation_lowers_to_exact_argv
W1A stdin_content_is_absent_from_argv
W1A exit_policy_perturbation_adds_the_exit_status_option
W1A unlowered_bindings_refuse
W1A unlowered_file_input_refuses

Known-open, stated rather than implied

  • The CliSurface seal is on shape, not provenance. sole_constructor closes the record
    literal and the cast; serialize_cli_arguments is a public fold taking caller-supplied lex
    rules, so it is an unrestricted mint. An earlier claim in this lane that this was stronger
    than TransportScript was backwards. Section 9's table is corrected accordingly. The repair is
    a sealed AdmittedCliInvocation on the input — admit_callers on the serializer is refused
    on section 3 grounds, since it would make a std module name every tool.
  • Static dependency grain. At execution grain the fold reaches no compiler machinery; at
    dependency grain it still imports target_model. The spelling seam wants extracting below it.
  • A measured, undiagnosed substrate observation about Optional<T> at a primitive T in
    field-construction position, with a section 5 line-stop owed before anything relies on it.
  • The jq -n three-arm fleet control for the SSH argument-boundary defect needs fleet access I
    have not taken unilaterally.

Coordination

eager-wren-138 (#8454) was sweeping the same jq class. Two correctness catches were accepted:
jq -e reads the last output so it converts legitimate false/null into failure, and
SensorIntegerValue has two live consumers whose empty output is a modeled third state, so
-e there would have collapsed Absent into Refused. They withdrew both extdeps edits and
ceded all 22 jq occurrences to this lane.

…is emitted

Design-note-first, no code. Supersedes the Lane B destination of
gunbc.plans.transport_argv_anemia_dissolution, whose diagnosis stands but
which terminates at typed extdeps/tools/* operations and ArgvCommand
builders -- both of which still contain literal argv, so it stops one layer
short.

Measured census (the plan's own numbers are stale by ~2.3x): 597 argv lines
across 129 files, 250 transport shell blocks, 173 operations still carrying
success: Bool from exit_success against 69 preserving exit_code. 78 of 282
literal argv heads are wrappers rather than tools, so tool identity is a
positional accident and the corpus cannot currently be censused for what it
invokes.

The model: JqInvocation (semantic axes) -> CliInvocationTree (options grouped
with their values) -> List<PosixArgument> -> extdeps.posix Command, with the
SSH leg going through the shell grammar already grounded by
extdeps.posix.shell_command_language. Two-level row derivation is the
keystone: semantic property -> option row prevents omission, option row ->
spelling prevents bespoke spelling. Centralizing 597 literals into N helper
functions fixes neither.

Records what measurement refuted during design, including three of my own
claims, so they are not re-derived: the declarative form is not fixed-arity;
RFC 4254 forces a string at the SSH boundary; ProcessInvocation is an
emit-harness carrier, not the general one; SensorIntegerValue is live and its
empty-output branch is a modeled OpenBmcSensorValueAbsent, so an -e sweep
would have collapsed a correct three-state decode.

Rung stated honestly: mechanically preventable, not structural. 04_infer does
not typecheck application argument types, so a nominal CliArgument newtype
makes nothing unwritable today.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@gunbai-bot gunbai-bot Bot changed the title argv migration CLI invocation emission design note: the tree is the authority, argv is emitted (design-note-first, no code) Aug 18, 2026
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review August 18, 2026 22:13
gunbc-ci-auto-heal and others added 4 commits August 18, 2026 22:27
… split rung

Four load-bearing corrections found by review, two of which were errors in the
first revision.

1. jq exit decoding is POLICY-INDEXED, not universal. Verified against
   jqlang.org/manual: default jq exits 0 regardless of output, and only
   --exit-status yields 1 (last result false/null) and 4 (no valid result ever
   produced). The first revision put JqProducedNoResult as a general arm, which
   claims a distinction JqProgramExit cannot supply -- and would have
   reintroduced the exact Absent -> Refused collapse #8454 withdrew.
   SensorIntegerValue derives Absent from successful empty stdout under
   JqProgramExit, never from a jq exit code.

2. No generic decode_exactly_one_nonempty_string. jq emits a stream and -r
   permits newlines inside a raw string, so collapsed stdout is ambiguous;
   --raw-output0 exists for exactly that reason. The note now promises only
   "nonempty observed stdout" until a framing lands.

3. The CLI tree is SEALED. CliOption { values: List<_> } freely constructible
   admits wrong arity, non-repeatable options twice, foreign-tool options.
   Rows carry arity, repeatability, placement and joining; the emitter accepts
   only an admitted tree; domain callers hold no constructor for
   AdmittedCliOptionUse.

4. The rung was too coarse, and stating one number for two subjects was the
   error. The migrated jq path can reach STRUCTURALLY GUARANTEED now via
   sole_constructor + admit_callers -- the wall that closed TransportScript.
   The corpus at large stays mechanically preventable while 575 raw argv lines
   remain. The wall is the sealed constructor, not the type name.

Also: ownership splits by what fact a program encodes, so only policy-bearing
fan programs move to gunbc.bmc_fan_projection while OpenBMC wire decoders stay
in extdeps.bmc; stdin/env/cwd/fd belong to the process plan, not CliSyntax;
generalizing extdeps.posix Command is not a prerequisite, one narrow local jq
realization with an explicit dissolution trigger is; SensorIntegerValue named
as the canonical first vertical with slices B-D after it.

New open question, stated as risk not defect: the 17 remote jq rows place the
filter after the SSH destination as though its local argv boundary survived,
but ssh joins words into RFC 4254's single command string and sshd re-parses
through a login shell. Those filters carry pipes and quotes. Unverified -- no
executed control -- and must be settled before Slice D.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ained rung, executing probe

Six corrections from review, four of them defects in my own prior revisions.

1. Termination and output presence are ORTHOGONAL, not a coproduct. The live
   SensorIntegerValue case holds exit 0 AND zero results simultaneously, so
   writing JqProducedNoResult as an arm beside JqExitZero makes the live case
   unrepresentable. Split into JqExitDisposition x JqOutputPresence.

2. Removing success: Bool was insufficient. An unsealed JqObservation still
   admits { exit: JqExitZero, exit_code: 4 } -- the same writable contradiction
   under richer names. JqObservation is now sole_constructor, minted only by the
   policy-aware decoder, with the raw process observation retained as evidence
   and decoded facts bound to it.

3. The rung sentence was internally inconsistent: "mechanically preventable
   because nothing refuses it" -- if nothing refuses it, it is not prevented.
   Replaced with a subject-grained matrix. The migrated path reaches
   structurally impossible NOW via sole_constructor; the corpus-wide raw-jq and
   raw-argv classes stay open. The terminal trigger is a DOMINATOR condition
   over jq execution paths, not application-argument typechecking, which is
   neither necessary for sealing this path nor sufficient against alternate
   raw routes.

4. Option spelling had two authorities -- jq "how it spells them" and CliSyntax
   "canonical spelling" -- committed inside a note about that exact violation.
   Tool row owns which forms exist and which is canonical; grammar owns how a
   chosen form is constructed.

5. The carrier probe will NOT refuse, so a compile-only probe false-greens.
   emit/serialize_target are fixed to Medium<String>, and v1.04_infer
   explicit_return_conformance_note records conformance is judged only by the
   ground-kernel-scalar and ground-element-collection discipline -- a structured
   Medium<String> vs Medium<CliSurface> mismatch is outside it. The probe is now
   an EXECUTING sibling-serializer probe with five controls, and does not begin
   by genericizing TargetModel.

6. The smallest complete vertical is LOCAL ONLY. SSH adds a second language
   target, RFC 4254 string loss, portable-word refusal, quoting and the sshpass
   -d 0 collision. Recut: Wave 0 probe, Wave 1A ObjectMapperServiceAt as the
   feature-rich exemplar, Wave 1B SensorIntegerValue as the required falsifier
   proving JqProgramExit selects no -e and absence is not refusal, Wave 2 SSH.

Also: the CLI inverse is partial and ambiguity-aware, answering
CliParseUnique | CliParseAmbiguous | CliParseRefused, and is not a Wave 1
acceptance criterion.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ting exists anywhere in the path

Traced end to end. The local half verified in this tree: push_shell_argv_tokens
pushes each evaluated String verbatim and both exec branches call
Command::new(argv[0]).args(argv[1..]), so transport shell at this boundary is
DIRECT PROCESS EXECUTION -- no local shell, no shell_quote, no command-string
renderer. sshpass execvps unchanged. OpenSSH's client consumes -- as its own
option terminator and joins remaining argv with single literal spaces, no
escaping. OpenBMC's default server is Dropbear (corrected from sshd), whose
run_shell_command invokes the login shell with -c.

So a filter containing unquoted pipes arrives remotely as shell pipeline
operators and the jq program's argument boundary is gone. The code assumes
shell_parse(join(argv, ' ')) == argv, which holds only inside the portable-word
alphabet typed_argv_exec exists to bound; these filters are outside it.

Judgments split rather than lumped: boundary preservation Violates
(source-proven); deployed client, reachability and production manifestation
Unverified; Dropbear shell exec StronglySupported but unobserved on this
firmware. Enumerated saving conditions, none visible in the repo. Executed
control specified with jq -n so it cannot mutate BMC state, with the
unexpected-success branch treated as evidence for an unmodeled layer rather
than dismissed.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…roven by execution

The CLI serializer is not a second emitter. bound_tokens_source_text folds a
grammar-selected token sequence, resolves each token to its spelling, and joins
with target_text_seq -- concatenation. That join is where argument boundaries
die, and re-deriving them afterwards is what shell_quote is at 36 sites.

bound_tokens_cli_arguments is the SAME fold with the SAME spelling resolution
and a different join: one argument per token. Nothing about the grammar walk
changes; only whether the boundary survives.

EXECUTED RECEIPT, not a compile:
  cli_serializer_preserves_argument_boundaries  returned true
  text_serializer_loses_the_argument_boundary   returned true
  definitely_not_a_real_function                errored

Two tokens chosen as the smallest thing that can separate the carriers:
"--argjson" and "[1,2] | length". The second carries a space and a pipe, the
shape that loses its boundary at the ssh seam in the 17 remote jq rows. The CLI
carrier yields two arguments with the program intact as one; the text carrier
yields "--argjson[1,2] | length" with the boundary gone.

The third arm is why the first two are evidence. A compile-only probe would
false-green here: emit and serialize_target are fixed to Medium<String>, and
v1.04_infer explicit_return_conformance_note records that declared-return
conformance is judged only by the ground-kernel-scalar and
ground-element-collection discipline, so a structured carrier mismatch raises
no diagnostic. An entry returning ProcessExit exits 0 SILENTLY, which is
indistinguishable from never running -- the first run of this probe produced
exactly that empty rc=0 and proved nothing. Running the Bool-returning
assertions directly forces gunbc to print the value it got, and the
nonexistent-function control proves the harness reaches this file at all.

CliSurface and CliArgument are sole_constructor with NO exported mint.
TransportScript needs transport_script_seal because production modules must
build one; nothing outside this module has business constructing a CLI
argument, because an argument is a RESULT of the grammar fold, never an
authored value. So there is no admit_callers list to add a name to.

WHAT THIS DOES NOT YET PROVE, stated rather than implied: this is the CARRIER
half (the join), not the SEAM half. emit_cli_probe binding translate's output
to this serializer is not built, corpus-wide text byte-identity is not
measured, the TargetSurfaceSerializerUnwired refusal is declared but not
exercised, and no probe yet proves CliSurface itself is sealed -- dropping the
keyword would red nothing today. The five sole_constructor controls in
gunbc.guarantee_probe_corpus prove the LANGUAGE FEATURE against a fixture; what
is owed is one probe that THIS type uses it.

Design: docs/plans/cli-invocation-emission-design.md

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@gunbai-bot gunbai-bot Bot changed the title CLI invocation emission design note: the tree is the authority, argv is emitted (design-note-first, no code) CLI invocation emission: design note + Wave 0 carrier probe (argument boundaries survive the grammar fold, proven by execution) Aug 18, 2026
gunbc-ci-auto-heal and others added 10 commits August 19, 2026 00:04
… backwards

Review found target_surface_serializer_unwired_diagnostic and
cli_surface_argument_count had zero callers. Deleted rather than wired or
deferred: no consumer exists, wiring would mean inventing one, and deferring
leaves specification-without-execution in the tree with a promise attached.
Model just-in-time -- the refusal arm arrives with the code that can reach it.
The irony is recorded because it is the point: TargetSurfaceSerializerUnwired
existed so a missing serializer could not silently fall back to text, and it
landed unwired, which is exactly as inert as the fallback it was meant to
prevent. Confirmed inert by execution, not by inspection: both probe
assertions still return true after the deletion.

The larger correction is to the carrier comment. It claimed this seal was
STRONGER than TransportScript because there is no exported mint and therefore
no admit_callers roster to add a name to. That is backwards.
bound_tokens_cli_arguments is public and takes tokens, lex rules and binding
spellings from its CALLER, so any module can synthesize arbitrary content and
receive a sealed CliSurface. You cannot author the record; you can author its
contents. That is the mint-function hole gunbc.guarantee_probe_corpus already
enumerates as sole_ctor_mint_fn_hole_probe -- read three hours earlier, cited
as the reason not to re-prove the language feature, then reproduced.

TransportScript's seal is admit_callers-restricted to two named production
decls. This fold admits everyone. So the carrier is WEAKER, and the claim was
made, reviewed and corroborated once before anyone checked it.

Not closed in this commit, deliberately. The fix is to stop taking
caller-supplied grammar -- the fold reachable only already bound to a target
model, so the lex table is the target's -- and that shape depends on whether
the jq path consumes translate's target model or bypasses it. An admit_callers
roster now would admit only this probe, which is a wall around an empty room.
Dissolves with the wave that adds the first production consumer.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…tautology

THE THEOREM I HAD BEEN ASSERTING WAS WRONG. Concatenation is not inherently
where CLI structure dies -- concatenation at the WRONG STRUCTURAL LEVEL is.
Within one argument concatenation is exactly right (["--color","=","never"] is
one argument --color=never; ["-","e","r"] is one argument -er). Across
arguments it destroys the boundary. So the algebra is nested, not flat:
fragments join WITHIN an argument, arguments stay separate BETWEEN.

THE OLD WITNESS PROVED A TAUTOLOGY. It supplied two tokens to a
one-token-one-argument fold and asserted two arguments came out, which chose
the argument split before the serializer ran. It established "one token
supplied, one argument retained" -- a restatement of the fold's own shape --
not "the grammar groups fragments into arguments". An approving review read it
as a positive claim plus a negative control, which is how a self-fulfilling
test passes for evidence.

THE NEW WITNESS CAN FAIL. Same three fragments, two groupings, executed:
  joined_fragments_render_one_argument        returned true   ["--color=never"]
  separated_fragments_render_three_arguments  returned true   ["--color","=","never"]
  both_groupings_flatten_to_the_same_text     returned true   "--color=never"
The third is the keystone: both groupings flatten to IDENTICAL text, so the
text carrier cannot distinguish them at all. Grouping is information the argv
carrier holds and text does not -- exactly what the 17 remote jq rows lose at
the ssh seam. Were grouping not load-bearing, arms one and two would agree.
The three function names do not exist in the parent commit, so their resolving
is itself the control that the new file reached the runner.

The inner join reuses bound_tokens_source_text rather than forking a second
concatenation: within an argument, the text fold is the correct tool, and
DESIGN section 2 says model once and derive.

ALSO CORRECTED: the comment claiming this "consumes what translate already
produced" was false -- the witness hand-constructs its tokens and nothing here
calls translate. It consumes the same ConcreteSyntaxToken representation the
existing target serializers use, which is the true and still-useful claim. And
probe_verdict() -> ProcessExit is DELETED: it exits 0 silently on success, the
exact false-green that made this probe's first run report nothing while
appearing to pass, and leaving that shape beside the corrected evidence is how
the trap gets re-sprung.

STILL OWED, unchanged: the mint hole. serialize_cli_arguments still takes
caller-supplied lex rules, so arbitrary content can still reach a sealed
CliSurface. The fix is to seal the INPUT (AdmittedCliInvocation) rather than
admit_callers the serializer, because listing every tool centrally would make
adding a tool a core edit -- anyone may call the serializer, nobody may forge
what it consumes. That needs the schema layer and lands with the first
consumer. Also owed: exact-type REDs against CliArgument/CliSurface
themselves, and tool: CliToolRef so tool identity stops being ambient.

Jq will NOT route through translate or TargetModel; emit_cli_probe is not to be
built. The surviving seam is the spelling algebra below them, which is the part
this wave actually found.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ared CLI surface

The domain module now states WHAT it wants of jq -- a program, an input, an output
encoding, an exit policy -- and the argv vector is derived from that, rather than being
the authority. Two-level derivation, so both defect classes are closed at their own
level: semantic property -> option identity (JqCliSelection) prevents OMISSION, and
option identity -> canonical spelling (bare name + cli_long_option_spelling) prevents
bespoke SPELLING. jq_option_long_name returns "raw-output", never "--raw-output": the
dashes belong to the grammar, not to the option's identity.

JqCliSelection is a coproduct rather than an Optional because "no option is required for
this semantic property" and "this property has no answer" are different states, and the
lane exists to stop collapsing exactly that kind of distinction.

The lowering REFUSES the axes with no live consumer yet -- bindings (the --argjson
vertical, landing with ObjectMapperServiceAt) and file input (the remote population) --
as typed, located refusals rather than a plausible guess.

Executed, on the real acceptance path (all nine return true; a nonexistent-function
control refuses with NoSuchFunction, so a silent no-run cannot read as a pass):
  W0  joined_fragments_render_one_argument
  W0  separated_fragments_render_three_arguments
  W0  both_groupings_flatten_to_the_same_text
  W0  keystone_flat_text_is_nonempty
  W1A sensor_invocation_lowers_to_exact_argv
  W1A stdin_content_is_absent_from_argv
  W1A exit_policy_perturbation_adds_the_exit_status_option
  W1A unlowered_bindings_refuse
  W1A unlowered_file_input_refuses

Three defects found and fixed getting there, each recorded rather than quietly patched:
a source annotation placed inside a declaration body (DESIGN 4c admits module-item grain
only); three stale call sites left when the Optional-returning selectors became
JqCliSelection; and a type mismatch at the stdin field, bisected remotely to
Present { value: ... } with the payload expression irrelevant -- a bound variable, a
renamed binding, a shorthand pattern and a bare literal all reproduce it while Absent
resolves. This uses the corpus's own String? sugar (625 existing optional fields). That
observation is recorded as MEASURED AND NOT DIAGNOSED in the design note, with a section
5 line-stop owed before anything in this lane relies on the distinction.

Nothing is cut over yet: no consumer is rewired and no transport argv is deleted. This
is the semantic layer plus its discriminating evidence, not the replacement.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…eal is on shape, not provenance

Section 9's table claimed forging a CliSurface is "structurally impossible now -- only the
row emitter, serializer and decoder may mint". That is false, and it is the exact failure
DESIGN 4b calls worse than sitting low: a carrier named for the top rung while occupying a
lower one, asserted here about this document's own subject.

sole_constructor closes the record literal and the cast. It says nothing about a public fold
taking caller-supplied inputs, and serialize_cli_arguments is precisely that -- public, and
accepting caller-supplied lex rules and fragments, so any module can obtain a well-typed
CliSurface carrying arbitrary text. The earlier claim in this lane that CliSurface was
therefore STRONGER than TransportScript had the comparison backwards: TransportScript's mint
is admit_callers-sealed to two named production declarations; CliSurface's is not sealed at
all.

The row is split, because one number for two populations was the error:
  forging by record literal or cast  -> structurally impossible (mechanism witnessed by the
                                       existing corpus sole-constructor-cross-module probes,
                                       deliberately not re-proved here -- that would be a
                                       second representation of one guarantee)
  minting content not derived from rows -> mitigatable only, no wall

Ceiling and trigger are now stated rather than implied. admit_callers on the serializer is
REFUSED on section 3 grounds: it would make v2.std.compilers.cli_surface name every tool
module that may emit a CLI, fusing dispatch into the interface -- the thing this lane exists
to keep peripheral. The wall belongs on the INPUT: a sealed AdmittedCliInvocation only a
tool's own row-derived lowering can produce. That is not built, and its mint's design is
genuinely open, since whatever seals it faces the same recursion one level up. Recorded as
open rather than improvised, since a fake wall here would be the inflation again.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…h had a trigger that could not close it

Surfaced by an approving review quoting the header back: it described the dissolve-on as
"first production consumer choosing the target-model path". Both halves of that were stale.

1. STALE SYMBOL. The note named the mint bound_tokens_cli_arguments, which no longer exists;
   it is serialize_cli_arguments. This is exactly the section 3 class -- a name-level claim a
   grep decides, sitting false in the file a reviewer reads to judge the seal.

2. AN ANSWERED QUESTION STILL BEING DEFERRED TO, and this is the substantive half. The note
   said the repair's shape "is decided by whether the jq path consumes translate's target model
   or bypasses it entirely". Wave 1A answered it by execution: jq BYPASSES it. The lowering
   builds CliArgumentSyntax from its own rows and never constructs a TargetModel, so "bind the
   fold to a target model so the lex table is the target's" is not merely undone -- it is
   unavailable, there being no target model on this path.

   The old trigger was therefore worse than vague: "the wave that adds the first production
   consumer" would have FIRED without closing the hole, retiring the obligation while the
   unrestricted mint stayed open.

The corrected repair is to seal the INPUT, not the fold: a sealed AdmittedCliInvocation only a
tool's own row-derived lowering can produce. admit_callers on the serializer stays refused on
section 3 grounds -- not because the roster would be short, but because it would make this std
module name every tool permitted to emit a CLI, fusing dispatch into the interface. The
dissolve-on is now that carrier, and provenance is stated as sitting at mitigatable meanwhile.

Verified still resolving after the edit (annotations are parsed, so a comment edit can break
the module): five representative Wave 0 and Wave 1A assertions re-run, all return true.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…corrected decomposition

The static-dependency finding stands. At execution grain the jq fold reaches no compiler
machinery; at dependency grain cli_surface imports target_model, whose closure carries
target-representation, host-runtime and node-query machinery. The property worth having is
not "nobody calls translate" but "this fold cannot acquire that dependency accidentally".

THE OBVIOUS REPAIR IS FORBIDDEN BY A RULING IN THE FILE IT WOULD EDIT. Extracting a shared
spell_concrete_syntax_fragments -> Outcome<String> and having the TargetText serializer wrap
its result is a String -> TargetText lift of an ALREADY-COMPOSED unit. target_model
target_text_carrier_scaffold_note (operator, 2026-07-15) places TargetText beside
bound_tokens_source_text precisely so that fold is carrier-native: the single String->carrier
introduction is text_atom applied to ONE grammar-classified token INSIDE the fold, the only
join is target_text_seq, the only exit is render_target_text, and it states there is
deliberately NO lift of a composed unit -- "that direction is the smuggle the wall closes."
I was one edit from dismantling a declared wall on a load-bearing file.

THE CORRECTED DECOMPOSITION IS BETTER ANYWAY. The shared authority is WHAT IS THIS TOKEN'S
SPELLING -- lex_rules_literal_for_class and bound_spelling_from_map, both token-grain -- not
HOW ARE SPELLINGS CONCATENATED. Concatenation is carrier-specific by construction: emitted
source composes through TargetText, an argv argument composes into a CliArgument, different
media. So the move is the token type plus the two token-grain lookups into
v2.std.compilers.concrete_syntax, with target_model importing them back and each carrier
keeping its own fold. No composed String is ever lifted, cli_surface stops importing
target_model, and one lookup authority still serves both.

RE-EXPORT IS MEASURED, NOT ASSUMED. A three-module probe showed a consumer importing a symbol
from a module that merely imported it resolves and executes. That alone proves nothing: this
resolver can bind by pool-membership coincidence (DESIGN Class B). The discriminating control
settles it -- importing the same symbol from a bystander module that never saw it REFUSES,
located, with the defining module still in the pool. Resolution is import-list-driven, so
target_model importing the seam back leaves its 167 other importers untouched.

NOT PERFORMED HERE. target_model is load-bearing and carries the ruling above, so the move is
its own increment under its own review rather than a rider on this one.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…specimen

extdeps.tools.jq jq_option_canonical_spelling calls cli_long_option_spelling while the module's
import list named only CliArgumentSyntax, CliSurface and serialize_cli_arguments. The call
resolved anyway -- and all nine Wave 1A assertions passed -- because cli_surface was already in
the assembled closure via those three imports. Found by review, not by any control I had.

That is the Class B accidental coverage DESIGN's import-strip thread records as blocking all
further dag/** import stripping: the binding came from pool membership, not from the
bare-reference closure.

Note which control does NOT catch it, since I ran one an hour earlier and it proved a
neighbouring property. The bystander probe refuses a QUALIFIED import of a name a module does
not export. This is an UNIMPORTED BARE REFERENCE into a module present for other reasons.
Different mechanism, and only the second is silent.

Swept all four files of this lane rather than fixing the reported site alone: this was the only
real hit. concat is a registered host builtin (target_model does not import it either) and
`then` was a false positive from inside a jq program string literal.

Verified after the fix: five Wave 1A assertions re-run, all return true.

THE GENERAL DEFECT IS UNTOUCHED and is not this lane's to fix -- nothing refuses the next such
reference. The durable lesson is recorded in the design note: a green witness is not evidence
that a module's imports are complete.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
All four raised by side-chat review of Wave 1A. Each was real; the notable part is that three
were invisible to a green assertion set.

1. THE FOLD WAS FAIL-OPEN ON A PATH TO Command::new. target_model bound_spelling_from_map
   answers an absent map entry with the binding SYMBOL'S OWN NAME rather than refusing.
   Defensible for compiler source text, where the symbol name is a legitimate rendering; for
   runtime CLI data it means a missing jq_program_text binding emits the literal argument
   "jq_program_text" -- fabricated plausible output (DESIGN section 5) that a process then runs.
   cli_surface now has its own CliArgument-native fold with required_bound_spelling, which
   refuses, typed and located.

   This also satisfies the carrier ruling rather than fighting it: the shared authority is
   TOKEN-GRAIN SPELLING, not sequence composition, so emitted source keeps composing through
   TargetText via text_atom/target_text_seq while an argv argument composes here, and no
   already-composed String is lifted into either carrier.

   PROVEN DISCRIMINATING, not assumed: a_bound_fragment_with_no_spelling_refuses returns true
   with the refusing fold and FALSE when the fallback is restored. Executed both ways.

2. THE PUBLIC RESULT DROPPED STDIN. jq_invocation_cli_arguments projected plan.arguments and
   discarded plan.stdin, so a jq program's input vanished at the module boundary. The witness
   could not catch it: "stdin does not appear in argv" is satisfied just as well by stdin being
   lost entirely -- a negative control that coexists with total loss is not evidence of routing.
   Adds sealed JqAdmittedProcessPlan { tool, surface, stdin } with both halves asserted, and it
   gives tool identity its first consumer so which binary runs stops being ambient.

3. THE REFUSAL CAUSE WAS ERASED. JqLoweringRefused carried a NonEmptyStr reason that
   jq_lowering_refused_diagnostic never read, collapsing both unlowered axes onto one identity
   while the witnesses asserted only a generic Rejected. Typed JqLoweringRefusal now projects
   distinct identities, asserted by three new witnesses.

4. The unlisted bare import fixed in the previous commit.

Fifteen assertions execute, all true. Deliberately NOT added: arity, repeatability and joining
discipline have no consumer. Placement does (jq_option_arguments orders options before the
program operand), but it belongs encoded structurally as options/operands on the future
AdmittedCliInvocation, not as a per-option enum on every row.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
jq_invocation_process_plan became the complete result in the previous commit, which made three
statements stale in the same motion: jq.dag's header, cli_surface's containment sentence, and
section 9 of the design note all said jq_invocation_cli_arguments was the single public entry.

The argv-only projection stays beside it, because the boundary witness asserts over it directly.
What is now written down is why a handler must NOT take it: recovering stdin would mean reopening
the JqInvocation, which gives the process projection two authorities -- the thing the sealed plan
exists to prevent.

This is the fourth stale-claim fix in this lane and they share one shape: the mechanism changed
and the sentence describing it did not. Verified after the edit, since annotations are parsed and
a comment change can break a module.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…669)

jq_invocation_process_plan used bind_outcome and outcome_accepted with neither in the module's
v2.std.diagnostic import list. The finding is correct and is fixed here.

THE REVIEW'S STATED CONSEQUENCE IS NOT CORRECT, and the difference matters more than the fix.
It said "as written this file will not resolve". The file resolves, and
stdin_survives_lowering_into_the_process_plan executes green THROUGH the affected function,
because v2.std.diagnostic is already in the closure via other imports. A reviewer predicting a
resolution failure would be refuted by running it and might then discard a real finding as a
false positive. The accurate statement: the references bind by pool membership, and nothing in
the tree reports it -- not the resolver, not CI, not a green witness.

THIS IS THE SECOND OCCURRENCE IN THIS LANE, in code written AFTER the class was documented two
commits ago. The cause is procedural and worth recording: the unimported-reference sweep had
been run and was clean, then jq_invocation_process_plan was added and the sweep was not re-run.
A one-time audit cannot close a class whose defect is invisible by construction; the sweep
belongs after every addition. Re-run across all four files of the lane, now clean (concat is a
registered host builtin; `then` is a false positive from inside a jq program string literal).

Six assertions re-run after the fix, all true.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Aug 19, 2026

Copy link
Copy Markdown
Contributor Author

review 53669 — finding confirmed and fixed in 17560cbf386. bind_outcome and outcome_accepted were used in jq_invocation_process_plan with neither in the module's v2.std.diagnostic import list. Both are now named.

One correction, because it changes what the next reader should conclude. The review states "as written this file will not resolve." It does resolve. stdin_survives_lowering_into_the_process_plan executes green through the affected function — verified before and after the fix — because v2.std.diagnostic is already in the assembled closure via other imports.

That matters practically: a reviewer who predicts a resolution failure would be refuted by simply running it, and might then discard a real finding as a false positive. The accurate statement is that the references bind by pool membership rather than through the import edge, and nothing in the tree reports it — not the resolver, not CI, not a green witness. This is the accidental-coverage mechanism DESIGN's import-strip thread records as blocking further dag/** import stripping.

This is the second occurrence in this lane, in code I wrote after documenting the class. The cause is procedural and recorded in the design note: I ran an unimported-reference sweep, it came back clean, then I added jq_invocation_process_plan and did not re-run it. A one-time audit cannot close a class whose defect is invisible by construction. The sweep now runs after every addition and is clean across all four files (concat is a registered host builtin, which is why target_model does not import it either; then is a false positive from inside a jq program string literal).

Merge readiness, unchanged by this fix: the approval tally is ten from a single provider (claude) against the ≥2-distinct-provider floor, so the bar is not met regardless of this REQUEST_CHANGES clearing. Not merging.

Also worth stating plainly for anyone reading the tally rather than the diff: nothing consumes this code yet. Zero production consumers; all 28 raw jq argv sites remain live. The next PR is the SensorIntegerValue cutover with the old transport shell { argv } deleted in the same commit, which is what takes the displacement numerator off zero.

— sent from sharp-ant-396

gunbc-ci-auto-heal and others added 3 commits August 19, 2026 04:30
…review)

Verified before removing, since "unused" is a claim about the whole tree:

  jq_option_for_binding      1 reference -- its own definition. Dead.
  JqCliOptionArgJson         reachable ONLY from that dead function, plus exhaustive match
  JqCliOptionArg             arms and lex rows for options nothing can select.
  jq_option_short_name       no consumer.
  cli_short_option_spelling  no consumer.

The binding-option rows are the interesting ones. jq_invocation_lower REFUSES any non-empty
bindings, so nothing could ever select them: a typed refusal already stood where those rows
implied a capability. Keeping them would have been a second answer to a question the refusal
already answers -- and they return with the --argjson vertical that earns them.

The long-option renderer's comment now says why only the long form is modeled: POSIX guideline
3 is cited in the design note, but a citation is not a consumer, and a rule nothing calls cannot
be shown to be right.

This is the third appearance of this class in this lane. Review caught two unwired declarations
earlier, I deleted them and wrote down the principle, and then authored five more. Stating the
principle has not prevented violating it; the mechanical sweep is what catches it, and it now
runs after every addition rather than once.

It also matters beyond tidiness. Unconsumed rows in a replacement Y are how a migration
accumulates authority before it removes any (DESIGN section 3), and this lane's displacement
numerator is still 0 of 28.

Fifteen assertions re-run after the deletions: 15 true, 0 false. The exhaustive-match arms were
the plausible breakage and did not break.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ted argument lists

A List<String> built by folding is CONCATENATED into one argv word. The identical list written
as a literal is SPLICED. Same declared type, same elements, same handler, two different
processes.

RECEIPT, through a real jq handler:

  arguments = ["--raw-output", "."]        literal  -> exit 0   (jq ran; two argv words)
  arguments = fold_list(... same two ...)  folded   -> exit 2
      jq: Unknown option --raw-output.

and from the first wet run of the real vertical, three lowered arguments arriving as one:

  $ jq --raw-output--exit-status.missing   (exit=2)

MECHANISM. v1_interpreter.rs push_shell_argv_tokens: Value::List splices each item, but
Value::Variant tries value_as_host_string FIRST, which walks a free monoid and concatenates it
into a single String pushed as one argv word; only on None does it fall through to
free_monoid_to_vec and splice. A folded list is monoid-encoded with all-Str elements, so the
concatenating reader wins. gunbc.WitnessBin.Run escapes this only because its args is authored
as a literal at each call site.

INDEPENDENTLY ATTACKED. An outside reviewer tried to refute it and failed: the source matches
the reading, and the collapse happens BEFORE Command::args, ruling out a downstream shell or
SSH join. Three confirmations from different directions.

NEITHER OBVIOUS REPAIR IS CORRECT. Reordering the arms splices this case but SHREDS a modeled
String, because a String is itself a monoid here -- both readings succeed on a monoid of Str,
and the runtime cannot separate "list of arguments" from "string assembled from pieces". The
disambiguator is the declared type, erased at that seam: the same missing application-argument
typechecking target_text_carrier_scaffold_note names as the trigger for every type-based
construction guarantee at a call boundary. Hand-authoring literal argv in the handler defeats
row-derived lowering and leaves the next caller silently joined -- the workaround shape section
5 treats as a line-stop.

WHY NO CODE LANDS WITH THIS. The recut's handler, JqProcessInput, JqProcessObservation and
sealed-plan executor are built and resolve, but they are unconsumed AND blocked: no consumer can
migrate onto them without silently destroying argument boundaries. Landing them would bank
exactly the unconsumed replacement surface this lane has spent the day deleting. They are held
out of tree until the blocker is decided.

THE IRONY IS THE POINT. This lane exists because argv arrays weld argument boundaries into
opaque strings. The substrate's own argv transport does that, silently, one layer below --
Wave 0's witness asserts fragments concatenate WITHIN an argument and never ACROSS, and the
transport violates precisely that assertion.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ocked on argument typechecking

The previous commit's DIAGNOSIS survived independent adversarial review -- the reviewer traced
build_service_param_env (clones call arguments, no conformance check), dispatch_shell, and
Command::new(&argv[0]).args(&argv[1..]), confirming the vector is malformed before Command sees
it, so no downstream join can explain the observation. The refusal to reorder the branches was
upheld for the reason given.

ITS CONCLUSION WAS WRONG. I wrote that neither obvious repair is correct and the cut is blocked
pending application-argument typechecking. There is a third repair, and the counter-evidence is
already in tree: OperationInputValue = InputText | InputTextList carries tagged list intent, and
its realization converts that tag into a native Value::List via free_monoid_to_vec + list_value.
Tagged intent to native list is proven possible today without global typechecking.

The deeper correction is the one I missed. Even fully typechecked, List<String> still does not
say whether a collection becomes several argv words, one JSON argument, a comma-joined option
value, or repeated option/value groups. That is a TRANSPORT ROLE, not a data type. The missing
fact must be modeled, not inferred from runtime encoding.

The construction: a sealed ShellArgvExpansion { surface: CliSurface } plus an interpreter branch
ahead of the generic heuristic that requires the nominal CliSurface, iterates its arguments, and
pushes exactly one host word per CliArgument. It carries CliSurface rather than List<String> so
the payload cannot be dynamically ambiguous -- a modeled string cannot impersonate a list of
nominal CliArgument records -- and value_as_host_string is then applied only to one admitted
argument's text, where concatenation is correct. Wave 0's theorem enforced at the host edge.

Also recorded: the six repairs that must NOT land, each with its reason, including accepting both
a raw List<String> and the explicit carrier -- two authorities with the unsafe one still reachable.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… make the exit code decodable

Deletes openbmc.JsonProjection.SensorIntegerValue -- transport argv, `success: Bool`
output and all -- and routes its two consumers through one shared function that states
what it wants extracted and never spells a flag, an option, an argument position or
argv[0]. The domain authors zero argv after this cut.

Carrier, at the host edge:

  ProcessArgvExpansion { surface: CliSurface }   sole_constructor

with the seed realization in v1_interpreter. It exists because a computed argument
vector was losing its argument boundaries: a folded List<String> is monoid-encoded, and
push_shell_argv_tokens tries value_as_host_string (which walks the monoid and
CONCATENATES) before free_monoid_to_vec (which splices), so a correctly-lowered
three-argument vector reached a real process as `jq --raw-output--exit-status.missing`,
exit 2. Literal lists escape only because they keep their native representation. The
carrier states the transport ROLE that List<String> cannot: iterate across arguments,
concatenate within one. Empty arguments are preserved (dropping one changes arity) and
an embedded NUL refuses with the argv position named, rather than reaching spawn as an
errno-shaped error naming neither.

Named ProcessArgvExpansion, not Shell: the realization is
Command::new(&argv[0]).args(&argv[1..]) -- no shell, no word splitting, no quoting
layer. Naming it for the `transport shell` keyword would name it after the surface DSL
rather than the boundary (S3).

The exit code now travels with its contract. JqAdmittedProcessPlan carries exit_policy
and jq_classify_observation is the only reader of an exit code, returning
Present | Absent | Refused. The sensor decoder previously mapped every nonzero exit to a
refusal -- correct under JqProgramExit, silently wrong under JqLastResultExit, where jq
documents exit 1 as a false-or-null last output (a value) and exit 4 as absence.
Changing the policy would have left the decoder answering the old contract: the
declaration edited while the realization goes on lying (S5).

Executed evidence:

  bmc_typed_operations         29/29   (2 migrated onto the typed outcome, 1 newly stateable)
  jq_invocation_lowering        9/9    lowering
                                5/5    exit-policy classification, incl. the row a
                                       policy-blind decoder cannot satisfy: exit 1 is a
                                       refusal under one policy and a value under the other
  bmc_fan_converge              duty_curve pass
  process_argv_expansion_receipt PASS  real jq, exit 0 reachable only with two argv words

Not claimed: the splice defect is repaired at ONE seam, not closed as a class -- 21
operations still splice a declared List through the guessing path. The remaining
JsonProjection operations are unmigrated and two need --argjson lowering, which is
unbuilt. No negative falsifier yet proves a REST path reaches none of these carriers.
The domain still authors one jq program row (design note S12: mitigatable, no wall,
dissolution trigger recorded -- the terminal shape is a modeled JSON projection of which
jq is one realization).

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Aug 19, 2026

Copy link
Copy Markdown
Contributor Author

Reworked against the shell → dag architectural verdict. The PR is no longer a carrier without a consumer — it now deletes a live argv site and rewires it.

What landed since the reviewed head (+1,979/−1):

  • openbmc.JsonProjection.SensorIntegerValue is deleted — transport argv, success: Bool output and all. Its two consumers route through one shared function. The domain authors zero argv after this cut: no -r, no --raw-output, no argument position, no argv[0].
  • ShellArgvExpansion → ProcessArgvExpansion, renamed before it spread. Verified against the seed: the realization is Command::new(&argv[0]).args(&argv[1..]) — no shell, no word splitting, no quoting layer. Naming it for the transport shell keyword would have named it after the surface DSL rather than the boundary.
  • Empty arguments preserved (dropping one changes arity); embedded NUL now refuses naming the argv position, instead of reaching spawn as an errno-shaped error naming neither the argument nor the surface.
  • The exit code now travels with its contract. The sensor decoder mapped every nonzero exit to a refusal — correct under JqProgramExit, silently wrong under JqLastResultExit, where jq documents exit 1 as a false-or-null last output (a value) and exit 4 as absence. Editing the policy would have left the decoder answering the old contract. JqAdmittedProcessPlan carries exit_policy; jq_classify_observation is the only exit-code reader; the domain matches Present | Absent | Refused.

Executed evidence (functions enumerated from each file, not hand-picked):

bmc_typed_operations           29/29   2 migrated onto the typed outcome, 1 newly stateable
jq_invocation_lowering          9/9    lowering
                                5/5    exit-policy classification
bmc_fan_converge                duty_curve pass
process_argv_expansion_receipt  PASS   real jq, exit 0 reachable only with two argv words

The discriminating row: exit 1 with stdout false is a refusal under one policy and a value under the other. A policy-blind decoder cannot satisfy both.

Not claimed. The splice defect is repaired at one seam, not closed as a class — 21 operations still splice a declared List through the guessing path. The other JsonProjection operations are unmigrated; two need --argjson lowering, which is unbuilt. No negative falsifier yet proves a REST path reaches none of these carriers. The domain still authors one jq program row — recorded at mitigatable, no wall, with the terminal shape named (a modeled JSON projection of which jq is one realization).

On the verdict item I declined: "handler privately selects a sealed program identity" relocates the jq source behind an indirection plus a registry rather than decomposing it — handler in OpenBMC leaves the text in OpenBMC; handler in jq means extdeps.tools.jq knows what a BMC sensor is. Reasoning in design note §12.

Also worth flagging against myself: I broke two enrolled witnesses and did not find them, because I had selected which witnesses to run by hand-picking from the importers of the changed file. The mechanism was fine; the denominator was authored. Recorded as §14, and verification now enumerates test functions from the file.

— sent from sharp-ant-396

gunbc-ci-auto-heal and others added 5 commits August 19, 2026 08:51
…ut_policy and red a file this branch never touched

CI caught what every local run missed. The jq witness declared

  type ExpectedOutcome = ExpectPresent | ExpectAbsent | ExpectRefused

and gunbc.output_policy already declares that name (ExpectSuccess | ExpectFailure |
OutcomeIsData) -- the carrier the interpreter's expectation frontier consumes. The second
declaration did not shadow the first; it made the PRE-EXISTING bare reference in
dag/test/claim/output_policy_witness_test.dag:92 unresolvable, so the failure landed in a
file that references none of this branch's symbols and that this branch never modified.

Renamed to JqOutcomeExpectation, with the reason recorded on the declaration so it does
not get renamed back.

WHY NO LOCAL RUN CAUGHT IT: bare-reference resolution is corpus-global, but a per-file
`gunbc run` loads only that file's closure, so a new top-level name can red a file no
closure of mine would ever load. A per-file run and the required floor are different
universes and only the floor is the acceptance path -- reporting the first as though it
were the second is rung inflation against a declared boundary (S4b), which the design
note states as a rule about other people's claims and which I then committed against my
own change.

Two mechanical checks adopted, recorded in the note (S14), because the hand-authored
version of this has now failed three times in this lane -- each time with a sound
mechanism and an AUTHORED denominator:

  # every top-level name the branch ADDS, taken from the diff, not from memory
  git diff main...HEAD -- '*.dag' | grep "^+" \
    | grep -oE "^\+\s*(type|fn|data)\s+[A-Za-z_][A-Za-z0-9_]*" | awk '{print $NF}' | sort -u
  # each must have exactly ONE declaration corpus-wide

  # and run what CI runs, before pushing
  claim_executor --required-floor --source-root dag --source-root src/v2

The first check now reports zero collisions across all 82 names this branch adds.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…, enrolled as a wet entry

The floor ran 9201 witnesses with one failure, and it was this receipt:

  FAIL test.manual.process_argv_expansion_receipt.case4_expansion_carrier_splices
    hermetic mode: no mock_response for operation RunWithStdin -- refusing to fabricate Unit

The refusal is correct. case4 dispatches a real jq, the hermetic envelope has no mock
for that operation, and it refuses rather than skipping -- one refusing member fails the
run.

MOCKING IS NOT THE REPAIR, for the reason gunbc.ci_layer_roots already records against
the stage0 rows: this witness's entire content is that a real jq exits 0 only when it
receives TWO argv words instead of one concatenated word. A mocked RunWithStdin lets it
pass with no process running -- a green that cannot fail, asserting nothing about the
boundary defect it exists to detect. That approach was tried and reverted elsewhere in
the corpus; this row does not retry it.

TWO ROWS, because they answer different questions (DESIGN 'witness cost derives from
purpose', operator ruling 2026-08-04):

  WitnessExclusionRow          keeps it off a hermetic batch it cannot pass
  bin_witness_wet_entries      gives it an executing consumer

Exclusion alone would be deletion of the evidence with the source file retained, which
is the exact specimen that ruling was written from. Both rows land together.

Path decided nothing: the file sits under dag/test/manual/ and was swept into unshrunk
discovery anyway -- the same ruling's point that a directory cannot answer an admission
question.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Caught before CI ran it, by reading the reconciliation witness the roster answers to
rather than copying the shape of a neighbouring row.

The two classifications are not interchangeable labels; they project different claims:

  BinWitnessWet      -> SchedulingEnrolled
  OfflineLocalRecipe -> SchedulingDark

This receipt IS enrolled in bin_witness_wet_entries and does run per-PR, so the offline
label would have declared a running witness dark -- understating its own coverage in the
carrier whose entire job is to report coverage honestly. It is also the arm DESIGN's
witness-cost ruling retired: a broad offline path verdict accepted unconditionally is
precisely the admission defect that ruling was written from, and I reached for it while
quoting that same ruling one commit earlier.

BinWitnessWet is additionally the arm held to account -- the reconciliation witness reds
an unbacked BinWitnessWet row, and this one is backed by the entry it names.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
# Conflicts:
#	dag/gunbc/ci_layer_roots.dag
…ults, and declare the coverage gap

The previous fix did not work and the CI receipt says why: modules_excluded stayed at 2
and the same witness failed identically. run_required_floor calls
prepare_repository_once(source_roots, &floor_prepared_subject_exclusions()) -- a
hardcoded Rust list, which is exactly those 2 entries -- and consults nothing else. The
rows I added to gunbc.ci_layer_roots were inert:

  witness_exclusion_frontier   feeds witness_admission_* paths, not the floor
  bin_witness_wet_entries      feeds wet batches that died with the floor cut

Both are reverted. A row in a roster with no live consumer is
specification-without-execution, and I had additionally asserted in a commit message that
they would take effect -- a claim about a mechanism whose caller I never traced. The
BinWitnessWet reclassification was the same error compounded: the one host projection
that does read those rows filters on OfflineLocalRecipe, so "correcting" the
classification moved the row further from the only consumer it had.

The file is now named in floor_prepared_subject_exclusions, beside the existing
test/manual/ precedent.

WHAT THIS BUYS AND WHAT IT DOES NOT. It buys a green floor. It does not buy coverage:
there is no wet lane in CI at all -- the falsifier and wet batches were deleted with the
floor cut, and v2.workflow.required_floor defers wet lanes until the question can be
"asked against a live consumer". So the claim is recorded as UNEXECUTED-IN-CI with its
local recipe and a re-enrollment trigger, not dressed up as an enrollment. Declaring a
counted gap is the honest rung; claiming an executing consumer for a witness nothing runs
would be the inflation DESIGN 4b names as worse than sitting low.

Mocking remains refused: case4 exists to prove a real jq exits 0 only on two argv words,
and a mocked dispatch passes it with no process running.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Aug 19, 2026

Copy link
Copy Markdown
Contributor Author

CI green at 5ea765c2e64.

required-floor: modules_resolved=3701 modules_excluded=3
required-floor: planned=9200 executed=9200 terminal=9200
                passed=8894 known_red_held=306 failed=0

modules_excluded moving 2 → 3 is the specific confirmation the two prior attempts never got. Both of those edited gunbc.ci_layer_roots rosters — witness_exclusion_frontier and bin_witness_wet_entries — and both times the receipt came back with an unchanged modules_excluded=2 and an identical failure. run_required_floor calls prepare_repository_once(source_roots, &floor_prepared_subject_exclusions()) and consults nothing else; those rosters feed other paths and wet batches that died with the floor cut. The rows were inert, and I had asserted in a commit message that they would take effect without tracing the mechanism’s caller. Both reverted rather than left standing.

What the exclusion buys, precisely: a green floor. Not coverage. There is no wet lane in CI — v2.workflow.required_floor defers wet lanes until the question can be "asked against a live consumer" — so the receipt is recorded as UNEXECUTED-IN-CI with its local recipe and a re-enrolment trigger, not dressed up as an enrolment. Mocking stays refused: case4 exists to prove a real jq exits 0 only on two argv words, and a mocked dispatch passes it with no process running.

Merge state: MERGEABLE, no REQUEST_CHANGES, checks green. The one outstanding requirement is a second distinct approval provider — 16 approvals are all from claude, so the tally reads 1/2 and more runs from the same provider will not move it. Nothing further from me on this PR.

— sent from sharp-ant-396

@briansrls
briansrls merged commit 073bbd4 into main Aug 19, 2026
1 check passed
@briansrls
briansrls deleted the session/sharp-ant-396 branch August 19, 2026 16:44
gunbai-bot Bot pushed a commit that referenced this pull request Aug 19, 2026
…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>
briansrls pushed a commit that referenced this pull request Aug 19, 2026
… 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>
gunbai-bot Bot pushed a commit that referenced this pull request Aug 19, 2026
…merge resolution had dropped from cli_run.rs

The floor refused at strict-preparation with 49 errors across 8 files, every one
of them in the region the fifth integration had just rewritten. They resolve
into two causes, and only the first is about names.

REPOINTING ERRORS (my cut, 32 of the 49). Six names were qualified to a module
that does not declare them -- the repointer prefers the longest shared namespace
prefix, which picks a plausible neighbour when the declaring module is not the
obvious one:

  Present/Absent          -> v2.std.collection    (declared in v2.std.optional;
                             the corpus norm is BARE, 5929 and 3914 sites, so
                             these revert to bare rather than move)
  HealthzEffectiveRead    -> gunbc.live_deploy.readiness
                             (gunbc.roadmap_site_surface_types)
  srv1_live_dashboard_instance -> gunbc.roadmap_belt_actuate
                             (gunbc.roadmap_dashboard_instance)
  roadmap_site_*_url_path -> gunbc.roadmap_static_site
                             (gunbc.roadmap_site_surface_render)
  Running                 -> gunbc.roadmap_belt_actuate (gunbc.roadmap_belt)

and four names main authored bare in files this branch had already cut, so
nothing supplied them: Port, GitObjectId, Fnv1a64Structural, LayerImportFact,
RealizationVocabImportEdge, LiveTreeDisposition. The `no field 'std' on type
'String'` class is what a wrong module path looks like once resolution gives up:
`v2` binds as a value and `.std` reads as a field.

A LOCAL FLOOR RUN IS WHAT MADE THIS CHEAP, and it is worth recording because I
had been treating the floor as CI-only: claim_executor --required-floor runs in
this container, reaches strict-preparation in about five minutes, and prints the
same located errors CI does. The turnaround is minutes instead of a 30-minute CI
cycle. strict-preparation now completes with 0 errors, modules_resolved=3707.

THE SECOND CAUSE IS MINE TOO, and it is not a name at all. Past strict-
preparation the floor refused with `no such function:
v2.workflow.required_floor.required_floor_claim_budget_ms`. That function does
not exist on main either -- main replaced it with three independently-read
constants. This branch's .dag already carried main's four functions, because
they arrived by ordinary merge; only cli_run.rs still asked for the old one.

The cause is an earlier integration of mine that resolved cli_run.rs by taking
this branch's side wholesale. Git then records the file as merged, so the
dropped work never reappears in a later conflict -- it is invisible to every
subsequent merge. Three main commits were missing, identified by testing the
tree for a distinctive added line from each rather than by reading the diff:

  5b884d3  #8531  RequiredFloorDisposition + LongHomeStorageAgreement
  4df942c  #8533  BUDGET POLICY CUT
  073bbd4  #8467  CLI invocation emission

All three are re-applied with git apply -3, in main's own order, so the result
is main's change rather than my transcription of it. One conflict, at the two
lines the budget cut exists to fix -- this branch armed both the CPU and wall
clocks from a single figure, which is exactly the fusion #8533 removes -- taken
as main authored it. `pub(crate) mod shared_fill;` is restored beside it; the
module file was on disk the whole time with nothing declaring it.

I considered a full three-way merge of cli_run.rs and rejected it: with the
branch's true fork point as base it reports 51 conflicts, because the branch has
already absorbed five main merges and the ancient base re-litigates all of them.
Three commits identified by content is the smaller and more honest instrument.
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
…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>
gunbai-bot Bot pushed a commit that referenced this pull request Sep 3, 2026
…on, derive the argv (#8467 grain)

The hostnamectl set-hostname vertical's realization was a hand-authored argv row —
`transport shell { argv: ["hostnamectl", "set-hostname", "{desired}"] }` — the exact
defect the CLI-invocation lane exists to remove: the subcommand and the operand were
opaque literals in a transport DSL, so the operation's own flags were hand-typed rather
than derived from cited rows. This is the #8467 grain of the shell->dag census's §5.A
hostname row: the §5.B grain (call a typed op) landed at #7194; the op's *realization*
is what this cut replaces.

The shape mirrors the jq vertical exactly:
- `hostnamectl_set_hostname_verb` is ONE cited row (freedesktop hostnamectl(1)); every
  argv derivation reads it, so a differently-spelled subcommand cannot reach argv.
- `HostnameSetInvocation { desired }` is what a caller describes — no flag, no argv
  position. A DnsLabel keeps the operand inside the hostnamectl-safe grammar.
- The lowering emits a two-argument surface [set-hostname, desired]: the subcommand as a
  FixedToken (spelling owned by the lex table), the operand as a BoundToken (spelling
  carried by the invocation). The executable is the handler's fixed tool name, exactly
  as jq.Process's transport row spells "jq".
- `hostname_set_invocation_process_plan` seals the surface into a sole_constructor plan;
  `hostname_set_execute_plan` runs it through the new `hostnamectl.Process.Run` handler;
  `hostname_set_classify_observation` owns the exit contract (0 = applied, nonzero =
  failed with stderr), so no domain code reads a raw exit code.

os.Hostname.Set is deleted with its transport row (the jq precedent: the semantic op
with hardwired argv is removed, the invocation layer answers its question). The local
leg (`hostname_set_local`) now builds the invocation and executes the sealed plan; the
SSH legs' privileged argv (`sudo -n <path> set-hostname <desired>`) reads the same
cited verb, so the local and remote legs cannot drift. The full-argv projection
`hostname_set_argv` is derived (executable + rendered surface) rather than a second
authority.

Witnesses: a new hermetic lowering witness (hostname_set_invocation_lowering_witness)
asserts the exact surface, the full-argv projection, the bound-operand perturbation,
and the exit contract; the census and host-identity witnesses are repointed onto the
invocation path. The v1 false-refusal rosters and the census ledger note the deletion.

Verified locally: build lane clean (regen first_generation_equal=true,
generated-artifact 36/36 match), witnesses lane clean (FloorClean, 3515 executed,
0 failed), infer_semantics_witness bin runs clean.
gunbai-bot Bot added a commit that referenced this pull request Sep 3, 2026
…on, derive the argv (#8467 grain) (#10211)

* os.Hostname.Set onto the CLI-invocation substrate: model the invocation, derive the argv (#8467 grain)

The hostnamectl set-hostname vertical's realization was a hand-authored argv row —
`transport shell { argv: ["hostnamectl", "set-hostname", "{desired}"] }` — the exact
defect the CLI-invocation lane exists to remove: the subcommand and the operand were
opaque literals in a transport DSL, so the operation's own flags were hand-typed rather
than derived from cited rows. This is the #8467 grain of the shell->dag census's §5.A
hostname row: the §5.B grain (call a typed op) landed at #7194; the op's *realization*
is what this cut replaces.

The shape mirrors the jq vertical exactly:
- `hostnamectl_set_hostname_verb` is ONE cited row (freedesktop hostnamectl(1)); every
  argv derivation reads it, so a differently-spelled subcommand cannot reach argv.
- `HostnameSetInvocation { desired }` is what a caller describes — no flag, no argv
  position. A DnsLabel keeps the operand inside the hostnamectl-safe grammar.
- The lowering emits a two-argument surface [set-hostname, desired]: the subcommand as a
  FixedToken (spelling owned by the lex table), the operand as a BoundToken (spelling
  carried by the invocation). The executable is the handler's fixed tool name, exactly
  as jq.Process's transport row spells "jq".
- `hostname_set_invocation_process_plan` seals the surface into a sole_constructor plan;
  `hostname_set_execute_plan` runs it through the new `hostnamectl.Process.Run` handler;
  `hostname_set_classify_observation` owns the exit contract (0 = applied, nonzero =
  failed with stderr), so no domain code reads a raw exit code.

os.Hostname.Set is deleted with its transport row (the jq precedent: the semantic op
with hardwired argv is removed, the invocation layer answers its question). The local
leg (`hostname_set_local`) now builds the invocation and executes the sealed plan; the
SSH legs' privileged argv (`sudo -n <path> set-hostname <desired>`) reads the same
cited verb, so the local and remote legs cannot drift. The full-argv projection
`hostname_set_argv` is derived (executable + rendered surface) rather than a second
authority.

Witnesses: a new hermetic lowering witness (hostname_set_invocation_lowering_witness)
asserts the exact surface, the full-argv projection, the bound-operand perturbation,
and the exit contract; the census and host-identity witnesses are repointed onto the
invocation path. The v1 false-refusal rosters and the census ledger note the deletion.

Verified locally: build lane clean (regen first_generation_equal=true,
generated-artifact 36/36 match), witnesses lane clean (FloorClean, 3515 executed,
0 failed), infer_semantics_witness bin runs clean.

* Review fix: hostname_set_argv becomes refusal-carrying instead of widening a lowering refusal to Empty

Review advisory (PR #10211): the full-argv projection's `Rejected => Empty` arm was a
silent widen — a lowering refusal would surface as an empty list a caller could mistake
for a real projection, against DESIGN section 5's "a failure arm must refuse, never
widen". It was loud-in-practice (the witnesses' `""` join mismatch) but dishonest as a
production-module projection.

`hostname_set_argv` now returns Outcome<List<String>>: a lowering refusal is carried as
Rejected, and the three witness consumers match the Outcome instead of reading a bare
list that has already swallowed the refusal. The jq vertical's own lowering witnesses
do the same (their `argv_of` renders Rejected to false), but there the widen lives in
the test file; here it was in the production module.

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant