Model firmware targets, boot diagnostics, and memory part selection

[briansrls]

Modeling work from a live srv3/srv4 incident: both hosts failed to boot after a DIMM upgrade. The first failure was host firmware three years stale — fixed, and both hosts now train all eight modules. The residual failure is a DDR4 LRDIMM data-buffer training step.

Nothing here is a blocklist. Each avoidance is derived from a mechanism, so a future ordering workflow can shop the whole market and explain every refusal by naming the failing step, rather than being locked to a vendor list.

New modules

extdeps.firmware.types — FirmwareTarget = BmcController | HostBios. The fleet could express which BMC image a host should run and had no way to express which BIOS, though BIOS owns DDR training. FirmwareImageKind distinguishes the OpenBMC tar (pushable to a dead host) from the Instant Flash ROM (needs a booting host). FirmwareReleaseRow carries a prerequisite, so an unappliable push is refused from the catalog rather than discovered from a vendor shell script after a 33 MB upload — which is exactly how it was discovered.

Consolidates BmcFirmwareSemanticVersion to FirmwareSemanticVersion across 8 files. A version triple is one concept; minting a second name for host firmware would be the CpuArchitecture/TargetArchitecture class section 3 names.

extdeps.ampere.scp_diagnostic — SCP console tokens as class + number, with meaning held separately. Deliberately no token-to-meaning function: no codebook was obtained, so every implementation of one would be invention. The E prefix classifies a namespace, not a consequence — E559/E571 appear on a same-family machine that boots normally. DiagnosticReadEffect records that several of these interfaces mutate what they report, which bit us: the error queues were polled repeatedly before their clear-on-read semantics were understood.

extdeps.memory.training — training steps with the required set derived from buffering. A registered module has no data buffer and therefore cannot fail buffer calibration: a difference in kind, not a probability, which is what makes it sound as a purchase filter. capacity_reachable_as_dual_rank_registered derives from JEDEC die density why cheap high-capacity DDR4 is disproportionately load-reduced.

gunbc.host_memory_qualification — four independent standings: board class support, specific part qualification, DDR training outcome, host boot outcome. None derives another. Their collapse into one "does the RAM work" question cost three refuted hypotheses during the incident. Causal experiments land as receipts, including HypothesisWeakenedByIntervention for an intervention weaker than the one that would settle the question — the CMOS cable pull, versus the vendor's documented battery plus CLRMOS1 procedure.

gunbc.memory_part_selection — a candidate is refused iff it must execute a step this board has been observed to fail, independent of vendor, part number, capacity, speed grade, or AVL membership. Implication is not a Pareto objective: implicated parts are refused before the frontier is computed, because trading "might not train" against price is how the failing modules were bought.

gunbc.host_boot_supervision and gunbc.host_diagnostic_channel — two independent reset supervisors kept separate because only one is configurable. Interval typed by how it is known: powermon's 306s is IntervalMeasured from eleven journal timestamps, not IntervalDeclared — storing it in a field called interval would present a measurement as a setting. Five diagnostic authorities with their transports, plus the standing that a missing projection does not establish a missing source.

Evidence discipline

• Every digest was measured by acquiring the artifact and hashing it. Nothing transcribed.
• The MREP evidence is typed AssociatedByIdenticalSignature, not DecodedFromPlatformSyndrome — we never read our own syndrome register. Ampere documents SCP register B5 as carrying the per-DIMM training syndrome that would upgrade this; it was not read because neither the BMC nor the session host has ipmitool. Recorded as the upgrade path.
• The BMC 03.22.00 row stays digest-Absent with an unobserved locator, and the note says so rather than implying it is fetchable.

Witnesses

dag/test/claim/host_memory_qualification_witness_test.dag covers the eight properties an external review required, with RED controls: population slot identity, training does not imply boot (plus positive control), class support does not imply part qualification, P-code does not imply error, E-code does not imply fatal, projection absence does not imply source absence, destructive read is not a snapshot.

Not verified

This has not been compiled. The local gunbc compile --target dag path rejects // at 1536 files corpus-wide, nearly all untouched by this branch, so it does not implement the section 4c annotation channel and cannot check this work. CI is the first real compile, and I expect it to find things.

No new scaffolds and no dissolution obligations introduced.

🤖 Generated with Claude Code

https://claude.ai/code/session_01CuRVynkbQYGqjmf9AnyxsS

[gunbai-bot]

Both items from review 51280 verified against the current code.

Blocking — bare Nat byte count: fixed. Confirmed present. Naming it symbolically rather than positionally (the review cited line 369; the symbol is at 350): extdeps.boards.asrock_rack asrock_altrad8ud_bios_3_10_obmc_push_artifact_bytes was the last bare-Nat byte count in the diff, and it sat in the same file as FirmwareReleaseRow.image_bytes, which had already moved to ByteSize — so it was a fork of the carrier within one file, which is the sharper version of the finding. Now byte_size(count: 33566720). It has no consumers, so nothing downstream changed shape.

Non-blocking — unused imports in extdeps.memory.training: declining, with a reason. The observation is correct: DimmBuffering, DramGeneration, bit_width, byte_size, byte_size_count, bit_width_count, ByteSize, BitWidth and NonEmptyStr each occur exactly once in that file — on the import line itself. I am not removing them, because removing an unused .dag import is not a no-op in this repository right now. DESIGN.md's #6985 open thread records Class B: a stripped file's bare cross-module references resolve only by pool-membership coincidence — resolve_in finds a target module exactly when some unrelated unstripped import elsewhere in the assembled closure has already dragged it into the pool — and concludes verbatim that this "blocks all further dag/** import-stripping until a closure-independent binding fix or a provable-coverage construction check lands." Neither has landed. So a cosmetically clean import list here can red an unrelated module whose binding was riding on this one's pool contribution, and the failure would surface far from this PR.

That is a standing repository constraint rather than a preference of mine, so I would rather leave the noise visible than take a housekeeping win that the corpus explicitly says is unsafe. If the intent is to clean these up, the honest route is the closure-independent binding fix that thread names, which retires the whole class at once instead of one file at a time.

— sent from quiet-badger-563

[gunbai-bot]

Two rounds of feedback addressed here, plus a defect I found in my own model that neither review caught.

review 51292 — both findings verified and fixed. firmware_release_applicability and host_boot_loop_cause had zero importing consumers and zero witnesses, which is specification-without-execution on the two functions this PR's fail-closed claims rest on. Applicability now has five rows binding the production release rows rather than fixtures: unreadable version refuses (the srv3 BIOS-null case), the real srv3 push at 2.07.00 is Unmet carrying what it observed, srv4's at 3.22.00 is Applicable, 3.06.00 is Unmet (higher major, lower minor — a major-only compare would wrongly admit it, and it's a real catalogued image), and the Instant Flash ROM row is Applicable on the same Absent observation that refuses on the tar row. Loop cause gets the powermon refutation as an executing check: the same E588 signature answers HostSelfResetOnError after the supervisor was stopped and the loop persisted, and LoopCauseConfounded when it wasn't — period alone can't decide it, since a 306-second cycle looks identical whether or not a 306-second timeout causes it.

The bigger problem, which I'd built in myself. The selection rule refused any module that merely executes a step some platform was observed to fail — on any board, at any evidence standing, including EvidenceUnobserved. Since capacities near a generation's die-density ceiling are disproportionately load-reduced, that removed most of the 64GB DDR4 market by construction. It was the blocklist this module's own prose claims to avoid, reached by a different route, and it defeated the actual purchasing goal it was written to serve.

Severity is now a function of evidence — which TrainingEvidenceStanding was already carrying and the verdict was discarding:

standing	verdict
DecodedFromPlatformSyndrome	refuse
AssociatedByIdenticalSignature / InferredFromSequencePosition	sample required, stays on the frontier
EvidenceUnobserved	implicates nothing

gunbc holds MREP at association standing, so the honest verdict for another ALTRAD8UD LRDIMM is buy-one-and-test, not reject. Failures are also scoped to the board they were observed on. Witnesses hold board, step and module fixed and vary only the evidence, so the grading is discriminating rather than incidental; two frontier rows show an association leaves both candidates ranked while a decoded refusal still drops one.

Declared gap rather than a silent one: BaseboardModel has exactly one variant today, so the board scoping is real in the code but has no executing cross-board control. Minting a second board purely to test it would be a fabricated entity — that control lands when a second real board is modeled.

— sent from quiet-badger-563

[gunbai-bot]

Checked review 51323 by simulating the exact code before changing anything. The finding as stated does not reproduce — but there is a real defect underneath it, in the opposite direction. Both are worth recording.

Not reproduced. The cited candidate ["A1","A1","B1","E1"] is refused today. population_slots_match folds a over b, and the call site passes a = p.slots (the documented row) and b = candidate — so the subset test runs documented-into-candidate, not candidate-into-documented as the finding describes. A duplicated candidate slot shrinks its distinct set, so a same-length documented row with four distinct slots can't be covered by it. I ran all four documented rows against that candidate and the other cases to confirm.

Real, and latent. The guard was equal-length-plus-subset rather than multiset equality, and it rested on an unstated precondition: that no documented row carries a duplicate. Violate that and it fails in the mirror direction of the report — documented ["A1","A1"] admits candidate ["A1","B1"], because both documented entries are found and the lengths agree. No board row has a duplicate today, which is exactly why it was latent, and why leaving correctness resting on that staying true is the wrong place to stop. So the conclusion — this needs multiset equality — was right even though the failing case wasn't.

Now compares occurrence counts. Three controls:

• the duplicated candidate stays refused (the property callers rely on, previously true only incidentally);
• a synthetic duplicated documented row does not admit a distinct pair — the case that was actually broken;
• that same row still admits its own multiset, so the refusal is multiset discrimination rather than a blanket rejection of duplicated rows.

The synthetic row is deliberate: no real board row has a duplicate, so the control has to construct one, and that's the point — the guard shouldn't depend on the corpus happening to stay duplicate-free.

— sent from quiet-badger-563

[gunbai-bot]

Taken, but the stated reasoning doesn't hold and the record is worth correcting.

The claim that it won't compile is false, and it was cheap to check. host_boot_loop_cause executed green in CI run 31566167444 — all three of its witnesses passed, including loop_persisting_after_supervisor_stop_is_host_self_reset and no_error_code_after_a_clean_stop_is_unobserved_not_attributed, which exercise the Present and Absent arms respectively. Bare Absent resolves in this corpus without the import: extdeps.bmc.capability matches on it in three arms and bmc_fan_converge_witness_test in two, both without a v2.std.optional import, and both green on main.

I've made the change anyway, because it's right for a different reason. That resolution works by pool-membership coincidence — the target module lands in the assembled closure only because some unrelated import elsewhere dragged it there. That's exactly the #6985 Class B hazard DESIGN records, and the remedy that thread names is making the binding closure-independent with an explicit import. asrock_live_probe_witness_test carries the same repair with the same rationale in its own note. So it isn't cosmetic: it removes a dependency on accidental closure membership that breaks the next time an unrelated lane edits its imports.

Flagging the distinction because it changes what the finding is worth. "This is broken" would have meant the witnesses I added were never executing — they were, and they're green. "This is fragile" is true and worth fixing. Those warrant different confidence, and I'd rather not let a fixed-because-asked read as a defect that existed.

Related, since it came up in review 51318 and again here: I fixed this same import class in extdeps.firmware.types and two witnesses earlier tonight after importing Present/Absent from std.types, where they genuinely don't live — that one was a hard resolution error. Omitting the import and importing it from the wrong module are different failures, and only the second breaks the build.

— sent from quiet-badger-563