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

dag/extdeps/linux/boot_console.dag

@@ -0,0 +1,41 @@
+module extdeps.linux.boot_console
+
+import std.types { NonEmptyStr }
+import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef }
+import std.decl_ref { DeclarationRef, WholeDeclaration }
+import extdeps.uri { Https, Uri }
+
+// THE KERNEL'S OWN CONSOLE LINES THE BOOT MODEL READS. Its panic line, Linux v6.8 kernel/panic.c: panic() prints
+// pr_emerg("Kernel panic - not syncing: %s\n", buf) once, and its end marker
+// "---[ end Kernel panic - not syncing: %s ]---". The reason after the prefix is the caller's text.
+data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
+  uri: Uri {
+    scheme: Https
+    locator: "github.com/torvalds/linux/blob/v6.8/kernel/panic.c"
+  }
+}
+
+data extdeps_model_scope: ExternalModelScope = ExternalModelScope {
+  subject: ExternalSubjectRef {
+    declaration: DeclarationRef {
+      module_path: "extdeps.linux.boot_console",
+      decl_name: "linux_kernel_panic_prefix",
+      field: WholeDeclaration
+    }
+  },
+  first_citation: extdeps_external_authority_anchor,
+  further_citations: [
+    ExternalAuthority {
+      uri: Uri { scheme: Https, locator: "github.com/torvalds/linux/blob/v6.8/init/version-timestamp.c" },
+    },
+  ],
+}
+
+// init/version-timestamp.c linux_banner: "Linux version " UTS_RELEASE ..., the first line the
+// kernel proper prints, so its presence establishes that the stub handed off to the kernel.
+data linux_banner_prefix: NonEmptyStr = "Linux version "
+
+data linux_kernel_panic_prefix: NonEmptyStr = "Kernel panic - not syncing: "
+
+// The end marker repeats the prefix; a reader that took it as a second panic would count one twice.
+data linux_kernel_panic_end_marker: NonEmptyStr = "---[ end Kernel panic - not syncing: "

dag/extdeps/linux/efi_stub.dag

@@ -0,0 +1,50 @@
+module extdeps.linux.efi_stub
+
+import std.types { NonEmptyStr }
+import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef }
+import std.decl_ref { DeclarationRef, WholeDeclaration }
+import extdeps.uri { Https, Uri }
+
+// THE LINUX EFI STUB'S CONSOLE LINES, Linux v6.8 drivers/firmware/efi/libstub. The stub runs as a
+// UEFI application before the kernel proper: efi_printk (printk.c) writes "EFI stub: " before every
+// message, efi_err (efistub.h) prefixes "ERROR: ", and efi_load_initrd (efi-stub-helper.c) prints
+// efi_err("Failed to load initrd: 0x%lx\n", status) when no initrd could be loaded, status being the
+// UEFI status it got. Only the lines the boot model reads are carried.
+data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
+  uri: Uri {
+    scheme: Https
+    locator: "github.com/torvalds/linux/blob/v6.8/drivers/firmware/efi/libstub/efi-stub-helper.c"
+  }
+}
+
+data extdeps_model_scope: ExternalModelScope = ExternalModelScope {
+  subject: ExternalSubjectRef {
+    declaration: DeclarationRef {
+      module_path: "extdeps.linux.efi_stub",
+      decl_name: "linux_efi_stub_initrd_load_failed_prefix",
+      field: WholeDeclaration
+    }
+  },
+  first_citation: extdeps_external_authority_anchor,
+  further_citations: [
+    ExternalAuthority {
+      uri: Uri { scheme: Https, locator: "github.com/torvalds/linux/blob/v6.8/drivers/firmware/efi/libstub/printk.c" },
+    },
+    ExternalAuthority {
+      uri: Uri { scheme: Https, locator: "github.com/torvalds/linux/blob/v6.8/drivers/firmware/efi/libstub/efistub.h" },
+    },
+    ExternalAuthority {
+      uri: Uri { scheme: Https, locator: "github.com/torvalds/linux/blob/v6.8/include/linux/efi.h" },
+    },
+  ],
+}
+
+// efi_printk: efi_puts("EFI stub: ") before the message.
+data linux_efi_stub_line_prefix: NonEmptyStr = "EFI stub: "
+
+// efi_err("Failed to load initrd: 0x%lx\n", status), so the whole printed prefix of the line.
+data linux_efi_stub_initrd_load_failed_prefix: NonEmptyStr = "EFI stub: ERROR: Failed to load initrd: 0x"
+
+// include/linux/efi.h: #define EFI_LOAD_ERROR ( 1 | (1UL << (BITS_PER_LONG-1))), printed by %lx on a
+// 64-bit stub. Any other status is carried as its printed digits, never mapped onto this one.
+data linux_efi_load_error_rendering: NonEmptyStr = "8000000000000001"

dag/gunbc/extdeps_scope_frontier.dag

@@ -374,6 +374,8 @@ data scope_carrier_paths: List<String> = [
   "dag/extdeps/instrument/fs_box_v3_v4_v5_faq.dag",
   "dag/extdeps/linux/edac.dag",
   "dag/extdeps/linux/kernel.dag",
+  "dag/extdeps/linux/efi_stub.dag",
+  "dag/extdeps/linux/boot_console.dag",
   "dag/extdeps/linux/mlx5_core.dag",
   "dag/extdeps/linux/proc_self_cgroup.dag",
   "dag/extdeps/os/debian.dag",

dag/gunbc/fleet/mtcollins_firmware_converge.dag

@@ -43,9 +43,11 @@ import gunbc.auth.authorization_pattern_selection {
 import gunbc.machine_intake_bmc_secure {
   BmcSecureStanding, BmcSecureRefusalCause, BmcSecured, BmcSecureRefused, ManagedCredentialReference,
 }
-import gunbc.machine_intake_boot_outcome {
-  HostBootObservation, HostReachedUefi, PostDdrProgressLost, HostBootUnobservable, ResetInitiator,
+import gunbc.machine_intake_mtcollins1_power_on_account {
+  FirmwareSetBootReadback, BootReachedUefiAfterSet, BootProgressLostAfterSet, BootReadbackUnobservable,
+  HostEnding, RestartedRepeatedly, ReachedCensus, StoppedWithStatedFailure, StoppedWithoutRestart, HostEndingNotEstablished,
 }
+import gunbc.machine_intake_ampere_checkpoint_console_observation { AmpereCheckpointRelation }
 import gunbc.machine_intake_mtcollins1_boot_diagnostic_bundle {
   SelSnapshotReading, SelSnapshotRead, SelSnapshotUnread, SelSnapshotNotTaken,
 }
@@ -363,8 +365,9 @@ type MtCollinsFirmwareWorld {
 }
 
 // WHAT THE HOST DID WHEN IT FIRST BOOTED AFTER THE SET is the only observation that says the set worked,
-// and it is gunbc.machine_intake_boot_outcome's fact, not this module's. Reaching UEFI grounds the set;
-// PostDdrProgressLost refuses.
+// and it is the power-on account's fact (gunbc.machine_intake_mtcollins1_power_on_account
+// firmware_set_boot_readback), not this module's. A UEFI milestone grounds the set unless the session
+// then restarted repeatedly; lost progress refuses (boot_verdict).
 
 // The witnessed AC power cycle. It is an operator-attested record: the substrate cannot see a power
 // cord, which is why selecting HumanOnlyStep was the honest answer. ac_off is what the
@@ -443,7 +446,8 @@ type FirmwareConvergenceRefusal
   | AcPowerCycleTooShort { target: FirmwareTarget, observed: Second, minimum: Second }
   | ReadbackMismatch { target: FirmwareTarget, reason: String }
   | AcCycleNotAHumanStep { target: FirmwareTarget }
-  | BootProgressLostAfterFirmwareSet { last_checkpoint: Int, soc_silent: Second, initiator: ResetInitiator }
+  | BootProgressLostAfterFirmwareSet { ending: HostEnding, last_relation: AmpereCheckpointRelation? }
+  | BootReachedUefiThenRestartedRepeatedly { cycle: Int, ending: HostEnding }
   | CpuSiliconSupportUnstated { socket: Nat, bios_family: NonEmptyStr }
   | NoRollbackImageRetained { target: FirmwareTarget, reason: NonEmptyStr }
   | RollbackImageNotTheInstalledVersion { target: FirmwareTarget }
@@ -1076,17 +1080,27 @@ fn uncited_readbacks(records: List<FlashStepRecord>) -> List<UncitedReadback> {
     })
 }
 
-fn boot_verdict(records: List<FlashStepRecord>, boot: HostBootObservation?) -> FirmwareConvergenceVerdict {
+// THE POST-SET READBACK IS A PROJECTION OF THE WHOLE POWER-ON ACCOUNT (gunbc.machine_intake_mtcollins1_power_on_account
+// firmware_set_boot_readback; ruling R1 on #13041 and #13071), never an authored observation. A UEFI
+// milestone in any cycle grounds the set unless the session then restarted repeatedly: reaching UEFI
+// and looping afterwards is not a converged boot, so both facts are read together.
+fn boot_verdict(records: List<FlashStepRecord>, boot: FirmwareSetBootReadback?) -> FirmwareConvergenceVerdict {
   match records.first() {
     Absent => FirmwareBaselineConverged { uncited_readbacks: [] }
     Present { value: _ } =>
       match boot {
         Absent => FirmwareBootReadbackDue
         Present { value: o } =>
           match o {
-            HostReachedUefi => FirmwareBaselineConverged { uncited_readbacks: uncited_readbacks(records: records) }
-            PostDdrProgressLost { last_checkpoint: c, soc_silent: q, chassis_power_on_while_silent: _, next_cycle_logged_s5_and_system_restart: _, watchdog: _, initiator: i } => refused(cause: BootProgressLostAfterFirmwareSet { last_checkpoint: c, soc_silent: q, initiator: i })
-            HostBootUnobservable { reason: r } => refused(cause: BootOutcomeUnobservable { reason: r })
+            BootReachedUefiAfterSet { cycle: c, milestone: _, ending: e, degradations: _, account: _ } => match e {
+              RestartedRepeatedly { cycles: _, last_cycle_ended_after: _, cadence: _, console_errors: _, sel_restarts: _, watchdog: _, reset_cause: _ } => refused(cause: BootReachedUefiThenRestartedRepeatedly { cycle: c, ending: e })
+              ReachedCensus => FirmwareBaselineConverged { uncited_readbacks: uncited_readbacks(records: records) }
+              StoppedWithStatedFailure { subject: _, error: _ } => FirmwareBaselineConverged { uncited_readbacks: uncited_readbacks(records: records) }
+              StoppedWithoutRestart { last_milestone: _, ended_after: _, console_errors: _, restarts_before: _ } => FirmwareBaselineConverged { uncited_readbacks: uncited_readbacks(records: records) }
+              HostEndingNotEstablished => FirmwareBaselineConverged { uncited_readbacks: uncited_readbacks(records: records) }
+            }
+            BootProgressLostAfterSet { ending: e, last_relation: r, account: _ } => refused(cause: BootProgressLostAfterFirmwareSet { ending: e, last_relation: r })
+            BootReadbackUnobservable { account: _ } => refused(cause: BootOutcomeUnobservable { reason: "the power-on account establishes neither a UEFI milestone nor a lost-progress ending" })
           }
       }
   }
@@ -1096,7 +1110,7 @@ fn converge_firmware(
   baseline: FirmwareBaseline,
   world: MtCollinsFirmwareWorld,
   records: List<FlashStepRecord>,
-  boot: HostBootObservation?,
+  boot: FirmwareSetBootReadback?,
 ) -> FirmwareConvergenceVerdict {
   match baseline_admission_refusal(b: baseline) {
     Present { value: cause } => refused(cause: BaselineNotAdmitted { cause: cause })