Repository navigation
jq argv dissolution: --argjson + file-input lowering, first SSH migration - #10148
Merged
Merged
Conversation
added 3 commits
September 2, 2026 23:20
…vocation_lower
The binding axis of the jq vertical stops refusing and starts lowering. A
JqJsonBinding (a typed name + JSON value) renders as THREE argv words --
the --argjson option, the binding name, the JSON value -- each its own
argument, inserted BEFORE the program operand (POSIX guideline 9: options
precede operands). The caller still never spells --argjson: the option
identity selects its cited long-form spelling exactly like raw-output and
exit-status do.
Three refusal causes replace the single placeholder:
- JqBindingNameDuplicate: a repeated name refuses rather than being
handed to jq's last-wins behaviour.
- JqTextBindingUnwired: no live consumer this wave; refuses rather than
emitting a plausible guess.
- JqFileInputLoweringUnwired: unchanged; file input lands with the
remote population.
The binding NAME and VALUE each need an injective spelling-map key, or one
binding's value can be silently substituted for another's. Keys carry a
role prefix that cannot collide with any name (prefixed keys begin with a
reserved dot-suffixed stem, and duplicate names refuse separately).
The unlowered-bindings refusal witnesses flip to a positive assertion
(json_binding_lowers_to_exact_argv) plus duplicate/text refusals, and the
three refusal causes carry distinct identities. All 16 witness tests pass;
whole-corpus regen is clean (first_generation_equal=true).
…onto the semantic invocation
The two ObjectMapper projections the sensor-service enumeration makes are
no longer argv-spelled shell operations. ObjectMapperServiceAt and
ObjectMapperServiceCount are deleted from openbmc.JsonProjection; their
callers now reach openbmc_object_mapper_service_at / _count, which build a
JqInvocation whose flags and bindings are derived:
- ServiceAt carries a typed JSON binding (index) through --argjson and
reads under JqLastResultExit: the program emits the service name at
that index, or nothing/exit-1 for an out-of-range index.
- ServiceCount reads the key count under the same policy.
Both callers decode a JqOutcome through jq_classify_observation and match
OpenBmcServiceObserved | OpenBmcServiceProjectionRefused (and the count
sibling) instead of reading success/value/stderr. The old 'success: Bool
from exit_success' second-representation field is gone with the operations.
Module typechecks cleanly and whole-corpus regen is first_generation_equal=true.
The --argjson binding lowering and the ObjectMapperServiceAt/ServiceCount migration (§17) supersede the §15 note that the lowering was unbuilt. The remaining unmigrated operation is ProjectFanConfig, which additionally needs file-input lowering (the remote population, Wave 2).
briansrls
marked this pull request as ready for review
September 3, 2026 01:30
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 707a65cab1
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| ], | ||
| input: JqInputStdin { content: content }, | ||
| output_encoding: JqRawOutput, | ||
| exit_policy: JqLastResultExit, |
There was a problem hiding this comment.
When index is outside the keys array, this filter emits null rather than no output. I confirmed with jq 1.7 (jq --help: -e, --exit-status set exit status code based on the output) that the equivalent command prints null and exits 1; jq_classify_observation maps exit 1 with nonempty stdout to JqOutputPresent, so openbmc_object_mapper_service_at_result returns OpenBmcServiceObserved { service: "null" } instead of the intended missing-index refusal. Make the filter emit empty for null/out-of-range results before classifying it.
Useful? React with 👍 / 👎.
Contributor
Author
There was a problem hiding this comment.
Fixed in a03f17d: the program row is now .data[0] | keys | .[$index] // empty, so an out-of-range index emits NO output (absence, exit 4) instead of null (a legitimate value under JqLastResultExit). A witness pins the program text (object_mapper_service_at_program_emits_empty_for_out_of_range).
added 3 commits
September 3, 2026 09:48
…lower The remote jq population (Wave 2 of the shell->dag migration) reads the config file on the BMC filesystem, so JqInputFile must lower instead of refusing. A file input is an ARGV OPERAND -- the path lands as one bound word AFTER the program operand (POSIX guideline 9), and the file's bytes never enter a process channel: the plan carries JqProcessNoStdin. JqFileInputLoweringUnwired dissolves on climb (DESIGN 4b); the refusal causes are now JqBindingNameDuplicate | JqTextBindingUnwired. Witnesses: the two file-input refusals flip to file_input_lowers_to_exact_argv (argv equality) and file_input_reaches_the_plan_as_no_stdin (process-input arm); the distinct-identity test drops the dissolved cause.
…remote jq realization
The first remote jq population leaves its raw sshpass/ssh argv
(["jq","-er","<program>","{config_path}"]) for a semantic
JqInvocation + remote realization:
- extdeps.tools.jq: (part 1) JqInputFile lowers; this part consumes it.
- openbmc_password_ssh_transport: FanStepwiseCount DELETED at the root;
RunCommand ADDED -- the RFC 4254 command-string carrier with fixed
sshpass/ssh argv, the command string as the SINGLE final word.
- openbmc_fan_control: openbmc_remote_jq_command / _execute compose the
plan -> remote words -> grammar-owned single-quote command string
(remote_exec_command_string, never append(ssh_prefix, inner.argv)) ->
transport. A stdin-fed remote plan is a TYPED refusal
(OpenBmcRemoteJqStdinUnwired): sshpass -d 0 holds fd 0, so a remote
stdin payload would collide. openbmc_fan_config_stepwise_count decodes
JqOutcome, never success/stdout/stderr.
- openbmc_operation: OpenBmcStepwiseCount removed from the query
coproduct; the dispatch arm and the transport operation are gone.
Also folds the PR#10148 review fix: openbmc_object_mapper_service_at_program
now ends `// empty`, so an out-of-range index emits NO output (absence,
exit 4) instead of null (a legitimate value under JqLastResultExit, which
would decode as a service named "null").
Witnesses: dag/test/claim/remote_jq_ssh_migration_witness (10 tests) --
the JqOutcome decode, the remote word vector, the exact RFC 4254 command
string, the stdin collision refusal (command and execute levels), the
Unknown-interpretation perturbation, and a pin on the review-fixed
program.
Adds §18 (Wave 2 cutover receipt -- the first SSH migration): the file-input lowering, the RunCommand carrier, the stdin-fed remote jq typed refusal, and the honest 'not established' ceiling -- the remote half is unexecuted against a live target (remote_exec_command_live_confirmation stays declared-unexecuted), ProjectFanConfig and the remaining remote population are not cut over, and JqTextBinding still refuses. Updates §15/§17 bullets that named file-input lowering as unbuilt.
gunbai-bot
Bot
changed the title
added 3 commits
September 3, 2026 12:32
Review observation (claude-opus-4-7, non-blocking): jq_option_arguments ends with list_append(..., right: Empty), which appends an empty list and changes nothing. Removed; the option/binding accumulation is now the inner two-way append and the program operand is snoc'd on directly. Emitted argv is byte-identical -- the argv-equality witnesses (sensor, json binding, file input, exit-policy perturbation) all still pass.
…sentinel Review observation (claude-opus-4-7, cosmetic): the seen map stored "" as its value because only key presence matters. A fabricated sentinel is a second representation of presence (DESIGN 5: never fabricate) -- the value now carries the actual binding name. Presence-check behavior is unchanged; the duplicate-name refusal and argv-equality witnesses all still pass. (The other observation from that review -- the no-op list_append(_, right: Empty) tail in jq_option_arguments -- was already removed in e675554.)
…ion (review 38602) REVIEW FINDING (codex/gpt-5.6-sol, REQUEST_CHANGES): the production path openbmc_remote_jq_execute hard-coded openbmc_dropbear_interpretation for every session -- an explicitly unverified deployment assumption (remote_exec_command_live_confirmation is declared Unexecuted), promoted into the accepted path and bypassing the Unknown refusal. DESIGN 4b: external reality is observed, refused, or mitigated at a declared boundary, never fabricated. DESIGN 5: refuse rather than emit a plausible guess. RESOLUTION (the review's offered option b, since no live BMC exists to confirm option a): the production path now passes Unknown and REFUSES with a typed, located cause (RemoteExecInterpretationUnknown) until a live OpenBMC/Dropbear target confirms a POSIX-shell interpretation. The pure emitter stays witnessable by passing an interpretation explicitly. Witnesses: remote_jq_execute_gates_on_unknown_interpretation asserts the execute-level gate; fan_config_stepwise_count_refuses_until_live_confirmation asserts the production caller's gate refusal. remote_jq witness suite is now 12/12; whole-corpus regen first_generation_equal=true.
gunbai-bot
Bot
force-pushed
the
session/snappy-lark-902
branch
from
September 3, 2026 20:33
5d8474e to
7c7e71a
Compare
…lue, FilePath, argjson authority, jq-owned executable; load-bearing live confirmation
Bar 1 (JqJsonBinding.value = JsonValue): the binding value is now the
canonical structured JSON type from extdeps.languages.json.emit, NOT a
NonEmptyStr that the caller serialized. The lowering owns serialization
(via serialize_json). The caller (openbmc_object_mapper_service_at) says
value: json_int(n: index), not serialize_json(json_int(index)) as NonEmptyStr.
Bar 2 (JqInputFile.path = FilePath): the file-input path is now the
repository's FilePath type (String where non_empty), not a bare NonEmptyStr.
Bar 3 (argjson option selected through the authority): the binding fold
now constructs JqBindingArgumentGroup (option + name + value held as ONE
group, preserving arity and order until final argv flattening), and the
option FixedToken selects through jq_option_token_class(JqCliOptionArgJson)
instead of a bare ^jq_opt_argjson literal — the two-level derivation
(semantic property → option identity → cited spelling) owns the token.
Bar 4 (sealed RemoteExecCommand): added type RemoteExecCommand
sole_constructor { rendered: NonEmptyStr } in gunbc.remote_shell_command.
Only remote_exec_command_string may mint one; the transport boundary
unwraps via remote_exec_command_rendered. RunCommand in the transport
receives the unwrapped NonEmptyStr (the wall is that no arbitrary module
can construct a RemoteExecCommand). Updated extdeps.exec.command
command_over_transport and both witness suites.
Bar 5 (jq owns its executable identity): added data jq_executable in
jq.dag; openbmc_remote_jq_words imports it from the jq module instead
of spelling "jq" as a literal.
Bar 6 (Unknown production gate preserved): openbmc_remote_jq_execute
still hard-fails under Unexecuted — the gate is load-bearing, matched
against remote_exec_command_live_confirmation. Under
RemoteExecCommandLiveConfirmationUnexecuted: Unknown → refusal. Under
RemoteExecCommandLiveConfirmationObserved: openbmc_dropbear_interpretation
→ path opens. The receipt genuinely unlocks execution (not a permanent
trigger wearing a stall's clothes).
Also fixed: the comment-in-function-body parse error (lines 1434-1435
and inner body-comments at jq.dag:330, openbmc_fan_control.dag:1444)
that caused the CI required-witnesses-floor failure — moved above the
function at module-item grain or removed entirely.
gunbai-bot
Bot
force-pushed
the
session/snappy-lark-902
branch
from
September 3, 2026 21:05
7c7e71a to
316b4ce
Compare
added 8 commits
September 4, 2026 03:43
…ved-arm fixture witness Extracts the receipt-to-interpretation derivation into a named function (openbmc_remote_jq_interpretation) so both arms are witnessable with hermetic fixtures. Adds a fixture test that proves the Observed arm returns PosixShellInterpreted (path opens) when called with a synthetic RemoteExecCommandLiveConfirmationObserved value — no live BMC needed, no fabrication, no permanent stall. Also fixes two import hygiene issues from review 59489: - Adds RemoteExecCommandLiveConfirmation, RemoteExecCommandLiveConfirmationObserved, RemoteExecCommandLiveConfirmationUnexecuted, SimpleCommandArgvRefused, and PosixShellInterpreted to the witness import block (was binding by pool membership rather than declared rule — DESIGN §5 binding rule). - Removes the string_contains(prose) assertion in fan_config_stepwise_count_refuses_until_live_confirmation; the typed- variant gate test (remote_jq_execute_gates_on_unknown_interpretation) already matches the typed cause directly. Witness suite: 13/13 pass.
…rmation test The test asserted 'refuses until live confirmation' but matched reason: _, accepting ANY refusal cause -- weaker than the prose assertion it replaced, failing exactly the admitted class the review correctly identified. The typed-variant gate test (remote_jq_execute_gates_on_unknown_interpretation) already covers the same claim at the correct abstraction layer by matching RemoteExecInterpretationUnknown directly. Remote_jq witness suite: 12/12 pass (removed the loose test, kept the Observed fixture witness as 13th).
OpenBmcIntegerRefused carries a rendered String, not a typed cause, so every consumer downstream is cause-blind for refusals. The typed cause is preserved through the execute layer (OpenBmcRemoteJqRefused carries OpenBmcRemoteJqRefusal) and can be matched there. Named as a follow-up: carry the typed cause through OpenBmcIntegerResult and move the renderer to the presentation edge.
…ngling section cite - Moved the LOSSY REFUSAL CARRIER block below data openbmc_fan_stepwise_count_program so it attaches to fn openbmc_fan_config_stepwise_count, not the data row. - Fixed type name: OpenBmcRemoteJqRefusal (not OpenBmcRemoteJqRefusalCause). - Dropped the dangling section-18 cite (the document ends at §16; the follow-up is named by the symbol it changes: OpenBmcIntegerResult).
…(3) rung drop for lossy carrier Finding 1 (fabricated label unlocks gate): remote_exec_command_live_confirmation's Observed variant now carries interpretation: RemoteExecCommandInterpretation (a typed coproduct arm) instead of result: NonEmptyStr (an arbitrary string). The fixture witness constructs RemoteExecCommandLiveConfirmationObserved with a real interpretation value (openbmc_dropbear_interpretation). Constructing an Observed value without a valid interpretation is structurally impossible — the type enforces it. openbmc_remote_jq_interpretation reads the interpretation from the confirmation rather than assuming PosixShellInterpreted for all Observed values. The composition fragility the manager noted (chain closes only because openbmc_dropbear_interpretation IS PosixShellInterpreted) is also resolved: the interpretation is carried through, not assumed. Finding 2 (lossy refusal carrier without a §4b(3) rung drop): added the full declaration — previous rung (mechanically preventable, typed cause at execute layer), this rung (structurally guaranteed at the stepwise_count boundary), reason (sole consumer needs prose for operator output), bounded population (count=1), restoration trigger (OpenBmcIntegerResult carries typed cause instead of String).
The block declared a drop that did not exist — the lossy carrier predates this PR and is a discovered error class, not a deliberate regression. The rung numbers ascended instead of descending. A comment is not a roster anyway: drops are declared in docs/design-rung-drops.md, failure modes in the projection above. The class is recorded in the PR description as a discovered error class at rung 4b(2), with ceiling 4b(3), gated on OpenBmcIntegerResult carrying the typed cause.
…efusal) Same class as the 1434 incident: two // lines inside the test fn body triggered a source-annotation parse refusal. The code was already clear from variable names and match arms; the comments were redundant.
Brings in gunbc#10302 (main_wet_verted) and other mainline changes that the heal-generated-artifacts CI job depends on.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Advances the jq vertical of the shell→dag argv-dissolution work (
docs/plans/cli-invocation-emission-design.md) through Wave 1A and the first SSH migration (Wave 2).What this PR does
Every change enforces one invariant: a caller describes a semantic
JqInvocationand flags are derived — no caller spells-e,-r,--argjson,--arg, an argv position, or the executable name.jq_invocation_lowerlowersJqJsonBinding→--argjson <name> <value>via the two-level row derivation (semantic property → option identity → cited spelling), held as aJqBindingArgumentGroupuntil final argv flattening. The argv-spelledObjectMapperServiceAt/ObjectMapperServiceCountshell operations are deleted at the root; callers decodeJqOutcome. The placeholder refusal (JqBindingLoweringUnwired) splits into typed causes;JqFileInputLoweringUnwireddissolves on climb with file-input lowering.JqInputFile→ file operand (JqProcessNoStdin).OpenBmcStepwiseCountleaves its rawsshpass/sshargv for a semantic invocation + remote realization that emits the RFC 4254 command string via the grammar-owned single-quote encoder (remote_exec_command_string→ sealedRemoteExecCommand sole_constructor). Stdin-fed remote jq refuses with a typed collision cause (sshpass -d 0holds fd 0).JsonValue(jq module owns serialization); JqInputFile.path carriesFilePath."jq".openbmc_remote_jq_executereadsremote_exec_command_live_confirmationand matches:Observed→ path opens;Unexecuted→ refusal (RemoteExecInterpretationUnknown). TheObservedvariant carries a typedRemoteExecCommandInterpretation(not an arbitrary string), so constructing one requires a real interpretation.emptyguard, no-oplist_appendtail removed,seen-map sentinel replaced with real binding name, comments moved to module-item grain.Discovered error class (not resolved by this PR)
OpenBmcIntegerRefusedcarries a renderedString(reason), not a typed cause — so every consumer downstream ofopenbmc_fan_config_stepwise_countis cause-blind for refusals. The typed cause is preserved through the execute layer (OpenBmcRemoteJqRefusedcarriesOpenBmcRemoteJqRefusal) and can be matched there. Currently at rung 4b(1) (mitigatable — the operation is total and the outcome is typed at the variant level, so a caller cannot mistake refusal for success; no mechanism discriminates the cause at this layer). The ceiling is 4b(4) (structurally impossible — ifOpenBmcIntegerRefusedcarried cause:OpenBmcRemoteJqRefusalinstead of reason:String, a cause-blind refusal has no constructor). A separate diff should carry the typed cause through and move the renderer to the presentation edge.Test plan
dag/test/claim/jq_invocation_lowering_witness_test.dag— 16/16 pass.dag/test/claim/remote_jq_ssh_migration_witness_test.dag— 12/12 pass (decode, remote word vector, exact RFC 4254 command string, stdin-collision refusal, Unknown-interpretation gate, Observed-arm fixture witness, review-fix pin).dag/test/claim/bmc/bmc_typed_operations_witness_test.dag— representative tests pass.claim_executor --required-regen --source-root dag --source-root src/v2→first_generation_equal=true.