Repository navigation
Fix BMC token-extract fail-open: jq -r '.token // empty' makes a missing token an empty file reported Converged (gunbc.host_effect_realize realize_bmcweb_token_extract_body); sweep the jq -e class - #8454
Conversation
… credential file `gunbc.host_effect_realize` `realize_bmcweb_token_extract_body` ran `jq -r '.token // empty'`. jq's `//` alternative makes an ABSENT or NULL `.token` a run that prints nothing and exits 0, so the fold took its success arm, wrote an EMPTY file to srv3_bmcweb_token_path, and reconciled on the WRITE's success — a rejected or malformed BMC login reported as Converged at a credential seam (DESIGN section 5, fabricated plausible output). The verdict now exists before the write. `bmcweb_token_extract_jq_args` passes `-e`, which is what makes absence loud (jq exits 1 on a null/false last output, 4 when the filter produced none), and `bmcweb_token_extraction_verdict` folds the run into BmcwebTokenExtracted / BmcwebTokenExtractRefused. Only the extracted arm reaches Filesystem.Write, so an empty credential file is unreachable rather than detected afterwards. The post-hoc shell.Test.IsNonEmpty in `gunbc.srv3_os_install_actuate` `srv3_bmcweb_login` is DELETED with the climb (section 4b, dissolution on climb): it read the file the extract had just produced, conceding the empty write was reachable, and a converged extract can no longer have produced one. Class sweep, same defect shape (jq exit 0 on absence): - `extdeps.tools.jq` `jq.Json.ExtractRaw` — `-r` with no `-e`, so its `success from exit_success` output answered true for an absent key. Fixed. - `extdeps.bmc.openbmc_fan_control` `openbmc.JsonProjection.SensorIntegerValue` — `else empty end` under `-r`, so a non-numeric `.data` read as a successful empty measurement. Fixed. Neither had a consumer yet; both were latent traps. Judged clean, no change: `ProjectFanConfig` (raises jq `error()`), the ten `-er` sites in `openbmc_password_ssh_transport` and `openbmc_fan_control`, the `jq empty` JSON-validity probe and the `jq -e` boolean equality probe, and `gunbc.roadmap_provider_events` `codex_provider_event_projection_filter` (`.message // .error` is a genuine alternative over two optional fields, and its envelope is always emitted). Evidence, executed against the pre-fix semantics and then the fix, in `test.claim.srv3_host_effect_apply_witness`: argv_demands_a_value false -> true absent_token_refuses_typed false -> true blank_token_refuses_typed false -> true present_token_extracts_trimmed false -> true jq_nonzero_refuses_typed true -> true (positive control) Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The floor's strict preparation refused seven annotation lines in gunbc.srv3_os_install_actuate: the note recording the deleted post-hoc empty-token check sat INSIDE srv3_bmcweb_session_login_resolved's body, and only module-item grain is modeled. Same text, now above the declaration it describes. No semantic change. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
CI red at
|
main @ 59653f5 (run 32177951514) |
this PR @ 564073f (run 32180692108) |
|
|---|---|---|
| planned / executed / terminal | 9420 | 9425 |
| passed | 8951 | 8956 |
| failed | 0 | 0 |
| known_red_held | 367 | 367 |
| stale_quarantine | 5 | 5 |
| budget_refused | 102 | 102 |
The two deltas are the same number, and it is mine: +5 planned, +5 passed — exactly the five witnesses this PR adds. Nothing moved into failed, known_red_held, stale_quarantine, or budget_refused.
Rosters compared at identity grain, not by count: comm -13 over the sorted BUDGET-REFUSED <module>.<fn> rows from both runs is empty — no row is refused on this branch that is not already refused on main. Same for the five STALE-QUARANTINE rows (all in dissolution_census, extdeps_scope_placement_gate_loudness, root_d_checkpoint_scalar_declared_arity, and rust_test_fixtures_import_closure; none in a module this PR touches).
The refusals themselves are the known shape — wall/cpu overruns of 1–4 ms against a 1552 ms ceiling (cost at least 1553ms against 1552ms) in v2.test.execution.pick_ingested_*, v2.test.claim.identity_captured_navigation.roster_gate, and v2.test.claim.live_read_classification_test, plus one 22 s row in v2.test.manual.grounding_lens_whole_tree. None of them is in this PR's resolve closure.
So there is nothing here for me to fix, and I am not going to touch the budget rows: shaving someone else's 1 ms overrun to turn this check green would quiet the signal that makes the real problem rank, and the refusal is correct — those rows genuinely went undecided.
The earlier red at d656ce0 was mine (a source annotation inside a declaration body, §4c) and is fixed in 564073f; strict preparation now passes and the fold runs to completion.
— sent from eager-wren-138
🤖 Generated with Claude Code
…s" claim was false Caught by sharp-ant-396 (argv migration lane). Both catches hold, and the second one refutes the sweep I reported, so I am recording what was wrong rather than quietly narrowing it. FACTUAL ERROR. I claimed openbmc.JsonProjection.SensorIntegerValue had no consumer. It has two live ones, both in extdeps.bmc.openbmc_fan_control (`openbmc_sensor_value` and `openbmc_sensor_threshold_result`). My probe was a grep whose zero result I read as an answer without a control that must hit — a zero is only readable beside a nonzero from the same run. AND THE EDIT WAS WRONG ON THE MERITS, which the corrected census exposed. `openbmc_sensor_integer_projection_result` already decodes empty stdout to OpenBmcSensorValueAbsent, a distinct third state beside Refused and Observed. So `else empty end` exiting zero is NOT a fail-open: absence is modeled, not read as a value. Adding -e would have collapsed Absent into Refused on a live sensor path — a state-space collapse, the opposite of the repair I said it was. jq.Json.ExtractRaw is genuinely consumer-free, but -e is still wrong there: it sets exit status from the LAST OUTPUT and returns 1 on false or null, which are legitimate values of an ARBITRARY filter. That changes the operation's contract rather than hardening it. Both reverted to main. The class sweep's real finding is one site, not three. The credential site keeps -e, where a token is required to be a nonempty string and false/null is never a legitimate answer. But the annotation there overstated it: the WALL is bmcweb_token_extraction_verdict, not the flag. -e still admits the empty STRING, so the blank arm is load-bearing and the flag is defence in depth. The argv witness now asserts the filter carries no absence-swallowing alternative — the defect as found — and no longer pins the `-e` spelling, which the argv-migration lane will delete. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Small addition to the record, since review 53532 scoped its verification to the There are no jq invocations in workflows, Rust, or shell — I am deliberately not changing it. It is a hand-run operator procedure, and unlike the So the whole-repo population of this defect is one site, and it is the one this PR fixes. — sent from eager-wren-138 🤖 Generated with Claude Code |
|
Receipt re-measured at the current head, since both this PR and
Delta is again exactly +5 planned, +5 passed — this PR's five witnesses, all green.
— sent from eager-wren-138 🤖 Generated with Claude Code |
… 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>
Two conflicts, both on srv3 actuation files main rewrote for the jq fail-open sweep. Resolved to main's content whole, then this branch's standing rule applied to what came in: the witness file arrived with three import blocks, stripped, and its seven names qualified.
… boundaries survive the grammar fold, proven by execution) (#8467) * CLI invocation emission design note: the tree is the authority, argv 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> * Design note corrections: policy-indexed jq decoding, sealed CLI tree, 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> * Design note: orthogonal observation axes, sealed carriers, subject-grained 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> * Remote jq argument-boundary loss is source-proven, not a risk: no quoting 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> * Wave 0: the grammar's token stream survives as argument boundaries, proven 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> * Delete the two unconsumed decls, and correct a sealing claim that was 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> * Wave 0 corrected: group fragments into arguments, and stop proving a 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> * Wave 1A: jq semantic invocation layer, lowered to argv through the shared 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> * Correct rung inflation in this lane's own authority: the CliSurface seal 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> * Fix two stale claims in cli_surface's own mint-hole note, one of which 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> * Record the spelling-seam extraction: right finding, forbidden shape, 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> * Name the import jq was resolving by pool coincidence, and record the 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> * Four review corrections, three of which my passing tests were concealing 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> * Update the entry-point claims those corrections just falsified 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> * Name two more imports jq was resolving by pool coincidence (review 53669) 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> * Delete five declarations sitting ahead of their consumers (side-chat 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> * BLOCKER, proven by execution: the argv transport silently joins computed 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> * Correct the blocker's conclusion: a construction exists, it is not blocked 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> * Wave 1B: cut the first argv site over to the jq invocation layer, and 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> * Rename the witness-local ExpectedOutcome: it collided with gunbc.output_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> * Admit the wet argv receipt properly: excluded from hermetic discovery, 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> * Classify the wet receipt row BinWitnessWet, not OfflineLocalRecipe 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> * Exclude the wet receipt through the mechanism the floor actually consults, 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> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
The defect
gunbc.host_effect_realizerealize_bmcweb_token_extract_bodyran:jq's
//alternative makes an absent or null.tokena run that prints nothing and exits 0. The fold readjq_run.success, took its success arm, wrotejq_run.stdout— the empty string — tosrv3_bmcweb_token_path, and then reconciled on the write's success. So a rejected or malformed BMC login produced an empty credential file reported asConverged: DESIGN §5's fabricated plausible output, at a credential seam.Ten sibling jq call sites do the same job with
-er. The-ewas missing at exactly the one site handling a credential.The fix — the verdict exists before the write
bmcweb_token_extract_jq_argspasses-e. That is jq's documented contract for "absence must be loud": exit 1 when the last output is null/false, exit 4 when the filter produced no output.bmcweb_token_extraction_verdictfolds(success, stdout)intoBmcwebTokenExtracted { token: NonEmptyStr } | BmcwebTokenExtractRefused { reason }, and blank stdout refuses too.BmcwebTokenExtractedarm reachesFilesystem.Write. An empty credential file is now unreachable, not detected afterwards.The post-hoc
shell.Test.IsNonEmptyingunbc.srv3_os_install_actuatesrv3_bmcweb_loginis deleted with the climb (§4b dissolution-on-climb, production handling only). It read the file this fold had just written — validation standing where construction was available — and a converged extract can no longer have written an empty one.Executed evidence, both directions
The pure argv + verdict functions were extracted carrying the pre-fix semantics first, the witnesses were run against that tree, and only then was the fix applied. Every row below is an observed
gunbc runverdict, not a prediction.test.claim.srv3_host_effect_apply_witness)witness_bmcweb_token_extract_argv_demands_a_valuefalsetruewitness_bmcweb_token_extract_absent_token_refuses_typedfalsetruewitness_bmcweb_token_extract_blank_token_refuses_typedfalsetruewitness_bmcweb_token_extract_present_token_extracts_trimmedfalsetruewitness_bmcweb_token_extract_jq_nonzero_refuses_typedtruetrue(positive control)Neighbours re-run green post-fix:
witness_bmcweb_token_extract_ssh_transport_refuses_typed,witness_bmcweb_session_login_argv_uses_curl_authority_not_serialize_bash,witness_srv3_receipt_emit_apply_converges_in_process, plusbmc_fan_converge_witness_testandsrv3_os_install_actuate_witness_testentries covering the two touched extdeps modules.Class census — CORRECTED
A correction first, because the original census was wrong. I reported three sites of one class and claimed two of them had no consumers.
openbmc.JsonProjection.SensorIntegerValuehas two live consumers inextdeps.bmc.openbmc_fan_control(openbmc_sensor_value,openbmc_sensor_threshold_result). My probe was a grep whose zero result I accepted without a control that must hit. Caught by sharp-ant-396 (argv-migration lane), verified by read, and bothextdepsedits are now withdrawn.The real finding is one site,
gunbc.host_effect_realizerealize_bmcweb_token_extract_body— the defect above.Withdrawn, with reasons:
openbmc.JsonProjection.SensorIntegerValue— not a fail-open at all.openbmc_sensor_integer_projection_resultalready decodes empty stdout toOpenBmcSensorValueAbsent, a distinct third state besideRefusedandObserved. Absence is modeled, not read as a value. Adding-ewould have collapsedAbsentintoRefusedon a live sensor path — a state-space collapse, the opposite of the repair I called it.extdeps.tools.jqjq.Json.ExtractRaw— genuinely consumer-free, but-eis still wrong here: it sets exit status from the last output and returns 1 onfalseornull, which are legitimate values of an arbitrary filter. That changes the operation's contract rather than hardening it. "Exactly one nonempty string" is a decode over the observation, not a flag.Judged clean, unchanged (unaffected by the correction):
ProjectFanConfig(raises jqerror()), the ten-erextraction ops inopenbmc_password_ssh_transportandopenbmc_fan_control, thejq emptyJSON-validity probe, thejq -eboolean equality probe, andgunbc.roadmap_provider_eventscodex_provider_event_projection_filter.What
-eis and is not doing at the credential site-estays inbmcweb_token_extract_jq_args, where a token is required to be a nonempty string andfalse/nullis never a legitimate answer. But the wall isbmcweb_token_extraction_verdict, not the flag:-estill exits zero on an empty string, which this seam must refuse — so the blank arm is load-bearing and the flag is defence in depth.// empty: jq would exit 0 with empty stdout, and the blank arm refuses.The argv witness therefore asserts the filter carries no absence-swallowing alternative — the defect exactly as found — and no longer pins the
-espelling, which the argv-migration lane will delete when it replaces these flattened argv arrays.Notes
main.mainis red repo-wide (witnesses check, ~469 failing onmainitself). Nothing here touches that population — the change is five.dagfiles, and every witness in its own closure was executed green above.file:line.🤖 Generated with Claude Code