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

[gunbai-bot]

Slice B2 of docs/plans/power-on-sequence-model.md §12: the firmware readback before power-on, tied to the attempt admission admitted. This is the firmware-only scope agreed with eager-gull-22; the controller-population reading (B3) waits on a retained mtcollins1 Redfish capture. Main already has B1 (#13230) and the hpm check parser (#13254).

What it adds

• Operation: extdeps.bmc.ipmi HpmCheck, a read-only, deadline-bounded ipmitool hpm check.
• Read site: gunbc.machine_intake_mtcollins1_boot_diagnostic_bundle mtcollins1_boot_hpm_check reads the table through extdeps.bmc.ipmitool_hpm_check. A failed read carries the controller's own cause.
• Join: gunbc.host_boot_attempt_admission pre_power_firmware_of_hpm_check and attempt_configuration_with_pre_power join the reading to the frozen configuration as FirmwareReadBeforeActuation { attempt, source, rows }.
  • attempt is the attempt admission bound.
  • Each component's active cell is kept as rendered, without decoding the auxiliary bytes.
  • An unread or refused table leaves firmware NotRecorded with its cause.
• Ordering: in gunbc.machine_intake_mtcollins1_boot_run, mtcollins1_boot_pre_power runs after BootAttemptCleared and before actuation, beside the SDR/SEL baseline. A refused receipt reads nothing.
• Matrix: the dry BMC (gunbc.bmc_dry_realization) answers HpmCheck with the retained BMC 0.32 capture, as a layout fixture.
  • The clock-jump case's look count moves from 3 to 2. The pre-power read joined the prefix before the media wait, and the case's own comment says the count follows that prefix. The refusal it holds is unchanged.
• Plan: §12b describes B2, and states B3's frontier and its 401 caveat.

Evidence (local claim_batch)

Witness	Result
admission (new claim the_hpm_check_table_is_bound_to_the_admitted_attempt_and_an_unread_one_stays_not_recorded)	15/15
acceptance matrix	29/29
boot_run	35/35
bundle	71/71
account	28/28

🤖 Generated with Claude Code

[briansrls]

REQUEST_CHANGES at exact head b36381e55c8ea4d01b7d6a93c889586f0867cfcc, against DESIGN.md §§3, 3d, 4b and 5 and power-on-sequence-model.md §12's explicit cross-attempt guarantee.

The production call ordering is right: admission precedes HpmCheck, which precedes the baseline and actuation. The operation is authenticated/deadline-bounded/read-only, failed reads preserve their cause, active cells keep their uninterpreted auxiliary bytes, and the dry BMC capture is honestly a layout fixture. B3 is explicitly deferred; I am not asking B2 to discharge #13254's separate post-flash FirmwareConverged frontier.

The remaining blocker is that the new 'join' does not bind the read to an attempt. PrePowerFirmwareRead contains only caller-authorable source text and rows. mtcollins1_boot_hpm_check receives no admitted attempt or subject carrier. attempt_configuration_with_pre_power then unconditionally copies c.attempt onto whichever rows it is supplied. A genuine reading obtained during A can be passed with B's genuine configuration and becomes FirmwareReadBeforeActuation { attempt: B, ... } without a read for B. Authored/fixture rows can take the same route. configuration_questions then treats that arm as recorded without consulting the attempt/source fields.

This contradicts §12: a readback from another attempt cannot fill this one. The new control checks that the copied output label equals n42; it does not discriminate the cross-attempt substitution.

Bind the successful read at its real producer to the admitted subject/attempt (or confine the complete read-and-join so an independently supplied successful population cannot enter it). Preserve that bound identity through the join and reject a mismatch instead of assigning a new identity. Supplied table controls should remain pure projections/classifiers rather than exporting the production observed standing. Add a RED using A's otherwise valid reading with B's configuration, alongside the B-with-B positive and unread refusal. No need for an additional provider-effect path or a B3 implementation.

Source/receipt review only; no controller reads, power actions, or local tests were performed by this reviewer.

[briansrls]

REQUEST_CHANGES at exact head 615927d85b565e6f2580e608e36593c5ad8079bb, against DESIGN.md §§3, 4b and 5 and power-on-sequence-model.md §12. One remaining construction bypass; the join repair itself is accepted.

Accepted: PrePowerFirmwareReading is sealed; the production read passes its clearance into the restricted pre_power_firmware_observed; the admitted receipt nonce (or the no-receipt run identity) labels the reading at that producer; the join checks both host and attempt and preserves the reading's own identity rather than assigning the configuration's. hpm_firmware_projection is a pure table projection. The B-with-B, A-with-B and unread control now discriminates the relabel defect. The existing admission → read → baseline → actuation ordering remains intact.

Remaining blocker: test.claim.host_boot_attempt_admission_witness::observed_for is an unrestricted sanctioned-constructor proxy. pre_power_firmware_minted admits it, and it returns PrePowerFirmware containing the sealed production reading from the retained 0.32 fixture for ANY supplied attempt. An outside caller holding B's mtcollins1 configuration can therefore call:

attempt_configuration_with_pre_power(
  c: b,
  firmware: observed_for(attempt: b.attempt),
)

That reaches FirmwareReadBeforeActuation without a clearance or an HpmCheck for B. No forged record literal or direct call to either restricted mint is needed. The new equality check correctly rejects an A-labelled value; it cannot reject a fixture that the public helper has already minted with B's label. Thus the earlier requirement that supplied controls not export the production observed standing remains unmet.

Minimal repair: delete observed_for, admit the exact Bool-returning test a_firmware_reading_joins_only_the_attempt_it_was_taken_for to pre_power_firmware_minted, and make the two fixture mints inside that test. Alternatively, confine the helper to that exact test, with no unrestricted carrier-returning wrapper above it. Keep the repaired join and its relabel mutation control. Add an outside-caller compiler RED for the surviving fixture-mint/helper boundary, paired with the admitted internal control; testing only a sealed record literal would miss this path.

No B3 implementation, new live operation, or separate post-flash FirmwareConverged work is requested. This is limited to closing the exported fixture carrier.

Reviewed the complete PR diff, the one-commit correction from b36381e55c8ea4d01b7d6a93c889586f0867cfcc, exact-head DESIGN, the admission producer and the witness helper. The reported 15/15, 29/29, 35/35 and 71/71 results and relabel mutant are author-reported; I did not execute local tests or any controller/power action. Exact-head witnesses run 37248246259 is still in progress; the finding is independent of its result.

[briansrls]

APPROVE at exact head 147963d547aff5b5b19a5b43f88fca8be304e177, against DESIGN.md §§3, 4b and 5 and power-on-sequence-model.md §12. The remaining fixture-constructor bypass from review 5409013978 is closed.

Reviewed the complete one-commit, three-file delta from 615927d85b565e6f2580e608e36593c5ad8079bb. DESIGN.md and the previously accepted production read, host/attempt join, refusal behavior and ordering are unchanged.

observed_for is deleted. The only admitted test caller of pre_power_firmware_minted is now a_firmware_reading_joins_only_the_attempt_it_was_taken_for, and both supplied readings are minted and consumed inside that Bool-returning claim. No fixture reading escapes through a carrier-returning witness facade. The production caller remains pre_power_firmware_observed, itself confined to the actual HpmCheck reader.

The new enrolled compiler probe calls the surviving mint from an outside module and requires a blocking ConstructorCallAdmissionRefused keyed to pre_power_firmware_minted, not merely a closure-wide diagnostic count. The public classifier/join control requires zero of that same refusal, and CensusNotRunnable cannot satisfy either assertion. The reported admit-list-removal mutant makes the outside-call RED fail. The existing B-with-B positive, A-with-B refusal and unread case remain intact; the join still preserves the reading's own identity instead of relabelling it.

This approves B2's bounded firmware-read implementation. It does not discharge B3, establish current hardware firmware from the dry 0.32 fixture, or retire the separate post-flash FirmwareConverged frontier.

Source/delta review only: admission 15/15, seal 2/2 and the mutation result are author-reported; I did not execute local tests or controller/power actions. Exact-head witnesses run 37249531401 remains in progress. No semantic blocker remains; land after required exact-head CI passes. The requested head was unchanged immediately before submission.