diff --git a/dag/extdeps/bmc/ipmi.dag b/dag/extdeps/bmc/ipmi.dag index b2c47aad375..1546dd86933 100644 --- a/dag/extdeps/bmc/ipmi.dag +++ b/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 } diff --git a/dag/gunbc/bmc_dry_realization.dag b/dag/gunbc/bmc_dry_realization.dag index 7f7fa113851..5fe9b888213 100644 --- a/dag/gunbc/bmc_dry_realization.dag +++ b/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(get: fn(S) -> BmcWorld, put: fn(S, BmcWorld) -> S, reply: fn(BmcWorld, OperationCall) -> BmcReply) -> fn(S, OperationCall) -> OperationStep { fn(state, call) { @@ -140,6 +147,7 @@ fn bmc_bindings(get: fn(S) -> BmcWorld, put: fn(S, BmcWorld) -> S) -> List 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 } + | 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 +} + +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 } + } + }, + } +} diff --git a/dag/gunbc/machine_intake/mtcollins1_boot_diagnostic_bundle.dag b/dag/gunbc/machine_intake/mtcollins1_boot_diagnostic_bundle.dag index 677e58c13dd..2bcc3c3a907 100644 --- a/dag/gunbc/machine_intake/mtcollins1_boot_diagnostic_bundle.dag +++ b/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 } + } +} diff --git a/dag/gunbc/machine_intake/mtcollins1_boot_run.dag b/dag/gunbc/machine_intake/mtcollins1_boot_run.dag index caeaa80ee57..431a67fbc76 100644 --- a/dag/gunbc/machine_intake/mtcollins1_boot_run.dag +++ b/dag/gunbc/machine_intake/mtcollins1_boot_run.dag @@ -88,7 +88,8 @@ 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 } @@ -96,7 +97,7 @@ 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) } diff --git a/dag/gunbc/machine_intake/mtcollins1_power_on_account.dag b/dag/gunbc/machine_intake/mtcollins1_power_on_account.dag index ea7594c0f55..06597e2de9c 100644 --- a/dag/gunbc/machine_intake/mtcollins1_power_on_account.dag +++ b/dag/gunbc/machine_intake/mtcollins1_power_on_account.dag @@ -125,7 +125,7 @@ type FirmwareReadbackRow { } type FirmwareReadbacks - = FirmwareReadBeforeActuation { rows: List } + = FirmwareReadBeforeActuation { attempt: NonEmptyStr, source: NonEmptyStr, rows: List } | 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 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(r: PopulationReading, field: ConfigurationField) -> List { diff --git a/dag/test/claim/host/host_boot_attempt_admission_witness_test.dag b/dag/test/claim/host/host_boot_attempt_admission_witness_test.dag index 45e33077920..2414dde5b5d 100644 --- a/dag/test/claim/host/host_boot_attempt_admission_witness_test.dag +++ b/dag/test/claim/host/host_boot_attempt_admission_witness_test.dag @@ -1,6 +1,7 @@ module test.claim.host_boot_attempt_admission_witness import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import v2.std.algebra { any } import std.types { Bool, Int, List, NonEmptyStr, String } import v2.std.optional { Present, Absent } import extdeps.crypto.hash { sha256_digest } @@ -9,11 +10,15 @@ import extdeps.ampere.mt_collins_getting_started_guide.dimm_layout { dimm_figure import product.placement_supply { HostIdentity } import gunbc.fleet_intent_network { operator_host_mtcollins1 } import gunbc.machine_intake_mtcollins1_power_on_account { + AttemptConfigurationReceipt, FirmwareReadbacks, FirmwareReadBeforeActuation, FirmwareReadbacksNotRecorded, ExpectedSockets, ExpectedTopologyNotRecorded, StimulusRequested, NoStimulusRequested, StimulusRequestNotRecorded, StimulusAppliedByReceipt, StimulusApplicationNotRecorded, PopulationOperatorAttested, PopulationNotRecorded, PopulationLiveObserved, PopulationConflicted, } +import extdeps.bmc.ipmitool_observed_output { ipmitool_hpm_check_bmc0_32 } +import extdeps.bmc.ipmitool_hpm_check { hpm_check_table_of } import gunbc.host_boot_attempt_admission { + PrePowerFirmware, PrePowerFirmwareUnread, pre_power_firmware_minted, attempt_configuration_with_pre_power, AttemptReceiptRefusal, ReceiptValidation, ReceiptValidated, ReceiptRefused, ReceiptHostHasNoRoute, ReceiptExecutorForAnotherHost, ReceiptExecutorNotOnStoreHost, ReceiptHostUnbound, ReceiptNonceMissing, ReceiptNonceNotSlotSafe, ReceiptHostNotSlotSafe, ReceiptPathOutsideReceipts, ReceiptFileUnreadable, ReceiptNotJson, ReceiptSchemaMismatch, @@ -335,3 +340,33 @@ test fn w_the_mt_collins_roster_is_the_guides_32_connectors_by_socket() -> Bool && any(roster, r => (r.label as String) == "J16" && r.socket == 0) && !any(roster, r => (r.label as String) == "25") } + +// ── THE PRE-POWER FIRMWARE READ, bound to the attempt admission admitted ───────────────────────── +fn admitted_configuration() -> AttemptConfigurationReceipt { + match validate(text: valid_text(), nonce: "n42") { + ReceiptValidated { receipt: r } => attempt_configuration_receipt_of(host: operator_host_mtcollins1, source: ConfigurationReceiptAdmitted { receipt: r, slot: "attempt-10-mtcollins1-n42" }, attempt: "run-1") + ReceiptRefused { cause: _ } => attempt_configuration_receipt_of(host: operator_host_mtcollins1, source: ConfigurationReceiptNotNamed, attempt: "run-1") + } +} + +fn firmware_attempt(f: FirmwareReadbacks) -> String { + match f { + FirmwareReadBeforeActuation { attempt: a, source: _, rows: rs } => if count(rs) == 5 && any(rs, r => (r.component as String) == "APP" && (r.version as String) == "0.32 01112100") { a as String } else { "wrong rows" } + FirmwareReadbacksNotRecorded { reason: _ } => "not recorded" + } +} + +// B'S READING JOINS B'S CONFIGURATION; A'S OTHERWISE VALID READING IS REFUSED FOR B, NOT RELABELLED; AN +// UNREAD TABLE STAYS NOT RECORDED. +test fn a_firmware_reading_joins_only_the_attempt_it_was_taken_for() -> Bool { + let b = admitted_configuration() + let table = hpm_check_table_of(stdout: ipmitool_hpm_check_bmc0_32) + let same = attempt_configuration_with_pre_power(c: b, firmware: pre_power_firmware_minted(host: operator_host_mtcollins1, attempt: "n42", table: table, source: "ipmitool hpm check")) + let other = attempt_configuration_with_pre_power(c: b, firmware: pre_power_firmware_minted(host: operator_host_mtcollins1, attempt: "n41", table: table, source: "ipmitool hpm check")) + let unread = attempt_configuration_with_pre_power(c: b, firmware: PrePowerFirmwareUnread { reason: "hpm check was not read: timeout" }) + let other_refused = match other.firmware { + FirmwareReadbacksNotRecorded { reason: r } => string_contains(s: r as String, pattern: "taken for attempt n41") && string_contains(s: r as String, pattern: "refused, not relabelled") + FirmwareReadBeforeActuation { attempt: _, source: _, rows: _ } => false + } + firmware_attempt(f: same.firmware) == "n42" && other_refused && firmware_attempt(f: unread.firmware) == "not recorded" +} diff --git a/dag/test/claim/host/host_pre_power_firmware_mint_seal_witness_test.dag b/dag/test/claim/host/host_pre_power_firmware_mint_seal_witness_test.dag new file mode 100644 index 00000000000..7ad48b7235f --- /dev/null +++ b/dag/test/claim/host/host_pre_power_firmware_mint_seal_witness_test.dag @@ -0,0 +1,41 @@ +module test.claim.host_pre_power_firmware_mint_seal_witness + +import gunbc.compile_diagnostic_census { + CompileDiagnosticCensus, + CensusObserved, + CensusNotRunnable, + census_count_at_key +} +import std.types { String, Bool, Int } +import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree } + +data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree + +// THE SEAL ON THE PRE-POWER FIRMWARE MINT. gunbc.host_boot_attempt_admission pre_power_firmware_minted +// returns a reading bound to whatever host and attempt it is handed, so it is admit_callers-sealed to +// the production binding (pre_power_firmware_observed, which takes them from a BootAttemptClearance) +// and to the one claim that exercises the join. The RED hands the compiler a module outside that +// roster minting a reading for an attempt of its choosing, and asserts the refusal keyed by the +// callee's name (gunbc.compile_diagnostic_census: a class-only count is a property of the closure). +fn keyed_refusals(source: String, callee: String) -> Int { + match compile_dag_diagnostic_census(source) { + CensusObserved { rows: rows } => + census_count_at_key(rows: rows, diagnostic_class: "ConstructorCallAdmissionRefused", subject_name: callee, blocking: true) + CensusNotRunnable { cause: _ } => 0 - 1 + } +} + +data forged_reading_source: String = "module probe_forged_pre_power_reading\nimport extdeps.bmc.ipmitool_hpm_check { hpm_check_table_of }\nimport gunbc.fleet_intent_network { operator_host_mtcollins1 }\nimport gunbc.host_boot_attempt_admission { PrePowerFirmware, pre_power_firmware_minted }\nfn forged() -> PrePowerFirmware {\n pre_power_firmware_minted(host: operator_host_mtcollins1, attempt: \"any-attempt\", table: hpm_check_table_of(stdout: \"\"), source: \"forged\")\n}\n" + +// THE GREEN CONTROL: a module using the public classifier and join compiles with no admission refusal +// on the mint, so the admitted internal call (pre_power_firmware_observed -> pre_power_firmware_minted) +// is accepted in the closure and the RED above is the seal, not a broken closure. +data public_join_source: String = "module probe_public_pre_power_join\nimport extdeps.bmc.ipmitool_hpm_check { hpm_check_table_of }\nimport gunbc.machine_intake_mtcollins1_power_on_account { AttemptConfigurationReceipt }\nimport gunbc.host_boot_attempt_admission { HpmFirmwareProjection, PrePowerFirmwareUnread, hpm_firmware_projection, attempt_configuration_with_pre_power }\nfn classify() -> HpmFirmwareProjection {\n hpm_firmware_projection(table: hpm_check_table_of(stdout: \"\"))\n}\nfn join_unread(c: AttemptConfigurationReceipt) -> AttemptConfigurationReceipt {\n attempt_configuration_with_pre_power(c: c, firmware: PrePowerFirmwareUnread { reason: \"not read\" })\n}\n" + +test fn a_reading_minted_outside_its_roster_is_refused_at_compile_time() -> Bool { + keyed_refusals(source: forged_reading_source, callee: "pre_power_firmware_minted") >= 1 +} + +test fn the_public_join_and_the_admitted_binding_resolve_under_the_seal() -> Bool { + keyed_refusals(source: public_join_source, callee: "pre_power_firmware_minted") == 0 +} diff --git a/dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag b/dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag index 195455c9d47..ca6b0991518 100644 --- a/dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag +++ b/dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag @@ -742,13 +742,15 @@ test fn a_wall_clock_stepping_back_during_readiness_refuses_as_unbounded() -> Bo // THE WALL CLOCK JUMPS TEN MINUTES FORWARD DURING THE READINESS WAIT. The window reads as closed at the // next look, and the attempt refuses without a handoff: a forward step shortens the wait, it never // buys an unbounded one. The look count follows the route's own schedule before the media wait -- it -// moved from 2 to 3 when #12434 put the notice-watcher wait ahead of it -- so a later change to that -// prefix moves it again; what the case holds is the refusal at the look after the jump. +// moved from 2 to 3 when #12434 put the notice-watcher wait ahead of it, and from 3 to 2 when the +// power-on account's pre-power hpm check read (one virtual second, after admission) joined the prefix +// -- so a later change to that prefix moves it again; what the case holds is the refusal at the look +// after the jump. test fn a_wall_clock_jumping_forward_during_readiness_closes_the_window() -> Bool { match run_attempt(world: with_clock_jump(w: world_with_console(lines: []), at: second(count: 20), by: 600)) { WitnessReturned { value, route } => string_contains(s: outcome_reason(a: value), pattern: "did not reach Started with a bound session") - && string_contains(s: outcome_reason(a: value), pattern: "(3 looks,") + && string_contains(s: outcome_reason(a: value), pattern: "(2 looks,") && reached_no_power_action(route: route) _ => false } diff --git a/docs/plans/power-on-sequence-model.md b/docs/plans/power-on-sequence-model.md index e713f9ae8ea..62c83258e63 100644 --- a/docs/plans/power-on-sequence-model.md +++ b/docs/plans/power-on-sequence-model.md @@ -400,3 +400,17 @@ Slice B1 is `gunbc.host_boot_attempt_admission`. It holds the plan and inspectio Where the build differs from the plan above, with reasons: - **Slot key.** The key is `attempt---`, with the host and nonce admitted only over `[A-Za-z0-9_-]`. It is injective by construction and is not a hash: the corpus's `content_hash_of_value` is a 64-bit structural hash, which does not meet "collision-safe" against a chosen nonce. - **The plan's identity.** The inspection names its plan by `plan_subject` and `plan_attempt`. Because an attempt identity admits one boot, that pair identifies the plan. + +### 12b. Slice B2 as built (firmware), and B3 (controller population) + +Slice B2 adds one pre-power read, `mtcollins1_boot_pre_power`. It is taken after admission and before `mtcollins1_boot_actuate_held`, and `gunbc.host_boot_attempt_admission` `attempt_configuration_with_pre_power` joins it to the frozen configuration. +- **The read.** `ipmitool hpm check` is a new `extdeps.bmc.ipmi` `HpmCheck` operation. It is parsed by `extdeps.bmc.ipmitool_hpm_check`, which landed with the CPLD route fix (#13254). +- **The rows.** Each component's active cell is kept as rendered, because the auxiliary bytes have no public decode. +- **Binding.** The readback is `FirmwareReadBeforeActuation { attempt, source, rows }`, where `attempt` is the attempt admission bound. An unread or refused table leaves firmware `NotRecorded` with its cause. +- **The acceptance matrix.** The dry BMC (`gunbc.bmc_dry_realization`) answers `HpmCheck` with the retained BMC 0.32 capture, as a layout fixture. + +**B3: `PopulationControllerReading` (declared frontier).** B3 is the pre-power Redfish population read. It is labelled `CachePossible`, and is joined to the inspection as corroborated or conflicted per socket. +- **Why it is not in B2:** its route dispatches `shell.Mktemp.Dir` and `shell.Remove.FileForce` (for the netrc) and `redfish.Http.GetResourceByPath`. The boot dry world does not model these, and no mtcollins1 Redfish response is retained to model them from. +- **Trigger:** a retained mtcollins1 Redfish capture of the service root, Systems, the system, Processors and Memory. eager-gull-22's read-only probe takes it when the BMC is reachable. +- **Caveat:** after the 2026-10-02 reflash, gunbc gets 401 on Redfish because its role is missing. If the capture is 401 bodies, the trigger also needs the login convergence to restore that role. +- **Already written:** the join and folds are in WIP commit `16a67dfb99d` on `session/calm-lynx-884-slice-b2`. \ No newline at end of file