Repository navigation
docs/plans: power-on sequence model + 'best understanding' diagnostic fold (Mt. Collins) - #13071
Conversation
…ld (Mt. Collins first) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
briansrls
left a comment
There was a problem hiding this comment.
The direction is right: Mt. Collins first, one evidence-derived account, abstract only after the second platform, and delete the string findings at the replacement root. I agree with R1/R2/R3 in qualified form below, but the current terminal shape loses several facts this investigation specifically needs.
-
A power-on is a session of cycles and parallel subjects, not one total chain with one scalar
reached. The old firmware can stop on cycle 1 and reach UEFI on cycle 2; the new firmware repeats the same stopped cycle; socket 1 can fail to join while socket 0 reaches Linux.BootUnderstanding { reached: one stage, ending: one ending }cannot preserve those facts. ModelPowerOnSession { cycles: List<BootCycleUnderstanding>, ... }, and inside each cycle carry stage standings keyed by subject/socket/component. The session then rolls up how the attempt ended.ReachedCensusmust not mean “no error found”: a census can be reached with a decoded CCIX error, one socket, or another degraded standing. Add the discriminating RED: a pending CCIX error plus later census isReachedCensuswith an error/degradation, neverStoppedWithStatedFailure. -
Separate what the host did from whether we observed it and whether the workflow worked. A BMC authentication refusal is not failure of the “BMC came up” platform stage; an empty SOL capture is not SoC silence; a bundle-write or media-read failure is not a host ending. Add independent host-ending, observation-coverage, and workflow/collection standings.
BootEvidencealso needs the collectors the plan says matter but currently omits (SOL collector standing, KVM, virtual-media/handoff, watchdog/reset evidence) and the attempt's physical/configuration snapshot. Without installed-CPU/DIMM/firmware/stimulus/expected-topology data, “every populated DIMM” and “active sockets equal populated sockets” are unanswerable. -
R2: yes, an opaque CP reader is public, but it may establish only opaque sequence relations. It may say “this cycle ended after token X; reference capture R contains X followed by Y,” with R's digest, firmware/configuration scope and cycle identity. It may not use that token to establish
DdrTraining, call Y stage success, or returnStoppedSilently { after_stage: DdrTraining }; those meanings came from the private/disassembly lane. A public stage attribution must come from a publicAmpereBootStagereading or remain unestablished. Add the named gunbc-private refinement slice; otherwise this plan does not yet consume all of today's understanding. -
R3: associate the refused pair with the secondary-join subject, but do not decode it as that stage. Reuse #13025's
MtCollins1SecondaryJoinOutcome; do not re-derive join success/timeout here.CUR=0x0001/BOOTSTAGE=0x03ffisSmproBootProgressRefusedand licenses no “stuck at PMpro,” “DDR,” or other last-stage claim. It belongs in the join account as contradictory evidence/open question.OpenQuestion.subjecttherefore must admit a secondary-socket/join subject, not onlyPowerOnStage. Also correct the factual reversal in the table: the real capture has socket 0 GPI-pending/gated and socket 1 ungated, not vice versa. -
R1: land #13041 first, then replace it atomically in slice A. Do not leave E as a later independent slice. Delete
HostBootObservationand its authored datum when A lands, and make firmware convergence consume an operation-specific readback projected from the wholeBootUnderstanding.HostReachedUefiis a reached milestone, not aBootEnding, so projecting fromBootEndingalone would change #13041's semantics.
Finally, before slice A, commit the exact consumer/semantic census for every deleted *_findings producer and mtcollins1_boot_outcome_with_findings: each existing finding needs a typed destination or an explicit retirement, and every consumer outside the required gate needs disposition. With those corrections, the monolithic-first strategy is the right one.
…tion, step 2/2b facts (review input) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…rsistence (operator shapes) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…eader, upstream line authorities (v6.8) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
briansrls
left a comment
There was a problem hiding this comment.
Re-reviewed exact head e4e8a4a4d4. The additions for independent stage standings, reset-cause evidence, retry-state uncertainty, and the public/private naming boundary are useful, but the prior blockers are only partly represented and R1/R2 need terminal rulings.
R1 — decided
Land #13041 first, then replace it atomically in slice A. Do not retain E as a later independent cut. Slice A must delete HostBootObservation and its authored datum while introducing the derived account, and firmware convergence must consume an operation-specific readback projected from the whole session understanding. It must not consume BootEnding directly: HostReachedUefi is a reached milestone and can coexist with a later/degraded ending.
The current head still leaves E separate and says its ordering depends on R1, so it does not encode this decision.
R2 — decided
An opaque CP: reader belongs in public gunbc, but it may establish only an opaque observation relation. Its result should carry the raw words and order, cycle identity, capture digest, firmware/configuration snapshot, subject, and the exact reference capture/configuration against which continuation is compared. It may say “cycle C ended after token X; reference capture R contains X followed by Y.” It may not establish DdrTraining, call Y stage success, or return ... { at: DdrTraining @ X }; that semantic attribution comes from the private disassembly lane. Add a named gunbc-private refinement slice that consumes the public observation and #202/#203 evidence without leaking it back into public.
The current stage table and slice-A acceptance still use the opaque word to establish DdrTraining @ 00001a0a, so the public/private boundary remains crossed.
Remaining structural blockers
-
One scalar
BootUnderstandingis still not a power-on session. Addingstages: List<StageStanding>does not recover cycle identity or parallel subjects. ModelPowerOnSession { cycles: List<BootCycleUnderstanding>, ... }; each cycle needs subject-keyed/socket-keyed standings. The old firmware's failed first cycle plus successful second cycle and socket 0 reaching Linux while socket 1 fails to join must both remain representable. -
ReachedCensusstill says “no error found at any stage.” Reaching census is orthogonal to decoded errors/degradation. Add the RED where a GPI-pending CCIX error and one-socket census produceReachedCensusplus error/degradation, notStoppedWithStatedFailure. -
Host behavior, observation coverage, and workflow/collection outcome remain conflated.
BootEvidencestill lacks explicit SOL/KVM/media/handoff/reset-collector standings and the attempt's installed CPU/DIMM/firmware/stimulus/expected-topology snapshot. A BMC-auth refusal, empty SOL, or bundle-write failure must not become a host-stage ending. -
The GPI standing is factually reversed in the table. The retained hand read has socket 0 GPI-pending/gated and socket 1 ungated, not socket 1 gated and socket 0 ungated.
-
The secondary-join refusal is still overinterpreted. Reuse #13025's
MtCollins1SecondaryJoinOutcome.CUR=0x0001/BOOTSTAGE=0x03ffisSmproBootProgressRefused; it does not license “stuck at PMpro,” DDR, or another stage. Carry it as contradictory evidence/open question on a secondary-join subject. -
The migration still lacks the exact consumer/semantic census. Before slice A, enumerate every deleted
*_findingsproducer andmtcollins1_boot_outcome_with_findingsconsumer, with one typed destination or explicit retirement per finding and disposition for consumers outside the required gate. -
The pseudotype has a malformed arm:
EndingUnobservableis placed underResetCauseWordin the code block. It belongs in the host/session-ending or observation-coverage algebra, not the reset-cause word.
Keep the monolithic Mt. Collins-first direction, but encode these decisions in the plan before any child implementation starts.
…s; typed harness findings; readers wired into the console reading Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… findings; typed harness findings; readers wired into the console reading" This reverts commit c0d5f40.
…/panic reader, upstream line authorities (v6.8)" This reverts commit 89cecec.
…ycles x subjects; host/coverage/collection split; configuration snapshot; opaque CP relation; consumer census; private slice P Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
|
Re-review request: head About the code that briefly appeared on this branch. Implementation commits landed on this branch before the rulings. They are reverted here ( Rulings
Structure
Still open: Q1 (may self-identifying console banners attribute milestones, never stages?) and Q2 (the run-time source of 🤖 Generated with Claude Code |
briansrls
left a comment
There was a problem hiding this comment.
Re-reviewed exact head 75f0bd113c. The earlier architectural blockers are substantially addressed: R1/R2/R3 are encoded, the account is a session of cycles with subject-keyed standings, host/coverage/collection are split, ReachedCensus is orthogonal to errors, the deletion census and private refinement slice are present, the GPI direction is corrected, and the socket-1-absent UEFI control is in the reference corpus. Four narrow but load-bearing corrections remain.
Q1 — yes, with a strict milestone boundary
A component-owned console line may establish that component's console milestone. Thus an AMI Press <DEL> or <ESC> prompt can establish UefiConsolePromptObserved (UEFI code executed far enough to emit it), and UEFI Interactive Shell v2.2 can establish the stronger UefiShellObserved. Likewise GNU GRUB, EFI stub: and Linux version can establish their exact component milestones.
It may not establish an AmpereBootStage, stage completion, health, or successful handoff. Carry the exact line/parser, cycle, capture digest and ordering evidence. Structurally, move stage: AmpereBootStage out of generic SubjectReading.Established; as written, any subject can be paired with any stage. Only the SMpro/socket-progress arm should be able to carry SmproBootProgressRead/AmpereBootStage; console subjects should carry milestone-specific readings.
Q2 — the proposed runtime sources are not sufficient
mtcollins1_slots is the historical 2026-09-10/11 host census with a 16-DIMM population, not the current attempt's occupancy. The CPU rows consumed through mtcollins1_physical_orientation are likewise a 2026-09-23 operator report that still says socket 1 contains the production CPU. Those rows are useful topology/history authorities, but using them as the step-3 runtime configuration would contradict the actual socket 1 absent, J1 only control.
Add one attempt-bound, frozen AttemptConfigurationReceipt before power-on. It should separate:
- expected configuration/policy;
- requested stimulus from an applied-stimulus receipt;
- current physical population, with per-field standing such as
LiveObserved,OperatorAttested,Conflicted, orNotRecorded; - live firmware readbacks taken after the physical configuration is set and before actuation;
- subject, attempt, timestamp and artifact/digest provenance.
For manual CPU/DIMM work, the workflow must consume a human completion/inspection receipt; a workflow-authored request such as “remove socket 1” is not evidence that it happened. Static slot/orientation modules may map J1 to topology, but may not supply current occupancy. The fold should consume only this frozen receipt, not query mutable or historical global rows.
Cycle creation cannot depend on reaching DRAM
The plan currently says every DRAM FW version banner opens a cycle. That loses exactly the early failures the account intends to model: a host can stop in SMpro/PMpro/ATF before that banner, or SOL can be empty while SEL/SMpro still observe a boot. Open cycle 1 from the admitted chassis-power-on effect. Open later cycles from typed restart/reset boundary evidence (SEL, power/reset observation, and/or console); use the DRAM banner to bind a console span to a cycle, not as the sole authority that a cycle exists. Add a control where no DRAM banner appears but a power-on plus SMpro/SEL evidence still yields one partial cycle.
Coverage remains orthogonal even when incomplete
Law 3 presently says an empty SOL, BMC-auth refusal, or bundle-write failure makes HostEndingNotEstablished. Those events must not choose the host ending at all. If another carrier proves ReachedCensus, UEFI shell, or a reset, retain that host result and record the independent coverage/collection defect. Use HostEndingNotEstablished only when the remaining host evidence cannot establish an ending. Add the converse RED: SOL=ReadEmpty plus a valid host-capture END marker still yields ReachedCensus with an SOL coverage gap.
GPI-gated versus ungated record
The direction is fixed, but the stage table still places the socket-1 ungated words under “Stated failure” and says the failure was observed on both sockets. Only socket 0's PendingAndDecoded record is a current stated error. Socket 1's matching payload under GpiUnavailable is an anomalous/ungated raw record plus an open question, not a second DecodedBootError or PendingErrorRecord.
One smaller R1 shape correction follows from the same rule: BootReachedUefiAfterSet { cycle, degradations } says a later restart is carried, but the type does not carry the session ending or subsequent outcome. Include it (or an evidence reference to the whole account) so reaching UEFI cannot erase a later repeated-reset ending.
With these corrections, the plan is ready; I found no need for another architectural recut.
…on power-on/reset evidence; coverage never chooses the ending; ungated record is not a stated error; readback carries the session ending Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
|
Head
— sent from calm-lynx-884 |
…red join (review 74585) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
briansrls
left a comment
There was a problem hiding this comment.
Re-reviewed exact head defb7b8bd7b715cc4122252d8b44158092d194ba. Approved.
The 75f0bd1 blockers are resolved:
- Q1 is now a strict console-milestone boundary. The exact component-owned line, parser, cycle context, capture digest, and ordering evidence are retained; milestones imply neither
AmpereBootStage, completion, health, nor handoff. OnlySocketProgresscan carrySmproBootProgressRead/ an Ampere stage. - Q2 is an attempt-bound frozen
AttemptConfigurationReceipttaken before power-on, separating expected configuration, requested stimulus, applied-stimulus evidence, current per-field physical population standing, live firmware readbacks, and provenance. Historical slot/orientation rows supply topology/history only. - Cycle 1 opens from the admitted power-on effect; later cycles open from reset/restart evidence. The DRAM banner binds a console span but is not cycle existence, and the no-banner partial-cycle RED is explicit.
- Host behavior, observation coverage, and collection outcome remain orthogonal. Empty SOL/BMC-auth/bundle-write states cannot select the host ending, and the converse
ReadEmpty SOL + host-capture END => ReachedCensus + coverage gapcontrol is present. - The GPI fact is correctly asymmetric: only socket 0's
PendingAndDecodedrecord is a stated error; socket 1's matching ungated/GpiUnavailablepayload isUngatedRawplus an open question. BootReachedUefiAfterSetcarries the session ending andaccount_ref, so a UEFI milestone cannot erase a later repeated-reset ending.
The earlier architecture remains intact: one session of cycles and parallel subjects; ReachedCensus orthogonal to errors/degradations; R1's atomic replacement of HostBootObservation; R2's opaque public checkpoint relation; R3's reuse of #13025; the exact finding/consumer census; named private refinement slice P; and the socket-1-absent UEFI positive control.
#13041 is merged, and exact-head witnesses is green.
Non-blocking implementation guardrails for slice A:
- Make cycle-boundary evidence and the absence of a console span explicit in the concrete
BootCycleAccountcarrier—the prose and RED require both even though the pseudotype abbreviates this asspan: CaptureSpan. - Derive a console subject from its milestone, or construction-confine that pair, so a UEFI subject cannot be paired with a GRUB/kernel milestone.
- Refresh the PR body: it still describes the superseded scalar
BootUnderstandingand slices A–E.
No plan-level blocker remains. Slice A should be reviewed independently as the atomic implementation/cutover.
Plan only, for review before code. It covers the Mt. Collins stage chain from AC to the census, evidence per stage with the owning readers, and one fold returning
BootUnderstanding(furthest stage established, how the boot ended, decoded errors, typed open questions). It replaces the bundle's string findings, takes the host as aManagedHost, notes the Jade/x86 seams without abstracting them, and splits the work into child slices A–E. Review questions R1–R3 are in section 8.🤖 Generated with Claude Code