From 128c8058461b5cbcedca555ba533a891fa83997f Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 18 Aug 2026 22:11:36 +0000 Subject: [PATCH 01/23] 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 -> 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) --- docs/plans/cli-invocation-emission-design.md | 509 +++++++++++++++++++ 1 file changed, 509 insertions(+) create mode 100644 docs/plans/cli-invocation-emission-design.md diff --git a/docs/plans/cli-invocation-emission-design.md b/docs/plans/cli-invocation-emission-design.md new file mode 100644 index 00000000000..850835778c8 --- /dev/null +++ b/docs/plans/cli-invocation-emission-design.md @@ -0,0 +1,509 @@ +# CLI invocation emission — the tree is the authority, argv is emitted + +**Status: DESIGN NOTE. No code lands from this note yet.** Design-note-first, per the +hollow-alias precedent. The first vertical is specified here; nothing is built until the +note is accepted. + +**Lane:** supersedes the Lane B destination of `gunbc.plans.transport_argv_anemia_dissolution`. +That plan's *diagnosis* stands — "the model is the request; the curl argv is one derived +realization of it" — and its Lane A (HTTP → `transport rest`) is substantially right. Its +Lane B destination is wrong: it terminates at typed `extdeps/tools/*` operations and +`ArgvCommand` builders, both of which still contain literal argv. The plan therefore stops +one layer short. + +--- + +## 1. The defect + +An invocation is authored today as a list of opaque strings: + +``` +argv: ["jq", "-er", "--argjson", "index", "{index}", ".data[0] | keys | .[$index]"] +``` + +Three independent facts are welded into that one list: + +1. **what jq is** — a program operand, a raw-output mode, typed variable bindings, an exit policy; +2. **how we reached it** — locally, or over `sshpass`+`ssh` to a BMC; +3. **what we asked it** — an OpenBMC-specific projection over fan PID zones. + +Because they are welded, every new question is a new hand-typed list, and each list +re-decides all three. The consequence is not stylistic. A flag nobody modeled is a flag +that is trivially droppable, which is how `--fail` went missing from eleven curl sites and +made a 401 read as success. + +### The census (measured in-tree, not inherited from the plan) + +| fact | count | +|---|---| +| `argv:` lines | 597 across 129 files | +| `transport shell` blocks | 250 | +| `transport rest` blocks | 95 | +| `operation` declarations | 322 | +| operations declaring `success: Bool from "exit_success"` | 173 | +| operations declaring `exit_code: Int from "exit_code"` | 69 | +| `shell_quote` call sites | 36 | +| argv lines with a literal program head | 282 | +| …of those, heads that are **wrappers**, not tools | 78 | +| `sh -c` / `bash -c` embedded-language leaves | 14 | + +Two precision bounds: 315 of 597 argv lines have computed heads and are unclassifiable by +this method, so 78 is a **lower bound** on wrapper-hidden tools; the metacharacter count is +a text match, not a parse. + +**The plan's own census is stale by ~2.3×** — it records 262 argv lines across 37 files, and +148/51 for the success/exit_code split. Both measured above. + +### The census cannot currently be taken + +Counting by argv head yields `git` 43, `sshpass` 40, `sh` 13, `sudo` 9, `env` 9. The middle +four are not tools; they are wrappers, and the real program sits at some positional offset +inside the list. All seventeen jq-over-ssh sites count as `sshpass`, not as jq. + +This is itself the argument. Tool identity is a positional accident inside a flat string +array, so the corpus cannot answer "what do we invoke" without knowing that `argv[11]` is +the real program because `argv[0..10]` happened to be an ssh prefix. + +--- + +## 2. Facts, separated by kind + +### 2a. Substrate facts (read from source) + +- `v2.std.compilers.target_model` `TargetModel` is target-agnostic in its bundle/lex/spellings + shape, but **text-specialized** in three fields: `binding_spellings: Map`, + `token_class_emit_transforms: Map String>`, `authority_source_text: String`. +- The emit carrier is `v2.std.compilers.target_model` `TargetText { source: String }` — one + String→atom introduction, concatenation as the only join, whole-value render as the only exit. +- `v2.extdeps.formats.sql_target` proves a **non-programming-language** target registers through + `target_model_make_with_emit_transforms`. It does **not** prove carrier independence: its + serialization node is still source-text shaped. +- The public emit seam commits to `Medium`. `Medium` itself is generic; the text lock + is in `TargetModel`, `serialize_target` and `emit`, not in `Medium`. +- `dag/extdeps/languages/` holds 32 language authorities. **None is a CLI-invocation authority.** +- `extdeps.exec.command` renders argv as `join(map(argv, shell_quote), " ")`, and is anchored to + the **SSH** manual while defining `curl`, `mkdir`, `tar`, `make`, `sed`, `cp` builders — plainly + a cross-tool realization utility, not the authority for those tools' semantics. +- `v2.std.host_transport` `ProcessInvocation` / `InvocationArg` exist with 72 consumer references. +- `v2.extdeps.posix` `Command`, `PosixArgument`, `SpawnProcessRequest` exist with **zero consumers + outside the declaring module**. +- `extdeps.posix.shell_command_language` exists as its own subject. +- `gunbc.command_runner` carries `command_runner_scaffold: Disposition = Scaffold`. + +### 2b. Upstream authority facts (cited) + +- **IEEE Std 1003.1-2024, Base Specifications Issue 8, §12** — 14 numbered Utility Syntax + Guidelines; `--` ends options; options precede operands (G9); `-` denotes stdin (G13); + option grouping behind one `-`; option-arguments as separate tokens. +- **POSIX `sed`** declares an explicit deviation: the relative order of `-e` and `-f` is + significant. So POSIX is the *base* grammar, never the whole tool grammar. +- **RFC 4254 §6.5** — the SSH `exec` channel request carries a single `command` field of type + **string**. No argv vector exists in the request, so argv structure cannot cross that boundary + as structure. The protocol does *not* define that string as shell source; shell re-parse is an + OpenSSH implementation fact, as `extdeps.ssh.session` already records. +- **IEEE Std 1003.1 Shell Command Language** — grounds the shell leg. Already cited by + `extdeps.posix.shell_command_language`, whose own note reserves it for exactly this use: + a POSIX-shell target "registers against THIS declaration and needs no new grounding." +- **jq manual** (`jqlang.org/manual/`) — `--raw-output`/`-r`, `--exit-status`/`-e`, + `--argjson name JSON-text`, `--arg name value`, `--` terminator, file operands vs stdin. +- **RFC 7950 (YANG 1.1)** — abstract data model held separate from concrete encoding; one model + renders as NETCONF XML or RESTCONF JSON. Cisco IOS XR ships "Model-Driven CLI" on that basis. + Prior art: the networking industry ran this exact migration from CLI-scraping to modeled trees. +- **PowerShell 7.6** — parameters bind to typed .NET objects; parameter metadata (`Position`, + `Required`, `Accepts multiple values`, `Accepts pipeline input`) is machine-readable. Evidence + that a per-tool option table can be data rather than prose. + +### 2c. Domain facts discovered during design (these constrain the model) + +- `extdeps.bmc.openbmc_fan_control` declares `OpenBmcSensorValueAbsent` — a **third state** + beside Refused and Observed. `openbmc_sensor_integer_projection_result` decodes empty stdout + to it, and `dag/test/claim/bmc_typed_operations_witness_test.dag` witnesses it. + **jq producing no output is a modeled value, not an error.** Any exit partition folding + "no result" into failure breaks working, witnessed code. +- `gunbc.host_effect_realize` `bmcweb_token_extraction_verdict` refuses blank stdout on its own. + So at that site `-e` was never the mechanism; it is transport *loudness*. +- Of the four jq operations in `openbmc_fan_control`, **all are live**: + `ProjectFanConfig`, `ObjectMapperServiceCount`, `ObjectMapperServiceAt`, `SensorIntegerValue`. + Only `extdeps.tools.jq` `jq.Json.ExtractRaw` is zero-consumer tree-wide. + +--- + +## 3. The layering + +A layer is only real if something varies at it. Checked against three CLI families: + +| layer | owns | POSIX | PowerShell | Cisco | +|---|---|---|---|---| +| **intent** | the tree: subject, named params, operands | *identical across all three* | +| **vocabulary** | which params exist, types, cardinality, positional, exclusivity | tool's manual | cmdlet parameter metadata | YANG module | +| **surface grammar** | how a bound param renders | `-a`, `--long=v`, bundling, `--` | `-Name value` / `-Name:value` | keyword paths in a mode hierarchy | +| **value encoding** | how a typed value becomes a param value | bytes; nested languages embedded | .NET objects — no serialization | typed per YANG leaf → XML/JSON | +| **carrier** | what the emitted thing physically is | argv vector *or* shell text | in-process object pipeline | NETCONF RPC document | +| **transport** | where it runs | local exec, ssh, enable-mode session, REST | + +The families agree completely at *intent* and disagree at *surface grammar*, *value encoding* +and *carrier*. That is what makes intent the authority and everything below a rendering. + +### Two consequences + +**Carrier ≠ surface grammar.** Emitting to shell text when the destination is `execve` invents +a quoting problem that does not exist. `shell_quote` at 36 sites is the current mitigation for +that conflation, not a requirement. + +**Value encoding nests.** A jq program is itself a language embedded as a leaf in a POSIX +argument. So is `sh -c` — 14 sites. A nested-language leaf should be a typed sub-tree, not an +opaque String. Modeling jq's *expression* language is a separate vertical from modeling its +*invocation* structure, and is explicitly not a prerequisite here. + +--- + +## 4. The model + +``` +JqInvocation semantic axes only; no flag spellings reachable + | + | jq cited option rows + shared CLI grammar rows + v +CliInvocationTree options grouped with their values; operands; terminator + | + | emission — roles erased here, correctly + v +List argument boundaries structural; no quoting + | + +-- local: tool resolution -> extdeps.posix Command -> spawn + | + +-- ssh: -> shell simple-command tree -> shell text -> RFC 4254 command string +``` + +### 4a. Semantic layer + +``` +type JqProgram { source: NonEmptyStr } // opaque, upstream-grounded, for now + +type JqBinding + = JqJsonBinding { name: NonEmptyStr, value: Json } + | JqTextBinding { name: NonEmptyStr, value: String } + +type JqInput + = JqInputFile { path: FilePath } + | JqInputStdin { content: String } + +type JqOutputEncoding = JqJsonText | JqRawText + +type JqExitPolicy = JqProgramExit | JqLastResultTruthiness + +type JqInvocation { + program: JqProgram + bindings: List + input: JqInput + output_encoding: JqOutputEncoding + exit_policy: JqExitPolicy +} +``` + +`JqInput` is where stdin stops pretending to be an option: `JqInputFile` produces one file +operand, `JqInputStdin` produces **no operand** and sets process stdin. That split is load-bearing +here — the four local sites are stdin-fed, the seventeen remote ones are file-operand. + +### 4b. Observation, decoded once + +``` +type JqExit + = JqExitedZero + | JqLastResultFalseOrNull + | JqProducedNoResult + | JqExecutionRefused { code: Int } + +type JqObservation { exit: JqExit, exit_code: Int, stdout: String, stderr: String } +``` + +`JqProducedNoResult` is its own arm because of the `OpenBmcSensorValueAbsent` specimen: absence +is a live, witnessed, modeled value. jq owns exit-code *decoding*; the domain owns whether that +outcome satisfies its contract. "Exactly one nonempty string" is a domain decode, not a jq flag — +and it is strictly stronger than `-e`, which still admits the empty string. + +**No `success: Bool`.** The seed derives it as exactly `exit_code == 0`, so the pair carries one +fact twice and makes a contradiction writable — a caller can pass `success: true` beside a nonzero +code. `extdeps.git.git` `ls_remote_reports_termination_not_success_note` already establishes this +and names itself the first consumer of the correction. 173 operations still carry the Bool. + +### 4c. Two-level row derivation — the keystone + +Both the **selection** of an option and its **spelling** must be row-derived: + +``` +JqLastResultTruthiness -> JqCliOptionExitStatus (prevents omission) +JqCliOptionExitStatus -> canonical "--exit-status", alias "-e" (prevents bespoke spelling) + +JqJsonBinding { name, value } + -> [ argument "--argjson", argument emit(name), argument emit(value, Json) ] +``` + +If only the second level is data-driven while a function still says "when policy is X, append +option Y," the droppable-option class survives one layer down. That is the difference between +this design and centralizing 597 literals into N helper functions. + +So the precise statement replacing "`-e` is part of the contract, not a flag" is: + +> `JqLastResultTruthiness` is part of the contract. `-e` and `--exit-status` are concrete +> spellings of that property in the jq CLI realization. + +### 4d. Grammar decomposition + +``` +shared CLI grammar option, option-argument, operand, repeated group, + terminator, short-option cluster, long spelling, + joined vs separate value + ++ per-tool cited rows jq options and operand order + sed's -e/-f ordering exception + git subcommand grammar + tar mode-word grammar + ssh -o forms +``` + +Named `CliSyntax`, not `PosixCli`: real tools deviate, POSIX `sed` provably so, and the name +should not assert conformance the corpus cannot claim. + +### 4e. The structured CLI tree — why roles live here and not in the arg vector + +``` +type CliElement + = CliOption { option: CliOptionRef, values: List } + | CliOperand { value: CliValue } + | CliOptionTerminator +``` + +An option's values cannot detach from their option: `--argjson`, its binding name and its JSON +value stay one subtree until the grammar lowers them. + +**Role and provenance are orthogonal axes and must not share a coproduct.** A workspace path may +be an option value *or* an operand; a produced artifact may be either; a literal may be an option, +subcommand, option value, mode word or operand. Fusing them makes `OptionValue ∧ WorkspacePath` +unrepresentable, and expanding to `WorkspacePathOptionValue`, `WorkspacePathOperand`, … is exactly +the combinatorial growth the grammar exists to remove. + +Roles are then **deliberately erased** at emission, because the operating system receives an +ordered vector of strings. That erasure is emission, not anemia. The present defect is only that +no preceding tree exists — authors write the vector directly. + +### 4f. Carrier: argv is native, text is the derived special case + +POSIX utility syntax operates over *arguments*. Shell syntax is the preceding language that turns +words and expansions into those arguments; quote removal happens before the utility sees them. +Therefore the argv vector is the higher-structure carrier and shell text is a serialization of it +through an additional language. + +Making text canonical and re-deriving argv by parsing would be backwards: it forces the strongest +local transport through an unnecessary shell grammar, quoting discipline and injection surface, +because one weaker remote transport loses structure. + +**Local and SSH are not two jq targets.** They are one utility target, two realization carriers, +and one *additional nested target* on the SSH path — the POSIX shell grammar, whose quoting and +parsing rules are modeled independently and are already grounded by +`extdeps.posix.shell_command_language`. + +The counterfactual that proves command text is not intrinsic: a remote receiver accepting a +structured request and calling `execve` itself would eliminate the shell leg while keeping SSH +as transport. + +**Existing precedent for the composition shape:** `effect_plan_bash_materialize` already obtains +an argv vector, converts it to Bash command nodes, then serializes the Bash grammar. Its argv +source is still the old declaration-owned materializer, but the shape is right. + +### 4g. Physical layer + +Lower into `v2.extdeps.posix` `Command` / `PosixArgument`, **not** `v2.std.host_transport` +`ProcessInvocation`. The latter is an emit-harness carrier whose `InvocationArg` variants +(`LiteralArg | WorkspacePath | ProducedArtifact`) classify build-workspace provenance, not CLI +roles; `build_transport_admission` only ever asks whether a step reads a declared workspace +resource, and `emit_host` flattens all three variants back to text. + +Evidence that its provenance vocabulary is hand-applied rather than derived: `python.dag` models +its script as `WorkspacePath`, `go.dag` models `main.go` as `WorkspacePath`, and `c.dag` models +`fixture.c`, `-o` and `fixture` as three undifferentiated `LiteralArg`s — so C's compiler read of +`fixture.c` is invisible to the admission fold. That is a real existing harness defect, and an +independent reason not to promote this carrier to the universal process boundary. + +`ProcessInvocation` is also missing process-wide axes already needed elsewhere: **no environment, +no stdin, no working directory, no file-descriptor mapping.** That omission has already been +discovered independently and forked around: `extdeps.llm.cursor_cli` minted its own +`CursorProcessInvocation { program, argv, environment }` rather than reuse it, and its note states +the general principle with a security consequence attached — + +> an argv is not a process. A process is a program, an argv AND an environment, and a credential +> passed by environment is invisible in a model whose output stops at the argv — there was no +> field for it to appear in. + +A fork in `dag/extdeps/llm` against a carrier in `src/v2/std` would not have been necessary if +`host_transport` `ProcessInvocation` were the general authority its name suggests. That is +independent corroboration of the name collision, arrived at by a different lane for a different +reason. + +**What `ProcessInvocation` remains good for.** It is not deleted by this lane. It stays as a +downstream adapter for the emit-host harness — fixed option spelling to `LiteralArg`, workspace +file operand to `WorkspacePath`, generated binary operand to `ProducedArtifact` — so the harness +keeps its effect provenance *after* CLI emission. Two constraints: no jq or domain caller +constructs those variants directly, and jq does not route through the emit-host harness merely +because that type already exists. The honest longer-term cleanup is renaming it and +`InvocationArg` to name their real scope (`EmitHostProcessInvocation`, +`EmitHostArgumentMaterialization`), which is a separate replacement migration and explicitly not +bundled here. + +`v2.extdeps.posix` `Command` is the right conceptual layer, with four bounded deficiencies: + +1. `program: AbsolutePath` — a semantic invocation names a *tool*; resolution must produce the + path at realization time. +2. no stdin or file-descriptor actions on `Command`/`SpawnProcessRequest`. +3. `PosixByteString = FreeMonoid` does not visibly exclude embedded NUL, which POSIX + process arguments require. +4. no executed proof that the active `dag/` lane can consume this `src/v2` carrier. + +--- + +## 5. Ownership + +| owner | owns | +|---|---| +| `extdeps.tools.jq` | what raw output means, what exit-status mode means, that `--argjson` takes a name and a JSON value, which options repeat, how jq spells them | +| shared `CliSyntax` | option/value structure, repeated options, operand ordering, separators, canonical short/long spelling, emission to argument tokens | +| `gunbc.bmc_fan_projection` | the `TEMP_SOC` policy, the fan curve, controller cardinality, the desired topology | +| `extdeps.bmc.*` | programs projecting a documented OpenBMC response or config field | +| realization | local vs SSH vs another handler | +| **no caller** | `-e`, `-r`, `--argjson`, `--`, or their positions | + +Filters leave both `extdeps.tools.jq` (business policy in extdeps is a layer inversion) and +`openbmc.PasswordSshTransport` (SSH does not own what the remote program means). They do not all +land in one generic "workflow layer": policy-bearing ones go to `gunbc.bmc_fan_projection`, which +already owns the board, firmware, curve, config path, controller entry and tach inputs. + +--- + +## 6. Rules + +1. `-e`, `-r`, `--argjson`, `--` and their aliases may appear **only** in cited concrete-syntax rows. +2. Semantic modules construct no option node and no argv string. +3. Per-tool lowering contains no bespoke option-selection fold; semantic variants select grammar + rows exhaustively. +4. Transport consumes an inner invocation. SSH may **not** be modeled as `append(ssh_prefix, inner.argv)`. +5. The CLI inverse consumes `List`, not shell text. Shell text is parsed by the shell + grammar first; only a static literal simple command projects back to a CLI surface. +6. Every vertical deletes its prior argv authoring site **in the same cut**. "New tree plus old + helper for compatibility" creates two authorities. +7. No new production function returns `List` or `ArgvCommand` containing tool flag literals. +8. `ArgvCommand` builders and `transport shell { argv: [...] }` are migration substrates, not the + final authority. + +--- + +## 7. The cut + +Per the §3 replacement-migration rule, stated at exact identity grain. + +**Authority being replaced:** argv-as-authored-authority for jq invocations. + +**Root consumer × subject population:** the four live `openbmc.JsonProjection` operations +(`ProjectFanConfig`, `ObjectMapperServiceCount`, `ObjectMapperServiceAt`, `SensorIntegerValue`) +plus the seventeen `openbmc_password_ssh_transport` remote jq operations. + +**First vertical (smallest complete):** + +1. `JqInvocation` and its semantic axes. +2. `CliInvocationTree`. +3. Shared CLI grammar rows + jq's cited option rows. +4. Emission to `List`. +5. Local resolution into `extdeps.posix` `Command`. +6. A process-input realization for jq stdin, separate from argv. +7. The SSH handler: emitted arguments → shell simple-command tree → shell text → RFC 4254 string. +8. One live jq population cut over, with its prior argv authoring site deleted. + +The carrier lands **with** its first live consumer, or in an immediately preceding stacked PR that +already contains an executing consumer. A standalone carrier PR with no consumer would reproduce +the current unconsumed `v2.extdeps.posix` situation exactly. + +**Deleted at cutover:** `extdeps.tools.jq` `jq.Json.ExtractRaw` (zero consumers — deleted first, +not kept beside the new authority); the migrated sites' `transport shell` argv literals; the +seventeen re-inlined `sshpass`/`ssh` prefixes. + +**Explicitly NOT in this cut:** adding variants to `InvocationArg`; updating its 72-reference +population; renaming the harness carrier to `EmitHostProcessInvocation`; repairing the C/Go/Python +descriptor inconsistency; making `HostTransportDescriptor` a general process authority; modeling +jq's expression language; the other 575 argv lines. Those are independent lanes. + +**Deliberately not built:** a coverage lens over argv arrays. Under the replacement-migration +rule that is a census over a structure being deleted — the deletion is the census, since every +real dependent refuses loudly. The plan proposes one; this note declines it. + +--- + +## 8. Witnesses + +Semantics and serialization are witnessed separately: + +- **semantic** — the caller requested the correct jq behavior. +- **emission** — that semantic tree lowers to the expected argument vector. +- **perturbation** — changing the jq option row changes or refuses the emitted vector. This is + the control that proves the rows are load-bearing rather than decorative. +- **domain** — absent, null, false, blank, wrong-type and multiple outputs cannot reach the write. +- **positive control** — one valid token still does. +- **absence control** — a non-numeric sensor reading still decodes to `OpenBmcSensorValueAbsent` + and does not become a refusal. + +--- + +## 9. Rung, honestly + +At the end of the first vertical the class sits at **mechanically preventable**, not structural: +a caller can still construct a raw `List` elsewhere in the corpus, and nothing yet +refuses it. + +The ceiling is **structurally impossible**, and its named trigger is application-argument +typechecking in `04_infer`. `v2.std.compilers.target_model` `target_text_carrier_scaffold_note` +records — proven by execution — that neither the v1 seed nor v2 `04_infer` typechecks +function-application argument types, so a raw `String` passed where a nominal carrier is declared +compiles clean. **A nominal `CliArgument` newtype alone therefore makes nothing unwritable today.** +Until that frontier closes, this design's guarantee rests on executing witnesses, and the +construction wall rejecting raw argv authoring — except an explicitly modeled escape population +at genuine foreign/bootstrap boundaries — is a later rung. + +Claiming otherwise would be rung inflation. + +--- + +## 10. Open questions + +1. **Carrier parameterization.** The terminal shape is conceptually + `emit(tree, text_target) -> Medium` beside `emit(tree, cli_target) -> Medium`. + `Medium` is already generic; the text lock is in `TargetModel`, `serialize_target` and `emit`. + **Whether that generic spelling compiles is unproven and needs an executing probe.** + Not-negotiable either way: do not add a fake textual encoding to avoid changing the seam. + Space-separated text reintroduces quoting where none exists; NUL-delimited text is a wire + encoding masquerading as the target artifact. +2. **`sshpass -d 0` and stdin.** The password occupies fd 0. A remote stdin-fed jq would collide. + Latent, not live — all seventeen remote sites use file operands. Must be a typed refusal, not + an accidental limitation. Options: remote file-input only; move password delivery to another + descriptor; or a framed remote receiver. +3. **Portable-word allowlist.** `gunbc.typed_argv_exec` bounds what may cross SSH. jq programs + contain spaces, pipes, brackets, parentheses and quotes — outside that alphabet. The shell leg + must own canonical shell-word serialization with injection controls, or refuse. +4. Which of the 315 computed-head argv lines hide further wrappers. + +--- + +## 11. Corrections receipt + +Claims asserted during this design and refuted by measurement, kept so they are not re-derived: + +- *"The declarative `transport shell` form is fixed-arity and cannot express variadic options."* + **False** — `ssh.Session.ExecArgv` and `ExecPortableWords` splice `List`. +- *"SSH becomes a bound handler over the same tree."* **Incomplete** — RFC 4254 forces a string + at that boundary; structure cannot cross it as structure. +- *"`ProcessInvocation` is the general process carrier."* **False** — it is an emit-harness carrier; + its argument variants are provenance, not CLI roles. +- *"`SensorIntegerValue` has no consumers."* **False** — two live consumers, and its empty-output + branch is a modeled `OpenBmcSensorValueAbsent`, so an `-e` sweep would have collapsed a correct + three-state decode into a refusal. +- *"`ExtractRaw` and `SensorIntegerValue` are both latent traps."* **False** for the second; only + `ExtractRaw` is zero-consumer. +- The plan's census (262 lines / 37 files; 148/51 success/exit_code) is **stale**; measured + 597/129 and 173/69. From 94320fbff03e1e0cac756ab8c516876be570c09b Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 18 Aug 2026 22:27:37 +0000 Subject: [PATCH 02/23] 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) --- docs/plans/cli-invocation-emission-design.md | 232 +++++++++++++++++-- 1 file changed, 212 insertions(+), 20 deletions(-) diff --git a/docs/plans/cli-invocation-emission-design.md b/docs/plans/cli-invocation-emission-design.md index 850835778c8..1f87d3269f1 100644 --- a/docs/plans/cli-invocation-emission-design.md +++ b/docs/plans/cli-invocation-emission-design.md @@ -181,14 +181,18 @@ List argument boundaries structural; no quoting type JqProgram { source: NonEmptyStr } // opaque, upstream-grounded, for now type JqBinding - = JqJsonBinding { name: NonEmptyStr, value: Json } - | JqTextBinding { name: NonEmptyStr, value: String } + = JqJsonBinding { name: JqBindingName, value: Json } + | JqTextBinding { name: JqBindingName, value: String } + +// JqBindingName is jq-owned, not a bare NonEmptyStr. Duplicate-name policy is declared, +// not left to jq's last-wins behaviour: the admission fold refuses a repeated name. type JqInput = JqInputFile { path: FilePath } | JqInputStdin { content: String } -type JqOutputEncoding = JqJsonText | JqRawText +type JqOutputEncoding = JqJsonOutput | JqRawOutput // -r writes STRING results raw; + // non-string results stay JSON-formatted type JqExitPolicy = JqProgramExit | JqLastResultTruthiness @@ -205,22 +209,69 @@ type JqInvocation { operand, `JqInputStdin` produces **no operand** and sets process stdin. That split is load-bearing here — the four local sites are stdin-fed, the seventeen remote ones are file-operand. -### 4b. Observation, decoded once +### 4b. Observation, decoded **policy-indexed** — not once + +An earlier revision of this section put `JqProducedNoResult` as a general arm on every jq +execution. That was wrong, and wrong in the exact direction #8454 had just corrected: it claims a +distinction the selected exit mode cannot supply. + +Verified against `jqlang.org/manual/`: + +``` +default exit 0 when the program runs successfully, REGARDLESS of output — + emitting nothing is still exit 0 +--exit-status / -e exit 0 last output value neither false nor null + exit 1 last output value false or null + exit 4 no valid result was ever produced +halt_error program-chosen code, default 5 +usage/system 2 compile error 3 +``` + +So "no result was produced" is **observable only under `JqLastResultExit`**. Under +`JqProgramExit`, exit zero means the program completed and says nothing about whether the output +stream was empty. Decoding is therefore indexed by the policy the caller selected: ``` -type JqExit - = JqExitedZero - | JqLastResultFalseOrNull - | JqProducedNoResult - | JqExecutionRefused { code: Int } +type JqExitPolicy = JqProgramExit | JqLastResultExit -type JqObservation { exit: JqExit, exit_code: Int, stdout: String, stderr: String } +type JqExecution + = JqProgramCompleted { stdout, stderr, exit_code } // no claim about results produced + | JqLastResultFalseOrNull { stdout, stderr } // JqLastResultExit only + | JqProducedNoResult { stdout, stderr } // JqLastResultExit only + | JqExecutionRefused { exit_code: Int, stderr } +``` + +``` +JqProgramExit + exit 0 -> JqProgramCompleted +JqLastResultExit + exit 1 -> JqLastResultFalseOrNull +JqLastResultExit + exit 4 -> JqProducedNoResult ``` -`JqProducedNoResult` is its own arm because of the `OpenBmcSensorValueAbsent` specimen: absence -is a live, witnessed, modeled value. jq owns exit-code *decoding*; the domain owns whether that -outcome satisfies its contract. "Exactly one nonempty string" is a domain decode, not a jq flag — -and it is strictly stronger than `-e`, which still admits the empty string. +The raw `exit_code` is preserved alongside the decoded arm, so decoding known meanings never +discards the observation. Spawn failure and signal termination belong to the **process layer**, +not to jq exit decoding — jq cannot report an exit code it never reached. + +**Why this matters concretely.** `SensorIntegerValue` runs under `JqProgramExit`. Its +`OpenBmcSensorValueAbsent` fact is derived by the OpenBMC domain decoder from *successful, empty +stdout over that exact program* — **not** from a jq exit code. Putting a general +`JqProducedNoResult` arm on jq would invite exactly the `Absent → Refused` collapse that the +blanket `-e` sweep was withdrawn for. + +**A stdout `String` cannot generically prove "exactly one nonempty raw string".** jq emits a +*stream* of results; under `--raw-output` a raw string may itself contain newlines, which is why +`--raw-output0` exists ("Like `-r` but jq will print NUL instead of newline after each output… +When the output value contains NUL, jq exits with non-zero code"). So `foo\nbar\n` is ambiguous +between one string containing a newline and two results, and once the process boundary has +collapsed stdout into one `String` no generic decoder can separate them. + +This does not block the first vertical — an integer has an unambiguous textual grammar, empty is +distinguishable from one integer, and multiple numeric results produce multi-line text a +`parse_int` refuses. It does mean **this note promises no generic +`decode_exactly_one_nonempty_string`.** For the credential path later, one of three honest +framings must land first: a single JSON envelope parsed as JSON; `--raw-output0` once jq +version/capability is modeled; or a program collecting its result into a one-result container the +domain decoder checks. Until then a decoder may enforce "nonempty observed stdout" and must not +claim "exactly one jq string result". **No `success: Bool`.** The seed derives it as exactly `exit_code == 0`, so the pair carries one fact twice and makes a contradiction writable — a caller can pass `success: true` beside a nonzero @@ -283,10 +334,52 @@ subcommand, option value, mode word or operand. Fusing them makes `OptionValue unrepresentable, and expanding to `WorkspacePathOptionValue`, `WorkspacePathOperand`, … is exactly the combinatorial growth the grammar exists to remove. +**`CliOption { values: List }` is too permissive as a *public* carrier.** Freely +constructible, it admits `--argjson` with zero, one or three values; a flag receiving a value; a +non-repeatable option used twice; options in an illegal order; an option belonging to a different +tool; operands before options where the tool forbids it. The cited row must therefore carry +option identity, canonical spelling, aliases, argument arity, repeatability, placement discipline +and joining discipline — and the emitter must accept only a **normalized, admitted** tree: + +``` +type CliOptionSchema { + option: CliOptionRef + arguments: CliArgumentSchema + repeatability: CliOptionRepeatability + spelling: CliCanonicalSpelling + placement: CliOptionPlacement +} + +type AdmittedCliInvocation { tool: CliToolRef, options: List, operands: List } +``` + +Domain callers receive **no constructor** for `AdmittedCliOptionUse`. The jq semantic-to-syntax +projection selects the row and supplies values; the admission fold checks the schema. This is the +`sole_constructor` + `admit_callers` shape that already sealed `TransportScript` in this corpus, +and it is what raises the rung for the migrated path — see §9. + Roles are then **deliberately erased** at emission, because the operating system receives an ordered vector of strings. That erasure is emission, not anemia. The present defect is only that no preceding tree exists — authors write the vector directly. +### 4e-bis. The process plan is not the CLI grammar + +`CliSyntax` owns how options and operands become argument boundaries. It owns **nothing else**: +standard input, environment, working directory and descriptor routing belong to the *process +plan*. + +``` +type JqProcessPlan { command: CliCommandSurface, stdin: ProcessInput } + +JqInputFile(path) -> one CLI operand, no jq-data stdin +JqInputStdin(content) -> no file operand, stdin = content +``` + +This is why `SensorIntegerValue` is a good first proof: the input content must stay **outside +argv** while the jq program must stay **one argv argument**. Two properties an argv-only model +cannot even state — and precisely the gap `extdeps.llm.cursor_cli` hit when an argv-shaped +carrier could not hold an environment-passed credential. + ### 4f. Carrier: argv is native, text is the derived special case POSIX utility syntax operates over *arguments*. Shell syntax is the preceding language that turns @@ -350,6 +443,16 @@ because that type already exists. The honest longer-term cleanup is renaming it `EmitHostArgumentMaterialization`), which is a separate replacement migration and explicitly not bundled here. +**Generalizing that subsystem is NOT a prerequisite for the first vertical.** Making stdin, cwd +and fd mapping land on `Command`/`SpawnProcessRequest` before any jq migration turns one proof +vertical into a process-runtime project. The stable boundary is `CliCommandSurface + ProcessInput`; +it binds first through one narrow local jq realization whose entire content is the jq executable +identity, a splice of already-emitted arguments, and the process channel wiring — **no option +spelling and no domain filter**. That is an honest realization boundary, not another argv +authority. Its dissolution trigger is explicit: it dissolves when the same emitted surface binds +to `extdeps.posix` `Command`. Emit a `CliToolRef` and let each realization resolve `"jq"` or an +absolute path. + `v2.extdeps.posix` `Command` is the right conceptual layer, with four bounded deficiencies: 1. `program: AbsolutePath` — a semantic invocation names a *tool*; resolution must produce the @@ -372,6 +475,15 @@ bundled here. | realization | local vs SSH vs another handler | | **no caller** | `-e`, `-r`, `--argjson`, `--`, or their positions | +The split is by **what fact the program encodes**, not by the fact that jq executes it. +`ProjectFanConfig` embeds `TEMP_SOC`, the aggregate fan PID entry, desired inputs, minimum and +failsafe duties, hysteresis and exact-one-controller policy — gunbc's chosen topology, so it moves. +`SensorIntegerValue`, `ObjectMapperServiceCount` and `ObjectMapperServiceAt` interpret **upstream +OpenBMC response shapes**; they stay under `extdeps.bmc` even though jq currently realizes them. +The several *remote* fan-query programs carrying a literal `TEMP_SOC` are the ambiguous middle: +they belong beside the projection authority, or should derive that value from it, rather than +keeping the literal in `extdeps`. + Filters leave both `extdeps.tools.jq` (business policy in extdeps is a layer inversion) and `openbmc.PasswordSshTransport` (SSH does not own what the remote program means). They do not all land in one generic "workflow layer": policy-bearing ones go to `gunbc.bmc_fan_projection`, which @@ -406,6 +518,46 @@ Per the §3 replacement-migration rule, stated at exact identity grain. (`ProjectFanConfig`, `ObjectMapperServiceCount`, `ObjectMapperServiceAt`, `SensorIntegerValue`) plus the seventeen `openbmc_password_ssh_transport` remote jq operations. +**Canonical first vertical: `SensorIntegerValue`.** Chosen because it has two live consumers; its +three-way domain contract is already explicit and witnessed; it exercises stdin as a *process +channel* rather than an argument; it proves `JqProgramExit` must emit **no** `--exit-status`; it +proves empty output can be a valid domain observation rather than a transport failure; its integer +output sidesteps the raw-string framing problem above; its program is small enough that the +architecture stays visible; and deleting its old operation is an exact, countable cut. + +Acceptance population for it: + +``` +{"data": 41.6} -> Observed 42 {"data": "41"} -> Absent +{"data": 41} -> Observed 41 {"data": null} -> Absent +{} -> Absent invalid JSON -> Refused +two numeric inputs -> Refused, never first-pick jq nonzero -> Refused +``` + +Emission side, proven separately from semantics: + +``` +JqRawOutput selects the raw-output option identity +that identity selects its canonical spelling +JqProgramExit emits NO exit-status option +the jq program is exactly one argument +stdin content appears NOWHERE in argv +argument order is stable +``` + +**Wave order after the proof.** Slice A `SensorIntegerValue` (above). Slice B +`ObjectMapperServiceCount` + `ObjectMapperServiceAt` together — adds `JqLastResultExit`, +`JqJsonBinding`, the two-argument `--argjson name JSON-text` row, canonical JSON serialization of +`index`. Slice C `ProjectFanConfig` — adds file input, JSON output, the `desired` binding, and +relocation of the policy-bearing program to `gunbc.bmc_fan_projection`. Slice D one remote +file-input scalar query — adds the password-SSH handler, arguments embedded through the shell +grammar, and an explicit stdin-input refusal for the `sshpass -d 0` channel. Each slice deletes +its old operations in the same cut. After D the remainder is repetitive migration, not +architecture. + +**Do not make the first vertical solve SSH.** Local exemplar and transport composition are +separate proofs. + **First vertical (smallest complete):** 1. `JqInvocation` and its semantic axes. @@ -453,15 +605,28 @@ Semantics and serialization are witnessed separately: ## 9. Rung, honestly -At the end of the first vertical the class sits at **mechanically preventable**, not structural: -a caller can still construct a raw `List` elsewhere in the corpus, and nothing yet -refuses it. +The rung is **two different rungs for two different subjects**, and stating one number for both +was too coarse. + +**For the migrated jq path: structurally guaranteed is reachable now.** If +`AdmittedCliOptionUse` is a `sole_constructor` record whose single mint is `admit_callers`-sealed +to the jq semantic-to-syntax projection, then no domain module can form an option use at all — +the same construction wall that already closed `TransportScript`, which needed both the record +seal and the cast judgement in `04_infer` `sole_constructor_construction_diags`. A migrated +caller cannot author `-e`, omit a required option, or mis-arity `--argjson`, because it holds no +constructor for any of them. + +**For the corpus at large: mechanically preventable at best.** A caller can still write a raw +`List` in any of the other 575 argv lines, and nothing refuses it. That is the weaker +claim, and it does not climb until the population is migrated and a construction guard rejects +raw argv authoring outside a declared foreign/bootstrap escape. -The ceiling is **structurally impossible**, and its named trigger is application-argument -typechecking in `04_infer`. `v2.std.compilers.target_model` `target_text_carrier_scaffold_note` +The ceiling for the *nominal-carrier* half remains **structurally impossible**, and its named +trigger is application-argument typechecking in `04_infer`. `v2.std.compilers.target_model` `target_text_carrier_scaffold_note` records — proven by execution — that neither the v1 seed nor v2 `04_infer` typechecks function-application argument types, so a raw `String` passed where a nominal carrier is declared -compiles clean. **A nominal `CliArgument` newtype alone therefore makes nothing unwritable today.** +compiles clean. **A nominal `CliArgument` newtype alone therefore makes nothing unwritable today** — which is +exactly why the wall must be the sealed constructor, not the type name. Until that frontier closes, this design's guarantee rests on executing witnesses, and the construction wall rejecting raw argv authoring — except an explicitly modeled escape population at genuine foreign/bootstrap boundaries — is a later rung. @@ -487,6 +652,22 @@ Claiming otherwise would be rung inflation. contain spaces, pipes, brackets, parentheses and quotes — outside that alphabet. The shell leg must own canonical shell-word serialization with injection controls, or refuse. 4. Which of the 315 computed-head argv lines hide further wrappers. +5. **The remote jq rows may already be broken — live, unverified.** The seventeen + `openbmc_password_ssh_transport` operations place the jq filter after the SSH destination as + though its local argv boundary survived remotely. It does not: the local `ssh` client joins its + command words with spaces into RFC 4254's single `command` string, and OpenSSH's server runs + that through the user's login shell, which re-parses it. Those filters contain spaces, pipes, + brackets, parentheses and double quotes — `[.zones[].pids[] | select(.name == "TEMP_SOC" …)] | + length` would reach the remote shell with `|` as a pipe operator and the quotes consumed. + **This is a transport-correctness risk, not a proven defect** — no executed control has been + run, and something upstream may be quoting. It must be settled by execution before Slice D, and + it is an argument for the design rather than a consequence of it: the current representation + cannot even express the question. +6. The SSH slice needs a discriminating program containing spaces, a pipe, quotes, brackets and a + value containing a single quote, and must reuse the grammar-owned quoting the effect-plan Bash + path already demonstrates rather than retaining `shell_quote`. +7. Reverse ingestion — reading argv back through the same rows — is the terminal second reading + and is **not a prerequisite for the first emitter cut**. --- @@ -507,3 +688,14 @@ Claims asserted during this design and refuted by measurement, kept so they are `ExtractRaw` is zero-consumer. - The plan's census (262 lines / 37 files; 148/51 success/exit_code) is **stale**; measured 597/129 and 173/69. +- *"`JqProducedNoResult` is a general arm on every jq execution."* **False** — verified against + `jqlang.org/manual/`: default jq exits 0 regardless of output, and only `--exit-status` yields + exit 4 for "no valid result was ever produced". Claiming the arm unconditionally would have + reintroduced the `Absent → Refused` collapse #8454 had just withdrawn. +- *"'Exactly one nonempty string' is a decode the domain can perform."* **Over-claimed** — jq emits + a stream and `-r` permits newlines inside a raw string, so a collapsed stdout `String` is + ambiguous. `--raw-output0` exists precisely because of this. +- *"The class sits at mechanically preventable."* **Too coarse** — that is the corpus-wide claim; + the migrated path can reach structurally guaranteed now via a sealed constructor. +- *"Filters move to `gunbc.bmc_fan_projection`."* **Needed splitting** — only policy-bearing + programs move; OpenBMC wire decoders stay in `extdeps.bmc`. From 99c41997de28f3be791bcb7516a1486e2c6911a9 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 18 Aug 2026 22:41:27 +0000 Subject: [PATCH 03/23] 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, 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 vs Medium 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) --- docs/plans/cli-invocation-emission-design.md | 295 ++++++++++++------- 1 file changed, 186 insertions(+), 109 deletions(-) diff --git a/docs/plans/cli-invocation-emission-design.md b/docs/plans/cli-invocation-emission-design.md index 1f87d3269f1..46a6c5b405a 100644 --- a/docs/plans/cli-invocation-emission-design.md +++ b/docs/plans/cli-invocation-emission-design.md @@ -209,74 +209,80 @@ type JqInvocation { operand, `JqInputStdin` produces **no operand** and sets process stdin. That split is load-bearing here — the four local sites are stdin-fed, the seventeen remote ones are file-operand. -### 4b. Observation, decoded **policy-indexed** — not once +### 4b. Observation: two orthogonal axes, sealed -An earlier revision of this section put `JqProducedNoResult` as a general arm on every jq -execution. That was wrong, and wrong in the exact direction #8454 had just corrected: it claims a -distinction the selected exit mode cannot supply. +Two earlier revisions of this section were wrong, in the same direction each time — putting on +one axis a fact that lives on two. + +**Termination and output presence are orthogonal.** The live `SensorIntegerValue` specimen proves +both can hold at once: exit status 0 **and** zero results produced. It runs `-r` without `-e`, its +filter takes the `empty` branch for a non-number, and that run exits zero with empty stdout. So +`JqExitZero | JqProducedNoResult` is not a coproduct — it is a product, and writing it as a sum +makes the live case unrepresentable. Verified against `jqlang.org/manual/`: ``` -default exit 0 when the program runs successfully, REGARDLESS of output — - emitting nothing is still exit 0 ---exit-status / -e exit 0 last output value neither false nor null - exit 1 last output value false or null +default exit 0 when the program runs successfully, REGARDLESS of output +--exit-status / -e exit 0 last output neither false nor null + exit 1 last output false or null exit 4 no valid result was ever produced -halt_error program-chosen code, default 5 -usage/system 2 compile error 3 -``` - -So "no result was produced" is **observable only under `JqLastResultExit`**. Under -`JqProgramExit`, exit zero means the program completed and says nothing about whether the output -stream was empty. Decoding is therefore indexed by the policy the caller selected: - +halt_error program-chosen, default 5 usage 2 compile error 3 ``` -type JqExitPolicy = JqProgramExit | JqLastResultExit -type JqExecution - = JqProgramCompleted { stdout, stderr, exit_code } // no claim about results produced - | JqLastResultFalseOrNull { stdout, stderr } // JqLastResultExit only - | JqProducedNoResult { stdout, stderr } // JqLastResultExit only - | JqExecutionRefused { exit_code: Int, stderr } ``` - -``` -JqProgramExit + exit 0 -> JqProgramCompleted -JqLastResultExit + exit 1 -> JqLastResultFalseOrNull -JqLastResultExit + exit 4 -> JqProducedNoResult +type JqExitDisposition + = JqExitZero + | JqExitFalseOrNullUnderExitStatus // JqLastResultExit only + | JqExitNoResultUnderExitStatus // JqLastResultExit only + | JqExitRefused { code: Int } + +type JqOutputPresence + = JqOutputAbsent + | JqOutputPresent { stdout: String } + +type JqObservation sole_constructor { + process: ProcessObservation // raw evidence, retained + exit: JqExitDisposition // decoded projection, bound to it + output: JqOutputPresence + stderr: String +} ``` -The raw `exit_code` is preserved alongside the decoded arm, so decoding known meanings never -discards the observation. Spawn failure and signal termination belong to the **process layer**, -not to jq exit decoding — jq cannot report an exit code it never reached. - -**Why this matters concretely.** `SensorIntegerValue` runs under `JqProgramExit`. Its -`OpenBmcSensorValueAbsent` fact is derived by the OpenBMC domain decoder from *successful, empty -stdout over that exact program* — **not** from a jq exit code. Putting a general -`JqProducedNoResult` arm on jq would invite exactly the `Absent → Refused` collapse that the -blanket `-e` sweep was withdrawn for. +| case | exit disposition | output presence | +|---|---|---| +| `SensorIntegerValue`, numeric | `JqExitZero` | `JqOutputPresent` | +| `SensorIntegerValue`, non-numeric | `JqExitZero` | **`JqOutputAbsent`** | +| `ObjectMapperServiceAt`, found | `JqExitZero` | `JqOutputPresent` | +| truthiness policy, no result | `JqExitNoResultUnderExitStatus` | `JqOutputAbsent` | +| jq execution error | `JqExitRefused` | independently observed | + +**The decoder is policy-indexed and is the only mint.** +`decode_jq_observation(invocation, process) -> JqObservation` — not a global `exit_code -> JqExit` +lookup, because codes 1 and 4 mean nothing under `JqProgramExit`, and zero results under +`JqProgramExit` still produce code zero. + +**Sealing is required, not decorative.** Rejecting `success: Bool` beside `exit_code` removes one +writable contradiction; leaving `JqObservation` freely constructible recreates it under richer +names — `{ exit: JqExitZero, exit_code: 4 }` would be authorable. `sole_constructor`, minted only +by the policy-aware decoder, closes it. The raw process observation is retained as evidence and +the decoded facts are a projection **bound to it**, never two caller-authored fields side by side. +This is the first concrete place where the answer to the rung question is *yes, a construction +wall is available today*. **A stdout `String` cannot generically prove "exactly one nonempty raw string".** jq emits a -*stream* of results; under `--raw-output` a raw string may itself contain newlines, which is why -`--raw-output0` exists ("Like `-r` but jq will print NUL instead of newline after each output… -When the output value contains NUL, jq exits with non-zero code"). So `foo\nbar\n` is ambiguous -between one string containing a newline and two results, and once the process boundary has -collapsed stdout into one `String` no generic decoder can separate them. - -This does not block the first vertical — an integer has an unambiguous textual grammar, empty is -distinguishable from one integer, and multiple numeric results produce multi-line text a -`parse_int` refuses. It does mean **this note promises no generic -`decode_exactly_one_nonempty_string`.** For the credential path later, one of three honest -framings must land first: a single JSON envelope parsed as JSON; `--raw-output0` once jq -version/capability is modeled; or a program collecting its result into a one-result container the -domain decoder checks. Until then a decoder may enforce "nonempty observed stdout" and must not -claim "exactly one jq string result". +*stream*; under `--raw-output` a raw string may contain newlines, which is why `--raw-output0` +exists ("Like `-r` but jq will print NUL instead of newline after each output"). So `foo\nbar\n` +is ambiguous between one string containing a newline and two results, and a collapsed stdout +`String` cannot separate them. This does not block the first vertical — an integer has an +unambiguous textual grammar — but **this note promises no generic +`decode_exactly_one_nonempty_string`.** Lifting that requires one of: a single JSON envelope +parsed as JSON; `--raw-output0` once jq version/capability is modeled; or a program collecting its +result into a one-result container the domain decoder checks. **No `success: Bool`.** The seed derives it as exactly `exit_code == 0`, so the pair carries one -fact twice and makes a contradiction writable — a caller can pass `success: true` beside a nonzero -code. `extdeps.git.git` `ls_remote_reports_termination_not_success_note` already establishes this -and names itself the first consumer of the correction. 173 operations still carry the Bool. +fact twice. `extdeps.git.git` `ls_remote_reports_termination_not_success_note` establishes this; +173 operations still carry the Bool. ### 4c. Two-level row derivation — the keystone @@ -468,12 +474,16 @@ absolute path. | owner | owns | |---|---| -| `extdeps.tools.jq` | what raw output means, what exit-status mode means, that `--argjson` takes a name and a JSON value, which options repeat, how jq spells them | -| shared `CliSyntax` | option/value structure, repeated options, operand ordering, separators, canonical short/long spelling, emission to argument tokens | +| `extdeps.tools.jq` | what raw output means, what exit-status mode means, that `--argjson` takes a name and a JSON value, which options repeat — and **which spellings exist and which is canonical** (`long = exit-status`, `short alias = e`, canonical preference, value cardinality) | +| shared `CliSyntax` | **how a chosen form is constructed** — a long name renders `--` + name, a short renders `-` + character, clustering where the tool row permits, joined vs separate values, option/operand/terminator order | | `gunbc.bmc_fan_projection` | the `TEMP_SOC` policy, the fan curve, controller cardinality, the desired topology | | `extdeps.bmc.*` | programs projecting a documented OpenBMC response or config field | | realization | local vs SSH vs another handler | -| **no caller** | `-e`, `-r`, `--argjson`, `--`, or their positions | +| **no caller** | `-e`, `-r`, `--argjson`, `--`, their positions, or the choice between `-e` and `--exit-status` | + +The tool row owns *which forms exist and which is canonical*; the grammar owns *how a chosen form +is constructed*. An earlier revision gave both authorities "canonical spelling" — two authorities +for one decision, the §3 violation this note is about, committed inside it. The split is by **what fact the program encodes**, not by the fact that jq executes it. `ProjectFanConfig` embeds `TEMP_SOC`, the aggregate fan PID entry, desired inputs, minimum and @@ -498,7 +508,11 @@ already owns the board, firmware, curve, config path, controller entry and tach 3. Per-tool lowering contains no bespoke option-selection fold; semantic variants select grammar rows exhaustively. 4. Transport consumes an inner invocation. SSH may **not** be modeled as `append(ssh_prefix, inner.argv)`. -5. The CLI inverse consumes `List`, not shell text. Shell text is parsed by the shell +5. The CLI inverse consumes `List`, not shell text — and it is **partial and + ambiguity-aware**, not bijective: clustered short options, optional option-arguments, operands + beginning with `-` and tool deviations admit multiple parses, so it answers + `CliParseUnique | CliParseAmbiguous | CliParseRefused`. It is **not** a Wave 1 acceptance + criterion; current argv remains an offline behavioral oracle. Shell text is parsed by the shell grammar first; only a static literal simple command projects back to a CLI surface. 6. Every vertical deletes its prior argv authoring site **in the same cut**. "New tree plus old helper for compatibility" creates two authorities. @@ -518,14 +532,32 @@ Per the §3 replacement-migration rule, stated at exact identity grain. (`ProjectFanConfig`, `ObjectMapperServiceCount`, `ObjectMapperServiceAt`, `SensorIntegerValue`) plus the seventeen `openbmc_password_ssh_transport` remote jq operations. -**Canonical first vertical: `SensorIntegerValue`.** Chosen because it has two live consumers; its -three-way domain contract is already explicit and witnessed; it exercises stdin as a *process -channel* rather than an argument; it proves `JqProgramExit` must emit **no** `--exit-status`; it -proves empty output can be a valid domain observation rather than a transport failure; its integer -output sidesteps the raw-string framing problem above; its program is small enough that the -architecture stays visible; and deleting its old operation is an exact, countable cut. - -Acceptance population for it: +**Recut: the first vertical is LOCAL only.** An earlier revision put local execution and SSH in +one "smallest complete" vertical. That is not smallest — SSH adds a second language target, RFC +4254 string loss, portable-word refusal, quoting, and the latent `sshpass -d 0` collision. The +unit is **one local jq vertical, demonstrated by one feature-rich migration and one discriminating +counterexample.** + +**Wave 0 — carrier probe.** Stacked with its first production consumer, never mergeable alone. +A probe-only non-text serializer beside the text one; sealed `CliSurface`; existing text emission +byte-identical; argument boundaries observable *by execution*; direct/cast/unadmitted-mint REDs; +explicit refusal when no CLI serializer is wired. See §10 — this probe must execute, because it +will not refuse at compile time. + +**Wave 1A — `ObjectMapperServiceAt`.** The strongest first exemplar, because its existing argv +exercises nearly every load-bearing axis at once: `-e` truthiness exit, `-r` raw output, a typed +JSON binding through `--argjson` (an option with **two** values), stdin input, a jq program +operand, exact nonempty-string domain decoding, and a live recursive consumer. After migration the +OpenBMC caller stops reading `success`/`stdout`/`stderr` itself and matches +`OpenBmcServiceObserved | OpenBmcServiceProjectionRefused`. No layer above jq's cited rows can +name `-e`, `-r`, `-er` or `--argjson`. + +**Wave 1B — `SensorIntegerValue`, the required falsifier.** Immediately stacked, *before* the +abstraction is advertised as ready for repetition. It is the counterexample to a design overfit to +`-e`, and it proves four things Wave 1A cannot: that `JqProgramExit` selects **no** +`JqCliOptionExitStatus`; that `JqOutputAbsent` is not automatically a refusal; that termination +and output presence really are orthogonal in the observation model; and that one lowering supports +two opposite domain policies unchanged. Its acceptance population: ``` {"data": 41.6} -> Observed 42 {"data": "41"} -> Absent @@ -534,26 +566,29 @@ Acceptance population for it: two numeric inputs -> Refused, never first-pick jq nonzero -> Refused ``` -Emission side, proven separately from semantics: +**Wave 2 — first SSH migration.** Only after the local vertical is green: `CliSurface` → shell +simple-command tree → shell grammar emission → RFC 4254 command string, reusing the grammar-owned +quoting the effect-plan Bash path already demonstrates rather than retaining `shell_quote`. Owns +the portable-word limitation, file-input-only admission, and a typed refusal for stdin-fed remote +jq while `sshpass -d 0` holds fd 0. Then the remaining remote population is mechanical. + +Emission-side witnesses, proven separately from semantics at every wave: ``` -JqRawOutput selects the raw-output option identity -that identity selects its canonical spelling +the semantic property selects the option identity (row level 1 perturbation) +that identity selects its canonical spelling (row level 2 perturbation) JqProgramExit emits NO exit-status option the jq program is exactly one argument stdin content appears NOWHERE in argv argument order is stable +direct / cast / unadmitted-mint construction refuses +the old transport argv site is absent in the same cut +no success: Bool survives on the new path ``` -**Wave order after the proof.** Slice A `SensorIntegerValue` (above). Slice B -`ObjectMapperServiceCount` + `ObjectMapperServiceAt` together — adds `JqLastResultExit`, -`JqJsonBinding`, the two-argument `--argjson name JSON-text` row, canonical JSON serialization of -`index`. Slice C `ProjectFanConfig` — adds file input, JSON output, the `desired` binding, and -relocation of the policy-bearing program to `gunbc.bmc_fan_projection`. Slice D one remote -file-input scalar query — adds the password-SSH handler, arguments embedded through the shell -grammar, and an explicit stdin-input refusal for the `sshpass -d 0` channel. Each slice deletes -its old operations in the same cut. After D the remainder is repetitive migration, not -architecture. +Both row levels need independent perturbation controls: a single spelling perturbation proves +concrete spelling is authoritative but says nothing about whether a required semantic property can +be omitted. **Do not make the first vertical solve SSH.** Local exemplar and transport composition are separate proofs. @@ -603,47 +638,73 @@ Semantics and serialization are witnessed separately: --- -## 9. Rung, honestly +## 9. Rung, by exact subject -The rung is **two different rungs for two different subjects**, and stating one number for both -was too coarse. +An earlier revision said "mechanically preventable, because a caller can still construct a raw +`List` and nothing yet refuses it." That sentence is internally inconsistent: **if nothing +refuses it, it is not mechanically prevented.** It is measured or mitigated, not prevented. It +also *understated* what the migrated path can reach. One number for several populations was the +error. -**For the migrated jq path: structurally guaranteed is reachable now.** If -`AdmittedCliOptionUse` is a `sole_constructor` record whose single mint is `admit_callers`-sealed -to the jq semantic-to-syntax projection, then no domain module can form an option use at all — -the same construction wall that already closed `TransportScript`, which needed both the record -seal and the cast judgement in `04_infer` `sole_constructor_construction_diags`. A migrated -caller cannot author `-e`, omit a required option, or mis-arity `--argjson`, because it holds no -constructor for any of them. +| exact subject | honest rung after the first vertical | mechanism | +|---|---|---| +| forging a `CliInvocationTree` / `CliSurface` / `JqObservation` | **structurally impossible now** | `sole_constructor`; only the row emitter, serializer and decoder may mint | +| omitting `--exit-status` from an accepted truthiness invocation | **structurally impossible within the new path** | exhaustive semantic→option selection; zero-or-many rows refuse; no mint on miss | +| hand-authoring flags inside a migrated route | **structurally impossible after cutover** | handler takes a semantic invocation, emits internally, old argv site deleted | +| reintroducing the exact old operation transport | mechanically preventable | structural deletion witness | +| writing another raw jq argv elsewhere | **still writable** | unrelated raw shell/process routes remain | +| arbitrary raw argv corpus-wide | outside this vertical | later process/transport confinement | -**For the corpus at large: mechanically preventable at best.** A caller can still write a raw -`List` in any of the other 575 argv lines, and nothing refuses it. That is the weaker -claim, and it does not climb until the population is migrated and a construction guard rejects -raw argv authoring outside a declared foreign/bootstrap escape. +So: **the first migrated jq path can be structural now; the repository-wide raw-jq class stays +open; the repository-wide raw-argv class is a later migration.** -The ceiling for the *nominal-carrier* half remains **structurally impossible**, and its named -trigger is application-argument typechecking in `04_infer`. `v2.std.compilers.target_model` `target_text_carrier_scaffold_note` -records — proven by execution — that neither the v1 seed nor v2 `04_infer` typechecks -function-application argument types, so a raw `String` passed where a nominal carrier is declared -compiles clean. **A nominal `CliArgument` newtype alone therefore makes nothing unwritable today** — which is -exactly why the wall must be the sealed constructor, not the type name. -Until that frontier closes, this design's guarantee rests on executing witnesses, and the -construction wall rejecting raw argv authoring — except an explicitly modeled escape population -at genuine foreign/bootstrap boundaries — is a later rung. +**Application-argument typechecking is not the terminal trigger.** The `04_infer` gap is real — +`explicit_return_conformance_note` records that conformance is judged only by the +ground-kernel-scalar and ground-element-collection discipline — but it is neither *necessary* for +sealing this path nor *sufficient* to eliminate alternate raw routes. It matters when a sealed +carrier crosses an open function boundary and correctness rests on ordinary argument conformance, +and the first vertical avoids that dependency: no arbitrary caller receives a public +`execute(surface: CliSurface)` to smuggle into. The domain caller passes a `JqInvocation`; the +handler emits and consumes the sealed surface internally. -Claiming otherwise would be rung inflation. +The real terminal trigger for the broad jq class is a **dominator condition**: ---- +> every production path capable of executing jq is dominated by the semantic jq handler, and raw +> process/shell routes cannot name jq except through an explicitly retained escape population. + +General argument typechecking strengthens the boundary; it does not prove that property. ## 10. Open questions -1. **Carrier parameterization.** The terminal shape is conceptually - `emit(tree, text_target) -> Medium` beside `emit(tree, cli_target) -> Medium`. - `Medium` is already generic; the text lock is in `TargetModel`, `serialize_target` and `emit`. - **Whether that generic spelling compiles is unproven and needs an executing probe.** - Not-negotiable either way: do not add a fake textual encoding to avoid changing the seam. - Space-separated text reintroduces quoting where none exists; NUL-delimited text is a wire - encoding masquerading as the target artifact. +1. **Carrier parameterization — and the probe will NOT refuse.** The exact current answer is not + "unknown diagnostic." It is: **there is no carrier-mismatch refusal on this path, so a + compile-only probe false-greens.** `emit`, `serialize_target` and + `serialize_source_for_emitted` are concretely fixed to `Medium`, and underneath them + `target_serialize_source_from_model_bounded` returns `TargetText` rendered through + `target_source_medium`. Passing a `cli_target` selects no other carrier — it still takes the + text serializer. 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 mismatch such as `Outcome>` vs + `Outcome>` sits outside the judged population and yields no diagnostic. + **Do not treat a green compile as a positive result.** + + The smallest discriminating probe is therefore a **sibling concrete seam**, executed rather + than compiled — `emit_cli_probe` binding `translate`'s target tree to a non-text serializer — + asking one question: can `translate`'s output be consumed by a non-text serializer while the + existing text serializer stays byte-identical? It does not ask the current `emit` to produce + something its signature cannot express, and it does **not** start by genericizing `TargetModel`. + + Its controls: existing `emit` returns the exact prior bytes; the probe returns a sealed + `CliSurface` whose argument boundaries are inspectable **by execution**; swapping the CLI + serializer for the text one must *fail the test*, not compile-green past it; direct, cast and + unadmitted-mint construction of `CliSurface` all refuse; and a missing serializer raises a new + typed `TargetSurfaceSerializerUnwired` rather than silently falling back to source text. + + Only after that receipt does the seam choice get made. Prior: `TargetSurfaceSerializer` is + the smaller terminal seam, with the existing `emit` kept as a compatibility wrapper selecting + the text serializer — parameterizing every `TargetModel` consumer before a non-text target has + proven it necessary is the larger and less reversible move. + 2. **`sshpass -d 0` and stdin.** The password occupies fd 0. A remote stdin-fed jq would collide. Latent, not live — all seventeen remote sites use file operands. Must be a typed refusal, not an accidental limitation. Options: remote file-input only; move password delivery to another @@ -699,3 +760,19 @@ Claims asserted during this design and refuted by measurement, kept so they are the migrated path can reach structurally guaranteed now via a sealed constructor. - *"Filters move to `gunbc.bmc_fan_projection`."* **Needed splitting** — only policy-bearing programs move; OpenBMC wire decoders stay in `extdeps.bmc`. +- *"`JqProducedNoResult` is an arm beside `JqExitZero`."* **False** — the live `SensorIntegerValue` + case holds both at once (exit 0, zero results), so termination and output presence are a + product, not a sum. Written as a sum, the live case is unrepresentable. +- *"Removing `success: Bool` closes the contradiction."* **Insufficient** — an unsealed + `JqObservation` lets `{ exit: JqExitZero, exit_code: 4 }` be authored, the same contradiction + under richer names. The carrier must be `sole_constructor`, minted only by the decoder. +- *"The class sits at mechanically preventable because nothing refuses it."* **Internally + inconsistent** — if nothing refuses it, it is not prevented. Replaced by the subject-grained + matrix. +- *"jq owns how it spells options AND `CliSyntax` owns canonical spelling."* **Two authorities for + one decision**, committed inside a note about exactly that. +- *"The carrier probe will hit a named refusal."* **False** — `emit`/`serialize_target` are fixed + to `Medium` and structured return mismatches fall outside the judged conformance + population, so a compile-only probe **false-greens**. +- *"The smallest complete vertical includes SSH."* **False** — SSH adds a second language target + and three independent failure modes; the unit is local-only. From 9b40c2127052b58b6d4be523b679582543716445 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 18 Aug 2026 22:53:52 +0000 Subject: [PATCH 04/23] 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) --- docs/plans/cli-invocation-emission-design.md | 66 ++++++++++++++++---- 1 file changed, 55 insertions(+), 11 deletions(-) diff --git a/docs/plans/cli-invocation-emission-design.md b/docs/plans/cli-invocation-emission-design.md index 46a6c5b405a..72b73eee6f7 100644 --- a/docs/plans/cli-invocation-emission-design.md +++ b/docs/plans/cli-invocation-emission-design.md @@ -713,17 +713,61 @@ General argument typechecking strengthens the boundary; it does not prove that p contain spaces, pipes, brackets, parentheses and quotes — outside that alphabet. The shell leg must own canonical shell-word serialization with injection controls, or refuse. 4. Which of the 315 computed-head argv lines hide further wrappers. -5. **The remote jq rows may already be broken — live, unverified.** The seventeen - `openbmc_password_ssh_transport` operations place the jq filter after the SSH destination as - though its local argv boundary survived remotely. It does not: the local `ssh` client joins its - command words with spaces into RFC 4254's single `command` string, and OpenSSH's server runs - that through the user's login shell, which re-parses it. Those filters contain spaces, pipes, - brackets, parentheses and double quotes — `[.zones[].pids[] | select(.name == "TEMP_SOC" …)] | - length` would reach the remote shell with `|` as a pipe operator and the quotes consumed. - **This is a transport-correctness risk, not a proven defect** — no executed control has been - run, and something upstream may be quoting. It must be settled by execution before Slice D, and - it is an argument for the design rather than a consequence of it: the current representation - cannot even express the question. +5. **The remote jq rows do not preserve the jq program as one argument. Source-proven.** + Traced end to end, with the local half verified in this tree: + + - `v1_interpreter.rs` `push_shell_argv_tokens` pushes each evaluated `String` **verbatim** — no + splitting, no quoting — and both exec branches call + `Command::new(&argv[0]).args(&argv[1..])`. So despite its name, `transport shell` at this + boundary is **direct process execution**: there is no local shell, no `shell_quote`, no + command-string renderer. + - `sshpass` parses its own options, copies the remaining argument pointers, and `execvp`s them + unchanged. + - OpenSSH's client consumes the `--` after the destination as its **own option terminator** + (not a remote quoting construct) and builds the remote command by appending each remaining + argv member separated by one literal space, with no escaping. + - OpenBMC's default SSH server is **Dropbear**, not OpenSSH — its `run_shell_command` + invokes the user's login shell with `-c`. + + So `["jq", "-er", "[.zones[].pids[] | select(...)] | length", path]` arrives remotely as + `jq -er [.zones[].pids[] | select(...)] | length /path`, and the remote shell reads the + unquoted `|` as pipeline operators. The argument boundary is gone. The law the code needs is + `shell_parse(join(map(shell_quote, argv), " ")) == argv`; what it currently assumes is + `shell_parse(join(argv, " ")) == argv`, which holds only inside a portable-word alphabet these + filters are outside — the same alphabet `gunbc.typed_argv_exec` exists to bound. Dynamic values + such as `config_path` are unquoted too; the current path happens to be shell-safe, but + `NonEmptyStr` does not establish that. + + **Split the judgments rather than calling the whole thing broken:** + + ``` + RemoteJqArgumentBoundaryPreservation Violates — source-proven + DeployedSshClientIsStandardOpenSsh Unverified + DeployedBmcServerUsesDropbearShellExec StronglySupported, not observed on this firmware + AffectedOperationReachability Unverified + ObservedProductionManifestation Unverified + ``` + + The saving conditions are enumerable and none is visible in the repository: a custom binary + named `ssh` that shell-quotes (most plausible, since `sshpass` resolves through `PATH`); filters + already carrying canonical outer quoting; a forced-command or structured receiver decoding an + encoded argv; or a row whose program happens to be entirely portable words. + + **The executed control** uses the exact current prefix and direct argv execution — not a local + shell — with `jq -n`, so it needs no stdin or file and cannot mutate BMC state: + + ``` + portable positive ["jq","-n","-r","7"] -> exit 0, stdout "7" + current form ["jq","-n","-r","[1,2] | length"] -> intended "2" + serialized form ["jq","-n","-r","'[1,2] | length'"] -> expected "2" + ``` + + Discriminating result: portable and serialized controls succeed while the current form does not + produce the same exit/stdout observation. Capture local client version, remote SSH banner and + remote login shell. **If the current form unexpectedly yields `2`, that is positive evidence for + an unmodeled saving layer**, and the next probe captures the actual command string seen + remotely. + 6. The SSH slice needs a discriminating program containing spaces, a pipe, quotes, brackets and a value containing a single quote, and must reuse the grammar-owned quoting the effect-plan Bash path already demonstrates rather than retaining `shell_quote`. From 1de10ed8c8e5de809cf746081337cfc175087dc0 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 18 Aug 2026 23:31:37 +0000 Subject: [PATCH 05/23] 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, 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) --- .../claim/cli_surface_boundary_probe_test.dag | 137 ++++++++++++++++++ src/v2/std/compilers/cli_surface.dag | 137 ++++++++++++++++++ 2 files changed, 274 insertions(+) create mode 100644 dag/test/claim/cli_surface_boundary_probe_test.dag create mode 100644 src/v2/std/compilers/cli_surface.dag diff --git a/dag/test/claim/cli_surface_boundary_probe_test.dag b/dag/test/claim/cli_surface_boundary_probe_test.dag new file mode 100644 index 00000000000..a584f06449e --- /dev/null +++ b/dag/test/claim/cli_surface_boundary_probe_test.dag @@ -0,0 +1,137 @@ +module test.claim.cli_surface_boundary_probe + +import std.algebra { Empty } +import std.process { ExitFailure, ExitSuccess, ProcessExit } +import std.types { Bool, Int, String } +import v2.std.algebra { fold_list, length } +import v2.std.collection { empty_map } +import v2.std.compilers.cli_surface { + CliSurface, + bound_tokens_cli_arguments, + cli_argument_text, + cli_surface_arguments +} +import v2.std.compilers.lexing { + LexRuleSet, + LiteralPattern, + ModeledLexRules, + TokenRule +} +import v2.std.compilers.target_model { + ConcreteSyntaxToken, + FixedToken, + bound_tokens_source_text, + render_target_text +} +import v2.std.diagnostic { Accepted, Rejected } + +// WAVE 0 PROBE (docs/plans/cli-invocation-emission-design.md). +// +// ONE question, executed rather than compiled: can the token sequence translate already produced +// be consumed by a non-text serializer, and does the argument boundary survive there while it is +// destroyed in the text carrier? +// +// The two token spellings are chosen to be the smallest thing that can tell the carriers apart. +// The second contains a SPACE and a PIPE, which is exactly the shape that made the seventeen +// remote jq rows lose their argument boundary at the ssh seam. Concatenated, the two tokens are +// indistinguishable from any other split of the same characters; as arguments, they are two. +// +// WHY THIS CANNOT PASS BY COMPILING. A compile-only probe would false-green: emit and +// serialize_target are fixed to Medium, 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 yields no diagnostic. +// Every assertion below therefore reads a VALUE produced by running the fold. + +data probe_option_class: String = "probe_option" + +data probe_program_class: String = "probe_program" + +// The discriminating spelling: a space and a pipe, unquoted. +data probe_program_spelling: String = "[1,2] | length" + +data probe_option_spelling: String = "--argjson" + +fn probe_lex_rules() -> ModeledLexRules { + ModeledLexRules { + root: LexRuleSet { + rules: [ + TokenRule { + token_class: ^probe_option, + pattern: LiteralPattern { text: probe_option_spelling } + }, + TokenRule { + token_class: ^probe_program, + pattern: LiteralPattern { text: probe_program_spelling } + }, + ] + } + } +} + +fn probe_tokens() -> List { + [ + FixedToken { token_class: ^probe_option }, + FixedToken { token_class: ^probe_program }, + ] +} + +// The CLI carrier preserves exactly two argument boundaries, and the second is the whole +// space-and-pipe-bearing program as ONE argument. +test fn cli_serializer_preserves_argument_boundaries() -> Bool { + match bound_tokens_cli_arguments( + tokens: probe_tokens(), + lex: probe_lex_rules(), + binding_spellings: empty_map() + ) { + Accepted { value: surface, diagnostics: _ } => + match cli_surface_arguments(surface: surface) { + Empty => false + Cons { head: first, tail: rest } => + match rest { + Empty => false + Cons { head: second, tail: after } => + match after { + Empty => + (cli_argument_text(argument: first) == probe_option_spelling) + && (cli_argument_text(argument: second) == probe_program_spelling) + Cons { head: _, tail: _ } => false + } + } + } + Rejected { diagnostics: _ } => false + } +} + +// The text carrier over the SAME tokens produces one blob in which the boundary is gone. This is +// the negative half: it is not a complaint about the text serializer, which is correct for source +// text. It is the proof that the two carriers are genuinely different answers, so selecting the +// wrong one cannot pass this probe. +test fn text_serializer_loses_the_argument_boundary() -> Bool { + match bound_tokens_source_text( + tokens: probe_tokens(), + lex: probe_lex_rules(), + binding_spellings: empty_map() + ) { + Accepted { value: text, diagnostics: _ } => + render_target_text(t: text) == "--argjson[1,2] | length" + Rejected { diagnostics: _ } => false + } +} + +fn probe_verdict() -> ProcessExit { + if cli_serializer_preserves_argument_boundaries() { + if text_serializer_loses_the_argument_boundary() { + ExitSuccess + } else { + ExitFailure { + code: 1, + reason: "text carrier did not render the expected concatenation; the probe is not comparing what it claims" + } + } + } else { + ExitFailure { + code: 1, + reason: "CLI carrier did not preserve exactly two argument boundaries" + } + } +} diff --git a/src/v2/std/compilers/cli_surface.dag b/src/v2/std/compilers/cli_surface.dag new file mode 100644 index 00000000000..29ae0c7ea91 --- /dev/null +++ b/src/v2/std/compilers/cli_surface.dag @@ -0,0 +1,137 @@ +module v2.std.compilers.cli_surface + +import std.algebra { Empty } +import std.types { String, Int, Bool } +import v2.std.algebra { fold_list, list_snoc_item, length } +import v2.std.collection { List, Map } +import v2.std.compilers.target_model { + BoundToken, + ConcreteSyntaxToken, + FixedToken, + LexRules, + bound_spelling_from_map, + lex_rules_literal_for_class +} +import v2.std.diagnostic { + Accepted, + Diagnostic, + None, + Outcome, + ExternalContractUnknown, + Rejected, + Unavailable, + bind_outcome, + node_locus, + outcome_accepted, + outcome_rejected +} +import v2.std.node { + Atom, + Node, + Symbol, + SyntheticOccurrence, + TypeNode +} + + +// WHY THIS EXISTS, and why it is a sibling rather than a transform of the text carrier. +// +// v2.std.compilers.target_model.bound_tokens_source_text folds a grammar-selected token sequence +// into TargetText, resolving each token to its spelling and joining with target_text_seq, which is +// concatenation. Concatenation is the step that DESTROYS argument boundaries: once the tokens are +// one String, "a b" and ["a", "b"] are the same value, and every consumer downstream must +// re-derive a boundary that the grammar already knew. That re-derivation is what shell_quote is, +// at 36 sites. +// +// This module folds the SAME tokens with the SAME spelling resolution and a DIFFERENT join: one +// argument per token. Nothing about the grammar walk changes; only whether the boundary survives. +// That is the whole claim the CLI-invocation-emission design rests on, reduced to the smallest +// thing that can be executed -- see docs/plans/cli-invocation-emission-design.md, Wave 0. +// +// NOT A SECOND EMITTER. It consumes what translate already produced. A target model that wants +// argument boundaries selects this serializer; one that wants source text selects the existing +// one. Both read one grammar. + +// Sealed, and deliberately WITHOUT an exported mint. TransportScript needs transport_script_seal +// because production modules must build one; nothing outside this module has any business +// constructing a CLI argument, because an argument is a RESULT of the grammar fold, never an +// authored value. So the wall here is stronger than TransportScript's: there is no admitted +// caller list to add a name to, because there is no mint to admit anyone to. +type CliArgument sole_constructor { text: String } + +type CliSurface sole_constructor { arguments: List } + +fn cli_surface_arguments(surface: CliSurface) -> List { + surface.arguments +} + +fn cli_argument_text(argument: CliArgument) -> String { + argument.text +} + +fn cli_surface_argument_count(surface: CliSurface) -> Int { + length(xs: surface.arguments) +} + +// The refusal that keeps a missing CLI serializer from degrading into source text. A target whose +// surface serializer is unwired must REFUSE (DESIGN section 5): answering with the text serializer +// would be the absorbing fallback -- a plausible artifact standing where an unanswerable question +// was, and the boundary loss would be invisible precisely because text can hold anything. +fn target_surface_serializer_unwired_diagnostic(target_identity: Symbol) -> Diagnostic { + Diagnostic { + reason: ^target_surface_serializer_unwired, + at: node_locus(node: Node { + kind: TypeNode { connective: Atom { identity: target_identity } }, + children: [], + occurrence_id: SyntheticOccurrence + }), + correction: Unavailable { reason: ExternalContractUnknown } + } +} + +// The sibling fold. Structurally identical to bound_tokens_source_text except that the +// accumulator is a list of arguments and each resolved spelling is snoc'd as its own argument +// rather than concatenated onto a running string. +fn bound_tokens_cli_arguments( + tokens: List, + lex: LexRules, + binding_spellings: Map +) -> Outcome { + bind_outcome( + o: fold_list( + xs: tokens, + empty: Accepted { value: Empty, diagnostics: None }, + cons: fn(acc, token) { + match acc { + Rejected { diagnostics: r } => Rejected { diagnostics: r } + Accepted { value: partial, diagnostics: ad } => + match token { + FixedToken { token_class: tc } => + bind_outcome( + o: lex_rules_literal_for_class(rules: lex, token_class: tc), + f: fn(spelling) { + Accepted { + value: list_snoc_item(xs: partial, item: CliArgument { text: spelling }), + diagnostics: ad + } + } + ) + BoundToken { token_class: _, binding: b } => + bind_outcome( + o: bound_spelling_from_map(binding_spellings: binding_spellings, binding: b), + f: fn(spelling) { + Accepted { + value: list_snoc_item(xs: partial, item: CliArgument { text: spelling }), + diagnostics: ad + } + } + ) + } + } + } + ), + f: fn(arguments) { + outcome_accepted(CliSurface { arguments: arguments }) + } + ) +} From 61e63ec08c6edcf5a282a09507da323392ad0958 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 19 Aug 2026 00:04:29 +0000 Subject: [PATCH 06/23] 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) --- src/v2/std/compilers/cli_surface.dag | 69 ++++++++++++---------------- 1 file changed, 29 insertions(+), 40 deletions(-) diff --git a/src/v2/std/compilers/cli_surface.dag b/src/v2/std/compilers/cli_surface.dag index 29ae0c7ea91..762ad2655c4 100644 --- a/src/v2/std/compilers/cli_surface.dag +++ b/src/v2/std/compilers/cli_surface.dag @@ -1,8 +1,8 @@ module v2.std.compilers.cli_surface import std.algebra { Empty } -import std.types { String, Int, Bool } -import v2.std.algebra { fold_list, list_snoc_item, length } +import std.types { String } +import v2.std.algebra { fold_list, list_snoc_item } import v2.std.collection { List, Map } import v2.std.compilers.target_model { BoundToken, @@ -14,24 +14,13 @@ import v2.std.compilers.target_model { } import v2.std.diagnostic { Accepted, - Diagnostic, None, Outcome, - ExternalContractUnknown, Rejected, - Unavailable, bind_outcome, - node_locus, - outcome_accepted, - outcome_rejected -} -import v2.std.node { - Atom, - Node, - Symbol, - SyntheticOccurrence, - TypeNode + outcome_accepted } +import v2.std.node { Symbol } // WHY THIS EXISTS, and why it is a sibling rather than a transform of the text carrier. @@ -52,11 +41,31 @@ import v2.std.node { // argument boundaries selects this serializer; one that wants source text selects the existing // one. Both read one grammar. -// Sealed, and deliberately WITHOUT an exported mint. TransportScript needs transport_script_seal -// because production modules must build one; nothing outside this module has any business -// constructing a CLI argument, because an argument is a RESULT of the grammar fold, never an -// authored value. So the wall here is stronger than TransportScript's: there is no admitted -// caller list to add a name to, because there is no mint to admit anyone to. +// SEALED AT THE RECORD, NOT AT THE MINT -- and the difference is a live hole, stated here +// because an earlier revision of this comment claimed the opposite and was wrong. +// +// WHAT HOLDS: sole_constructor means no other module can write CliSurface { arguments: ... } or +// cast into one. The record literal and the cast are both closed (04_infer +// sole_constructor_construction_diags judges the two forms through one authority). +// +// WHAT DOES NOT HOLD: bound_tokens_cli_arguments below is public and takes tokens, lex rules AND +// binding spellings FROM ITS CALLER, so any module can synthesize whatever token sequence and lex +// table it likes and receive a sealed CliSurface carrying arbitrary content. 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, reproduced here. +// +// SO THE EARLIER CLAIM WAS BACKWARDS. This is WEAKER than extdeps.shell.exec TransportScript, not +// stronger: transport_script_seal is admit_callers-restricted to two named production decls, while +// this fold admits everyone. The claim was made, reviewed, and corroborated once before anyone +// checked it -- which is why it is written down here rather than quietly amended. +// +// WHY IT IS NOT CLOSED IN THIS COMMIT: the fix is to stop taking caller-supplied grammar at all -- +// the fold should be reachable only already bound to a target model, so the lex table is the +// target's rather than the caller's -- and that shape is decided by whether the jq path consumes +// translate's target model or bypasses it entirely. Sealing to 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, which is also the wave that answers the target-model question. + type CliArgument sole_constructor { text: String } type CliSurface sole_constructor { arguments: List } @@ -69,26 +78,6 @@ fn cli_argument_text(argument: CliArgument) -> String { argument.text } -fn cli_surface_argument_count(surface: CliSurface) -> Int { - length(xs: surface.arguments) -} - -// The refusal that keeps a missing CLI serializer from degrading into source text. A target whose -// surface serializer is unwired must REFUSE (DESIGN section 5): answering with the text serializer -// would be the absorbing fallback -- a plausible artifact standing where an unanswerable question -// was, and the boundary loss would be invisible precisely because text can hold anything. -fn target_surface_serializer_unwired_diagnostic(target_identity: Symbol) -> Diagnostic { - Diagnostic { - reason: ^target_surface_serializer_unwired, - at: node_locus(node: Node { - kind: TypeNode { connective: Atom { identity: target_identity } }, - children: [], - occurrence_id: SyntheticOccurrence - }), - correction: Unavailable { reason: ExternalContractUnknown } - } -} - // The sibling fold. Structurally identical to bound_tokens_source_text except that the // accumulator is a list of arguments and each resolved spelling is snoc'd as its own argument // rather than concatenated onto a running string. From 8e07969ed9b880f0e2af3d32404ebb64bf9ab956 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 19 Aug 2026 00:22:35 +0000 Subject: [PATCH 07/23] 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) --- .../claim/cli_surface_boundary_probe_test.dag | 175 +++++++++--------- src/v2/std/compilers/cli_surface.dag | 90 +++++---- 2 files changed, 145 insertions(+), 120 deletions(-) diff --git a/dag/test/claim/cli_surface_boundary_probe_test.dag b/dag/test/claim/cli_surface_boundary_probe_test.dag index a584f06449e..7f4247df8f0 100644 --- a/dag/test/claim/cli_surface_boundary_probe_test.dag +++ b/dag/test/claim/cli_surface_boundary_probe_test.dag @@ -1,15 +1,14 @@ module test.claim.cli_surface_boundary_probe -import std.algebra { Empty } -import std.process { ExitFailure, ExitSuccess, ProcessExit } -import std.types { Bool, Int, String } -import v2.std.algebra { fold_list, length } -import v2.std.collection { empty_map } +import std.algebra { Cons, Empty } +import std.types { Bool, String } +import v2.std.algebra { fold_list, list_snoc_item } +import v2.std.collection { List, empty_map } import v2.std.compilers.cli_surface { - CliSurface, - bound_tokens_cli_arguments, + CliArgumentSyntax, cli_argument_text, - cli_surface_arguments + cli_surface_arguments, + serialize_cli_arguments } import v2.std.compilers.lexing { LexRuleSet, @@ -17,121 +16,125 @@ import v2.std.compilers.lexing { ModeledLexRules, TokenRule } -import v2.std.compilers.target_model { - ConcreteSyntaxToken, - FixedToken, - bound_tokens_source_text, - render_target_text -} +import v2.std.compilers.target_model { FixedToken, bound_tokens_source_text, render_target_text } import v2.std.diagnostic { Accepted, Rejected } -// WAVE 0 PROBE (docs/plans/cli-invocation-emission-design.md). -// -// ONE question, executed rather than compiled: can the token sequence translate already produced -// be consumed by a non-text serializer, and does the argument boundary survive there while it is -// destroyed in the text carrier? +// WAVE 0 (docs/plans/cli-invocation-emission-design.md). // -// The two token spellings are chosen to be the smallest thing that can tell the carriers apart. -// The second contains a SPACE and a PIPE, which is exactly the shape that made the seventeen -// remote jq rows lose their argument boundary at the ssh seam. Concatenated, the two tokens are -// indistinguishable from any other split of the same characters; as arguments, they are two. +// WHAT AN EARLIER REVISION OF THIS WITNESS GOT WRONG, kept because it is the instructive part: +// it supplied exactly two tokens to a flat one-token-one-argument fold and asserted exactly two +// arguments came out. That CHOSE THE ARGUMENT SPLIT BEFORE THE SERIALIZER RAN. It proved "one +// token supplied, one argument retained" -- a restatement of the fold's own shape -- and not +// "the grammar groups fragments into arguments". // -// WHY THIS CANNOT PASS BY COMPILING. A compile-only probe would false-green: emit and -// serialize_target are fixed to Medium, 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 yields no diagnostic. -// Every assertion below therefore reads a VALUE produced by running the fold. - -data probe_option_class: String = "probe_option" +// The discriminating question is instead: do the SAME fragments, grouped two ways, produce two +// DIFFERENT surfaces while flattening to the same text? If grouping were not load-bearing, the +// two would be indistinguishable. That is the property an argv vector has and source text does +// not, so it is the property worth executing. -data probe_program_class: String = "probe_program" - -// The discriminating spelling: a space and a pipe, unquoted. -data probe_program_spelling: String = "[1,2] | length" - -data probe_option_spelling: String = "--argjson" +data probe_dash_option_class: String = "probe_dash_option" +data probe_equals_class: String = "probe_equals" +data probe_value_class: String = "probe_value" fn probe_lex_rules() -> ModeledLexRules { ModeledLexRules { root: LexRuleSet { rules: [ - TokenRule { - token_class: ^probe_option, - pattern: LiteralPattern { text: probe_option_spelling } - }, - TokenRule { - token_class: ^probe_program, - pattern: LiteralPattern { text: probe_program_spelling } - }, + TokenRule { token_class: ^probe_dash_option, pattern: LiteralPattern { text: "--color" } }, + TokenRule { token_class: ^probe_equals, pattern: LiteralPattern { text: "=" } }, + TokenRule { token_class: ^probe_value, pattern: LiteralPattern { text: "never" } }, ] } } } -fn probe_tokens() -> List { +// ONE argument composed of three fragments: within an argument, concatenation is CORRECT. +fn joined_grouping() -> List { + [ + CliArgumentSyntax { + fragments: [ + FixedToken { token_class: ^probe_dash_option }, + FixedToken { token_class: ^probe_equals }, + FixedToken { token_class: ^probe_value }, + ] + }, + ] +} + +// THREE arguments from the same three fragments: across arguments, concatenation DESTROYS. +fn separated_grouping() -> List { [ - FixedToken { token_class: ^probe_option }, - FixedToken { token_class: ^probe_program }, + CliArgumentSyntax { fragments: [FixedToken { token_class: ^probe_dash_option }] }, + CliArgumentSyntax { fragments: [FixedToken { token_class: ^probe_equals }] }, + CliArgumentSyntax { fragments: [FixedToken { token_class: ^probe_value }] }, ] } -// The CLI carrier preserves exactly two argument boundaries, and the second is the whole -// space-and-pipe-bearing program as ONE argument. -test fn cli_serializer_preserves_argument_boundaries() -> Bool { - match bound_tokens_cli_arguments( - tokens: probe_tokens(), +fn argument_texts(arguments: List) -> List { + match serialize_cli_arguments( + arguments: arguments, lex: probe_lex_rules(), binding_spellings: empty_map() ) { Accepted { value: surface, diagnostics: _ } => - match cli_surface_arguments(surface: surface) { + fold_list( + xs: cli_surface_arguments(surface: surface), + empty: Empty, + cons: fn(acc, argument) { + list_snoc_item(xs: acc, item: cli_argument_text(argument: argument)) + } + ) + Rejected { diagnostics: _ } => Empty + } +} + +// Grouped as one: exactly one argument, "--color=never". +test fn joined_fragments_render_one_argument() -> Bool { + match argument_texts(arguments: joined_grouping()) { + Empty => false + Cons { head: only, tail: rest } => + match rest { + Empty => only == "--color=never" + Cons { head: _, tail: _ } => false + } + } +} + +// Grouped as three: exactly three arguments, and the middle one is bare "=". +test fn separated_fragments_render_three_arguments() -> Bool { + match argument_texts(arguments: separated_grouping()) { + Empty => false + Cons { head: a, tail: r1 } => + match r1 { Empty => false - Cons { head: first, tail: rest } => - match rest { + Cons { head: b, tail: r2 } => + match r2 { Empty => false - Cons { head: second, tail: after } => - match after { - Empty => - (cli_argument_text(argument: first) == probe_option_spelling) - && (cli_argument_text(argument: second) == probe_program_spelling) + Cons { head: c, tail: r3 } => + match r3 { + Empty => (a == "--color") && (b == "=") && (c == "never") Cons { head: _, tail: _ } => false } } } - Rejected { diagnostics: _ } => false } } -// The text carrier over the SAME tokens produces one blob in which the boundary is gone. This is -// the negative half: it is not a complaint about the text serializer, which is correct for source -// text. It is the proof that the two carriers are genuinely different answers, so selecting the -// wrong one cannot pass this probe. -test fn text_serializer_loses_the_argument_boundary() -> Bool { +// THE KEYSTONE. Both groupings flatten to the same source text, so the text carrier cannot tell +// them apart at all. Grouping is therefore information the argv carrier holds and text does not +// -- which is exactly the fact the 17 remote jq rows lose at the ssh seam. +test fn both_groupings_flatten_to_the_same_text() -> Bool { match bound_tokens_source_text( - tokens: probe_tokens(), + tokens: [ + FixedToken { token_class: ^probe_dash_option }, + FixedToken { token_class: ^probe_equals }, + FixedToken { token_class: ^probe_value }, + ], lex: probe_lex_rules(), binding_spellings: empty_map() ) { Accepted { value: text, diagnostics: _ } => - render_target_text(t: text) == "--argjson[1,2] | length" + render_target_text(t: text) == "--color=never" Rejected { diagnostics: _ } => false } } - -fn probe_verdict() -> ProcessExit { - if cli_serializer_preserves_argument_boundaries() { - if text_serializer_loses_the_argument_boundary() { - ExitSuccess - } else { - ExitFailure { - code: 1, - reason: "text carrier did not render the expected concatenation; the probe is not comparing what it claims" - } - } - } else { - ExitFailure { - code: 1, - reason: "CLI carrier did not preserve exactly two argument boundaries" - } - } -} diff --git a/src/v2/std/compilers/cli_surface.dag b/src/v2/std/compilers/cli_surface.dag index 762ad2655c4..6b0871b197d 100644 --- a/src/v2/std/compilers/cli_surface.dag +++ b/src/v2/std/compilers/cli_surface.dag @@ -5,12 +5,10 @@ import std.types { String } import v2.std.algebra { fold_list, list_snoc_item } import v2.std.collection { List, Map } import v2.std.compilers.target_model { - BoundToken, ConcreteSyntaxToken, - FixedToken, LexRules, - bound_spelling_from_map, - lex_rules_literal_for_class + bound_tokens_source_text, + render_target_text } import v2.std.diagnostic { Accepted, @@ -66,6 +64,11 @@ import v2.std.node { Symbol } // admit only this probe, which is a wall around an empty room. DISSOLVES WITH: the wave that adds // the first production consumer, which is also the wave that answers the target-model question. +// One argv argument, as GRAMMAR: the fragments that compose it, before any spelling is resolved. +// Not sealed -- it is an input shape a tool's rows author, and sealing an input a caller must +// build would only push the forgery one level out. What is sealed is the OUTPUT. +type CliArgumentSyntax { fragments: List } + type CliArgument sole_constructor { text: String } type CliSurface sole_constructor { arguments: List } @@ -78,49 +81,68 @@ fn cli_argument_text(argument: CliArgument) -> String { argument.text } -// The sibling fold. Structurally identical to bound_tokens_source_text except that the -// accumulator is a list of arguments and each resolved spelling is snoc'd as its own argument -// rather than concatenated onto a running string. -fn bound_tokens_cli_arguments( - tokens: List, +// THE FOLD IS NESTED, AND THE NESTING IS THE WHOLE POINT. +// +// An earlier revision folded a FLAT List one-token-one-argument, and its +// witness supplied exactly two tokens and asserted exactly two arguments. That witness chose the +// argument split before the serializer ran, so it established "one token supplied, one argument +// retained" and NOT "the grammar groups fragments into arguments". The distinction is not +// pedantic: 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 there are two folds, not one. The inner fold resolves each fragment's spelling and +// concatenates WITHIN one argument. The outer fold preserves the argument boundary BETWEEN them. +// Both directions are then reachable from the same fragments, which is what makes the witness +// discriminating rather than self-fulfilling. +fn cli_argument_from_fragments( + fragments: List, + lex: LexRules, + binding_spellings: Map +) -> Outcome { + bind_outcome( + o: bound_tokens_source_text( + tokens: fragments, + lex: lex, + binding_spellings: binding_spellings + ), + f: fn(text) { + outcome_accepted(CliArgument { text: render_target_text(t: text) }) + } + ) +} + +fn serialize_cli_arguments( + arguments: List, lex: LexRules, binding_spellings: Map ) -> Outcome { bind_outcome( o: fold_list( - xs: tokens, + xs: arguments, empty: Accepted { value: Empty, diagnostics: None }, - cons: fn(acc, token) { + cons: fn(acc, argument) { match acc { Rejected { diagnostics: r } => Rejected { diagnostics: r } Accepted { value: partial, diagnostics: ad } => - match token { - FixedToken { token_class: tc } => - bind_outcome( - o: lex_rules_literal_for_class(rules: lex, token_class: tc), - f: fn(spelling) { - Accepted { - value: list_snoc_item(xs: partial, item: CliArgument { text: spelling }), - diagnostics: ad - } - } - ) - BoundToken { token_class: _, binding: b } => - bind_outcome( - o: bound_spelling_from_map(binding_spellings: binding_spellings, binding: b), - f: fn(spelling) { - Accepted { - value: list_snoc_item(xs: partial, item: CliArgument { text: spelling }), - diagnostics: ad - } - } - ) + match cli_argument_from_fragments( + fragments: argument.fragments, + lex: lex, + binding_spellings: binding_spellings + ) { + Rejected { diagnostics: r } => Rejected { diagnostics: r } + Accepted { value: rendered, diagnostics: _ } => + Accepted { + value: list_snoc_item(xs: partial, item: rendered), + diagnostics: ad + } } } } ), - f: fn(arguments) { - outcome_accepted(CliSurface { arguments: arguments }) + f: fn(rendered) { + outcome_accepted(CliSurface { arguments: rendered }) } ) } From 05f1c91b39573371c0dda8bf90026db56f1bdb68 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 19 Aug 2026 02:25:14 +0000 Subject: [PATCH 08/23] 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) --- dag/extdeps/tools/jq.dag | 277 +++++++++++++++++- .../claim/cli_surface_boundary_probe_test.dag | 77 +++-- .../jq_invocation_lowering_witness_test.dag | 128 ++++++++ docs/plans/cli-invocation-emission-design.md | 27 ++ src/v2/std/compilers/cli_surface.dag | 75 ++--- 5 files changed, 528 insertions(+), 56 deletions(-) create mode 100644 dag/test/claim/jq_invocation_lowering_witness_test.dag diff --git a/dag/extdeps/tools/jq.dag b/dag/extdeps/tools/jq.dag index 7777636554e..cf4cdb81ecf 100644 --- a/dag/extdeps/tools/jq.dag +++ b/dag/extdeps/tools/jq.dag @@ -1,6 +1,22 @@ module extdeps.tools.jq -import std.types { NonEmptyStr, String, Bool } +import std.types { NonEmptyStr, String, Bool, List } +import std.algebra { Cons, Empty } +import v2.std.algebra { list_append, list_snoc_item } +import v2.std.collection { Map, empty_map, map_insert } +import v2.std.compilers.cli_surface { CliArgumentSyntax, CliSurface, serialize_cli_arguments } +import v2.std.compilers.lexing { LexRuleSet, LiteralPattern, ModeledLexRules, TokenRule } +import v2.std.compilers.target_model { BoundToken, FixedToken } +import v2.std.diagnostic { + Diagnostic, + ExternalContractUnknown, + Outcome, + Unavailable, + node_locus, + outcome_rejected +} +import v2.std.node { Atom, Node, Symbol, SyntheticOccurrence, TypeNode } +import v2.std.optional { Absent, Optional, Present } import extdeps.external_authority { ExternalAuthority } import extdeps.uri { Uri, Https } import extdeps.tools { CliTool, SourceApt } @@ -35,3 +51,262 @@ service jq.Json { } } } + +// --------------------------------------------------------------------------------------------- +// WAVE 1A: the semantic invocation, and the two-level derivation from it to argv. +// docs/plans/cli-invocation-emission-design.md +// +// The caller describes WHAT IT WANTS OF JQ. It never names a flag. Nothing below is reachable +// from a domain module except through jq_invocation_cli_arguments, and that function emits the +// spellings rather than accepting them. + +// A jq program is opaque HERE on purpose. Modeling jq's expression language is a separate +// vertical from modeling its invocation structure, and conflating them would make this wave +// unbounded. It is a distinct type rather than a bare String so a program cannot be passed where +// a path or a binding value is expected. +type JqProgram { source: NonEmptyStr } + +type JqBindingName { name: NonEmptyStr } + +type JqBinding + = JqJsonBinding { name: JqBindingName, value: NonEmptyStr } + | JqTextBinding { name: JqBindingName, value: String } + +// Input is an AXIS, not an operand, because the two arms differ in WHERE the bytes go: a file is +// an argv operand, stdin is a process channel. An argv-only model cannot state that difference, +// which is the same gap extdeps.llm.cursor_cli hit when an environment credential had no field. +type JqInput + = JqInputFile { path: NonEmptyStr } + | JqInputStdin { content: String } + +// -r writes STRING results raw; non-string results stay JSON-formatted. Hence JqRawOutput rather +// than a "RawText" that would overclaim what the flag does. +type JqOutputEncoding + = JqJsonOutput + | JqRawOutput + +// The exit CONTRACT the caller is asking for, not a flag. Under JqProgramExit jq exits 0 when the +// program ran, INCLUDING when it emitted nothing -- so "produced no result" is not observable on +// this arm, and a domain that needs absence reads empty stdout instead. Under JqLastResultExit jq +// reports 1 for a false-or-null last output and 4 for no valid result. +type JqExitPolicy + = JqProgramExit + | JqLastResultExit + +type JqInvocation { + program: JqProgram + bindings: List + input: JqInput + output_encoding: JqOutputEncoding + exit_policy: JqExitPolicy +} + +// LEVEL ONE of the derivation: a semantic property SELECTS an option identity. This is the level +// that makes omission impossible -- a JqInvocation carrying JqRawOutput cannot reach argv without +// the raw-output option, because the selection is a total function over the coproduct rather than +// an "if policy is X, append Y" a fold could forget. +type JqCliOption + = JqCliOptionRawOutput + | JqCliOptionExitStatus + | JqCliOptionArgJson + | JqCliOptionArg + +// ABSENCE IS A DECLARED ROW, NOT A MISSING ONE. An earlier revision returned Optional +// and answered Absent for JqProgramExit -- which makes "this policy deliberately requires no +// option" and "nobody wrote a row for this policy" the SAME VALUE. That is the state-space +// conflation DESIGN names, built here while writing about it: the two states have different +// remedies (one is correct, one is a missing row that should refuse) and the Optional collapsed +// them. JqCliNoOptionRequired is the deliberate case stated out loud, so a genuinely absent row +// has somewhere else to go. +type JqCliSelection + = JqCliOptionSelected { option: JqCliOption } + | JqCliNoOptionRequired + +fn jq_selection_for_output_encoding(encoding: JqOutputEncoding) -> JqCliSelection { + match encoding { + JqJsonOutput => JqCliNoOptionRequired + JqRawOutput => JqCliOptionSelected { option: JqCliOptionRawOutput } + } +} + +fn jq_selection_for_exit_policy(policy: JqExitPolicy) -> JqCliSelection { + match policy { + JqProgramExit => JqCliNoOptionRequired + JqLastResultExit => JqCliOptionSelected { option: JqCliOptionExitStatus } + } +} + +fn jq_option_for_binding(binding: JqBinding) -> JqCliOption { + match binding { + JqJsonBinding { name: _, value: _ } => JqCliOptionArgJson + JqTextBinding { name: _, value: _ } => JqCliOptionArg + } +} + +// LEVEL TWO: an option identity selects its CITED SPELLING. jqlang.org/manual/ is the authority +// for every string below; the long form is canonical because it is self-describing at a call +// site, and the short alias is recorded as a fact about jq rather than used. +fn jq_option_token_class(option: JqCliOption) -> Symbol { + match option { + JqCliOptionRawOutput => ^jq_opt_raw_output + JqCliOptionExitStatus => ^jq_opt_exit_status + JqCliOptionArgJson => ^jq_opt_argjson + JqCliOptionArg => ^jq_opt_arg + } +} + +// THE ROW STORES THE BARE LONG NAME. An earlier revision stored "--raw-output", which bakes a +// SHARED GRAMMAR RULE (a long option renders as two hyphens followed by its name) into a +// per-tool row -- so every tool would re-spell the same rule and a tool could silently disagree +// with it. The tool owns which names exist and which form is canonical; the grammar owns how a +// chosen form is constructed. +fn jq_option_long_name(option: JqCliOption) -> NonEmptyStr { + match option { + JqCliOptionRawOutput => "raw-output" + JqCliOptionExitStatus => "exit-status" + JqCliOptionArgJson => "argjson" + JqCliOptionArg => "arg" + } +} + +fn jq_option_canonical_spelling(option: JqCliOption) -> NonEmptyStr { + cli_long_option_spelling(name: jq_option_long_name(option: option)) +} + +// The short aliases jq also accepts. Declared so the corpus records what jq's surface IS, and +// deliberately not consulted by the lowering: a caller cannot ask for -r over --raw-output, +// because which form is canonical is jq's decision and not the caller's. +// The short names jq also accepts, again bare: the grammar renders one hyphen. argjson and arg +// have no short form, which is a fact about jq rather than an omission here. +fn jq_option_short_name(option: JqCliOption) -> Optional { + match option { + JqCliOptionRawOutput => Present { value: "r" } + JqCliOptionExitStatus => Present { value: "e" } + JqCliOptionArgJson => Absent + JqCliOptionArg => Absent + } +} + +// The lex table jq itself authors: one row per option identity, spelling from the cited rows +// above. A caller cannot supply this -- which is half of closing the Wave 0 mint hole, because +// arbitrary content can no longer be spelled through a caller-authored table on the jq path. +fn jq_cli_lex_rules() -> ModeledLexRules { + ModeledLexRules { + root: LexRuleSet { + rules: [ + TokenRule { + token_class: jq_option_token_class(option: JqCliOptionRawOutput), + pattern: LiteralPattern { text: jq_option_canonical_spelling(option: JqCliOptionRawOutput) } + }, + TokenRule { + token_class: jq_option_token_class(option: JqCliOptionExitStatus), + pattern: LiteralPattern { text: jq_option_canonical_spelling(option: JqCliOptionExitStatus) } + }, + TokenRule { + token_class: jq_option_token_class(option: JqCliOptionArgJson), + pattern: LiteralPattern { text: jq_option_canonical_spelling(option: JqCliOptionArgJson) } + }, + TokenRule { + token_class: jq_option_token_class(option: JqCliOptionArg), + pattern: LiteralPattern { text: jq_option_canonical_spelling(option: JqCliOptionArg) } + }, + ] + } + } +} + +// WHAT THE PROCESS NEEDS, which is more than an argv: an argv is not a process. The stdin arm is +// carried here rather than smuggled into the arguments, so a consumer physically cannot route the +// JSON payload through argv by mistake. +type JqProcessPlan { + arguments: List + binding_spellings: Map + stdin: String? +} + +type JqLowering + = JqLowered { plan: JqProcessPlan } + | JqLoweringRefused { reason: NonEmptyStr } + +// The lowering REFUSES the axes this wave has no live consumer for, rather than emitting a +// plausible guess. Bindings land with ObjectMapperServiceAt (the --argjson vertical) and file +// input with the remote population; until then an invocation carrying them is a typed, located +// refusal, never a silently dropped flag. DESIGN section 5: a failure arm must refuse, never +// widen -- and never fabricate. +fn jq_invocation_lower(invocation: JqInvocation) -> JqLowering { + match invocation.bindings { + Cons { head: _, tail: _ } => + JqLoweringRefused { + reason: "jq bindings are not lowered yet; the --arg/--argjson vertical lands with ObjectMapperServiceAt" + } + Empty => + match invocation.input { + JqInputFile { path: _ } => + JqLoweringRefused { + reason: "jq file input is not lowered yet; the operand vertical lands with the remote population" + } + JqInputStdin { content: content } => + JqLowered { + plan: JqProcessPlan { + arguments: jq_option_arguments(invocation: invocation), + binding_spellings: map_insert( + m: empty_map(), + key: ^jq_program_text, + value: invocation.program.source as String + ), + stdin: Present { value: content } + } + } + } + } +} + +// Options first, then the program operand. Order is jq's, not the caller's: POSIX guideline 9 +// puts options before operands, and jq does not deviate. +fn jq_option_arguments(invocation: JqInvocation) -> List { + list_snoc_item( + xs: list_append( + left: jq_selected_option_argument(selection: jq_selection_for_output_encoding(encoding: invocation.output_encoding)), + right: jq_selected_option_argument(selection: jq_selection_for_exit_policy(policy: invocation.exit_policy)) + ), + item: CliArgumentSyntax { + fragments: [BoundToken { token_class: ^jq_program_operand, binding: ^jq_program_text }] + } + ) +} + +fn jq_selected_option_argument(selection: JqCliSelection) -> List { + match selection { + JqCliNoOptionRequired => Empty + JqCliOptionSelected { option: chosen } => + [CliArgumentSyntax { + fragments: [FixedToken { token_class: jq_option_token_class(option: chosen) }] + }] + } +} + +// The one function a domain module calls. It returns the exact argument vector, or refuses. +fn jq_invocation_cli_arguments(invocation: JqInvocation) -> Outcome { + match jq_invocation_lower(invocation: invocation) { + JqLoweringRefused { reason: reason } => + outcome_rejected(jq_lowering_refused_diagnostic(reason: reason)) + JqLowered { plan: plan } => + serialize_cli_arguments( + arguments: plan.arguments, + lex: jq_cli_lex_rules(), + binding_spellings: plan.binding_spellings + ) + } +} + +fn jq_lowering_refused_diagnostic(reason: NonEmptyStr) -> Diagnostic { + Diagnostic { + reason: ^jq_lowering_refused, + at: node_locus(node: Node { + kind: TypeNode { connective: Atom { identity: ^jq_invocation_lowering } }, + children: [], + occurrence_id: SyntheticOccurrence + }), + correction: Unavailable { reason: ExternalContractUnknown } + } +} diff --git a/dag/test/claim/cli_surface_boundary_probe_test.dag b/dag/test/claim/cli_surface_boundary_probe_test.dag index 7f4247df8f0..d25d168ba76 100644 --- a/dag/test/claim/cli_surface_boundary_probe_test.dag +++ b/dag/test/claim/cli_surface_boundary_probe_test.dag @@ -2,7 +2,7 @@ module test.claim.cli_surface_boundary_probe import std.algebra { Cons, Empty } import std.types { Bool, String } -import v2.std.algebra { fold_list, list_snoc_item } +import v2.std.algebra { fold_list, list_append, list_snoc_item } import v2.std.collection { List, empty_map } import v2.std.compilers.cli_surface { CliArgumentSyntax, @@ -16,7 +16,7 @@ import v2.std.compilers.lexing { ModeledLexRules, TokenRule } -import v2.std.compilers.target_model { FixedToken, bound_tokens_source_text, render_target_text } +import v2.std.compilers.target_model { ConcreteSyntaxToken, FixedToken, bound_tokens_source_text, render_target_text } import v2.std.diagnostic { Accepted, Rejected } // WAVE 0 (docs/plans/cli-invocation-emission-design.md). @@ -48,26 +48,42 @@ fn probe_lex_rules() -> ModeledLexRules { } } -// ONE argument composed of three fragments: within an argument, concatenation is CORRECT. -fn joined_grouping() -> List { +// ONE AUTHORITY for the fragments. An earlier revision authored the same three tokens in three +// places, so "the SAME fragments grouped two ways" was maintained by author discipline: one +// grouping could drift while the flattening test kept passing. Both groupings and the flattening +// check now derive from this list, which makes the keystone mechanically true instead of copied. +fn probe_fragments() -> List { [ - CliArgumentSyntax { - fragments: [ - FixedToken { token_class: ^probe_dash_option }, - FixedToken { token_class: ^probe_equals }, - FixedToken { token_class: ^probe_value }, - ] - }, + FixedToken { token_class: ^probe_dash_option }, + FixedToken { token_class: ^probe_equals }, + FixedToken { token_class: ^probe_value }, ] } -// THREE arguments from the same three fragments: across arguments, concatenation DESTROYS. +// All fragments in ONE argument: within an argument, concatenation is CORRECT. +fn joined_grouping() -> List { + [CliArgumentSyntax { fragments: probe_fragments() }] +} + +// Each fragment its OWN argument: across arguments, concatenation DESTROYS. fn separated_grouping() -> List { - [ - CliArgumentSyntax { fragments: [FixedToken { token_class: ^probe_dash_option }] }, - CliArgumentSyntax { fragments: [FixedToken { token_class: ^probe_equals }] }, - CliArgumentSyntax { fragments: [FixedToken { token_class: ^probe_value }] }, - ] + fold_list( + xs: probe_fragments(), + empty: Empty, + cons: fn(acc, fragment) { + list_snoc_item(xs: acc, item: CliArgumentSyntax { fragments: [fragment] }) + } + ) +} + +// Flatten a grouping back to the fragment sequence it was built from, so the keystone compares +// the ACTUAL grouping values rather than a third hand-authored list. +fn flatten_grouping(arguments: List) -> List { + fold_list( + xs: arguments, + empty: Empty, + cons: fn(acc, argument) { list_append(left: acc, right: argument.fragments) } + ) } fn argument_texts(arguments: List) -> List { @@ -123,13 +139,30 @@ test fn separated_fragments_render_three_arguments() -> Bool { // THE KEYSTONE. Both groupings flatten to the same source text, so the text carrier cannot tell // them apart at all. Grouping is therefore information the argv carrier holds and text does not // -- which is exactly the fact the 17 remote jq rows lose at the ssh seam. +fn grouping_flat_text(arguments: List) -> String { + match bound_tokens_source_text( + tokens: flatten_grouping(arguments: arguments), + lex: probe_lex_rules(), + binding_spellings: empty_map() + ) { + Accepted { value: text, diagnostics: _ } => render_target_text(t: text) + Rejected { diagnostics: _ } => "" + } +} + +// THE KEYSTONE, now comparing the two ACTUAL grouping values rather than a hand-copied list: +// both flatten to identical text, so the text carrier cannot separate them at all, while the +// two assertions above show the argv carrier does. Grouping is exactly the information the argv +// vector holds and source text loses -- which is what the 17 remote jq rows lose at the ssh seam. test fn both_groupings_flatten_to_the_same_text() -> Bool { + (grouping_flat_text(arguments: joined_grouping()) == "--color=never") + && (grouping_flat_text(arguments: joined_grouping()) + == grouping_flat_text(arguments: separated_grouping())) +} + +test fn keystone_flat_text_is_nonempty() -> Bool { match bound_tokens_source_text( - tokens: [ - FixedToken { token_class: ^probe_dash_option }, - FixedToken { token_class: ^probe_equals }, - FixedToken { token_class: ^probe_value }, - ], + tokens: flatten_grouping(arguments: separated_grouping()), lex: probe_lex_rules(), binding_spellings: empty_map() ) { diff --git a/dag/test/claim/jq_invocation_lowering_witness_test.dag b/dag/test/claim/jq_invocation_lowering_witness_test.dag new file mode 100644 index 00000000000..1b693299a1b --- /dev/null +++ b/dag/test/claim/jq_invocation_lowering_witness_test.dag @@ -0,0 +1,128 @@ +module test.claim.jq_invocation_lowering_witness + +import std.algebra { Cons, Empty } +import std.types { Bool, String } +import v2.std.algebra { fold_list, list_snoc_item } +import v2.std.collection { List } +import v2.std.compilers.cli_surface { cli_argument_text, cli_surface_arguments } +import v2.std.diagnostic { Accepted, Rejected } +import extdeps.tools.jq { + JqInputFile, + JqInputStdin, + JqInvocation, + JqJsonBinding, + JqBindingName, + JqLastResultExit, + JqProgram, + JqProgramExit, + JqRawOutput, + jq_invocation_cli_arguments +} + +// WAVE 1A. The semantic invocation SensorIntegerValue will make, lowered to argv. +// docs/plans/cli-invocation-emission-design.md +// +// The point of every assertion below is that the caller named no flag. It asked for raw output +// and for jq's ordinary exit contract; --raw-output and the ABSENCE of --exit-status are derived. + +data sensor_stdin: String = "{\"data\": 41.6}" + +data sensor_program: String = "if (.data | type) == \"number\" then (.data | round) else empty end" + +fn sensor_invocation() -> JqInvocation { + JqInvocation { + program: JqProgram { source: sensor_program }, + bindings: Empty, + input: JqInputStdin { content: sensor_stdin }, + output_encoding: JqRawOutput, + exit_policy: JqProgramExit, + } +} + +fn argv_of(invocation: JqInvocation) -> List { + match jq_invocation_cli_arguments(invocation: invocation) { + Accepted { value: surface, diagnostics: _ } => + fold_list( + xs: cli_surface_arguments(surface: surface), + empty: Empty, + cons: fn(acc, a) { list_snoc_item(xs: acc, item: cli_argument_text(argument: a)) } + ) + Rejected { diagnostics: _ } => Empty + } +} + +// JqRawOutput selects the raw-output option and it renders in its CANONICAL long form, not -r. +// JqProgramExit selects NO exit-status option. The program is exactly ONE argument even though it +// contains spaces, quotes and parentheses. +test fn sensor_invocation_lowers_to_exact_argv() -> Bool { + match argv_of(invocation: sensor_invocation()) { + Empty => false + Cons { head: first, tail: rest } => + match rest { + Empty => false + Cons { head: second, tail: after } => + match after { + Empty => (first == "--raw-output") && (second == sensor_program) + Cons { head: _, tail: _ } => false + } + } + } +} + +// THE STDIN CONTROL. The JSON payload is a process channel, not an argument: it must appear +// nowhere in argv. An argv-only model could not even state this. +test fn stdin_content_is_absent_from_argv() -> Bool { + fold_list( + xs: argv_of(invocation: sensor_invocation()), + empty: true, + cons: fn(acc, arg) { acc && (arg != sensor_stdin) } + ) +} + +// PERTURBATION, LEVEL ONE: change the semantic property and the emitted vector changes. This is +// what proves the SELECTION row is authoritative rather than decorative -- a spelling-only test +// would pass even if the option could be omitted. +test fn exit_policy_perturbation_adds_the_exit_status_option() -> Bool { + match argv_of(invocation: JqInvocation { + program: JqProgram { source: sensor_program }, + bindings: Empty, + input: JqInputStdin { content: "{}" }, + output_encoding: JqRawOutput, + exit_policy: JqLastResultExit, + }) { + Empty => false + Cons { head: first, tail: rest } => + match rest { + Empty => false + Cons { head: second, tail: _ } => + (first == "--raw-output") && (second == "--exit-status") + } + } +} + +// The unlowered axes REFUSE rather than emitting a plausible guess. +test fn unlowered_bindings_refuse() -> Bool { + match jq_invocation_cli_arguments(invocation: JqInvocation { + program: JqProgram { source: sensor_program }, + bindings: [JqJsonBinding { name: JqBindingName { name: "index" }, value: "3" }], + input: JqInputStdin { content: "{}" }, + output_encoding: JqRawOutput, + exit_policy: JqProgramExit, + }) { + Rejected { diagnostics: _ } => true + Accepted { value: _, diagnostics: _ } => false + } +} + +test fn unlowered_file_input_refuses() -> Bool { + match jq_invocation_cli_arguments(invocation: JqInvocation { + program: JqProgram { source: sensor_program }, + bindings: Empty, + input: JqInputFile { path: "/tmp/x.json" }, + output_encoding: JqRawOutput, + exit_policy: JqProgramExit, + }) { + Rejected { diagnostics: _ } => true + Accepted { value: _, diagnostics: _ } => false + } +} diff --git a/docs/plans/cli-invocation-emission-design.md b/docs/plans/cli-invocation-emission-design.md index 72b73eee6f7..acfcaf24ad5 100644 --- a/docs/plans/cli-invocation-emission-design.md +++ b/docs/plans/cli-invocation-emission-design.md @@ -773,6 +773,33 @@ General argument typechecking strengthens the boundary; it does not prove that p path already demonstrates rather than retaining `shell_quote`. 7. Reverse ingestion — reading argv back through the same rows — is the terminal second reading and is **not a prerequisite for the first emitter cut**. +8. **Measured substrate observation — `Optional` at a primitive `T` in record-field + construction position.** `stdin: Optional` with an inline `Present { value: … }` + refuses with `expected 'Coproduct(Optional)', got 'Primitive(String)'`, and the refusal is + independent of the payload expression: a pattern-bound variable, a renamed binding, a + shorthand pattern, and a bare `"x"` literal all reproduce it, while `stdin: Absent` resolves. + Inline `Present` into an explicitly-declared `Optional` field is ordinary elsewhere in the + tree (`gunbc.witness_row_cost` `basis`, `gunbc.declared_import_closure_binding` + `binding_source`, `v2.workflow.effect_plan_bash_materialize` `operation`), but every such `T` + observed is a record or coproduct — so the discriminator is the **primitive type argument**, + not the field form and not the explicit-vs-sugar spelling. This lane uses the corpus's own + `String?` sugar, which is the existing modeled form for an optional field (625 sites) rather + than a workaround around an unexplained error. **The observation is recorded, not diagnosed:** + whether the sugar and the explicit generic genuinely differ at a primitive argument, or the + refusal has another cause this bisect did not separate, is unestablished — and a §5 line-stop + is owed on it before anything else in this lane relies on the distinction. + +9. **A downstream typed verdict may be the redundant lower rung, not a peer** (raised by + `eager-wren-138`, 2026-08-18). `gunbc.host_effect_realize` `bmcweb_token_extraction_verdict` + refuses blank stdout as its own decode — the wall that actually closed that fail-open, with + `jq -e` only ever loudness beside it. If the semantic layer makes *absence-is-a-value* + unwritable at the decode, that verdict is a second representation of one requirement (§2/§3) + and must **dissolve into** the decode rather than sit beside it. This is a §4b climb, so its + discriminating RED stays enrolled against the new decode while the production check is the + part deleted. Open because it is not yet established whether the requirement is exactly one + nonempty string at *every* consumer or only at the credential path; the OpenBMC sensor path + models absence as a legitimate third state (`OpenBmcSensorValueAbsent`), so a blanket + absence-is-refusal decode would be the state-space collapse this lane exists to remove. --- diff --git a/src/v2/std/compilers/cli_surface.dag b/src/v2/std/compilers/cli_surface.dag index 6b0871b197d..7f781c83ecb 100644 --- a/src/v2/std/compilers/cli_surface.dag +++ b/src/v2/std/compilers/cli_surface.dag @@ -1,7 +1,7 @@ module v2.std.compilers.cli_surface import std.algebra { Empty } -import std.types { String } +import std.types { NonEmptyStr, String } import v2.std.algebra { fold_list, list_snoc_item } import v2.std.collection { List, Map } import v2.std.compilers.target_model { @@ -14,6 +14,9 @@ import v2.std.diagnostic { Accepted, None, Outcome, + ShortCircuit, + StageDiagnosticPolicy, + append_outcome_value, Rejected, bind_outcome, outcome_accepted @@ -21,23 +24,18 @@ import v2.std.diagnostic { import v2.std.node { Symbol } -// WHY THIS EXISTS, and why it is a sibling rather than a transform of the text carrier. +// WHY THIS EXISTS. // -// v2.std.compilers.target_model.bound_tokens_source_text folds a grammar-selected token sequence -// into TargetText, resolving each token to its spelling and joining with target_text_seq, which is -// concatenation. Concatenation is the step that DESTROYS argument boundaries: once the tokens are -// one String, "a b" and ["a", "b"] are the same value, and every consumer downstream must -// re-derive a boundary that the grammar already knew. That re-derivation is what shell_quote is, -// at 36 sites. +// CliArgumentSyntax preserves the GROUPING a tool's CLI projection selected. bound_tokens_source_text +// is reused only INSIDE one argument, where concatenation is correct (["--color","=","never"] is the +// single argument --color=never). The outer fold preserves boundaries BETWEEN arguments, which is +// the information an argv vector carries and source text cannot. // -// This module folds the SAME tokens with the SAME spelling resolution and a DIFFERENT join: one -// argument per token. Nothing about the grammar walk changes; only whether the boundary survives. -// That is the whole claim the CLI-invocation-emission design rests on, reduced to the smallest -// thing that can be executed -- see docs/plans/cli-invocation-emission-design.md, Wave 0. -// -// NOT A SECOND EMITTER. It consumes what translate already produced. A target model that wants -// argument boundaries selects this serializer; one that wants source text selects the existing -// one. Both read one grammar. +// This module consumes ConcreteSyntaxToken. It does NOT consume compiler translate output and is +// independent of TargetModel as a semantic authority -- an earlier revision of this comment +// asserted the opposite on both counts, and asserted a flat one-token-one-argument fold that no +// longer exists. Those claims are gone rather than amended, because a file that states the +// refuted architecture above the corrected one hands its next reader two plausible instructions. // SEALED AT THE RECORD, NOT AT THE MINT -- and the difference is a live hole, stated here // because an earlier revision of this comment claimed the opposite and was wrong. @@ -69,6 +67,19 @@ import v2.std.node { Symbol } // build would only push the forgery one level out. What is sealed is the OUTPUT. type CliArgumentSyntax { fragments: List } +// THE SHARED RENDERING RULE, owned here and not by any tool row. A tool declares WHICH names +// exist and which form is canonical; how a long name becomes two hyphens plus the name, or a +// short name one hyphen plus the character, is one rule every POSIX-conventional tool shares +// (IEEE Std 1003.1-2024 XBD 12). A tool row storing "--raw-output" would re-spell that rule per +// tool and could silently disagree with it. +fn cli_long_option_spelling(name: NonEmptyStr) -> NonEmptyStr { + concat("--", name) +} + +fn cli_short_option_spelling(name: NonEmptyStr) -> NonEmptyStr { + concat("-", name) +} + type CliArgument sole_constructor { text: String } type CliSurface sole_constructor { arguments: List } @@ -113,6 +124,11 @@ fn cli_argument_from_fragments( ) } +// The outer fold routes through append_outcome_value rather than re-implementing part of the +// Outcome algebra. An earlier revision matched the inner result and bound its accepted +// diagnostics to _, silently ERASING evidence the spelling fold had produced -- latent only +// because these rows happen to return None today. A generic serializer must not drop diagnostics +// because its first callers had none. fn serialize_cli_arguments( arguments: List, lex: LexRules, @@ -121,24 +137,17 @@ fn serialize_cli_arguments( bind_outcome( o: fold_list( xs: arguments, - empty: Accepted { value: Empty, diagnostics: None }, + empty: outcome_accepted(Empty), cons: fn(acc, argument) { - match acc { - Rejected { diagnostics: r } => Rejected { diagnostics: r } - Accepted { value: partial, diagnostics: ad } => - match cli_argument_from_fragments( - fragments: argument.fragments, - lex: lex, - binding_spellings: binding_spellings - ) { - Rejected { diagnostics: r } => Rejected { diagnostics: r } - Accepted { value: rendered, diagnostics: _ } => - Accepted { - value: list_snoc_item(xs: partial, item: rendered), - diagnostics: ad - } - } - } + append_outcome_value( + acc: acc, + child: cli_argument_from_fragments( + fragments: argument.fragments, + lex: lex, + binding_spellings: binding_spellings + ), + policy: StageDiagnosticPolicy { accumulation: ShortCircuit } + ) } ), f: fn(rendered) { From 736612ffd89097793862d2a5035adc5466dd1040 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 19 Aug 2026 02:26:33 +0000 Subject: [PATCH 09/23] 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) --- docs/plans/cli-invocation-emission-design.md | 22 +++++++++++++++++++- 1 file changed, 21 insertions(+), 1 deletion(-) diff --git a/docs/plans/cli-invocation-emission-design.md b/docs/plans/cli-invocation-emission-design.md index acfcaf24ad5..84180b33c6f 100644 --- a/docs/plans/cli-invocation-emission-design.md +++ b/docs/plans/cli-invocation-emission-design.md @@ -648,7 +648,8 @@ error. | exact subject | honest rung after the first vertical | mechanism | |---|---|---| -| forging a `CliInvocationTree` / `CliSurface` / `JqObservation` | **structurally impossible now** | `sole_constructor`; only the row emitter, serializer and decoder may mint | +| forging a `CliSurface` **by record literal or cast** | structurally impossible | `sole_constructor`, whose cross-module refusal is witnessed by the corpus `sole-constructor-cross-module` probes — not re-proved here | +| minting a `CliSurface` **whose content did not come from rows** | **mitigatable only** | *no wall.* `serialize_cli_arguments` is public and accepts caller-supplied `lex` and fragments, so any module can obtain a well-typed `CliSurface` carrying arbitrary text | | omitting `--exit-status` from an accepted truthiness invocation | **structurally impossible within the new path** | exhaustive semantic→option selection; zero-or-many rows refuse; no mint on miss | | hand-authoring flags inside a migrated route | **structurally impossible after cutover** | handler takes a semantic invocation, emits internally, old argv site deleted | | reintroducing the exact old operation transport | mechanically preventable | structural deletion witness | @@ -658,6 +659,25 @@ error. So: **the first migrated jq path can be structural now; the repository-wide raw-jq class stays open; the repository-wide raw-argv class is a later migration.** +**The seal is on the shape, not on the provenance — corrected 2026-08-19.** The row above +previously read *structurally impossible now — only the row emitter, serializer and decoder may +mint*, which is false and was the §4b inflation this document warns about, asserted about this +document's own subject. `sole_constructor` closes the record literal and the cast; it says nothing +about a **public fold that takes caller-supplied inputs**, and `serialize_cli_arguments` is +exactly that. An 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, and `CliSurface`'s is not sealed at all. + +**Ceiling and trigger, stated rather than left implied.** The obvious repair — `admit_callers` on +the serializer — is refused on §3 grounds: it would make `v2.std.compilers.cli_surface` name every +tool module that may emit a CLI, which is dispatch fused into the interface, the thing this lane +exists to keep peripheral. So the wall belongs on the **input**, not on the serializer: a sealed +`AdmittedCliInvocation` that only a tool's own row-derived lowering can produce, with the +serializer total over it. That is **not built**, and the design of its mint is genuinely open — +whatever seals it faces the same recursion one level up. Until it lands, provenance sits at +*mitigatable*, and the practical containment is that the only public jq entry point is +`jq_invocation_cli_arguments`, which is a convention, not a wall. + **Application-argument typechecking is not the terminal trigger.** The `04_infer` gap is real — `explicit_return_conformance_note` records that conformance is judged only by the ground-kernel-scalar and ground-element-collection discipline — but it is neither *necessary* for From d807a3aa8eb0e7cfb96816b85125a1165882de79 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 19 Aug 2026 02:51:04 +0000 Subject: [PATCH 10/23] 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) --- src/v2/std/compilers/cli_surface.dag | 25 ++++++++++++++++++------- 1 file changed, 18 insertions(+), 7 deletions(-) diff --git a/src/v2/std/compilers/cli_surface.dag b/src/v2/std/compilers/cli_surface.dag index 7f781c83ecb..bcbfa2351e7 100644 --- a/src/v2/std/compilers/cli_surface.dag +++ b/src/v2/std/compilers/cli_surface.dag @@ -44,7 +44,7 @@ import v2.std.node { Symbol } // cast into one. The record literal and the cast are both closed (04_infer // sole_constructor_construction_diags judges the two forms through one authority). // -// WHAT DOES NOT HOLD: bound_tokens_cli_arguments below is public and takes tokens, lex rules AND +// WHAT DOES NOT HOLD: serialize_cli_arguments below is public and takes tokens, lex rules AND // binding spellings FROM ITS CALLER, so any module can synthesize whatever token sequence and lex // table it likes and receive a sealed CliSurface carrying arbitrary content. You cannot author // the record; you can author its contents. That is the mint-function hole gunbc.guarantee_probe_corpus @@ -55,12 +55,23 @@ import v2.std.node { Symbol } // this fold admits everyone. The claim was made, reviewed, and corroborated once before anyone // checked it -- which is why it is written down here rather than quietly amended. // -// WHY IT IS NOT CLOSED IN THIS COMMIT: the fix is to stop taking caller-supplied grammar at all -- -// the fold should be reachable only already bound to a target model, so the lex table is the -// target's rather than the caller's -- and that shape is decided by whether the jq path consumes -// translate's target model or bypasses it entirely. Sealing to 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, which is also the wave that answers the target-model question. +// WHY IT IS NOT CLOSED IN THIS COMMIT -- and the open question this comment used to defer to is +// now ANSWERED. It read: the shape "is decided by whether the jq path consumes translate's target +// model or bypasses it entirely." Wave 1A answered that 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" is not available as the repair -- there is no target model on this path. +// +// THE REPAIR, RESTATED: seal the INPUT, not the fold. A sealed AdmittedCliInvocation that only a +// tool's own row-derived lowering can produce, with the serializer total over it. admit_callers on +// the serializer is REFUSED on DESIGN section 3 grounds, and not merely because the roster would be +// short: it would make this std module name every tool module permitted to emit a CLI, which is +// dispatch fused into the interface -- the exact shape this lane exists to keep peripheral. +// +// NOT BUILT, and its mint's design is genuinely open, because whatever seals AdmittedCliInvocation +// faces the same recursion one level up. Until it lands, provenance sits at MITIGATABLE and the +// only containment is that jq's single public entry point is jq_invocation_cli_arguments -- a +// convention, not a wall. DISSOLVES WITH: that sealed input carrier, not with "the first +// production consumer", which was the previous trigger and would have fired without closing this. // One argv argument, as GRAMMAR: the fragments that compose it, before any spelling is resolved. // Not sealed -- it is an input shape a tool's rows author, and sealing an input a caller must From cf1ee9f7a259bfd21aee0cbfaed1e9ca5a4d0381 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 19 Aug 2026 02:52:38 +0000 Subject: [PATCH 11/23] 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 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) --- docs/plans/cli-invocation-emission-design.md | 41 +++++++++++++++++++- 1 file changed, 40 insertions(+), 1 deletion(-) diff --git a/docs/plans/cli-invocation-emission-design.md b/docs/plans/cli-invocation-emission-design.md index 84180b33c6f..9f39bbbd060 100644 --- a/docs/plans/cli-invocation-emission-design.md +++ b/docs/plans/cli-invocation-emission-design.md @@ -809,7 +809,46 @@ General argument typechecking strengthens the boundary; it does not prove that p refusal has another cause this bisect did not separate, is unestablished — and a §5 line-stop is owed on it before anything else in this lane relies on the distinction. -9. **A downstream typed verdict may be the redundant lower rung, not a peer** (raised by +9. **The spelling-seam extraction is right, but its obvious shape is forbidden — corrected + 2026-08-19.** The static-dependency finding stands: at execution grain the jq fold reaches no + compiler machinery, but at dependency grain `cli_surface` imports `v2.std.compilers.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 proposed repair — extract a shared `spell_concrete_syntax_fragments -> Outcome` + below `target_model`, and have the TargetText serializer wrap its result — **violates an + operator ruling carried in the file it would edit.** `target_model` `target_text_carrier_scaffold_note` + (operator, 2026-07-15) places `TargetText` beside `bound_tokens_source_text` so that fold is + *carrier-native*: the single `String -> TargetText` 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** `String -> TargetText` lift + of an already-composed unit, "that direction is the smuggle the wall closes." Wrapping a + composed `String` is precisely that lift. + + **The corrected decomposition, and it is the better one 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`, and those are different media. So the extraction moves the token type and the two + token-grain lookups into `v2.std.compilers.concrete_syntax`, `target_model` imports them back + (re-export is proven to work — see below), and each carrier keeps 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 result alone proves + nothing, because this resolver can bind by *pool-membership coincidence* (DESIGN's Class B + finding). The discriminating control settles it: importing the same symbol from a bystander + module that never saw it **refuses**, located — `name 'ProbeToken' not found in module + '...bystander'` — even with the defining module in the pool. Qualified-import resolution is + import-list-driven, so `target_model` importing the seam back keeps its 167 other importers + untouched. + + **Not performed.** `target_model` is load-bearing and carries the ruling above, so the move is + its own increment under its own review, not a rider on this one. + +10. **A downstream typed verdict may be the redundant lower rung, not a peer** (raised by `eager-wren-138`, 2026-08-18). `gunbc.host_effect_realize` `bmcweb_token_extraction_verdict` refuses blank stdout as its own decode — the wall that actually closed that fail-open, with `jq -e` only ever loudness beside it. If the semantic layer makes *absence-is-a-value* From 76d4393686b858417f5427a1f5fac6b5152c18b9 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 19 Aug 2026 03:14:59 +0000 Subject: [PATCH 12/23] 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) --- dag/extdeps/tools/jq.dag | 2 +- docs/plans/cli-invocation-emission-design.md | 18 ++++++++++++++++-- 2 files changed, 17 insertions(+), 3 deletions(-) diff --git a/dag/extdeps/tools/jq.dag b/dag/extdeps/tools/jq.dag index cf4cdb81ecf..bd579cd245e 100644 --- a/dag/extdeps/tools/jq.dag +++ b/dag/extdeps/tools/jq.dag @@ -4,7 +4,7 @@ import std.types { NonEmptyStr, String, Bool, List } import std.algebra { Cons, Empty } import v2.std.algebra { list_append, list_snoc_item } import v2.std.collection { Map, empty_map, map_insert } -import v2.std.compilers.cli_surface { CliArgumentSyntax, CliSurface, serialize_cli_arguments } +import v2.std.compilers.cli_surface { CliArgumentSyntax, CliSurface, cli_long_option_spelling, serialize_cli_arguments } import v2.std.compilers.lexing { LexRuleSet, LiteralPattern, ModeledLexRules, TokenRule } import v2.std.compilers.target_model { BoundToken, FixedToken } import v2.std.diagnostic { diff --git a/docs/plans/cli-invocation-emission-design.md b/docs/plans/cli-invocation-emission-design.md index 9f39bbbd060..00d84274651 100644 --- a/docs/plans/cli-invocation-emission-design.md +++ b/docs/plans/cli-invocation-emission-design.md @@ -809,7 +809,21 @@ General argument typechecking strengthens the boundary; it does not prove that p refusal has another cause this bisect did not separate, is unestablished — and a §5 line-stop is owed on it before anything else in this lane relies on the distinction. -9. **The spelling-seam extraction is right, but its obvious shape is forbidden — corrected +9. **A live Class B specimen, in this lane's own new code (found by review, 2026-08-19).** + `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 every Wave 1A assertion passed — because `cli_surface` was + already in the assembled closure via those three imports. That is exactly the 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 this — the bystander probe above refuses a *qualified* import of + a name a module does not export, whereas this is an *unimported bare reference* into a module + that is present for other reasons. Different mechanism, and only the second is silent. Fixed by + naming the symbol in the import list. **The general defect is untouched and not this lane's:** + nothing refuses the next such reference, and a green witness is not evidence that a module's + imports are complete. + +10. **The spelling-seam extraction is right, but its obvious shape is forbidden — corrected 2026-08-19.** The static-dependency finding stands: at execution grain the jq fold reaches no compiler machinery, but at dependency grain `cli_surface` imports `v2.std.compilers.target_model`, whose closure carries target-representation, host-runtime and node-query machinery. The @@ -848,7 +862,7 @@ General argument typechecking strengthens the boundary; it does not prove that p **Not performed.** `target_model` is load-bearing and carries the ruling above, so the move is its own increment under its own review, not a rider on this one. -10. **A downstream typed verdict may be the redundant lower rung, not a peer** (raised by +11. **A downstream typed verdict may be the redundant lower rung, not a peer** (raised by `eager-wren-138`, 2026-08-18). `gunbc.host_effect_realize` `bmcweb_token_extraction_verdict` refuses blank stdout as its own decode — the wall that actually closed that fail-open, with `jq -e` only ever loudness beside it. If the semantic layer makes *absence-is-a-value* From 96133bbeb37f1cab664ce17c311e5ada93bd0558 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 19 Aug 2026 03:43:40 +0000 Subject: [PATCH 13/23] 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) --- dag/extdeps/tools/jq.dag | 78 +++++++++++-- .../claim/cli_surface_boundary_probe_test.dag | 27 ++++- .../jq_invocation_lowering_witness_test.dag | 85 ++++++++++++++- src/v2/std/compilers/cli_surface.dag | 103 +++++++++++++++--- 4 files changed, 264 insertions(+), 29 deletions(-) diff --git a/dag/extdeps/tools/jq.dag b/dag/extdeps/tools/jq.dag index bd579cd245e..45bbfd2895d 100644 --- a/dag/extdeps/tools/jq.dag +++ b/dag/extdeps/tools/jq.dag @@ -224,9 +224,18 @@ type JqProcessPlan { stdin: String? } +// THE CAUSE IS TYPED, NOT PROSE. An earlier revision carried a NonEmptyStr reason that +// jq_lowering_refused_diagnostic never read, so both unlowered axes collapsed to one +// ^jq_lowering_refused identity and the two witnesses could only assert a generic Rejected -- +// authored payload, carried briefly, then erased. Each cause now projects a distinct diagnostic +// identity the witnesses assert, so the two refusals are distinguishable by a consumer. +type JqLoweringRefusal + = JqBindingLoweringUnwired + | JqFileInputLoweringUnwired + type JqLowering = JqLowered { plan: JqProcessPlan } - | JqLoweringRefused { reason: NonEmptyStr } + | JqLoweringRefused { cause: JqLoweringRefusal } // The lowering REFUSES the axes this wave has no live consumer for, rather than emitting a // plausible guess. Bindings land with ObjectMapperServiceAt (the --argjson vertical) and file @@ -236,15 +245,11 @@ type JqLowering fn jq_invocation_lower(invocation: JqInvocation) -> JqLowering { match invocation.bindings { Cons { head: _, tail: _ } => - JqLoweringRefused { - reason: "jq bindings are not lowered yet; the --arg/--argjson vertical lands with ObjectMapperServiceAt" - } + JqLoweringRefused { cause: JqBindingLoweringUnwired } Empty => match invocation.input { JqInputFile { path: _ } => - JqLoweringRefused { - reason: "jq file input is not lowered yet; the operand vertical lands with the remote population" - } + JqLoweringRefused { cause: JqFileInputLoweringUnwired } JqInputStdin { content: content } => JqLowered { plan: JqProcessPlan { @@ -285,11 +290,53 @@ fn jq_selected_option_argument(selection: JqCliSelection) -> List CliSurface { plan.surface } + +fn jq_admitted_plan_stdin(plan: JqAdmittedProcessPlan) -> String? { plan.stdin } + +fn jq_invocation_process_plan(invocation: JqInvocation) -> Outcome { + match jq_invocation_lower(invocation: invocation) { + JqLoweringRefused { cause: cause } => + outcome_rejected(jq_lowering_refused_diagnostic(cause: cause)) + JqLowered { plan: plan } => + bind_outcome( + o: serialize_cli_arguments( + arguments: plan.arguments, + lex: jq_cli_lex_rules(), + binding_spellings: plan.binding_spellings + ), + f: fn(surface) { + outcome_accepted(JqAdmittedProcessPlan { + tool: jq_cli_tool, + surface: surface, + stdin: plan.stdin + }) + } + ) + } +} + +// The argv-only projection, retained because the boundary witness asserts over it directly. fn jq_invocation_cli_arguments(invocation: JqInvocation) -> Outcome { match jq_invocation_lower(invocation: invocation) { - JqLoweringRefused { reason: reason } => - outcome_rejected(jq_lowering_refused_diagnostic(reason: reason)) + JqLoweringRefused { cause: cause } => + outcome_rejected(jq_lowering_refused_diagnostic(cause: cause)) JqLowered { plan: plan } => serialize_cli_arguments( arguments: plan.arguments, @@ -299,9 +346,16 @@ fn jq_invocation_cli_arguments(invocation: JqInvocation) -> Outcome } } -fn jq_lowering_refused_diagnostic(reason: NonEmptyStr) -> Diagnostic { +fn jq_lowering_refusal_identity(cause: JqLoweringRefusal) -> Symbol { + match cause { + JqBindingLoweringUnwired => ^jq_binding_lowering_unwired + JqFileInputLoweringUnwired => ^jq_file_input_lowering_unwired + } +} + +fn jq_lowering_refused_diagnostic(cause: JqLoweringRefusal) -> Diagnostic { Diagnostic { - reason: ^jq_lowering_refused, + reason: jq_lowering_refusal_identity(cause: cause), at: node_locus(node: Node { kind: TypeNode { connective: Atom { identity: ^jq_invocation_lowering } }, children: [], diff --git a/dag/test/claim/cli_surface_boundary_probe_test.dag b/dag/test/claim/cli_surface_boundary_probe_test.dag index d25d168ba76..54df28cf9ab 100644 --- a/dag/test/claim/cli_surface_boundary_probe_test.dag +++ b/dag/test/claim/cli_surface_boundary_probe_test.dag @@ -16,7 +16,8 @@ import v2.std.compilers.lexing { ModeledLexRules, TokenRule } -import v2.std.compilers.target_model { ConcreteSyntaxToken, FixedToken, bound_tokens_source_text, render_target_text } +import v2.std.compilers.target_model { BoundToken, ConcreteSyntaxToken, FixedToken, bound_tokens_source_text, render_target_text } +import v2.std.node { Symbol } import v2.std.diagnostic { Accepted, Rejected } // WAVE 0 (docs/plans/cli-invocation-emission-design.md). @@ -171,3 +172,27 @@ test fn keystone_flat_text_is_nonempty() -> Bool { Rejected { diagnostics: _ } => false } } + + +// A MISSING BINDING REFUSES. This is the perturbation control for the fail-open this fold used +// to inherit: target_model's bound-token lookup answers an absent map entry with the binding +// SYMBOL'S OWN NAME, so a generic serializer would have emitted the literal argument +// "probe_unbound_value" -- a plausible-looking argv the process would then have run. Defensible +// for compiler source text, where the symbol name is a legitimate rendering; fabricated +// plausible output for runtime CLI data (DESIGN section 5). +// +// The assertion is deliberately Rejected-vs-Accepted rather than a text comparison: if the +// fallback ever returns, this goes red because the fold ACCEPTS, and no assertion about the +// emitted text is needed to see it. +test fn a_bound_fragment_with_no_spelling_refuses() -> Bool { + match serialize_cli_arguments( + arguments: [CliArgumentSyntax { + fragments: [BoundToken { token_class: ^probe_value_class, binding: ^probe_unbound_value }] + }], + lex: probe_lex_rules(), + binding_spellings: empty_map() + ) { + Rejected { diagnostics: _ } => true + Accepted { value: _, diagnostics: _ } => false + } +} diff --git a/dag/test/claim/jq_invocation_lowering_witness_test.dag b/dag/test/claim/jq_invocation_lowering_witness_test.dag index 1b693299a1b..572e8325493 100644 --- a/dag/test/claim/jq_invocation_lowering_witness_test.dag +++ b/dag/test/claim/jq_invocation_lowering_witness_test.dag @@ -16,8 +16,18 @@ import extdeps.tools.jq { JqProgram, JqProgramExit, JqRawOutput, - jq_invocation_cli_arguments + JqBindingLoweringUnwired, + JqFileInputLoweringUnwired, + JqLowered, + JqLoweringRefused, + jq_admitted_plan_stdin, + jq_admitted_plan_surface, + jq_invocation_cli_arguments, + jq_invocation_lower, + jq_invocation_process_plan, + jq_lowering_refusal_identity } +import v2.std.optional { Absent, Present } // WAVE 1A. The semantic invocation SensorIntegerValue will make, lowered to argv. // docs/plans/cli-invocation-emission-design.md @@ -126,3 +136,76 @@ test fn unlowered_file_input_refuses() -> Bool { Accepted { value: _, diagnostics: _ } => false } } + + +// STDIN MUST SURVIVE, not merely stay out of argv. +// +// stdin_content_is_absent_from_argv above is a NEGATIVE control, and a negative control is +// satisfied just as well by the content being lost entirely -- which is exactly what the public +// projection used to do. These two assertions are the positive half: the content reaches the +// process plan, and it reaches it WITHOUT also appearing in the argument vector. Neither one +// alone distinguishes correct routing from total loss. +test fn stdin_survives_lowering_into_the_process_plan() -> Bool { + match jq_invocation_process_plan(invocation: sensor_invocation()) { + Rejected { diagnostics: _ } => false + Accepted { value: plan, diagnostics: _ } => + match jq_admitted_plan_stdin(plan: plan) { + Absent => false + Present { value: carried } => carried == sensor_stdin + } + } +} + +test fn stdin_reaches_the_plan_without_entering_the_argument_vector() -> Bool { + match jq_invocation_process_plan(invocation: sensor_invocation()) { + Rejected { diagnostics: _ } => false + Accepted { value: plan, diagnostics: _ } => + fold_list( + xs: cli_surface_arguments(surface: jq_admitted_plan_surface(plan: plan)), + empty: true, + cons: fn(acc, arg) { acc && (cli_argument_text(argument: arg) != sensor_stdin) } + ) + } +} + +// THE TWO UNLOWERED AXES ARE DISTINGUISHABLE. The refusal witnesses above assert only a generic +// Rejected, which one shared diagnostic identity would satisfy -- and did, while the cause was +// prose the diagnostic never read. +test fn the_two_unlowered_causes_carry_distinct_identities() -> Bool { + jq_lowering_refusal_identity(cause: JqBindingLoweringUnwired) + != jq_lowering_refusal_identity(cause: JqFileInputLoweringUnwired) +} + +test fn unlowered_bindings_refuse_with_the_binding_cause() -> Bool { + match jq_invocation_lower(invocation: JqInvocation { + program: JqProgram { source: sensor_program }, + bindings: [JqJsonBinding { name: JqBindingName { name: "index" }, value: "3" }], + input: JqInputStdin { content: "{}" }, + output_encoding: JqRawOutput, + exit_policy: JqProgramExit, + }) { + JqLowered { plan: _ } => false + JqLoweringRefused { cause: cause } => + match cause { + JqBindingLoweringUnwired => true + JqFileInputLoweringUnwired => false + } + } +} + +test fn unlowered_file_input_refuses_with_the_file_cause() -> Bool { + match jq_invocation_lower(invocation: JqInvocation { + program: JqProgram { source: sensor_program }, + bindings: Empty, + input: JqInputFile { path: "/tmp/x.json" }, + output_encoding: JqRawOutput, + exit_policy: JqProgramExit, + }) { + JqLowered { plan: _ } => false + JqLoweringRefused { cause: cause } => + match cause { + JqBindingLoweringUnwired => false + JqFileInputLoweringUnwired => true + } + } +} diff --git a/src/v2/std/compilers/cli_surface.dag b/src/v2/std/compilers/cli_surface.dag index bcbfa2351e7..cce3ae4dcba 100644 --- a/src/v2/std/compilers/cli_surface.dag +++ b/src/v2/std/compilers/cli_surface.dag @@ -5,31 +5,39 @@ import std.types { NonEmptyStr, String } import v2.std.algebra { fold_list, list_snoc_item } import v2.std.collection { List, Map } import v2.std.compilers.target_model { + BoundToken, ConcreteSyntaxToken, + FixedToken, LexRules, - bound_tokens_source_text, - render_target_text + lex_rules_literal_for_class } +import v2.std.collection { map_get } import v2.std.diagnostic { Accepted, + Diagnostic, + ExternalContractUnknown, None, Outcome, ShortCircuit, StageDiagnosticPolicy, + Unavailable, append_outcome_value, Rejected, bind_outcome, - outcome_accepted + node_locus, + outcome_accepted, + outcome_rejected } -import v2.std.node { Symbol } +import v2.std.node { Atom, Node, Symbol, SyntheticOccurrence, TypeNode } +import v2.std.optional { Absent, Present } // WHY THIS EXISTS. // -// CliArgumentSyntax preserves the GROUPING a tool's CLI projection selected. bound_tokens_source_text -// is reused only INSIDE one argument, where concatenation is correct (["--color","=","never"] is the -// single argument --color=never). The outer fold preserves boundaries BETWEEN arguments, which is -// the information an argv vector carries and source text cannot. +// CliArgumentSyntax preserves the GROUPING a tool's CLI projection selected. Fragments concatenate +// only INSIDE one argument, where concatenation is correct (["--color","=","never"] is the single +// argument --color=never). The outer fold preserves boundaries BETWEEN arguments, which is the +// information an argv vector carries and source text cannot. // // This module consumes ConcreteSyntaxToken. It does NOT consume compiler translate output and is // independent of TargetModel as a semantic authority -- an earlier revision of this comment @@ -118,20 +126,85 @@ fn cli_argument_text(argument: CliArgument) -> String { // concatenates WITHIN one argument. The outer fold preserves the argument boundary BETWEEN them. // Both directions are then reachable from the same fragments, which is what makes the witness // discriminating rather than self-fulfilling. +// A MISSING BINDING REFUSES HERE. It does not fall back to the binding's own symbol name. +// +// This fold used to route through target_model bound_tokens_source_text, whose bound-token +// lookup answers an absent entry with the symbol's interned spelling instead of a refusal. That +// is defensible for compiler source text, where the symbol name IS a legitimate rendering. It is +// fail-open for runtime CLI data: a missing jq_program_text binding would have emitted the +// literal argument "jq_program_text" -- a plausible-looking argv the process would then run. +// DESIGN section 5: no fabricated plausible output. Absence is a typed, located refusal. +// +// So the two carriers keep their own folds, which is also what the carrier ruling requires. The +// shared authority is TOKEN-GRAIN SPELLING (lex_rules_literal_for_class, and the map lookup +// below), not sequence composition: emitted source composes through TargetText via text_atom and +// target_text_seq, an argv argument composes into a CliArgument here, and no already-composed +// String is ever lifted into either carrier. +fn required_bound_spelling( + binding_spellings: Map, + binding: Symbol +) -> Outcome { + match map_get(binding_spellings, binding) { + Rejected { diagnostics: ds } => Rejected { diagnostics: ds } + Accepted { value: found, diagnostics: pending } => + match found { + Present { value: spelling } => Accepted { value: spelling, diagnostics: pending } + Absent => outcome_rejected(cli_binding_spelling_missing_diagnostic(binding: binding)) + } + } +} + +fn cli_binding_spelling_missing_diagnostic(binding: Symbol) -> Diagnostic { + Diagnostic { + reason: ^cli_binding_spelling_missing, + at: node_locus(node: Node { + kind: TypeNode { connective: Atom { identity: binding } }, + children: [], + occurrence_id: SyntheticOccurrence + }), + correction: Unavailable { reason: ExternalContractUnknown } + } +} + +fn cli_fragment_spelling( + fragment: ConcreteSyntaxToken, + lex: LexRules, + binding_spellings: Map +) -> Outcome { + match fragment { + FixedToken { token_class: tc } => + lex_rules_literal_for_class(rules: lex, token_class: tc) + BoundToken { token_class: _, binding: b } => + required_bound_spelling(binding_spellings: binding_spellings, binding: b) + } +} + fn cli_argument_from_fragments( fragments: List, lex: LexRules, binding_spellings: Map ) -> Outcome { bind_outcome( - o: bound_tokens_source_text( - tokens: fragments, - lex: lex, - binding_spellings: binding_spellings + o: fold_list( + xs: fragments, + empty: outcome_accepted(""), + cons: fn(acc, fragment) { + bind_outcome( + o: acc, + f: fn(partial) { + bind_outcome( + o: cli_fragment_spelling( + fragment: fragment, + lex: lex, + binding_spellings: binding_spellings + ), + f: fn(spelling) { outcome_accepted(concat(partial, spelling)) } + ) + } + ) + } ), - f: fn(text) { - outcome_accepted(CliArgument { text: render_target_text(t: text) }) - } + f: fn(text) { outcome_accepted(CliArgument { text: text }) } ) } From d6db90cab1ac1be0df481da64c08c046badb83c2 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 19 Aug 2026 03:50:57 +0000 Subject: [PATCH 14/23] 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) --- dag/extdeps/tools/jq.dag | 9 ++++++--- docs/plans/cli-invocation-emission-design.md | 2 +- src/v2/std/compilers/cli_surface.dag | 2 +- 3 files changed, 8 insertions(+), 5 deletions(-) diff --git a/dag/extdeps/tools/jq.dag b/dag/extdeps/tools/jq.dag index 45bbfd2895d..364eb12cade 100644 --- a/dag/extdeps/tools/jq.dag +++ b/dag/extdeps/tools/jq.dag @@ -56,9 +56,12 @@ service jq.Json { // WAVE 1A: the semantic invocation, and the two-level derivation from it to argv. // docs/plans/cli-invocation-emission-design.md // -// The caller describes WHAT IT WANTS OF JQ. It never names a flag. Nothing below is reachable -// from a domain module except through jq_invocation_cli_arguments, and that function emits the -// spellings rather than accepting them. +// The caller describes WHAT IT WANTS OF JQ. It never names a flag. A domain module reaches this +// module through jq_invocation_process_plan -- the complete result, carrying tool, argv and stdin +// -- and those functions emit the spellings rather than accepting them. jq_invocation_cli_arguments +// remains beside it as the argv-only projection the boundary witness asserts over; it is NOT the +// handler's entry point, because a handler that took it would have to reopen the JqInvocation to +// recover stdin, giving the process projection two authorities. // A jq program is opaque HERE on purpose. Modeling jq's expression language is a separate // vertical from modeling its invocation structure, and conflating them would make this wave diff --git a/docs/plans/cli-invocation-emission-design.md b/docs/plans/cli-invocation-emission-design.md index 00d84274651..7e19cb5ac46 100644 --- a/docs/plans/cli-invocation-emission-design.md +++ b/docs/plans/cli-invocation-emission-design.md @@ -676,7 +676,7 @@ exists to keep peripheral. So the wall belongs on the **input**, not on the seri serializer total over it. That is **not built**, and the design of its mint is genuinely open — whatever seals it faces the same recursion one level up. Until it lands, provenance sits at *mitigatable*, and the practical containment is that the only public jq entry point is -`jq_invocation_cli_arguments`, which is a convention, not a wall. +`jq_invocation_process_plan`, which is a convention, not a wall. **Application-argument typechecking is not the terminal trigger.** The `04_infer` gap is real — `explicit_return_conformance_note` records that conformance is judged only by the diff --git a/src/v2/std/compilers/cli_surface.dag b/src/v2/std/compilers/cli_surface.dag index cce3ae4dcba..43375d50d55 100644 --- a/src/v2/std/compilers/cli_surface.dag +++ b/src/v2/std/compilers/cli_surface.dag @@ -77,7 +77,7 @@ import v2.std.optional { Absent, Present } // // NOT BUILT, and its mint's design is genuinely open, because whatever seals AdmittedCliInvocation // faces the same recursion one level up. Until it lands, provenance sits at MITIGATABLE and the -// only containment is that jq's single public entry point is jq_invocation_cli_arguments -- a +// only containment is that jq's complete public entry point is jq_invocation_process_plan -- a // convention, not a wall. DISSOLVES WITH: that sealed input carrier, not with "the first // production consumer", which was the previous trigger and would have fired without closing this. From 17560cbf38651b721faf444c69b85ee4059c6954 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 19 Aug 2026 04:07:05 +0000 Subject: [PATCH 15/23] 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) --- dag/extdeps/tools/jq.dag | 2 ++ docs/plans/cli-invocation-emission-design.md | 18 ++++++++++++++++++ 2 files changed, 20 insertions(+) diff --git a/dag/extdeps/tools/jq.dag b/dag/extdeps/tools/jq.dag index 364eb12cade..c5f6683313b 100644 --- a/dag/extdeps/tools/jq.dag +++ b/dag/extdeps/tools/jq.dag @@ -12,7 +12,9 @@ import v2.std.diagnostic { ExternalContractUnknown, Outcome, Unavailable, + bind_outcome, node_locus, + outcome_accepted, outcome_rejected } import v2.std.node { Atom, Node, Symbol, SyntheticOccurrence, TypeNode } diff --git a/docs/plans/cli-invocation-emission-design.md b/docs/plans/cli-invocation-emission-design.md index 7e19cb5ac46..f5a2d51745f 100644 --- a/docs/plans/cli-invocation-emission-design.md +++ b/docs/plans/cli-invocation-emission-design.md @@ -823,6 +823,24 @@ General argument typechecking strengthens the boundary; it does not prove that p nothing refuses the next such reference, and a green witness is not evidence that a module's imports are complete. +9-bis. **The Class B specimen RECURRED, in code written after it was documented (review 53669, + 2026-08-19).** `jq_invocation_process_plan` used `bind_outcome` and `outcome_accepted` with + neither in the module's `v2.std.diagnostic` import list. Same mechanism as the + `cli_long_option_spelling` case one commit earlier, same lane, introduced by the same author + who had just written that entry. + + **Two things this settles.** First, the mitigation has to run *after every addition*: the + unimported-reference sweep had been run and was clean, then a new function was added and the + sweep was not re-run. A one-time audit does not close a class whose defect is invisible. + Second — and this corrects the review that found it — the stated consequence, "as written this + file will not resolve", is **false**, and its falsity is the whole point. 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 have been refuted by running it, and might then have + dismissed a real finding. The correct statement is: the reference is unimported, it binds by + pool membership, and **nothing in the tree will tell you** — not the resolver, not CI, not a + green witness. + 10. **The spelling-seam extraction is right, but its obvious shape is forbidden — corrected 2026-08-19.** The static-dependency finding stands: at execution grain the jq fold reaches no compiler machinery, but at dependency grain `cli_surface` imports `v2.std.compilers.target_model`, From eef165b82cf1cde6c705111ae699b97368b1a046 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 19 Aug 2026 04:30:45 +0000 Subject: [PATCH 16/23] 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) --- dag/extdeps/tools/jq.dag | 35 ---------------------------- src/v2/std/compilers/cli_surface.dag | 15 ++++++------ 2 files changed, 8 insertions(+), 42 deletions(-) diff --git a/dag/extdeps/tools/jq.dag b/dag/extdeps/tools/jq.dag index c5f6683313b..cb6c97c2184 100644 --- a/dag/extdeps/tools/jq.dag +++ b/dag/extdeps/tools/jq.dag @@ -113,8 +113,6 @@ type JqInvocation { type JqCliOption = JqCliOptionRawOutput | JqCliOptionExitStatus - | JqCliOptionArgJson - | JqCliOptionArg // ABSENCE IS A DECLARED ROW, NOT A MISSING ONE. An earlier revision returned Optional // and answered Absent for JqProgramExit -- which makes "this policy deliberately requires no @@ -141,13 +139,6 @@ fn jq_selection_for_exit_policy(policy: JqExitPolicy) -> JqCliSelection { } } -fn jq_option_for_binding(binding: JqBinding) -> JqCliOption { - match binding { - JqJsonBinding { name: _, value: _ } => JqCliOptionArgJson - JqTextBinding { name: _, value: _ } => JqCliOptionArg - } -} - // LEVEL TWO: an option identity selects its CITED SPELLING. jqlang.org/manual/ is the authority // for every string below; the long form is canonical because it is self-describing at a call // site, and the short alias is recorded as a fact about jq rather than used. @@ -155,8 +146,6 @@ fn jq_option_token_class(option: JqCliOption) -> Symbol { match option { JqCliOptionRawOutput => ^jq_opt_raw_output JqCliOptionExitStatus => ^jq_opt_exit_status - JqCliOptionArgJson => ^jq_opt_argjson - JqCliOptionArg => ^jq_opt_arg } } @@ -169,8 +158,6 @@ fn jq_option_long_name(option: JqCliOption) -> NonEmptyStr { match option { JqCliOptionRawOutput => "raw-output" JqCliOptionExitStatus => "exit-status" - JqCliOptionArgJson => "argjson" - JqCliOptionArg => "arg" } } @@ -178,20 +165,6 @@ fn jq_option_canonical_spelling(option: JqCliOption) -> NonEmptyStr { cli_long_option_spelling(name: jq_option_long_name(option: option)) } -// The short aliases jq also accepts. Declared so the corpus records what jq's surface IS, and -// deliberately not consulted by the lowering: a caller cannot ask for -r over --raw-output, -// because which form is canonical is jq's decision and not the caller's. -// The short names jq also accepts, again bare: the grammar renders one hyphen. argjson and arg -// have no short form, which is a fact about jq rather than an omission here. -fn jq_option_short_name(option: JqCliOption) -> Optional { - match option { - JqCliOptionRawOutput => Present { value: "r" } - JqCliOptionExitStatus => Present { value: "e" } - JqCliOptionArgJson => Absent - JqCliOptionArg => Absent - } -} - // The lex table jq itself authors: one row per option identity, spelling from the cited rows // above. A caller cannot supply this -- which is half of closing the Wave 0 mint hole, because // arbitrary content can no longer be spelled through a caller-authored table on the jq path. @@ -207,14 +180,6 @@ fn jq_cli_lex_rules() -> ModeledLexRules { token_class: jq_option_token_class(option: JqCliOptionExitStatus), pattern: LiteralPattern { text: jq_option_canonical_spelling(option: JqCliOptionExitStatus) } }, - TokenRule { - token_class: jq_option_token_class(option: JqCliOptionArgJson), - pattern: LiteralPattern { text: jq_option_canonical_spelling(option: JqCliOptionArgJson) } - }, - TokenRule { - token_class: jq_option_token_class(option: JqCliOptionArg), - pattern: LiteralPattern { text: jq_option_canonical_spelling(option: JqCliOptionArg) } - }, ] } } diff --git a/src/v2/std/compilers/cli_surface.dag b/src/v2/std/compilers/cli_surface.dag index 43375d50d55..eb153b51db6 100644 --- a/src/v2/std/compilers/cli_surface.dag +++ b/src/v2/std/compilers/cli_surface.dag @@ -87,17 +87,18 @@ import v2.std.optional { Absent, Present } type CliArgumentSyntax { fragments: List } // THE SHARED RENDERING RULE, owned here and not by any tool row. A tool declares WHICH names -// exist and which form is canonical; how a long name becomes two hyphens plus the name, or a -// short name one hyphen plus the character, is one rule every POSIX-conventional tool shares -// (IEEE Std 1003.1-2024 XBD 12). A tool row storing "--raw-output" would re-spell that rule per -// tool and could silently disagree with it. +// exist and which form is canonical; how a long name becomes two hyphens plus the name is one +// rule every POSIX-conventional tool shares (IEEE Std 1003.1-2024 XBD 12). A tool row storing +// "--raw-output" would re-spell that rule per tool and could silently disagree with it. +// +// Only the LONG form is modeled, because only the long form has a consumer. The short-form +// renderer was authored beside it and deleted unused: 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. +// It returns with the first tool row that selects a short spelling. fn cli_long_option_spelling(name: NonEmptyStr) -> NonEmptyStr { concat("--", name) } -fn cli_short_option_spelling(name: NonEmptyStr) -> NonEmptyStr { - concat("-", name) -} type CliArgument sole_constructor { text: String } From 012ef2327d73a65025d6bb6d2b4a67c95f49fb31 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 19 Aug 2026 05:48:13 +0000 Subject: [PATCH 17/23] BLOCKER, proven by execution: the argv transport silently joins computed argument lists A List 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) --- docs/plans/cli-invocation-emission-design.md | 50 ++++++++++++++++++++ 1 file changed, 50 insertions(+) diff --git a/docs/plans/cli-invocation-emission-design.md b/docs/plans/cli-invocation-emission-design.md index f5a2d51745f..f0f6d2c71ed 100644 --- a/docs/plans/cli-invocation-emission-design.md +++ b/docs/plans/cli-invocation-emission-design.md @@ -823,6 +823,56 @@ General argument typechecking strengthens the boundary; it does not prove that p nothing refuses the next such reference, and a green witness is not evidence that a module's imports are complete. +9-ter. **BLOCKER, PROVEN BY EXECUTION: the argv transport silently destroys argument boundaries + for computed lists (2026-08-19).** A `List` built by folding is CONCATENATED into a + single argv word; the identical list written as a literal is SPLICED. Same declared type, same + elements, same handler, two different processes. + + **Receipt, through the production handler `jq.Process.RunWithStdin`:** + + ``` + 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. + `Value::Variant` tries `value_as_host_string` FIRST, which walks a free monoid and concatenates + it into one String, pushing a single 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 succeeds and wins. `gunbc.WitnessBin.Run` escapes this only because + its `args` is authored as a literal at each call site. + + **Independently attacked:** an outside reviewer attempted to refute this and failed — the + source matches the reading, and the collapse occurs BEFORE `Command::args`, which rules out a + downstream shell or SSH join. + + **Why neither obvious repair is correct.** Reordering the arms would splice this case but + SHRED a modeled `String`, because a String is itself a monoid here (`value_as_host_string` + reconstructs one from code points): both readings succeed on a monoid of `Str`s, 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 that `target_model` `target_text_carrier_scaffold_note` + names as the trigger for every type-based construction guarantee at a call boundary. + Hand-authoring a literal argv in the handler defeats row-derived lowering and leaves the next + caller silently joined, which is the workaround shape §5 treats as a line-stop. + + **Rung:** this is a §5 fail-open — it fabricates one plausible argument instead of refusing — + and it is the LANE'S OWN DEFECT CLASS one layer below the lane: Wave 0's witness asserts that + fragments concatenate within an argument and never across, and the transport violates exactly + that. It is also a live specimen of the model↔realization fork DESIGN tracks as an open thread. + + **Consequence for this lane:** the cutover is BLOCKED at the execution seam. The semantic + spine is built and resolving; no consumer can move until this is decided, because every + migrated call site computes its argv rather than authoring it literally — which is precisely + what the migration asks callers to start doing. + 9-bis. **The Class B specimen RECURRED, in code written after it was documented (review 53669, 2026-08-19).** `jq_invocation_process_plan` used `bind_outcome` and `outcome_accepted` with neither in the module's `v2.std.diagnostic` import list. Same mechanism as the From ce7694aa4774fb6214487ee68ec1d431854095fd Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 19 Aug 2026 06:03:02 +0000 Subject: [PATCH 18/23] 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 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 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 and the explicit carrier -- two authorities with the unsafe one still reachable. Co-Authored-By: Claude Opus 5 (1M context) --- docs/plans/cli-invocation-emission-design.md | 40 +++++++++++++++++++- 1 file changed, 39 insertions(+), 1 deletion(-) diff --git a/docs/plans/cli-invocation-emission-design.md b/docs/plans/cli-invocation-emission-design.md index f0f6d2c71ed..7275bb413ef 100644 --- a/docs/plans/cli-invocation-emission-design.md +++ b/docs/plans/cli-invocation-emission-design.md @@ -868,7 +868,45 @@ General argument typechecking strengthens the boundary; it does not prove that p fragments concatenate within an argument and never across, and the transport violates exactly that. It is also a live specimen of the model↔realization fork DESIGN tracks as an open thread. - **Consequence for this lane:** the cutover is BLOCKED at the execution seam. The semantic + **CORRECTION (same day, adversarial review): "blocked on application-argument typechecking" + was WRONG, and too strong.** The diagnosis above survived independent verification — the + reviewer traced `build_service_param_env` (which clones call arguments with no conformance + check), `dispatch_shell`, and `Command::new(&argv[0]).args(&argv[1..])`, confirming the vector + is already malformed before `Command` sees it, so no later join is available as an alternative + explanation. The refusal to reorder the branches was also upheld. But the conclusion was not: + **a correct construction is available now.** + + The counter-evidence is in-tree: `OperationInputValue = InputText | InputTextList` already + carries tagged list intent, and its realization explicitly converts that tag into a native + `Value::List` (`free_monoid_to_vec` then `list_value`), so the later flattening splices. Tagged + intent → native list is therefore proven possible *without* global argument typechecking. + + And the deeper correction: even a fully typechecked system would still not answer the question + the transport must ask. `List` 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**, and the missing fact should be modeled rather than + inferred from runtime encoding. Application-argument typechecking remains independently + valuable and is neither necessary nor sufficient here. + + **The construction:** one explicit nominal carrier — `ShellArgvExpansion { surface: CliSurface }`, + sealed — with an interpreter branch placed BEFORE the generic string/list heuristic that requires + the nominal `CliSurface`, iterates its arguments, and pushes exactly one host word per + `CliArgument`, concatenating that argument's fragments into that one word. It carries `CliSurface` + rather than `List` precisely 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 used only on one admitted argument's text, where concatenation IS correct. That is Wave 0's + theorem enforced at the host edge. + + **Explicitly not to be landed** (each rejected for a stated reason): reversing the two `Variant` + branches (damages modeled strings); `map(identity)` to coerce a native list, rebuilding the + emitted argv as a literal, or join-then-shell-split (runtime-representation workarounds, and the + last reintroduces shell parsing); routing jq through `OperationInputValue` permanently (that + carrier belongs to declaration-owned operation materialization); or accepting BOTH a raw + `List` and the explicit carrier (two authorities, with future callers free to pick the + unsafe one). The raw-list handler signature is REPLACED, not retained for compatibility. + + **Consequence for this lane:** the cutover is blocked at the execution seam *until that carrier + lands*, which is a build, not a decision. The semantic spine is built and resolving; no consumer can move until this is decided, because every migrated call site computes its argv rather than authoring it literally — which is precisely what the migration asks callers to start doing. From 273fcb796081715caf6d9b7566aec384de1f32a3 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 19 Aug 2026 08:28:29 +0000 Subject: [PATCH 19/23] 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 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 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) --- dag/extdeps/bmc/openbmc_fan_control.dag | 115 ++++++---- dag/extdeps/tools/jq.dag | 180 +++++++++++++-- .../bmc_typed_operations_witness_test.dag | 27 ++- .../jq_invocation_lowering_witness_test.dag | 133 ++++++++++- .../process_argv_expansion_receipt_test.dag | 73 ++++++ docs/plans/cli-invocation-emission-design.md | 214 +++++++++++++++++- src/v1/stage0/src/v1_interpreter.rs | 130 +++++++++++ src/v2/std/compilers/cli_surface.dag | 51 +++++ 8 files changed, 842 insertions(+), 81 deletions(-) create mode 100644 dag/test/manual/process_argv_expansion_receipt_test.dag diff --git a/dag/extdeps/bmc/openbmc_fan_control.dag b/dag/extdeps/bmc/openbmc_fan_control.dag index 7ad6866a95e..6dcdf33bd9e 100644 --- a/dag/extdeps/bmc/openbmc_fan_control.dag +++ b/dag/extdeps/bmc/openbmc_fan_control.dag @@ -1,6 +1,7 @@ module extdeps.bmc.openbmc_fan_control -import std.algebra { trim } +import std.algebra { Empty, trim } +import v2.std.diagnostic { Accepted, Rejected } import extdeps.external_authority { ExternalAuthority } import extdeps.uri { Https, Uri } @@ -18,7 +19,21 @@ import extdeps.languages.json.emit { json_string, serialize_json, } -import extdeps.tools.jq { jq_authority } +import extdeps.tools.jq { + JqInputStdin, + JqInvocation, + JqProgram, + JqProgramExit, + JqRawOutput, + jq_authority, + JqOutcome, + JqOutputAbsent, + JqOutputPresent, + JqExecutionRefused, + jq_classify_observation, + jq_execute_admitted_plan, + jq_invocation_process_plan +} import extdeps.systemd.systemctl { systemctl_authority } import extdeps.bmc.openbmc_operation { OpenBmcCopyFilePreservingMetadata, @@ -792,23 +807,6 @@ service openbmc.JsonProjection { } } - operation SensorIntegerValue { - input { content: String } - output { - value: String from "stdout" - success: Bool from "exit_success" - stderr: String from "stderr" - } - readonly - transport shell { - argv: ["jq", "-r", "if (.data | type) == \"number\" then (.data | round) else empty end"] - stdin: content - } - exit { - 0 => Unit - nonzero => String "sensor integer projection failed" - } - } } fn openbmc_read_file( @@ -881,23 +879,56 @@ type OpenBmcSensorValueResult | OpenBmcSensorValueAbsent | OpenBmcSensorValueRefused { reason: String } +// exit_code, not `success: Bool`. Two fields for one fact is a second representation: success is +// exactly exit_code == 0, derived here where the three states are decided rather than carried +// alongside them. +// THE PROGRAM IS THE DOMAIN'S, THE FLAGS ARE JQ'S. This module states what it wants extracted; +// it never spells -r, --raw-output or an argv position. `else empty end` is deliberate and +// load-bearing: a non-numeric reading emits NOTHING and exits zero, which the decoder below reads +// as OpenBmcSensorValueAbsent -- a real third state beside Refused and Observed. That is why this +// path must NOT carry jq's --exit-status: it would collapse Absent into Refused on a live sensor. +data openbmc_sensor_integer_program: String = "if (.data | type) == \"number\" then (.data | round) else empty end" + +// One place builds the sensor projection invocation, so both call sites cannot drift apart. +fn openbmc_sensor_integer_projection(content: String) -> OpenBmcSensorValueResult { + match jq_invocation_process_plan(invocation: JqInvocation { + program: JqProgram { source: openbmc_sensor_integer_program }, + bindings: Empty, + input: JqInputStdin { content: content }, + output_encoding: JqRawOutput, + exit_policy: JqProgramExit, + }) { + Rejected { diagnostics: _ } => + OpenBmcSensorValueRefused { reason: "sensor value projection could not be lowered to a jq invocation" } + Accepted { value: plan, diagnostics: _ } => { + let observed = jq_execute_admitted_plan(plan: plan) + openbmc_sensor_integer_projection_result( + outcome: jq_classify_observation(plan: plan, observation: observed), + ) + } + } +} + +// THIS DECODER NO LONGER READS AN EXIT CODE, and that is the point of the arm it matches instead. +// It previously took exit_code/stdout/stderr and mapped every nonzero exit to a refusal -- correct +// under JqProgramExit, silently wrong under any other exit policy, and nothing connected the two. +// jq_classify_observation now owns that reading, against the policy carried on the plan, so this +// function decides only what OpenBMC alone can decide: whether a present projection is an integer. fn openbmc_sensor_integer_projection_result( - success: Bool, - value: String, - stderr: String, + outcome: JqOutcome, ) -> OpenBmcSensorValueResult { - if !success { - OpenBmcSensorValueRefused { reason: stderr } - } else if trim(value) == "" { - OpenBmcSensorValueAbsent - } else { - match parse_int(s: trim(value)) { - Absent => - OpenBmcSensorValueRefused { - reason: "sensor value projection is not an integer", - } - Present { value: parsed } => OpenBmcSensorValueObserved { value: parsed } - } + match outcome { + JqExecutionRefused { exit_code: _, stderr: stderr } => + OpenBmcSensorValueRefused { reason: stderr } + JqOutputAbsent => OpenBmcSensorValueAbsent + JqOutputPresent { text: text } => + match parse_int(s: trim(text)) { + Absent => + OpenBmcSensorValueRefused { + reason: "sensor value projection is not an integer", + } + Present { value: parsed } => OpenBmcSensorValueObserved { value: parsed } + } } } @@ -1025,14 +1056,7 @@ fn openbmc_sensor_value( if !remote.success { OpenBmcSensorValueRefused { reason: remote.stderr } } else { - let extracted = openbmc.JsonProjection.SensorIntegerValue( - content: remote.stdout, - ) - openbmc_sensor_integer_projection_result( - success: extracted.success, - value: extracted.value, - stderr: extracted.stderr, - ) + openbmc_sensor_integer_projection(content: remote.stdout) } } @@ -1059,12 +1083,7 @@ fn openbmc_sensor_threshold_result( if !remote.success { OpenBmcSensorValueRefused { reason: remote.stderr } } else { - let extracted = openbmc.JsonProjection.SensorIntegerValue(content: remote.stdout) - openbmc_sensor_integer_projection_result( - success: extracted.success, - value: extracted.value, - stderr: extracted.stderr, - ) + openbmc_sensor_integer_projection(content: remote.stdout) } } diff --git a/dag/extdeps/tools/jq.dag b/dag/extdeps/tools/jq.dag index cb6c97c2184..1a4940191a3 100644 --- a/dag/extdeps/tools/jq.dag +++ b/dag/extdeps/tools/jq.dag @@ -1,10 +1,10 @@ module extdeps.tools.jq -import std.types { NonEmptyStr, String, Bool, List } -import std.algebra { Cons, Empty } +import std.types { NonEmptyStr, String, Bool, Int, List } +import std.algebra { Cons, Empty, trim } import v2.std.algebra { list_append, list_snoc_item } import v2.std.collection { Map, empty_map, map_insert } -import v2.std.compilers.cli_surface { CliArgumentSyntax, CliSurface, cli_long_option_spelling, serialize_cli_arguments } +import v2.std.compilers.cli_surface { CliArgumentSyntax, CliSurface, cli_long_option_spelling, process_argv_expansion, serialize_cli_arguments } import v2.std.compilers.lexing { LexRuleSet, LiteralPattern, ModeledLexRules, TokenRule } import v2.std.compilers.target_model { BoundToken, FixedToken } import v2.std.diagnostic { @@ -41,15 +41,58 @@ data jq_cli_tool: CliTool = CliTool { installable_via: [SourceApt { package: package_jq }], } -service jq.Json { - operation ExtractRaw { - input { filter: NonEmptyStr, path: NonEmptyStr } - output { value: String from "stdout", success: Bool from "exit_success" } +// THE EXECUTION HANDLER, and the argv here is NOT a second authority on jq's flags. +// +// jq.Json.ExtractRaw stood here: input { filter, path }, argv ["jq","-r","{filter}","{path}"]. +// That was a SEMANTIC argv -- it decided that raw output is what a caller wants and spelled the +// flag itself -- and it had zero consumers tree-wide. Deleted rather than migrated: the semantic +// layer above answers the question it was answering. +// +// What replaces it spells nothing. `arguments` arrives already lowered from a sealed plan, and +// the only literal is the executable -- the same shape as gunbc.WitnessBin.Run's +// ["env","-C","{workdir}","{bin_path}", args]: a process-spawn form at the REALIZATION layer. +// +// THE ARGUMENTS ARRIVE AS ProcessArgvExpansion, NOT List, and that is load-bearing rather +// than decorative. A computed List does NOT reach the process as separate words: a folded +// list is concatenated into one argv word while an identical literal splices (receipt: literal +// ["--raw-output","."] -> exit 0; the same two elements folded -> exit 2, `jq: Unknown option +// --raw-output.`). The transport was guessing the expansion role from runtime encoding. The +// carrier states it nominally, and the seed realizes it fail-closed. The raw-list signature is +// REPLACED rather than kept beside the carrier: two accepted forms would leave the unsafe one +// reachable by every future caller. +service jq.Process { + operation RunWithStdin { + input { arguments: ProcessArgvExpansion, stdin_payload: String } + output { + exit_code: Int from "exit_code" + stdout: String from "stdout" + stderr: String from "stderr" + } + readonly + transport shell { + argv: ["jq", arguments] + stdin: stdin_payload + } + exit { + 0 => Unit + nonzero => Unit + } + } + + operation RunWithoutStdin { + input { arguments: ProcessArgvExpansion } + output { + exit_code: Int from "exit_code" + stdout: String from "stdout" + stderr: String from "stderr" + } readonly - transport shell { argv: ["jq", "-r", "{filter}", "{path}"] } + transport shell { + argv: ["jq", arguments] + } exit { 0 => Unit - nonzero => String "jq extract failed" + nonzero => Unit } } } @@ -59,7 +102,7 @@ service jq.Json { // docs/plans/cli-invocation-emission-design.md // // The caller describes WHAT IT WANTS OF JQ. It never names a flag. A domain module reaches this -// module through jq_invocation_process_plan -- the complete result, carrying tool, argv and stdin +// module through jq_invocation_process_plan -- the complete result, carrying argv and process input // -- and those functions emit the spellings rather than accepting them. jq_invocation_cli_arguments // remains beside it as the argv-only projection the boundary witness asserts over; it is NOT the // handler's entry point, because a handler that took it would have to reopen the JqInvocation to @@ -191,7 +234,7 @@ fn jq_cli_lex_rules() -> ModeledLexRules { type JqProcessPlan { arguments: List binding_spellings: Map - stdin: String? + process_input: JqProcessInput } // THE CAUSE IS TYPED, NOT PROSE. An earlier revision carried a NonEmptyStr reason that @@ -229,7 +272,7 @@ fn jq_invocation_lower(invocation: JqInvocation) -> JqLowering { key: ^jq_program_text, value: invocation.program.source as String ), - stdin: Present { value: content } + process_input: JqProcessStdin { content: content } } } } @@ -270,15 +313,86 @@ fn jq_selected_option_argument(selection: JqCliSelection) -> List, which conflates them -- the same state-space +// collapse JqCliSelection exists to prevent one layer up, reintroduced at the process boundary. +type JqProcessInput + = JqProcessStdin { content: String } + | JqProcessNoStdin + +// exit_code and NOT a success Bool beside it: two fields for one fact is a second +// representation, since success is exactly exit_code == 0, derived where it is decided. +type JqProcessObservation { + exit_code: Int + stdout: String + stderr: String +} + +// No `tool` field. A jq-owned handler already fixes the executable, so carrying CliTool here +// would restate the carrier's own type. It returns when a genuinely generic executor consumes it +// to RESOLVE an executable -- that consumer does not exist yet. +// THE PLAN CARRIES ITS OWN OBSERVATION CONTRACT, and it must, because how jq's exit code is to be +// READ is decided by the exit policy that produced the argv. A plan carrying only a surface and an +// input is decodable only by a consumer that separately remembers which policy it asked for -- and +// a consumer that remembers is a consumer that can forget. The live specimen: the sensor decoder +// mapped every nonzero exit to a refusal, which is correct under JqProgramExit and WRONG under +// JqLastResultExit, where exit 1 means the last output was false-or-null (a legitimate value) and +// exit 4 means no valid result (absence). Editing the policy in the invocation would have left the +// decoder silently answering the old contract -- DESIGN section 5's tell exactly: the declaration +// changes while the realization goes on lying. type JqAdmittedProcessPlan sole_constructor { - tool: CliTool surface: CliSurface - stdin: String? + process_input: JqProcessInput + exit_policy: JqExitPolicy +} + +// The three states a jq run can be in, as the DOMAIN needs them. Presence, absence and refusal are +// separate arms because they are separate facts with different remedies -- collapsing absence into +// refusal is the state-space conflation that would report a non-numeric sensor reading as a broken +// BMC. +type JqOutcome + = JqOutputPresent { text: String } + | JqOutputAbsent + | JqExecutionRefused { exit_code: Int, stderr: String } + +// The one authority that reads an exit code, and it reads it AGAINST the policy that asked for it. +// +// Under JqProgramExit jq exits 0 whenever the program ran, including when it emitted nothing, so +// absence is observable only as empty output and any nonzero exit is a genuine failure. +// +// Under JqLastResultExit the same codes mean different things, per jq's documented contract: 1 is a +// false-or-null LAST OUTPUT -- a real value, carried in stdout, and NOT a failure -- and 4 is "no +// valid result was ever produced", which is absence. 2 (usage or system error) and 3 (program +// compile error) remain refusals under both policies. A single "nonzero means broken" rule would +// mis-decode three of those four codes. +fn jq_classify_observation(plan: JqAdmittedProcessPlan, observation: JqProcessObservation) -> JqOutcome { + match plan.exit_policy { + JqProgramExit => + if observation.exit_code != 0 { + JqExecutionRefused { exit_code: observation.exit_code, stderr: observation.stderr } + } else if trim(observation.stdout) == "" { + JqOutputAbsent + } else { + JqOutputPresent { text: observation.stdout } + } + JqLastResultExit => + if observation.exit_code == 4 { + JqOutputAbsent + } else if observation.exit_code == 0 || observation.exit_code == 1 { + if trim(observation.stdout) == "" { + JqOutputAbsent + } else { + JqOutputPresent { text: observation.stdout } + } + } else { + JqExecutionRefused { exit_code: observation.exit_code, stderr: observation.stderr } + } + } } fn jq_admitted_plan_surface(plan: JqAdmittedProcessPlan) -> CliSurface { plan.surface } -fn jq_admitted_plan_stdin(plan: JqAdmittedProcessPlan) -> String? { plan.stdin } +fn jq_admitted_plan_input(plan: JqAdmittedProcessPlan) -> JqProcessInput { plan.process_input } fn jq_invocation_process_plan(invocation: JqInvocation) -> Outcome { match jq_invocation_lower(invocation: invocation) { @@ -293,9 +407,9 @@ fn jq_invocation_process_plan(invocation: JqInvocation) -> Outcome Diagnostic { correction: Unavailable { reason: ExternalContractUnknown } } } + + +// EXECUTION. The one function a domain module calls to actually run jq. +// +// It takes the SEALED plan, so the arguments reaching the process are the ones the row-driven +// lowering produced -- a caller cannot hand it an argv it authored. The handler operation is +// selected by matching the process-input arm rather than by an if, so a third input form would be +// a non-exhaustive match here rather than a silently wrong execution. +// +// Nonzero exit is DATA, not failure: a consumer's decoder maps nonzero to its own refusal state, +// exit-zero with empty stdout to absence, and exit-zero with content to an observation. A handler +// that treated nonzero as an error would collapse that three-state decode into two. +fn jq_execute_admitted_plan(plan: JqAdmittedProcessPlan) -> JqProcessObservation { + let arguments = process_argv_expansion(surface: plan.surface) + match plan.process_input { + JqProcessStdin { content: payload } => { + let ran = jq.Process.RunWithStdin(arguments: arguments, stdin_payload: payload) + JqProcessObservation { exit_code: ran.exit_code, stdout: ran.stdout, stderr: ran.stderr } + } + JqProcessNoStdin => { + let ran = jq.Process.RunWithoutStdin(arguments: arguments) + JqProcessObservation { exit_code: ran.exit_code, stdout: ran.stdout, stderr: ran.stderr } + } + } +} + +// The four-case receipt's entry point (test/manual/process_argv_expansion_receipt_test.dag). It +// exists so the receipt asserts through the SAME handler production uses, rather than a +// look-alike declared in the witness -- a witness-local service would prove nothing about this one. +fn jq_argv_expansion_probe(expansion: ProcessArgvExpansion, payload: String) -> Int { + jq.Process.RunWithStdin(arguments: expansion, stdin_payload: payload).exit_code +} diff --git a/dag/test/claim/bmc_typed_operations_witness_test.dag b/dag/test/claim/bmc_typed_operations_witness_test.dag index 826c83acb40..104916408e9 100644 --- a/dag/test/claim/bmc_typed_operations_witness_test.dag +++ b/dag/test/claim/bmc_typed_operations_witness_test.dag @@ -14,6 +14,7 @@ import extdeps.bmc.openbmc_fan_control { OpenBmcPathRefused, OpenBmcSensorServicesObserved, OpenBmcSensorValueAbsent, + OpenBmcSensorValueObserved, OpenBmcSensorValueRefused, OpenBmcTachAtOrAboveThreshold, OpenBmcTachBelowThreshold, @@ -33,6 +34,7 @@ import extdeps.bmc.openbmc_fan_control { openbmc_service_active_result, openbmc_zone_failsafe_result, } +import extdeps.tools.jq { JqExecutionRefused, JqOutputAbsent, JqOutputPresent } import extdeps.ssh.password_session { PasswordSshExecResult } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } import std.measure { byte_size_count, rpm, rpm_count } @@ -83,11 +85,15 @@ test fn failed_threshold_transport_cannot_become_threshold_unstated() -> Bool { } } +// These two took `success: Bool` and an untyped `value`/`stderr` triple until the sensor path moved +// onto the jq invocation layer. They now state the SAME two requirements against the typed jq +// outcome: a refusal must not decay into absence, and an empty successful projection must not decay +// into a refusal. The requirement is unchanged; only what carries it is, which is why these are +// re-enrolled rather than retired (DESIGN section 3 -- evidence for a surviving claim survives the +// representation that used to hold it). test fn failed_sensor_projection_cannot_become_absent() -> Bool { match openbmc_sensor_integer_projection_result( - success: false, - value: "", - stderr: "malformed OpenBMC JSON", + outcome: JqExecutionRefused { exit_code: 2, stderr: "malformed OpenBMC JSON" }, ) { OpenBmcSensorValueRefused { reason } => reason == "malformed OpenBMC JSON" _ => false @@ -96,15 +102,24 @@ test fn failed_sensor_projection_cannot_become_absent() -> Bool { test fn successful_empty_sensor_projection_is_absent() -> Bool { match openbmc_sensor_integer_projection_result( - success: true, - value: "", - stderr: "", + outcome: JqOutputAbsent, ) { OpenBmcSensorValueAbsent => true _ => false } } +// The third state, which the old triple could not express at all: a PRESENT projection carrying a +// number is an observation. Added with the migration because the outcome type made it stateable. +test fn present_numeric_sensor_projection_is_observed() -> Bool { + match openbmc_sensor_integer_projection_result( + outcome: JqOutputPresent { text: "42" }, + ) { + OpenBmcSensorValueObserved { value } => value == 42 + _ => false + } +} + test fn tach_below_controller_threshold_is_not_healthy() -> Bool { match openbmc_tach_health_from_floor( sensor: "FAN4", diff --git a/dag/test/claim/jq_invocation_lowering_witness_test.dag b/dag/test/claim/jq_invocation_lowering_witness_test.dag index 572e8325493..3db0f065fa7 100644 --- a/dag/test/claim/jq_invocation_lowering_witness_test.dag +++ b/dag/test/claim/jq_invocation_lowering_witness_test.dag @@ -20,16 +20,28 @@ import extdeps.tools.jq { JqFileInputLoweringUnwired, JqLowered, JqLoweringRefused, - jq_admitted_plan_stdin, + JqOutcome, + JqExitPolicy, + JqOutputAbsent, + JqOutputPresent, + JqExecutionRefused, + JqProcessObservation, + jq_classify_observation, + jq_invocation_process_plan, + jq_admitted_plan_input, + JqProcessStdin, + JqProcessNoStdin, jq_admitted_plan_surface, jq_invocation_cli_arguments, jq_invocation_lower, jq_invocation_process_plan, jq_lowering_refusal_identity } -import v2.std.optional { Absent, Present } -// WAVE 1A. The semantic invocation SensorIntegerValue will make, lowered to argv. +// WAVE 1B, LANDED. The semantic invocation the OpenBMC sensor projection makes, lowered to argv. +// Not "will make": openbmc.JsonProjection.SensorIntegerValue is DELETED and +// extdeps.bmc.openbmc_fan_control openbmc_sensor_integer_projection is the live consumer of this +// lowering. (The note calls the ObjectMapper site Wave 1A; it is blocked on --argjson lowering.) // docs/plans/cli-invocation-emission-design.md // // The point of every assertion below is that the caller named no flag. It asked for raw output @@ -149,9 +161,9 @@ test fn stdin_survives_lowering_into_the_process_plan() -> Bool { match jq_invocation_process_plan(invocation: sensor_invocation()) { Rejected { diagnostics: _ } => false Accepted { value: plan, diagnostics: _ } => - match jq_admitted_plan_stdin(plan: plan) { - Absent => false - Present { value: carried } => carried == sensor_stdin + match jq_admitted_plan_input(plan: plan) { + JqProcessNoStdin => false + JqProcessStdin { content: carried } => carried == sensor_stdin } } } @@ -209,3 +221,112 @@ test fn unlowered_file_input_refuses_with_the_file_cause() -> Bool { } } } + + +// THE EXIT CODE MEANS DIFFERENT THINGS UNDER DIFFERENT POLICIES, and these four assertions are the +// discriminating evidence for that. Each holds ONE observation fixed and varies only the exit +// policy the plan carries. A decoder that read the exit code without the policy -- which is what +// the sensor path did before this landed -- cannot make all four true at once: it must answer +// Refused for exit 1 under both policies, and the second assertion below would go red. + +type ExpectedOutcome = ExpectPresent | ExpectAbsent | ExpectRefused + +fn outcome_matches(outcome: JqOutcome, expected: ExpectedOutcome) -> Bool { + match expected { + ExpectPresent => + match outcome { + JqOutputPresent { text: _ } => true + JqOutputAbsent => false + JqExecutionRefused { exit_code: _, stderr: _ } => false + } + ExpectAbsent => + match outcome { + JqOutputPresent { text: _ } => false + JqOutputAbsent => true + JqExecutionRefused { exit_code: _, stderr: _ } => false + } + ExpectRefused => + match outcome { + JqOutputPresent { text: _ } => false + JqOutputAbsent => false + JqExecutionRefused { exit_code: _, stderr: _ } => true + } + } +} + +// A plan that fails to lower answers FALSE rather than being replaced by a fabricated one: if the +// lowering ever refuses this invocation, these assertions must go red, not quietly test a stand-in. +fn classifies_as( + policy: JqExitPolicy, + observation: JqProcessObservation, + expected: ExpectedOutcome, +) -> Bool { + match jq_invocation_process_plan(invocation: JqInvocation { + program: JqProgram { source: sensor_program }, + bindings: Empty, + input: JqInputStdin { content: "{}" }, + output_encoding: JqRawOutput, + exit_policy: policy, + }) { + Rejected { diagnostics: _ } => false + Accepted { value: plan, diagnostics: _ } => + outcome_matches( + outcome: jq_classify_observation(plan: plan, observation: observation), + expected: expected, + ) + } +} + +// Exit 1 with output "false": a program-exit contract never produces it, so it is a failure. +test fn exit_one_is_a_refusal_under_program_exit() -> Bool { + classifies_as( + policy: JqProgramExit, + observation: JqProcessObservation { exit_code: 1, stdout: "false", stderr: "" }, + expected: ExpectRefused, + ) +} + +// The SAME observation under the last-result contract is a legitimate VALUE -- jq documents exit 1 +// as "the last output was false or null", and false is a value a filter may correctly produce. +// This is the assertion a policy-blind decoder cannot satisfy while satisfying the one above. +test fn exit_one_is_a_value_under_last_result_exit() -> Bool { + classifies_as( + policy: JqLastResultExit, + observation: JqProcessObservation { exit_code: 1, stdout: "false", stderr: "" }, + expected: ExpectPresent, + ) +} + +// Exit 4 is jq's "no valid result was ever produced" -- absence, not breakage. +test fn exit_four_is_absence_under_last_result_exit() -> Bool { + classifies_as( + policy: JqLastResultExit, + observation: JqProcessObservation { exit_code: 4, stdout: "", stderr: "" }, + expected: ExpectAbsent, + ) +} + +// Exit 2 is a usage or system error and refuses under BOTH policies -- the policy changes how +// SOME codes read, not whether jq can fail. +test fn exit_two_refuses_under_both_policies() -> Bool { + classifies_as( + policy: JqProgramExit, + observation: JqProcessObservation { exit_code: 2, stdout: "", stderr: "usage" }, + expected: ExpectRefused, + ) + && classifies_as( + policy: JqLastResultExit, + observation: JqProcessObservation { exit_code: 2, stdout: "", stderr: "usage" }, + expected: ExpectRefused, + ) +} + +// Empty output on a zero exit is absence, not an empty observation -- the sensor path's third +// state, which is the whole reason JqProgramExit must not carry --exit-status. +test fn empty_output_on_zero_exit_is_absence() -> Bool { + classifies_as( + policy: JqProgramExit, + observation: JqProcessObservation { exit_code: 0, stdout: " ", stderr: "" }, + expected: ExpectAbsent, + ) +} diff --git a/dag/test/manual/process_argv_expansion_receipt_test.dag b/dag/test/manual/process_argv_expansion_receipt_test.dag new file mode 100644 index 00000000000..7486c644ac4 --- /dev/null +++ b/dag/test/manual/process_argv_expansion_receipt_test.dag @@ -0,0 +1,73 @@ +module test.manual.process_argv_expansion_receipt + +import std.algebra { Cons, Empty } +import std.types { Bool, Int, String } +import v2.std.algebra { fold_list, list_snoc_item } +import v2.std.collection { List, empty_map } +import v2.std.compilers.cli_surface { + CliArgumentSyntax, + cli_argument_text, + cli_surface_arguments, + serialize_cli_arguments, + process_argv_expansion +} +import v2.std.compilers.lexing { LexRuleSet, LiteralPattern, ModeledLexRules, TokenRule } +import v2.std.compilers.target_model { ConcreteSyntaxToken, FixedToken } +import v2.std.diagnostic { Accepted, Rejected } +import extdeps.tools.jq { jq_argv_expansion_probe } + +// THE FOUR-CASE HOST RECEIPT for the argv splice law (design note, open question 9-ter). +// +// Each case alone is ambiguous; the set is the evidence: +// +// 1 native literal list -> splices (nothing existing was broken) +// 2 folded monoid, old path-> JOINS (the residue, recorded honestly, not closed) +// 3 modeled string -> stays ONE word (the arm did not shred strings -- the exact +// failure mode that ruled out reordering) +// 4 ProcessArgvExpansion -> splices (the claim itself) +// +// Cases 2 and 3 are why a branch reorder is not the repair: both are FreeMonoid at runtime, and +// the two readings both succeed, so no ordering recovers the erased intent. +// +// ONLY CASE 4 IS COMMITTED, DELIBERATELY, and this note is here so the gap does not read as an +// omission. Cases 1-3 were executed live against a real jq while the defect was being isolated -- +// their receipts are quoted in the design note (open question 9-ter) with the exact commands and +// exit codes. They are not enrolled here because each ASSERTS THE OLD BEHAVIOR: case 2 in +// particular pins the concatenating read as the expected outcome, and an enrolled test asserting a +// defect is how that defect acquires immortality (DESIGN section 4b -- evidence whose only subject +// is behavior the model rejects is retired with a receipt, not left standing). What survives +// enrolled is the claim the carrier makes: case 4 is red unless jq receives exactly two words. +// +// WET: this executes a real jq process. It is a manual receipt, not a floor witness, and its home +// under test/manual says so. + +fn probe_lex() -> ModeledLexRules { + ModeledLexRules { + root: LexRuleSet { + rules: [ + TokenRule { token_class: ^raw_output_opt, pattern: LiteralPattern { text: "--raw-output" } }, + TokenRule { token_class: ^dot_filter, pattern: LiteralPattern { text: "." } } + ] + } + } +} + +fn two_argument_surface() -> List { + [ + CliArgumentSyntax { fragments: [FixedToken { token_class: ^raw_output_opt }] }, + CliArgumentSyntax { fragments: [FixedToken { token_class: ^dot_filter }] } + ] +} + +// CASE 4 -- the carrier. jq exits 0 only if it received TWO argv words. +test fn case4_expansion_carrier_splices() -> Bool { + match serialize_cli_arguments( + arguments: two_argument_surface(), + lex: probe_lex(), + binding_spellings: empty_map() + ) { + Rejected { diagnostics: _ } => false + Accepted { value: surface, diagnostics: _ } => + jq_argv_expansion_probe(expansion: process_argv_expansion(surface: surface), payload: "1") == 0 + } +} diff --git a/docs/plans/cli-invocation-emission-design.md b/docs/plans/cli-invocation-emission-design.md index 7275bb413ef..6542eab5b4f 100644 --- a/docs/plans/cli-invocation-emission-design.md +++ b/docs/plans/cli-invocation-emission-design.md @@ -1,9 +1,22 @@ # CLI invocation emission — the tree is the authority, argv is emitted -**Status: DESIGN NOTE. No code lands from this note yet.** Design-note-first, per the +**Status: DESIGN NOTE PLUS ITS FIRST CUT.** An earlier revision of this line read "No code lands +from this note yet" and kept reading that way while the branch carried a carrier, a seed +realization, witnesses and one migrated production site. That is the stale-citation class in the +lane's own authority: a status sentence nobody edits because nobody is touching the paragraph +around it. What has landed is stated at each wave below; what has not is stated as not. Design-note-first, per the hollow-alias precedent. The first vertical is specified here; nothing is built until the note is accepted. +**Lane scope, narrowed (raised by the `shell → dag` session, accepted):** this note governs +**CLI-backed host effects only** — effects whose realization is a process invoked with an argument +vector. It is *not* a universal effect model, and the distinction is load-bearing rather than +pedantic: a Redfish/REST path reaches a modeled request and must reach **no** `JqInvocation`, no +`CliSurface`, no `ProcessArgvExpansion` and no shell target at all. Treating every host effect as a +CLI invocation would re-import at the effect layer exactly the mistake this lane is removing at the +argv layer — one realization mistaken for the interface. A negative falsifier witness proving a +REST path reaches none of these carriers is **owed by this lane and not yet built.** + **Lane:** supersedes the Lane B destination of `gunbc.plans.transport_argv_anemia_dissolution`. That plan's *diagnosis* stands — "the model is the request; the curl argv is one derived realization of it" — and its Lane A (HTTP → `transport rest`) is substantially right. Its @@ -544,6 +557,16 @@ byte-identical; argument boundaries observable *by execution*; direct/cast/unadm explicit refusal when no CLI serializer is wired. See §10 — this probe must execute, because it will not refuse at compile time. +**WAVE ORDER CORRECTED BY EXECUTION: 1B CUT FIRST, and the note was wrong, not the branch.** +Wave 1A was named the strongest first exemplar because it exercises the most axes at once — +including a typed JSON binding through `--argjson`. That is exactly why it cannot be first: the +binding lowering is **not built**, and `jq_invocation_lower` refuses it as +`JqBindingLoweringUnwired`. Choosing the richest site as the first cut selected the one site whose +lowering is unimplemented. `SensorIntegerValue` (Wave 1B) migrated first because its every axis is +wired: program operand, stdin input, raw output, and `JqProgramExit` selecting no exit-status +option. Its falsifier role is undiminished by going first — a counterexample does not require the +thing it falsifies to exist yet. 1A follows once `--argjson` lowers. + **Wave 1A — `ObjectMapperServiceAt`.** The strongest first exemplar, because its existing argv exercises nearly every load-bearing axis at once: `-e` truthiness exit, `-r` raw output, a typed JSON binding through `--argjson` (an option with **two** values), stdin input, a jq program @@ -601,8 +624,13 @@ separate proofs. 4. Emission to `List`. 5. Local resolution into `extdeps.posix` `Command`. 6. A process-input realization for jq stdin, separate from argv. -7. The SSH handler: emitted arguments → shell simple-command tree → shell text → RFC 4254 string. -8. One live jq population cut over, with its prior argv authoring site deleted. +7. One live jq population cut over, with its prior argv authoring site deleted. + +The SSH handler is **Wave 2 and is deliberately absent from this list.** An earlier revision +carried it here as item 7, directly contradicting "Do not make the first vertical solve SSH" two +paragraphs above and the recut in §7 — the same list could be cited to prove either scope. SSH adds +a second language target, RFC 4254 string loss and the `sshpass -d 0` collision; none of that is +needed to prove a local vertical. The carrier lands **with** its first live consumer, or in an immediately preceding stacked PR that already contains an executing consumer. A standalone carrier PR with no consumer would reproduce @@ -653,6 +681,9 @@ error. | omitting `--exit-status` from an accepted truthiness invocation | **structurally impossible within the new path** | exhaustive semantic→option selection; zero-or-many rows refuse; no mint on miss | | hand-authoring flags inside a migrated route | **structurally impossible after cutover** | handler takes a semantic invocation, emits internally, old argv site deleted | | reintroducing the exact old operation transport | mechanically preventable | structural deletion witness | +| a computed argument vector losing its argument boundaries at the host edge | **mitigatable only** | the `ProcessArgvExpansion` arm makes boundaries survive *on the carrier path* and refuses every malformed shape it is handed, but the guessing path it sits in front of is untouched for every value that is not this carrier — 21 operations still splice a declared `List` param. This is a repair at ONE seam, not a wall over the class | +| a domain module authoring jq program source | **mitigatable only** | §12 — `JqProgram` is public; nothing prevents it | +| decoding a jq exit code against the wrong contract | **structurally guaranteed on the new path** | §13 — the policy travels on the plan and `jq_classify_observation` is the only reader; a domain module has no exit code to misread | | writing another raw jq argv elsewhere | **still writable** | unrelated raw shell/process routes remain | | arbitrary raw argv corpus-wide | outside this vertical | later process/transport confinement | @@ -888,7 +919,7 @@ General argument typechecking strengthens the boundary; it does not prove that p inferred from runtime encoding. Application-argument typechecking remains independently valuable and is neither necessary nor sufficient here. - **The construction:** one explicit nominal carrier — `ShellArgvExpansion { surface: CliSurface }`, + **The construction:** one explicit nominal carrier — `ProcessArgvExpansion { surface: CliSurface }`, sealed — with an interpreter branch placed BEFORE the generic string/list heuristic that requires the nominal `CliSurface`, iterates its arguments, and pushes exactly one host word per `CliArgument`, concatenating that argument's fragments into that one word. It carries `CliSurface` @@ -1026,3 +1057,178 @@ Claims asserted during this design and refuted by measurement, kept so they are population, so a compile-only probe **false-greens**. - *"The smallest complete vertical includes SSH."* **False** — SSH adds a second language target and three independent failure modes; the unit is local-only. + +--- + +## 12. `JqProgram` is public, and the domain still authors jq source + +Raised by the `shell → dag` session against the `SensorIntegerValue` cut. The objection: after the +migration, `extdeps.bmc.openbmc_fan_control` no longer authors argv — but it *does* author + +``` +data openbmc_sensor_integer_program: String = + "if (.data | type) == \"number\" then (.data | round) else empty end" +``` + +so the workflow moved from authoring shell to authoring jq. `JqProgram { source: NonEmptyStr }` +is a public constructor, so every domain module may do the same. + +**The objection is right about the residue and should not be argued down.** What the cut +established is narrower than "the domain stopped authoring foreign syntax": it stopped authoring +*argv*. Measured at the cut, OpenBMC no longer names `-r`, `--raw-output`, an option spelling, an +argument position, argv[0], or the stdin routing — all of those are now derived from jq's cited +rows, and that is the property the two-level derivation buys. The jq *program* is untouched by it. + +**The proposed remedy — keep `OpenBmcSensorIntegerProjection { content }` public and have the +handler privately select a sealed program identity — is refused as stated, on §2.** It does not +decompose the program; it relocates the same string behind an indirection and adds a registry to +maintain. Ask where the text lives afterwards. If the handler is OpenBMC's, the jq source is still +in the OpenBMC layer and only a wrapper was added. If the handler is jq's, then `extdeps.tools.jq` +knows what a BMC sensor reading is — a layer inversion, jq depending upward on its consumer's +domain. Neither position is better than the row that exists, and the second is worse. A sealed +identity would buy something only if the identity were *derived*, which is the real answer: + +**The terminal shape is that the program is not authored at all.** `.data`, "is it a number", +"round it", "otherwise nothing" are a modeled JSON projection — a path, a type guard, a rounding +policy, and an absence arm — of which a jq program is ONE realization, exactly as an argv vector +is one serialization of a `CliSurface`. Under that model the domain declares the projection, jq's +module derives the program text from it the way it already derives option spellings, and a second +realization (a native JSON fold with no process at all) becomes possible for free. That is the same +move the lane already made one layer out, applied one layer in — and it is what stops this work +generalizing into a thousand bespoke jq programs where it found a thousand bespoke argv lines. + +**Rung, honestly.** Domain-authored jq source is **mitigatable**: nothing prevents it, and the only +things standing between it and an arbitrary computed program are that the row is `data` rather than +a function — so it cannot vary per call — and review. Not a wall, and it should not be reported as +one. + +**Dissolution trigger:** a modeled JSON projection carrier with jq as a derived realization. Until +it lands, `JqProgram` stays public and this section is the reason, not an oversight. This is +deliberately NOT scoped into the current cut: modeling a JSON projection algebra is its own +vertical, and bundling it would repeat the Wave 1A mistake of selecting the richest thing first. + + +--- + +## 13. The observation contract travels with the plan + +Raised as "`JqAdmittedProcessPlan` cannot be decoded" by the `shell → dag` session. Verified +against the code and **worse than raised** — it was not a missing convenience, it was a live latent +defect in the cut itself. + +The sensor decoder read `exit_code`, `stdout` and `stderr` directly and mapped every nonzero exit to +a refusal. That is correct under `JqProgramExit` and silently wrong under `JqLastResultExit`, where +jq documents exit **1** as "the last output was false or null" — a legitimate *value* — and exit +**4** as "no valid result was ever produced" — *absence*. Nothing connected the decoder to the +policy that produced the argv, so changing `exit_policy` in the invocation would have left the +decoder confidently answering the previous contract. That is §5's own tell: the declaration is +edited while the realization goes on lying, and the model's own witnesses stay green because they +never varied the policy. + +**Repair.** `JqAdmittedProcessPlan` carries `exit_policy`, so the plan is self-describing. One +authority, `jq_classify_observation`, reads an exit code *against* the policy that asked for it and +returns `JqOutputPresent | JqOutputAbsent | JqExecutionRefused`. The domain matches those arms and +decides only what OpenBMC alone can decide — whether a present projection parses as an integer. No +domain module reads a jq exit code any more. + +**Discriminating evidence, and why it discriminates.** Five assertions hold one observation fixed +and vary only the policy: + +``` +exit 1, stdout "false" under JqProgramExit -> Refused +exit 1, stdout "false" under JqLastResultExit -> Present <- the policy-blind decoder fails here +exit 4, stdout "" under JqLastResultExit -> Absent +exit 2, stderr "usage" under BOTH -> Refused +exit 0, stdout " " under JqProgramExit -> Absent +``` + +The second row is the discriminator: a decoder reading the exit code without the policy must answer +`Refused` for exit 1 under both policies, so it cannot make rows one and two true at once. The +fourth row is the control that keeps the law from overfitting — the policy changes how *some* codes +read, not whether jq can fail. + +**This also closes the point `eager-wren-138` reached from the other direction.** That session +proposed sweeping `-e` across jq sites as hardening; the counter was that `-e` reports on the *last +output*, so it converts legitimate `false`/`null` into failure. Both facts are now modeled rather +than argued: selecting `JqLastResultExit` changes the *decode*, not just the flag, and absence +remains a state distinct from refusal on both arms. + +--- + +## 14. Verification scoped to the consumers I already knew about + +Recorded because it is the third instance of one failure mode in this lane's own work, and the +first two were caught by other people. + +Changing `openbmc_sensor_integer_projection_result`'s signature broke two enrolled witnesses +(`failed_sensor_projection_cannot_become_absent`, `successful_empty_sensor_projection_is_absent`) +that call the decoder directly. I did not find them, because I had selected the witnesses to run by +asking which files import `openbmc_fan_control.dag` **and then hand-picking three of them** — the +verification denominator was a list I wrote, not a list the tree produced. The break surfaced only +when the resolve failed on an unrelated run. + +The same shape produced the two earlier defects: an unimported-reference sweep run *before* the +last addition rather than after it, and a grep whose zero result was accepted without a control +that must hit. In each case the mechanism was sound and the **denominator** was authored. + +**The rule adopted for the rest of the lane:** verification enumerates test functions from the +FILE, never from memory — + +``` +grep "^test fn" | sed 's/test fn \([a-z_0-9]*\).*/\1/' +``` + +— and every function in every witness file touching a changed signature runs, not a chosen subset. +This is the same principle §5 states for oracles, applied to coverage: a population I author is not +an observation of the population that exists. + +**What the break itself demonstrates, and it is the argument for the cut.** Both witnesses were +re-enrolled unchanged in *requirement* — a refusal must not decay into absence, an empty successful +projection must not decay into a refusal — while their *carrier* moved from a `success: Bool` triple +to the typed jq outcome. The migration also made a third requirement stateable that the old triple +could not express: that a present numeric projection is an observation. That is a replacement +migration behaving correctly (§3): deletion surfaced the load, the load was dispositioned as +re-enrolled evidence rather than restored by reflex, and the new representation was strictly more +expressive than the one it replaced. + +--- + +## 15. Wave 1B cutover receipt + +Executed on BuildBuddy against the branch tree. Counts are from enumerating `^test fn` in each +file, not from a chosen subset (§14). + +``` +extdeps.bmc.openbmc_fan_control SensorIntegerValue operation DELETED + consumers rewired 2 (openbmc_sensor_value, openbmc_sensor_threshold_result) + both now route through openbmc_sensor_integer_projection (one shared fn, not two call sites) + argv authored by the domain after cutover 0 -- no -r, no --raw-output, no argv position, no argv[0] + residual foreign syntax authored 1 jq program row (S12, mitigatable, trigger recorded) + +test/claim/bmc_typed_operations_witness 29 / 29 pass + of which migrated onto the typed jq outcome 2 (requirement unchanged, carrier replaced) + of which newly stateable and added 1 (present numeric projection is an observation) +test/claim/jq_invocation_lowering_witness 9 / 9 pass (lowering) + 5 / 5 pass (S13 exit-policy classification) +test/claim/bmc_fan_converge_witness duty_curve pass +test/manual/process_argv_expansion_receipt case 4 pass -- real jq, exit 0 reachable only + with two argv words, through the production handler +``` + +**What this receipt does NOT establish**, stated because the table above reads stronger than the +lane's actual position: + +- The argv splice defect is repaired at **one seam**, not closed as a class. 21 operations still + splice a declared `List` parameter through the guessing path. +- The other three `openbmc.JsonProjection` operations are unmigrated, and two of them + (`ObjectMapperServiceCount`, `ObjectMapperServiceAt`) need `--argjson` lowering, which is unbuilt. +- No negative falsifier exists yet proving a REST path reaches none of these carriers. +- The wet receipt run reports `[expectation-frontier] 1 site(s), 1 dispatch(es) undeclared: + jq.Process.RunWithStdin=1`. That is the new handler's dispatch not being declared to the + expectation registry. It is left standing rather than silenced because it is exactly the shape §5 + asks for — typed, located, counted, and visible — but it IS an open item, and a reader should not + infer from a `PASS` line that nothing else was reported. +- The 5 classification assertions and the wet receipt executed in separate runs from the 29+9; a + single run of all 43 exceeded the 45-minute remote timeout, because every `gunbc run` pays a + whole-corpus typecheck. That is a cost-shape observation about the harness, not evidence about + the code, and it is recorded rather than left as an unexplained split. diff --git a/src/v1/stage0/src/v1_interpreter.rs b/src/v1/stage0/src/v1_interpreter.rs index 871bc87acc6..9559788d28e 100644 --- a/src/v1/stage0/src/v1_interpreter.rs +++ b/src/v1/stage0/src/v1_interpreter.rs @@ -7201,8 +7201,138 @@ pub(crate) struct ShellResult { pub(crate) stderr: bounded_shell_host_drain::CapturedStreamEvidence, } +/// Expand a `ProcessArgvExpansion` into argv words, one word per `CliArgument`. +/// +/// SEED REALIZATION OF A MODELED LAW, not a seed-only special case. The authority is +/// `v2.std.compilers.cli_surface` `ProcessArgvExpansion`, which states: +/// +/// across the surface's arguments -- ITERATE, never concatenate +/// within one argument's fragments -- CONCATENATE into exactly one word +/// +/// WHY AN EXPLICIT ARM RATHER THAN A BETTER GUESS. `push_shell_argv_tokens` below decides +/// "one word or many?" from the RUNTIME ENCODING of a generic value, and that distinction is +/// genuinely erased: a `FreeMonoid` is equally a modeled String assembled from fragments +/// and a modeled list whose members are strings. `value_as_host_string` and `free_monoid_to_vec` +/// BOTH succeed on it, so no branch order recovers the intent -- reordering them would splice +/// lists correctly and shred modeled strings. The missing fact is the transport ROLE, and this +/// carrier supplies it nominally. +/// +/// FAIL-CLOSED. Every shape mismatch is a typed error. There is deliberately no arm that falls +/// through to the guessing path: a carrier that says "expand this" and then silently produced one +/// joined word would be the exact defect it exists to remove (DESIGN section 5). +fn push_process_argv_expansion( + argv: &mut Vec, + fields: &[(Symbol, Value)], +) -> InterpResult<()> { + let surface = fields + .iter() + .find(|(name, _)| resolve_sym(*name).rsplit('.').next() == Some("surface")) + .map(|(_, v)| v) + .ok_or_else(|| InterpError::TypeError { + msg: "ProcessArgvExpansion carries no `surface` field; argv expansion refuses rather \ + than emitting a guessed word" + .to_string(), + })?; + let arguments = match surface { + Value::Record { type_name, fields } => { + if resolve_sym(*type_name).rsplit('.').next() != Some("CliSurface") { + return Err(InterpError::TypeError { + msg: format!( + "ProcessArgvExpansion.surface must be a CliSurface record, found `{}`", + resolve_sym(*type_name) + ), + }); + } + fields + .iter() + .find(|(name, _)| resolve_sym(*name).rsplit('.').next() == Some("arguments")) + .map(|(_, v)| v.clone()) + .ok_or_else(|| InterpError::TypeError { + msg: "CliSurface carries no `arguments` field".to_string(), + })? + } + other => { + return Err(InterpError::TypeError { + msg: format!( + "ProcessArgvExpansion.surface must be a CliSurface record, found `{other}`" + ), + }) + } + }; + let items = match &arguments { + Value::List(items) => items.iter().cloned().collect::>(), + variant @ Value::Variant { .. } => { + free_monoid_to_vec(variant).ok_or_else(|| InterpError::TypeError { + msg: "CliSurface.arguments is neither a native list nor a list-shaped value" + .to_string(), + })? + } + other => { + return Err(InterpError::TypeError { + msg: format!("CliSurface.arguments must be a list, found `{other}`"), + }) + } + }; + for item in items { + let text = match &item { + Value::Record { type_name, fields } => { + if resolve_sym(*type_name).rsplit('.').next() != Some("CliArgument") { + return Err(InterpError::TypeError { + msg: format!( + "CliSurface.arguments member must be a CliArgument record, found `{}`", + resolve_sym(*type_name) + ), + }); + } + fields + .iter() + .find(|(name, _)| resolve_sym(*name).rsplit('.').next() == Some("text")) + .map(|(_, v)| v.clone()) + .ok_or_else(|| InterpError::TypeError { + msg: "CliArgument carries no `text` field".to_string(), + })? + } + other => { + return Err(InterpError::TypeError { + msg: format!( + "CliSurface.arguments member must be a CliArgument, found `{other}`" + ), + }) + } + }; + // Concatenation is CORRECT here and only here: this is one argument's own text. + let word = value_as_host_string(&text).ok_or_else(|| InterpError::TypeError { + msg: "CliArgument.text is not a host string".to_string(), + })?; + // An EMPTY argument is a real argument and is pushed unchanged: `jq ""` passes one empty + // word, and silently dropping it would change arity -- the same boundary destruction the + // concatenating path performs, in the other direction. + // + // An embedded NUL REFUSES rather than reaching the exec boundary. A C argument vector is + // NUL-terminated, so no argument can contain one; std::process would reject it at spawn + // with an errno-shaped error naming neither the argument nor the surface. Refusing here + // yields a located diagnostic instead (DESIGN section 5: refuse, never widen or fabricate). + if word.contains('\0') { + return Err(InterpError::TypeError { + msg: format!( + "CliArgument.text contains an embedded NUL at argv position {}; a process \ + argument vector is NUL-terminated and cannot carry one", + argv.len() + ), + }); + } + argv.push(word); + } + Ok(()) +} + fn push_shell_argv_tokens(argv: &mut Vec, val: Value) -> InterpResult<()> { match &val { + Value::Record { type_name, fields } + if resolve_sym(*type_name).rsplit('.').next() == Some("ProcessArgvExpansion") => + { + push_process_argv_expansion(argv, fields) + } Value::Str(s) => { argv.push(s.to_string()); Ok(()) diff --git a/src/v2/std/compilers/cli_surface.dag b/src/v2/std/compilers/cli_surface.dag index eb153b51db6..f06fa062dd7 100644 --- a/src/v2/std/compilers/cli_surface.dag +++ b/src/v2/std/compilers/cli_surface.dag @@ -112,6 +112,57 @@ fn cli_argument_text(argument: CliArgument) -> String { argument.text } +// THE TRANSPORT ROLE, stated rather than inferred from runtime encoding. +// +// WHY THIS EXISTS, and it is not a wrapper for tidiness. A `List` reaching an argv +// position does not say what the collection MEANS there: several argv words, one JSON argument, +// one comma-joined option value, or repeated option/value groups are all realizable from the +// same declared type. That is a TRANSPORT ROLE, not a data type, and the seed currently GUESSES +// it from how the value happens to be represented at runtime. +// +// THE MEASURED DEFECT THAT FORCED THIS (design note, open question 9-ter; receipts there): +// a folded List is CONCATENATED into one argv word while an identical literal list is +// SPLICED -- same declared type, two different processes. `jq --raw-output--exit-status.missing` +// reached a real process from a correctly-lowered three-argument vector. +// +// THE LAW THIS CARRIER STATES, which is Wave 0's theorem at the host edge: +// +// across the surface's arguments -- ITERATE, never concatenate +// within one argument's fragments -- CONCATENATE into exactly one word +// +// IT CARRIES CliSurface, NOT List, and that is the whole strength of it. CliSurface is +// sole_constructor and its members are nominal CliArgument records, so a realization can check +// both nominal layers and a modeled string cannot impersonate a list of arguments. A wrapper +// around a raw list would state the role while leaving the payload dynamically ambiguous -- the +// same guess one level up. +// +// V2 CORRESPONDENCE (this is why the seed may realize it): v2.std.operation_argv already models +// the same distinction for DECLARATION-owned materialization -- OperationInputValue is +// InputText | InputTextList, and binding a token list into a string position is the typed +// refusal TokenListInStringPosition. That module's own note records that expression-valued argv +// elements instead execute through the interpreter's dispatch_shell path, "which evaluates argv +// expressions in the full evaluator and is untouched here". This carrier is that same law for +// the computed-surface case, so the seed arm realizes a modeled fact rather than inventing a +// seed-only special case. +// NOT "SHELL", AND THE NAME WAS CORRECTED BEFORE IT SPREAD. This branch's own investigation of +// the seed established that the realization is Command::new(&argv[0]).args(&argv[1..]) -- a direct +// process exec with no shell in the path, no word splitting, no glob expansion and no quoting +// layer to be correct about. Naming the carrier for `transport shell` would name it after the +// surface DSL keyword that happens to declare these operations today, which is DESIGN section 3 +// nicknaming: a second name for a concept -- process argument-vector construction -- that the +// host boundary already names. A shell-hosted transport, if one is ever modeled, is a DIFFERENT +// realization binding, not the thing this carrier describes. + +type ProcessArgvExpansion sole_constructor { surface: CliSurface } + +fn process_argv_expansion(surface: CliSurface) -> ProcessArgvExpansion { + ProcessArgvExpansion { surface: surface } +} + +fn process_argv_expansion_surface(expansion: ProcessArgvExpansion) -> CliSurface { + expansion.surface +} + // THE FOLD IS NESTED, AND THE NESTING IS THE WHOLE POINT. // // An earlier revision folded a FLAT List one-token-one-argument, and its From b3b4f06ffa42595f7624901a2f99d33f44a5131f Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 19 Aug 2026 08:51:10 +0000 Subject: [PATCH 20/23] 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) --- .../jq_invocation_lowering_witness_test.dag | 13 +++++++--- docs/plans/cli-invocation-emission-design.md | 24 +++++++++++++++++++ 2 files changed, 34 insertions(+), 3 deletions(-) diff --git a/dag/test/claim/jq_invocation_lowering_witness_test.dag b/dag/test/claim/jq_invocation_lowering_witness_test.dag index 3db0f065fa7..4b8dcfab4c0 100644 --- a/dag/test/claim/jq_invocation_lowering_witness_test.dag +++ b/dag/test/claim/jq_invocation_lowering_witness_test.dag @@ -229,9 +229,16 @@ test fn unlowered_file_input_refuses_with_the_file_cause() -> Bool { // the sensor path did before this landed -- cannot make all four true at once: it must answer // Refused for exit 1 under both policies, and the second assertion below would go red. -type ExpectedOutcome = ExpectPresent | ExpectAbsent | ExpectRefused +// NAMED JqOutcomeExpectation, NOT ExpectedOutcome, and the first attempt taught the reason the +// hard way. gunbc.output_policy already declares a type under that name +// (ExpectSuccess | ExpectFailure | OutcomeIsData) -- the load-bearing carrier the interpreter's +// expectation frontier consumes. Minting a second one did not merely shadow it: it made the +// PRE-EXISTING bare reference in output_policy_witness_test.dag unresolvable, so a file this branch +// never touched went red under the whole-corpus strict resolve. Names are corpus-global to bare +// reference resolution, and a witness-local helper must be named as one. +type JqOutcomeExpectation = ExpectPresent | ExpectAbsent | ExpectRefused -fn outcome_matches(outcome: JqOutcome, expected: ExpectedOutcome) -> Bool { +fn outcome_matches(outcome: JqOutcome, expected: JqOutcomeExpectation) -> Bool { match expected { ExpectPresent => match outcome { @@ -259,7 +266,7 @@ fn outcome_matches(outcome: JqOutcome, expected: ExpectedOutcome) -> Bool { fn classifies_as( policy: JqExitPolicy, observation: JqProcessObservation, - expected: ExpectedOutcome, + expected: JqOutcomeExpectation, ) -> Bool { match jq_invocation_process_plan(invocation: JqInvocation { program: JqProgram { source: sensor_program }, diff --git a/docs/plans/cli-invocation-emission-design.md b/docs/plans/cli-invocation-emission-design.md index 6542eab5b4f..a53126fc36a 100644 --- a/docs/plans/cli-invocation-emission-design.md +++ b/docs/plans/cli-invocation-emission-design.md @@ -1171,6 +1171,30 @@ The same shape produced the two earlier defects: an unimported-reference sweep r last addition rather than after it, and a grep whose zero result was accepted without a control that must hit. In each case the mechanism was sound and the **denominator** was authored. +**A third instance, one level up, caught by CI after the above was written.** The rule below fixed +the witness denominator and was still not enough: I minted `type ExpectedOutcome` in the jq witness, +colliding with `gunbc.output_policy`'s load-bearing carrier of the same name, and the failure landed +in `output_policy_witness_test.dag` — **a file that references none of my symbols and that this +branch never touched.** Bare-reference resolution is corpus-global, so a new top-level name can red +a file no per-file closure of mine would ever load. Every local run passed; the whole-corpus strict +resolve is what caught it. + +Two rules follow, and both are mechanical because the authored version keeps failing: + +``` +# every top-level name the branch ADDS, 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 one must have exactly ONE declaration corpus-wide + +# and run what CI runs, before pushing, not after it fails +claim_executor --required-floor --source-root dag --source-root src/v2 +``` + +The second is the one that matters: **a per-file run and the floor are different universes**, and +only the floor is the acceptance path. Reporting a per-file green as though it were the floor is +rung inflation against a declared boundary (§4b) — the same error as citing the strongest path while +another stays silent, committed against my own change. + **The rule adopted for the rest of the lane:** verification enumerates test functions from the FILE, never from memory — From 00556e7f4f778e6c3b3907c89d835ae7226cd735 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 19 Aug 2026 09:18:17 +0000 Subject: [PATCH 21/23] 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) --- dag/gunbc/ci_layer_roots.dag | 7 +++++++ .../process_argv_expansion_receipt_test.dag | 16 ++++++++++++++-- 2 files changed, 21 insertions(+), 2 deletions(-) diff --git a/dag/gunbc/ci_layer_roots.dag b/dag/gunbc/ci_layer_roots.dag index 9fce220e8bf..4ae9c895e66 100644 --- a/dag/gunbc/ci_layer_roots.dag +++ b/dag/gunbc/ci_layer_roots.dag @@ -138,6 +138,12 @@ data witness_exclusion_frontier: List = [ reason: "SUBSTANTIATED per-row (found 2026-08-06, PR #7894 CI red, run 31069215347): maintenance_census_report_positive_control_derives_from_current_head calls current_rust_maintenance_census_report(), which reaches current_stage0_rust_source_observation() and therefore git.Inspect.HeadCommit without mock_response — the same class stage0_rust_host_observation_live_witness_test.dag documents above; a refusing hermetic discovery member fails its whole batch (batch 3 discovery-corpus, 7298-row corpus). This row alone would only remove the function from hermetic discovery, which is not an executing consumer by itself (DESIGN.md 'witness cost derives from purpose', operator ruling 2026-08-04) — so, mirroring stage0_rust_host_observation_live_witness_test.dag's closing contract, the function is ALSO enrolled in bin_witness_wet_entries below (GITHUB_SHA supplied by the runner, not hand-set), which is its real per-PR executing consumer under WitnessHasExecutingConsumer standing; this exclusion row only keeps it off the hermetic per-PR discovery batch it cannot pass. This origin file has only the one witness, so no scaffold-witness residue remains offline-only.", dissolution: unbound_dissolution(description: "mock_response coverage lands for the git.Inspect revision-addressed operations used by current_stage0_rust_source_observation AND this assertion is re-checked under a fixed mock; or the fn enrolls on a scheduled wet lane. Either way this row deletes.") }, + WitnessExclusionRow { + pattern: "process_argv_expansion_receipt_test.dag", + classification: OfflineLocalRecipe, + reason: "SUBSTANTIATED per-row (found 2026-08-19, PR #8467 CI red, run 32234654398, 1 of 9201): case4_expansion_carrier_splices dispatches jq.Process.RunWithStdin, which carries no mock_response, so the hermetic envelope REFUSES rather than skipping and one refusing member fails the run. PUBLISHING A MOCK IS THE WRONG REPAIR HERE, for the reason the stage0 rows above record: this witness's ENTIRE content is that a real jq exits 0 only when it receives two argv words rather than one concatenated one, so a mocked RunWithStdin would let it pass without any process ever running — a green that cannot fail, asserting nothing about the boundary defect it exists to detect. Path was not admission either: the file sits under dag/test/manual/ and was swept into unshrunk discovery regardless, exactly as DESIGN's witness-cost ruling says a directory cannot decide an admission question. This row only keeps it off the hermetic batch; its real executing consumer is the bin_witness_wet_entries enrollment below, under WitnessHasExecutingConsumer standing.", + dissolution: unbound_dissolution(description: "the argv boundary law becomes observable without executing a process -- e.g. the emitted argument vector is inspectable at the host seam as typed data rather than only through a real exit code -- at which point the assertion moves hermetic and this row deletes") + }, WitnessExclusionRow { pattern: "claim/long/mandatory_tag_extdeps_corpus", classification: OfflineLocalRecipe, @@ -943,6 +949,7 @@ data bin_witness_wet_entries: List = [ bin_wet(entry: "dag/test/claim/self_host_artifact_materialization_real_execution_witness_test.dag", f: "the_digest_is_of_the_file_cargo_named_not_of_some_other_real_file"), bin_wet(entry: "dag/test/claim/self_host_artifact_materialization_real_execution_witness_test.dag", f: "changing_only_the_source_bytes_names_exactly_the_artifact_axis"), bin_wet(entry: "dag/test/claim/self_host_artifact_materialization_real_execution_witness_test.dag", f: "rebuilding_identical_source_in_place_moves_no_axis"), + bin_wet(entry: "dag/test/manual/process_argv_expansion_receipt_test.dag", f: "case4_expansion_carrier_splices"), bin_wet(entry: "dag/test/claim/run_verdict_exit_status_witness_test.dag", f: "run_failure_verdict_reaches_nonzero_exit"), bin_wet(entry: "dag/test/claim/run_verdict_exit_status_witness_test.dag", f: "run_success_verdict_reaches_zero_exit"), bin_wet(entry: "dag/test/claim/run_verdict_exit_status_witness_test.dag", f: "run_non_process_exit_return_refuses"), diff --git a/dag/test/manual/process_argv_expansion_receipt_test.dag b/dag/test/manual/process_argv_expansion_receipt_test.dag index 7486c644ac4..99d6bd4b2f1 100644 --- a/dag/test/manual/process_argv_expansion_receipt_test.dag +++ b/dag/test/manual/process_argv_expansion_receipt_test.dag @@ -38,8 +38,20 @@ import extdeps.tools.jq { jq_argv_expansion_probe } // is behavior the model rejects is retired with a receipt, not left standing). What survives // enrolled is the claim the carrier makes: case 4 is red unless jq receives exactly two words. // -// WET: this executes a real jq process. It is a manual receipt, not a floor witness, and its home -// under test/manual says so. +// WET: this executes a real jq process, so it is EXCLUDED from hermetic discovery and ENROLLED in +// gunbc.ci_layer_roots bin_witness_wet_entries. Both rows are required and they answer different +// questions: the exclusion keeps it off a batch it cannot pass (jq.Process.RunWithStdin carries no +// mock_response, and the envelope refuses rather than skipping), while the enrollment is what gives +// it an executing consumer. Exclusion alone would be deletion-with-the-file-retained -- DESIGN's +// witness-cost ruling, whose specimen is exactly that. +// +// Its home under test/manual/ decides NOTHING: the file was swept into unshrunk discovery by path +// regardless, which is the same ruling's point that a directory cannot answer an admission +// question. The rows are the admission; the path is only where it lives. +// +// AND A MOCK IS NOT THE REPAIR. Mocking RunWithStdin would make this pass without any process +// running, while its entire content is that a REAL jq exits 0 only on two argv words -- a green +// that cannot fail. fn probe_lex() -> ModeledLexRules { ModeledLexRules { From 50fb645e02711833d7bcbe0c43e784cdaccceddc Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 19 Aug 2026 09:20:04 +0000 Subject: [PATCH 22/23] 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) --- dag/gunbc/ci_layer_roots.dag | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/dag/gunbc/ci_layer_roots.dag b/dag/gunbc/ci_layer_roots.dag index 4ae9c895e66..184dbbdd7fb 100644 --- a/dag/gunbc/ci_layer_roots.dag +++ b/dag/gunbc/ci_layer_roots.dag @@ -140,8 +140,8 @@ data witness_exclusion_frontier: List = [ }, WitnessExclusionRow { pattern: "process_argv_expansion_receipt_test.dag", - classification: OfflineLocalRecipe, - reason: "SUBSTANTIATED per-row (found 2026-08-19, PR #8467 CI red, run 32234654398, 1 of 9201): case4_expansion_carrier_splices dispatches jq.Process.RunWithStdin, which carries no mock_response, so the hermetic envelope REFUSES rather than skipping and one refusing member fails the run. PUBLISHING A MOCK IS THE WRONG REPAIR HERE, for the reason the stage0 rows above record: this witness's ENTIRE content is that a real jq exits 0 only when it receives two argv words rather than one concatenated one, so a mocked RunWithStdin would let it pass without any process ever running — a green that cannot fail, asserting nothing about the boundary defect it exists to detect. Path was not admission either: the file sits under dag/test/manual/ and was swept into unshrunk discovery regardless, exactly as DESIGN's witness-cost ruling says a directory cannot decide an admission question. This row only keeps it off the hermetic batch; its real executing consumer is the bin_witness_wet_entries enrollment below, under WitnessHasExecutingConsumer standing.", + classification: BinWitnessWet, + reason: "SUBSTANTIATED per-row (found 2026-08-19, PR #8467 CI red, run 32234654398, 1 of 9201): case4_expansion_carrier_splices dispatches jq.Process.RunWithStdin, which carries no mock_response, so the hermetic envelope REFUSES rather than skipping and one refusing member fails the run. PUBLISHING A MOCK IS THE WRONG REPAIR HERE, for the reason the stage0 rows above record: this witness's ENTIRE content is that a real jq exits 0 only when it receives two argv words rather than one concatenated one, so a mocked RunWithStdin would let it pass without any process ever running — a green that cannot fail, asserting nothing about the boundary defect it exists to detect. Path was not admission either: the file sits under dag/test/manual/ and was swept into unshrunk discovery regardless, exactly as DESIGN's witness-cost ruling says a directory cannot decide an admission question. This row only keeps it off the hermetic batch; its real executing consumer is the bin_witness_wet_entries enrollment below, under WitnessHasExecutingConsumer standing. CLASSIFIED BinWitnessWet, NOT OfflineLocalRecipe: the two differ in what they CLAIM, since BinWitnessWet projects SchedulingEnrolled while OfflineLocalRecipe projects SchedulingDark, so the offline label on a row that really does run per-PR would understate its own coverage -- and per DESIGN's witness-cost ruling a broad offline path verdict is exactly the unconditional admission that was retired. BinWitnessWet is also the arm the reconciliation witness holds to account: an unbacked BinWitnessWet row reds, and this one is backed by the entry below.", dissolution: unbound_dissolution(description: "the argv boundary law becomes observable without executing a process -- e.g. the emitted argument vector is inspectable at the host seam as typed data rather than only through a real exit code -- at which point the assertion moves hermetic and this row deletes") }, WitnessExclusionRow { From 5ea765c2e64fccffab15a65e972be96b0f51b463 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 19 Aug 2026 09:51:37 +0000 Subject: [PATCH 23/23] 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) --- dag/gunbc/ci_layer_roots.dag | 7 ------- docs/plans/cli-invocation-emission-design.md | 22 ++++++++++++++++++++ src/v1/stage0/src/cli_run.rs | 19 +++++++++++++++++ 3 files changed, 41 insertions(+), 7 deletions(-) diff --git a/dag/gunbc/ci_layer_roots.dag b/dag/gunbc/ci_layer_roots.dag index 00fa5c6bd81..1e62abcd0b9 100644 --- a/dag/gunbc/ci_layer_roots.dag +++ b/dag/gunbc/ci_layer_roots.dag @@ -132,12 +132,6 @@ data witness_exclusion_frontier: List = [ reason: "SUBSTANTIATED per-row (found 2026-08-06, PR #7894 CI red, run 31069215347): maintenance_census_report_positive_control_derives_from_current_head calls current_rust_maintenance_census_report(), which reaches current_stage0_rust_source_observation() and therefore git.Inspect.HeadCommit without mock_response — the same class stage0_rust_host_observation_live_witness_test.dag documents above; a refusing hermetic discovery member fails its whole batch (batch 3 discovery-corpus, 7298-row corpus). This row alone would only remove the function from hermetic discovery, which is not an executing consumer by itself (DESIGN.md 'witness cost derives from purpose', operator ruling 2026-08-04) — so, mirroring stage0_rust_host_observation_live_witness_test.dag's closing contract, the function is ALSO enrolled in bin_witness_wet_entries below (GITHUB_SHA supplied by the runner, not hand-set), which is its real per-PR executing consumer under WitnessHasExecutingConsumer standing; this exclusion row only keeps it off the hermetic per-PR discovery batch it cannot pass. This origin file has only the one witness, so no scaffold-witness residue remains offline-only.", dissolution: unbound_dissolution(description: "mock_response coverage lands for the git.Inspect revision-addressed operations used by current_stage0_rust_source_observation AND this assertion is re-checked under a fixed mock; or the fn enrolls on a scheduled wet lane. Either way this row deletes.") }, - WitnessExclusionRow { - pattern: "process_argv_expansion_receipt_test.dag", - classification: BinWitnessWet, - reason: "SUBSTANTIATED per-row (found 2026-08-19, PR #8467 CI red, run 32234654398, 1 of 9201): case4_expansion_carrier_splices dispatches jq.Process.RunWithStdin, which carries no mock_response, so the hermetic envelope REFUSES rather than skipping and one refusing member fails the run. PUBLISHING A MOCK IS THE WRONG REPAIR HERE, for the reason the stage0 rows above record: this witness's ENTIRE content is that a real jq exits 0 only when it receives two argv words rather than one concatenated one, so a mocked RunWithStdin would let it pass without any process ever running — a green that cannot fail, asserting nothing about the boundary defect it exists to detect. Path was not admission either: the file sits under dag/test/manual/ and was swept into unshrunk discovery regardless, exactly as DESIGN's witness-cost ruling says a directory cannot decide an admission question. This row only keeps it off the hermetic batch; its real executing consumer is the bin_witness_wet_entries enrollment below, under WitnessHasExecutingConsumer standing. CLASSIFIED BinWitnessWet, NOT OfflineLocalRecipe: the two differ in what they CLAIM, since BinWitnessWet projects SchedulingEnrolled while OfflineLocalRecipe projects SchedulingDark, so the offline label on a row that really does run per-PR would understate its own coverage -- and per DESIGN's witness-cost ruling a broad offline path verdict is exactly the unconditional admission that was retired. BinWitnessWet is also the arm the reconciliation witness holds to account: an unbacked BinWitnessWet row reds, and this one is backed by the entry below.", - dissolution: unbound_dissolution(description: "the argv boundary law becomes observable without executing a process -- e.g. the emitted argument vector is inspectable at the host seam as typed data rather than only through a real exit code -- at which point the assertion moves hermetic and this row deletes") - }, WitnessExclusionRow { pattern: "claim/long/mandatory_tag_extdeps_corpus", classification: OfflineLocalRecipe, @@ -939,7 +933,6 @@ data bin_witness_wet_entries: List = [ bin_wet(entry: "dag/test/claim/self_host_artifact_materialization_real_execution_witness_test.dag", f: "the_digest_is_of_the_file_cargo_named_not_of_some_other_real_file"), bin_wet(entry: "dag/test/claim/self_host_artifact_materialization_real_execution_witness_test.dag", f: "changing_only_the_source_bytes_names_exactly_the_artifact_axis"), bin_wet(entry: "dag/test/claim/self_host_artifact_materialization_real_execution_witness_test.dag", f: "rebuilding_identical_source_in_place_moves_no_axis"), - bin_wet(entry: "dag/test/manual/process_argv_expansion_receipt_test.dag", f: "case4_expansion_carrier_splices"), bin_wet(entry: "dag/test/claim/stage0_regen_convergence_real_execution_witness_test.dag", f: "a_real_regen_stage0_verify_run_reports_zero_divergence"), bin_wet(entry: "dag/test/claim/stage0_regen_convergence_real_execution_witness_test.dag", f: "w_RED_an_unrecognized_flag_does_not_report_the_success_marker"), bin_wet(entry: "dag/test/claim/run_verdict_exit_status_witness_test.dag", f: "run_failure_verdict_reaches_nonzero_exit"), diff --git a/docs/plans/cli-invocation-emission-design.md b/docs/plans/cli-invocation-emission-design.md index a53126fc36a..48d8c8b5284 100644 --- a/docs/plans/cli-invocation-emission-design.md +++ b/docs/plans/cli-invocation-emission-design.md @@ -1247,6 +1247,28 @@ lane's actual position: - The other three `openbmc.JsonProjection` operations are unmigrated, and two of them (`ObjectMapperServiceCount`, `ObjectMapperServiceAt`) need `--argjson` lowering, which is unbuilt. - No negative falsifier exists yet proving a REST path reaches none of these carriers. +- **The wet receipt does not execute in CI, and this is a declared gap rather than an enrollment.** + The hermetic floor refuses `jq.Process.RunWithStdin` (no `mock_response`) and mocking would + defeat the assertion, so the file is named in `cli_run.rs` `floor_prepared_subject_exclusions`. + No wet lane exists to host it: the falsifier and wet batches died with the floor cut, and + `v2.workflow.required_floor` deliberately defers wet lanes until the question can be "asked + against a live consumer". So the claim sits at **UNEXECUTED-IN-CI**, evidenced only by the + recorded run above and reproducible locally with: + + ``` + claim_batch --wet --source-root dag --source-root src/v2 --entry dag/test/manual/process_argv_expansion_receipt_test.dag --functions case4_expansion_carrier_splices + ``` + + **Re-enrollment trigger:** a wet lane with a live consumer exists again. + + The first attempt at this admission added rows to `gunbc.ci_layer_roots` + (`witness_exclusion_frontier` + `bin_witness_wet_entries`) and a commit message asserting they + would take effect. They did not — `run_required_floor` consults the Rust list and nothing else, + and the CI receipt was an unchanged `modules_excluded=2`. Both rows were reverted rather than + left standing: a row in a roster with no live consumer is specification-without-execution, and + the enrollment half would have been worse than useless, since it would have *claimed* an + executing consumer for a witness nothing runs. Recorded because the mistake is instructive — + I read a neighbouring row's shape as the mechanism instead of tracing the mechanism's caller. - The wet receipt run reports `[expectation-frontier] 1 site(s), 1 dispatch(es) undeclared: jq.Process.RunWithStdin=1`. That is the new handler's dispatch not being declared to the expectation registry. It is left standing rather than silenced because it is exactly the shape §5 diff --git a/src/v1/stage0/src/cli_run.rs b/src/v1/stage0/src/cli_run.rs index 6f5b2e19133..b407b6bd8b0 100644 --- a/src/v1/stage0/src/cli_run.rs +++ b/src/v1/stage0/src/cli_run.rs @@ -38004,6 +38004,25 @@ pub fn floor_prepared_subject_exclusions() -> Vec { vec![ "test/fixture/meta_exec_confinement_scan/".to_string(), "test/manual/ownership_movable_test.dag".to_string(), + // WET RECEIPT, AND IT HAS NO CI CONSUMER TODAY — stated plainly rather than dressed up + // as an enrollment. case4_expansion_carrier_splices dispatches a real jq through + // jq.Process.RunWithStdin, which carries no mock_response, so the hermetic floor refuses + // it and one refusing member fails the run. Mocking is not the repair: the witness exists + // to prove that a REAL jq exits 0 only on two argv words rather than one concatenated + // one, and a mocked dispatch passes it without any process running. + // + // The first attempt at this fix added rows to gunbc.ci_layer_roots + // (witness_exclusion_frontier + bin_witness_wet_entries) and asserted they would take + // effect. They did not: run_required_floor consults THIS list and nothing else, the CI + // receipt was an unchanged modules_excluded=2, and the wet batches those rosters feed + // were deleted with the old floor. Adding a row to a roster with no live consumer is + // specification-without-execution, so both rows were reverted rather than left standing. + // + // What this exclusion buys is a green floor; what it does NOT buy is coverage. The claim + // sits at UNEXECUTED-IN-CI with a local recipe recorded in the design note (§15), and + // re-enrolls when a wet lane exists again — which required_floor.dag deliberately defers + // until it can be "asked against a live consumer". + "test/manual/process_argv_expansion_receipt_test.dag".to_string(), ] }