Skip to content

shell-typed-invocation first slice: the USB gadget setup is described commands, not shell text - #12579

Merged
gunbai-bot[bot] merged 17 commits into
mainfrom
session/stern-moth-249
Oct 1, 2026
Merged

gunbai-bot[bot] merged 17 commits into
mainfrom
session/stern-moth-249

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Sep 29, 2026 •

Copy link
Copy Markdown
Contributor

Roadmap node: rn_7T6WSS1JYCV6GQNW1PZG73B0G3 — shell-typed-invocation ("Describe what a command should do, instead of writing shell text"). Authority: docs/plans/shell-to-dag-residual-census-and-arc-completion.md; specimen: the USB gadget configfs setup, whose script once prefixed set -e and joined rendered lines carrying 2>/dev/null || true.

What this change does

The script builders are deleted, not wrapped. The instruction is now the typed staging: ConfigfsOp (five arms) folds through configfs_staging_of into one ConfigfsStaging — ConfigfsStagingReady { operations: List<ConfigfsPreparedOp> } or ConfigfsStagingRefused { reason }. There is no state in which a refused op sits beside prepared ones: the fold stops at the first op that does not prepare, and a refused staging carries no operation list at all, so a bad argument cannot act while the ops around it are skipped past. Ready, not Ran — nothing has run yet; the name says what the value is.

Containment is one validated fact, not a string prefix: configfs_path_verdict(gadget, path) answers Inside / Escaped / Outside for THIS gadget's own config_root, segment-wise — ./.. segments and sibling gadgets under the same mount refuse with a distinct escape reason; paths off the mount refuse with the outside reason. The old hard-coded gadget_configfs_root data row is deleted; the mount is a modeled input, and a fixture gadget rooted at a different configfs mount stages READY. The gadget's own name is a plain NonEmptyStr, and the spelling is the consumer's literal again, where the literal belongs (review 5360078848's sketch: the carrier proved custody, not segment validity — in-file construction around a/b stayed legal, so the constant was well-formed only by reviewed authorship, and moving the spelling into extdeps reversed the consumer/authority boundary). The segment law is instead taken by acceptance at the staging mint: configfs_staging_of takes configfs_name_verdict(gadget.name) FIRST — inside the only mint of sealed prepared operations, before usb_gadget_dir establishes the containment root — refusing the whole staging with a distinct reason before any op is prepared, so a gadget named a/b cannot redefine the boundary its own paths would be validated against. configfs_name_verdict stays the one place the law lives (dashboard review 72848, finding 1); it now gates link names, configuration names, and the gadget's own name. The paired production-route control distinguishes content, which a foreign-construction probe cannot: the slash-named gadget stages REFUSED, the estate's own name stages READY (sixteen prepared operations) on the identical route.

The link arms carry names, not paths: ConfigfsLinkFunction { function, configuration } / ConfigfsUnlinkFunction. Both endpoints are derived from the gadget's own record (<g>/functions/<f>, <g>/configs/<c>/), so "this gadget's function into this gadget's configuration" is a construction that cannot be authored wrong — an arbitrary target (the old fixture's /dev/nbd0 positive) is no longer expressible, and a name that is not a single well-formed segment refuses before anything is prepared.

Realization boundary (recommended next slice, delivered in the same change)

ConfigfsOpRunsArgv is no longer a semantic surface. ConfigfsPreparedOp is a sealed staged value: the five prepared variants are the public descriptive sum ConfigfsPreparedDisposition, and the wrapper is a sole_constructor record — construction is confined to extdeps.linux.usb_gadget, the only mint is configfs_op_prepared behind the containment and name verdicts — and the mint itself is caller-sealed (review 5360613023's finding: "sole caller today" is a census fact, not an enforcement boundary; without a wall a foreign module could call the mint directly with a slash-named gadget and configfs_path_verdict would validate against the root that name redefined): configfs_op_prepared carries an admit_callers wall naming exactly one production caller, configfs_staging_of, so the direct call is a ConstructorCallAdmissionRefused at resolve time — the same wall the caller-sealed transport_script_seal relies on. Sealed-value custody (sole_constructor), construction-route custody (admit_callers), and name content (verdict at the staging fold) are three laws; each has its own enforced boundary and its own witness control. configfs_prepared_realization accepts the sealed value and nothing else, so a cross-module author of a prepared op with a gadget_dir it chose is refused at compile time — proven, not asserted: the domain witness compiles a foreign module source through the guarantee probe corpus and requires the census to refuse the hand-authored construction (SoleConstructorViolation). The lowering: mkdir -p (mkdir builder), ln -sf <functions endpoint> <config dir/> (the into-directory ln builder), rm -f (rm builder), rmdir (rmdir builder) — or the native ConfigfsOpWritesAttr (a typed write(2), never a shell redirect). The eventual executor consumes the sealed prepared value (or a realization receipt minted from it), never an open command sum as authorization. Consumers of the semantic operation stop at the sealed staged value; only the execution boundary and the tool-realization witness see argv.

Witness split. dag/test/claim/shell/shell_typed_invocation_witness_test.dag is the domain side: verdicts, relationships, refusals-as-a-whole, the gadget-name segment guard, the phase fold that pins the teardown's order (detach → unlink → five rmdirs, innermost first), the two render-absence oracles the roadmap contract pins by name (usb_gadget_setup_emits_no_shell_control_word, teardown sibling), and the cross-module construction probe (prepared-op seal) with the paired production-route name control beside it. It imports no argv type. dag/test/claim/bmc/bmc_virtual_media_witness_test.dag is the fixture + tool-realization side: which builder each prepared op lowers to, asserted over argv fields (program against the builder's declared name row, argument counts, word membership, exactly one directory-spelled argument on the ln command) — it never calls shell_command_render and never searches a rendered string. Closing control, structural: no domain witness or configfs/BMC consumer learns what an operation means from anything rendered.

Frontiers (typed DissolutionConditions on the census roster, beside the declarations they front)

  • configfs_attr_write_realization_frontier_rows — the typed attribute write is owed to the host-effect lane's configfs effect family (roadmap rn_TAPSSCRTTBBV274TFK1PAGAP49, docs/plans/host-effect-orchestration.md). Unbound deliberately: the family is not yet named anywhere in the lane's plan, so a bound forward ref would cite a symbol nobody declared.
  • configfs_rmdir_absent_as_converged_frontier_rows — moved here from extdeps.tools.gnu_coreutils (it fronted the generic rmdir builder, whose other callers have no such policy): "already absent means converged" is configfs teardown policy. Population, complete: the five ConfigfsRmdir operations of the gunbcvm teardown — functions/mass_storage.0, configs/c.1/strings/0x409, configs/c.1, strings/0x409, and the gadget root. The plain rmdir stays the instruction; no || true re-enters.

The old renderer's retirement obligation is discharged, not carried: configfs_op_line is deleted and its trigger went with it — a trigger citing an absent declaration is the dead vocabulary this repository removes.

Scope and verification

  • The nbd lane (srv4_nbd_*) is the pre-existing CLI-authority surface and is untouched.
  • srv4_vm_gadget() is the fixture accessor the witnesses build from.
  • Locally verified at this head: the shell, bmc, and dissolution oracle wrappers all exit 0 (witness test functions executed by gunbc run, both foreign-module wall probes and the paired name control included); CI runs the same estate.
  • Stats at this head: 11 files changed, +1238 / −97.
  • Not authorized to merge in this session; merge awaits the operator once the tally floor is re-met.

— sent from stern-moth-249

… commands, not shell text

Each ConfigfsOp now maps to a typed command -- an ArgvCommand minted through the
tool's own cited builder (mkdir/ln/rm/rmdir, PATH-resolved), a typed attribute
write, or a typed refusal for a path outside the gadget configfs tree -- and the
string-building (configfs_op_line, configfs_ops_script, usb_gadget_setup_script,
usb_gadget_teardown_script) is deleted, not stubbed. Consumers read the described
form: bmc_virtual_media carries *_commands/*_display, the acceptance oracle
usb_gadget_setup_emits_no_shell_control_word is green by execution, the bmc
witness module asserts on commands, and the floor_expected_red roster row for the
greened probe is removed per DESIGN 4b(4) (the witness stays as the permanent
regression control). Verified locally by execution: shell oracle, all four bmc
witness fns, and migrated_production_retirement_conditions_are_bound all exit 0.
Brian Searls added 2 commits September 29, 2026 02:53
…er; import ends_with

required-ci refused this head twice. (1) CITED-DECLARATION-ABSENT:
configfs_op_render_dissolution_trigger cites configfs_op_line, which the
migration deleted -- a retirement obligation whose declaration no longer exists
is complete, so the trigger went with the declaration (kept-and-citing-absent
was exactly the dead vocabulary the repository removes). The discharge is
recorded where the trigger stood, in the census witness's comment (five live
obligations remain, not six -- explained, not silently dropped), and in the
coreutils prose. (2) UnimportedBareProvider: usb_gadget declares imports, so its
bare channel is off; ends_with now comes from gunbc.rust_item_scan, the same
provider heal_publisher_provision imports it from (starts_with is a builtin and
stays bare). Verified locally by execution: dissolution census, shell oracle,
and bmc witness wrappers all exit 0.
…consumer

Finding 1: the per-op ConfigfsOpRefused arm is gone. The ops fold into one
ConfigfsStaging -- ConfigfsStagingRan { commands } or
ConfigfsStagingRefused { reason } -- so a bad argument stops the WHOLE
setup or teardown instead of sitting beside runnable commands. The
discriminating fixtures run at the staging grain: a path outside the
gadget tree refuses naming the path, the same bad op mixed into an
otherwise-good staging refuses the whole staging, the good staging alone
mints its one command, and the symlink arm refuses until its link is
directory-spelled.

Finding 2: the display fold is modeled once, in configfs_staging_display;
srv4_vm_gadget_setup_display and the new srv4_vm_gadget_teardown_display
call it instead of repeating the fold beside it. The dangling
usb_gadget_setup_display caller is gone with the duplication.

Finding 3: the already-absent tolerance the old '|| true' carried is a
declared frontier (DESIGN section 3c) beside rmdir_command, and the
attribute write's realization is a declared frontier beside
ConfigfsOpWritesAttr -- each names its later consumer (the host-effect
lane's configfs effect family), the named later change (roadmap node
rn_TAPSSCRTTBBV274TFK1PAGAP49, fleet-closed-loop-converge,
docs/plans/host-effect-orchestration.md), and the trigger stated beside
the declaration.

The teardown now has its described-form consumer: the BMC witness reads
the teardown staging (seven commands, the empty UDC write first, rm -f on
the mass-storage link, every command naming the gadget's own configfs
directory) and the shell witness gates the teardown display against shell
control words. Oracle wrappers extended accordingly; all green by
execution.
@gunbai-bot

gunbai-bot Bot commented Sep 29, 2026

Copy link
Copy Markdown
Contributor Author

Addressing review 38602 — all three findings, fixed in 31ffa0d:

1. The refusal is now a stop at the grain a caller consumes, and it is exercised. The per-op ConfigfsOpRefused arm is deleted. The ops fold into one typed result, ConfigfsStaging — ConfigfsStagingRan { commands } or ConfigfsStagingRefused { reason } — so there is no state in which a refused op sits in a list beside runnable commands: a bad argument stops the WHOLE setup or teardown, and a refused staging carries no command list a caller could act on. Exercised green by execution in the shell witness (bad_arguments_refuse_the_whole_staging_before_any_command_acts: an outside-tree path refuses with the reason naming the path; the same bad op mixed into an otherwise-good staging refuses the whole staging; the good staging alone mints its one command; plus symlink_refuses_until_its_link_is_directory_spelled, both ways). Provenance note: the per-op refusal fixture this review asked for previously lived in the stacked PR #12585; it is now on this PR at the staging grain, and #12585 slims accordingly.

2. The display fold is modeled once. configfs_staging_display in extdeps.linux.usb_gadget is the one fold; usb_gadget_setup_display/usb_gadget_teardown_display derive from it, and bmc's srv4_vm_gadget_setup_display/srv4_vm_gadget_teardown_display call those instead of repeating the fold inline. The dangling usb_gadget_setup_display caller is gone with the duplication.

3. Both "later consumer" gaps are now declared frontiers with the trigger stated beside the declaration (DESIGN §3c). The dropping of || true stays (correct under §5's absorbing-fallback rule); what was missing — a named consumer — is now named: rmdir_already_absent_realization_frontier beside rmdir_command in gnu_coreutils, and configfs_attr_write_realization_frontier beside ConfigfsOpWritesAttr in usb_gadget. Each names the later consumer (the host-effect lane's configfs effect family), the named later change (roadmap node rn_TAPSSCRTTBBV274TFK1PAGAP49, fleet-closed-loop-converge, docs/plans/host-effect-orchestration.md), and the trigger. Additionally, the teardown now has its described-form consumer on this PR: the BMC witness reads the teardown staging (seven commands, the empty-UDC write first — pinned by the display's first line — rm -f on the mass-storage link, every command naming the gadget's own configfs directory), and the shell witness gates the teardown display against shell control words.

Oracle wrappers extended to carry the new fixtures; all green by execution (shell, bmc, dissolution census).

— sent from stern-moth-249

Brian Searls added 3 commits September 29, 2026 04:03
…ardown's last act

The staging-refusal fixture now refuses a write-attr outside the tree too
(/etc/passwd, reason naming the path), so the discriminator covers both
non-argv arms, and the BMC teardown witness pins the teardown's last act:
an rmdir of the gadget root itself (the closing quote in the pattern keeps
deeper rmdirs from satisfying it). With these, the stacked slice's witness
content is fully absorbed by this PR.
…gebra

The changed-witness sublane rosters bare providers on changed lines: the
staging fold's append(cs, items: minted) rode a loose local channel the
required-ci adjudication does not honor (UnimportedBareProvider
Unrostered usb_gadget.dag#append). The builtin's rostered name is
list_append in std.algebra; the fold now calls it by that name and the
module imports it.
A refused staging renders as 'refused: ...' lines, and those carry no
shell control word -- so an all-refused fixture (the gadget's config_root
changed away from the gadget tree) would green
usb_gadget_setup_emits_no_shell_control_word while the setup would act on
nothing. Both oracle fns now red on a refusal rendering; the route itself
is asserted in the bmc witness, which matches ConfigfsStagingRan and
fails on Refused for the same fixture. Dashboard review against fb46893
(artifact /api/reviews/72447), finding 1's witness clause.
@gunbai-bot

gunbai-bot Bot commented Sep 29, 2026

Copy link
Copy Markdown
Contributor Author

Addressing the dashboard review against fb46893 (artifact /api/reviews/72447/artifacts/stdout.log) — same shape as review 38602, and both are addressed by the same climb. Per finding:

1. The refusal doesn't stop anything; the oracle can't tell a refusal from success. Fixed in 31ffa0d: the per-op ConfigfsOpRefused arm is gone; the ops fold into one typed coproduct, ConfigfsStaging — ConfigfsStagingRan { commands } or ConfigfsStagingRefused { reason } — so one refusal refuses the WHOLE list and a refused staging carries no command list a caller could act on. The witness clause you asked for landed twice: the bmc witness matches ConfigfsStagingRan and fails on Refused for the srv4 fixture (the ROUTE asserted directly), and 223ec93 makes the acceptance oracle itself red on a refusal rendering — your all-refused scenario (config_root changed away from the gadget tree) now reds usb_gadget_setup_emits_no_shell_control_word instead of greening it, because a refused staging renders refused: … lines and the oracle no longer accepts them. The staging-grain fixtures also run in the same change: outside-tree mkdir and write-attr refuse naming the path, the same bad op mixed into an otherwise-good staging refuses the whole staging, the good staging alone mints its one command, and the symlink arm refuses until directory-spelled (both ways).

2. No-consumer declarations + duplicated fold. All wired or deleted in 31ffa0d/d0be5f7309: usb_gadget_setup_display is called — bmc's srv4_vm_gadget_setup_display delegates to it; the fold is modeled ONCE, configfs_staging_display, and both the usb-level and srv4-level displays derive from it; srv4_vm_gadget_teardown_commands is deleted (replaced by srv4_vm_gadget_teardown_staging, consumed by the bmc witness, which reads the real producer path); and the already-absent tolerance the old || true carried has a NAMED consumer — the declared frontier beside rmdir_command in gnu_coreutils names the host-effect lane's configfs teardown realization, the named later change (roadmap node rn_TAPSSCRTTBBV274TFK1PAGAP49, fleet-closed-loop-converge, docs/plans/host-effect-orchestration.md), and the trigger stated beside the declaration. The attribute-write arm carries the same kind of frontier beside ConfigfsOpWritesAttr.

3. Advisory: the extdeps import of a string helper from a gunbc scan module. Verified: ends_with IS a std primitive — its contract sits in dag/std/primitives.dag — but std.primitives exports only contract and roster rows, no importable callable binding, so the primitive cannot be imported. The only callable ends_with in the tree is the same-named fn in gunbc.rust_item_scan, and the required-ci roster demanded an explicit import for the bare name on a changed line (bare starts_with next to it was never flagged — the collision with that fn declaration is the difference). I kept the import: it is floor-green and the only rostered route today. Left for the std lane, where the honest fixes are: export a callable binding for the primitive, or roster primitives above same-named fns so the disambiguating import is never needed. Happy to take that as a follow-up slice if you want it owned here.

— sent from stern-moth-249

… prose Strings

review 72478 (against d0be5f7, applies equally to the head): both frontier
rows were data-String commentary nothing could read -- the exact defect DESIGN
4c names -- and the already-absent rmdir outcome had no typed rung-change
record (4b(3)).

Both rows are now List<FrontierRow> exports built with frontier_row_decl +
unbound_dissolution (the house spelling of extdeps.tools.sha256sum's
sha256_verify_native_transport_frontier_rows and std.machine_constraints'
machine_width_literal_roster_frontier), with the fronting rationale moved
into // comments, and both are appended to gunbc.census_closure_frontier's
roster -- the census now reads them, so they are consumed declarations (3c)
and not dead data (4c).

UNBOUND, deliberately: each condition is the ARRIVAL of a family the
host-effect plan (rn_TAPSSCRTTBBV274TFK1PAGAP49) names nowhere, so a bound
forward ref would cite a symbol nobody declared -- the fabricated-citation
class std.dissolution refuses; stated beside each row. The rmdir carrier's
description carries the full 4b(3) record: previous rung (unmodeled shell
fallback -- silent absorption, below the ladder), temporary rung (honest
nonzero, witnesses gate the staging), reason, bounded population
(ConfigfsRmdir arm, the builder's sole executing call site), restoration
trigger (the lane's configfs teardown realization).

The discharged renderer trigger was NOT restored: required-ci refused it as
CITED-DECLARATION-ABSENT (its ref named configfs_op_line, which the migration
deleted -- a retirement obligation whose declaration no longer exists is
complete); the discharge stays recorded in the census witness.

Verified locally by execution: dissolution census, shell oracle, and bmc
witness wrapper mains all exit 0 on this head; the census consumers assert
membership and structural partitions only, so the two new rows shift no
asserted count.
@gunbai-bot

gunbai-bot Bot commented Sep 29, 2026

Copy link
Copy Markdown
Contributor Author

Addressing review 72478 (dashboard-only artifact, against d0be5f7; both findings apply equally to the prior head and are now fixed on the new head 438bdb3).

Finding 1 — the two frontier rows were unread prose Strings (§4c), a step backwards from the typed trigger. Fixed in 438bdb3, in the shape the corpus already uses for exactly this:

  • Both rows are retyped as List<FrontierRow> exports built with frontier_row_decl + unbound_dissolution — the house spelling of extdeps.tools.sha256sum sha256_verify_native_transport_frontier_rows and std machine_width_literal_roster_frontier — with the fronting rationale moved into // comments (the second form your finding offers).
  • Both rows are appended to gunbc.census_closure_frontier's roster, so the dissolution census now READS them. This also repairs the §3c half: before this commit they were a data row no fold reads (dangling); now the census verdict folds them like every other frontier row.
  • UNBOUND, deliberately, and the reason is stated beside each row: each condition is the ARRIVAL of a family the host-effect plan (roadmap node rn_TAPSSCRTTBBV274TFK1PAGAP49, docs/plans/host-effect-orchestration.md) names nowhere — the plan has no configfs effect-family symbol yet — so a bound forward ref would cite a symbol nobody has declared, which is the fabricated-citation class std.dissolution's own header refuses. The paying change binds the realization and deletes the row; until then the census reports it as unmet debt rather than letting it be invisible.

On "a step backwards": the deletion of configfs_op_render_dissolution_trigger was forced, not chosen — required-ci refused the head as CITED-DECLARATION-ABSENT because that trigger's ref named configfs_op_line, which the migration itself deleted; a retirement obligation whose declaration no longer exists is complete, and keeping a trigger citing an absent declaration is the dead vocabulary the repository removes. The discharge is recorded where the trigger stood and in the census witness's comment (five live obligations, not six — explained, not silently dropped). The two new frontiers are different debt — the unrealized attribute-write realization and the unmodeled already-absent teardown outcome — and they are now typed, which is the regression your finding flagged, undone.

Finding 2 — no typed rung-change record for the already-absent rmdir outcome (§4b(3)). Fixed in the same commit: the rmdir_command carrier's description now carries the record in full — PREVIOUS RUNG (tolerated by an unmodeled shell fallback: silent absorption, below the ladder rather than a rung on it), TEMPORARY RUNG (the described teardown surfaces the honest nonzero; the witnesses gate the staging as a description), REASON (absorbing-fallback shell is forbidden, and modeling absence without a state observer would fabricate a readback the described command cannot supply), BOUNDED POPULATION (the ConfigfsRmdir arm of the configfs staging — the builder's sole executing call site — the final rmdir of the gunbcvm gadget teardown), RESTORATION TRIGGER (the host-effect lane's configfs teardown realization, roadmap node rn_TAPSSCRTTBBV274TFK1PAGAP49, which observes the target's state and records an absent directory as already-converged; when it binds, this frontier dissolves and no || true re-enters).

Verification: the three hermetic wrapper mains (dissolution census, shell oracle, BMC witness) all exit 0 on 438bdb3 locally. The census consumers assert membership and structural partitions only — unbound + pending + fired == length, fired_still_present == 0, per-row membership — so the two new rows shift no asserted count; the census verdict stays clean because unbound rows never fire.

— sent from stern-moth-249

@gunbai-bot

gunbai-bot Bot commented Sep 29, 2026

Copy link
Copy Markdown
Contributor Author

Addressing review 72511 (against f792108; the head is now 438bdb3).

Finding 1 — the two frontier rows were commentary stored as String (§4c), and dangling (§3c). Already fixed on the head in 438bdb3, in exactly the shape your finding offers: both rows are now typed List<FrontierRow> exports built with frontier_row_decl + unbound_dissolution — the house spelling of extdeps.tools.sha256sum sha256_verify_native_transport_frontier_rows and std machine_width_literal_roster_frontier — with the wording moved into // annotations AND kept as the typed carrier's dissolution description, so the machine-visible claim is not given up. Both rows are appended to gunbc.census_closure_frontier's roster, so the dissolution census now reads them: they were a data row no fold reads before; they are folded frontier rows now. On the deleted configfs_op_render_dissolution_trigger: that deletion was forced by the floor — required-ci refused the head as CITED-DECLARATION-ABSENT because the trigger's ref named configfs_op_line, which the migration itself deleted; a retirement obligation whose declaration no longer exists is complete. The discharge is recorded in the census witness (five live obligations, not six — explained, not silently dropped).

Finding 2 — ConfigfsWriteAttr has no realization; the staging has no consumer that executes it. The §3c limb of this finding is resolved by the same commit: your objection was that "the trigger for this frontier sits in one of the prose rows … not in a typed carrier. So as written, this frontier does not meet the §3c bar." The trigger now lives in the typed carrier beside the declaration it fronts, which is the bar you cite and the unblock your verdict names ("Put the frontier in a typed carrier and this is close to mergeable").

The §5 limb — "a dissolution condition … does not authorize creating the debt … Approval is external to the diff" — is satisfied by that externality, and I want to cite it precisely. The debt's authorization is this slice's assignment under the roadmap node this PR implements (rn_7T6WSS1JYCV6GQNW1PZG73B0G3), and the node's authority document, docs/plans/shell-to-dag-residual-census-and-arc-completion.md, both orders this migration and names the realization's destination:

  • Line 10: "Runtime-present shell … all funnels onto one keystone: host_effect_apply carrying typed effects."
  • Line 155: command_runner_dissolution_trigger "dissolves when host_effect_apply binds ArgvCommand execution as a typed transport handler … what remains open is host_effect_apply itself."
  • Track 2 (line 318): "runtime-present shell onto host_effect_apply (the §2 keystone cascade)".
  • And the census's own deferred-sites table lists this very site as its own row: "bmc_virtual_media.dag srv4 gadget scripts | BMC provisioning, separate lane."

So the document that mandates this change also reserves the execution-binding vertical as a separate, gated lane — which is why this slice must not start it, and why the frontier (now typed and census-visible) is the correct in-slice record of that debt.

On "Before this PR, the script was at least an executable instruction": a factual correction from git history. The pre-PR artifact was srv4_vm_gadget_setup_script → usb_gadget_setup_script (a shell string), and its in-tree consumers were exactly two witness modules — test.claim.bmc_virtual_media_witness_test and test.claim.shell.shell_typed_invocation_witness_test (git grep srv4_vm_gadget_setup 6f96d86ebc). Nothing in the closure executed it before this PR either; that is why the site sat on the census punch-list as residual shell. The PR therefore removed no executing route — it removed unchecked shell text and replaced it with a typed staging whose consumers (one display fold, the witnesses) are the same surfaces the script had. The realization consumer is the declared keystone above, named in the frontier.

Finding 3 (minor) — ends_with from gunbc.rust_item_scan. Verified: no std text authority exports a callable ends_with. dag/std/algebra.dag:830 sits in the String-method contract table (concat, contains, starts_with, ends_with, …) — declared contracts, not bindings; std.primitives likewise carries only ends_with_contract data. The only callable provider in the tree is gunbc.rust_item_scan's, and the floor itself forced this import (bare use on changed lines in a module that declares imports is refused as UnimportedBareProvider). Same answer as review 72447's F3: keep the import, and the gap is flagged for the std lane — the contract row proves std intends the method; the callable is owed beside it.

— sent from stern-moth-249

The ln-flags comment said the one live caller was configfs_op_command --
a function the staging climb deleted when it folded per-op minting into
configfs_op_staging. The refusal claim itself is unchanged and true: the
sole executing call site (usb_gadget.dag, the staging's link arm) refuses
a destination that is not directory-spelled before any argv is minted.
The citation now names the function that does it. Comment-only change;
all three wrapper mains (oracle, bmc, dissolution census) exit 0 after.
@gunbai-bot

gunbai-bot Bot commented Sep 29, 2026

Copy link
Copy Markdown
Contributor Author

Addressing review 72541 (against 223ec93; the head has since moved twice and now sits at a28daf4).

Finding 1 — the two frontier rows were plain prose strings nothing reads (§4c, §3c). Already fixed before this review arrived: commit 438bdb3 (one commit after the 223ec93 you reviewed) retyped both rows as typed List<FrontierRow> carriers — frontier_row_decl + unbound_dissolution, the house spelling of extdeps.tools.sha256sum sha256_verify_native_transport_frontier_rows and std machine_width_literal_roster_frontier — moved the rationale into // annotations, and enrolled both rows in gunbc.census_closure_frontier's roster, so the dissolution census now folds them: they were a data row no fold reads; they are consumed frontier rows now. Your suggested fix ("carry each frontier in a typed carrier … If the reasoning is just human rationale, move it into a // annotation") is implemented in both halves: typed carrier for the machine-visible debt, annotations for the human rationale. On the deleted typed trigger: configfs_op_render_dissolution_trigger was removed because required-ci refused the head as CITED-DECLARATION-ABSENT — its ref named configfs_op_line, which the migration itself deleted; a retirement obligation whose declaration no longer exists is complete, and the discharge is recorded in the census witness (five live obligations, not six — explained, not silently dropped).

Finding 2 — a comment names a symbol that doesn't exist (configfs_op_command). Valid and fixed: commit a28daf4 points the ln-flags comment at configfs_op_staging, the function that actually does the refusing. The comment's substantive claim was re-verified against the current tree and is unchanged and true: the sole executing call site of ln_symbolic_force_into_directory_command is the staging's link arm (usb_gadget.dag), which refuses a destination that is not directory-spelled before any argv is minted — the same contract the comment records, now cited at the right symbol. git grep 'configfs_op_command\b' is empty on the head. Comment-only change; all three wrapper mains (shell oracle, BMC witness, dissolution census) exit 0 after.

— sent from stern-moth-249

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

HOLD at a28daf48440557b190211b53c28ca7ef1882ac1a.

The root cut is right: the script builders are deleted rather than wrapped, refusal now stops the whole staging, and the setup/teardown consumers read the typed route. The required witnesses run is green. I found three correctness blockers before this is an honest handback.

  1. configfs_op_staging does not establish containment, and it ignores the gadget's declared root. Every arm accepts a raw starts_with(path, gadget_configfs_root) check. A path such as /sys/kernel/config/usb_gadget/../outside passes and is then handed to mkdir, rm, rmdir, or the future native write even though it resolves outside the gadget tree. Conversely, UsbGadget.config_root is an input to the model, but staging hard-codes /sys/kernel/config/usb_gadget/, so any other admitted configfs mount is refused. Carry the gadget/root context into staging and construct or validate typed descendants of that root (including rejection of ./.. segments), rather than treating a string prefix as containment. The controls should include both an escaping-path RED and an alternate-root positive.

  2. The symlink arm validates only the destination spelling; it never validates the target or the relation between the two. It will mint ln -sf for an arbitrary target, and the new positive fixture actually uses /dev/nbd0 as the target. The configfs operation here is associating one of this gadget's function instances with one of this gadget's configurations; an arbitrary target is an unavailable/invalid operation that should refuse before argv is minted under this node's own red control. Model that relation (target under this gadget's functions, destination under its configs) and add the opposite control. Also give the missing-trailing-slash case its own refusal reason; today it is reported as “outside the gadget tree” even when it is inside.

  3. rmdir_already_absent_realization_frontier_rows is attached to the wrong authority and its claimed population is false. Plain rmdir_command correctly models the generic coreutils operation; “already absent means converged” is configfs teardown realization/policy, not a property of every rmdir invocation. The carrier also says the bounded population is “i.e. the final rmdir,” while usb_gadget_teardown_ops emits five ConfigfsRmdir operations. Put any genuinely owed absence handling beside ConfigfsRmdir/the teardown realization and name the whole population, or delete this frontier and let the eventual host-effect realization model the outcome when it exists. Do not burden the generic tool builder with a configfs-specific debt row.

The PR description also needs rebinding to this head: it still describes the deleted ConfigfsOpRefused and *_commands surfaces, says configfs_op_render_dissolution_trigger was kept and bound although it was deleted, and reports 7 files / +236−53 rather than the current 9 / +515−65.

argv dissolution next: yes. This is a good first vertical once the validation boundary is repaired, but do not spread ConfigfsOpRunsArgv as the next authority. Keep the semantic configfs/tool operation as the value consumers inspect and make ArgvCommand a private leaf produced only at the process-realization edge. This vertical gives a bounded first cut—mkdir-parents, link-function-into-config, unlink, remove-empty-directory, plus the native attribute write. A useful closing control is that no domain consumer or witness needs shell_command_render or argument-string inspection to know what any of those operations means; only the execution boundary sees argv.

…argv leaves the semantic surface

Blocker 1: the starts_with guard admitted <mount>/usb_gadget/<g>/../outside
and every sibling gadget; the verdict is now one containment fact validated
segment-wise against the gadget's own config_root (the hard-coded
gadget_configfs_root data row is deleted -- the mount is a modeled input).

Blocker 2: ConfigfsSymlink/ConfigfsRemoveLink carried paths and blessed any
target (/dev/nbd0 was the fixture's positive); the ops are
ConfigfsLinkFunction/ConfigfsUnlinkFunction carrying NAMES -- staging derives
both endpoints from this gadget's record, so the functions-into-configs
relationship is a construction, not a check. Refusal reasons are distinct per
fault: outside the mount, escaped the gadget directory, name not a segment.

Blocker 3: the rmdir already-absent frontier moved beside ConfigfsRmdir in
usb_gadget.dag -- the debt is configfs TEARDOWN policy, not a property of
every rmdir invocation -- and its population is the five teardown rmdirs,
complete, not the final one.

Recommended next slice: ConfigfsOpRunsArgv stops being a semantic surface.
Staging returns ConfigfsPreparedOp (ConfigfsStagingReady, not Ran: nothing has
run yet); configfs_prepared_realization lowers each prepared op at the
realization boundary to the private ArgvCommand carrier or the native write.
The domain witness stops at prepared ops and imports no argv type; the
tool-realization witness asserts argv fields (program rows, argument counts,
word membership, the directory argument's directory-spelled form) and never
calls shell_command_render. Staging is refused as a whole at the first op that
does not prepare; the teardown's order is gated by a phase fold over the
authored ops, not by reading the display's first line.

Locally verified: shell, bmc, and dissolution oracle wrappers all exit 0.
@gunbai-bot

gunbai-bot Bot commented Sep 29, 2026

Copy link
Copy Markdown
Contributor Author

All three blockers are repaired and the recommended argv-dissolution slice is delivered, in fbe377f2a3 (answering this review).

1. Containment, against the gadget's declared root. configfs_op_staging and the gadget_configfs_root data row are deleted. configfs_path_verdict(gadget, path) -> ConfigfsPathVerdict answers one containment fact three ways — ConfigfsPathInside / ConfigfsPathEscaped / ConfigfsPathOutside — validated segment-wise against the gadget's own config_root: not under the mount → Outside; a ./.. segment, or under the mount but not under this gadget's directory (sibling gadget, class entry) → Escaped; under this gadget's directory → Inside. Staging takes the gadget. The controls you asked for are both in: an escaping-path RED (/sys/kernel/config/usb_gadget/gunbcvm/../elsewhere refuses with the escape reason) and a sibling-gadget refusal, plus the alternate-root positive (gadget_stages_against_its_own_mount_not_a_hard_coded_root — a fixture gadget rooted at /mnt/configfs/usb_gadget stages READY, and the same path that was inside under the conventional mount refuses there).

2. The link relation is a construction, not a check. ConfigfsSymlink/ConfigfsRemoveLink are gone; the arms are ConfigfsLinkFunction { function, configuration } / ConfigfsUnlinkFunction carrying NAMES. Staging derives both endpoints from this gadget's record — <g>/functions/<f> as the target, <g>/configs/<c>/ as the directory-spelled destination — so an arbitrary target is not an op that might pass a guard; it has no field to be authored into, and the /dev/nbd0 positive fixture is deleted with the old type. The name guard (configfs_name_verdict) refuses a name that is not a single well-formed segment (slash, ./.., leading dot) before anything is prepared — that is the refusal reason for a derived endpoint that would leave the gadget tree, distinct from the two path reasons. The missing-trailing-slash case no longer exists to be mislabeled: nothing is authored directory-spelled anymore; the builder's into-directory contract is asserted in the tool-realization witness as an argv-field fact (exactly one argument ends with /, and it is the derived configuration directory). The opposite control you asked for: link_names_that_are_not_single_segments_refuse_the_staging (slash and ../ refuse; the EMPTY name is refused one rung earlier — the type checker declines to author it as a NonEmptyStr at all), and link_function_relates_this_gadgets_function_to_this_gadgets_configuration pins the endpoints as derived. ConfigfsStagingRan → ConfigfsStagingReady: ready is what the value is (a prepared plan), not what will happen to it.

3. The rmdir frontier moved to the right authority, with the true population. rmdir_already_absent_realization_frontier_rows is deleted from extdeps.tools.gnu_coreutils — you're right that the plain builder models the generic coreutils operation and carries no tolerance policy; its comment now says exactly that. The debt lives beside ConfigfsRmdir in extdeps.linux.usb_gadget as configfs_rmdir_absent_as_converged_frontier_rows, and the carrier names the whole population: the FIVE ConfigfsRmdir operations of the gunbcvm teardown (functions/mass_storage.0, configs/c.1/strings/0x409, configs/c.1, strings/0x409, and the gadget root), complete — the census roster import and group entry were swapped accordingly.

PR description: rebound to this head — it now describes the shipped surfaces (staged/prepared ops, the verdicts, the two frontiers at their new home) and the current stats (9 files, +1055/−86). Nothing in it claims a deleted declaration was kept.

argv dissolution next — done as you prescribed. Staging returns List<ConfigfsPreparedOp>; ConfigfsOpRunsArgv exists only inside configfs_prepared_realization's return type at the process-realization edge, next to the native write. The vertical is the bounded five: mkdir-parents, link-function-into-config, unlink, remove-empty-directory, native attribute write. The closing control is structural, not just asserted: the domain witness (dag/test/claim/shell/...) imports no argv type and stops at prepared ops; the tool-realization witness (dag/test/claim/bmc/...) reads argv FIELDS — program against the builder's declared name row, argument counts, word membership, the directory argument's spelling — and calls shell_command_render nowhere; the only rendered-string reads left in the estate's configfs/BMC lane are the two contract-pinned render-absence oracles, which check a whole display for the absence of shell control words, never for meaning. The teardown's order is gated by a phase fold over the authored ops (detach first, then the unlink, then only rmdirs), not by reading the display's first line.

Locally verified at this head: shell, bmc, and dissolution oracle wrappers all exit 0.

— sent from stern-moth-249

…se (review 72665, minor)

The comment beside shell_typed_invocation_execution_contract still said the
deleted usb_gadget_setup_script "prefixes set -e" and that the witness
"FAILS TODAY" and "IS ENROLLED" in floor_expected_red -- all three true when
written, all three false since the slice landed. It now narrates the completed
transition: the script was then (and is deleted), the witness was red until
2026-09-29, the enrollment ended when the row left the roster by the counted
un-quarantine, and the green probe stays as the regression control.
@gunbai-bot

gunbai-bot Bot commented Sep 29, 2026

Copy link
Copy Markdown
Contributor Author

Thank you — approval noted. The one minor remark is fixed in 87ca1482a5: the comment beside shell_typed_invocation_execution_contract now narrates the red→green transition in the past tense (the script was then and is deleted; the witness was red until 2026-09-29; the floor_expected_red row left by the counted un-quarantine, and the green probe stays as the regression control). Comment-only change; CI re-runs on the new head.

— sent from stern-moth-249

…ed (review 72683, minor)

The comment claimed its dissolve-on examples "are all live declarations"; the
shell-typed-invocation slice deleted configfs_op_line, so one of them was not.
The list now carries the live examples, and the retired one is named as
retired -- its disappearance WAS the retirement, and it went.
@gunbai-bot

gunbai-bot Bot commented Sep 29, 2026

Copy link
Copy Markdown
Contributor Author

Tidied in 51c4ca9e3e, answering this review: the comment's own claim was that its dissolve-on examples "are all live declarations", and the shell-typed-invocation slice deleted one of them. The list now carries the live examples (sol_console_send, nbd_server_config_text, fleet_converge_apply_shell — both re-verified live), and the retired one is named as retired: its disappearance WAS the retirement, and it went. Comment-only; CI re-runs on the new head.

— sent from stern-moth-249

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

HOLD at 51c4ca9e3ee78ff5a997eeefb8b827986a90be08.

The three blockers from a28daf4844 are repaired on the intended route: containment is now gadget-relative with escape/sibling refusals and an alternate-root positive; the link relation carries names and derives same-gadget endpoints; and the absent-rmdir frontier is beside ConfigfsRmdir with the complete five-operation population. The argv split is also materially better: the domain witness stops at semantic/prepared operations, and the tool witness inspects fields rather than scraping rendered shell. All exact-head CI lanes are green.

Two construction blockers remain before the handback is honest.

  1. The prepared/realization boundary is publicly forgeable, so staging validation is optional. ConfigfsPreparedOp is a plain coproduct, ConfigfsStagingReady is a plain coproduct, ConfigfsOpCommand is a plain coproduct, and configfs_prepared_realization is an exported function. In this language there is no function privacy, and the repository already records that sole_constructor is discarded on coproduct variants (gunbc.recurring_failure_mode.modifier_accepted_on_a_shape_its_check_cannot_see; the repaired pattern is in gunbc.review_sheet_identity). A caller can therefore author, cross-module, for example ConfigfsPreparedLinkFunction { gadget_dir: "/etc", function: "passwd", configuration: "x" } and pass it straight to configfs_prepared_realization, bypassing both configfs_path_verdict and configfs_name_verdict. The open ConfigfsOpWritesAttr arm has the same problem if the eventual host-effect consumer accepts ConfigfsOpCommand. Thus the comments and PR body currently overclaim “validated,” “cannot be authored wrong,” and “private process-boundary carrier.”

    Use the existing public disposition + sole_constructor record wrapper pattern: staging alone mints a sealed prepared value; realization accepts that sealed value. Have the eventual executor consume the sealed prepared value and lower internally, or seal the realization result too—do not make an open ConfigfsOpCommand the authorization to act. Add a cross-module RED proving that direct preparation/realization construction is refused; the current route tests prove the honest path works, not that the bypass is unwritable.

  2. The gadget identity used to define containment is still not a path segment. UsbGadget.name remains a bare NonEmptyStr, and usb_gadget_dir joins it into the root before configfs_path_verdict defines what “inside this gadget” means. A gadget named a/b (or a/) produces a nested gadget_dir; every generated setup path then compares inside that same derived string and stages READY. configfs_name_verdict protects function/configuration names, but never the gadget name. This is the same self-grounding hole one level up from the repaired link endpoints. Validate/mint the gadget name as one segment before deriving any path—preferably a sealed name carrier—and add the slash-containing-name RED plus the ordinary-name positive.

Minor handback drift: the PR body still says 9 files, +1055/−86, while this exact head is 11 files, +1073/−97 after the two comment fixes. Rebind that when the code blockers are repaired.

…a sealed segment

Blocker 1 -- the prepared/realization boundary was publicly forgeable: a
foreign module could author ConfigfsPreparedLinkFunction with a gadget_dir
it chose and hand it to configfs_prepared_realization, so staging's
containment and name verdicts were optional for anyone willing to skip
them. The five prepared variants are now the public descriptive sum
ConfigfsPreparedDisposition, and ConfigfsPreparedOp is a sole_constructor
record wrapper around it: construction is confined to this file, the only
mint is configfs_op_prepared behind both verdicts, and realization accepts
the sealed value and nothing else. The eventual executor consumes the
sealed prepared value (or a realization receipt it mints from it), never
an open command sum as authorization. Cross-module RED: a probe source
compiled through the guarantee probe corpus constructs the wrapper by hand
and asserts the census refuses it (SoleConstructorViolation >= 1).

Blocker 2 -- the gadget identity that defines containment was still not a
path segment: usb_gadget_dir joined a bare NonEmptyStr under the class
root before any verdict ran, so a gadget named a/b redefined its own
containment boundary and self-validated inside it. UsbGadget.name now
carries UsbGadgetName, a sealed single-segment carrier whose only mints
are the verdict's well-formed arm and the named estate constant
(gunbcvm_gadget_name); usb_gadget_dir derives from the proven segment.
Controls: slash and dot-segment names refuse the name verdict, the
ordinary name passes and agrees with the constant, and a second cross-module
probe authors the carrier around "a/b" and is refused.

Minor: the realization-boundary comment no longer calls ArgvCommand
private -- the enforced boundary is the sealed staged value, not a
visibility keyword the language does not have.
@gunbai-bot

gunbai-bot Bot commented Sep 29, 2026

Copy link
Copy Markdown
Contributor Author

Addressing review 5357430436 at head bc73a3ed59:

Blocker 1 — the prepared/realization boundary is publicly forgeable. Repaired on exactly the named pattern: the five prepared variants are now the public descriptive sum ConfigfsPreparedDisposition, and ConfigfsPreparedOp is type ConfigfsPreparedOp sole_constructor { disposition: ConfigfsPreparedDisposition } — a record wrapper, not a coproduct, so the modifier sits on the shape the check can see (the gunbc.review_sheet_identity / UriValidatedScalar shape). Construction is confined to extdeps.linux.usb_gadget; the only mint is configfs_op_prepared, behind configfs_path_verdict and configfs_name_verdict; configfs_prepared_realization(op: ConfigfsPreparedOp) matches op.disposition and takes the sealed value and nothing else. The executor obligation is stated at the boundary: the eventual executor consumes the sealed prepared value (or a realization receipt it mints from it), never an open ConfigfsOpCommand as authorization. The "private carrier" and "cannot be authored wrong" overclaims are rewritten — enforcement is now the seal, and the comment says so.

Cross-module RED, as required: the domain witness now carries foreign_module_cannot_hand_author_a_prepared_op_to_the_realization — a foreign module source compiled as data through the guarantee probe corpus (the operation_admit_callers_inert_witness_test harness) that authors the review's exact spelling — ConfigfsPreparedOp { disposition: ConfigfsPreparedLinkFunction { gadget_dir: "/sys/kernel/config/usb_gadget/gunbcvm", ... } } — and hands it to configfs_prepared_realization. The test requires the census to refuse it (SoleConstructorViolation ≥ 1). This is the control the honest-route tests did not provide.

Blocker 2 — the gadget identity is still not a path segment. Repaired with the sealed name carrier: type UsbGadgetName sole_constructor { segment: NonEmptyStr }, UsbGadget.name: UsbGadgetName. The carrier's only mints are the verdict's well-formed arm (usb_gadget_name_verdict, the same segment law as configfs_name_verdict: not empty, no /, not a dot segment, no leading dot — the empty spelling is refused one rung earlier by the type checker, which will not author it as a NonEmptyStr) and the named estate constant gunbcvm_gadget_name, minted in the authority file. usb_gadget_dir derives from the proven segment, so the name is one segment before any path is derived, and no UsbGadget reaching staging can carry an unvalidated name because no unvalidated spelling constructs the carrier — the proof is the field's type.

Controls: gadget_name_must_be_a_single_well_formed_segment (RED: "a/b" and ".." → UsbGadgetNameNotASegment; positive: "gunbcvm" → well-formed and identical to the estate constant), plus a second cross-module probe, foreign_module_cannot_construct_the_gadget_name_carrier, which authors UsbGadgetName { segment: "a/b" } from outside and requires the census to refuse it — the direct proof that the slash spelling cannot enter any UsbGadget from outside.

Minor — handback stats. Recomputed exactly at bc73a3ed59: 11 files changed, +1226 / −100, and the PR body is rebound via edit with the seal, the name carrier, and the probes described.

Local verification at this head: the shell oracle (all eight pre-existing witness tests plus the three new controls), the bmc oracle, and the dissolution oracle all exit 0 under gunbc run; CI runs the same estate and is being polled.

Not merging from this session — the tally re-evaluation and merge decision stay with you.

— sent from stern-moth-249

…uthorship is stated

Finding 2 -- the sealed-name verdict was decoration: nothing on the
production path called usb_gadget_name_verdict, and the estate constant
was built directly beside it, so the check gated nothing and the test
checked the verdict and the constant separately. Deleted on the review's
own offered route: UsbGadgetName stays a sealed sole_constructor carrier,
the estate constant stays an in-file authored data row, and the comment
now states the enforcement plainly -- construction is confined to the
authority module, the constant is authored there where the segment law
lives, and the cross-module probe in the shell witness (constructing the
carrier around a/b from outside, refused) is the RED. A runtime verdict
kept beside the seal would have been a second copy of a law nothing
called.

Finding 1 -- the segment law was written out twice, once in
configfs_name_verdict and once in the deleted verdict. With the verdict
gone the law lives in exactly one place again. The n == "" arm stays in
that one copy, with its reach stated: the type checker refuses an authored
empty spelling, but a join over empty parts computes one, so the law stays
total over what can reach it at runtime.

Oracle reruns green at this head: all eight pre-existing witness tests plus
both cross-module construction probes exit 0.
@gunbai-bot

gunbai-bot Bot commented Sep 29, 2026

Copy link
Copy Markdown
Contributor Author

Addressing dashboard review 72848 at head a00c5f6a83 (artifact — the review was not posted to the PR, so this reply carries it):

Finding 1 — the same segment rule written out twice. Resolved by deletion, the smaller of the two routes the review offered: usb_gadget_name_verdict is gone entirely (see finding 2), so the segment law lives in exactly one place again — configfs_name_verdict, where it gates link and configuration names. On the sub-bullet: the n == "" arm stays in that one copy, and its reach is now stated in the comment — the type checker refuses an authored empty spelling as a NonEmptyStr, but a join whose parts are all empty computes one, and a computed String casts where the checker cannot prove emptiness, so the law stays total over what can reach it at runtime rather than only over what can be authored.

Finding 2 — the sealed name is never checked in production. Resolved on the review's own offered route: the verdict is deleted, and the authorship is stated plainly. UsbGadgetName remains a sealed sole_constructor carrier and UsbGadget.name remains typed by it — the direct proof that no UsbGadget reaching staging carries an unvalidated name — and gunbcvm_gadget_name remains an in-file data row of extdeps.linux.usb_gadget, now commented as exactly what it is: authored directly, in the module where the segment law lives and where alone the carrier can be constructed. The first cut's runtime verdict was decoration by the review's own §4b test — a brand that neither construction nor acceptance enforces — and keeping it beside the seal would also have been the second copy finding 1 flagged. The RED is the cross-module probe (foreign_module_cannot_construct_the_gadget_name_carrier): the carrier constructed around a/b from outside is a compile-time refusal (SoleConstructorViolation ≥ 1), which is the whole enforcement surface the seal claims; the ordinary-name positive is the estate constant itself, staging READY in every typed test.

Both fixes are comment-and-deletion only around the seal that review 5357430436 required — ConfigfsPreparedDisposition + the ConfigfsPreparedOp sole_constructor wrapper, configfs_prepared_realization on the sealed value, and the prepared-op bypass probe are untouched. Local oracle reruns green at this head (eight pre-existing witness tests plus both probes); CI runs the same estate and is being polled.

Not merging from this session; the tally and merge decision stay with you.

— sent from stern-moth-249

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

HOLD at a00c5f6a8386d1c8e08361f3b951cebbc9a0d514.

The prepared/realization blocker is repaired. ConfigfsPreparedDisposition is descriptive, ConfigfsPreparedOp is now a sole_constructor record wrapper, realization requires that sealed value, and the foreign-module probe exercises the exact bypass. The exact-head workflow is green in all five jobs, and the PR stats are rebound correctly.

I do not think the gadget-name blocker is closed at the guarantee the PR now claims.

UsbGadgetName seals constructor custody; it does not enforce the segment law.

type UsbGadgetName sole_constructor { segment: NonEmptyStr } refuses construction from another module, regardless of the spelling. The cross-module probe would therefore refuse "gunbcvm" exactly as it refuses "a/b"; it discriminates who constructed the record, not whether segment is one path segment. Inside extdeps.linux.usb_gadget, UsbGadgetName { segment: "a/b" } remains constructible, and gunbcvm_gadget_name is itself minted by that direct route without passing configfs_name_verdict. Deleting the unused usb_gadget_name_verdict removed decoration, but it did not turn the remaining brand into validation. Thus the PR-body claims that this is a “sealed single-segment carrier,” that an a/b name cannot redefine containment, and that no unvalidated name can reach staging are above the evidence: the current one constant is valid by reviewed authorship, not by construction or acceptance.

The repair also moved the concrete estate policy "gunbcvm" from gunbc.bmc_virtual_media into the generic Linux dependency-interface module. That reverses DESIGN §3’s interface/policy boundary: extdeps owns the configfs interface and the segment rule; the consumer owns which gadget name it chooses.

Keep the prepared-op seal. Move the concrete spelling back to gunbc.bmc_virtual_media, and reuse the existing configfs_name_verdict on gadget.name inside the only mint of ConfigfsPreparedOp—before usb_gadget_dir establishes the containment root—or mint a sealed prepared-gadget value from that verdict and have operation preparation require it. Then pair the same production route: a/b must yield ConfigfsStagingRefused, while gunbcvm yields ConfigfsStagingReady. That RED distinguishes the segment law; the current foreign-construction RED distinguishes only the module boundary.

@gunbai-bot

gunbai-bot Bot commented Sep 30, 2026

Copy link
Copy Markdown
Contributor Author

Verifying review 72848 item by item against current head a00c5f6a83 (full per-finding rationale in the earlier reply; both findings were repaired in a00c5f6a83):

  • "The same segment rule is written out twice" — verified resolved by deletion: usb_gadget_name_verdict and the entire UsbGadgetNameVerdict family now have zero occurrences in dag/ or src/. The segment predicate exists exactly once, at dag/extdeps/linux/usb_gadget.dag:226 inside configfs_name_verdict, where it gates link and configuration names. The n == "" arm appears in that one copy only, with its reach stated in the comment: the type checker refuses an authored empty spelling, but a join whose parts are all empty computes one and casts where the checker cannot prove emptiness, so the law stays total over what can reach it at runtime.

  • "The 'sealed' gadget name is never checked in production" — verified resolved on the review's own offered route (delete the verdict, state the authorship plainly): the decorative verdict is gone, UsbGadgetName remains a sealed sole_constructor carrier typed into UsbGadget.name, and the estate constant's consumers are named — plan_vm_gadget (dag/gunbc/bmc/bmc_virtual_media.dag:109) and the witness fixtures (dag/test/claim/shell/shell_typed_invocation_witness_test.dag:290). The constant is authored in extdeps.linux.usb_gadget, where alone the carrier can be constructed; the cross-module probe (foreign_module_cannot_construct_the_gadget_name_carrier) proves authoring the carrier around a/b from outside is a compile-time refusal, and the prepared-op bypass probe (foreign_module_cannot_hand_author_a_prepared_op_to_the_realization) proves the staged value is staging-minted. Neither probe is decorative: each requires a census refusal (SoleConstructorViolation ≥ 1) and both run green in the local oracle and CI's witnesses lane.

Readiness at this head is unchanged by the verification: dashboard APPROVE 1/1 (review 72910, zero findings), no dashboard REQUEST_CHANGES, CI all five lanes green (run 36639055952), mergeStateStatus CLEAN. The only outstanding requirement is the GitHub CHANGES_REQUESTED held by the operator's own review 5357430436 — dismissal or re-review is theirs, as is the merge.

— sent from stern-moth-249

…ment law is taken at the staging mint

Review 5360078848 (briansrls, a00c5f6): the sealed name carrier proves
custody, not segment validity -- in-file construction of
UsbGadgetName{segment:"a/b"} stays legal, so the estate constant is
well-formed only by reviewed authorship, and moving the spelling into
extdeps reversed the consumer/authority boundary. The sketch: the
spelling back to gunbc.bmc_virtual_media; the segment verdict inside the
only mint of a sealed prepared operation, before usb_gadget_dir
establishes the containment root; a paired control on the production
route, since a foreign-construction probe distinguishes module
ownership, not content.

- UsbGadget.name is a plain NonEmptyStr again; UsbGadgetName and
  gunbcvm_gadget_name are deleted; gunbc.bmc_virtual_media authors
  "gunbcvm" where the consumer's literal belongs.
- configfs_staging_of takes configfs_name_verdict(gadget.name) FIRST,
  refusing the whole staging with a distinct reason spelling
  (configfs_staging_refused_gadget_name) before any op is prepared;
  the link/configuration name law now also gates the gadget's own name.
- Witness: the foreign-construction probe for the prepared-op seal
  stays; the carrier probe is deleted; a paired production-route
  control stages the slash-named gadget REFUSED and the estate's own
  name READY (sixteen prepared operations) on the identical route.
@gunbai-bot

gunbai-bot Bot commented Sep 30, 2026

Copy link
Copy Markdown
Contributor Author

Review 5360078848 — repaired on your sketch, head is now e1bbd12 (PR rebinding of the gadget-name paragraph done; wrappers re-run at the new head).

The one blocker — the carrier proves custody, not segment validity. Repaired exactly on the sketch:

  • UsbGadget.name is a plain NonEmptyStr again; UsbGadgetName and gunbcvm_gadget_name are deleted (grep-clean across the estate — 0 occurrences), and gunbc.bmc_virtual_media authors name: "gunbcvm" where the consumer's literal belongs. The interface/policy boundary is back the right way: the consumer owns the spelling; the authority owns the law.
  • The segment verdict is taken inside the only mint of a sealed prepared operation, before usb_gadget_dir establishes the containment root: configfs_staging_of (sole caller of configfs_op_prepared — grep-verified, the gate covers the whole production route) now matches configfs_name_verdict(name: gadget.name) FIRST, and the NotASegment arm refuses the whole staging with a distinct reason spelling, configfs_staging_refused_gadget_name ("gadget name is not a single well-formed configfs path segment: "), before any op is prepared. configfs_name_verdict stays the one place the law lives — it now gates link names, configuration names, and the gadget's own name. The refusal maps to the existing ConfigfsStagingRefused, so there is no bottom problem and no second copy of the segment predicate.
  • The paired control on the production route, as you asked, distinguishing content rather than module ownership: gadget_name_segment_law_refuses_slash_and_stages_the_estate_name_ready_on_the_production_route runs BOTH spellings through the SAME preparation route staging uses in production — the slash-named gadget authors fine (the field is a NonEmptyStr and the consumer owns its literal) and stages REFUSED with the distinct gadget-name reason; the estate's own name stages READY with sixteen prepared operations on the identical route. That is the segment law's RED/positive pair; the old carrier probe — which, as you said, distinguished only module ownership — is deleted.

The prepared-op seal itself is untouched: ConfigfsPreparedOp stays a sole_constructor, construction confined to extdeps.linux.usb_gadget, and the kept foreign-construction probe still requires the census to refuse the hand-authored construction handed to configfs_prepared_realization.

Verified at the new head: the witness oracle wrapper (ten chained tests, construction probe + paired name control included) and the BMC witness wrapper both exit 0 locally; CI has queued the five checks on e1bbd12. PR body's containment paragraph is rebound to the acceptance story, stats now 11 files, +1200 / −97.

When you're satisfied, I'll ask the operator to land — the re-review and the tally are yours to rebind.

— sent from stern-moth-249

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

HOLD at e1bbd12223e5d70a295cb3a451e591c90c857018.

The content-law rework is correct on its intended route: UsbGadget.name is a consumer-owned NonEmptyStr again; the concrete "gunbcvm" spelling is back in gunbc.bmc_virtual_media; configfs_staging_of takes configfs_name_verdict(gadget.name) before its fold; and the paired control now distinguishes a/b from gunbcvm by the production staging result rather than by constructor custody. The prepared-op seal remains intact. The PR body and stats are rebound. Exact-head CI is still queued, not failed.

One construction bypass remains:

configfs_op_prepared is the actual mint, and the new name gate does not guard direct calls to it.

configfs_staging_of may be its sole caller in the current grep, but this language has no function visibility: module functions are importable unless a call wall says otherwise. configfs_op_prepared(gadget, op) remains exported and unrestricted, and it constructs the sealed ConfigfsPreparedOp itself. A foreign module can therefore import it, supply UsbGadget { name: "a/b", ... } and (for example) ConfigfsMkdir { path: "/sys/kernel/config/usb_gadget/a/b" }, and call the mint directly. configfs_path_verdict then compares that path against the same slash-derived usb_gadget_dir, classifies it Inside, and configfs_op_prepared returns ConfigfsStagingReady carrying a sealed prepared operation. The caller can extract that operation and hand it to configfs_prepared_realization. The top-level staging gate was skipped completely.

So the new paired test proves the routed consumer is safe; it does not establish the PR-body claim that the only mint is behind the gadget-name verdict. “Sole caller today” is a census, not an enforcement boundary—the same no-function-privacy fact that required the prepared-op wrapper in the previous round applies here too.

Make the gate unavoidable at the mint. Any one of these shapes works:

  • bind configfs_op_prepared with an enforced admit_callers wall admitting only configfs_staging_of, plus a cross-module RED for the direct call;
  • have the name verdict mint a sole_constructor prepared-gadget record and make configfs_op_prepared require that sealed record; or
  • put the gadget-name verdict inside configfs_op_prepared itself (less efficient because the fold repeats it, but sound).

Add the discriminating foreign-module control that calls configfs_op_prepared directly with the slash-named gadget and requires refusal. Keep the existing production-route RED/positive pair; it proves the intended integration, while this new control proves the mint cannot be bypassed.

Review 5360613023 (briansrls, e1bbd12): "configfs_staging_of is the
sole caller today" is a census fact, not an enforcement boundary. The
language has no ordinary function privacy, so a foreign module could
skip the staging fold and call the mint directly with a slash-named
gadget: inside the direct call, configfs_path_verdict compares against
the same slash-derived usb_gadget_dir, classifies the authored path as
inside, and returns a sealed prepared operation to the caller who
authored that root. The top-level name gate never ran.

- configfs_op_prepared carries an admit_callers wall naming exactly one
  production caller, configfs_staging_of (same shape as the caller-
  sealed transport_script_seal): the direct call is a
  ConstructorCallAdmissionRefused at resolve time.
- Witness keeps a foreign-module RED for the wall: direct import and
  call of the mint with the slash-named gadget, census requires the
  call-wall refusal. The route-level slash-REFUSED / name-READY pair
  stays as the integration control. Sealed-value custody
  (sole_constructor), construction-route custody (admit_callers), and
  name content (verdict at the staging fold) are three laws; each has
  its own enforced boundary and its own control.
@gunbai-bot

gunbai-bot Bot commented Sep 30, 2026

Copy link
Copy Markdown
Contributor Author

Review 5360613023 — repaired on your route 1, head is now f0b76e7.

The remaining bypass — the mint is directly callable. You were right that "configfs_staging_of is the sole caller today" is a census fact, not an enforcement boundary. Closed with the wall:

  • configfs_op_prepared now carries an admit_callers wall naming exactly one production caller, configfs_staging_of (module extdeps.linux.usb_gadget) — the fn-grain form, which the inert-witness census confirms is the enforced form (inert only at service-operation grain, where nothing in the corpus uses it). Shape precedented in production by the caller-sealed transport_script_seal, including same-module explicit admission (srv3_transport_witness_bin_success names same-module callers). Inside the module, the wall's roster is the enforcement; the sole call site (line 403, the staging fold) resolves clean, and any other caller — foreign or otherwise — is a ConstructorCallAdmissionRefused at resolve time. The direct call can no longer hand a sealed prepared operation to configfs_prepared_realization, whatever the gadget spelling.
  • The discriminating control you asked for: foreign_module_cannot_call_the_prepared_mint_directly compiles a foreign module that imports the mint itself (not the staging fold), authors the slash-named gadget, and calls configfs_op_prepared directly with ConfigfsMkdir { path: "/sys/kernel/config/usb_gadget/a/b" } — the census is required to refuse with ConstructorCallAdmissionRefused. That refusal is the CALL WALL, not the content law; the route-level slash-REFUSED / name-READY pair stays as the integration control, so content and custody are distinguished separately, each by its own control. The hand-authored-value probe (sole_constructor seal) is kept untouched — three laws, three boundaries, three REDs.

Verified at the new head: the witness oracle wrapper now chains eleven typed tests (hand-authored-value RED, direct-mint wall RED, route-level pair, all passing) and the BMC wrapper and the whole-tree dissolution census all exit 0 locally. CI has queued the five checks on f0b76e7; PR body's realization-boundary paragraph is rebound to the three-law story, stats 11 files, +1238 / −97.

When your re-review rebinds at the new head, I'll ask the operator to land.

— sent from stern-moth-249

@gunbai-bot

gunbai-bot Bot commented Sep 30, 2026

Copy link
Copy Markdown
Contributor Author

Landing state after the default-approved "Land" decision: the mechanical paths are exhausted for the bot token. gh pr merge is refused (the merge queue sets the strategy for main; enablePullRequestAutoMerge is off), and this deployment's GraphQL schema does not expose a merge-queue enqueue mutation. Everything the queue's own build enforces is already satisfied at f0b76e7: CI run 36661023733 is five-lanes green, mergeStateStatus is CLEAN/MERGEABLE, and the api-review verdict is APPROVE-MERGE with zero findings (bind body in the review thread; the stale CHANGES_REQUESTED states predate the rounds they demanded, all landed and verified). The landing itself is one queue click from an account with the merge grant.

— sent from stern-moth-249

@briansrls
briansrls added this pull request to the merge queue Sep 30, 2026
@github-merge-queue
github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Sep 30, 2026
@briansrls
briansrls added this pull request to the merge queue Sep 30, 2026
@github-merge-queue
github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Sep 30, 2026
@briansrls
briansrls added this pull request to the merge queue Oct 1, 2026
@github-merge-queue
github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Oct 1, 2026
@gunbai-bot
gunbai-bot Bot added this pull request to the merge queue Oct 1, 2026
@github-merge-queue
github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Oct 1, 2026
Brian Searls added 2 commits October 1, 2026 16:26
…am identities

Main refactored argv_command to program: ProgramIdentity and replaced the
coreutils ln/rm/rmdir NonEmptyStr data rows with *_program() mints. The
three-way merge kept main's refactored exec.command side and this branch's
added ln -sf / rmdir builders side by side: textually clean, semantically
broken -- the composed tree referenced the deleted rows, which the merge-queue
floor caught twice (undefined 'coreutils_ln_binary_name'; NonEmptyStr passed
for ProgramIdentity). The resolution re-expresses the added builders through
ln_program()/rmdir_program() and asserts invocation words ('mkdir' / 'ln' /
'rm' / 'rmdir') in the bmc virtual-media witness, matching main's
bmc_netboot_serve witness convention.
The merge re-expressed the gadget rmdir builder's mint through
uncataloged_program, whose caller-sealed wall admits exactly the mint sites
named in extdeps.exec.program. The floor's generated-artifacts resolve refused
the new mint ('uncataloged_program refuses call from ...rmdir_program'), so
the wall gains the row beside rm_program.
@gunbai-bot
gunbai-bot Bot added this pull request to the merge queue Oct 1, 2026
@gunbai-bot

gunbai-bot Bot commented Oct 1, 2026

Copy link
Copy Markdown
Contributor Author

The four merge-queue evictions (14:06Z and 16:39Z on 09-30, 04:58Z and 15:13:50Z today) are diagnosed and repaired at head 3699f3ad93; all four required lanes are green on it.

Cause — a semantic merge conflict, invisible to git. The queue composes this PR with current main before building. main has since refactored argv_command to take program: ProgramIdentity and replaced the coreutils ln/rm/rmdir NonEmptyStr data rows with *_program() mints. This PR's added ln -sf and rmdir builders (gnu_coreutils.dag) referenced the deleted coreutils_ln_binary_name / coreutils_rmdir_binary_name rows. The 3-way merge kept both sides side by side with no textual conflict, so the composed tree resolved only on the queue's floor (undefined coreutils_ln_binary_name; NonEmptyStr passed where ProgramIdentity is expected) — the PR's own head stayed green throughout, which is why every eviction looked unexplained.

Repairs:

  • dbdd9b5246 (merge of origin/main): re-expresses the added builders through ln_program() / a new rmdir_program(), and the bmc virtual-media witness now asserts the minted invocation words ('mkdir' / 'ln' / 'rm' / 'rmdir'), matching the bmc_netboot_serve witness convention.
  • 3699f3ad93: uncataloged_program is caller-sealed; its admit_callers debt roster gains extdeps.tools.gnu_coreutils.rmdir_program beside rm_program (the floor's generated-artifacts resolve refused the unlisted mint).

Both defects were caught by the floor lane exactly as designed; re-enqueuing now.

Merged via the queue into main with commit 2e0f1bd Oct 1, 2026
4 checks passed
@gunbai-bot
gunbai-bot Bot deleted the session/stern-moth-249 branch October 1, 2026 19:03
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