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 7777636554e..1a4940191a3 100644 --- a/dag/extdeps/tools/jq.dag +++ b/dag/extdeps/tools/jq.dag @@ -1,6 +1,24 @@ module extdeps.tools.jq -import std.types { NonEmptyStr, String, Bool } +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, 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 { + Diagnostic, + ExternalContractUnknown, + Outcome, + Unavailable, + bind_outcome, + node_locus, + outcome_accepted, + 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 } @@ -23,15 +41,442 @@ 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", "-r", "{filter}", "{path}"] } + 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", arguments] + } exit { 0 => Unit - nonzero => String "jq extract failed" + nonzero => Unit + } + } +} + +// --------------------------------------------------------------------------------------------- +// 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. A domain module reaches this +// 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 +// 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 +// 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 + +// 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 } + } +} + +// 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 + } +} + +// 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" + } +} + +fn jq_option_canonical_spelling(option: JqCliOption) -> NonEmptyStr { + cli_long_option_spelling(name: jq_option_long_name(option: option)) +} + +// 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) } + }, + ] + } + } +} + +// 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 + process_input: JqProcessInput +} + +// 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 { 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 +// 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 { cause: JqBindingLoweringUnwired } + Empty => + match invocation.input { + JqInputFile { path: _ } => + JqLoweringRefused { cause: JqFileInputLoweringUnwired } + 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 + ), + process_input: JqProcessStdin { content: 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 COMPLETE RESULT, because argv alone cannot carry a jq invocation. An earlier revision made +// jq_invocation_cli_arguments the public entry: it projected plan.arguments into a CliSurface and +// DISCARDED plan.stdin, so the program's input silently vanished at the module boundary. The +// witness did not catch it, and could not have: "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 correct routing. +// +// This carrier also gives tool identity its first real consumer, so which binary runs stops being +// ambient. A handler consumes THIS, never a bare CliSurface it must reopen the JqInvocation to +// complete -- that would give the process projection two authorities. +// A PROCESS WITH NO STDIN CHANNEL AND A PROCESS GIVEN EMPTY STDIN ARE DIFFERENT EXECUTIONS. +// An earlier revision carried Optional, 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 { + surface: CliSurface + 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_input(plan: JqAdmittedProcessPlan) -> JqProcessInput { plan.process_input } + +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 { + surface: surface, + process_input: plan.process_input, + exit_policy: invocation.exit_policy + }) + } + ) + } +} + +// 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 { cause: cause } => + outcome_rejected(jq_lowering_refused_diagnostic(cause: cause)) + JqLowered { plan: plan } => + serialize_cli_arguments( + arguments: plan.arguments, + lex: jq_cli_lex_rules(), + binding_spellings: plan.binding_spellings + ) + } +} + +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_refusal_identity(cause: cause), + at: node_locus(node: Node { + kind: TypeNode { connective: Atom { identity: ^jq_invocation_lowering } }, + children: [], + occurrence_id: SyntheticOccurrence + }), + 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/cli_surface_boundary_probe_test.dag b/dag/test/claim/cli_surface_boundary_probe_test.dag new file mode 100644 index 00000000000..54df28cf9ab --- /dev/null +++ b/dag/test/claim/cli_surface_boundary_probe_test.dag @@ -0,0 +1,198 @@ +module test.claim.cli_surface_boundary_probe + +import std.algebra { Cons, Empty } +import std.types { Bool, String } +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, + cli_argument_text, + cli_surface_arguments, + serialize_cli_arguments +} +import v2.std.compilers.lexing { + LexRuleSet, + LiteralPattern, + ModeledLexRules, + TokenRule +} +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). +// +// 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". +// +// 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_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_dash_option, pattern: LiteralPattern { text: "--color" } }, + TokenRule { token_class: ^probe_equals, pattern: LiteralPattern { text: "=" } }, + TokenRule { token_class: ^probe_value, pattern: LiteralPattern { text: "never" } }, + ] + } + } +} + +// 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 { + [ + FixedToken { token_class: ^probe_dash_option }, + FixedToken { token_class: ^probe_equals }, + FixedToken { token_class: ^probe_value }, + ] +} + +// 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 { + 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 { + match serialize_cli_arguments( + arguments: arguments, + lex: probe_lex_rules(), + binding_spellings: empty_map() + ) { + Accepted { value: surface, diagnostics: _ } => + 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: b, tail: r2 } => + match r2 { + Empty => false + Cons { head: c, tail: r3 } => + match r3 { + Empty => (a == "--color") && (b == "=") && (c == "never") + Cons { head: _, tail: _ } => false + } + } + } + } +} + +// 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: flatten_grouping(arguments: separated_grouping()), + lex: probe_lex_rules(), + binding_spellings: empty_map() + ) { + Accepted { value: text, diagnostics: _ } => + render_target_text(t: text) == "--color=never" + 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 new file mode 100644 index 00000000000..4b8dcfab4c0 --- /dev/null +++ b/dag/test/claim/jq_invocation_lowering_witness_test.dag @@ -0,0 +1,339 @@ +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, + JqBindingLoweringUnwired, + JqFileInputLoweringUnwired, + JqLowered, + JqLoweringRefused, + 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 +} + +// 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 +// 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 + } +} + + +// 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_input(plan: plan) { + JqProcessNoStdin => false + JqProcessStdin { content: 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 + } + } +} + + +// 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. + +// 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: JqOutcomeExpectation) -> 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: JqOutcomeExpectation, +) -> 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..99d6bd4b2f1 --- /dev/null +++ b/dag/test/manual/process_argv_expansion_receipt_test.dag @@ -0,0 +1,85 @@ +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, 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 { + 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 new file mode 100644 index 00000000000..48d8c8b5284 --- /dev/null +++ b/docs/plans/cli-invocation-emission-design.md @@ -0,0 +1,1280 @@ +# CLI invocation emission — the tree is the authority, argv is emitted + +**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 +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: 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 = JqJsonOutput | JqRawOutput // -r writes STRING results raw; + // non-string results stay JSON-formatted + +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: two orthogonal axes, sealed + +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 +--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, default 5 usage 2 compile error 3 +``` + +``` +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 +} +``` + +| 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*; 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. `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 + +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. + +**`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 +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. + +**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 + 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 — 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`, `--`, 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 +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 +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 — 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. +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. + +**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 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 +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 +{"data": 41} -> Observed 41 {"data": null} -> Absent +{} -> Absent invalid JSON -> Refused +two numeric inputs -> Refused, never first-pick jq nonzero -> Refused +``` + +**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: + +``` +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 +``` + +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. + +**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. 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 +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, by exact subject + +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. + +| exact subject | honest rung after the first vertical | mechanism | +|---|---|---| +| 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 | +| 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 | + +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_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 +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. + +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 — 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 + 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. +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`. +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 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. + +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. + + **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 — `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` + 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. + +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`, + 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. + +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* + 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. + +--- + +## 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. +- *"`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`. +- *"`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. + +--- + +## 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. + +**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 — + +``` +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 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 + 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/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(), ] } diff --git a/src/v1/stage0/src/v1_interpreter.rs b/src/v1/stage0/src/v1_interpreter.rs index ecd4070a3bb..ab43fe8bd06 100644 --- a/src/v1/stage0/src/v1_interpreter.rs +++ b/src/v1/stage0/src/v1_interpreter.rs @@ -7231,8 +7231,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 new file mode 100644 index 00000000000..f06fa062dd7 --- /dev/null +++ b/src/v2/std/compilers/cli_surface.dag @@ -0,0 +1,293 @@ +module v2.std.compilers.cli_surface + +import std.algebra { Empty } +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, + 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, + node_locus, + outcome_accepted, + outcome_rejected +} +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. 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 +// 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. +// +// 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: 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 +// 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 -- 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 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. + +// 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 } + +// 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 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) +} + + +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 +} + +// 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 +// 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. +// 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: 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: text }) } + ) +} + +// 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, + binding_spellings: Map +) -> Outcome { + bind_outcome( + o: fold_list( + xs: arguments, + empty: outcome_accepted(Empty), + cons: fn(acc, argument) { + 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) { + outcome_accepted(CliSurface { arguments: rendered }) + } + ) +}