Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
18 commits
Select commit Hold shift + click to select a range
81aaeac
Wave 1A, part 1: lower JqJsonBinding to --argjson name value in jq_in…
Sep 2, 2026
8c31e61
Wave 1A, part 2: migrate the ObjectMapper sensor-service projections …
Sep 3, 2026
707a65c
Record the Wave 1A cutover receipt in the CLI-invocation design note
Sep 3, 2026
7cb5de8
Wave 2, part 1: lower JqInputFile to a file operand in jq_invocation_…
Sep 3, 2026
a03f17d
Wave 2, part 2: first SSH migration -- OpenBmcStepwiseCount onto the …
Sep 3, 2026
01b84a0
Record the Wave 2 cutover receipt in the CLI-invocation design note
Sep 3, 2026
e675554
jq_option_arguments: drop the no-op list_append(_, right: Empty) tail
Sep 3, 2026
86b506e
jq_bindings_lower: record the seen binding name, not a fabricated "" …
Sep 3, 2026
f0ce1ea
Gate the remote-jq production cutover on the remote-shell interpretat…
Sep 3, 2026
316b4ce
Six-bar rework (review 59375 REQUEST_CHANGES): sealed carrier, JsonVa…
Sep 3, 2026
f78565e
Remote jq live confirmation: add pure interpretation function + Obser…
Sep 4, 2026
1df2d63
Remove cause-blind fan_config_stepwise_count_refuses_until_live_confi…
Sep 4, 2026
4f4f59a
Annotate the lossy refusal carrier at openbmc_fan_config_stepwise_count
Sep 4, 2026
20fca88
Fix annotation: attach to correct declaration, fix type name, drop da…
Sep 4, 2026
57d1488
Review 59745: typed interpretation in Observed confirmation; full §4b…
Sep 4, 2026
c6e5307
Revert the §4b(3) rung-drop block to a plain lossy-carrier annotation
Sep 4, 2026
dbdd816
Remove body comments in Observed-arm witness test (section 4c parse r…
Sep 4, 2026
4c1ced6
Merge origin/main into session/snappy-lark-902
Sep 4, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
463 changes: 372 additions & 91 deletions dag/extdeps/bmc/openbmc_fan_control.dag

Large diffs are not rendered by default.

3 changes: 1 addition & 2 deletions dag/extdeps/bmc/openbmc_operation.dag
Original file line number Diff line number Diff line change
Expand Up @@ -69,8 +69,7 @@ type OpenBmcOperation
| OpenBmcWaitSeconds { duration: Second }

type OpenBmcFanConfigQuery
= OpenBmcStepwiseCount
| OpenBmcMinimumDuty
= OpenBmcMinimumDuty
| OpenBmcZoneFailsafeDuty
| OpenBmcSensorFailsafeDuty
| OpenBmcPositiveHysteresis
Expand Down
40 changes: 20 additions & 20 deletions dag/extdeps/bmc/openbmc_password_ssh_transport.dag
Original file line number Diff line number Diff line change
Expand Up @@ -18,9 +18,28 @@ data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
// v2.lens.mandatory_tag.corpus_scan when native witness realization runs the parse-grain corpus
// witness.

data openbmc_password_ssh_transport_note: String = "Every transport operation has fixed argv selected by the closed OpenBmcOperation interpreter. There is no command-string or caller-authored argv input. SSH verifies the target-specific known-hosts file and password material stays on inherited fd 0."
data openbmc_password_ssh_transport_note: String = "Every transport operation has fixed argv selected by the closed OpenBmcOperation interpreter. The ONE command-string row, RunCommand, carries the RFC 4254 exec payload for the Wave 2 remote-jq migration: a typed NonEmptyStr produced one layer up by gunbc.remote_shell_command remote_exec_command_string -- never caller-authored argv -- and the operation's own sshpass/ssh argv stays fixed. The remote jq population was seventeen re-inlined sshpass/ssh argv prefixes; the first migrated site routes through the semantic jq layer (extdeps.tools.jq) and reaches RunCommand as ONE command string -- the SINGLE final word after the \"--\" separator, with sshpass feeding the password on fd 0 (-d 0). A stdin-fed remote jq refuses one layer up (openbmc_fan_control openbmc_remote_jq_execute): fd 0 is the password's channel here, so a remote stdin payload would collide with it. SSH verifies the target-specific known-hosts file and password material stays on inherited fd 0."

service openbmc.PasswordSshTransport {
operation RunCommand {
input { host: NonEmptyStr, username: NonEmptyStr, password: Secret, known_hosts_path: NonEmptyStr, command: NonEmptyStr }
output {
exit_code: Int from "exit_code"
success: Bool from "exit_success"
stdout: String from "stdout"
stderr: String from "stderr"
}
readonly
transport shell {
argv: ["sshpass", "-d", "0", "ssh", "-T", "-o", "PreferredAuthentications=password,keyboard-interactive", "-o", "PubkeyAuthentication=no", "-o", "StrictHostKeyChecking=yes", "-o", "UserKnownHostsFile={known_hosts_path}", "-o", "LogLevel=ERROR", "-o", "ConnectTimeout=10", "{username}@{host}", "--", "{command}"]
stdin: password
}
exit {
0 => Unit
nonzero => String "closed OpenBMC password-SSH operation failed"
}
}

operation ReadFile {
input { host: NonEmptyStr, username: NonEmptyStr, password: Secret, known_hosts_path: NonEmptyStr, path: NonEmptyStr }
output {
Expand Down Expand Up @@ -210,25 +229,6 @@ service openbmc.PasswordSshTransport {
}
}

operation FanStepwiseCount {
input { host: NonEmptyStr, username: NonEmptyStr, password: Secret, known_hosts_path: NonEmptyStr, config_path: NonEmptyStr }
output {
exit_code: Int from "exit_code"
success: Bool from "exit_success"
stdout: String from "stdout"
stderr: String from "stderr"
}
readonly
transport shell {
argv: ["sshpass", "-d", "0", "ssh", "-T", "-o", "PreferredAuthentications=password,keyboard-interactive", "-o", "PubkeyAuthentication=no", "-o", "StrictHostKeyChecking=yes", "-o", "UserKnownHostsFile={known_hosts_path}", "-o", "LogLevel=ERROR", "-o", "ConnectTimeout=10", "{username}@{host}", "--", "jq", "-er", "[.zones[].pids[] | select(.name == \"TEMP_SOC\" and .type == \"stepwise\")] | length", "{config_path}"]
stdin: password
}
exit {
0 => Unit
nonzero => String "closed OpenBMC password-SSH operation failed"
}
}

operation FanMinimumDuty {
input { host: NonEmptyStr, username: NonEmptyStr, password: Secret, known_hosts_path: NonEmptyStr, config_path: NonEmptyStr }
output {
Expand Down
4 changes: 3 additions & 1 deletion dag/extdeps/exec/command.dag
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ import gunbc.remote_shell_command {
RemoteExecCommandBuilt,
RemoteExecCommandRefused,
RemoteExecCommandRefusalCause,
remote_exec_command_rendered,
remote_exec_command_string,
}

Expand Down Expand Up @@ -181,7 +182,8 @@ fn command_over_transport(command: ArgvCommand, transport: CommandTransport) ->
SshExec { ssh_target: t, interpretation: interp } =>
match remote_exec_command_string(argv: map(argv_words(command: command), a => a as NonEmptyStr), interpretation: interp) {
RemoteExecCommandRefused { cause: c } => CommandOverTransportRefused { cause: c }
RemoteExecCommandBuilt { command: s } =>
RemoteExecCommandBuilt { command: sealed } =>
let s = remote_exec_command_rendered(command: sealed)
CommandOverTransportBuilt {
command: argv_command(
program: sshpass_binary_name,
Expand Down
202 changes: 176 additions & 26 deletions dag/extdeps/tools/jq.dag
Original file line number Diff line number Diff line change
Expand Up @@ -3,10 +3,11 @@ module extdeps.tools.jq
import std.occurrence_identity { OccurrenceSynthetic }
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.algebra { list_append, list_snoc_item, fold_list }
import v2.std.collection { Map, empty_map, map_insert, map_lookup }
import v2.std.text { string_join }
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.lexing { LexRuleSet, LiteralPattern, ModeledLexRules, TokenRule, symbol_intern_lexeme }
import v2.std.compilers.target_model { BoundToken, FixedToken }
import v2.std.diagnostic {
Diagnostic,
Expand All @@ -20,6 +21,8 @@ import v2.std.diagnostic {
}
import v2.std.node { Atom, Node, Symbol, TypeNode }
import v2.std.optional { Absent, Optional, Present }
import std.types { FilePath }
import extdeps.languages.json.emit { JsonValue, serialize_json }
import extdeps.external_authority { ExternalAuthority }
import extdeps.uri { Uri, Https }
import extdeps.shell.exec { ProcessObservation, process_observation }
Expand Down Expand Up @@ -123,14 +126,14 @@ type JqProgram { source: NonEmptyStr }
type JqBindingName { name: NonEmptyStr }

type JqBinding
= JqJsonBinding { name: JqBindingName, value: NonEmptyStr }
= JqJsonBinding { name: JqBindingName, value: JsonValue }
| 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 }
= JqInputFile { path: FilePath }
| JqInputStdin { content: String }

// -r writes STRING results raw; non-string results stay JSON-formatted. Hence JqRawOutput rather
Expand Down Expand Up @@ -162,6 +165,7 @@ type JqInvocation {
type JqCliOption
= JqCliOptionRawOutput
| JqCliOptionExitStatus
| JqCliOptionArgJson

// ABSENCE IS A DECLARED ROW, NOT A MISSING ONE. An earlier revision returned Optional<JqCliOption>
// and answered Absent for JqProgramExit -- which makes "this policy deliberately requires no
Expand Down Expand Up @@ -195,6 +199,7 @@ fn jq_option_token_class(option: JqCliOption) -> Symbol {
match option {
JqCliOptionRawOutput => ^jq_opt_raw_output
JqCliOptionExitStatus => ^jq_opt_exit_status
JqCliOptionArgJson => ^jq_opt_argjson
}
}

Expand All @@ -207,6 +212,7 @@ fn jq_option_long_name(option: JqCliOption) -> NonEmptyStr {
match option {
JqCliOptionRawOutput => "raw-output"
JqCliOptionExitStatus => "exit-status"
JqCliOptionArgJson => "argjson"
}
}

Expand All @@ -229,11 +235,20 @@ fn jq_cli_lex_rules() -> ModeledLexRules {
token_class: jq_option_token_class(option: JqCliOptionExitStatus),
pattern: LiteralPattern { text: jq_option_canonical_spelling(option: JqCliOptionExitStatus) }
},
TokenRule {
token_class: jq_option_token_class(option: JqCliOptionArgJson),
pattern: LiteralPattern { text: jq_option_canonical_spelling(option: JqCliOptionArgJson) }
},
]
}
}
}

// The executable identity that jq owns. Every consumer of a JqProcessPlan reads the executable
// from this row; no external module spells "jq" as a literal. The local handler (jq.Process) and
// the remote realization both derive from it.
data jq_executable: NonEmptyStr = "jq"

// 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.
Expand All @@ -249,32 +264,150 @@ type JqProcessPlan {
// 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
= JqBindingNameDuplicate
| JqTextBindingUnwired

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 }
// A binding's NAME and VALUE each need their own spelling-map key, and the keys must be
// INJECTIVE over (name, role) or one binding's value can be silently substituted for another's --
// the state-space collapse this lane exists to remove. Names are arbitrary NonEmptyStr, so no
// fixed separator is safe; instead each key carries a role prefix that cannot collide with any
// name (the prefixes are disjoint and no name can equal a prefixed key, because every prefixed
// key begins with a reserved dot-suffixed stem). Duplicate NAMES refuse separately, so two
// bindings never share a name-key either.
data jq_binding_name_key_prefix: String = "gunbc.jq.binding.name."
data jq_binding_value_key_prefix: String = "gunbc.jq.binding.value."

fn jq_binding_name_key(binding_name: String) -> Symbol {
symbol_intern_lexeme(lexeme: string_join(fields: [jq_binding_name_key_prefix, binding_name], separator: ""))
}

fn jq_binding_value_key(binding_name: String) -> Symbol {
symbol_intern_lexeme(lexeme: string_join(fields: [jq_binding_value_key_prefix, binding_name], separator: ""))
}

type JqBindingsResult
= JqBindingsLowered { arguments: List<CliArgumentSyntax>, spellings: Map<Symbol, String> }
| JqBindingsRefused { cause: JqLoweringRefusal }

// A JSON binding lowers to THREE consecutive argv words -- the option, the binding name, and the
// JSON value -- held as one group to enforce arity and order until final argv flattening.
type JqBindingArgumentGroup {
option_word: CliArgumentSyntax
name_word: CliArgumentSyntax
value_word: CliArgumentSyntax
}

fn jq_binding_group_argv(group: JqBindingArgumentGroup) -> List<CliArgumentSyntax> {
[group.option_word, group.name_word, group.value_word]
}

// THE BINDING FOLD. Each JqJsonBinding renders as THREE arguments -- the --argjson option, the
// binding name, the JSON value -- each its own argv word, inserted BEFORE the program operand
// (POSIX guideline 9: options precede operands). The three words are held as ONE JqBindingArgumentGroup
// to enforce arity and order until final argv flattening. A repeated name is refused, never handed
// to jq's last-wins behaviour. JqTextBinding has no live consumer this wave and refuses rather than
// emitting a plausible guess. DESIGN section 5: a failure arm must refuse, never widen.
//
// The `seen` map records every binding name already folded, keyed by the interned name; the VALUE
// is the name itself (a fabricated sentinel would be a second representation of presence -- the
// map is used as a presence set, but the value carries the real name, never a fake string).
//
// THE OPTION TOKEN IS SELECTED THROUGH THE AUTHORITY. The FixedToken carries
// jq_option_token_class(JqCliOptionArgJson), NOT a bare ^jq_opt_argjson literal -- the two-level
// derivation from semantic property to cited spelling owns the token, not a hand-spelled constant.
fn jq_bindings_lower(
bindings: List<JqBinding>,
seen: Map<Symbol, String>,
groups: List<JqBindingArgumentGroup>,
spellings: Map<Symbol, String>
) -> JqBindingsResult {
match bindings {
Empty =>
JqBindingsLowered {
arguments: fold_list(
xs: groups,
empty: Empty,
cons: fn(acc, g) { list_append(left: acc, right: jq_binding_group_argv(group: g)) }
),
spellings: spellings
}
Cons { head: binding, tail: rest } =>
match binding {
JqTextBinding { name: _, value: _ } =>
JqBindingsRefused { cause: JqTextBindingUnwired }
JqJsonBinding { name: JqBindingName { name: binding_name }, value: value } =>
match map_lookup(m: seen, key: symbol_intern_lexeme(lexeme: binding_name as String)) {
Present { value: _ } =>
JqBindingsRefused { cause: JqBindingNameDuplicate }
Absent =>
let name_key = jq_binding_name_key(binding_name: binding_name as String)
let value_key = jq_binding_value_key(binding_name: binding_name as String)
let new_group = JqBindingArgumentGroup {
option_word: CliArgumentSyntax {
fragments: [FixedToken { token_class: jq_option_token_class(option: JqCliOptionArgJson) }]
},
name_word: CliArgumentSyntax {
fragments: [BoundToken { token_class: ^jq_binding_name, binding: name_key }]
},
value_word: CliArgumentSyntax {
fragments: [BoundToken { token_class: ^jq_binding_value, binding: value_key }]
},
}
let new_spellings = map_insert(
m: map_insert(m: spellings, key: name_key, value: binding_name as String),
key: value_key,
value: serialize_json(v: value)
)
let new_seen = map_insert(m: seen, key: symbol_intern_lexeme(lexeme: binding_name as String), value: binding_name as String)
jq_bindings_lower(
bindings: rest,
seen: new_seen,
groups: list_append(left: groups, right: [new_group]),
spellings: new_spellings
)
}
}
}
}

// The lowering REFUSES the one axis this wave has no live consumer for (a text binding), rather
// than emitting a plausible guess. A JSON binding and a file input now lower. DESIGN section 5: a
// failure arm must refuse, never widen -- and never fabricate.
fn jq_invocation_lower(invocation: JqInvocation) -> JqLowering {
match jq_bindings_lower(bindings: invocation.bindings, seen: empty_map(), groups: Empty, spellings: empty_map()) {
JqBindingsRefused { cause: cause } =>
JqLoweringRefused { cause: cause }
JqBindingsLowered { arguments: binding_arguments, spellings: binding_spellings } =>
match invocation.input {
JqInputFile { path: _ } =>
JqLoweringRefused { cause: JqFileInputLoweringUnwired }
JqInputFile { path } =>
JqLowered {
plan: JqProcessPlan {
arguments: jq_file_input_arguments(
invocation: invocation,
binding_arguments: binding_arguments,
path: path
),
binding_spellings: map_insert(
m: map_insert(m: binding_spellings, key: ^jq_program_text, value: invocation.program.source as String),
key: ^jq_file_input_text,
value: path as String
),
process_input: JqProcessNoStdin
}
}
JqInputStdin { content: content } =>
JqLowered {
plan: JqProcessPlan {
arguments: jq_option_arguments(invocation: invocation),
arguments: jq_option_arguments(
invocation: invocation,
binding_arguments: binding_arguments
),
binding_spellings: map_insert(
m: empty_map(),
m: binding_spellings,
key: ^jq_program_text,
value: invocation.program.source as String
),
Expand All @@ -285,13 +418,30 @@ fn jq_invocation_lower(invocation: JqInvocation) -> JqLowering {
}
}

// THE FILE OPERAND. A file input is an ARGV OPERAND, not a process channel -- jq reads the named
// file itself, so the bytes travel on the filesystem, and the path lands AFTER the program
// operand (POSIX guideline 9: options precede operands; jq's program precedes its input file).
// The path is a bound word like the program, never an option and never caller-authored spelling.
fn jq_file_input_arguments(invocation: JqInvocation, binding_arguments: List<CliArgumentSyntax>, path: NonEmptyStr) -> List<CliArgumentSyntax> {
list_snoc_item(
xs: jq_option_arguments(invocation: invocation, binding_arguments: binding_arguments),
item: CliArgumentSyntax {
fragments: [BoundToken { token_class: ^jq_file_input_operand, binding: ^jq_file_input_text }]
}
)
}

// 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<CliArgumentSyntax> {
// puts options before operands, and jq does not deviate. Bindings are options (each is an
// --argjson triplet), so they sit with the options, ahead of the program operand.
fn jq_option_arguments(invocation: JqInvocation, binding_arguments: List<CliArgumentSyntax>) -> List<CliArgumentSyntax> {
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))
left: 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))
),
right: binding_arguments
),
item: CliArgumentSyntax {
fragments: [BoundToken { token_class: ^jq_program_operand, binding: ^jq_program_text }]
Expand Down Expand Up @@ -437,8 +587,8 @@ fn jq_invocation_cli_arguments(invocation: JqInvocation) -> Outcome<CliSurface>

fn jq_lowering_refusal_identity(cause: JqLoweringRefusal) -> Symbol {
match cause {
JqBindingLoweringUnwired => ^jq_binding_lowering_unwired
JqFileInputLoweringUnwired => ^jq_file_input_lowering_unwired
JqBindingNameDuplicate => ^jq_binding_name_duplicate
JqTextBindingUnwired => ^jq_text_binding_unwired
}
}

Expand Down
Loading
Loading