power-on account slice B2: pre-power hpm check firmware readback bound to the admitted attempt

dag/extdeps/bmc/ipmi.dag

@@ -416,6 +416,23 @@ service diagnostic.ipmi.Tool {
     }
   }
 
+  operation HpmCheck {
+    requires Network
+    input { bmc_host: NonEmptyStr, username: NonEmptyStr, password_file: NonEmptyStr, deadline: NonEmptyStr, kill_after: NonEmptyStr }
+    output {
+      stdout: String from "stdout",
+      transport_stderr: String from "stderr",
+      exit_code: Int from "exit_code",
+      success: Bool from "exit_success",
+    }
+    readonly
+    transport shell { argv: ["timeout", "--kill-after", "{kill_after}", "{deadline}", "ipmitool", "-H", "{bmc_host}", "-I", "lanplus", "-U", "{username}", "-f", "{password_file}", "hpm", "check"] }
+    exit {
+      0 => Unit
+      nonzero => String "ipmitool hpm check failed"
+    }
+  }
+
   operation McInfo {
     requires Network
     input { bmc_host: NonEmptyStr, username: NonEmptyStr, password_file: NonEmptyStr, deadline: NonEmptyStr, kill_after: NonEmptyStr }

dag/gunbc/bmc_dry_realization.dag

@@ -27,6 +27,7 @@ import extdeps.bmc.megarac_observed_output {
 import extdeps.languages.json.parse { parse_json_document, JsonDocumentParsed, JsonDocumentUnreadable }
 import gunbc.machine_intake_megarac_media_attach { json_string_member, json_number_member }
 import extdeps.bmc.ipmitool_observed_output {
+  ipmitool_hpm_check_bmc0_32,
   ipmitool_mc_info_mt_collins,
   ipmitool_bootparam5_no_override, ipmitool_bootparam5_cdrom_efi_next_boot, ipmitool_bootdev_cdrom_reply,
   ipmitool_sel_elist_line,
@@ -117,6 +118,12 @@ fn bmc_mc_info_reply(world: BmcWorld, call: OperationCall) -> BmcReply {
   BmcReplied { stdout: ipmitool_mc_info_mt_collins, world: world }
 }
 
+// THE COMPONENT TABLE AS THE CONTROLLER PRINTED IT: the one retained capture, a layout fixture of
+// BMC 0.32 (extdeps.bmc.ipmitool_observed_output ipmitool_hpm_check_bmc0_32), not a modeled version.
+fn bmc_hpm_check_reply(world: BmcWorld, call: OperationCall) -> BmcReply {
+  BmcReplied { stdout: ipmitool_hpm_check_bmc0_32, world: world }
+}
+
 // One IPMI round trip takes one virtual second.
 fn bmc_lift<S>(get: fn(S) -> BmcWorld, put: fn(S, BmcWorld) -> S, reply: fn(BmcWorld, OperationCall) -> BmcReply) -> fn(S, OperationCall) -> OperationStep<S> {
   fn(state, call) {
@@ -140,6 +147,7 @@ fn bmc_bindings<S>(get: fn(S) -> BmcWorld, put: fn(S, BmcWorld) -> S) -> List<Op
     OperationBinding { at: bmc_ipmi_operation(operation: "SelListAuthenticated"), handler: bmc_lift(get: get, put: put, reply: bmc_sel_elist_reply) },
     OperationBinding { at: bmc_ipmi_operation(operation: "SelListAuthenticatedCached"), handler: bmc_lift(get: get, put: put, reply: bmc_sel_elist_reply) },
     OperationBinding { at: bmc_ipmi_operation(operation: "McInfo"), handler: bmc_lift(get: get, put: put, reply: bmc_mc_info_reply) },
+    OperationBinding { at: bmc_ipmi_operation(operation: "HpmCheck"), handler: bmc_lift(get: get, put: put, reply: bmc_hpm_check_reply) },
   ]
 }
 

dag/gunbc/host/host_boot_attempt_admission.dag

@@ -40,8 +40,9 @@ import gunbc.machine_intake_mtcollins1_power_on_account {
   StimulusRequest, StimulusRequested, NoStimulusRequested, StimulusRequestNotRecorded,
   StimulusApplication, StimulusAppliedByReceipt, StimulusApplicationNotRecorded,
   SocketCpuRow, SlotRow, PopulationReading, PopulationOperatorAttested, PopulationNotRecorded,
-  FirmwareReadbacksNotRecorded,
+  FirmwareReadbacks, FirmwareReadBeforeActuation, FirmwareReadbacksNotRecorded, FirmwareReadbackRow,
 }
+import extdeps.bmc.ipmitool_hpm_check { HpmCheckTable, HpmCheckRead, HpmCheckUpgradeVariant, HpmCheckUnreadable, hpm_version_cell_text }
 
 // THE ADMISSION OF ONE BOOT ATTEMPT'S CONFIGURATION RECEIPT, host-generic over a gunbc.managed_host
 // ManagedHostBinding (docs/plans/power-on-sequence-model.md section 12; Q5 decided by eager-gull-22
@@ -802,7 +803,8 @@ fn boot_attempt_receipt_not_named_reason() -> NonEmptyStr {
   ], "") as NonEmptyStr
 }
 
-data boot_attempt_firmware_frontier: NonEmptyStr = "the pre-power-on firmware readback is slice B2 of docs/plans/power-on-sequence-model.md section 12 and is not read yet"
+// BEFORE THE PRE-POWER READS ARE JOINED (attempt_configuration_with_pre_power), firmware is not recorded.
+data boot_attempt_firmware_frontier: NonEmptyStr = "the pre-power-on firmware readback is joined after admission and was not taken for this attempt"
 
 fn receipt_label(e: ReceiptEvidence) -> NonEmptyStr {
   join([e.path as String, "@", e.commit as String, " (", digest_label(d: e.digest) as String, ")"], "") as NonEmptyStr
@@ -899,3 +901,86 @@ fn cas_store_failure_text(cause: CasStoreFailure) -> String {
     CasGenerationSpaceExhausted { head: h } => join(["the slot's generation space is exhausted at ", to_string(cas_generation_count(g: h))], "")
   }
 }
+
+// ── THE PRE-POWER READ, bound to its attempt where it is taken ───────────────────────────────────
+// A reading is the attempt's only if the read was taken FOR that attempt: the production read mints a
+// PrePowerFirmwareReading from the attempt's BootAttemptClearance, and the join keeps that identity and
+// refuses a configuration of any other attempt or host. Nothing re-labels a reading.
+
+// THE TABLE'S ACTIVE CELLS, AS RENDERED (the auxiliary bytes have no public decode here). A pure
+// classifier: it carries no attempt and no observed standing, so it cannot enter a configuration.
+type HpmFirmwareProjection
+  = HpmFirmwareRows { rows: List<FirmwareReadbackRow> }
+  | HpmFirmwareUnreadable { reason: NonEmptyStr }
+
+fn hpm_firmware_projection(table: HpmCheckTable) -> HpmFirmwareProjection {
+  match table {
+    HpmCheckRead { rows: rs } => HpmFirmwareRows { rows: map(rs, r => FirmwareReadbackRow { component: r.name, version: hpm_version_cell_text(c: r.active) as NonEmptyStr }) }
+    HpmCheckUpgradeVariant { header: h } => HpmFirmwareUnreadable { reason: concat("hpm check printed the upgrade-progress table, not the component properties: ", h as String) as NonEmptyStr }
+    HpmCheckUnreadable { detail: d } => HpmFirmwareUnreadable { reason: concat("hpm check output is unreadable: ", d as String) as NonEmptyStr }
+  }
+}
+
+type PrePowerFirmwareReading sole_constructor {
+  host: HostIdentity
+  attempt: NonEmptyStr
+  source: NonEmptyStr
+  rows: List<FirmwareReadbackRow>
+}
+
+type PrePowerFirmware
+  = PrePowerFirmwareRead { reading: PrePowerFirmwareReading }
+  | PrePowerFirmwareUnread { reason: NonEmptyStr }
+
+// THE ATTEMPT A CLEARANCE ADMITTED: the receipt's attempt (the dispatch nonce) when one was admitted,
+// otherwise the run's own identity. attempt_configuration_receipt labels the configuration the same way.
+fn cleared_attempt(clearance: BootAttemptClearance, run_attempt: NonEmptyStr) -> NonEmptyStr {
+  match clearance.source {
+    ConfigurationReceiptNotNamed => run_attempt
+    ConfigurationReceiptAdmitted { receipt: r, slot: _ } => r.plan.attempt
+  }
+}
+
+// THE PRODUCTION READ'S BINDING: the reading belongs to the host and attempt the clearance admitted.
+fn pre_power_firmware_observed(clearance: BootAttemptClearance, run_attempt: NonEmptyStr, table: HpmCheckTable, source: NonEmptyStr) -> PrePowerFirmware
+  admit_callers: [
+    decl_ref(module_path: "gunbc.machine_intake_mtcollins1_boot_diagnostic_bundle", decl_name: "mtcollins1_boot_hpm_check"),
+  ]
+{
+  pre_power_firmware_minted(host: clearance.host, attempt: cleared_attempt(clearance: clearance, run_attempt: run_attempt), table: table, source: source)
+}
+
+// THE ONE MINT OF A READING, reachable only from the production binding above and from the witness
+// that exercises the join's cross-attempt refusal.
+fn pre_power_firmware_minted(host: HostIdentity, attempt: NonEmptyStr, table: HpmCheckTable, source: NonEmptyStr) -> PrePowerFirmware
+  admit_callers: [
+    decl_ref(module_path: "gunbc.host_boot_attempt_admission", decl_name: "pre_power_firmware_observed"),
+    decl_ref(module_path: "test.claim.host_boot_attempt_admission_witness", decl_name: "a_firmware_reading_joins_only_the_attempt_it_was_taken_for"),
+  ]
+{
+  match hpm_firmware_projection(table: table) {
+    HpmFirmwareUnreadable { reason: r } => PrePowerFirmwareUnread { reason: r }
+    HpmFirmwareRows { rows: rs } => PrePowerFirmwareRead { reading: PrePowerFirmwareReading { host: host, attempt: attempt, source: source, rows: rs } }
+  }
+}
+
+fn attempt_configuration_with_pre_power(c: AttemptConfigurationReceipt, firmware: PrePowerFirmware) -> AttemptConfigurationReceipt {
+  AttemptConfigurationReceipt {
+    subject: c.subject,
+    attempt: c.attempt,
+    expected: c.expected,
+    requested: c.requested,
+    applied: c.applied,
+    cpus: c.cpus,
+    dimms: c.dimms,
+    firmware: match firmware {
+      PrePowerFirmwareUnread { reason: r } => FirmwareReadbacksNotRecorded { reason: r }
+      PrePowerFirmwareRead { reading: r } =>
+        if (r.attempt as String) == (c.attempt as String) && (r.host as String) == (c.subject as String) {
+          FirmwareReadBeforeActuation { attempt: r.attempt, source: r.source, rows: r.rows }
+        } else {
+          FirmwareReadbacksNotRecorded { reason: join(["a firmware reading taken for attempt ", r.attempt as String, " on ", r.host as String, " is not this attempt's (", c.attempt as String, " on ", c.subject as String, "); it was refused, not relabelled"], "") as NonEmptyStr }
+        }
+    },
+  }
+}

dag/gunbc/machine_intake/mtcollins1_boot_diagnostic_bundle.dag

@@ -1,5 +1,9 @@
 module gunbc.machine_intake_mtcollins1_boot_diagnostic_bundle
 
+import extdeps.bmc.ipmitool_hpm_check { hpm_check_table_of }
+import gunbc.host_boot_attempt_admission {
+  PrePowerFirmware, PrePowerFirmwareUnread, pre_power_firmware_observed, BootAttemptClearance,
+}
 import std.decl_ref { decl_ref }
 import std.types { Bool, Int, List, NonEmptyStr, Secret, String }
 import std.nat { Nat }
@@ -2529,3 +2533,22 @@ fn mtcollins1_boot_outcome_after_bundle(outcome: ProcessExit, bundle: MtCollins1
       }
   }
 }
+
+// ── THE PRE-POWER READS (gunbc.host_boot_attempt_admission attempt_configuration_with_pre_power) ──
+// Taken by the boot run after admission and before actuation. hpm check's table is parsed by
+// extdeps.bmc.ipmitool_hpm_check; a failed read carries the controller's own cause.
+fn mtcollins1_boot_hpm_check(username: NonEmptyStr, password_file: NonEmptyStr, clearance: BootAttemptClearance, run_attempt: NonEmptyStr) -> PrePowerFirmware {
+  let at = clock_now_probed_at_or_unknown()
+  let r = diagnostic.ipmi.Tool.HpmCheck(
+    bmc_host: mtcollins1_endpoint.host,
+    username: username,
+    password_file: password_file,
+    deadline: coreutils_duration_operand(d: mtcollins1_boot_ipmi_read_deadline) as NonEmptyStr,
+    kill_after: coreutils_duration_operand(d: mtcollins1_boot_ipmi_kill_after) as NonEmptyStr,
+  )
+  if r.success {
+    pre_power_firmware_observed(clearance: clearance, run_attempt: run_attempt, table: hpm_check_table_of(stdout: r.stdout), source: join(["ipmitool hpm check on ", mtcollins1_endpoint.host as String, " at ", at as String], "") as NonEmptyStr)
+  } else {
+    PrePowerFirmwareUnread { reason: concat("hpm check was not read: ", bmc_read_cause_text(cause: bmc_ipmitool_read_cause(endpoint: mtcollins1_ipmi_endpoint(), at: at, exit_code: r.exit_code, stderr: r.transport_stderr))) as NonEmptyStr }
+  }
+}

dag/gunbc/machine_intake/mtcollins1_boot_run.dag

@@ -88,15 +88,16 @@ import gunbc.managed_host {
 import extdeps.bmc.ipmi_boot_selection { IpmiBootSelection }
 import extdeps.bmc.ipmi_chassis_control { ChassisPowerObservation, chassis_observation_text }
 import gunbc.host_boot_attempt_admission {
-  BootAttemptCleared, BootAttemptRefused, admit_boot_attempt, attempt_configuration_receipt,
+  BootAttemptCleared, BootAttemptRefused, BootAttemptClearance, admit_boot_attempt, attempt_configuration_receipt,
+  attempt_configuration_with_pre_power, PrePowerFirmwareUnread,
   attempt_configuration_not_recorded, attempt_configuration_refused, attempt_receipt_refusal_text,
 }
 import gunbc.machine_intake_mtcollins1_power_on_account { AttemptConfigurationReceipt, CarrierRead, CarrierReadEmpty, CarrierPartial, CarrierRefused, CarrierNotTaken, mtcollins1_power_on_account_notes, carrier_text, carrier_standing_text }
 import gunbc.machine_intake_mtcollins1_boot_diagnostic_bundle {
   MtCollins1BootDiagnosticBundle, SelSnapshotReading, SelSnapshotNotTaken, inventory_not_taken,
   SdrCacheReading, SdrCacheNotTaken, mtcollins1_boot_sdr_cache,
   SensorsNotTaken, mtcollins1_boot_sensors, SmproProbed, SmproNotTaken,
-  mtcollins1_boot_sel_snapshot, mtcollins1_boot_inventory, mtcollins1_boot_console,
+  mtcollins1_boot_sel_snapshot, mtcollins1_boot_inventory, mtcollins1_boot_hpm_check, mtcollins1_boot_console,
   mtcollins1_boot_write_bundle, mtcollins1_boot_outcome_after_bundle, mtcollins1_boot_findings, harness_finding_text, bundle_write_receipt_line,
   mtcollins1_boot_diagnostics_allowance, AttemptIdentityReading, AttemptRunId, AttemptIdentityUnavailable, attempt_identity_text,
   SmproReading, BootParam5Reading, BootParam5NotTaken, BootParam5Read, BootParam5Unread, PowerAfterUnobserved, MtCollins1BootRunRecord, run_record_not_taken, MtCollins1MediaAttachRecord, MediaAttachNotAttempted, MtCollins1HandoffMedia, recheck_text, MtCollins1EndMedia, EndMediaNotTaken, EndMediaObserved, HandoffMediaNotReached, HandoffMediaWithheldAtRecheck, HandoffMediaAttempted, HandoffConfirmed, HandoffAttemptedUnconfirmed, end_media_is_owed, media_loss_after_handoff, outcome_attributing_media_loss, mtcollins1_boot_param5, mtcollins1_boot_chassis_power,
@@ -2510,7 +2511,7 @@ fn mtcollins1_boot_under_live_unit_hold(
           }
         }
         BootAttemptCleared { clearance: clearance } => {
-          let configuration = attempt_configuration_receipt(clearance: clearance, attempt: run_id)
+          let configuration = mtcollins1_boot_pre_power(configuration: attempt_configuration_receipt(clearance: clearance, attempt: run_id), clearance: clearance, run_attempt: run_id, password_file: password_file)
           let taken = baseline()
           let actuation = mtcollins1_boot_actuate_held(proof: p, subject: subject, password_file: password_file, run_id: run_id, sol_pid_path: sol_pid_path, sol_capture_path: sol_capture_path, resolve_toolchain: resolve_toolchain)
           MtCollins1HeldBoot { actuation: actuation, configuration: configuration, baseline: taken }
@@ -2519,6 +2520,20 @@ fn mtcollins1_boot_under_live_unit_hold(
   }
 }
 
+// THE PRE-POWER READ, AFTER ADMISSION AND BEFORE ANY WRITE: the firmware each component runs (hpm
+// check), joined to the frozen configuration by gunbc.host_boot_attempt_admission.
+fn mtcollins1_boot_pre_power(configuration: AttemptConfigurationReceipt, clearance: BootAttemptClearance, run_attempt: NonEmptyStr, password_file: String) -> AttemptConfigurationReceipt {
+  match mtcollins1_bmc_username {
+    Absent => attempt_configuration_with_pre_power(c: configuration, firmware: PrePowerFirmwareUnread { reason: "mtcollins1's BMC is not BmcSecured, so no account is modeled to read it with" })
+    Present { value: user } =>
+      if password_file == "" {
+        attempt_configuration_with_pre_power(c: configuration, firmware: PrePowerFirmwareUnread { reason: "no BMC credential path is bound" })
+      } else {
+        attempt_configuration_with_pre_power(c: configuration, firmware: mtcollins1_boot_hpm_check(username: user, password_file: password_file as NonEmptyStr, clearance: clearance, run_attempt: run_attempt))
+      }
+  }
+}
+
 fn mtcollins1_boot_baseline(username: NonEmptyStr, password_file: NonEmptyStr) -> MtCollins1BootBaseline {
   let sdr = mtcollins1_boot_sdr_cache(username: username, password_file: password_file, path: concat(password_file as String, mtcollins1_boot_sdr_cache_suffix) as NonEmptyStr)
   MtCollins1BootBaseline { sdr: sdr, sel_before: mtcollins1_boot_sel_snapshot(username: username, password_file: password_file, sdr: sdr) }

dag/gunbc/machine_intake/mtcollins1_power_on_account.dag

@@ -125,7 +125,7 @@ type FirmwareReadbackRow {
 }
 
 type FirmwareReadbacks
-  = FirmwareReadBeforeActuation { rows: List<FirmwareReadbackRow> }
+  = FirmwareReadBeforeActuation { attempt: NonEmptyStr, source: NonEmptyStr, rows: List<FirmwareReadbackRow> }
   | FirmwareReadbacksNotRecorded { reason: NonEmptyStr }
 
 // THE EXPECTED TOPOLOGY THIS ATTEMPT IS JUDGED AGAINST, recorded for the attempt or not at all: a
@@ -987,7 +987,7 @@ fn configuration_questions(c: AttemptConfigurationReceipt) -> List<OpenQuestion>
   concat(match c.applied { StimulusAppliedByReceipt { receipt: _, attested_by: _ } => [] StimulusApplicationNotRecorded { reason: _ } => [OpenQuestion { subject: PlatformBmc, question: ConfigurationNotRecorded { field: ConfiguredStimulus } }] },
   concat(population_question(r: c.cpus, field: ConfiguredCpuPopulation),
   concat(population_question(r: c.dimms, field: ConfiguredDimmPopulation),
-    match c.firmware { FirmwareReadBeforeActuation { rows: _ } => [] FirmwareReadbacksNotRecorded { reason: _ } => [OpenQuestion { subject: PlatformBmc, question: ConfigurationNotRecorded { field: ConfiguredFirmware } }] }))))
+    match c.firmware { FirmwareReadBeforeActuation { attempt: _, source: _, rows: _ } => [] FirmwareReadbacksNotRecorded { reason: _ } => [OpenQuestion { subject: PlatformBmc, question: ConfigurationNotRecorded { field: ConfiguredFirmware } }] }))))
 }
 
 fn population_question<T>(r: PopulationReading<T>, field: ConfigurationField) -> List<OpenQuestion> {