Mt. Collins power-on account (slice A): one fold replaces the string findings and HostBootObservation

[gunbai-bot]

Slice A of docs/plans/power-on-sequence-model.md (#13071, approved and queued). This PR adds the Mt. Collins power-on account: one fold over a boot's evidence that returns our best understanding of what happened. It is never a pass/fail bit.

It replaces two things in one change (ruling R1, delete-first):

• the boot bundle's string findings and every per-reader *_findings producer;
• mtcollins firmware update as a convergence pattern #13041's authored HostBootObservation and its datum mtcollins1_post_firmware_set_boot_2026_10_03.

What lands

Readers (public; opaque where R2 requires). Every capture these readers ever read is self-observed.

• gunbc.machine_intake_ampere_checkpoint_console_observation: CP: tokens grouped into banner-delimited console spans. A token is opaque: the reader reports only order and equality. AmpereCheckpointRelation says "span S of capture C ended after token X; reference R (digest, firmware scope, configuration scope) continued with Y". It never names a stage.
• gunbc.machine_intake_mtcollins1_console_milestone_observation (Q1): exact component-owned lines become milestones. Examples are the DRAM firmware banner, the firmware summary, the AMI setup prompt (UefiConsolePromptObserved), the edk2 shell (UefiShellObserved), GRUB, the EFI stub and the kernel banner. Each carries its line, its marker, its line index and its span. Spans come from the checkpoint reader's own fold, not a second count.
• extdeps.linux.efi_stub and extdeps.linux.boot_console cite Linux v6.8: EFI stub: , efi_err + Failed to load initrd: 0x%lx, EFI_LOAD_ERROR, Kernel panic - not syncing: , and the Linux version banner. gunbc.machine_intake_linux_boot_console_observation reads them. Both modules are enrolled as scope carriers in gunbc.extdeps_scope_frontier.

The account: gunbc.machine_intake_mtcollins1_power_on_account.

• Separate standings. Host, coverage and collection are kept apart. Collection is the bundle's typed HarnessFinding, composed beside the account in MtCollins1BootFindings.
• Configuration. One frozen AttemptConfigurationReceipt.
• Cycles. Cycles open on the confirmed power-on and on SEL restart records. Banners bind console spans only when the counts agree, so a cycle can exist without reaching DRAM.
• Stages. A stage comes only from an SMpro pair, decoded by smpro_boot_progress_of. A refused pair (SmproBootProgressRefused) is evidence plus an open question on the second socket's join subject.
• The second socket's join. It reuses mtcollins1 socket 1: SecondaryJoinTimeout, not 'defective'; CPU0 pairing weakened by matching characteristics #13025's secondary_join_outcome.
• SMpro/PMpro internal error records: errmon registers, public decoder, capture row, collector #13058's error records. These are placed by their gate:

Gate	Becomes
PendingAndDecoded	stated error plus a degradation
GpiUnavailable	RecordUngated anomaly plus UngatedRecordUnexplained
contradictory gate	anomaly
nonzero event register	anomaly

• Ending (HostEnding):
  • ReachedCensus: orthogonal to errors and degradations.
  • StoppedWithStatedFailure: the furthest stated failure that the last cycle did not get past.
  • RestartedRepeatedly: only when the last cycle got no further than an earlier one. It carries the cadence (counted, not timed), the console error count, the SEL restarts, the watchdog, and ResetCauseUnobserved naming the sweep that found no window.
  • StoppedWithoutRestart { restarts_before }
  • HostEndingNotEstablished: only when the host evidence establishes none.
• Open questions. All are typed:
  • reset cause;
  • whether retry state persists;
  • what a checkpoint token means;
  • refused SMpro pairs and ungated records;
  • the restart cadence, which isn't timed;
  • configuration fields not recorded or conflicted;
  • carriers not read;
  • console spans that can't be bound to cycles.
• Readback for convergence. firmware_set_boot_readback projects the whole account. BootReachedUefiAfterSet carries the session ending and the account itself.

Convergence. gunbc.fleet.mtcollins_firmware_converge boot_verdict reads FirmwareSetBootReadback?:

• a UEFI milestone converges the set unless the session then restarted repeatedly; that case refuses as the new BootReachedUefiThenRestartedRepeatedly;
• lost progress refuses as BootProgressLostAfterFirmwareSet { ending, last_relation }.

gunbc.machine_intake_boot_outcome is deleted.

Bundle and receipt.

• The bundle text renders the account.
• The one-line refusal appends the account's notes (its ending, errors, degradations and anomalies), then the harness findings, and never flips the verdict.
• The receipt's findings= line becomes three lines: account=, coverage= (carriers that were not fully read) and harness=.

Consumer census (plan §6): each deleted producer and where it went

Deleted	Destination
mtcollins1_boot_bundle_findings	mtcollins1_boot_findings → MtCollins1BootFindings { account, harness }
the "every BMC read failed" finding	HarnessFinding.EveryBmcReadFailed, plus coverage CarrierRefused
processor_findings, memory_findings, socket_absent_finding, sel_findings	BmcAnomaly rows placed on subjects
mtcollins1_sensor_findings	mtcollins1_sensor_anomalies (typed, in the sensor module)
mtcollins1_smpro_findings, mtcollins1_smpro_stage_findings (including #13058's record lines)	SocketProgressAccount, gated record errors and anomalies, secondary_join_outcome. The "sockets differ" string is retired: the difference is now the two typed readings.
ampere_dram_findings	ampere_dram_untrained_sockets (the closed-roster rule, in the DRAM module) → DramSocketUntrained. Malformed rows become anomalies.
socket_summary_findings	ActiveSocketsBelowExpected, SocketNotJoined
kernel_module_decompression_findings	KernelModuleRefused stated error
media, handoff, override and power-after findings; credential residue	typed HarnessFinding
HostBootObservation and the authored datum	FirmwareSetBootReadback. The 2026-10-03 case is now derived from the committed step-1 capture excerpt.

Every migrated witness keeps its discriminating input; the assertions now read typed values.

Evidence

Every witness file this change touches was run with a claim_batch built from this tree: cargo build --release -p v1-compiler --bin claim_batch, then claim_batch --entry <file> --functions <every test fn>.

Witness	Passed
account	24/24
readers and milestones	14/14
bundle	69/69
firmware convergence	69/69
SMpro observation	21/21
SMpro error records	21/21
DRAM	17/17
sensors	10/10
kernel module	13/13
MegaRAC media	87/87
physical orientation (Q3 edit)	16/16

• Fixtures are exact-byte excerpts, each with file and excerpt sha256 recorded:
  • branch mtcollins1-captures-2026-10-03 (step 1);
  • run 37069907299's SOL capture;
  • artifacts/bmc/mtcollins1-hw-census-sol.log and mtcollins1-first-own-image-boot.log.
• REDs per law:
  • a CCIX-pending record plus a one-socket census still gives ReachedCensus;
  • an empty SOL plus an END marker still gives ReachedCensus, with an SOL coverage gap;
  • power-on plus SMpro progress with no banner gives one partial cycle;
  • changing the last token changes only the relation;
  • a refused pair is an open question on the join;
  • an ungated record is not a stated error;
  • UEFI followed by a loop refuses convergence.
• Inhabitance: a bundle claim runs the real console route end to end, from mtcollins1_boot_console_reading over the step-1 bytes to the account's RestartedRepeatedly ending after 00001a0a.
• Pre-existing red on main, fixed here: the_allowance_is_the_sum_of_the_bounds still hard-coded 10 SMpro probes after SMpro/PMpro internal error records: errmon registers, public decoder, capture row, collector #13058 raised the per-socket read order to 24 registers. Its oracle is now the sum of bounds over mtcollins1_smpro_read_order.

Side-chat review of 807e996: five gaps, all addressed

1. Cycles open only on typed evidence.
   • Cycle 1 opens on the confirmed power-on, or on a SEL Initiated by power up record. These are one boundary, never two.
   • Each SEL restart record opens one more cycle.
   • A console banner never opens a cycle. Spans bind only when the counts agree; otherwise they are ConsoleSpansUnbound.
   • REDs: two banners with no reset give one cycle and unbound spans, and not RestartedRepeatedly. The same console plus one reset gives two bound cycles.
2. Topology is judged only against the receipt.
   • AttemptConfigurationReceipt.expected is ExpectedSockets or ExpectedTopologyNotRecorded. Production records it as not recorded.
   • Without a recorded expectation, no ActiveSocketsBelowExpected, SocketNotJoined or DramSocketUntrained degradation is minted, and neither are the BMC inventory shortfalls. Each shortfall needs the expected topology or the DIMM population recorded.
   • SMpro readings are taken for the sockets each pass probed.
   • REDs: one active socket with nothing recorded gives questions only. A receipt expecting one socket is not degraded by one active socket.
3. Errors carry their cycle.
   • The milestone reader also locates each failure line (firmware statement, GRUB, initrd, panic, module refusal) in a span, using the owning modules' markers.
   • LocatedError.cycle is set through the same span binding. SMpro and SEL errors stay unbound.
   • Only a failure in the last cycle can choose the ending.
   • RED: a cycle-1 panic, then a reset, then a stable UEFI shell in cycle 2 ends at the shell. The panic is kept with cycle: 1.
4. SMpro/PMpro internal error records: errmon registers, public decoder, capture row, collector #13058's data is kept.
   • PendingAndDecoded { error: Absent, warning: Present } survives as a typed SmproWarningAccount.
   • The error-record registers get their own coverage carrier, SmproErrorRegisters.
   • REDs: a lone pending warning is kept. A CUR/BOOTSTAGE pair that reads while GPI/TYPE refuse gives SmproRegisters read and SmproErrorRegisters refused or partial.
5. Milestones carry provenance. Each milestone is a MilestoneEvidence { sighting, capture digest, reader } through the account and BootReachedUefiAfterSet. Control: the same line from two differently digested captures stays two facts.

Also changed:

• The refusal line now carries the open questions too.
• The bundle's route claim now runs on ONE real attempt: run 37069907299's console plus its own raw SEL window, where c26 is the power-up and c2b the restart, giving two typed cycles bound to two DRAM spans.

Observed caveat (step 1): on this MegaRAC, the first boot after a chassis power-on can be logged System Restart rather than Initiated by power up. Under the strict rule that is one cycle more than the console shows, so the account reports the spans unbound and does not guess. Step 1's before and after SEL snapshots also renumbered (the ids reset), so that window is no clean fixture.

CI fixes:

• New files import any and filter from v2.std.algebra explicitly (the floor's unimported-bare-provider rule).
• The sensor module's bare filter roster row is retired as ImportsFixed.
• Merged main (extdeps.ampere.nvparam: NVParamDef.h key table; decode the boot's NVPARAM dump #13059 NVPARAM): its nvparam field is carried through.

Local results at 21630c59d01: every touched witness file passes in full, 375 claims across 12 files, including NVPARAM 13/13 and physical orientation 16/16.

Side-chat review of 21630c5, plus the floor's NonFoldResidueRosterDiverged

1. SEL boot boundaries are typed per record. SelBootBoundaryStanding = PowerOnCorroboration | DistinctRestart | BoundaryAmbiguous.
   • A power-up row after the confirmed power-on corroborates it: one boundary.
   • A later restart is a distinct reset.
   • A first System Restart after the power-on with no power-up row is ambiguous. It opens no cycle and becomes the open question BootBoundaryAmbiguous, so it can never give a repeated-restart ending.
   • Records are never coalesced by time, because the BMC clock is not joined to ours.
   • REDs: power-on plus one first restart gives one cycle and the question, not RestartedRepeatedly. Run 37069907299 (c26 power-up, then c2b restart) stays the clean two-cycle control.
2. Absence needs an expectation.
   • SocketSensorsAbsent only for a socket the receipt expects.
   • A Redfish processor reading Absent becomes ProcessorAbsentOnExpectedSocket only on an expected socket. Unhealthy and other down states stay unconditional.
   • MemoryAbsentOnSocket only when the receipt records more populated slots on that socket than the BMC shows present. SlotRow now carries its socket.
   • Controls: expected [0] with CPU1 absent and no sensors gives no anomaly. An explicitly unpopulated slot reading Absent gives none. Both become anomalies when expected.
3. One located error per failure line. The milestone reader records every failure line. Panic and initrd errors are derived per line, each in its own cycle. RED: panic A in cycle 1, a reset, panic B in cycle 2. Both are kept with their cycles, and B ends the attempt.
4. The reader is a DeclarationRef. MilestoneEvidence.reader is decl_ref(gunbc.machine_intake_mtcollins1_console_milestone_observation, mtcollins1_console_milestones). A one-variant nullary sum does not resolve in this substrate, so the resolvable citation is used instead.
5. Floor NonFoldResidue. Every wildcard arm this PR added over a closed coproduct is now explicit arms: 39 sites across the account, bundle, boot_run and convergence. None is rostered.

Local results at c7beccad16e: 384/384 claims across 12 witness files.

Side-chat review of c7beccad, plus the floor's per-witness eval budget

1. One located error per occurrence, everywhere.
   • The firmware-statement, GRUB and module-refusal readers run over each console span's own lines (SpanConsoleReading, derived by span_console_readings from ampere_console_span_lines, the checkpoint reader's own fold).
   • Each error is bound to its span's cycle. Panics and initrd failures stay per line.
   • REDs: a GRUB failure in cycle 1, a reset, then a GRUB failure in cycle 2 keeps both, each in its own cycle, and the second ends the attempt. Two firmware statements give two errors.
2. The SEL classification is an ordered fold with no look-ahead.
   • Only the FIRST boot record can corroborate the power-on (a power-up) or be ambiguous (a restart after a confirmed power-on).
   • Every later record, a second power-up included, is a distinct boundary.
   • Controls: classify(prefix) == prefix(classify(prefix + later power-up)). A power-on plus two ordered power-ups gives an initial cycle plus one later cycle.
3. Completeness is per socket. ProcessorsListedBelowSockets, MemoryListedBelowSlots and MemoryAbsentOnSocket are replaced:
   • Processors, checked once per expected socket: ProcessorMissingOnExpectedSocket, ProcessorSocketDuplicated, ProcessorSocketUnreadable.
   • Memory, MemoryBelowRecordedPopulation per socket, over the union of expected-populated and observed sockets.
   • REDs: expecting [0, 1] with two members both naming socket 0 gives socket 1 missing and socket 0 duplicated. One recorded DIMM on socket 1, with a collection that lists only socket 0, reports socket 1.
4. Eval budget. Two reader claims exceeded the new-witness budget (72300 steps) by parsing the whole census capture. They now take lines 344–356 of it, the slice the relation claim is about. The bundle's route claim takes lines 1–89 of run 37069907299. The largest new claims now measure about 62k steps locally.

Local results at 86ee13ff0c7: every touched witness file passes in full: account 28/28, bundle 71/71, convergence 69/69, readers 14/14, SMpro 21/21 and 21/21, sensors 10/10, DRAM 17/17, kernel module 13/13, NVPARAM 13/13, physical orientation 16/16, MegaRAC media 87/87. No added wildcard arm remains.

Declared frontiers and deliberate departures (plan §10a, pushed with #13071's follow-up)

• Receipt live inputs: a declared frontier, slice B. The fleet-converge boot takes no stimulus, population or pre-power-on firmware input today. So mtcollins1_attempt_configuration_receipt records those fields as NotRecorded with that reason, and every question needing them is open. Historical rows are never used. Slice B (decided Q4) adds a boot-workflow input for:

  • the applied stimulus;
  • the current CPU and DIMM population;
  • firmware read back before power-on.

  The human inspection receipt comes through the existing operator-attested route. Trigger: slice B lands, and replaces these NotRecorded fields with the received values.

• The host is still the literal "mtcollins1". It becomes a ManagedHost row when Managed-host cut 0: gunbc.managed_host seam; reset roster as a filter over managed_hosts() #13055 lands (slice D).

• SMpro passes are reported per pass, not placed into cycles. No clock joins them to the console.

• MtCollins1SecondaryJoinReading.secondary_checkpoints is deleted (decided Q3). Attributing an opaque CP token to a socket decodes it, which R2 forbids in public. The field, its outcome counterpart secondary_host_checkpoints, the reference row's eight 1xxxxxxx tokens, the renderer and the witness uses are all removed. The public join outcome keeps only the SMpro stage words and the inter-socket lines. Per-socket CP classification belongs to the gunbc-private refinement slice.

🤖 Generated with Claude Code

[briansrls]

Re-reviewed exact head 807e9969fa51198ceaca892bbf67010c3242c65e. The root migration is directionally right: HostBootObservation is replaced atomically, convergence consumes a whole-account projection, the public checkpoint reader stays opaque, #13025's socket-attributed CP fields are deleted, the bundle/harness split is typed, and the hard-coded SMpro allowance is removed. Five load-bearing gaps remain.

1. A DRAM banner or any progress reading can still mint a boot cycle

dag/gunbc/machine_intake/mtcollins1_power_on_account.dag:564-582 takes the maximum of the admitted power/SEL boundaries, the number of banner spans, and a generic host-evidence floor. boundary_of then constructs OpenedByConsoleBannerOnly or OpenedByProgressEvidenceOnly when no power/reset boundary exists. The production account can therefore infer a restart merely because the banner printed twice.

The account witness does exactly that: dag/test/claim/machine_intake/mtcollins1_power_on_account_witness_test.dag:120-145 supplies SelEventsNotRead, two DRAM banners and no typed reset transition, then requires RestartedRepeatedly { cycles: 2 }.

That contradicts the approved plan's law: a DRAM banner binds a console span; it is not the authority that another cycle exists. A later cycle needs typed reset/restart boundary evidence. With two spans but no such evidence, retain one established cycle plus ConsoleSpansUnbound, not a fabricated repeated restart.

Required controls:

• two banners + no reset evidence -> no second cycle and no RestartedRepeatedly;
• the same bytes + one matching typed reset boundary -> two cycles.

2. NotRecorded attempt configuration still produces configuration-dependent degradations

The production receipt says current stimulus, CPU population, DIMM population and pre-power-on firmware are all NotRecorded, while expected_sockets is populated from the historical board census (dag/gunbc/machine_intake/mtcollins1_boot_diagnostic_bundle.dag:1464-1485). But degradations_of unconditionally uses that socket list to derive ActiveSocketsBelowExpected, SocketNotJoined and DramSocketUntrained (dag/gunbc/machine_intake/mtcollins1_power_on_account.dag:761-770).

So the account simultaneously says “the applied configuration is unknown” and judges the attempt as though it were a two-socket attempt. In particular, the socket-1-removed positive control can be reported as degraded even though its intended topology is one socket—the exact historical-row substitution law 6 forbids.

Until slice B supplies an attempt-specific expected topology/population, these must remain open questions. NotRecorded or Conflicted current configuration may not emit a topology/population degradation.

Required RED: a one-socket summary with current CPU/DIMM/stimulus NotRecorded produces configuration questions and no ActiveSocketsBelowExpected, SocketNotJoined, or DramSocketUntrained. A one-socket attempt receipt that explicitly expects one socket must likewise be non-degraded.

3. Unlocated earlier-cycle and unbound-pass failures can choose the final ending

LocatedError carries a subject but no cycle (dag/gunbc/machine_intake/mtcollins1_power_on_account.dag:268-282). console_errors explicitly flattens whole-capture failures without locating them in a span/cycle, and ending_failure then compares every such error's subject rank with only the last cycle's furthest milestone (dag/gunbc/machine_intake/mtcollins1_power_on_account.dag:626-705). SMpro failures are also taken from session-level passes that this PR correctly says cannot be joined to cycles, yet they enter the same ending population.

This lets an error from an earlier cycle—or an SMpro failure from an unbound pass—decide StoppedWithStatedFailure for a later cycle. Example: cycle 1 panics, a reset occurs, and cycle 2 reaches a stable UEFI shell. The global kernel error outranks UEFI and still wins the final ending.

Any error allowed to choose HostEnding must be bound to the cycle it ended. Evidence that cannot be joined to a cycle should remain explicitly unbound/session-level and cannot decide the final cycle's ending.

Required RED: cycle 1 kernel panic + typed reset + cycle 2 stable UEFI must preserve the cycle-1 error but must not end the session at that panic.

4. The #13058 integration can report complete coverage while losing records

Two separate losses occur:

• record_set_stated consumes only PendingAndDecoded.error; a gated pending warning is discarded, while record_set_anomalies also returns nothing for PendingAndDecoded (dag/gunbc/machine_intake/mtcollins1_power_on_account.dag:455-480). The old #13058 rendering retained both error and warning records.
• smpro_coverage is CarrierRead when any register word answered, and the account has no separate SmproErrorRecords carrier (dag/gunbc/machine_intake/mtcollins1_boot_diagnostic_bundle.dag:1388-1459). CUR/BOOTSTAGE could succeed while GPI and 0xA0-0xAD all refuse, and the account would report no error-record coverage gap.

Retain a pending warning as its own typed warning/anomaly standing, and restore completeness-aware coverage for the error-record register set separately from ordinary SMpro progress.

Required REDs:

• PendingAndDecoded { error: Absent, warning: Present } survives into the account;
• a progress word read with all error-record registers refused yields SmproRegisters = Read and SmproErrorRecords = Refused/Partial, not one blanket Read.

5. Q1's milestone provenance is lost at the account boundary

ConsoleMilestoneSighting carries the line, marker, line index and span, but no capture digest and no typed parser/reader identity (dag/gunbc/machine_intake/mtcollins1_console_milestone_observation.dag:52-58). The digest exists in ConsoleEvidence while folding, but PowerOnAccount retains only the sightings. FirmwareSetBootReadback then exports the account without the evidence identity that established its UEFI milestone.

Carry either a milestone evidence reference or an account-level console observation identity containing the capture digest and reader/parser declaration. The line index is useful ordering evidence, but it is not source identity.

Required control: identical milestone text from two differently digested captures remains distinguishable in the resulting account/readback.

These changes do not require reopening R1/R2/R3 or the private mechanism boundary. They make the implementation obey the approved account laws instead of letting the new aggregate overstate what the available evidence establishes.

[briansrls]

Re-reviewed exact head 21630c59d01e87d851687e369f1871037b5a4b7d. The five requested areas are materially improved: banners/progress no longer mint cycles, the main topology degradations and inventory-count shortfalls are receipt-gated, only final-cycle located failures enter ending_failure, pending warnings survive, error registers have separate coverage, and milestone evidence retains the capture digest. Four load-bearing issues remain.

1. The observed System Restart caveat is not safe as-is

is_restart_boundary(SystemRestart) is unconditionally true, and cycle_boundaries appends every such row after the admitted power-on. On the known MegaRAC behavior—one admitted power-on, one initial-boot System Restart, one console span—the account creates two cycles, binds no span, gives both cycles reach -1, and last_cycle_repeats can therefore produce RestartedRepeatedly. That is a strong false conclusion, not merely an honest unbound-span standing.

Do not identify every restart row in the broad before/after SEL window with power-on either: SelWindowEvent explicitly carries an unjoined BMC clock rendering, so membership in that delta does not prove temporal identity with the power transition.

Use a typed interpretation between raw SEL rows and cycle boundaries, for example:

SelBootBoundaryStanding
  = PowerOnCorroboration { record }
  | DistinctRestart { record }
  | BoundaryAmbiguous { record, reason }

A clean rule available from current ordering is:

• confirmed power-on plus an explicit InitiatedByPowerUp row: that row corroborates cycle 1; later restart rows are distinct;
• confirmed power-on, no explicit power-up row, and a first SystemRestart: it may be the MegaRAC's initial-boot rendering, so it is ambiguous and must not mint an extra cycle or RestartedRepeatedly;
• later restart rows can then establish later boundaries.

Required controls:

• power-on + one SystemRestart + one banner does not become two cycles or RestartedRepeatedly;
• explicit power-up + later SystemRestart still gives two cycles for run 37069907299.

2. Historical/absent-resource topology still leaks through BMC anomalies

The three headline degradations are gated, but the bundle still calls:

mtcollins1_sensor_anomalies(..., sockets: mtcollins1_census_sockets())

while the production attempt receipt says expected topology is not recorded. That can mint SocketSensorsAbsent { socket: 1 } from the historical two-socket census during an intentionally one-socket attempt.

The inventory path has the same semantic leak at member grain: processor_anomalies treats StateAbsent as ProcessorNotNominal without checking expected sockets, and memory_anomalies emits MemoryAbsentOnSocket for every absent member without checking the attempt's DIMM population. StateAbsent is a direct observation, but whether absence is anomalous is an expectation-dependent judgment.

Keep the raw resource states in the observation. Mint absence anomalies only when the attempt receipt says the socket/slot was expected populated. Health Warning/Critical can remain unconditional.

Required controls:

• ExpectedSockets [0] plus no CPU1 sensors and a CPU1 StateAbsent member produces no socket-1 absence anomaly;
• an explicitly unpopulated DIMM row plus Redfish StateAbsent produces no MemoryAbsentOnSocket;
• the same observations become anomalies when the receipt says those resources were expected.

3. Failure-to-cycle binding still joins only by failure kind

ConsoleFailureSighting carries only kind, line_index, and span. locate_console_error filters by failure_kind_matches and takes .first(). Therefore every kernel panic, initrd failure, GRUB failure, etc. is attached to the first sighting of that kind, even when the same kind occurs in multiple cycles.

A session with a panic in cycle 1 and a different panic in cycle 2 cannot be represented correctly: the final-cycle panic may be attached to cycle 1 and therefore be unable to choose the final ending. The existing RED has only one panic, so it does not discriminate this join.

Bind by exact occurrence—line/index plus parser result—or derive one decoded LocatedError directly from each failure sighting. Required RED: two distinct kernel-panic lines in two cycles are both retained with their own cycle, and the cycle-2 panic chooses the ending.

4. The milestone reader identity is still free text

MilestoneEvidence.reader is NonEmptyStr, populated by the string "gunbc.machine_intake_mtcollins1_console_milestone_observation mtcollins1_console_milestones". The control checks that the string contains the function name. Renaming or deleting the reader leaves the evidence and test green, so the requested parser/reader identity is not structural.

Use DeclarationRef (or a closed reader-identity sum) and construct it with decl_ref. Add a stale-rename control, or rely on symbol resolution so a rename breaks the reference.

The answer to the caveat is therefore: yes, add a typed power-on/reset interpretation, but do not coalesce solely because the raw record is inside the broad SEL delta. Ambiguity must remain ambiguity and must not decide an extra cycle or repeated-restart ending.

The atomic R1 replacement, opaque public checkpoint boundary, #13025 field deletion, gated #13058 records, and convergence projection remain directionally approved. Exact-head CI is still running; these blockers are semantic regardless of its result.

[briansrls]

Re-reviewed exact head c7beccad16ef5f19f96ea12bfcb347330e2c4ebd. The requested changes mostly land: an ambiguous first restart no longer opens a cycle; the clean 37069907299 power-up→restart route stays two cycles; explicit absent processor/member/sensor observations are gated by the attempt receipt; panic and initrd lines are occurrence-local; the milestone reader is a DeclarationRef; and the new closed-sum matches are explicit rather than rostered. Three structural gaps remain.

1. The account still does not produce one located error per failure occurrence

ConsoleFailureSighting now retains every line, but console_errors derives occurrence-local errors only for KernelPanicLine and InitrdLoadFailureLine. FirmwareStatement, BootLoaderFailed, and KernelModuleRefused are still whole-capture aggregates from console_errors_unlocated, then locate_console_error binds each aggregate to filter(... kind ...).first().

Therefore two GRUB failures in different cycles still collapse into one BootLoaderFailed { errors: all_capture_errors } located in the first cycle. The later-cycle failure cannot choose the final ending. The same defect remains for firmware statements and module-decompression refusals.

Required repair: run each owning reader at span/cycle grain, or derive an exact decoded error from each sighting/occurrence. Add a RED with a GRUB terminal in cycle 1, a reset, a different GRUB terminal in cycle 2; both must be retained with their cycles and the second must choose the ending. The two-panic RED alone does not discriminate the remaining aggregate paths.

2. SEL boundary classification is not prefix-stable and drops later power-up boundaries

sel_boundary_standings computes power_up_seen over the entire future record list before folding it. Appending a later InitiatedByPowerUp can therefore retroactively change an earlier first SystemRestart from BoundaryAmbiguous to DistinctRestart.

Also, every power-up row becomes PowerOnCorroboration. The first may corroborate/open the admitted initial power-on, but a second InitiatedByPowerUp is evidence of a later power cycle and currently opens no cycle at all.

Make the classification an ordered stateful fold: exactly the initial qualifying power-up may corroborate/open the first boundary; later boot-init rows—including later power-up rows—are distinct boundaries. Required controls:

• classification of a prefix does not change when a later power-up row is appended;
• confirmed power-on plus two ordered InitiatedByPowerUp rows yields an initial boundary plus one later cycle, not one cycle.

3. Absence is receipt-gated, but expected-resource completeness is still count/observed-population based

processor_anomalies uses count(ps) < count(expected_sockets). Two distinct processor members both naming socket 0 satisfy expected [0, 1] and produce no missing-socket anomaly.

memory_anomalies iterates only the socket identities present in the Redfish member population. If the receipt records a populated DIMM on socket 1 but Redfish returns no socket-1 members at all, socket 1 is never examined. populated_short compares total member rows—including absent/unpopulated rows on other sockets—to the number of expected populated rows, so those unrelated rows can mask the omission.

Join completeness by identity:

• for processors, evaluate each expected socket against the parsed member socket population and refuse/report duplicates or missing members independently of total count;
• for memory, iterate the union of expected-populated sockets and observed sockets, then compare present members to the receipt's populated count per socket.

Required REDs:

• expected [0,1] plus two members both naming socket 0 does not satisfy processor completeness;
• one populated receipt row on socket 1 plus a complete Redfish collection containing members only on socket 0 reports the socket-1 absence.

The reader citation, ambiguous-first-restart behavior, explicit absence controls, and NonFoldResidue cleanup are otherwise accepted. Exact-head CI is currently queued; these are semantic blockers independently of its result.

[briansrls]

Re-reviewed exact head 86ee13ff0c7d645dfcf6cbbaf790e0269448720a. The three blockers from the c7beccad review are closed.

1. Failure occurrences no longer collapse across cycles. ampere_console_span_lines partitions the raw console with the checkpoint reader's own fold. span_console_readings then runs the firmware, GRUB, and module-refusal owners over each span separately, and console_errors binds each resulting error through that span's cycle. Panic and initrd failures remain line-local. The two-cycle GRUB control is discriminating: it requires two located BootLoaderFailed values, one in each cycle, and requires the final ending to carry the distinct second-cycle error.

2. SEL boundary classification is prefix-stable. sel_boundary_standings is now a left-to-right fold with no whole-population look-ahead. Only the first boot record can corroborate the admitted power-on or be ambiguous; every later boot record is a distinct boundary, including a later InitiatedByPowerUp. The prefix-extension control and the power-on-plus-two-power-ups control exercise both sides of that rule.

3. Inventory completeness is keyed by socket identity. Processor completeness is evaluated independently for every expected socket, with separate missing, duplicated, and unreadable-socket outcomes. Memory completeness iterates the union of receipt-populated sockets and observed sockets, then compares present members with the recorded populated count per socket. The duplicate-socket processor RED and the wholly unmentioned socket-1 memory RED both falsify the prior count-based implementations.

The eval-budget repair narrows only the supplied witness excerpts to the bytes each claim actually reads; it does not narrow the production readers or account. The exact-head local receipt reports 400/400 claims across the 12 touched witness files, with the largest new claim below the 72.3k-step wall.

No semantic blocker remains. Exact-head required CI is still queued, so this approval is conditional only on the ordinary requirement that the witnesses workflow finish green before landing.