Repository navigation
Conversation
…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).
…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 2 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.)
gunbai-bot
Bot
force-pushed
the
work-jq-10148
branch
from
September 3, 2026 13:36
14cb0fc to
86b506e
Compare
added 2 commits
September 3, 2026 16:56
…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.
…lue, FilePath, argjson authority, jq-owned executable
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 passes interpretation: Unknown, refusing with
RemoteExecInterpretationUnknown until a live target confirms.
Also fixed: the comment-in-function-body parse error (lines 1434-1435)
that caused the CI required-witnesses-floor failure — moved above the
function at the module-item grain.
Witness receipts: jq lowering 16/16, remote_jq SSH migration 12/12,
remote_shell_command 8/8 (witness_metacharacter_word_holds pending),
bmc_typed_operations representative tests pass. Whole-corpus regen
first_generation_equal=true, zero source-annotation errors.
Contributor
|
Closing as the duplicate vehicle. This change has had two PR numbers over one line of work: #10185 on work-jq-10148 and #10148 on session/snappy-lark-902. They have now DIVERGED -- this PR sits at 5d8474e while #10148 carries 7c7e71a, which adds the source-annotation grain fix on top of the same six-bar rework. The split already did measurable harm once: reviews landed on different vehicles, so this PR's readiness summary reported 3 approvals and zero request-changes while its twin carried an outstanding REQUEST_CHANGES on the identical commit, and that summary was very nearly used to justify a merge. #10148 is the survivor and carries the current head. Continuing work, reviews and CI belong there. Reopen if that turns out to be the wrong choice. |
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). The point of every change: a caller describes a semanticJqInvocationand the flags are derived — no caller spells-e,-r,--argjsonor an argv position.jq_invocation_lowernow lowersJqJsonBindingto--argjson <name> <value>(three argv words before the program operand) instead of refusing. The argv-spelledObjectMapperServiceAt/ObjectMapperServiceCountshell operations are deleted at the root; their callers route through semantic invocations and decodeJqOutcome. The placeholder refusal splits into typed causes.JqInputFilenow lowers to a file operand (JqFileInputLoweringUnwireddissolves on climb).OpenBmcStepwiseCountleaves its rawsshpass/sshargv for a semantic invocation + remote realization that emits the RFC 4254 command string with the grammar-owned single-quote encoding (remote_exec_command_string) — neverappend(ssh_prefix, inner.argv)— and refuses stdin-fed remote jq as a typed collision (sshpass -d 0holds fd 0).remote_exec_command_live_confirmationis declared Unexecuted — soopenbmc_remote_jq_executepassesUnknownand refuses with a typed cause until a live OpenBMC/Dropbear target confirms one (DESIGN §4b/§5: never fabricate an unobserved assumption). The pure emitter stays witnessable under an explicitly supplied interpretation.emptyfor an out-of-range index (absence, not a service named"null"); the no-oplist_appendtail and the""sentinel in the binding fold were removed.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 perturbation, production-gate refusals, 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.remote_exec_command_live_confirmationis observed against a live target.