diff --git a/dag/extdeps/bmc/ipmi_boot_selection.dag b/dag/extdeps/bmc/ipmi_boot_selection.dag new file mode 100644 index 00000000000..93daffe429d --- /dev/null +++ b/dag/extdeps/bmc/ipmi_boot_selection.dag @@ -0,0 +1,147 @@ +module extdeps.bmc.ipmi_boot_selection + +import std.types { Bool, NonEmptyStr, String } +import extdeps.external_authority { ExternalAuthority } +import extdeps.uri { Uri, Https } +import extdeps.toolchain.types { Architecture, Aarch64 } + +// THE CLI SURFACE IS ipmitool's BOOT-FLAG ENCODER, not the IPMI wire itself. The IPMI 2.0 +// chassis boot parameter has separate valid, persistence and boot-type bits; ipmitool exposes +// them through the final `options=...` argv word. The exact implementation authority is the +// upstream source whose option table names `valid`, `persistent` and `efiboot` and whose +// set-bootdev path sets the valid bit before writing parameter 5. +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "github.com/ipmitool/ipmitool/blob/master/lib/ipmi_chassis.c" + } +} + +type IpmiBootDevice + = IpmiBootPxe + | IpmiBootCdrom + +type IpmiFirmwareBootMode + = IpmiBootLegacy + | IpmiBootEfi + +type IpmiBootPersistence + = IpmiBootOnce + | IpmiBootPersistent + +// A VALID BOOT SELECTION, NOT THREE INDEPENDENT SCALARS. This record is sole_constructor so a +// caller cannot place Aarch64 beside Legacy or manufacture an opaque options word. The only +// constructor currently exported is aarch64_uefi_once_boot_selection: its signature has no mode +// or persistence parameter, hence `(Aarch64, Legacy, Cdrom)` and persistent intake overrides +// have no source spelling at all. A future x86 legacy requirement adds a different constructor +// here; it does not widen this one with a Boolean or raw-string escape hatch. +// +// The wire and read-back spellings travel with the semantic axes because they are one CLI +// serialization. A caller selects `IpmiBootCdrom`; it never authors `cdrom`, +// `options=efiboot`, or one of the four strings used to adjudicate parameter 5. +type IpmiBootSelection sole_constructor { + architecture: Architecture + device: IpmiBootDevice + firmware_mode: IpmiFirmwareBootMode + persistence: IpmiBootPersistence + device_wire: NonEmptyStr + options_wire: NonEmptyStr + expected_flag_rendering: NonEmptyStr + expected_device_rendering: NonEmptyStr + expected_mode_rendering: NonEmptyStr + expected_persistence_rendering: NonEmptyStr +} + +fn aarch64_uefi_once_boot_selection(device: IpmiBootDevice) -> IpmiBootSelection { + match device { + IpmiBootPxe => IpmiBootSelection { + architecture: Aarch64, + device: IpmiBootPxe, + firmware_mode: IpmiBootEfi, + persistence: IpmiBootOnce, + device_wire: "pxe", + options_wire: "options=efiboot", + expected_flag_rendering: "Boot Flag Valid", + expected_device_rendering: "Force PXE", + expected_mode_rendering: "BIOS EFI boot", + expected_persistence_rendering: "Options apply to only next boot", + } + IpmiBootCdrom => IpmiBootSelection { + architecture: Aarch64, + device: IpmiBootCdrom, + firmware_mode: IpmiBootEfi, + persistence: IpmiBootOnce, + device_wire: "cdrom", + options_wire: "options=efiboot", + expected_flag_rendering: "Boot Flag Valid", + expected_device_rendering: "Force Boot from CD/DVD", + expected_mode_rendering: "BIOS EFI boot", + expected_persistence_rendering: "Options apply to only next boot", + } + } +} + +fn ipmi_boot_device_label(device: IpmiBootDevice) -> NonEmptyStr { + match device { + IpmiBootPxe => "pxe" + IpmiBootCdrom => "cdrom" + } +} + +fn ipmi_boot_mode_label(mode: IpmiFirmwareBootMode) -> NonEmptyStr { + match mode { + IpmiBootLegacy => "legacy" + IpmiBootEfi => "efi" + } +} + +fn ipmi_boot_persistence_label(persistence: IpmiBootPersistence) -> NonEmptyStr { + match persistence { + IpmiBootOnce => "once" + IpmiBootPersistent => "persistent" + } +} + +fn ipmi_boot_selection_label(selection: IpmiBootSelection) -> NonEmptyStr { + join([ + ipmi_boot_device_label(device: selection.device) as String, + "/", + ipmi_boot_mode_label(mode: selection.firmware_mode) as String, + "/", + ipmi_boot_persistence_label(persistence: selection.persistence) as String, + ], "") as NonEmptyStr +} + +// ONE ARGV WORD PER UPSTREAM CONCEPT. No `sh -c`, no joined command, and no caller-supplied +// `options=` string. ipmitool receives the secret by -f exactly as extdeps.bmc.ipmi does; the +// boot selection is projected from the sole-constructor record above. +service diagnostic.ipmi.BootSelection { + operation Set { + input { + bmc_host: NonEmptyStr + username: NonEmptyStr + password_file: NonEmptyStr + selection: IpmiBootSelection + } + output { + stdout: String from "stdout" + success: Bool from "exit_success" + } + transport shell { + argv: [ + "ipmitool", + "-H", "{bmc_host}", + "-I", "lanplus", + "-U", "{username}", + "-f", "{password_file}", + "chassis", "bootdev", + selection.device_wire, + selection.options_wire + ] + } + exit { + 0 => Unit + nonzero => String "ipmitool typed boot selection failed" + } + } +} diff --git a/dag/gunbc/host/host_reset_return_run.dag b/dag/gunbc/host/host_reset_return_run.dag index 2476ad6ab95..e3d1469c272 100644 --- a/dag/gunbc/host/host_reset_return_run.dag +++ b/dag/gunbc/host/host_reset_return_run.dag @@ -20,6 +20,7 @@ import gunbc.hostname_allocation { canonical_hostname_for_fleet_slot } import extdeps.github.actions_environment { github_run_id_variable_name } import gunbc.actions_run_binding { ActionsVariableAbsent, ActionsVariablePresent, actions_variable_read } import product.placement_supply { HostIdentity } +import extdeps.bmc.ipmi_boot_selection { ipmi_boot_selection_label } import gunbc.host_reset_return { AttemptReceiptMinted, AttemptReceiptPairingRefused, @@ -74,35 +75,23 @@ import gunbc.host_reset_return { } import gunbc.host_reset_subject_roster { ResetSubjectCandidate, reset_observer_peer_roster, reset_subject_candidate_for, reset_subject_roster } import gunbc.machine_intake_oob_boot_handoff { - oob_boot_handoff, - BootHandoffCompleted, - BootHandoffNotAdmitted, + oob_boot_control_issue, + BootControlIssued, + BootControlNotAdmitted, + BootSelectionFirmwareModeMismatch, BootSelectionFlagInvalid, BootSelectionNotApplied, + BootSelectionPersistenceMismatch, BootSelectionRefused, BootSelectionUnverifiable, - OobBootHandoffOutcome, + OobBootControlOutcome, PowerCycleRefused, } -// THE OBSERVER'S SIDE OF ONE RESET ATTEMPT, EXECUTED. Every fold in gunbc.host_reset_return is pure -// and is exercised by its witness against fixtures, which is what a fold is owed. This module is -// what a fold is not owed and a RECEIPT is: the instruments that produce the observation, run from a -// machine that is not the subject. -// -// WHAT IS DELIBERATELY NOT HERE. This module does not issue the reset. Issuing it is -// gunbc.machine_intake_oob_boot_handoff's operation and it is already modeled, already admitted from -// a capability row, and already refuses before any write; a second issuer here would be the §3 fork -// that module's own note warns about. This is the OBSERVER, and keeping the two apart is not tidiness -// -- the observer must be able to run on a machine that holds no controller credential at all. +// THE OBSERVER'S SIDE OF ONE RESET ATTEMPT, EXECUTED. The controller operation only issues the +// typed control request; this module independently observes the host go down and return. Neither +// fact substitutes for the other. -// ── the liveness instrument ──────────────────────────────────────────────────────────────────── - -// ONE PROBE, NAMED, SO THE RECEIPT SAYS WHAT IT WATCHED. ssh.Session.Reachability is an ssh channel -// request with BatchMode and a five-second connect timeout: it answers "this machine completed an -// ssh handshake", which is a considerably stronger statement than a ping and the right one here, -// because a host that answers ICMP from its firmware has not returned in any sense a runner cares -// about. data host_reset_return_probe_label: NonEmptyStr = "ssh.Session.Reachability, BatchMode, ConnectTimeout=5" func host_is_reachable(host: NonEmptyStr) -> Bool @@ -111,15 +100,6 @@ func host_is_reachable(host: NonEmptyStr) -> Bool return ssh.Session.Reachability(host: host).reachable } -// ── the two waits ────────────────────────────────────────────────────────────────────────────── - -// A BOUNDED FOLD RATHER THAN A LOOP UNTIL TRUE, and the bound is the whole safety property: a wait -// that cannot end is a job that hangs until the platform kills it, and a killed job writes nothing, -// which is once again the empty value that reads as a positive answer. -// -// THE SHAPE IS THE CORPUS'S, NOT THIS MODULE'S. gunbc.instruments.fabric_seat_probe wait_until_epoch -// already paces a bounded wait as a fold over nat_range_inclusive with one-second sleeps between -// clock reads; this is that idiom applied to a different predicate. type LivenessWatch = WatchSaw { at: EpochMs, samples: Int } | WatchTimedOut { samples: Int, watched_until: EpochMs } @@ -131,9 +111,6 @@ type WatchFold { last_seen_at: EpochMs } -// WAITING FOR A STATE, NOT FOR A CHANGE. `want_reachable: false` is the down watch and `true` is the -// back watch, so one fold serves both and the two waits cannot drift apart in their pacing, their -// bound or their clock discipline. func watch_step(acc: WatchFold, want_reachable: Bool, host: NonEmptyStr) -> WatchFold uses net: std.resources.Network { @@ -176,12 +153,8 @@ func watch_for(host: NonEmptyStr, want_reachable: Bool, max_samples: Nat) -> Liv } } -// ── the observation, assembled from the two watches ──────────────────────────────────────────── - -// THE DOWN WATCH RUNS FIRST AND THE BACK WATCH IS REACHABLE ONLY THROUGH ITS SUCCESS ARM. That is -// the ordering made structural rather than sequential: there is no path on which a return is -// observed without a departure having been observed first, so "down then up" cannot degenerate into -// "up", which is what a host that never rebooted would answer. +// THE DOWN WATCH RUNS FIRST. A return observation is reachable only after a departure observation, +// so an already-up host cannot be reported as having rebooted. func observe_reset_return(host: NonEmptyStr, down_samples_max: Nat, back_samples_max: Nat) -> HostReturnObservation uses net: std.resources.Network { @@ -216,24 +189,8 @@ func observe_reset_return(host: NonEmptyStr, down_samples_max: Nat, back_samples } } -// ── the observer's self-corroboration ────────────────────────────────────────────────────────── - -// THE OBSERVER READS ITS OWN HOSTNAME AND COMPARES IT TO THE SUBJECT'S ALLOCATED ONE. Two -// instruments with nothing in common: the runner label decides where the job ran, the machine's own -// hostname says what it is, and the allocation roster says what the subject's would be. A runner -// mislabeled onto the subject chassis passes the first and fails this. -// -// AN UNALLOCATED SUBJECT MAKES THE CHECK UNPERFORMABLE, AND UNPERFORMABLE REFUSES. Nothing here -// invents a hostname to clear that refusal: a canonical hostname is an ALLOCATION, and a guessed one -// would be a fabricated observation standing exactly where the check that catches fabrication runs, -// so the guess would disarm the instrument it was feeding. -// -// THE ALLOCATION EXISTS, AND THIS COMMENT USED TO SAY IT DID NOT. An earlier version said -// gunbc_fleet_hostname_allocations carried no Mt. Collins row and that the first attempt would refuse -// here; that row is now authored in gunbc.hostname_allocation, so the arm is no longer what the first -// attempt hits. Review 61747 caught the stale claim -- the same "a comment asserts a refusal that does -// not happen" class this branch had already been caught by once, which is the argument for reading -// every sentence that names a state as a claim to be re-measured rather than as description. +// The runner label, the observer's own hostname, and the allocation roster are independent reads. +// A mislabeled runner on the subject chassis cannot pass by merely differing in one spelling. func observer_self_corroboration(observer: HostIdentity, subject: HostIdentity) -> ObserverSelfIdentity uses net: std.resources.Network { @@ -276,12 +233,7 @@ func observer_self_corroboration(observer: HostIdentity, subject: HostIdentity) } } -// ── the attempt, end to end ──────────────────────────────────────────────────────────────────── - -// THE BASELINE, TAKEN BEFORE ANY WRITE. A host already unreachable when the reset is issued would -// satisfy the down watch instantly, and the whole reading would be a fabrication of a reset that -// moved nothing. So reachability is established first, and a subject that was not up refuses on its -// own arm rather than proceeding into a watch whose answer is already decided. +// A subject already unreachable before issuance cannot prove that this attempt moved it down. func subject_baseline(host: NonEmptyStr) -> HostReturnObservation? uses net: std.resources.Network { @@ -301,70 +253,49 @@ func subject_baseline(host: NonEmptyStr) -> HostReturnObservation? } } -// THE ACKNOWLEDGEMENT IS THE HANDOFF'S OUTCOME, TRANSLATED AND NOT FLATTENED. Each refusal arm of -// gunbc.machine_intake_oob_boot_handoff leaves the controller in a materially different state, so -// each becomes its own diagnostic rather than one "reset failed" -- the same reason that module -// keeps them apart in the first place. -fn acknowledgement_of_handoff(outcome: OobBootHandoffOutcome, issued_at: EpochMs) -> ResetCommandAcknowledgement { +// THE ACKNOWLEDGEMENT IS CONTROL-PLANE GRAIN. BootControlIssued means the complete typed parameter +// read back and the power command was accepted; it does not claim an artifact booted. The independent +// down/back observation below supplies this workflow's terminal reset property. +fn acknowledgement_of_boot_control(outcome: OobBootControlOutcome, issued_at: EpochMs) -> ResetCommandAcknowledgement { match outcome { - BootHandoffCompleted { selected: d } => + BootControlIssued { selection: s } => ResetAccepted { - controller_response: join(["boot source override verified for '", d as String, "' and the power action was accepted"], "") as NonEmptyStr, + controller_response: join(["typed boot control ", ipmi_boot_selection_label(selection: s) as String, " read back and the power action was accepted"], "") as NonEmptyStr, issued_at: issued_at, } - BootSelectionRefused => - ResetRefusedByController { diagnostic: "the controller refused the boot source override; nothing was cycled" } - BootSelectionNotApplied { requested: d, readback: r } => + BootSelectionRefused { selection: s } => + ResetRefusedByController { diagnostic: join(["controller refused typed boot selection ", ipmi_boot_selection_label(selection: s) as String, "; nothing was cycled"], "") as NonEmptyStr } + BootSelectionNotApplied { selection: s, readback: r } => + ResetRefusedByController { + diagnostic: join(["device selector disagreed with ", ipmi_boot_selection_label(selection: s) as String, "; parameter 5: ", r], "") as NonEmptyStr, + } + BootSelectionFirmwareModeMismatch { selection: s, readback: r } => + ResetRefusedByController { + diagnostic: join(["firmware mode disagreed with ", ipmi_boot_selection_label(selection: s) as String, "; parameter 5: ", r], "") as NonEmptyStr, + } + BootSelectionPersistenceMismatch { selection: s, readback: r } => ResetRefusedByController { - diagnostic: join(["the override for '", d as String, "' did not take; boot parameter 5 read back: ", r], "") as NonEmptyStr, + diagnostic: join(["persistence disagreed with ", ipmi_boot_selection_label(selection: s) as String, "; parameter 5: ", r], "") as NonEmptyStr, } - BootSelectionFlagInvalid { requested: d, readback: r } => + BootSelectionFlagInvalid { selection: s, readback: r } => ResetRefusedByController { - diagnostic: join(["the override for '", d as String, "' was reported alongside an INVALID boot flag, so it will not be honoured; read back: ", r], "") as NonEmptyStr, + diagnostic: join(["boot flag invalid for ", ipmi_boot_selection_label(selection: s) as String, "; parameter 5: ", r], "") as NonEmptyStr, } - BootSelectionUnverifiable { requested: d, readback: r } => + BootSelectionUnverifiable { selection: s, readback: r } => ResetRefusedByController { - diagnostic: join(["boot parameter 5 did not read back, so the override for '", d as String, "' is unverified; output: ", r], "") as NonEmptyStr, + diagnostic: join(["parameter 5 unreadable for ", ipmi_boot_selection_label(selection: s) as String, "; output: ", r], "") as NonEmptyStr, } - PowerCycleRefused { selected: d } => + PowerCycleRefused { selection: s } => ResetRefusedByController { - diagnostic: join(["the override for '", d as String, "' APPLIED but the power cycle was refused; the controller holds an unconsumed next-boot override"], "") as NonEmptyStr, + diagnostic: join(["typed selection applied but power cycle refused for ", ipmi_boot_selection_label(selection: s) as String], "") as NonEmptyStr, } - BootHandoffNotAdmitted { admission: _ } => + BootControlNotAdmitted { admission: _ } => ResetNotAttempted { cause: "the controller was not admitted for out-of-band drive; no write was attempted" } } } -// THE SAMPLE CADENCE IS A MEASURED DURATION, NOT A STRING. This paced the watch with -// sleep.Delay.Seconds(seconds: "1") until review 61938, which is a flat scalar naming a domain unit -// where std.measure already carries one -- and extdeps.tools.sleep does not merely offer the carrier, -// it declares the flat-scalar form's own dissolution binding onto -// sleep_delay_seconds_second_carrier_projection. Minting the duration again as a bare string was -// therefore re-inventing a concept that already has an authority (DESIGN sections 2 and 3), on the -// exact line the upstream module had marked for retirement. -// -// IT IS ALSO WHAT MAKES THE WATCH BOUNDS MEAN ANYTHING. The sample counts below are derived from the -// step budget by multiplying by this cadence; with the cadence spelled as a string at the call site, -// that arithmetic was carried in prose and nothing tied the two together. data host_reset_watch_sample_cadence: Second = second(count: 1) - -// HOW LONG THE OBSERVER WATCHES, in samples rather than in seconds, because a sample is what the -// fold actually counts and a seconds figure would be a second unit for the same bound. The receipt -// carries the OBSERVED instants and never a budget, so these numbers bound the watch and describe -// nothing about the outage. -// -// THE TWO BOUNDS ARE NOT THE SAME NUMBER BECAUSE A SAMPLE COSTS DIFFERENT AMOUNTS ON EACH SIDE, and -// the first draft picked round figures without noticing. While waiting for the host to go DOWN the -// probe SUCCEEDS, returning immediately, so a sample is about the one-second sleep. While waiting for -// it to come BACK the probe FAILS, and ssh.Session.Reachability carries ConnectTimeout=5, so a sample -// is about six seconds. Six hundred back-samples is therefore an hour of wall time inside a step -// whose budget is gunbc_ci_runner_guest_image_step_timeout_minutes -- a watch that the platform would -// kill before the fold could return, and a killed job writes nothing, which is once again the empty -// value that reads as a positive answer. The bound is derived from the step budget rather than -// chosen: two hundred samples is about twenty minutes, inside a thirty-minute step with margin for -// the prelude and the issuance. data host_reset_down_watch_samples: Nat = 120 - data host_reset_back_watch_samples: Nat = 200 func host_reset_return_attempt( @@ -447,16 +378,15 @@ func host_reset_return_issue_and_watch( ) -> ResetAttemptMint uses net: std.resources.Network { - let outcome = oob_boot_handoff( + let outcome = oob_boot_control_issue( observation: candidate.observation, capability_row: candidate.capability_row, username: candidate.username, password_file: password_file, - device: candidate.boot_device, - expected_rendering: candidate.boot_readback_rendering, + selection: candidate.boot_selection, power_action: candidate.power_action, ) - let ack = acknowledgement_of_handoff(outcome: outcome, issued_at: issued_at) + let ack = acknowledgement_of_boot_control(outcome: outcome, issued_at: issued_at) let observation = observe_reset_return( host: candidate.host as NonEmptyStr, down_samples_max: host_reset_down_watch_samples, @@ -472,40 +402,8 @@ func host_reset_return_issue_and_watch( ) } -// ── the entry the converge workflow invokes ──────────────────────────────────────────────────── - -// ZERO ARGUMENTS, AND THE SUBJECT IS NOT AN INPUT. The dispatch names the OBSERVER; this entry reads -// that label, looks it up in the assignment, and takes the subject the assignment gives it. There is -// no parameter, environment row or dispatch field through which anyone can name a subject, so no -// operator and no later edit can point this run at a chosen machine. -// -// AND IT DOES NOT DERIVE THE LABEL FROM ITS OWN HOSTNAME, which an earlier version did. That made the -// label and the machine one reading and quietly disarmed the corroboration between them: a runner -// labelled as a peer but living on the subject chassis failed the assignment lookup as "not an -// assigned observer" and never reached the identity check the hardware depends on. -// THE CREDENTIAL PATH COMES FROM ONE ROW THAT THE WRITER AND THE READER BOTH CONSULT, which is the -// shape gunbc.spark.grant_privileged_operation spark_grant_credential_path_env already establishes for -// exactly this problem: the converge prelude materializes a 0600 file under RUNNER_TEMP and exports -// its PATH -- never the credential -- and the entry reads the path from the same named row. An -// argument would have been a second authority on where the file is, and the prelude is the only party -// that actually knows. -// -// AND extdeps.shell IS IMPORTED FOR A MEASURED REASON. Service operations register from the IMPORT -// CLOSURE, so an unimported service compiles clean and refuses at RUN TIME naming the operation -// rather than the missing import; gunbc.machine_intake_mtcollins1_actuate lost a run to exactly that -// diagnostic and wrote it down. data host_reset_bmc_credential_path_env: NonEmptyStr = "GUNBC_HOST_RESET_BMC_CREDENTIAL_FILE" as NonEmptyStr -// THE PREFLIGHT REFUSAL WRITES ITS RECEIPT AND THEN EXITS, in that order, because the upload step -// that carries the evidence off the runner runs `if: always()` and errors when the file is absent. -// Before review 62016 these arms exited straight away, so the file the upload demanded never existed -// and the run's final red named the missing artifact instead of the missing credential -- the located -// diagnostic displaced by plumbing, on every refusal the mode can actually reach today. -// -// attempt=none-minted IS THE HONEST FIELD, not a placeholder. These refusals happen before a pairing -// exists, so there is no attempt label and no subject to name; writing "unknown" into those fields -// would be the fabricated-plausible-output shape, and a reader sorting receipts by subject would find -// a row claiming one. The line says which vocabulary answered it so the two are never confused. func host_reset_return_preflight_exit(refusal: ResetPreflightRefusal, remedy: String) -> ProcessExit uses net: std.resources.Network { @@ -519,23 +417,6 @@ func host_reset_return_preflight_exit(refusal: ResetPreflightRefusal, remedy: St ) } -// THE DISPATCH ADMISSION ENTRY, RUN IN THE BUILD JOB RATHER THAN THE RESET JOB. The reset job's -// runs-on is resolved before any of its steps exist, so a gate inside it is unreachable in exactly -// the state it would diagnose; `build` carries generic labels, is always schedulable, and every -// host-scoped job needs it, so refusing here stops the line before anything is scheduled. -// -// IT WAS A HAND-SHELL STEP FIRST, AND THAT WAS THE DEFECT. A concat-built `run:` gate carried a -// net-new dissolution obligation with no operator verdict, which the scaffold-admission doctrine -// calls a hard reject -- and the doctrine's own test applies: the modeled route existed, so the -// scaffold bought nothing but authoring, review, maintenance, deletion and review of the deletion. -// The only cost of doing it modeled is that the refusal lands after the release build rather than -// before it, wasting one build on a dispatch that was already wrong; the safety property is -// identical, because the reset job needs `build` either way. -// -// IT REFUSES WITH A CAUSE RATHER THAN SKIPPING. A gate that silently declines to run reads as a pass -// to anyone looking at the job list, which is the absorbing fallback one layer up from the one this -// module refuses -- so the not-this-mode arm exits SUCCESSFULLY and says so, and the unnamed-observer -// arm exits non-zero with the located diagnostic. func host_reset_return_dispatch_admission_wet() -> ProcessExit uses net: std.resources.Network { @@ -579,7 +460,7 @@ func host_reset_return_wet() -> ProcessExit if observer_raw == "" { return host_reset_return_preflight_exit( refusal: ObserverLabelUnset { variable: host_reset_observer_label_env }, - remedy: "this run does not know which observer the dispatch placed it as, and it deliberately does NOT fall back to its own hostname: that would make the label and the machine one reading, and the corroboration between them is the only thing standing between a mislabelled runner and a host resetting itself", + remedy: "this run does not know which observer the dispatch placed it as, and it deliberately does NOT fall back to its own hostname", ) } let observer = observer_raw as NonEmptyStr @@ -587,7 +468,7 @@ func host_reset_return_wet() -> ProcessExit RouteUnidentified { variable: v, detail: d } => return host_reset_return_preflight_exit( refusal: IssuingRunUnidentified { variable: v, detail: d }, - remedy: "a receipt minted here could not name the run that drove the machine, and this mode's whole claim is that the reset was unattended and went through converge, which a receipt no reader can trace back to its run does not establish", + remedy: "a receipt minted here could not name the run that drove the machine", ) RouteEstablished { route: r } => r } @@ -626,26 +507,6 @@ func host_reset_return_wet() -> ProcessExit } } -// THE ROUTE THIS ENTRY DECLARES ABOUT ITSELF. It is reachable only from the fleet converge workflow's -// reset job, so IssuedThroughConverge is a statement about where the code runs and not a claim the -// caller supplies -- there is no parameter here through which a hand invocation could describe itself -// as converge-driven, and the verdict refuses the out-of-band arm outright. -// -// THE RUN ID IS READ, AND A SENTENCE IN THAT FIELD WAS THE DEFECT REVIEW 61998 FOUND. It carried -// "unbound: the run identifier is not read by this entry ...", so every real receipt this mode would -// ever mint carried prose in a field whose type says it names the run that issued a power cycle -- -// section 4c's misplaced data, in the one field a reader needs to go find the evidence. The -// annotation defending it argued only against an INTERPOLATION-SHAPED LITERAL, which was never the -// choice on offer: extdeps.github.actions_environment github_run_id_variable_name already models the -// reading, gunbc.actions_run_binding actions_variable_read already performs it with an absent-versus- -// empty distinction, and this step already proves the env route works because it hands the observer -// label over the same way. -// -// AN UNIDENTIFIED RUN REFUSES RATHER THAN ISSUING. The alternative -- an optional field -- would let -// the reset proceed and mint a receipt that cannot say which run drove the machine, and "unattended, -// through converge" is precisely the claim this carrier exists to establish. A receipt nobody can -// trace back to its run does not establish it, so the honest arm is to refuse before the controller -// write rather than to record the gap afterwards. func host_reset_return_converge_route_read() -> ResetIssuanceRouteRead uses net: std.resources.Network { @@ -667,17 +528,6 @@ fn host_reset_return_attempt_label(observer: NonEmptyStr, subject: NonEmptyStr) join([subject as String, "-observed-by-", observer as String], "") as NonEmptyStr } -// THE EXIT IS THE VERDICT, RENDERED. Every refusal arm gets its own sentence because they leave the -// world in materially different states and a caller retrying needs to know which -- a controller that -// refused wrote nothing, a host that did not return is still down, and an observer that could not -// establish its own identity did not look at all. -// THE ATTEMPT LABEL MOVED FROM THE FILENAME INTO THE LINE, which is where it was always doing its -// work. It identifies which attempt this transcript belongs to; it was never the thing that kept two -// attempts apart on disk, because two attempts are two dispatches with two workspaces. -// -// THE MEASURED FIGURE IS WRITTEN ONLY ON THE ARM THAT MEASURED IT. A refusal line names its cause and -// carries no number at all, rather than a zero standing in for one -- zero sorts to the top of any -// ranking of outage times, which makes it the fabrication nobody finds by reading a list. fn host_reset_return_receipt_line(verdict: ResetReturnVerdict, subject: NonEmptyStr, attempt: NonEmptyStr) -> String { match verdict { HostDrivenBackToKnownState { downtime: ms } => diff --git a/dag/gunbc/host/host_reset_subject_roster.dag b/dag/gunbc/host/host_reset_subject_roster.dag index 7ebd66d62db..1f8150cccfd 100644 --- a/dag/gunbc/host/host_reset_subject_roster.dag +++ b/dag/gunbc/host/host_reset_subject_roster.dag @@ -4,6 +4,7 @@ import std.types { Bool, List, NonEmptyStr, String } import product.placement_supply { HostIdentity } import extdeps.bmc.access_profile { BmcAccessObservation } import extdeps.bmc.capability { BmcFirmwareReleaseCapabilityRow } +import extdeps.bmc.ipmi_boot_selection { IpmiBootSelection } import gunbc.machine_intake_oob_boot_handoff { OobBootHandoffAdmission, oob_boot_handoff_admission, @@ -15,59 +16,30 @@ import gunbc.machine_intake_mtcollins1_access_observation { } import gunbc.machine_intake_mtcollins1_actuate { mtcollins1_bmc_username, - mtcollins1_cdrom_device, - mtcollins1_cdrom_readback_rendering, + mtcollins1_cdrom_selection, mtcollins1_power_action, } import gunbc.fleet_intent_network { operator_host_mtcollins1 } import gunbc.fleet_runner_connectivity { fleet_hosts } -// WHICH HOSTS THIS FLEET MAY DRIVE BACK TO A KNOWN STATE THROUGH THEIR CONTROLLERS, and it is a -// DERIVED SUBSET rather than a list anyone maintains. +// WHICH HOSTS THIS FLEET MAY DRIVE BACK TO A KNOWN STATE THROUGH THEIR CONTROLLERS. Membership is +// derived from the same admission fold the control issuer runs, so the roster cannot authorize a +// controller the operation itself refuses. // -// "MAY HAVE ITS POWER DRIVEN OUT OF BAND" IS NOT "IS AN EXECUTOR FLEET HOST", and conflating the two -// is the §3 meaning fork this module exists to avoid. gunbc.fleet_runner_connectivity fleet_hosts() -// means "commits runner slots" -- its consumers fold it as an eligible host set and to gather -// committed slot identities -- so a host reachable only through its BMC does not belong in it, and a -// host with runner slots is not thereby drivable out of band. Two predicates, two rosters, one -// naming authority underneath both: every identity here comes from gunbc.fleet_intent_network. -// -// MEMBERSHIP IS AN IDENTITY JOIN AGAINST THE ADMISSION THE ACTUATION ARM ALREADY PERFORMS. A host is -// a reset subject exactly when oob_boot_handoff_admission -- the same fold -// gunbc.machine_intake_oob_boot_handoff runs before it writes anything to a controller -- admits its -// observation against its capability row. So the roster cannot drift from the capability it claims -// to describe: the evidence that authorizes the act is the evidence that produces the membership, -// and there is no second place to edit. -// THE PER-HOST RESET POLICY TRAVELS WITH THE ROSTER ROW, and that is the layer it belongs to rather -// than an accident of convenience. gunbc.machine_intake_oob_boot_handoff takes the boot device, the -// expected read-back rendering and the power action as PARAMETERS precisely because which of them a -// workflow picks is business policy, and its own note says so; this roster is the workflow-layer -// authority that picks them for a reset. -// -// THE VALUES ARE IMPORTED, NEVER RE-SPELLED. gunbc.machine_intake_mtcollins1_actuate already carries -// them as measured rows -- the device word, the exact text ipmitool renders for it, the cycle verb -// the unit's own SEL confirmed takes effect, and the administrator account measured as the only -// enabled one on the channel. Copying any of them here would be a §3 fork of a MEASUREMENT, which is -// the worst kind: the copy keeps reading correct long after the unit stops agreeing with it. +// THE BOOT POLICY TRAVELS AS ONE TYPED SELECTION. The prior row carried a device string and a +// read-back substring independently, while firmware mode and persistence were absent. That let a +// caller request `cdrom`, accept the matching selector, and silently leave parameter 5 in legacy +// mode. IpmiBootSelection is sole-constructor; this roster can neither forge its wire words nor +// pair Aarch64 with legacy mode. type ResetSubjectCandidate { host: HostIdentity observation: BmcAccessObservation capability_row: BmcFirmwareReleaseCapabilityRow username: NonEmptyStr - boot_device: NonEmptyStr - boot_readback_rendering: NonEmptyStr + boot_selection: IpmiBootSelection power_action: NonEmptyStr } -// THE CANDIDATE SET IS EVERY HOST THAT HAS LANDED THE EVIDENCE, ADMITTED OR NOT. It is stated as -// candidates rather than as members so that the admission fold below has something to refuse: a -// roster assembled from already-admitted hosts would make its own filter unreachable. -// -// THERE IS EXACTLY ONE TODAY AND THAT IS A MEASUREMENT, NOT A CHOICE. Outside test fixtures the -// corpus carries exactly one landed BmcAccessObserved standing, mtcollins1_access_standing, and -// gunbc.machine_intake_mtcollins1_access_observation says so about itself -- it is the first landed -// BmcAccessObservation in the repository and no host, srv3 included, has ever authored one. A second -// host joins this list the day it authors an observation, and nobody edits a roster to let it. fn reset_subject_candidates() -> List { [ ResetSubjectCandidate { @@ -75,8 +47,7 @@ fn reset_subject_candidates() -> List { observation: mtcollins1_access_observation, capability_row: mtcollins1_capability_row, username: mtcollins1_bmc_username, - boot_device: mtcollins1_cdrom_device, - boot_readback_rendering: mtcollins1_cdrom_readback_rendering, + boot_selection: mtcollins1_cdrom_selection, power_action: mtcollins1_power_action, }, ] @@ -89,12 +60,6 @@ fn reset_subject_admission(candidate: ResetSubjectCandidate) -> OobBootHandoffAd ) } -// THE FILTER IS A PREDICATE, NOT A FAILURE ARM, AND THE DIFFERENCE MATTERS HERE. Dropping a -// candidate whose controller does not admit power control is not an absorbing fallback swallowing a -// diagnostic -- it is the membership condition doing its job, and the dropped host is not a loss but -// a non-member. The refusal that DOES have to be loud is one level up, in -// gunbc.host_reset_return reset_dispatch_options, where an unmintable observer pairing refuses the -// whole option list rather than quietly shrinking it. fn reset_subject_roster() -> List { fold( reset_subject_candidates(), @@ -108,17 +73,12 @@ fn reset_subject_roster() -> List { ) } -// THE PEERS THAT MAY OBSERVE A RESET are the executor fleet hosts, and this is the one place the two -// rosters legitimately meet: an observer needs a runner to run on, which is exactly what fleet_hosts() -// means. Derived from that authority rather than spelled, so enrolling or retiring an executor host -// moves the observer set with it. +// RESET OBSERVERS are executor hosts, not reset subjects by implication. The two sets meet only +// here because observing a reset needs a runner on a peer. fn reset_observer_peer_roster() -> List { map(fleet_hosts(), h => h as NonEmptyStr) } -// THE ROW FOR ONE SUBJECT, so a caller that resolved a subject label can reach the evidence and the -// policy for it without re-walking the roster in its own vocabulary. Absent means the label names no -// candidate, which a caller must treat as a refusal and never as a host it may drive with defaults. fn reset_subject_candidate_for(host: NonEmptyStr) -> ResetSubjectCandidate? { fold( reset_subject_candidates(), diff --git a/dag/gunbc/machine_intake/megarac_media_attach.dag b/dag/gunbc/machine_intake/megarac_media_attach.dag index 8b5298a800d..6d73003b0f2 100644 --- a/dag/gunbc/machine_intake/megarac_media_attach.dag +++ b/dag/gunbc/machine_intake/megarac_media_attach.dag @@ -1,10 +1,12 @@ module gunbc.machine_intake_megarac_media_attach import std.types { Bool, Int, NonEmptyStr, String } +import std.nat { Nat, nat_range_inclusive } +import std.measure { Second, second } +import extdeps.tools.sleep { sleep_delay_seconds_second_carrier_projection } import extdeps.bmc.megarac import extdeps.languages.json.parse { JsonArray, - JsonDocumentParse, JsonDocumentParsed, JsonDocumentUnreadable, JsonMemberFound, @@ -16,69 +18,17 @@ import extdeps.languages.json.parse { some_json_value, } -// ATTACHING A REMOTE IMAGE, AS A MODELED OPERATION RATHER THAN A SHELL SCRIPT. extdeps.bmc.megarac -// described this API in prose for months and carried no transport, so the first attach against a -// Mt. Collins unit was driven by hand-written curl — the unmodeled realization DESIGN §6 names, and -// the reason the netboot lane could not claim its image was procured through .dag. The service rows -// made the surface reachable; this module is the caller that makes it reached. +// ATTACHING A REMOTE IMAGE, AS A MODELED OPERATION. The effect is adjudicated only by the +// configurations read-back. HTTP status is not an effect oracle on this firmware: PUT and POST +// requests have returned HTTP 500 both when their writes applied and when they did not. // -// EVERY STEP READS BACK, AND THAT IS FORCED BY THE CONTROLLER'S OWN BEHAVIOUR rather than chosen for -// rigour. gunbc.machine_intake_mtcollins1_diskless_boot_receipt records two measured cases of this -// firmware answering HTTP 500 WHILE THE WRITE TOOK EFFECT: PUT media/general (code 16425) with the -// share re-mounting anyway, and stop-media (code 1411) with the following attach succeeding. An -// operation that treated a non-zero exit as refusal would refuse a write that worked, and the caller -// would then retry or abort against a controller whose state had already moved. So success here is -// never an exit status; it is the configurations listing naming the image. -// -// THE IMAGE INDEX IS RESOLVED, NEVER ASSUMED. start-media takes an image_index, and the controller -// assigns indices by its own enumeration of the share — the same file was index 0 on one scan and -// index 1 after another image appeared. A baked index attaches whatever now occupies that slot, -// which on a share holding a memtest ISO and an installer ISO is a silent wrong-boot rather than a -// failure. The index is read from the images listing by matching the image NAME. -// -// THE IMAGES LISTING ENUMERATES WHAT IS AVAILABLE TO ATTACH, NOT WHAT THE SHARE HOLDS, and an -// earlier revision of this module got that exactly backwards in a way worth recording because the -// wrong diagnosis had a dangerous remedy attached to it. Measured on this unit 2026-09-06: with two -// ISOs in the export, /remote/images listed both; after start-media attached one, the listing -// returned ONLY THE OTHER, and the survivor's image_index moved from 1 to 0. The attached image had -// not vanished — it had moved to /remote/configurations, which is where a presented image lives. -// -// THE EARLIER READING WAS THAT THE LISTING IS A CACHE THAT GOES STALE, with the remedy "re-assert -// mount_cd". That remedy appeared to work, and the reason it appeared to work is the problem: -// toggling mount_cd DETACHES EVERYTHING, which is what returns the image to the available pool. A -// remedy that works by undoing the desired state is worse than no remedy, and it was written into -// an operator-facing message on a lane whose entire purpose is hosts booted from that medium. -// -// WHAT THE HAZARD IS, AT THE STRENGTH IT WAS ACTUALLY MEASURED, because an earlier revision of this -// paragraph overstated it in the same breath as retracting an overstatement. It claimed the toggle -// pulls the running root out from under a booted host. That is the MECHANISM — the presented medium -// is withdrawn, and casper reads the read-only lower layer from it on demand rather than from RAM, -// per this lane's own boot receipt — but it is not what was observed. The toggle WAS performed on -// this unit while it was booted from the medium, and the running installer survived it: measured -// afterwards over serial console, still interactive at its own menu. The controller is configured -// rmedia_retry_count 3 / rmedia_retry_interval 15, and the system was idle at a prompt rather than -// reading, either of which may explain the survival. -// -// SO THE HONEST STATEMENT IS THAT THE BLAST RADIUS IS UNQUANTIFIED, not that it is catastrophic and -// not that it is safe. One observation of one idle host is not evidence that a toggle during heavy -// reads is survivable, and the remedy is still wrong for the reason that does not depend on any of -// this: it "fixes" the listing by undoing the attachment the caller asked for. -// -// SO THE ORDER OF READS IS LOAD-BEARING AND CONFIGURATIONS COMES FIRST. Asking the available list -// whether an already-attached image is present is asking the wrong authority a question it answers -// "no" for the one reason that means SUCCESS. That is what made the operation non-idempotent: a -// second converge against a correctly-attached host refused, which for a converge step is the -// failure mode that matters most, since converge is run repeatedly by construction. -// THE CLEANUP OUTCOME IS CARRIED BESIDE THE ATTACH OUTCOME, never folded into it. Whether the -// image attached and whether the session was released are different facts with different owners: a -// successful attach that leaked a session is still a successful attach, and reporting it as a -// failure would hide the thing that worked while a caller retried it and leaked another. The -// controller's session table is finite — this lane exhausted one service's sessions by opening one -// per probe and closing none — so the release has to be observable rather than assumed. -// -// SessionReleaseUncertain EXISTS BECAUSE A LOST RESPONSE IS NOT A KNOWN STATE. A DELETE whose reply -// never arrived may have released the session or may not; treating that as released would -// under-count leaks exactly when the transport is already misbehaving, which is when leaks matter. +// THE STATUS ENUM IS THE CONTROLLER'S OWN, recovered from source.min.js served by the live BMC and +// then exercised on mtcollins1. 0 is idle; 100 is connecting; 1 is the healthy steady state +// (frontend: Started / Connection Accepted); 2,3,4,5 are Connection Denied, Login Failed, +// MAX Session Reached and Permission Denied. The old predicate `status != 0` therefore accepted +// every known refusal as success and also treated connecting as ready. Only status 1 with a real +// session index is ready. + type SessionRelease = SessionReleased | SessionReleaseRefused { detail: String } @@ -93,19 +43,22 @@ type MegaRacAttachOutcome = MegaRacAttached { image_name: NonEmptyStr, image_index: String } | MegaRacAlreadyAttached { image_name: NonEmptyStr } | MegaRacConfigurationsUnreadable { detail: String } + | MegaRacConfigurationAmbiguous { image_name: NonEmptyStr, matches: Int } + | MegaRacWrongMediaType { image_name: NonEmptyStr, observed: String } + | MegaRacSessionIndexUnavailable { image_name: NonEmptyStr, configurations: String } + | MegaRacConnectionDenied { image_name: NonEmptyStr, configurations: String } + | MegaRacLoginFailed { image_name: NonEmptyStr, configurations: String } + | MegaRacMaxSessionReached { image_name: NonEmptyStr, configurations: String } + | MegaRacPermissionDenied { image_name: NonEmptyStr, configurations: String } + | MegaRacStopped { image_name: NonEmptyStr, status: String, configurations: String } + | MegaRacAttachTimedOut { image_name: NonEmptyStr, samples: Nat, configurations: String } | MegaRacSessionRefused { detail: String } | MegaRacSessionTokenUnreadable { detail: String } | MegaRacImagesUnreadable { detail: String } | MegaRacImageListingEmpty | MegaRacImageListingUnparseable { detail: String } | MegaRacImageNotEnumerated { image_name: NonEmptyStr } - | MegaRacStartRefused { detail: String } - | MegaRacAttachUnconfirmed { image_name: NonEmptyStr, configurations: String } -// THE CSRF TOKEN IS READ FROM THE PARSED DOCUMENT, not scraped. The shell version matched a regex -// over the response body, which is a second reading of JSON beside the one this repository already -// owns; extdeps.languages.json.parse is the single recognition authority and a document it cannot -// parse is unreadable rather than partially believed. fn json_string_member(doc: JsonValue, key: String) -> String? { match json_object_unique_member(v: doc, key: key) { JsonMemberFound { value: v } => @@ -128,9 +81,6 @@ fn json_number_member(doc: JsonValue, key: String) -> String? { } } -// THE INDEX OF A NAMED IMAGE, folded over the parsed array. Returns the FIRST match and the fold -// keeps it, because a controller enumerating one name twice is a state this module has never -// observed and would rather report as the index it acted on than silently prefer the last. fn image_index_named(elements: List, image_name: String) -> String? { fold(elements, init: none, f: (acc, element) => match acc { @@ -156,11 +106,8 @@ fn images_array_elements(doc: JsonValue) -> List? { } } -// THE START-MEDIA BODY, rendered here rather than by the caller so image_redirection cannot be -// omitted by a caller who does not know it is required. extdeps.bmc.megarac records that omitting -// it makes the firmware refuse with opaque codes 13410/13460, recovered from the firmware's own UI -// bundle rather than from documentation — exactly the kind of fact that is lost when a body is -// assembled at a call site. +// THE REQUIRED FIELD IS ENCODED HERE AND HAS NO CALLER-SUPPLIED ABSENT FORM. Omitting +// image_redirection:1 was measured to produce opaque 13410/13460 refusals. fn start_media_body(image_name: NonEmptyStr, image_index: String) -> NonEmptyStr { join([ "{\"image_name\":\"", image_name as String, @@ -169,23 +116,6 @@ fn start_media_body(image_name: NonEmptyStr, image_index: String) -> NonEmptyStr ], "") as NonEmptyStr } -// THE EFFECT SEQUENCE. Session, list, resolve, start, confirm — and the confirmation is a separate -// read rather than the start call's own answer, for the reason given at the top of this module. -// -// THE CREDENTIAL IS A VALUE HERE AND A FILE PATH EVERYWHERE ELSE IN THIS LANE, and that asymmetry is -// forced rather than chosen: OpenSession is form-encoded, and curl offers no netrc equivalent for a -// form body, so the password reaches argv for exactly one call. Every subsequent operation carries -// no credential at all because the cookie is the bearer. The ipmi operations beside this take a -// password FILE for the same threat and can, because -f exists there. Naming the asymmetry is the -// point; hiding it behind a wrapper would make one call's exposure look like none. -// -// AN OPENED SESSION WHOSE TOKEN CANNOT BE READ IS STILL AN ALLOCATED SESSION. An earlier -// revision returned SessionReleaseNotAttempted here, which is the leak that saturated this -// controller: OpenSession succeeded, the cookie was written, and CloseSession never ran because -// the renderer treated the arm as "never opened". The DELETE still needs an X-CSRFTOKEN header -// by the upstream contract; the cookie is the bearer, so the header is supplied as a sentinel -// rather than inventing a second CloseSession shape. A refused or uncertain close remains -// SessionReleaseRefused, never NotAttempted. func megarac_attach_remote_image( bmc_host: NonEmptyStr, username: NonEmptyStr, @@ -252,9 +182,6 @@ func megarac_release_unreadable_session( } } -// THE RELEASE RUNS ON EVERY PATH THROUGH THE ATTACH, which is why the attach outcome is computed -// first and the close follows it unconditionally rather than sitting inside a success arm. A -// refusal allocated the same session a success does. func megarac_attach_then_release( bmc_host: NonEmptyStr, cookie_jar: NonEmptyStr, @@ -282,14 +209,219 @@ func megarac_attach_then_release( } } -// CONFIGURATIONS IS CONSULTED BEFORE ANYTHING IS WRITTEN, so the converged case performs no write -// at all. This is not an optimisation: start-media against an already-presented image is a write -// whose effect on a booted host is unmodelled, and the point of reading first is to not make it. -// -// MALFORMED PRESENTED STATE IS UNKNOWN, NOT "NOT ATTACHED". An earlier revision collapsed a -// JSON parse failure or a non-array document to false, then walked the available-images list -// and could StartMedia over a controller whose current attachment was unreadable. That is the -// absorbing-fallback DESIGN §5 forbids: ignorance rendered as the empty case. +fn configuration_row_names(row: JsonValue, image_name: NonEmptyStr) -> Bool { + match json_string_member(doc: row, key: "image_name") { + Absent => false + Present { value: n } => n == (image_name as String) + } +} + +// ONE NAMED ROW'S EXACT STATE. Session index 255 is the controller's N/A sentinel and cannot be +// promoted into a serving session even beside status 1. +type PresentedMediaStanding + = PresentedMediaUnreadable { detail: String } + | PresentedMediaNotAttached + | PresentedMediaIdle + | PresentedMediaConnecting { session_index: String } + | PresentedMediaReady { session_index: String } + | PresentedMediaConnectionDenied + | PresentedMediaLoginFailed + | PresentedMediaMaxSessionReached + | PresentedMediaPermissionDenied + | PresentedMediaStopped { status: String } + | PresentedMediaSessionIndexUnavailable + | PresentedMediaWrongType { observed: String } + | PresentedMediaAmbiguous { matches: Int } + +fn configuration_row_standing(row: JsonValue) -> PresentedMediaStanding { + let media_type = match json_number_member(doc: row, key: "media_type") { + Absent => "unreadable" + Present { value: mt } => mt + } + if media_type != "1" { + return PresentedMediaWrongType { observed: media_type } + } + + let session_index = match json_number_member(doc: row, key: "session_index") { + Absent => "unreadable" + Present { value: idx } => idx + } + return match json_number_member(doc: row, key: "redirection_status") { + Absent => PresentedMediaUnreadable { detail: "named configuration has no numeric redirection_status" } + Present { value: status } => + if status == "0" { + PresentedMediaIdle + } else if status == "100" { + PresentedMediaConnecting { session_index: session_index } + } else if status == "1" { + if session_index == "255" || session_index == "unreadable" { + PresentedMediaSessionIndexUnavailable + } else { + PresentedMediaReady { session_index: session_index } + } + } else if status == "2" { + PresentedMediaConnectionDenied + } else if status == "3" { + PresentedMediaLoginFailed + } else if status == "4" { + PresentedMediaMaxSessionReached + } else if status == "5" { + PresentedMediaPermissionDenied + } else { + PresentedMediaStopped { status: status } + } + } +} + +fn presented_media_standing(body: String, image_name: NonEmptyStr) -> PresentedMediaStanding { + match parse_json_document(s: body) { + JsonDocumentUnreadable { gap: _ } => PresentedMediaUnreadable { detail: body } + JsonDocumentParsed { value: v } => + match images_array_elements(doc: v) { + Absent => PresentedMediaUnreadable { detail: body } + Present { value: rows } => { + let named = rows |> filter(r => configuration_row_names(row: r, image_name: image_name)) + let matches = count(named) + if matches == 0 { + PresentedMediaNotAttached + } else if matches > 1 { + PresentedMediaAmbiguous { matches: matches } + } else { + match named.first() { + Absent => PresentedMediaNotAttached + Present { value: row } => configuration_row_standing(row: row) + } + } + } + } + } +} + +fn presented_terminal_outcome( + standing: PresentedMediaStanding, + image_name: NonEmptyStr, + configurations: String, +) -> MegaRacAttachOutcome? { + match standing { + PresentedMediaConnectionDenied => Present { value: MegaRacConnectionDenied { image_name: image_name, configurations: configurations } } + PresentedMediaLoginFailed => Present { value: MegaRacLoginFailed { image_name: image_name, configurations: configurations } } + PresentedMediaMaxSessionReached => Present { value: MegaRacMaxSessionReached { image_name: image_name, configurations: configurations } } + PresentedMediaPermissionDenied => Present { value: MegaRacPermissionDenied { image_name: image_name, configurations: configurations } } + PresentedMediaStopped { status: s } => Present { value: MegaRacStopped { image_name: image_name, status: s, configurations: configurations } } + PresentedMediaSessionIndexUnavailable => Present { value: MegaRacSessionIndexUnavailable { image_name: image_name, configurations: configurations } } + PresentedMediaWrongType { observed: mt } => Present { value: MegaRacWrongMediaType { image_name: image_name, observed: mt } } + PresentedMediaAmbiguous { matches: n } => Present { value: MegaRacConfigurationAmbiguous { image_name: image_name, matches: n } } + PresentedMediaUnreadable { detail: d } => Present { value: MegaRacConfigurationsUnreadable { detail: d } } + PresentedMediaNotAttached => none + PresentedMediaIdle => none + PresentedMediaConnecting { session_index: _ } => none + PresentedMediaReady { session_index: _ } => none + } +} + +// 100->1 was measured at twelve seconds. Thirty one-second samples bound the asynchronous window +// without turning "keep polling" into an unbounded success search. +data megarac_media_ready_sample_cadence: Second = second(count: 1) +data megarac_media_ready_max_samples: Nat = 30 + +type MediaReadyPollFold { + outcome: MegaRacAttachOutcome? + samples: Nat + last_configurations: String +} + +func media_ready_poll_step( + acc: MediaReadyPollFold, + bmc_host: NonEmptyStr, + cookie_jar: NonEmptyStr, + csrf_token: NonEmptyStr, + image_name: NonEmptyStr, + started_image_index: String?, +) -> MediaReadyPollFold + uses net: std.resources.Network +{ + match acc.outcome { + Present { value: _ } => return acc + Absent => none + } + + configurations = megarac.Media.GetRemoteConfigurations( + bmc_host: bmc_host, + cookie_jar: cookie_jar, + csrf_token: csrf_token, + ) + if configurations.success == false { + return MediaReadyPollFold { + outcome: Present { value: MegaRacConfigurationsUnreadable { detail: configurations.body } }, + samples: acc.samples + 1, + last_configurations: configurations.body, + } + } + + let standing = presented_media_standing(body: configurations.body, image_name: image_name) + return match standing { + PresentedMediaReady { session_index: _ } => + MediaReadyPollFold { + outcome: Present { + value: match started_image_index { + Absent => MegaRacAlreadyAttached { image_name: image_name } + Present { value: idx } => MegaRacAttached { image_name: image_name, image_index: idx } + } + }, + samples: acc.samples + 1, + last_configurations: configurations.body, + } + _ => + match presented_terminal_outcome(standing: standing, image_name: image_name, configurations: configurations.body) { + Present { value: terminal } => + MediaReadyPollFold { + outcome: Present { value: terminal }, + samples: acc.samples + 1, + last_configurations: configurations.body, + } + Absent => { + let _delay = sleep_delay_seconds_second_carrier_projection(duration: megarac_media_ready_sample_cadence) + MediaReadyPollFold { + outcome: none, + samples: acc.samples + 1, + last_configurations: configurations.body, + } + } + } + } +} + +func await_media_ready( + bmc_host: NonEmptyStr, + cookie_jar: NonEmptyStr, + csrf_token: NonEmptyStr, + image_name: NonEmptyStr, + started_image_index: String?, +) -> MegaRacAttachOutcome + uses net: std.resources.Network +{ + let folded = fold( + nat_range_inclusive(lo: 1, hi: megarac_media_ready_max_samples), + init: MediaReadyPollFold { outcome: none, samples: 0, last_configurations: "no read-back yet" }, + f: (acc, _sample) => media_ready_poll_step( + acc: acc, + bmc_host: bmc_host, + cookie_jar: cookie_jar, + csrf_token: csrf_token, + image_name: image_name, + started_image_index: started_image_index, + ), + ) + return match folded.outcome { + Present { value: outcome } => outcome + Absent => MegaRacAttachTimedOut { + image_name: image_name, + samples: folded.samples, + configurations: folded.last_configurations, + } + } +} + func megarac_attach_with_token( bmc_host: NonEmptyStr, cookie_jar: NonEmptyStr, @@ -306,12 +438,24 @@ func megarac_attach_with_token( if presented.success == false { return MegaRacConfigurationsUnreadable { detail: presented.body } } - match presented_media_standing(body: presented.body, image_name: image_name) { - PresentedMediaUnreadable { detail: d } => - return MegaRacConfigurationsUnreadable { detail: d } - PresentedMediaAttached => + + let initial = presented_media_standing(body: presented.body, image_name: image_name) + match initial { + PresentedMediaReady { session_index: _ } => return MegaRacAlreadyAttached { image_name: image_name } - PresentedMediaNotAttached => none + PresentedMediaConnecting { session_index: _ } => + return await_media_ready( + bmc_host: bmc_host, + cookie_jar: cookie_jar, + csrf_token: csrf_token, + image_name: image_name, + started_image_index: none, + ) + _ => + match presented_terminal_outcome(standing: initial, image_name: image_name, configurations: presented.body) { + Present { value: terminal } => return terminal + Absent => none + } } images = megarac.Media.GetRemoteImages( @@ -323,25 +467,16 @@ func megarac_attach_with_token( return MegaRacImagesUnreadable { detail: images.body } } - match parse_json_document(s: images.body) { + let elements = match parse_json_document(s: images.body) { JsonDocumentUnreadable { gap: _ } => return MegaRacImageListingUnparseable { detail: images.body } JsonDocumentParsed { value: v } => match images_array_elements(doc: v) { - Absent => - return MegaRacImageListingUnparseable { detail: images.body } - Present { value: _ } => none - } - } - let elements = match parse_json_document(s: images.body) { - JsonDocumentParsed { value: v } => - match images_array_elements(doc: v) { + Absent => return MegaRacImageListingUnparseable { detail: images.body } Present { value: es } => es - Absent => [] } - JsonDocumentUnreadable { gap: _ } => [] } - if (elements |> count) == 0 { + if count(elements) == 0 { return MegaRacImageListingEmpty } @@ -358,70 +493,9 @@ func megarac_attach_with_token( } } -// THE CONFIRMATION READS ONE EXACT ACTIVE ROW, not a substring of a body. An earlier form asked -// whether the configurations text CONTAINED the image name, which admits a stopped configuration -// that still names it, and admits an error body that happens to mention it. -// -// THE INDEX IS DELIBERATELY NOT COMPARED, and an earlier revision of this check did compare it — -// first reading image_index, which is absent here so every genuine attachment was reported -// unconfirmed, then reading media_index, which is present and agrees. The second spelling passed, -// and it was still wrong: media_index is the VIRTUAL CD DEVICE SLOT, alongside session_index, not a -// position in the image enumeration. It agreed with the resolved image_index only because this unit -// presents a single CD device, so both are 0. Comparing them is the §3 nicknaming failure — two -// unrelated concepts joined because they share a coincidence and half a name — and it would have -// started refusing the moment a controller offered a second slot, with a message blaming the image. -// -// WHAT IS COMPARED IS WHAT THE ROW ACTUALLY ASSERTS: this device is presenting THIS NAME, as CD -// media, with redirection active. That is the whole of the desired state. -fn configuration_row_confirms(row: JsonValue, image_name: NonEmptyStr) -> Bool { - let name_ok = match json_string_member(doc: row, key: "image_name") { - Absent => false - Present { value: n } => n == (image_name as String) - } - let active = match json_number_member(doc: row, key: "redirection_status") { - Absent => false - Present { value: st } => st != "0" - } - let cd_media = match json_number_member(doc: row, key: "media_type") { - Absent => false - Present { value: mt } => mt == "1" - } - name_ok && active && cd_media -} - -type PresentedMediaStanding - = PresentedMediaUnreadable { detail: String } - | PresentedMediaAttached - | PresentedMediaNotAttached - -fn presented_media_standing(body: String, image_name: NonEmptyStr) -> PresentedMediaStanding { - match parse_json_document(s: body) { - JsonDocumentUnreadable { gap: _ } => PresentedMediaUnreadable { detail: body } - JsonDocumentParsed { value: v } => - match images_array_elements(doc: v) { - Absent => PresentedMediaUnreadable { detail: body } - Present { value: rows } => - if rows |> any(r => configuration_row_confirms(row: r, image_name: image_name)) { - PresentedMediaAttached - } else { - PresentedMediaNotAttached - } - } - } -} - -// A NON-ZERO START FOLLOWED BY NO CONFIRMATION IS PENDING, NOT REFUSED, and this firmware is why: -// the same controller answers HTTP 500 on writes that take effect, and its mount daemon is -// asynchronous. Reporting MegaRacStartRefused on a status code would refuse an attach that is -// merely still mounting. The bounded read-back decides; the status code only distinguishes which -// unconfirmed state is reported. -// -// THE READ-BACK DECIDES, INCLUDING WHEN START REPORTED FAILURE. This firmware answers HTTP 500 -// on writes that take effect; mapping start.success == false to MegaRacStartRefused refused an -// attach that was merely still mounting, and contradicted the comment this function already -// carried. A missing confirmation after any start response is pending (Unconfirmed). StartRefused -// is reserved for a start that failed AND whose configurations document is itself unreadable -// as JSON — that is, when we cannot even ask the read-back. +// START-MEDIA'S EXIT STATUS IS RECORDED BY THE TRANSPORT BUT DOES NOT SELECT AN OUTCOME HERE. +// Whether the HTTP response was 2xx or 500, the bounded configurations read-back above is the sole +// effect authority. func megarac_start_and_confirm( bmc_host: NonEmptyStr, cookie_jar: NonEmptyStr, @@ -431,32 +505,17 @@ func megarac_start_and_confirm( ) -> MegaRacAttachOutcome uses net: std.resources.Network { - start = megarac.Media.StartMedia( + let _start = megarac.Media.StartMedia( bmc_host: bmc_host, cookie_jar: cookie_jar, csrf_token: csrf_token, json_body: start_media_body(image_name: image_name, image_index: image_index), ) - - configurations = megarac.Media.GetRemoteConfigurations( + return await_media_ready( bmc_host: bmc_host, cookie_jar: cookie_jar, csrf_token: csrf_token, + image_name: image_name, + started_image_index: Present { value: image_index }, ) - if configurations.success == false { - return MegaRacAttachUnconfirmed { image_name: image_name, configurations: configurations.body } - } - - return match presented_media_standing(body: configurations.body, image_name: image_name) { - PresentedMediaAttached => - MegaRacAttached { image_name: image_name, image_index: image_index } - PresentedMediaNotAttached => - MegaRacAttachUnconfirmed { image_name: image_name, configurations: configurations.body } - PresentedMediaUnreadable { detail: d } => - if start.success == false { - MegaRacStartRefused { detail: start.body } - } else { - MegaRacAttachUnconfirmed { image_name: image_name, configurations: d } - } - } } diff --git a/dag/gunbc/machine_intake/mtcollins1_actuate.dag b/dag/gunbc/machine_intake/mtcollins1_actuate.dag index 257c8669414..28da68efa75 100644 --- a/dag/gunbc/machine_intake/mtcollins1_actuate.dag +++ b/dag/gunbc/machine_intake/mtcollins1_actuate.dag @@ -9,72 +9,54 @@ import extdeps.bmc.capability { CapabilityBootSourceOverride, CapabilityPowerControl, } +import extdeps.bmc.ipmi_boot_selection { + IpmiBootCdrom, + IpmiBootPxe, + IpmiBootSelection, + aarch64_uefi_once_boot_selection, + ipmi_boot_selection_label, +} import gunbc.machine_intake_mtcollins1_access_observation { mtcollins1_access_observation, mtcollins1_capability_row, } import gunbc.machine_intake_oob_boot_handoff { - BootHandoffCompleted, - BootHandoffNotAdmitted, + BootControlIssued, + BootControlNotAdmitted, + BootSelectionFirmwareModeMismatch, BootSelectionFlagInvalid, BootSelectionNotApplied, + BootSelectionPersistenceMismatch, BootSelectionRefused, BootSelectionUnverifiable, - OobBootHandoffOutcome, + OobBootControlOutcome, PowerCycleRefused, - oob_boot_handoff, + oob_boot_control_issue, } -// THE POLICY LAYER FOR ONE HOST, and it is a separate module from the arm on purpose. The arm takes -// device, power action and expected rendering as PARAMETERS because which of those a workflow picks -// is business policy (DESIGN §3); this module is where that policy is decided for Mt. Collins, so -// the arm stays reusable by the next host and by the Sparks without carrying anyone's choices. +// THE POLICY LAYER FOR THIS UNIT. A boot request is no longer a device string beside an assumed +// default. Each row below is an IpmiBootSelection that can be constructed only by the aarch64 +// UEFI-one-shot constructor. There is no argument, field or sibling constructor with which this +// module can request legacy firmware mode or a persistent override. // -// THE CLI REACHES ZERO-ARG AND SINGLE-String FUNCS ONLY, which is the mechanical reason this -// wrapper exists at all — the same reason gunbc.tools.bmc_onboard carries srv3_/srv4_ wrappers -// around a parameterized probe. It is NOT a per-host fork of the arm: everything host-specific here -// is a value, and a second host is a second wrapper over the identical operation, never a second -// operation. The one argument is the credential path, for the reason given on mtcollins1_password_file. -data mtcollins1_boot_device: NonEmptyStr = "pxe" +// Execution on 2026-09-10 grounded the distinction: `cdrom` alone read back PC-compatible legacy +// mode and failed on aarch64; adding `options=efiboot,persistent` selected EFI and booted. The model +// deliberately keeps the useful EFI bit and drops the experimental persistence bit: intake wants +// one boot, and ipmitool's absence of `persistent` reads back as "only next boot". +data mtcollins1_netboot_selection: IpmiBootSelection = + aarch64_uefi_once_boot_selection(device: IpmiBootPxe) -// WHAT ipmitool RENDERS WHEN THE OVERRIDE TOOK. `chassis bootparam get 5` prints a "Boot Device -// Selector : Force PXE" line, and the wire word sent to `chassis bootdev` is "pxe" — two different -// vocabularies for one fact, so the expected text is supplied here rather than guessed inside the -// arm. A mapping guessed there would be a second, undeclared authority on IPMI's boot device names. -// Measured on this unit 2026-09-05. -data mtcollins1_boot_readback_rendering: NonEmptyStr = "Force PXE" +data mtcollins1_cdrom_selection: IpmiBootSelection = + aarch64_uefi_once_boot_selection(device: IpmiBootCdrom) -// A CYCLE AND NOT A RESET, because the unit's own SEL is the evidence that a cycle takes effect -// here: driving `chassis power cycle` produced "Power Unit — Power cycle | Asserted" and "System -// Boot Initiated — Initiated by power up". Nothing has established the same for `reset` on this -// controller, and picking the unmeasured verb would assert a capability this repository does not -// hold evidence for. +// A CYCLE AND NOT A RESET, because the unit's own SEL is the evidence that a cycle takes effect: +// driving `chassis power cycle` produced both the power-cycle event and a boot-initiated event. data mtcollins1_power_action: NonEmptyStr = "cycle" -// THE ADMINISTRATOR ACCOUNT AS MEASURED, not as assumed: `ipmitool user list 1` reports user ID 2 -// named "admin" with ADMINISTRATOR privilege as the ONLY enabled account on the channel. This is -// the account the converge rotation phase will re-key, which is why it is a named row rather than -// a literal buried in a call. +// The only enabled administrator account observed on channel 1. Rotation is a separate arrival +// phase and this module receives only a credential FILE path; no secret is placed in argv. data mtcollins1_bmc_username: NonEmptyStr = "admin" -// THE CREDENTIAL ARRIVES AS AN EXPLICIT PATH ARGUMENT, not from the environment. The first draft -// read it from BMC_PASSWORD_FILE through shell.Env.Get and refused at run time with -// `Unimplemented { what: "unknown service operation: shell.Env.Get" }`. THAT DIAGNOSTIC IS -// MISLEADING: the operation is implemented and widely used — gunbc.actions_run_binding calls it on -// the live converge path — and it refused only because this module did not carry -// `import extdeps.shell`. Service operations register from the IMPORT CLOSURE, so an unimported -// service compiles clean and refuses at run time naming the operation rather than the import. -// -// The argument is kept anyway, because it is the better shape independent of that defect: the -// credential's location becomes a declared input the caller must state rather than ambient state -// the func silently depends on, which matters most for the value that rotates mid-program. -// -// AN EMPTY PATH REFUSES BEFORE ANY EFFECT, and the previous form did not. It substituted the string -// "bmc-password-file-argument-empty" and handed that to ipmitool as a filename — so a caller that -// supplied nothing produced either an authentication failure that reads as the CONTROLLER rejecting -// a credential, or, if a file of that name happened to exist, an unintended credential source. The -// comment called it a refusal; it was a rename. A missing input is now a typed outcome returned -// before the first write, so the zero-effects case is reachable and testable. type CredentialPathStanding = CredentialPathGiven { path: NonEmptyStr } | CredentialPathMissing @@ -87,118 +69,84 @@ fn mtcollins1_password_file(raw: String) -> CredentialPathStanding { } } -// DRIVES THE REAL CONTROLLER. Every outcome arm is rendered as its own failure reason, because the -// four refusals leave the host in materially different states and a caller retrying needs to know -// which: BootSelectionNotApplied means the override never took and must be re-applied, while -// PowerCycleRefused means it DID take and the controller is holding a next-boot override nothing -// has consumed. Collapsing them into one "handoff failed" would be the state-space conflation -// DESIGN's failure-mode list names. -// ONE RENDERER FOR BOTH ROUTES. Each outcome arm gets its own reason because the refusals leave the -// host in materially different states: BootSelectionNotApplied means the override never took and -// must be re-applied; BootSelectionFlagInvalid means the controller reported the selector WHILE -// declaring its boot flags invalid, so the override is present and will not be honoured; -// BootSelectionUnverifiable means the read itself failed and establishes nothing about the -// controller either way; PowerCycleRefused means the override APPLIED and the controller now holds -// an unconsumed next-boot override. Collapsing these into one failure would be the state-space -// conflation DESIGN's failure-mode list names. -fn mtcollins1_render_outcome(label: NonEmptyStr, outcome: OobBootHandoffOutcome) -> ProcessExit { +// ONE RENDERER FOR BOTH CONTROL TARGETS. ExitSuccess means exactly "the typed control request was +// issued" because the entrypoint names that proposition. It does not mean a boot completed. A +// completed delivery is earned by the image's own host-side receipt, not by this renderer. +fn mtcollins1_render_control_outcome(label: NonEmptyStr, outcome: OobBootControlOutcome) -> ProcessExit { match outcome { - BootHandoffCompleted { selected: _ } => ExitSuccess - BootSelectionRefused => - exit_failure(reason: concat(label as String, ": controller refused the boot source override")) - BootSelectionNotApplied { requested: d, readback: r } => - exit_failure(reason: concat(label as String, ": override for '", d as String, "' did not take; boot parameter 5 read back: ", r)) - BootSelectionFlagInvalid { requested: d, readback: r } => - exit_failure(reason: concat(label as String, ": override for '", d as String, "' reported alongside an INVALID boot flag, so it will not be honoured; boot parameter 5 read back: ", r)) - BootSelectionUnverifiable { requested: d, readback: r } => - exit_failure(reason: concat(label as String, ": boot parameter 5 read did not succeed, so the override for '", d as String, "' is unverified; output: ", r)) - PowerCycleRefused { selected: d } => - exit_failure(reason: concat(label as String, ": override for '", d as String, "' APPLIED but the power cycle was refused; the controller holds an unconsumed next-boot override")) - BootHandoffNotAdmitted { admission: _ } => - exit_failure(reason: concat(label as String, ": controller not admitted for out-of-band drive; no write was attempted")) + BootControlIssued { selection: _ } => ExitSuccess + BootSelectionRefused { selection: s } => + exit_failure(reason: join([label as String, ": controller refused typed boot selection ", ipmi_boot_selection_label(selection: s) as String], "")) + BootSelectionNotApplied { selection: s, readback: r } => + exit_failure(reason: join([label as String, ": device selector did not match ", ipmi_boot_selection_label(selection: s) as String, "; parameter 5: ", r], "")) + BootSelectionFirmwareModeMismatch { selection: s, readback: r } => + exit_failure(reason: join([label as String, ": firmware boot mode did not match ", ipmi_boot_selection_label(selection: s) as String, "; parameter 5: ", r], "")) + BootSelectionPersistenceMismatch { selection: s, readback: r } => + exit_failure(reason: join([label as String, ": override persistence did not match ", ipmi_boot_selection_label(selection: s) as String, "; parameter 5: ", r], "")) + BootSelectionFlagInvalid { selection: s, readback: r } => + exit_failure(reason: join([label as String, ": boot flag invalid for ", ipmi_boot_selection_label(selection: s) as String, "; parameter 5: ", r], "")) + BootSelectionUnverifiable { selection: s, readback: r } => + exit_failure(reason: join([label as String, ": parameter 5 unreadable for ", ipmi_boot_selection_label(selection: s) as String, "; output: ", r], "")) + PowerCycleRefused { selection: s } => + exit_failure(reason: join([label as String, ": selection applied but power cycle refused for ", ipmi_boot_selection_label(selection: s) as String], "")) + BootControlNotAdmitted { admission: _ } => + exit_failure(reason: join([label as String, ": controller not admitted for out-of-band boot control; no write attempted"], "")) } } -func mtcollins1_netboot_handoff(password_file_raw: String) -> ProcessExit +fn mtcollins1_issue_selection( + label: NonEmptyStr, + password_file: NonEmptyStr, + selection: IpmiBootSelection, +) -> ProcessExit + uses net: std.resources.Network +{ + mtcollins1_render_control_outcome( + label: label, + outcome: oob_boot_control_issue( + observation: mtcollins1_access_observation, + capability_row: mtcollins1_capability_row, + username: mtcollins1_bmc_username, + password_file: password_file, + selection: selection, + power_action: mtcollins1_power_action, + ), + ) +} + +func mtcollins1_netboot_control_issue(password_file_raw: String) -> ProcessExit uses net: std.resources.Network { match mtcollins1_password_file(raw: password_file_raw) { CredentialPathMissing => - exit_failure(reason: "mtcollins1 handoff: no credential path supplied; refusing before any controller write") + exit_failure(reason: "mtcollins1 PXE control issue: no credential path supplied; refusing before any controller write") CredentialPathGiven { path: pw } => - mtcollins1_render_outcome( - label: "mtcollins1 handoff", - outcome: oob_boot_handoff( - observation: mtcollins1_access_observation, - capability_row: mtcollins1_capability_row, - username: mtcollins1_bmc_username, - password_file: pw, - device: mtcollins1_boot_device, - expected_rendering: mtcollins1_boot_readback_rendering, - power_action: mtcollins1_power_action, - ) + mtcollins1_issue_selection( + label: "mtcollins1 PXE control issue", + password_file: pw, + selection: mtcollins1_netboot_selection, ) } } -// THE SECOND BOOT ROUTE FOR THE SAME UNIT, and it is the shape this module predicted: a second -// wrapper over the IDENTICAL operation, not a second operation. Everything that differs between -// netbooting and booting the BMC's virtual CD is a value — the device word and the text ipmitool -// renders for it — so oob_boot_handoff is reused unchanged. -// -// WHY A CD ROUTE EXISTS AT ALL ON A UNIT THAT DEMONSTRABLY PXE-BOOTS. Measured 2026-09-05, the -// controller answers `local_media_support: 0` and `sd_media: 0`, so it cannot HOLD a boot image; -// it answers `remote_media_support: 1` and enumerates images from an NFS share, so it can PRESENT -// one. That split is the whole reason this route matters: the host reaches a bootstrap without any -// PXE server on the segment, because the controller fetches the image itself and offers it as -// removable media. The DHCP capture in gunbc.machine_intake_mtcollins1_netboot_client_observation -// records the other half — the host asks for a boot file over PXE and nothing on the segment -// answers — so today this is the only delivery route that reaches this machine at all. -data mtcollins1_cdrom_device: NonEmptyStr = "cdrom" - -// Measured, not guessed: `chassis bootdev cdrom` followed by `chassis bootparam get 5` renders -// "Boot Device Selector : Force Boot from CD/DVD". The netboot route's rendering is "Force PXE", -// a different string for the same field, which is exactly why the arm takes the expected text from -// its caller rather than deriving it from the device word. -data mtcollins1_cdrom_readback_rendering: NonEmptyStr = "Force Boot from CD/DVD" - -func mtcollins1_cdrom_handoff(password_file_raw: String) -> ProcessExit +func mtcollins1_cdrom_control_issue(password_file_raw: String) -> ProcessExit uses net: std.resources.Network { match mtcollins1_password_file(raw: password_file_raw) { CredentialPathMissing => - exit_failure(reason: "mtcollins1 cdrom handoff: no credential path supplied; refusing before any controller write") + exit_failure(reason: "mtcollins1 CD control issue: no credential path supplied; refusing before any controller write") CredentialPathGiven { path: pw } => - mtcollins1_render_outcome( - label: "mtcollins1 cdrom handoff", - outcome: oob_boot_handoff( - observation: mtcollins1_access_observation, - capability_row: mtcollins1_capability_row, - username: mtcollins1_bmc_username, - password_file: pw, - device: mtcollins1_cdrom_device, - expected_rendering: mtcollins1_cdrom_readback_rendering, - power_action: mtcollins1_power_action, - ) + mtcollins1_issue_selection( + label: "mtcollins1 CD control issue", + password_file: pw, + selection: mtcollins1_cdrom_selection, ) } } -// THE ENFORCEMENT CONTROL, and it is deliberately not a test of the admission fold. That fold is -// pure and already exercised by gunbc.machine_intake_mtcollins1_handoff_probe; what it cannot show -// is that a REFUSAL HAPPENS BEFORE ANY WRITE. Classification and enforcement are different claims, -// and only the second is what a caller driving real hardware depends on. -// -// The capability row below carries the same capabilities the measured one does and a DIFFERENT -// firmware release, so admission refuses on OobHandoffFirmwareMismatch — the arm that exists -// because a capability row for release A could otherwise be handed beside an observation for -// release B. Everything else about the call is the real thing: the real endpoint, the real -// credential, the real operation. -// -// HOW TO READ THE RESULT. A non-zero exit naming "not admitted" is necessary but not sufficient: -// the load-bearing observation is EXTERNAL, that boot parameter 5 is unchanged after this runs. -// Reset it to a known value first, run this, and read it back. If the selector moved, the refusal -// came after a write and the ordering is decorative. +// THE ENFORCEMENT CONTROL. Same real operation and target, but a capability row for a different +// firmware release. Admission must refuse before the typed boot-selection write. The independent +// wet check remains parameter 5 unchanged after this entry returns non-zero. data mtcollins1_mismatched_firmware: BmcFirmwareReleaseIdentity = BmcFirmwareReleaseIdentity { family: AmiMegaRac, raw_version: "0.31-not-this-unit", @@ -220,17 +168,16 @@ func mtcollins1_denied_admission_control(password_file_raw: String) -> ProcessEx CredentialPathMissing => exit_failure(reason: "mtcollins1 denied-admission control: no credential path supplied") CredentialPathGiven { path: pw } => - mtcollins1_render_outcome( + mtcollins1_render_control_outcome( label: "mtcollins1 denied-admission control", - outcome: oob_boot_handoff( + outcome: oob_boot_control_issue( observation: mtcollins1_access_observation, capability_row: mtcollins1_mismatched_capability_row, username: mtcollins1_bmc_username, password_file: pw, - device: mtcollins1_boot_device, - expected_rendering: mtcollins1_boot_readback_rendering, + selection: mtcollins1_netboot_selection, power_action: mtcollins1_power_action, - ) + ), ) } } diff --git a/dag/gunbc/machine_intake/mtcollins1_media_attach.dag b/dag/gunbc/machine_intake/mtcollins1_media_attach.dag index a21529dee9c..c44a2b7a9dd 100644 --- a/dag/gunbc/machine_intake/mtcollins1_media_attach.dag +++ b/dag/gunbc/machine_intake/mtcollins1_media_attach.dag @@ -11,110 +11,92 @@ import gunbc.machine_intake_megarac_media_attach { SessionReleaseNotAttempted, SessionReleaseRefused, SessionReleased, - MegaRacAttachUnconfirmed, MegaRacAttached, MegaRacAlreadyAttached, + MegaRacAttachTimedOut, + MegaRacConfigurationAmbiguous, MegaRacConfigurationsUnreadable, + MegaRacConnectionDenied, MegaRacImageListingEmpty, MegaRacImageListingUnparseable, MegaRacImageNotEnumerated, MegaRacImagesUnreadable, + MegaRacLoginFailed, + MegaRacMaxSessionReached, + MegaRacPermissionDenied, + MegaRacSessionIndexUnavailable, MegaRacSessionRefused, MegaRacSessionTokenUnreadable, - MegaRacStartRefused, + MegaRacStopped, + MegaRacWrongMediaType, megarac_attach_remote_image, } -// THE POLICY LAYER FOR ONE HOST'S MEDIA ATTACH, separate from the operation for the same reason the -// boot-handoff wrappers are: which image this unit should carry is a workflow decision, and the -// operation stays reusable by the next controller without carrying anyone's choices. -// -// THE IMAGE NAME IS IMPORTED RATHER THAN AUTHORED, and it used to be authored here. That made this -// module and the fetch module two authorities for one fact — the artifact this host boots — which -// admitted verifying one image and attaching another, with every individual step reporting success. -// See gunbc.machine_intake_mtcollins1_boot_artifact. - -// THE JAR IS ATTEMPT-OWNED, AND A FIXED LITERAL HERE WAS THE DEFECT. extdeps.bmc.megarac's note -// once claimed that making the jar a parameter meant an attempt owned its own — it does not: a -// parameter PERMITS a per-attempt path and this wrapper passed a constant, so two concurrent -// attempts shared one bearer file. The attempt identifier is now part of the path, so the caller -// establishes the ownership the operation cannot. fn mtcollins1_media_cookie_jar(attempt: NonEmptyStr) -> NonEmptyStr { join(["/tmp/gunbc-mtcollins1-megarac-jar-", attempt as String], "") as NonEmptyStr } data mtcollins1_media_username: NonEmptyStr = "admin" -// EACH OUTCOME RENDERS ITS OWN REASON because they have different remedies, and the remedies are -// what an operator acts on — which is why one of these messages previously had to be retracted -// rather than reworded. It advised re-asserting mount_cd to fix an "empty" listing. The listing was -// never stale: the image was simply attached, and attached images leave the available listing. The -// advice "worked" only by detaching every presented image, which is to say by undoing the state the -// caller had asked for. See gunbc.machine_intake_megarac_media_attach, which also records how far -// the danger to a booted host was and was not measured. -// -// MegaRacAlreadyAttached IS A SUCCESS AND IS RENDERED AS ONE. Converge is run repeatedly by -// construction, so the second run finding the desired state already held is the normal case, not an -// exception to it — and no write is performed on that path. -// -// MegaRacAttachUnconfirmed is the one state where waiting is right: start-media was accepted and -// the configurations listing does not name the image yet. The controller's mount daemon is -// asynchronous, so this is pending rather than failed — but it is reported rather than slept -// through, because a caller that polls until something looks successful has no deadline. +// Only status 1 with a non-255 session index reaches a success arm. Connecting (100) is consumed +// by the bounded poll inside the operation; 2-5 remain separate terminal outcomes so a login +// failure can never render as an attached image. fn mtcollins1_render_attach(outcome: MegaRacAttachOutcome) -> ProcessExit { match outcome { MegaRacAttached { image_name: _, image_index: _ } => ExitSuccess MegaRacAlreadyAttached { image_name: _ } => ExitSuccess MegaRacConfigurationsUnreadable { detail: d } => - exit_failure(reason: concat("mtcollins1 media attach: the presented-media listing could not be read, so whether anything is attached is UNKNOWN; refusing rather than attaching over an unknown state: ", d)) + exit_failure(reason: concat("mtcollins1 media attach: configurations unreadable; attachment state unknown: ", d)) + MegaRacConfigurationAmbiguous { image_name: n, matches: m } => + exit_failure(reason: join(["mtcollins1 media attach: ", to_string(m), " configuration rows name '", n as String, "'; refusing an ambiguous device state"], "")) + MegaRacWrongMediaType { image_name: n, observed: mt } => + exit_failure(reason: join(["mtcollins1 media attach: '", n as String, "' is present under media_type ", mt, " rather than CD media_type 1"], "")) + MegaRacSessionIndexUnavailable { image_name: n, configurations: c } => + exit_failure(reason: join(["mtcollins1 media attach: '", n as String, "' reported Started but session_index is absent or 255/N/A: ", c], "")) + MegaRacConnectionDenied { image_name: n, configurations: c } => + exit_failure(reason: join(["mtcollins1 media attach: connection denied for '", n as String, "': ", c], "")) + MegaRacLoginFailed { image_name: n, configurations: c } => + exit_failure(reason: join(["mtcollins1 media attach: remote-share login failed for '", n as String, "': ", c], "")) + MegaRacMaxSessionReached { image_name: n, configurations: c } => + exit_failure(reason: join(["mtcollins1 media attach: controller reached its maximum redirection sessions for '", n as String, "': ", c], "")) + MegaRacPermissionDenied { image_name: n, configurations: c } => + exit_failure(reason: join(["mtcollins1 media attach: permission denied for '", n as String, "': ", c], "")) + MegaRacStopped { image_name: n, status: st, configurations: c } => + exit_failure(reason: join(["mtcollins1 media attach: '", n as String, "' reached stopped redirection status ", st, ": ", c], "")) + MegaRacAttachTimedOut { image_name: n, samples: samples, configurations: c } => + exit_failure(reason: join(["mtcollins1 media attach: '", n as String, "' did not reach status 1 within ", to_string(samples), " bounded samples; last configurations: ", c], "")) MegaRacSessionRefused { detail: d } => - exit_failure(reason: concat("mtcollins1 media attach: session refused: ", d)) + exit_failure(reason: concat("mtcollins1 media attach: BMC session refused: ", d)) MegaRacSessionTokenUnreadable { detail: d } => - exit_failure(reason: concat("mtcollins1 media attach: session succeeded but no CSRFToken could be read from its document: ", d)) + exit_failure(reason: concat("mtcollins1 media attach: BMC session opened but CSRF token was unreadable: ", d)) MegaRacImagesUnreadable { detail: d } => - exit_failure(reason: concat("mtcollins1 media attach: images listing unreadable: ", d)) + exit_failure(reason: concat("mtcollins1 media attach: available-image listing unreadable: ", d)) MegaRacImageListingEmpty => - exit_failure(reason: "mtcollins1 media attach: the image is not presented AND the controller offers no image available to attach; check that the export is reachable from the controller and holds the file. Do NOT toggle mount_cd to 'refresh' this — it works by detaching every presented image, so on a host booted from that medium it withdraws what the running system is reading from") + exit_failure(reason: "mtcollins1 media attach: desired image is not presented and the controller offers no image to attach; do not toggle mount_cd as a refresh because that detaches presented media") MegaRacImageListingUnparseable { detail: d } => - exit_failure(reason: concat("mtcollins1 media attach: the images listing was not valid JSON, which is a protocol failure rather than the stale-cache case above: ", d)) + exit_failure(reason: concat("mtcollins1 media attach: available-image listing is not valid JSON: ", d)) MegaRacImageNotEnumerated { image_name: n } => - exit_failure(reason: concat("mtcollins1 media attach: the image is not presented, and the controller offers other images but not '", n as String, "' — so it is absent from the share as the controller sees it, rather than already in use")) - MegaRacStartRefused { detail: d } => - exit_failure(reason: concat("mtcollins1 media attach: start-media refused AND the configurations listing does not name the image: ", d)) - MegaRacAttachUnconfirmed { image_name: n, configurations: c } => - exit_failure(reason: concat("mtcollins1 media attach: start-media was accepted but configurations does not yet name '", n as String, "'; the mount daemon is asynchronous so this may be pending: ", c)) + exit_failure(reason: join(["mtcollins1 media attach: desired image '", n as String, "' is neither ready nor offered by the controller"], "")) } } -// A LEAKED SESSION IS REPORTED EVEN WHEN THE ATTACH SUCCEEDED, and it does not turn a success into -// a failure. The controller's session table is finite and this lane exhausted one service's -// sessions by never closing any; a caller that reads "attached" and ignores an unreleased session -// will keep attaching until the table fills, which presents as an unrelated 403 much later. The -// release is therefore surfaced in the reason text rather than folded into the verdict. fn mtcollins1_render_release(standing: SessionRelease) -> String { match standing { SessionReleased => "" - SessionReleaseNotAttempted => " (session was never opened, so nothing to release)" - SessionReleaseRefused { detail: d } => concat(" WARNING: the session was NOT released and remains allocated on the controller: ", d) + SessionReleaseNotAttempted => " (session was never opened)" + SessionReleaseRefused { detail: d } => concat(" WARNING: controller session was not released: ", d) } } -// THE DISCRIMINATING CONTROL, and it is the arm this operation most needs one for. Every other -// refusal here is reachable only by breaking the controller or the network; this one is reachable -// on a healthy unit and it is the arm that decides whether a name that is NOT present can be -// reported as attached. Without it, "the attach succeeded" is a claim about a run in which nothing -// could have failed — the specification-without-execution shape DESIGN §5 names. -// -// IT RUNS AGAINST THE SAME LIVE CONTROLLER AS THE POSITIVE PATH, differing in exactly one input, -// so a green positive and a red control together establish that the confirmation reads the name -// rather than reporting whatever the controller happens to be presenting. Running it costs one -// session and performs no write: the absent name is refused after the two reads, before start. func mtcollins1_attach_absent_image_control(password_raw: String, attempt: String) -> ProcessExit uses net: std.resources.Network { if password_raw == "" { return exit_failure(reason: "mtcollins1 media attach control: no controller password supplied; refusing before any request") } + if attempt == "" { + return exit_failure(reason: "mtcollins1 media attach control: no attempt identifier supplied") + } return mtcollins1_render_attach_result( result: megarac_attach_remote_image( bmc_host: mtcollins1_endpoint.host, @@ -133,16 +115,17 @@ func mtcollins1_attach_diskless_image(password_raw: String, attempt: String) -> return exit_failure(reason: "mtcollins1 media attach: no controller password supplied; refusing before any request") } if attempt == "" { - return exit_failure(reason: "mtcollins1 media attach: no attempt identifier supplied; the cookie jar is attempt-owned and a shared jar is what lets two runs consume one session") + return exit_failure(reason: "mtcollins1 media attach: no attempt identifier supplied; cookie jars are attempt-owned") } - let result = megarac_attach_remote_image( - bmc_host: mtcollins1_endpoint.host, - username: mtcollins1_media_username, - password: password_raw as NonEmptyStr, - cookie_jar: mtcollins1_media_cookie_jar(attempt: attempt as NonEmptyStr), - image_name: mtcollins1_diskless_image_name, + return mtcollins1_render_attach_result( + result: megarac_attach_remote_image( + bmc_host: mtcollins1_endpoint.host, + username: mtcollins1_media_username, + password: password_raw as NonEmptyStr, + cookie_jar: mtcollins1_media_cookie_jar(attempt: attempt as NonEmptyStr), + image_name: mtcollins1_diskless_image_name, + ) ) - return mtcollins1_render_attach_result(result: result) } fn mtcollins1_render_attach_result(result: MegaRacAttachResult) -> ProcessExit { @@ -150,7 +133,7 @@ fn mtcollins1_render_attach_result(result: MegaRacAttachResult) -> ProcessExit { ExitSuccess => match result.session_release { SessionReleased => ExitSuccess - _ => exit_failure(reason: concat("mtcollins1 media attach: the image attached, but the session was not released.", mtcollins1_render_release(standing: result.session_release))) + _ => exit_failure(reason: concat("mtcollins1 media attach: image became ready, but the BMC session was not released.", mtcollins1_render_release(standing: result.session_release))) } other => other } diff --git a/dag/gunbc/machine_intake/oob_boot_handoff.dag b/dag/gunbc/machine_intake/oob_boot_handoff.dag index 72453ab52ac..01610028179 100644 --- a/dag/gunbc/machine_intake/oob_boot_handoff.dag +++ b/dag/gunbc/machine_intake/oob_boot_handoff.dag @@ -2,6 +2,10 @@ module gunbc.machine_intake_oob_boot_handoff import std.types { Bool, NonEmptyStr, String } import extdeps.bmc.ipmi +import extdeps.bmc.ipmi_boot_selection { + IpmiBootSelection, + ipmi_boot_selection_label, +} import extdeps.bmc.access_profile { BmcAccessObservation, BmcAccessRoute, @@ -15,33 +19,19 @@ import extdeps.bmc.capability { release_row_has_capability, } -// THE OUT-OF-BAND BOOT HANDOFF: the operation a converge program performs against a host it cannot -// reach THROUGH. Every existing transport in this repository — gunbc.host_effect LocalShell and -// FleetSsh — talks to a machine via the operating system being installed, so neither can act on a -// host that has none. This module models the arm that acts on the CONTROLLER instead, which is the -// only arm that can move a bare host toward serving. -// -// WHY THIS IS A SEPARATE REALIZATION AND NOT A FORK OF THE IN-HOST PATH (DESIGN §3). Reaching a host -// over its BMC and reaching it over ssh are two realizations of ONE interface — drive this host -// toward its desired state — so the choice between them is dispatch, and dispatch sits peripheral. -// What makes them genuinely different is not the wire protocol but WHAT IS CONVERGED: an in-host arm -// mutates a persistent root, while this arm sets a boot chain and restarts. For a diskless host the -// second is the whole of convergence, because there is no persistent root to mutate and therefore -// nowhere for drift to live. +// THE OUT-OF-BAND BOOT-CONTROL ISSUER. This module performs exactly one control-plane transition: +// apply a typed IPMI boot selection, read back every load-bearing flag, and request the power +// action. It does NOT claim that the selected device executed. That terminal fact belongs to the +// delivered image's own receipt, whose producer runs on the host and cannot be substituted by a +// controller acknowledgement. // -// WHAT THIS MODULE DOES NOT DO, stated because the omission is the design and not an unfinished -// edge. It does not serve the boot artifacts, it does not decide which image a host should run, and -// it does not observe what booted. It performs one transition — select boot source, verify the -// selection took, restart — and every other phase is a separate authority. A module that also served -// the image would fuse artifact delivery into boot control, and the first host wanting a different -// delivery would have to fork it. -// -// WHETHER A CONTROLLER MAY BE DRIVEN AT ALL is decided from its capability row rather than from its -// route list. A route says the controller ANSWERED over that transport; a capability says a WRITE -// through it was observed to take effect. Only the second licenses driving a host, and the -// distinction is load-bearing here: the Mt. Collins unit answers Redfish paths with 404 while -// serving IPMI, so a route-shaped admission would have to enumerate absent Redfish locators, and a -// capability-shaped one simply reads what was measured. +// The prior type called its positive arm BootHandoffCompleted as soon as the selector text matched +// and `chassis power cycle` exited zero. Execution on mtcollins1 showed that arm firing on every +// failed boot: the controller genuinely held `Force Boot from CD/DVD` and accepted the power action +// while parameter 5 simultaneously requested PC-compatible legacy boot on an aarch64 machine. The +// host then fell through to unanswered PXE and the UEFI shell. The precondition was real; the +// reported effect was not. This module now names only what it can observe: BootControlIssued. + type OobBootHandoffAdmission = OobHandoffAdmitted { route: BmcAccessRoute } | OobHandoffRouteUnobserved @@ -49,11 +39,6 @@ type OobBootHandoffAdmission | OobHandoffPowerControlUnavailable | OobHandoffFirmwareMismatch { observed: BmcFirmwareReleaseIdentity, capability: BmcFirmwareReleaseIdentity } -// The first boot-control route the observation carries, as an Option. The list is folded rather than -// pattern-matched because the surface grammar admits no list patterns — measured, not assumed: a -// match with [] and [first, ..] arms fails to parse with "expected FatArrow, found LBracket". This -// is the same fold shape gunbc.machine_intake_access control_route_evidence_unnamed uses over the -// same field, so the idiom is the corpus's rather than this module's. fn first_observed_boot_control_route(observation: BmcAccessObservation) -> BmcAccessRoute? { fold( observation.boot_control_routes, @@ -65,12 +50,6 @@ fn first_observed_boot_control_route(observation: BmcAccessObservation) -> BmcAc ) } -// The refusals are SEPARATE ARMS rather than one not-capable reason, because they have different -// owners and different repairs. A missing boot-source override is a firmware capability question -// answered by the catalog; a missing power control is the same; an unobserved route means nobody has -// probed this controller yet and the repair is an intake attempt, not a catalog edit. Collapsing -// them would be the state-space conflation DESIGN's failure-mode list names — one symbol standing -// for conditions whose remedies point at different people. fn oob_boot_handoff_admission( observation: BmcAccessObservation, capability_row: BmcFirmwareReleaseCapabilityRow, @@ -91,8 +70,6 @@ fn oob_boot_handoff_admission( } } -// WHETHER AN ADMISSION ADMITS, as its own fn so the handoff's guard is one named question rather -// than a match inlined into an effect sequence. fn oob_handoff_is_admitted(admission: OobBootHandoffAdmission) -> Bool { match admission { OobHandoffAdmitted { route: _ } => true @@ -103,81 +80,56 @@ fn oob_handoff_is_admitted(admission: OobBootHandoffAdmission) -> Bool { } } -// WHAT A HANDOFF ATTEMPT CONCLUDED. BootSelectionNotApplied is the arm this type exists for: the -// controller accepted chassis bootdev and boot parameter 5 did NOT read back the requested device. -// Without it, a handoff whose override silently failed would restart the host into whatever it was -// going to boot anyway and report success — the fabricated-plausible-output failure DESIGN §5 -// forbids, in the one place where it costs a whole install cycle to discover. -// -// PowerCycleRefused is distinct from BootSelectionNotApplied even though both leave the host in the -// wrong state, because the boot selection has by then been APPLIED: the controller is holding a -// next-boot override that nothing has consumed. A caller that retries must know which of the two it -// is looking at, since one needs the selection re-applied and the other does not. -type OobBootHandoffOutcome - = BootHandoffCompleted { selected: NonEmptyStr } - | BootSelectionRefused - | BootSelectionNotApplied { requested: NonEmptyStr, readback: String } - | BootSelectionUnverifiable { requested: NonEmptyStr, readback: String } - | BootSelectionFlagInvalid { requested: NonEmptyStr, readback: String } - | PowerCycleRefused { selected: NonEmptyStr } - | BootHandoffNotAdmitted { admission: OobBootHandoffAdmission } +// WHAT THE CONTROLLER ATTEMPT ESTABLISHED. No arm here says a boot completed. BootControlIssued +// establishes only that the complete typed selection read back and the power command was accepted. +// A caller that needs a boot postcondition must join this to host-produced execution evidence. +type OobBootControlOutcome + = BootControlIssued { selection: IpmiBootSelection } + | BootSelectionRefused { selection: IpmiBootSelection } + | BootSelectionNotApplied { selection: IpmiBootSelection, readback: String } + | BootSelectionUnverifiable { selection: IpmiBootSelection, readback: String } + | BootSelectionFlagInvalid { selection: IpmiBootSelection, readback: String } + | BootSelectionFirmwareModeMismatch { selection: IpmiBootSelection, readback: String } + | BootSelectionPersistenceMismatch { selection: IpmiBootSelection, readback: String } + | PowerCycleRefused { selection: IpmiBootSelection } + | BootControlNotAdmitted { admission: OobBootHandoffAdmission } -// WHAT A BOOT-PARAMETER-5 READ-BACK ESTABLISHED. Three outcomes, because they have three different -// remedies and collapsing them is what made the previous form unsafe. -// -// THE PREVIOUS FORM WAS A SUBSTRING TEST AND IT ACCEPTED AN INVALID OVERRIDE. `chassis bootparam -// get 5` renders a block of boot flags, and a controller can answer with BOTH of these lines at -// once: -// -// Boot Flag Invalid -// Boot Device Selector : Force PXE -// -// That is a documented output shape, not a contrived one, and it means the controller is reporting -// the selector it holds WHILE saying the flags are not valid. A `contains(expected)` test sees -// "Force PXE", answers true, and the handoff proceeds to power-cycle a machine whose override will -// not be honoured — producing exactly the wasted boot cycle reported as success that the -// select-verify-restart ordering exists to prevent. The verification was the weakest link in a -// sequence built around it. -// -// THE SUCCESS FLAG IS CHECKED FIRST, AND SEPARATELY. The previous form applied the predicate to -// `readback.stdout` without ever consulting `readback.success`, so a failed read whose output -// happened to carry the expected words would verify. A read that did not complete establishes -// nothing about the controller's state, which is a different fact from a read that completed and -// disagreed. +// PARAMETER 5 IS A PRODUCT TYPE, NOT A SELECTOR STRING. The read-back has four independent axes: +// validity, device, firmware mode, and persistence. All four must agree before the power action is +// reachable. The order is deliberate: invalid flags dominate every apparent value; then the +// selector, mode and persistence each name the first disagreement a retry must repair. type BootReadbackVerdict = BootReadbackConfirmed | BootReadbackFlagInvalid - | BootReadbackSelectorAbsent - -// THE INVALID-FLAG MARKER IS AN UPSTREAM RENDERING, carried as a row rather than inlined so the one -// string this judgment turns on is nameable. ipmitool prints it inside the parameter-5 flag block. -data ipmi_boot_flag_invalid_rendering: NonEmptyStr = "Boot Flag Invalid" + | BootReadbackSelectorMismatch + | BootReadbackFirmwareModeMismatch + | BootReadbackPersistenceMismatch -// ORDER MATTERS AND IS NOT INTERCHANGEABLE: invalidity is checked BEFORE the selector, because a -// block carrying both is invalid, not confirmed. Checking the selector first would return the old -// behaviour with extra steps. -fn boot_readback_verdict(readback: String, expected_rendering: NonEmptyStr) -> BootReadbackVerdict { - if readback |> contains(ipmi_boot_flag_invalid_rendering as String) { +fn boot_readback_verdict(readback: String, selection: IpmiBootSelection) -> BootReadbackVerdict { + if readback |> contains(selection.expected_flag_rendering as String) == false { BootReadbackFlagInvalid - } else if readback |> contains(expected_rendering as String) { - BootReadbackConfirmed + } else if readback |> contains(selection.expected_device_rendering as String) == false { + BootReadbackSelectorMismatch + } else if readback |> contains(selection.expected_mode_rendering as String) == false { + BootReadbackFirmwareModeMismatch + } else if readback |> contains(selection.expected_persistence_rendering as String) == false { + BootReadbackPersistenceMismatch } else { - BootReadbackSelectorAbsent + BootReadbackConfirmed } } -// THE RESTART LIVES BEHIND THE CONFIRMED ARM, which is what makes select-verify-restart structural -// rather than merely sequential. The power cycle is not a statement that follows a check; it is the -// body of the one verdict that permits it, so a future edit cannot reorder a refusal past it or fall -// through to it. The previous form eliminated the verdict for its refusals and then continued to the -// cycle, which is the same ordering held by convention instead of by shape. +// THE POWER ACTION IS REACHABLE ONLY THROUGH THE FOUR-AXIS CONFIRMED ARM. Its positive result is +// deliberately named ISSUED rather than completed: a controller response cannot testify that the +// host loaded an image, and SOL is not promoted into that role either. The delivered artifact's +// own receipt is the postcondition producer. func oob_power_cycle_after_confirmed_selection( bmc_host: NonEmptyStr, username: NonEmptyStr, password_file: NonEmptyStr, - device: NonEmptyStr, + selection: IpmiBootSelection, power_action: NonEmptyStr, -) -> OobBootHandoffOutcome +) -> OobBootControlOutcome uses net: std.resources.Network { cycle = diagnostic.ipmi.Tool.ChassisPowerControl( @@ -187,48 +139,39 @@ func oob_power_cycle_after_confirmed_selection( action: power_action, ) return if cycle.success { - BootHandoffCompleted { selected: device } + BootControlIssued { selection: selection } } else { - PowerCycleRefused { selected: device } + PowerCycleRefused { selection: selection } } } -// THE HANDOFF ITSELF, and the ordering is the point: SELECT, VERIFY, THEN RESTART. A restart issued -// before the selection is verified converts a silently-refused override into a wasted boot cycle -// that reports success, which is the one failure this whole module exists to make unrepresentable. -// So the power cycle is reachable only through the arm where the read-back already matched. -// -// THE CREDENTIAL IS TAKEN AS A FILE PATH, NOT AS A SECRET VALUE. This func does not read, decrypt or -// materialize anything: it receives the path to a file some caller wrote and hands that path to -// ipmitool. Materialization is a separate concern with its own authority (gunbc.auth.materialized_secret), -// and a func that both resolved a secret and drove a controller would fuse two facts that rotate on -// different clocks — which matters here because the operator's ruling is that the factory credential -// is rotated DURING converge, so the value behind this path changes mid-program while the path does not. -func oob_boot_handoff( +// SELECT, VERIFY THE WHOLE PARAMETER, THEN RESTART. The selection is sole-constructor upstream: +// current aarch64 callers can obtain only UEFI + one-shot values, so the executed failure state +// `(Aarch64, Legacy, Cdrom)` cannot be authored and no raw `options=` string crosses this boundary. +func oob_boot_control_issue( observation: BmcAccessObservation, capability_row: BmcFirmwareReleaseCapabilityRow, username: NonEmptyStr, password_file: NonEmptyStr, - device: NonEmptyStr, - expected_rendering: NonEmptyStr, + selection: IpmiBootSelection, power_action: NonEmptyStr, -) -> OobBootHandoffOutcome +) -> OobBootControlOutcome uses net: std.resources.Network { let admission = oob_boot_handoff_admission(observation: observation, capability_row: capability_row) if oob_handoff_is_admitted(admission: admission) == false { - return BootHandoffNotAdmitted { admission: admission } + return BootControlNotAdmitted { admission: admission } } let bmc_host = observation.endpoint.host - set = diagnostic.ipmi.Tool.ChassisBootDev( + set = diagnostic.ipmi.BootSelection.Set( bmc_host: bmc_host, username: username, password_file: password_file, - device: device, + selection: selection, ) if set.success == false { - return BootSelectionRefused + return BootSelectionRefused { selection: selection } } readback = diagnostic.ipmi.Tool.ChassisBootParamGet( @@ -238,19 +181,47 @@ func oob_boot_handoff( parameter: "5", ) if readback.success == false { - return BootSelectionUnverifiable { requested: device, readback: readback.stdout } + return BootSelectionUnverifiable { selection: selection, readback: readback.stdout } } - return match boot_readback_verdict(readback: readback.stdout, expected_rendering: expected_rendering) { - BootReadbackFlagInvalid => BootSelectionFlagInvalid { requested: device, readback: readback.stdout } - BootReadbackSelectorAbsent => BootSelectionNotApplied { requested: device, readback: readback.stdout } + return match boot_readback_verdict(readback: readback.stdout, selection: selection) { + BootReadbackFlagInvalid => + BootSelectionFlagInvalid { selection: selection, readback: readback.stdout } + BootReadbackSelectorMismatch => + BootSelectionNotApplied { selection: selection, readback: readback.stdout } + BootReadbackFirmwareModeMismatch => + BootSelectionFirmwareModeMismatch { selection: selection, readback: readback.stdout } + BootReadbackPersistenceMismatch => + BootSelectionPersistenceMismatch { selection: selection, readback: readback.stdout } BootReadbackConfirmed => oob_power_cycle_after_confirmed_selection( bmc_host: bmc_host, username: username, password_file: password_file, - device: device, + selection: selection, power_action: power_action, ) } } + +fn oob_boot_control_outcome_label(outcome: OobBootControlOutcome) -> NonEmptyStr { + match outcome { + BootControlIssued { selection: s } => + join(["issued:", ipmi_boot_selection_label(selection: s) as String], "") as NonEmptyStr + BootSelectionRefused { selection: s } => + join(["selection-refused:", ipmi_boot_selection_label(selection: s) as String], "") as NonEmptyStr + BootSelectionNotApplied { selection: s, readback: _ } => + join(["selector-mismatch:", ipmi_boot_selection_label(selection: s) as String], "") as NonEmptyStr + BootSelectionUnverifiable { selection: s, readback: _ } => + join(["readback-unverifiable:", ipmi_boot_selection_label(selection: s) as String], "") as NonEmptyStr + BootSelectionFlagInvalid { selection: s, readback: _ } => + join(["flag-invalid:", ipmi_boot_selection_label(selection: s) as String], "") as NonEmptyStr + BootSelectionFirmwareModeMismatch { selection: s, readback: _ } => + join(["firmware-mode-mismatch:", ipmi_boot_selection_label(selection: s) as String], "") as NonEmptyStr + BootSelectionPersistenceMismatch { selection: s, readback: _ } => + join(["persistence-mismatch:", ipmi_boot_selection_label(selection: s) as String], "") as NonEmptyStr + PowerCycleRefused { selection: s } => + join(["power-refused:", ipmi_boot_selection_label(selection: s) as String], "") as NonEmptyStr + BootControlNotAdmitted { admission: _ } => "not-admitted" + } +} diff --git a/dag/test/claim/machine_intake/boot_control_grounding_witness_test.dag b/dag/test/claim/machine_intake/boot_control_grounding_witness_test.dag new file mode 100644 index 00000000000..9bfad4b9463 --- /dev/null +++ b/dag/test/claim/machine_intake/boot_control_grounding_witness_test.dag @@ -0,0 +1,199 @@ +module test.claim.machine_intake.boot_control_grounding_witness_test + +import std.types { Bool, Int, String } +import extdeps.bmc.ipmi_boot_selection { + IpmiBootCdrom, + aarch64_uefi_once_boot_selection, +} +import gunbc.machine_intake_oob_boot_handoff { + BootReadbackConfirmed, + BootReadbackFirmwareModeMismatch, + BootReadbackFlagInvalid, + BootReadbackPersistenceMismatch, + BootReadbackSelectorMismatch, + boot_readback_verdict, +} +import gunbc.machine_intake_megarac_media_attach { + PresentedMediaConnecting, + PresentedMediaConnectionDenied, + PresentedMediaIdle, + PresentedMediaLoginFailed, + PresentedMediaMaxSessionReached, + PresentedMediaPermissionDenied, + PresentedMediaReady, + PresentedMediaSessionIndexUnavailable, + PresentedMediaStopped, + presented_media_standing, + start_media_body, +} +import gunbc.compile_diagnostic_census { + CensusNotRunnable, + CensusObserved, + census_rows_of_class, + census_total_count, + compile_dag_diagnostic_census, +} + +fn valid_cd_efi_once_readback() -> String { + "Boot Flag Valid\nOptions apply to only next boot\nBIOS EFI boot\nBoot Device Selector : Force Boot from CD/DVD" +} + +test fn all_four_boot_axes_confirm() -> Bool { + let selection = aarch64_uefi_once_boot_selection(device: IpmiBootCdrom) + match boot_readback_verdict(readback: valid_cd_efi_once_readback(), selection: selection) { + BootReadbackConfirmed => true + _ => false + } +} + +test fn legacy_beside_cdrom_refuses_as_mode_mismatch() -> Bool { + let selection = aarch64_uefi_once_boot_selection(device: IpmiBootCdrom) + match boot_readback_verdict( + readback: "Boot Flag Valid\nOptions apply to only next boot\nBIOS PC Compatible (legacy) boot\nBoot Device Selector : Force Boot from CD/DVD", + selection: selection, + ) { + BootReadbackFirmwareModeMismatch => true + _ => false + } +} + +test fn persistent_beside_one_shot_refuses() -> Bool { + let selection = aarch64_uefi_once_boot_selection(device: IpmiBootCdrom) + match boot_readback_verdict( + readback: "Boot Flag Valid\nOptions apply to all future boots\nBIOS EFI boot\nBoot Device Selector : Force Boot from CD/DVD", + selection: selection, + ) { + BootReadbackPersistenceMismatch => true + _ => false + } +} + +test fn invalid_flag_dominates_matching_other_axes() -> Bool { + let selection = aarch64_uefi_once_boot_selection(device: IpmiBootCdrom) + match boot_readback_verdict( + readback: "Boot Flag Invalid\nOptions apply to only next boot\nBIOS EFI boot\nBoot Device Selector : Force Boot from CD/DVD", + selection: selection, + ) { + BootReadbackFlagInvalid => true + _ => false + } +} + +test fn wrong_selector_refuses() -> Bool { + let selection = aarch64_uefi_once_boot_selection(device: IpmiBootCdrom) + match boot_readback_verdict( + readback: "Boot Flag Valid\nOptions apply to only next boot\nBIOS EFI boot\nBoot Device Selector : Force PXE", + selection: selection, + ) { + BootReadbackSelectorMismatch => true + _ => false + } +} + +test fn typed_aarch64_selection_emits_efi_once_without_persistent() -> Bool { + let selection = aarch64_uefi_once_boot_selection(device: IpmiBootCdrom) + selection.options_wire == "options=efiboot" + && selection.expected_mode_rendering == "BIOS EFI boot" + && selection.expected_persistence_rendering == "Options apply to only next boot" +} + +fn status_body(status: String, session_index: String) -> String { + join([ + "[{\"image_name\":\"census.iso\",\"media_type\":1,\"session_index\":", + session_index, + ",\"redirection_status\":", + status, + "}]", + ], "") +} + +test fn status_zero_is_idle() -> Bool { + match presented_media_standing(body: status_body(status: "0", session_index: "255"), image_name: "census.iso") { + PresentedMediaIdle => true + _ => false + } +} + +test fn status_one_with_bound_session_is_ready() -> Bool { + match presented_media_standing(body: status_body(status: "1", session_index: "0"), image_name: "census.iso") { + PresentedMediaReady { session_index: idx } => idx == "0" + _ => false + } +} + +test fn status_one_with_na_session_refuses() -> Bool { + match presented_media_standing(body: status_body(status: "1", session_index: "255"), image_name: "census.iso") { + PresentedMediaSessionIndexUnavailable => true + _ => false + } +} + +test fn status_one_hundred_is_connecting_not_ready() -> Bool { + match presented_media_standing(body: status_body(status: "100", session_index: "255"), image_name: "census.iso") { + PresentedMediaConnecting { session_index: idx } => idx == "255" + _ => false + } +} + +test fn status_two_is_connection_denied() -> Bool { + match presented_media_standing(body: status_body(status: "2", session_index: "255"), image_name: "census.iso") { + PresentedMediaConnectionDenied => true + _ => false + } +} + +test fn status_three_is_login_failed() -> Bool { + match presented_media_standing(body: status_body(status: "3", session_index: "255"), image_name: "census.iso") { + PresentedMediaLoginFailed => true + _ => false + } +} + +test fn status_four_is_max_session_reached() -> Bool { + match presented_media_standing(body: status_body(status: "4", session_index: "255"), image_name: "census.iso") { + PresentedMediaMaxSessionReached => true + _ => false + } +} + +test fn status_five_is_permission_denied() -> Bool { + match presented_media_standing(body: status_body(status: "5", session_index: "255"), image_name: "census.iso") { + PresentedMediaPermissionDenied => true + _ => false + } +} + +test fn unrecognized_status_is_stopped_not_ready() -> Bool { + match presented_media_standing(body: status_body(status: "17", session_index: "255"), image_name: "census.iso") { + PresentedMediaStopped { status: s } => s == "17" + _ => false + } +} + +test fn start_encoder_always_carries_image_redirection() -> Bool { + (start_media_body(image_name: "census.iso", image_index: "0") as String) + |> contains("\"image_redirection\":1") +} + +fn sole_constructor_violations(source: String) -> Int { + match compile_dag_diagnostic_census(source) { + CensusObserved { rows: rows } => + census_total_count(rows: census_rows_of_class(rows: rows, wanted: "SoleConstructorViolation")) + CensusNotRunnable { cause: _ } => 0 - 1 + } +} + +// The red fixture differs from the sanctioned route at the construction site itself. It spells +// Aarch64 + Legacy + CD + Persistent as a cross-module record literal. Its strings are ordinary +// valid source strings; the expected refusal is SoleConstructorViolation, not a parser accident. +data forged_legacy_aarch64_source: String = "module probe_legacy_aarch64_boot\nimport extdeps.bmc.ipmi_boot_selection { IpmiBootSelection, IpmiBootCdrom, IpmiBootLegacy, IpmiBootPersistent }\nimport extdeps.toolchain.types { Aarch64 }\nfn forged() -> IpmiBootSelection {\n IpmiBootSelection {\n architecture: Aarch64,\n device: IpmiBootCdrom,\n firmware_mode: IpmiBootLegacy,\n persistence: IpmiBootPersistent,\n device_wire: \"cdrom\",\n options_wire: \"options=persistent\",\n expected_flag_rendering: \"Boot Flag Valid\",\n expected_device_rendering: \"Force Boot from CD/DVD\",\n expected_mode_rendering: \"BIOS PC Compatible (legacy) boot\",\n expected_persistence_rendering: \"Options apply to all future boots\",\n }\n}\n" + +test fn legacy_cdrom_on_aarch64_is_unconstructible() -> Bool { + sole_constructor_violations(source: forged_legacy_aarch64_source) >= 1 +} + +data sanctioned_aarch64_source: String = "module probe_sanctioned_aarch64_boot\nimport extdeps.bmc.ipmi_boot_selection { IpmiBootCdrom, aarch64_uefi_once_boot_selection }\nfn legal() -> Bool {\n let selection = aarch64_uefi_once_boot_selection(device: IpmiBootCdrom)\n true\n}\n" + +test fn sanctioned_aarch64_constructor_remains_clean() -> Bool { + sole_constructor_violations(source: sanctioned_aarch64_source) == 0 +}