docs/plans: power-on account, slice-A decisions (§10a)

[gunbai-bot]

Records in docs/plans/power-on-sequence-model.md the decisions taken while implementing slice A (#13117) and through its side-chat reviews:

• typed SEL boundary standings from an ordered fold;
• one located error per occurrence, with only the last cycle choosing the ending;
• loop versus progress after a restart;
• per-socket completeness against the receipt;
• SMpro gating, warnings and coverage;
• milestone provenance;
• the convergence refusal for UEFI followed by a loop;
• the Q3 deletion.

It also renames slice B to the receipt-inputs slice (Q4). Docs only, and it does not depend on #13117 merging first.

🤖 Generated with Claude Code

[briansrls]

Reviewed exact head db41267afa674d2e077a209de9b44e025df25fe1. Approved.

The §10a record is faithful to slice A's implemented semantics and to the review sequence that produced them:

• cycle creation remains owned by admitted power/reset evidence; the ordered SEL fold makes only the first boot record corroborating-or-ambiguous and every later record distinct, while banners bind spans but never create cycles;
• failure decoding is occurrence-local at the owning-reader grain, and only a failure bound to the final cycle can choose the ending;
• RestartedRepeatedly is distinguished from a later cycle that made progress;
• topology, population completeness, and absence findings are conditional on the frozen attempt receipt, with health readings kept unconditional;
• #13058's gated records, warning population, pass-level placement, and dedicated SmproErrorRegisters coverage are retained;
• milestone provenance carries the capture digest plus a resolvable DeclarationRef;
• firmware convergence reads the whole-account projection and refuses UEFI followed by a repeated loop;
• the public secondary-join model no longer attributes opaque CP tokens to sockets, leaving that classification to the private refinement;
• the former error-record slice is correctly folded into A, and slice B now names the still-missing live inputs to AttemptConfigurationReceipt rather than another interpretation layer.

This is a retrospective decision record, not a parallel executable fold: the concrete types/functions and their witnesses remain the mechanism, while §10a records why those shapes were selected. No new open question or alternate authority is introduced.

Non-blocking precision if this file is touched again: the Q3 bullet names secondary_checkpoints, while the implementation also removed secondary_host_checkpoints and the reference row's socket-attributed CP tokens; and §11 could say Q1–Q4 rather than mentioning only Q1/Q2. The semantic rule is already stated correctly, so neither is a landing blocker.

Exact-head required CI is currently queued; land after witnesses is green.

[briansrls]

Re-reviewed exact current head af824fbedba4f47412de589e6f7e34d122a0b08b. The §10a retrospective remains approved, but this head added a substantive slice-B design and two purported operator decisions after the approved db41267 head. That new material is not ready to become the plan authority.

1. Q5/Q6 are recorded as decided without a ruling, and the document contradicts itself

The same text now says:

• Delivery (Q5, decided...);
• Question for the operator ... confirm;
• Q5 and Q6 are both decided in §11.

No operator ruling is cited, and the PR body still describes only the slice-A decision record plus the slice-B rename. Q4 established that slice B needs boot-workflow inputs; it does not by itself establish the external delivery mechanism or authorize a new workflow-dispatch field.

Required repair: either cite the actual operator ruling for each decision, or leave Q5/Q6 open. My recommendation is that Q6 requires a separate ruling because a new dispatch input is a change to the existing mode's public surface even though it creates neither a mode nor a job.

2. The proposed inspection receipt is not bound to the attempt it claims to describe

The proposed shape is:

AttemptInspectionReceipt {
  host,
  requested,
  applied,
  cpus,
  dimms,
  completed_at,
  witnessed_by
}

It does not carry the exact MachineIntakeSubject, IntakeAttemptId, a predeclared plan identity, or its evidence artifact/digest. A dispatch path can therefore select an old receipt for the same host, or a receipt authored after seeing the result, and still populate the current attempt. Computing the selected file's digest records which stale file was used; it does not prove applicability.

The one-authority shape should be closer to:

AttemptConfigurationPlan sole_constructor {
  subject
  attempt
  expected
  requested
  fixed_at: ObserverTimestamp
}

AttemptInspectionReceipt sole_constructor {
  plan: AttemptConfigurationPlan
  applied
  cpus
  dimms
  completed_at: ObserverTimestamp
  evidence
  witnessed_by
}

The parser/admission—not an open record literal—must mint the receipt only after the committed artifact's digest, subject, attempt, host binding, plan identity, and ordering all match. The pre-power firmware readback must be bound to that same plan/subject/attempt as well.

This also removes the present duplicate authorities: expected topology and requested stimulus are independently authored in the receipt row and then requested is authored again in the inspection receipt. Fix them once in the predeclared plan; the inspection reports what was applied against that plan.

3. A possibly cached Redfish inventory cannot be PopulationLiveObserved

The table explicitly says the pre-power-on BMC view may be cached from the last POST, then allows a Redfish-only result to construct PopulationLiveObserved. Those statements are incompatible. A stale pre-change inventory is not a live observation of the physical population this attempt will boot.

Keep the controller reading as a separate standing, for example PopulationControllerCached { ... } or a reading with FreshnessEstablished | CachePossible. It may corroborate the human inspection or create PopulationConflicted; it may construct PopulationLiveObserved only when this platform establishes that the controller refreshed the inventory after the physical change. With no such standing, Redfish-only leaves current population unestablished rather than upgrading cached data into fact.

4. DischargedAt must cite an evidence instance/producer, not merely a record type

std.human_intervention says completion evidence points at the declaration carrying the evidence. Citing the declaration of AttemptInspectionReceipt alone would prove only that a type exists, just as citing AcPowerCycleWitness does not identify a particular attempt's completed intervention.

Name the concrete construction-confined producer or committed per-attempt evidence row that DischargedAt cites. Its observer-sourced timestamp and artifact identity must be the values consumed by the ordering fold. A bare caller-authored EpochMs is not enough to prove inspection-before-power-on.

5. Clarify the absent-receipt behavior

The text says an absent/refused receipt leaves fields NotRecorded, but also says the boot never proceeds on a guessed configuration. Slice A deliberately permits NotRecorded and reports open questions. State one exact rule:

• unknown is admitted and the boot proceeds without topology/population conclusions; or
• slice B makes the receipt an actuation precondition and refuses before power-on.

Do not leave both interpretations available.

Non-blocking after the structural fixes: place §11 before §12 (the current document numbers them in reverse), update the PR body to disclose the slice-B design and workflow-surface decision, and expand Q3 to name secondary_host_checkpoints and the reference row's socket-attributed CP tokens as well as secondary_checkpoints.

The original §10a summary is still sound; the blockers are entirely in the later slice-B additions. Exact-head CI is currently queued, but these are plan semantics rather than CI findings.

[briansrls]

Re-reviewed exact head 6d51cb6ed00fa6e191feefb509019092bc91497f. The prior §10a material remains sound, and three of the slice-B blockers are substantially fixed: expected/requested now have one authority in a sole-constructor plan; the inspection receipt is construction-confined and carries content-addressed evidence; controller inventory has an explicit freshness standing; and Q6 is correctly left open rather than inferred from Q4.

Two load-bearing gaps remain.

1. The receipt is still not joined to the CURRENT boot attempt

AttemptConfigurationPlan.attempt: AttemptPlanId and AttemptInspectionReceipt.plan make the artifact internally self-consistent, but the plan text only checks that “the attempt is the plan the dispatch input named.” The dispatch input names the receipt FILE, so an old, valid file for this host can still bring its own old plan/attempt identity and satisfy that check on a new boot.

The admission must compare the artifact's attempt identity to an independently minted identity for the boot that is about to actuate — e.g. the boot-run/intake attempt created by the dispatch/runtime authority — not merely to another value read from the same committed artifact.

Required control:

• a valid, correctly digested receipt for mtcollins1 attempt A selected during attempt B refuses before pre-power reads/actuation even though host, plan identity, and internal ordering are otherwise valid.

Related precision: if fixed_at and completed_at are serialized in the committed JSON, say how they become ObserverTimestamp. Parsing an authored timestamp string does not itself establish an observer-clock reading. Either make them operator-attested timestamps with that standing, or bind them to a construction-confined clock receipt.

2. The absent/refused-receipt actuation policy is still ambiguous

The text still says both:

• “A receipt that is absent or refused leaves the fields NotRecorded or refused with their cause”; and
• “The boot never proceeds on a guessed configuration.”

Slice A deliberately permits NotRecorded and reports open questions, so this still does not answer the review's requested policy question: does slice B make the receipt a pre-power-on admission requirement, or may the boot proceed with explicitly unknown configuration?

Choose one and state it structurally:

• permissive: absent/refused receipt -> fields remain unknown -> boot may actuate, but no configuration-dependent conclusion is constructible; or
• strict: absent/refused receipt -> attempt configuration admission refuses -> no power write.

A RED should pin the selected policy on the real pre-power path.

Q5 being explicitly attributed to eager-gull-22 is acceptable as an implementation-design decision so long as it is not represented as an operator ruling; Q6 correctly remains the operator-facing workflow-surface decision. The Redfish CachePossible correction and the producer citation for DischargedAt are otherwise acceptable.

No other blocker from the previous review remains.

[briansrls]

Re-reviewed exact head 58a010d9a4384de3dc4ebcf352bd2fef52276b6b. The two prior blockers are materially addressed: the receipt is now joined to an attempt identity minted outside the artifact, the authored times are correctly typed as operator-attested rather than observer-clock readings, and the absent-vs-refused receipt behavior is explicit with separate REDs.

One load-bearing ambiguity remains in the replay rule.

A compare-and-set does not by itself establish “this nonce has never been consumed”

The plan says the dispatch's transaction_nonce is “consumed once with a compare-and-set on the unit's durable hold store” and therefore a second run with the same identity refuses. That conclusion depends entirely on the shape of the durable key/value transition, which is not specified.

A single per-unit CAS slot has two bad possible interpretations:

• if A consumes the empty slot, then B cannot ever consume it unless the slot is reset/replaced;
• if B replaces A, then a later replay of A can replace B unless the transition retains historical membership somewhere.

std.durable_compare_and_set gives atomicity/generation; it is not by itself a set of every nonce ever seen.

Make the anti-replay representation explicit and construction-safe. The simplest shape is a create-once slot keyed by (managed subject, transaction_nonce) under a disjoint attempt-admission namespace in the durable store: admission succeeds only on Absent -> Consumed and that key is never reset/reused by normal boot cleanup. Equivalently, use a durable monotone seen-set if one already exists. Do not overload the live unit-hold slot itself, whose lifecycle intentionally returns to free.

Required controls:

• A first use of nonce A succeeds;
• a concurrent second use of A loses/refuses;
• after a different nonce B succeeds, replaying A still refuses;
• normal unit-hold release does not erase A's consumed standing.

Because transaction_nonce becomes load-bearing, slice B must also update its existing workflow contract that currently describes it as “Not consumed by any step”, and a named receipt with empty nonce must refuse before the receipt can be admitted. An empty receipt may retain today's permissive NotRecorded route; that does not imply an empty attempt identity may admit a named receipt.

Everything else from the prior review is accepted, including the structural pre-actuation ordering and the explicit empty-input permissive arm. Q6 correctly remains open with the operator. No exact-head workflow run is currently attached to this docs-only head; this blocker is plan semantics, not CI.

[briansrls]

Re-reviewed exact head 7543f5a746687db6c101119b38afa899359d1b36. Approved.

The remaining anti-replay blocker is closed. The plan now names a durable representation whose semantics actually imply historical non-reuse:

• one create-once slot per (managed subject, transaction_nonce);
• an attempt-admission namespace disjoint from the live unit-hold slot;
• Absent -> Consumed as the sole successful CAS transition;
• no normal hold release, recovery, or cleanup route that deletes or rewrites an attempt-admission slot.

That gives the intended properties simultaneously: A's first admission can succeed, concurrent/repeated A loses, B has an independent key and can succeed, replaying A after B still loses, and returning the unit hold to free does not erase A's consumed standing. The five listed controls discriminate each of those laws rather than relying on CAS as an unexplained shorthand.

The attempt join is also now complete at plan level: the artifact's plan must equal the current dispatch's externally minted transaction_nonce; a named receipt with an absent/empty nonce is in the refused-receipt arm; and the implementation cut must replace the workflow's stale “not consumed by any step” description with this admission role. The earlier valid-A/dispatch-B RED remains required before any pre-power read or actuation.

The authored times remain honestly OperatorAttestedTime, ordered only against one another. Admission-before-actuation is structural rather than fabricated by comparing them to an observer clock. The empty-receipt route is separately permissive (NotRecorded, no configuration-dependent judgment), while every named-but-refused receipt is a typed pre-actuation refusal.

The prior approvals also remain intact: one authority for expected/requested configuration, construction-confined plan and receipt, content-addressed evidence, plan-bound firmware readback, controller-cache freshness standing, and DischargedAt citing the fail-closed evidence producer. Q6 correctly remains open with the operator.

Implementation guardrails, non-blocking for this docs PR: derive the durable slot key from the stable managed-host identity with collision-safe encoding rather than serializing the mutable ManagedHost row or using the nonce as a raw path; perform all non-replay validation before consuming the key; and execute the CAS through the same admitted store-host authority as the unit hold.

No plan-level blocker remains. Exact-head required CI is pending; land after witnesses is green.

[briansrls]

Re-reviewed exact head 7543f5a746687db6c101119b38afa899359d1b36. The remaining anti-replay blocker is resolved.

The plan now names a representation whose laws support the claimed behavior: one create-once attempt-admission slot per (managed subject, transaction_nonce), in a namespace separate from the live unit hold. Absent -> Consumed is the only successful transition; ordinary hold release, dead-holder recovery and cleanup have no authority to delete or rewrite these slots. This gives the required monotonicity: A succeeds once; concurrent/repeated A refuses; B remains independent and can succeed; A still refuses after B; releasing the unit hold does not erase A's consumed standing.

The five implementation REDs pin those laws individually rather than treating CAS as a synonym for a seen-set. The implementation obligations also close the associated workflow contract: transaction_nonce must no longer say it is unused, and a named receipt with an empty nonce refuses before admission. The permissive empty-receipt arm remains distinct and honest: no receipt named means NotRecorded and no topology judgment, not a guessed configuration.

The previously approved slice-B structure remains intact: the receipt's attempt is joined to the externally minted dispatch identity; expected/requested have one authority in the sealed plan; the sealed inspection receipt carries content-addressed evidence; attested times are not promoted to observer-clock facts; firmware readback is bound to the same plan; cached controller inventory has an explicit freshness standing; and named-but-invalid receipts refuse before pre-power reads or actuation. Q6 correctly remains open with the operator.

Implementation guardrails, non-blocking at plan review: derive the persistent slot key from stable host identity plus nonce with a collision-safe encoding; complete all artifact/subject/attempt/order checks before consuming the slot so a malformed receipt cannot burn a valid nonce; and route the CAS through the admitted store-host authority rather than trusting a caller's host label.

No plan-level blocker remains. Exact-head required witnesses is still running; land after it is green.