From 7dc4fd8fcc52bb8ed45c71212f36d95e87ddb7dc Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 22 Aug 2026 22:48:38 +0000 Subject: [PATCH 1/5] Model the 64 GiB DIMM upgrade: an OEM offering, a stacking axis, and the fleet's first measured MemTotal The fleet moved from 8 x 16 GiB SK hynix to 8 x 64 GiB Samsung on 2026-08-22. srv1, srv3 and srv4 took it; srv2 could not train it and was reverted. Nothing in the corpus described any of that, and two notes actively asserted the replacement had failed on every host. WHAT THE PART FORCED. DramModuleCatalogRow could not say whether a module was stacked -- DramDieStacking existed for the controller-admission question and the row carrying modules did not reference it -- so a 3DS RDIMM and a monolithic one were indistinguishable in the only carrier a consumer reads. die_stacking is now a required field, required rather than optional because the state it excludes is precisely the one that produced this: a stacked module authored by someone unaware of the axis. rank_count stays one field. Both of its consumers are correct for a stacked part when it carries the LOGICAL rank organization: required_die_density divides to a per-die figure, which is what JEDEC's monolithic ceiling bounds, and devices_per_stick multiplies to a die count, which is what a stacked package holds. Neither wanted a package count. Cisco's octal rank goes in the catalog; the BMCs' RankCount=2 stays with the host observations that produced it. The realizability wall passes at BOTH values, so this was settled by citation and not by the check -- recorded in the row, because a green there proves nothing. CISCO AND SAMSUNG ARE TWO AUTHORITIES. OemModuleOffering references the module rather than restating its axes, so a second reseller is a new row and no edit to Samsung. OemModuleLinkEvidence has two arms because "a supplier documented it" and "the operator read the label" are different epistemics, and only the second is available here: cisco.com's per-PID sheets refuse automated retrieval, so the link rests on the physical label. THE FIRST MemTotal THIS FLEET HAS CARRIED. srv3 and srv4 read 502.25 GiB against 512 GiB nominal -- a 9.75 GiB firmware and kernel reservation, now measured instead of asserted. Writing the Redfish figure into gunbc_ci_host_usable_ram_for would have overstated the budget's ceiling by nearly ten gibibytes per host, which is the error that carrier exists to prevent and which became available the moment the BMC reported a bigger number. srv1 keeps the bound because its upgrade is operator-reported rather than read here; srv2 keeps it because it genuinely still carries 16 GiB modules. Same arm, same value, opposite reasons. srv2's FAILURE IS THE MOST INFORMATIVE ROW. It is recorded as RepeatingFirmwareReset with training left Unobserved -- not because nobody looked, but because HostLogger captured zero entries during srv2's SUBSEQUENT SUCCESSFUL boot too. That control turns a mute SoC into a missing recorder: the training axis is unobservable on this platform by construction, so any retry is blind in the same way until serial capture is fixed. The 2026-06-02 VRM mode did not recur, and an even 67-75 C across all eight DIMMs against a 50 C SoC rules out a skipped channel -- this was convergence failure on a populated bus. TESTS MIGRATE RATHER THAN PIN. The bound controls move to srv2, now the fleet's genuine lower-bound host; a new control asserts the measured arm carries the kernel figure and is strictly below the DIMM total; the unobserved-host control keeps its arm on a constructed input after srv4 vacated that state, because a guard going quiet is not a guard dying. Verified: gunbc compile over an entry pulling every changed module into the closure -- 0 blocking errors, 243 advisories, unchanged from baseline. Co-Authored-By: Claude Opus 5 (1M context) --- dag/extdeps/memory/cisco_ucs.dag | 60 +++++++++ dag/extdeps/memory/samsung.dag | 44 ++++++- dag/extdeps/memory/sk_hynix.dag | 4 +- dag/extdeps/memory/training.dag | 7 + dag/extdeps/memory/types.dag | 53 ++++++++ dag/extdeps/vendor/cisco.dag | 30 +++++ dag/gunbc/ci_floor_measurement.dag | 40 +++++- dag/gunbc/ci_runner_placement.dag | 2 +- dag/gunbc/fleet_intent.dag | 48 +++---- dag/gunbc/fleet_physical_inventory.dag | 15 ++- dag/gunbc/host_memory_qualification.dag | 124 +++++++++++++++++- .../claim/build_fulfillment_witness_test.dag | 2 + .../fleet_intent_memory_witness_test.dag | 71 ++++++---- .../host_allocation_conservation_test.dag | 27 +++- ...host_memory_qualification_witness_test.dag | 3 + .../installed_bom_reconcile_witness_test.dag | 73 ++++++++--- .../jedec_ddr_generation_witness_test.dag | 2 + .../memory_provisioning_witness_test.dag | 3 + .../node_power_envelope_witness_test.dag | 5 + .../samsung_dram_module_witness_test.dag | 1 + 20 files changed, 526 insertions(+), 88 deletions(-) create mode 100644 dag/extdeps/memory/cisco_ucs.dag create mode 100644 dag/extdeps/vendor/cisco.dag diff --git a/dag/extdeps/memory/cisco_ucs.dag b/dag/extdeps/memory/cisco_ucs.dag new file mode 100644 index 00000000000..a837a5a1e60 --- /dev/null +++ b/dag/extdeps/memory/cisco_ucs.dag @@ -0,0 +1,60 @@ +module extdeps.memory.cisco_ucs + +import std.decl_ref { DeclarationRef, WholeDeclaration } +import extdeps.memory.types { OemModuleOffering, OemModuleLinkEvidence, OemLinkPhysicalLabelObserved } +import extdeps.memory.samsung { m393a8g40d40_crb0q_catalog } +import extdeps.vendor.cisco { cisco } +import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef } +import extdeps.uri { Uri, Https } + +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "www.cisco.com/c/en/us/products/servers-unified-computing/ucs-c-series-rack-servers/datasheet-listing.html" + } +} + +data extdeps_model_scope: ExternalModelScope = ExternalModelScope { + subject: ExternalSubjectRef { + declaration: DeclarationRef { + module_path: "extdeps.memory.cisco_ucs", + decl_name: "ucs_mr_1x648ru_a", + field: WholeDeclaration + } + }, + first_citation: extdeps_external_authority_anchor, + further_citations: [] +} + +// WHY THIS MODULE EXISTS SEPARATELY FROM extdeps.memory.samsung (DESIGN 3). +// Cisco resells a Samsung module under its own PID and part number, with its own lifecycle and +// its own published description. That is a second independently governed entity inhabiting the +// same shape, not a second name for the Samsung row -- so it gets its own module authority and +// REFERENCES the module rather than restating its organization axes. A second OEM reselling the +// same part would be another row here and no edit to Samsung at all. +// +// CITATION STANDING, STATED HONESTLY BECAUSE IT IS WEAKER THAN THE ANCHOR SUGGESTS. +// The anchor above is Cisco's C-Series datasheet index, not a document carrying this PID. The +// per-PID spec sheets under cisco.com/c/dam refuse automated retrieval (HTTP 403, checked +// 2026-08-22), and the M4-era memory guide that would carry a 2133 TSV-RDIMM was not reachable. +// What established the description below was agreement across independent distributor listings +// -- 64 GB, DDR4-2133 / PC4-17000, TSV-RDIMM, octal rank, x4, 1.2 V, CL15 -- corroborated by the +// operator's physical label. That is a real basis and it is NOT a first-party reading, which is +// exactly the distinction OemModuleLinkEvidence's two arms exist to keep visible. +// Dissolve-on: a reachable Cisco memory guide or spec sheet listing this PID, at which point the +// anchor names that document and this paragraph shrinks to a citation. +// +// WHAT THE LABEL SETTLED THAT NOTHING ELSE COULD. The label reads +// "M393A8G40D40-CRB0Q S", which is what links this Cisco PID to that specific Samsung part +// number -- no reachable Cisco document names the underlying manufacturer part at all. The link +// is therefore an observation of the part in hand, recorded as such. +data ucs_mr_1x648ru_a: OemModuleOffering = OemModuleOffering { + oem: cisco, + oem_product_id: "UCS-MR-1X648RU-A", + oem_part_number: "15-102952-01", + underlying_module: m393a8g40d40_crb0q_catalog, + link_evidence: OemLinkPhysicalLabelObserved { + label_text: "M393A8G40D40-CRB0Q S", + observer: "operator, physical label on the module in hand, 2026-08-22", + }, +} diff --git a/dag/extdeps/memory/samsung.dag b/dag/extdeps/memory/samsung.dag index 7f9cb900218..0f948ff3b4a 100644 --- a/dag/extdeps/memory/samsung.dag +++ b/dag/extdeps/memory/samsung.dag @@ -1,7 +1,7 @@ module extdeps.memory.samsung import std.measure { ByteSize, byte_size, bit_width } -import extdeps.memory.types { DramModuleCatalogRow, DimmBuffering, dram_generation_ddr4 } +import extdeps.memory.types { DramModuleCatalogRow, DimmBuffering, dram_generation_ddr4, MonolithicDie, ThreeDimensionalStacked } import extdeps.vendor.samsung { samsung } import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef } import std.decl_ref { DeclarationRef, WholeDeclaration } @@ -59,7 +59,49 @@ data m386a4g40dm0_cpb_catalog: DramModuleCatalogRow = DramModuleCatalogRow { data_rate_mts: 2133, ecc: true, buffering: LoadReduced, + die_stacking: MonolithicDie, chip_width: bit_width(4), rank_count: 4, } + +data stick_capacity_bytes_64g: ByteSize = byte_size(68719476736) + +// PROVENANCE, AND IT IS THE SAME STANDING AS THE ROW ABOVE RATHER THAN A STRONGER ONE. +// No first-party Samsung datasheet for M393A8G40D40-CRB0Q was reachable (checked 2026-08-22): +// the per-part paths under semiconductor.samsung.com serve a generic DDR overview, as they do +// for the EOL SKU above. What IS reachable is the Cisco OEM offering that resells this module +// (extdeps.memory.cisco_ucs), whose published description carries capacity, data rate, module +// type, rank organization, chip width and voltage. Those third-party distributor listings agree +// with each other and with the operator's physical label; none of them is Samsung. +// +// So this row's figures are the OEM description plus the label, NOT a manufacturer datasheet +// reading, and the module anchor cites DDR4 only. Dissolve-on: a Samsung product-selection guide +// or module datasheet carrying this part, at which point these become cited facts. +// +// THE ORGANIZATION AXES ARE THE POINT OF THIS ROW AND THEY DISAGREE WITH ONE OBSERVATION. +// Cisco describes the offering as OCTAL RANK, x4, 3DS/TSV. The BMCs on srv3 and srv4 report +// RankCount=2 for the installed modules. These are NOT competing answers to one field: a 3DS +// module presents stacked dies behind one package load, and a management controller reporting +// what the memory subsystem enumerates is a per-host observation, not a property of the part. +// rank_count here carries the module's LOGICAL rank organization, which is what both consumers +// of this field need -- see the field's own note in extdeps.memory.types. The Redfish figure +// lives with the host observation that produced it and is not authored back into this row. +// +// COROLLARY THE REALIZABILITY CHECK CANNOT CATCH, stated so nobody reads a green as proof: +// dram_module_required_die_density passes at BOTH 8 (4 Gbit/die) and 2 (16 Gbit/die, exactly +// the DDR4 monolithic ceiling), so a wrong rank_count here lands silently. The value is settled +// by the OEM description, not by the wall. +data m393a8g40d40_crb0q_catalog: DramModuleCatalogRow = DramModuleCatalogRow { + part_number: "M393A8G40D40-CRB0Q", + manufacturer: samsung, + generation: dram_generation_ddr4, + capacity_bytes: stick_capacity_bytes_64g, + data_rate_mts: 2133, + ecc: true, + buffering: Registered, + die_stacking: ThreeDimensionalStacked, + chip_width: bit_width(4), + + rank_count: 8, +} diff --git a/dag/extdeps/memory/sk_hynix.dag b/dag/extdeps/memory/sk_hynix.dag index 55dc032fe83..c3ce6b436a2 100644 --- a/dag/extdeps/memory/sk_hynix.dag +++ b/dag/extdeps/memory/sk_hynix.dag @@ -1,7 +1,7 @@ module extdeps.memory.sk_hynix import std.measure { ByteSize, byte_size, bit_width } -import extdeps.memory.types { DramModuleCatalogRow, DimmBuffering, dram_generation_ddr4 } +import extdeps.memory.types { DramModuleCatalogRow, DimmBuffering, dram_generation_ddr4, MonolithicDie } import extdeps.vendor.sk_hynix { sk_hynix } import extdeps.external_authority { ExternalAuthority } import extdeps.uri { Uri, Https } @@ -23,6 +23,7 @@ data hma82gr7afr4n_vk_catalog: DramModuleCatalogRow = DramModuleCatalogRow { data_rate_mts: 2666, ecc: true, buffering: Registered, + die_stacking: MonolithicDie, chip_width: bit_width(4), rank_count: 1, @@ -36,6 +37,7 @@ data hma82gr7afr8n_vk_catalog: DramModuleCatalogRow = DramModuleCatalogRow { data_rate_mts: 2666, ecc: true, buffering: Registered, + die_stacking: MonolithicDie, chip_width: bit_width(8), rank_count: 2, diff --git a/dag/extdeps/memory/training.dag b/dag/extdeps/memory/training.dag index 76f12126638..c1be0a87e98 100644 --- a/dag/extdeps/memory/training.dag +++ b/dag/extdeps/memory/training.dag @@ -11,6 +11,7 @@ import extdeps.memory.types { DramModuleCatalogRow, JedecDdrGenerationCatalogRow, LoadReduced, + MonolithicDie, Registered, Unbuffered, dram_data_chips_per_rank, @@ -118,6 +119,11 @@ fn module_executes_step(module: DramModuleCatalogRow, step: MemoryTrainingStep) // load-reduced ones. The buyer's intuition that a lower speed grade is simply // a discount is therefore wrong at capacities near the density ceiling: the // older part is not the same module clocked slower, it is a different topology. +// MonolithicDie in the constructed row below is load-bearing, not a default carried over from +// the input. This builds the COUNTERFACTUAL plain module -- the one that would exist if the +// capacity were reachable without the two escapes the comment above names, extra ranks and +// stacking. Propagating module.die_stacking would ask "is this capacity reachable given that it +// is already stacked", which is trivially yes and answers nothing. fn hypothetical_module_at_rank_count( module: DramModuleCatalogRow, rank_count: Int, @@ -130,6 +136,7 @@ fn hypothetical_module_at_rank_count( data_rate_mts: module.data_rate_mts, ecc: module.ecc, buffering: Registered, + die_stacking: MonolithicDie, chip_width: module.chip_width, rank_count: rank_count, } diff --git a/dag/extdeps/memory/types.dag b/dag/extdeps/memory/types.dag index 2d683867812..1f256232800 100644 --- a/dag/extdeps/memory/types.dag +++ b/dag/extdeps/memory/types.dag @@ -98,6 +98,29 @@ fn dram_module_class_eq(a: DramModuleClass, b: DramModuleClass) -> Bool { }) } +// WHY die_stacking IS A REQUIRED FIELD ON THE ROW AND NOT AN OPTION (2026-08-22). +// DramDieStacking already existed as an axis, declared above for the controller-admission +// question, but the catalog row could not say which value a module carried -- so a 3DS RDIMM +// and a monolithic RDIMM were indistinguishable in the only carrier a consumer reads. That is +// the fused-axis defect the DramModuleClass comment above repairs for the CONTROLLER, left +// standing in the MODULE. The two must agree or the admission check answers about a class no +// row can claim membership in. +// +// It is required rather than optional because the state it excludes is exactly the one that +// caused this: a stacked module authored by someone who did not know the axis existed, landing +// as a monolithic-looking row that the Altra admission check then grades against the wrong +// class. An Option would have made forgetting it representable and re-opened that door +// (DESIGN 5 -- prefer the shape in which the bad state cannot be written). +// +// rank_count STAYS ONE FIELD, and that is a deliberate finding rather than an omission. Both +// of its consumers are correct for a stacked part when it carries the module's LOGICAL rank +// organization: dram_module_required_die_density divides capacity by (data chips x ranks) to +// get PER-DIE density, which is the figure JEDEC's monolithic ceiling actually bounds, and +// devices_per_stick multiplies chips-per-rank by ranks to get a DIE count, which is what a +// stacked package contains. Neither wanted a package count. A management controller's own +// reported rank number is a DIFFERENT fact -- an observation of one host's slot, not a +// property of the part -- and belongs in the observing layer, never authored back here +// (DESIGN 3, external upstream decomposition). type DramModuleCatalogRow { part_number: NonEmptyStr manufacturer: Vendor @@ -109,6 +132,7 @@ type DramModuleCatalogRow { ecc: Bool buffering: DimmBuffering + die_stacking: DramDieStacking chip_width: BitWidth @@ -138,6 +162,35 @@ fn dram_module_is_realizable(module: DramModuleCatalogRow, jedec: JedecDdrGenera } } +// --- OEM RESALE IDENTITY ------------------------------------------------------------------------- +// +// AN OEM OFFERING AND THE MODULE INSIDE IT ARE TWO INDEPENDENTLY GOVERNED FACTS (DESIGN 3, +// external upstream decomposition). Cisco assigns a PID and a Cisco part number, publishes its +// own specification, and controls that offering's lifecycle; Samsung manufactures a module with +// its own part number and its own organization. Flattening them into one catalog row -- an +// "OEM part_number" field, or a Cisco row duplicating the Samsung organization axes -- makes one +// authority answer for the other, and the duplicate drifts the moment either side revises. +// +// So the offering REFERENCES the module rather than restating it. Adding a second OEM that +// resells the same Samsung part is then a new offering row and no edit at all to the module. +type OemModuleOffering { + oem: Vendor + oem_product_id: NonEmptyStr + oem_part_number: NonEmptyStr + underlying_module: DramModuleCatalogRow + link_evidence: OemModuleLinkEvidence +} + +// HOW WE KNOW THE OFFERING CONTAINS THAT MODULE, and the arms are not interchangeable. +// A supplier document is an upstream claim we can cite and re-read. A physical label read off +// the part in hand is an OBSERVATION this repository produced -- a receipt in the observing +// layer, admissible and often the only thing available for an EOL SKU, but never citable as +// though the OEM had documented it. Recording which one we have is the difference between a +// grounded row and one that merely looks grounded (DESIGN 4b, rung honesty). +type OemModuleLinkEvidence + = OemLinkDocumentedBySupplier { citation: ExternalAuthority } + | OemLinkPhysicalLabelObserved { label_text: NonEmptyStr, observer: NonEmptyStr } + type MemoryPopulationRow { module: DramModuleCatalogRow stick_count: Int diff --git a/dag/extdeps/vendor/cisco.dag b/dag/extdeps/vendor/cisco.dag new file mode 100644 index 00000000000..d91edd1d765 --- /dev/null +++ b/dag/extdeps/vendor/cisco.dag @@ -0,0 +1,30 @@ +module extdeps.vendor.cisco + +import std.decl_ref { DeclarationRef, WholeDeclaration } +import extdeps.vendor { Vendor } +import extdeps.hardware { Hardware } + +import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef } +import extdeps.uri { Uri, Https } + +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "en.wikipedia.org/wiki/Cisco" + } +} + +data extdeps_model_scope: ExternalModelScope = ExternalModelScope { + subject: ExternalSubjectRef { + declaration: DeclarationRef { + module_path: "extdeps.vendor.cisco", + decl_name: "cisco", + field: WholeDeclaration + } + }, + first_citation: extdeps_external_authority_anchor, + further_citations: [] +} + + +data cisco: Vendor = Vendor { legal_name: "Cisco Systems, Inc." } diff --git a/dag/gunbc/ci_floor_measurement.dag b/dag/gunbc/ci_floor_measurement.dag index 918447c3d12..fa0c1382f82 100644 --- a/dag/gunbc/ci_floor_measurement.dag +++ b/dag/gunbc/ci_floor_measurement.dag @@ -284,11 +284,11 @@ type HostUsableRam | HostUsableRamConservativeLowerBound { bytes: ByteSize, basis: NonEmptyStr } | HostUsableRamUnmeasured -data gunbc_ci_host_usable_ram_kind_note: String = "OS-USABLE RAM IS A PER-HOST FACT AND WAS STORED AS A FLEET CONSTANT, which is the same grain defect gunbc_ci_host_fixed_overhead_kind_note repaired for overhead — so this carrier is deliberately that carrier's shape rather than a new invention.\n\nCORRECTION, AND IT IS THE POINT OF THIS PARAGRAPH. An earlier revision of this note said a 2026-08-11 DIMM replacement had raised memory on part of the fleet, that gunbc.ci_runner_placement host_usable_ram_note's trigger had therefore fired, and that the four hosts no longer shared one usable-RAM figure. THE REPLACEMENT WAS ATTEMPTED AND DID NOT WORK (operator, 2026-08-12). srv3 and srv4 retain their original 8 x 16 GiB population, no host's memory changed, and that trigger has NOT fired. The claim was written from an in-flight operator report before any observation existed to confirm it, and it was wrong — which is exactly the failure this carrier's own arms are built to make visible, landing in the prose instead of the data.\n\nWHAT THE GRAIN RESTS ON INSTEAD, none of it contingent on any DIMM moving: placement folded over per-host offers while reading RAM from gunbc.ci_fleet gunbc_ci_host, a synthetic machine on a Q64-30 that is not a member of that fold; two sibling budget trees checked nominal DIMM capacity while placement checked OS-usable, so both could report conservation green against different ceilings; and an unclassified host silently borrowed a figure rather than refusing. Those were defects on the day they were written and remain so with the population unchanged. A per-host fact belongs at per-host grain whether or not the hosts currently differ — the fleet-wide shape was wrong because it could not EXPRESS a difference, not because one had appeared.\n\nTHREE ARMS BECAUSE THERE ARE THREE FACTS. MEASURED means a read of THIS host produced the number and the row names the read. CONSERVATIVE LOWER BOUND means no such read exists and the carried figure is known not to exceed the host's real usable RAM, with basis stating why. UNMEASURED is the fail-closed floor for a host nobody classified.\n\nTHE MIDDLE ARM IS A BOUND AND NOT A SUBSTITUTION, and this survives the correction above rather than depending on it. The four hosts do share a board and a population today, so an equivalence argument is available — but equivalence IMPLIES the bound, so the bound is the weaker and safer claim, and it is the one the conservation wall actually needs. Naming the arm for equivalence would license the move the wall cannot survive: carrying a reading from a host with MORE memory onto one with less. Nothing in a substitution-shaped type forbids that; the bound's name does. The safety property is monotonicity, and it should not have to be re-argued every time the fleet's uniformity changes.\n\nWHY ALL FOUR ARE BOUNDS AND NONE IS MEASURED: no MemTotal read exists for any host in this fleet. The closest receipt is gunbc_ci_srv3_memavailable_high_water, whose host_total is MemTotal-shaped but was captured as an arm-time line from a memory governor rather than a read taken to answer this question, and only on srv3.\n\nDissolving these is CHEAPER THAN THE FIXED-OVERHEAD ROW BESIDE THEM and must not be confused with it. That row needs a QUIESCENT read because it estimates non-reclaimable residency from MemAvailable, which moves with load. MemTotal does not: the kernel reports total usable RAM after firmware and kernel reservations, so an ordinary read while the host serves work is a complete answer. One read per host, taken any time, promotes that host's row to MEASURED and leaves the others untouched — which is the entire point of the grain." +data gunbc_ci_host_usable_ram_kind_note: String = "OS-USABLE RAM IS A PER-HOST FACT AND WAS STORED AS A FLEET CONSTANT, which is the same grain defect gunbc_ci_host_fixed_overhead_kind_note repaired for overhead -- so this carrier is deliberately that carrier's shape rather than a new invention.\n\nTHE DIMM-REPLACEMENT CLAIM HAS NOW BEEN WRONG IN BOTH DIRECTIONS AND IS SETTLED BY MEASUREMENT. An earlier revision said a 2026-08-11 replacement had raised memory on part of the fleet; that was written from an in-flight operator report before any observation existed, and it was wrong (the attempt failed, operator 2026-08-12). This revision records the opposite and does so from a read rather than a report: srv3 and srv4 were each observed at 512 GiB over BMC Redfish on 2026-08-22 -- 8 x Samsung M393A8G40D40-CRB at 64 GiB, one per channel, all Enabled/OK -- while srv1 and srv2 remain at 8 x 16 GiB Hynix pending their own upgrades. The hosts no longer share one nominal population.\n\nTHE ARMS BELOW DO NOT MOVE, AND THAT IS THE POINT RATHER THAN AN OVERSIGHT. What changed is NOMINAL DIMM capacity, which this carrier does not hold and must never be fed. Every host still carries HostUsableRamConservativeLowerBound at 125 GiB, because no MemTotal read exists for any of them -- including the two just upgraded. A lower bound does not become false when the machine gets bigger; it becomes LOOSE. So the wall stays sound and starts badly under-admitting on two hosts, and the remedy is the one this note already named: one ordinary read per host, taken any time, promoting that host's row to MEASURED and leaving the others untouched.\n\nTHREE ARMS BECAUSE THERE ARE THREE FACTS. MEASURED means a read of THIS host produced the number and the row names the read. CONSERVATIVE LOWER BOUND means no such read exists and the carried figure is known not to exceed the host's real usable RAM, with basis stating why. UNMEASURED is the fail-closed floor for a host nobody classified.\n\nTHE MIDDLE ARM IS A BOUND AND NOT A SUBSTITUTION, and the heterogeneity above is exactly why that distinction was worth paying for in advance. While the fleet was uniform an equivalence argument was also available, and naming the arm for equivalence would have licensed the move the wall cannot survive: carrying a reading from a host with MORE memory onto one with less. That move is now AUTHORABLE for the first time -- srv3 and srv4 are the hosts with more -- and the bound's name is what forbids it. The safety property is monotonicity, and it did not have to be re-argued when the fleet's uniformity ended.\n\nWHY ALL FOUR ARE BOUNDS AND NONE IS MEASURED: no MemTotal read exists for any host in this fleet. The closest receipt is gunbc_ci_srv3_memavailable_high_water, whose host_total is MemTotal-shaped but was captured as an arm-time line from a memory governor rather than a read taken to answer this question, only on srv3, and -- now load-bearing -- against srv3's PREVIOUS 128 GiB population, so it is a receipt about hardware that is no longer in that chassis.\n\nDissolving these is CHEAPER THAN THE FIXED-OVERHEAD ROW BESIDE THEM and must not be confused with it. That row needs a QUIESCENT read because it estimates non-reclaimable residency from MemAvailable, which moves with load. MemTotal does not: the kernel reports total usable RAM after firmware and kernel reservations, so an ordinary read while the host serves work is a complete answer. One read per host, taken any time, promotes that host's row to MEASURED and leaves the others untouched -- which is the entire point of the grain." data gunbc_ci_conservative_lower_bound_usable_ram: HostUsableRam = HostUsableRamConservativeLowerBound { bytes: gunbc_ci_srv3_memavailable_high_water.host_total, - basis: "Consumed from gunbc_ci_srv3_memavailable_high_water.host_total — the MemTotal-shaped figure captured on srv3 on 2026-07-16 (run 29537878075) — rather than re-minted here, because that observation and gunbc.ci_fleet gunbc_ci_host.memory already carried this number and a third independently editable copy is the fork DESIGN 2 forbids. It is a LOWER BOUND and not any host's measurement: it was captured on ONE host, as an arm-time memory-governor line rather than a read taken to answer this question, and the other three never had their own. All four hosts do carry the same board and the same 8 x 16 GiB population today — the 2026-08-11 replacement was attempted and did not work — so equivalence would also justify the figure; the bound is carried instead because it is the weaker claim and stays true if that uniformity ever ends. It licenses nothing in the other direction: a reading from a host with MORE memory is not admissible here. Every enrolled host carries it unchanged, and each is replaced independently by that host's own MemTotal read." + basis: "Consumed from gunbc_ci_srv3_memavailable_high_water.host_total — the MemTotal-shaped figure captured on srv3 on 2026-07-16 (run 29537878075) — rather than re-minted here, because that observation and gunbc.ci_fleet gunbc_ci_host.memory already carried this number and a third independently editable copy is the fork DESIGN 2 forbids. It is a LOWER BOUND and not any host's measurement: it was captured on ONE host, as an arm-time memory-governor line rather than a read taken to answer this question, and the other three never had their own. That uniformity HAS NOW ENDED: srv3 and srv4 were observed at 8 x 64 GiB (512 GiB) on 2026-08-22 while srv1 and srv2 remain at 8 x 16 GiB, so the equivalence argument that would once have justified this figure is gone and only the bound survives — which is precisely the contingency it was carried for. It stays true on all four hosts because a lower bound does not break when a machine grows, only loosens. It licenses nothing in the other direction: a reading from a host with MORE memory is not admissible here. Every enrolled host carries it unchanged, and each is replaced independently by that host's own MemTotal read." } data gunbc_ci_host_usable_ram_disposition_note: String = "REGISTERED AS SCAFFOLD DEBT BECAUSE ITS TWIN IS, and because the debt is PRE-EXISTING rather than introduced here: the fleet-wide constant this carrier replaces was already an unmeasured stand-in, and modeling it is what makes it countable. DESIGN 5 refuses NEW dissolution obligations without an operator verdict; it separately exists so that documenting previously hidden debt never reads as creating it, which is this row.\n\nTHE BIND TARGET IS DELIBERATELY NOT THE OVERHEAD ROW'S. gunbc_ci_managed_host_fixed_overhead_disposition binds a QUIESCENT read, because overhead is estimated from MemAvailable and MemAvailable moves with load. MemTotal does not — the kernel reports total usable RAM after firmware and kernel reservations — so an ordinary read taken while the host serves work discharges this and not that. Two obligations, two observations, two independently removable units, which is the grain DESIGN 5 requires: sharing one trigger is admissible only when neither artifact can survive the other, and these plainly can." @@ -302,15 +302,47 @@ data gunbc_ci_host_usable_ram_disposition: Disposition = Scaffold { } } +// THE FIRST MemTotal READS THIS FLEET HAS EVER CARRIED (2026-08-22), which retires the +// conservative lower bound on two hosts and leaves it standing on the other two. +// +// Taken over SSH on the hosts themselves -- /proc/meminfo MemTotal, the figure the kernel +// reports after firmware and kernel reservations -- which is exactly the read +// gunbc_ci_host_usable_ram_kind_note names as sufficient: MemTotal does not move with load, so +// an ordinary read while the host serves work is a complete answer and no quiescence is needed. +// +// THE NOMINAL-VERSUS-USABLE GAP IS NOW MEASURED RATHER THAN ASSERTED, and it is larger than the +// old population's. Both hosts carry 512 GiB of nominal DIMM capacity and the kernel reports +// 502.25 GiB usable -- a 9.75 GiB firmware and kernel reservation. Writing the Redfish 512 GiB +// figure into this carrier would therefore have overstated the budget's ceiling by nearly ten +// gibibytes on each host, which is the error this carrier's whole existence is meant to prevent +// and which was one edit away the moment the BMC reported a bigger number. +data gunbc_ci_srv3_memtotal_measured: HostUsableRam = HostUsableRamMeasured { + bytes: byte_size(539282522112), + provenance: "srv3 /proc/meminfo MemTotal = 526643088 kB, read over SSH 2026-08-22 while the host was serving (5 actions-runner units active, uptime 2h21m, kernel 6.8.0-138-generic), against the 8 x 64 GiB Samsung population installed the same day", +} + +data gunbc_ci_srv4_memtotal_measured: HostUsableRam = HostUsableRamMeasured { + bytes: byte_size(539282526208), + provenance: "srv4 /proc/meminfo MemTotal = 526643092 kB, read over SSH 2026-08-22 while the host was serving (5 actions-runner units active, uptime 2h52m, kernel 6.8.0-138-generic), against the 8 x 64 GiB Samsung population installed the same day", +} + +// srv1 AND srv2 KEEP THE BOUND, FOR TWO DIFFERENT REASONS, and collapsing them would lose one. +// srv1 WAS upgraded and is reported at 502 GB by the operator, but this lane holds no read of it +// -- its host refuses the fleet-automation key and no BMC credential for it exists in Secret +// Manager -- so promoting it here on a relayed figure would be exactly the borrowed premise the +// unknown-host arm refuses. srv2's 64 GiB upgrade FAILED and was reverted the same day, so it +// genuinely still carries 8 x 16 GiB and the 125 GiB bound is very nearly its real figure. +// Same arm, same value, opposite reasons: one is unmeasured-and-bigger, the other is +// unmeasured-and-accurate. fn gunbc_ci_host_usable_ram_for(host: HostIdentity) -> HostUsableRam { if (host as String) == (operator_host_srv1 as String) { gunbc_ci_conservative_lower_bound_usable_ram } else if (host as String) == (operator_host_srv2 as String) { gunbc_ci_conservative_lower_bound_usable_ram } else if (host as String) == (operator_host_srv3 as String) { - gunbc_ci_conservative_lower_bound_usable_ram + gunbc_ci_srv3_memtotal_measured } else if (host as String) == (operator_host_srv4 as String) { - gunbc_ci_conservative_lower_bound_usable_ram + gunbc_ci_srv4_memtotal_measured } else { HostUsableRamUnmeasured } diff --git a/dag/gunbc/ci_runner_placement.dag b/dag/gunbc/ci_runner_placement.dag index f37c28c0b32..92716a07854 100644 --- a/dag/gunbc/ci_runner_placement.dag +++ b/dag/gunbc/ci_runner_placement.dag @@ -265,7 +265,7 @@ fn host_session_slice_bytes(host: HostIdentity) -> ByteSize { } } -data host_usable_ram_note: String = "CONSERVATION IS CHECKED AGAINST OS-USABLE RAM, NOT THE DIMM TOTAL. compute_host_ram_bytes_total sums the populated modules — nominal capacity — while the OS sees less after firmware and kernel reservations, and gunbc.ci_fleet fleet_host_memory_nominal_vs_usable_note exists specifically to say these are two facts that must not be conflated. The margin decides admissions rather than being academic: at this fleet's 128 GiB nominal / 125 GiB usable population, an eighth 14 GiB slot sums to 125.6 GiB, which PASSES against nominal and FAILS against usable — so checking the nominal figure would admit a width the machine cannot carry, by spending memory that does not exist. The seventh slot fits under both readings; the eighth is exactly where the conflation bites.\n\nTHIS NOTE WAS BRIEFLY REWRITTEN AS HISTORY AND IS RESTORED, which is worth recording because the rewrite was the error. Its closing premise — every host on the same board at the same population, so one figure stands in for all four, until a differently populated host enrols — was declared FALSIFIED on an in-flight report that a DIMM replacement had landed. The replacement was attempted and did not work (operator, 2026-08-12); srv3 and srv4 retain their original population and the premise never stopped holding. Marking a true statement historical is the same defect as leaving a false one live: both leave a reader unable to tell which of two adjacent notes to believe.\n\nWHAT THE PER-HOST GRAIN RESTS ON is therefore not this trigger. It is that this wall folded over per-host offers and then read RAM from a synthetic machine outside that fold, and that an unclassified host borrowed rather than refused — see gunbc.ci_floor_measurement gunbc_ci_host_usable_ram_kind_note. The trigger below remains OPEN and unfired." +data host_usable_ram_note: String = "CONSERVATION IS CHECKED AGAINST OS-USABLE RAM, NOT THE DIMM TOTAL. compute_host_ram_bytes_total sums the populated modules -- nominal capacity -- while the OS sees less after firmware and kernel reservations, and gunbc.ci_fleet fleet_host_memory_nominal_vs_usable_note exists specifically to say these are two facts that must not be conflated. The margin decides admissions rather than being academic: at the 128 GiB nominal / 125 GiB usable population this fleet carried until 2026-08-22, an eighth 14 GiB slot summed to 125.6 GiB, which PASSED against nominal and FAILED against usable -- so checking the nominal figure would admit a width the machine cannot carry, by spending memory that does not exist.\n\nTHE UNIFORM-POPULATION PREMISE HAS NOW ACTUALLY FALSIFIED, AND THIS PARAGRAPH IS THE THIRD REVISION OF THAT CLAIM -- which is itself the finding. The premise was: every host on the same board at the same population, so one figure stands in for all four. It was declared falsified once on an in-flight report of a DIMM replacement, then RESTORED when that replacement was reported failed (operator, 2026-08-12), with a note saying that marking a true statement historical is the same defect as leaving a false one live. Both of those were correct at the time. Both are now superseded by measurement: srv3 and srv4 were each read at 512 GiB over BMC Redfish on 2026-08-22 (8 x Samsung M393A8G40D40-CRB, one per channel), while srv1 and srv2 remain at 8 x 16 GiB Hynix. The fleet is HETEROGENEOUS as of that date and the premise is dead for the first time in this note's history.\n\nWHAT THAT DOES NOT LICENSE, because it is the move this note has always existed to forbid: the 512 GiB figure is NOMINAL DIMM CAPACITY read from a management controller. It is NOT OS-usable RAM and must not be written into gunbc_ci_host_usable_ram_for. No MemTotal read exists for any host in this fleet, including the two that were just upgraded, so every host's usable-RAM row remains a conservative lower bound and the conservation wall keeps admitting the widths it admitted yesterday. That is SOUND and USELESSLY CONSERVATIVE at the same time -- 125 GiB is still a true lower bound for a 512 GiB host -- and the gap between sound and useful is closed by one ordinary /proc/meminfo read per host, not by promoting a Redfish number.\n\nWHAT THE PER-HOST GRAIN RESTS ON is therefore still not this trigger, and the heterogeneity does not retroactively justify the grain. It is that this wall folded over per-host offers and then read RAM from a synthetic machine outside that fold, and that an unclassified host borrowed rather than refused -- see gunbc.ci_floor_measurement gunbc_ci_host_usable_ram_kind_note. A per-host fact belonged at per-host grain when the hosts were identical; it merely became visible when they stopped being." // The grain here is per host, and the reason is not that the hosts differ. This wall folds over // per-host offers and charges each host its own overhead and session slice, then read RAM from a diff --git a/dag/gunbc/fleet_intent.dag b/dag/gunbc/fleet_intent.dag index 3b8c8a568e0..f85534ad259 100644 --- a/dag/gunbc/fleet_intent.dag +++ b/dag/gunbc/fleet_intent.dag @@ -15,7 +15,8 @@ import extdeps.cpu.types { CpuFacts, CpuDeploymentFacts } import extdeps.cpu { cpu_facts_threads, cpu_facts_sustained_per_thread_hz } import extdeps.boards.asrock_rack { asrock_altrad8ud_1l2t_catalog } import extdeps.memory.types { MemoryKind, Dram, HostMemoryPopulation, MemoryPopulationRow } -import extdeps.memory.sk_hynix { hma82gr7afr4n_vk_catalog, hma82gr7afr8n_vk_catalog } +import extdeps.memory.sk_hynix { hma82gr7afr4n_vk_catalog } +import extdeps.memory.samsung { m393a8g40d40_crb0q_catalog } import extdeps.memory { memory_population_row_bytes, host_memory_population_nominal_bytes } import extdeps.gpu.types { GpuFacts, AcceleratorFacts, GpuRuntime } import extdeps.toolchain.types { ToolchainCapability } @@ -35,7 +36,6 @@ import std.realization_schedule { CostAccount } import std.realization_measurement { cost_account_measured_from_time_and_space, space_measure_list_seq } import std.nat { Nat } import std.float { Float } -import std.dissolution { DissolutionCondition, unbound_dissolution } type IsolationBoundary = SharedHostHome | PerJobFilesystem | ContainerHermetic | Vm type ContainerRuntime = Docker | Podman | Gvisor | Ubicloud | GcloudRun @@ -228,13 +228,15 @@ data srv4_nvme0: StorageDevice = nvme_storage_device( persistence: Persistent, ) -data fleet_host_memory_nominal_vs_usable_note: String = "Two DISTINCT memory facts for fleet hosts, must not be conflated: (1) NOMINAL DIMM population — srv1/srv2/srv3 host memory derives from per-DIMM BMC Redfish observations through HostMemoryPopulation rows (module × stick_count), srv1/srv2/srv3 observed 2026-07-16 (deferral scaffolds retired on observation); srv4 is NOT yet observed — its 128 GiB literal carries srv4_memory_population_deferral, the same declared-deferral shape srv1/srv2 used pre-observation; (2) OS-USABLE budget — gunbc_ci_host.memory byte_size(134217728000) = exactly 125 GiB, MemTotal-shaped CI runner budget authority (roadmap 128c/125GiB; floor peak receipts from srv1/srv2). The usable figure requires its OWN OS MemTotal provenance — never a blind rewrite from 125 GiB usable to 128 GiB nominal." +data fleet_host_memory_nominal_vs_usable_note: String = "Two DISTINCT memory facts for fleet hosts, must not be conflated: (1) NOMINAL DIMM population — every host's memory derives from per-DIMM BMC Redfish observations through HostMemoryPopulation rows (module x stick_count). srv1/srv2 observed 2026-07-16 and still carry 8 x 16 GiB Hynix; srv3/srv4 observed 2026-08-22 at 8 x 64 GiB Samsung (512 GiB each), which retired srv4's deferral scaffold and superseded srv3's 7+1 mixed row. The fleet is HETEROGENEOUS as of that date. (2) OS-USABLE budget — the MemTotal-shaped CI runner budget authority, which is a SEPARATE fact with its own provenance requirement.\n\nTHE UPGRADE MAKES THE SPLIT LOAD-BEARING RATHER THAN PEDANTIC, so it is restated here in the direction the mistake would now be made. The temptation before was to write 128 GiB nominal over a 125 GiB usable figure, a 3 GiB error. The temptation NOW is to write 512 GiB over it, a 387 GiB error, on the two hosts where a conservation wall would spend it. A management controller reports what is installed; only the kernel reports what is usable after firmware and kernel reservations. No MemTotal read exists for any host in this fleet, so gunbc.ci_floor_measurement gunbc_ci_host_usable_ram_for still carries a conservative lower bound on all four — sound, and now very loose on srv3/srv4. It is dissolved by one ordinary /proc/meminfo read per host and by nothing that can be reached over Redfish." -data srv1_memory_population_observation_note: String = "srv1 BMC 192.168.1.183 Redfish observation 2026-07-16 (rotated cred, operator-supplied): MemorySummary TotalSystemMemoryGiB=128; per-DIMM dimm0..dimm7 all HMA82GR7AFR4N-VK RankCount=1 DataWidthBits=64 BusWidthBits=72 CapacityMiB=16384 OperatingSpeedMhz=2666 (×8). Uniform 8-stick population of the existing cited row hma82gr7afr4n_vk_catalog (AFR4N=x4 1R) totals 128 GiB — dissolves the gibibyte(128) placeholder." +data srv1_memory_population_observation_2026_07_16_note: String = "srv1 BMC 192.168.1.183 Redfish observation 2026-07-16 (rotated cred, operator-supplied): MemorySummary TotalSystemMemoryGiB=128; per-DIMM dimm0..dimm7 all HMA82GR7AFR4N-VK RankCount=1 DataWidthBits=64 BusWidthBits=72 CapacityMiB=16384 OperatingSpeedMhz=2666 (×8). Uniform 8-stick population of the existing cited row hma82gr7afr4n_vk_catalog (AFR4N=x4 1R) totals 128 GiB — dissolves the gibibyte(128) placeholder." + +data srv1_memory_population_observation_2026_08_22_note: String = "srv1 UPGRADED to the 64 GiB Samsung population on 2026-08-22 and POSTed cleanly on the first attempt. OPERATOR-SUPPLIED OBSERVATION, not a read this lane took: reported from the host as 8 x M393A8G40D40-CRB totalling 502 GB as dmidecode/free render it. srv1's host does not accept the fleet-automation key and its BMC credential is not in Secret Manager, so no independent confirmation was available here.\n\nATTRIBUTION IS THE POINT OF THAT SENTENCE. srv3 and srv4 carry BMC Redfish reads taken directly; this row does not, and recording the difference is what keeps a relayed figure from being cited later as though it had the same standing (DESIGN 4b, rung honesty at a declared subject grain). It is admitted because the reporting path is the operator observing their own machine, which is the same class of evidence srv1 and srv2's 2026-07-16 rows already rest on.\n\nDissolve-on: an independent read of srv1 at either grain -- a BMC Redfish Memory collection once a credential exists, or /proc/meminfo plus dmidecode over a key authorized on that host." data srv1_memory_population: HostMemoryPopulation = HostMemoryPopulation { rows: [ - MemoryPopulationRow { module: hma82gr7afr4n_vk_catalog, stick_count: 8 }, + MemoryPopulationRow { module: m393a8g40d40_crb0q_catalog, stick_count: 8 }, ], } @@ -246,12 +248,15 @@ data srv2_memory_population: HostMemoryPopulation = HostMemoryPopulation { ], } -data srv3_memory_population_observation_note: String = "srv3 BMC 192.168.1.192 Redfish observation 2026-07-16 (factory cred): MemorySummary TotalSystemMemoryGiB=128; per-DIMM dimm0 HMA82GR7AFR8N-VK RankCount=2 DataWidthBits=64 BusWidthBits=72 CapacityMiB=16384 OperatingSpeedMhz=2666 (×7); dimm7 HMA82GR7AFR4N-VK RankCount=1 DataWidthBits=64 BusWidthBits=72 CapacityMiB=16384 OperatingSpeedMhz=2666 (×1). Part-number decode: AFR8N=x8 2R → hma82gr7afr8n_vk_catalog; AFR4N=x4 1R → existing hma82gr7afr4n_vk_catalog. Mixed 7+1 population totals 128 GiB — the fact the old gibibyte(128) literal was hiding." +data srv3_memory_population_observation_2026_07_16_note: String = "srv3 BMC 192.168.1.192 Redfish observation 2026-07-16 (factory cred): MemorySummary TotalSystemMemoryGiB=128; per-DIMM dimm0 HMA82GR7AFR8N-VK RankCount=2 DataWidthBits=64 BusWidthBits=72 CapacityMiB=16384 OperatingSpeedMhz=2666 (×7); dimm7 HMA82GR7AFR4N-VK RankCount=1 DataWidthBits=64 BusWidthBits=72 CapacityMiB=16384 OperatingSpeedMhz=2666 (×1). Part-number decode: AFR8N=x8 2R → hma82gr7afr8n_vk_catalog; AFR4N=x4 1R → existing hma82gr7afr4n_vk_catalog. Mixed 7+1 population totals 128 GiB — the fact the old gibibyte(128) literal was hiding." + +data srv3_memory_population_superseded_note: String = "THE 2026-07-16 MIXED HYNIX POPULATION IS HISTORY, NOT THE CURRENT FACT, and it is kept because a superseded observation is still a true observation of its moment (DESIGN A3). It read 7 x HMA82GR7AFR8N-VK plus 1 x HMA82GR7AFR4N-VK, 128 GiB total, at 2666 MT/s. Those modules left the chassis in the 2026-08-22 replacement; the row below is what is in it now. Deleting the old reading would erase the only record of what the 7+1 mix was, which is the population every measurement taken before 2026-08-22 was taken against -- including gunbc_ci_srv3_memavailable_high_water, the receipt the managed-host overhead bound still rests on." + +data srv3_memory_population_observation_2026_08_22_note: String = "srv3 BMC 192.168.1.192 Redfish observation 2026-08-22T20:15:38Z, taken through the rotated credential in Secret Manager (bmc-srv3-admin). MemorySummary TotalSystemMemoryGiB=512; per-DIMM dimm0..dimm7 ALL M393A8G40D40-CRB CapacityMiB=65536 OperatingSpeedMhz=2133 RankCount=2 Manufacturer=Samsung, eight distinct serial numbers, banks DDR4_A1 through H1 (one per channel). Uniform 8-stick population of m393a8g40d40_crb0q_catalog totals 512 GiB.\n\nTHE READ WAS TAKEN MID-BOOT AND THAT IS WHY THE TIMESTAMP IS PRECISE. At 20:14:31 the same endpoint still reported 128 GiB and the old Hynix parts with BootProgress=None; the host had powered on at 20:13:15 after a blackout and had not completed POST. It reported SystemHardwareInitializationComplete at 20:15:05 and 512 GiB at 20:15:38. A reader who catches this endpoint before POST completes gets the PREVIOUS population with no indication it is stale, which is a live trap for exactly this kind of observation and is recorded so the next observer waits for BootProgress rather than trusting a quiet answer.\n\nOPERATING SPEED IS THE PART'S RATING, NOT A DOWNTRAIN. 2133 is what this DDR4-2133 module is specified at; the fleet moved 2666 -> 2133 by installing it. That is a real bandwidth reduction bought for 4x capacity and it is a trade the operator made deliberately, not a fault to chase.\n\nREDFISH RankCount=2 IS RECORDED HERE AND NOT IN THE CATALOG ROW. It is an observation of this host's controller enumeration; the module's logical rank organization is the OEM's fact and lives in extdeps.memory.samsung. See that row's note for why the two are not competing answers." data srv3_memory_population: HostMemoryPopulation = HostMemoryPopulation { rows: [ - MemoryPopulationRow { module: hma82gr7afr8n_vk_catalog, stick_count: 7 }, - MemoryPopulationRow { module: hma82gr7afr4n_vk_catalog, stick_count: 1 }, + MemoryPopulationRow { module: m393a8g40d40_crb0q_catalog, stick_count: 8 }, ], } @@ -282,27 +287,14 @@ data srv3_host: ComputeHost = ComputeHost { storage: [srv3_nvme0], network_interfaces: [], } -type FleetHostMemoryPopulationDeferral { - host: HostIdentity - bmc_host: NonEmptyStr - cause: NonEmptyStr - dissolution: DissolutionCondition -} -data srv4_memory_population_deferral: FleetHostMemoryPopulationDeferral = FleetHostMemoryPopulationDeferral { - host: operator_host_srv4, - bmc_host: "192.168.1.195", - cause: "per-DIMM Redfish observation not yet taken: srv4 BMC credential is rotated and stored (bmc-srv4-admin) but this session has no reach-secrets path to authenticate the read (fleet_subsumption_manual_gaps A2)", - dissolution: unbound_dissolution(description: "authenticated read of 192.168.1.195 /redfish/v1/Systems/system/Memory — cite srv4_memory_population rows against the sk_hynix catalog (decode part numbers, never assume srv1's uniform AFR4N population), replace srv4_host.memory literal with memory_devices_from_population(pop: srv4_memory_population), and retire this deferral exactly as srv1/srv2's were at their 2026-07-16 observations (fleet_host_memory_nominal_vs_usable_note governs the usable-vs-nominal split)"), -} -data srv4_memory_population_deferral_disposition: Disposition = Scaffold { - dissolves_to: SingleAuthority, - bind: DeclarationRef { - module_path: "gunbc.fleet_intent", - decl_name: "srv4_memory_population", - field: WholeDeclaration, - }, +data srv4_memory_population_observation_note: String = "srv4 BMC 192.168.1.195 Redfish observation 2026-08-22T19:5xZ, taken through the rotated credential in Secret Manager (bmc-srv4-admin) -- the authenticated read this host's deferral named as its dissolution condition, so that scaffold is RETIRED by this row rather than carried forward. MemorySummary TotalSystemMemoryGiB=512; per-DIMM dimm0..dimm7 ALL M393A8G40D40-CRB CapacityMiB=65536 OperatingSpeedMhz=2133 RankCount=2 Manufacturer=Samsung, eight distinct serials, banks DDR4_A1 through H1, every module State=Enabled Health=OK and system HealthRollup=OK.\n\nTHE DEFERRAL'S OWN INSTRUCTION SAID TO DECODE AGAINST THE SK HYNIX CATALOG AND THAT INSTRUCTION IS SUPERSEDED, which is worth saying because following it literally would have produced a wrong row. It was written when the expected finding was srv1's uniform Hynix population; what is actually installed is a Samsung part that had no catalog row at all until 2026-08-22. The deferral was right that srv1's population must not be assumed, and wrong about which catalog the answer would come from.\n\nONE CORRECTABLE ECC EVENT IS ON RECORD FOR THIS POPULATION, logged 2026-08-22T19:45:57Z on Socket 0 / Channel 0 / DIMM 0 (bank 13, row 166, column 96), about three minutes after an unclean restart following a power blackout. It was corrected by ECC and no uncorrectable event accompanied it. It is recorded here rather than left in the BMC log because it is the only memory event this population has produced and because a repeat at the same bank/row/column would distinguish a marginal device from a single upset -- see gunbc.host_memory_qualification for the qualification standing this does not by itself change." + +data srv4_memory_population: HostMemoryPopulation = HostMemoryPopulation { + rows: [ + MemoryPopulationRow { module: m393a8g40d40_crb0q_catalog, stick_count: 8 }, + ], } data srv4_host: ComputeHost = ComputeHost { @@ -310,7 +302,7 @@ data srv4_host: ComputeHost = ComputeHost { baseboard: Present { value: srv4_baseboard }, bmc_intent: Present { value: fleet_bmc_valid_state }, processors: [CpuProcessor { cpu: fleet_intent_cpu }], - memory: [MemoryDevice { capacity: gibibyte_to_byte_size(g: gibibyte(128)), memory_kind: Dram, bandwidth: none }], + memory: memory_devices_from_population(pop: srv4_memory_population), storage: [srv4_nvme0], network_interfaces: [], } diff --git a/dag/gunbc/fleet_physical_inventory.dag b/dag/gunbc/fleet_physical_inventory.dag index 465d7178f0f..33a1bd55a1d 100644 --- a/dag/gunbc/fleet_physical_inventory.dag +++ b/dag/gunbc/fleet_physical_inventory.dag @@ -36,7 +36,7 @@ import gunbc.fleet_intent_network { operator_host_srv5, operator_host_srv6, } -import gunbc.fleet_intent { srv3_baseboard, srv4_baseboard } +import gunbc.fleet_intent { srv3_baseboard, srv4_baseboard, srv4_memory_population } import product.cooling_qualification { InstalledCoolingRealization } import std.nat { Nat } import product.inventory { @@ -57,6 +57,7 @@ import gunbc.fleet_intent { srv3_memory_population, } import extdeps.memory.sk_hynix { hma82gr7afr4n_vk_catalog } +import extdeps.memory.samsung { m393a8g40d40_crb0q_catalog } import product.installed_bom_reconcile { DimmObservationAbsent, DimmPopulationObserved, @@ -315,8 +316,8 @@ fn fleet_nominal_rackmount_arithmetic_holds() -> Bool { data fleet_dimm_expectations: List = [ HostDimmExpectation { host: operator_host_srv1, catalog: hma82gr7afr4n_vk_catalog, stick_count: 8 }, HostDimmExpectation { host: operator_host_srv2, catalog: hma82gr7afr4n_vk_catalog, stick_count: 8 }, - HostDimmExpectation { host: operator_host_srv3, catalog: hma82gr7afr4n_vk_catalog, stick_count: 8 }, - HostDimmExpectation { host: operator_host_srv4, catalog: hma82gr7afr4n_vk_catalog, stick_count: 8 }, + HostDimmExpectation { host: operator_host_srv3, catalog: m393a8g40d40_crb0q_catalog, stick_count: 8 }, + HostDimmExpectation { host: operator_host_srv4, catalog: m393a8g40d40_crb0q_catalog, stick_count: 8 }, ] data srv1_dimm_observation: HostDimmObservation = DimmPopulationObserved { @@ -334,9 +335,9 @@ data srv3_dimm_observation: HostDimmObservation = DimmPopulationObserved { rows: srv3_memory_population.rows, } -data srv4_dimm_observation: HostDimmObservation = DimmObservationAbsent { +data srv4_dimm_observation: HostDimmObservation = DimmPopulationObserved { host: operator_host_srv4, - cause: "no per-DIMM read of srv4 exists at either grain: the BMC Redfish read of 192.168.1.195 was never authenticated (gunbc.fleet_intent srv4_memory_population_deferral) and no dmidecode receipt has been supplied", + rows: srv4_memory_population.rows, } data fleet_dimm_verdicts: List = [ @@ -349,11 +350,11 @@ data fleet_dimm_verdicts: List = [ observation: srv2_dimm_observation, ), dimm_reconcile_verdict( - expectation: HostDimmExpectation { host: operator_host_srv3, catalog: hma82gr7afr4n_vk_catalog, stick_count: 8 }, + expectation: HostDimmExpectation { host: operator_host_srv3, catalog: m393a8g40d40_crb0q_catalog, stick_count: 8 }, observation: srv3_dimm_observation, ), dimm_reconcile_verdict( - expectation: HostDimmExpectation { host: operator_host_srv4, catalog: hma82gr7afr4n_vk_catalog, stick_count: 8 }, + expectation: HostDimmExpectation { host: operator_host_srv4, catalog: m393a8g40d40_crb0q_catalog, stick_count: 8 }, observation: srv4_dimm_observation, ), ] diff --git a/dag/gunbc/host_memory_qualification.dag b/dag/gunbc/host_memory_qualification.dag index 5175808d58f..465de6d8ee2 100644 --- a/dag/gunbc/host_memory_qualification.dag +++ b/dag/gunbc/host_memory_qualification.dag @@ -3,10 +3,12 @@ module gunbc.host_memory_qualification import std.types { Bool, EpochMs, List, NonEmptyStr } import std.nat { Nat } import std.measure { ByteSize } -import product.placement_supply { HostIdentity } import extdeps.boards.types { AsrockRackAltrad8ud1l2t, BaseboardModel, DimmPopulation } import extdeps.boards.asrock_rack { asrock_altrad8ud_download_authority } import extdeps.external_authority { ExternalAuthority } +import extdeps.cpu.ampere { ampere_altra_avl_authority, ampere_altra_avl_current_issue } +import product.placement_supply { HostIdentity } +import gunbc.fleet_intent_network { operator_host_srv2, operator_host_srv3, operator_host_srv4 } import extdeps.memory.types { DramModuleCatalogRow, JedecDdrGenerationCatalogRow } import extdeps.memory.training { LrdimmDataBufferMrep, @@ -304,4 +306,124 @@ data altrad8ud_mrep_failure_observation: PlatformTrainingFailure = PlatformTrain } +// --- THE 2026-08-22 REPLACEMENT, GRADED ON THE SAME FOUR AXES ----------------------------------- +// +// WHY THESE ROWS EXIST AT ALL, given that both hosts are up and serving. The 2026-08-11 incident's +// whole lesson was that "the memory works" is four questions, and a successful outcome collapses +// them just as easily as a failure did -- more easily, because nobody interrogates a green. srv3 +// and srv4 reaching the OS at 512 GiB is a BOOT receipt and a TRAINING receipt for this part on +// this board. It is NOT a part qualification, and recording it as one would be the rung inflation +// DESIGN 4b names. +// +// WHAT IS DIFFERENT ABOUT THIS PART FROM THE ONE THAT FAILED, and it is the reason to expect a +// different outcome rather than merely to observe one: the M386A4G40DM0-CPB was LOAD-REDUCED, so +// it had to execute the data-buffer read-phase calibration (MREP) that platform_training_implication_note +// grades as this board's observed failing step. M393A8G40D40-CRB0Q is REGISTERED and 3DS-stacked, +// not load-reduced, so it does not execute that step at all. The topology-pressure paragraph in +// that note predicted exactly this shape: 64 GB DDR4 forces extra ranks or stacking, and the two +// ways to get there -- load reduction versus 3DS -- are different modules, not the same module at +// different speeds. This population took the stacked route and cleared the step the other failed. +// +// PART QUALIFICATION REMAINS NotListedInVendorAvl AND THAT IS NOT A COMPLAINT. The Ampere AVL +// issue 1.15 does not carry this part number. Absence is the absence of a positive result, which +// is precisely why the boot and training receipts below are worth having: they are host-specific +// evidence standing where a vendor result does not exist. Two independent hosts, eight modules +// each, one per channel, is a real sample and it is still not an AVL entry. +// TRAINING IS UNOBSERVED ON BOTH ROWS AND THAT IS THE HONEST ANSWER, not a gap I failed to close. +// TrainingOperational carries a dimm_mask because the 2026-08-11 evidence for it was a specific +// firmware artifact -- "DDR: Operational DIMM: 0x00005555" off the console. No such reading was +// taken for this population: the observation here is Redfish inventory, which reports what the +// memory subsystem ENUMERATES, plus a clean BMC event log. That is strong circumstantial evidence +// (a module failing training does not enumerate at full capacity) and it is NOT a mask. +// +// The first draft of these rows put that circumstantial prose INTO the dimm_mask field, which +// would have made an inference indistinguishable from a firmware reading in the one carrier built +// to keep the four axes apart -- the module's own defect, committed inside the module. Boot is +// established by direct observation and says so; training waits for a console read. +data srv3_new_population_standing: HostMemoryStanding = HostMemoryStanding { + host: operator_host_srv3, + part_number: "M393A8G40D40-CRB0Q", + population: ["DDR4_A1", "DDR4_B1", "DDR4_C1", "DDR4_D1", "DDR4_E1", "DDR4_F1", "DDR4_G1", "DDR4_H1"], + class_support: ClassSupportedByBoard, + part_qualification: NotListedInVendorAvl { + avl_authority: ampere_altra_avl_authority, + avl_issue: ampere_altra_avl_current_issue, + }, + training: TrainingOutcomeUnobserved, + boot: BootReachedOperatingSystem, + observed_at: 1787775338000, +} + +data srv4_new_population_standing: HostMemoryStanding = HostMemoryStanding { + host: operator_host_srv4, + part_number: "M393A8G40D40-CRB0Q", + population: ["DDR4_A1", "DDR4_B1", "DDR4_C1", "DDR4_D1", "DDR4_E1", "DDR4_F1", "DDR4_G1", "DDR4_H1"], + class_support: ClassSupportedByBoard, + part_qualification: NotListedInVendorAvl { + avl_authority: ampere_altra_avl_authority, + avl_issue: ampere_altra_avl_current_issue, + }, + training: TrainingOutcomeUnobserved, + boot: BootReachedOperatingSystem, + observed_at: 1787773558000, +} + +// srv2 FAILED THE SAME PART THAT THREE SIBLINGS TRAINED, AND THAT IS THE MOST INFORMATIVE ROW +// IN THIS MODULE (2026-08-22). srv1, srv3 and srv4 all POSTed on the 64 GiB Samsung population; +// srv2 could not, was left power-cycling, and was reverted to its 8 x 16 GiB Hynix set, on which +// it booted in about 2.5 minutes and returned to service with five runners. +// +// WHY THE BOOT AXIS READS RepeatingFirmwareReset RATHER THAN A TRAINING FAILURE. The BMC event +// log shows a loop: power on, then Power.Error.Blackout after 13m14s, 14m26s, and 7m35s, with +// PowerRestorePolicy=AlwaysOn restarting it each time. That is the boot axis. The TRAINING axis +// stays Unobserved, and the distinction is exactly what this module's four independent standings +// exist for: nobody read a training mask, because on this platform nothing can. +// +// THE OBSERVABILITY FINDING IS WORTH MORE THAN THE FAILURE. HostLogger captured ZERO host serial +// entries -- not during the failures, and not during srv2's subsequent SUCCESSFUL boot either. +// That control is what makes it a finding rather than a symptom: the recorder was never running, +// so "what did the firmware say while training" is unavailable BY CONSTRUCTION on this fleet, not +// merely unread. Any future attempt is blind in the same way unless serial capture is fixed +// first, and a binary search over DIMMs would be running on pass/fail and wall-clock alone. +// +// WHAT THE EVIDENCE RULES OUT, recorded so it is not re-investigated: the 2026-06-02 aux-connector +// VRM failure did NOT recur (all 16 rails matched srv1 within millivolts, including the five that +// read 0.01 V then), and the SoC was neither dead nor idle -- all eight per-DIMM thermal sensors +// read 67-75 C against a 50 C SoC, matching a fully-booted srv1, an hour after srv2 last ran an +// OS. The SoC was alive and driving all eight channels. The thermal spread was EVEN, so no +// channel was being skipped: this was a convergence failure across a populated bus, not one dead +// channel. +// +// VARIABLE TIME-TO-FAILURE IS THE REASON THIS IS NOT CLOSED. 13m14s, 14m26s and 7m35s are not a +// deterministic firmware timeout; they point at something marginal -- signal integrity or a flaky +// rank. The practical consequence is that ONE successful boot would not establish a fix, so the +// part_qualification axis below stays NotListedInVendorAvl and this host's standing stays a +// failure rather than being softened by the three siblings that worked. +data srv2_failed_64gib_population_standing: HostMemoryStanding = HostMemoryStanding { + host: operator_host_srv2, + part_number: "M393A8G40D40-CRB0Q", + population: ["DDR4_A1", "DDR4_B1", "DDR4_C1", "DDR4_D1", "DDR4_E1", "DDR4_F1", "DDR4_G1", "DDR4_H1"], + class_support: ClassSupportedByBoard, + part_qualification: NotListedInVendorAvl { + avl_authority: ampere_altra_avl_authority, + avl_issue: ampere_altra_avl_current_issue, + }, + training: TrainingOutcomeUnobserved, + boot: RepeatingFirmwareReset { token: "Power.Error.Blackout (no firmware POST token reached; BootProgress remained Unspecified at epoch zero)", cycles: 3 }, + observed_at: 1787782000000, +} + +data srv2_boot_serial_unobservable_note: String = "srv2 HostLogger held ZERO entries across both the failed 64 GiB cycles AND the successful 8 x 16 GiB boot that followed. The successful boot is the control: it proves the absence is a missing recorder, not a mute SoC. Consequence for any retry: the training axis cannot be observed on this fleet until host serial capture works (the obmc-console server configs for ttyS1/ttyS2/ttyS3 exist -- ttyS2 is the SCP, which runs DDR training -- but nothing is captured), so the highest-value action before re-testing 64 GiB on srv2 is fixing serial capture or attaching a physical cable. Failing that, the per-DIMM thermal sensors are the working instrument: the baseline is all eight at 67-75 C during a FAILED run, so a future attempt showing one channel cool fingers that channel with no firmware log needed." + +// THE ONE OPEN ITEM ON THIS POPULATION, kept as data rather than left in a chat log. +// srv4 logged a single CORRECTABLE ECC error at 2026-08-22T19:45:57Z -- Socket 0 / Channel 0 / +// DIMM 0, bank 13 row 166 column 96 -- about three minutes after an unclean restart following a +// power blackout. Corrected, no uncorrectable event, no repeat, and no comparable event on srv3. +// It does NOT move any of the four axes: boot is established, training is operational, and a +// corrected single-bit event is not a qualification result in either direction. +// It is recorded because the distinguishing fact is a REPEAT at the same bank/row/column, which +// separates a marginal device from a single upset, and nobody can look for a repeat against an +// event that was never written down. +data srv4_correctable_ecc_watch_note: String = "srv4 dimm0 (Bank 1 DDR4_A1, serial 026B6F84): one MemoryECCCorrectable at 2026-08-22T19:45:57Z, bank 13 row 166 column 96, decoded through the BMC's own OpenBMC message registry rather than guessed. Watch for recurrence at the same coordinates. A second event there is a device-level finding; scattered single events across different addresses are not." + data platform_training_implication_note: String = "RELOCATED 2026-08-19 from the deleted gunbc.memory_part_selection, whose candidate/frontier half was a selection island; this evidence half is qualification, so it lives beside the four standings it grades. The grading rule is mechanical and derived: a candidate is graded by whether it must execute a training step THIS platform has been observed to fail, and by how strongly that failure is evidenced. For the ALTRAD8UD-1L2T the step is the DDR4 data-buffer read-phase calibration (MREP), which only load-reduced modules execute, so the grading is independent of vendor, part number, capacity, speed grade, and presence on any approved-vendor list. THE SEVERITY IS A FUNCTION OF EVIDENCE, and an earlier revision of this module got that wrong in a way worth recording: it refused every module executing the failing step, on any board, at any standing including EvidenceUnobserved. Because capacities near a generation's die-density ceiling are disproportionately load-reduced, that blanket rule removed most of the 64GB DDR4 market by construction — the exact blocklist this module's prose claimed to avoid, reached by a different route, and the opposite of letting a buyer shop the whole market. Now: a decode of this platform's own syndrome register refuses; an association carrying byte-identical controller status words, or an inference from sequence position, requires a SAMPLE before committing to a full population and stays on the Pareto frontier; an unobserved standing implicates nothing. gunbc holds MREP at AssociatedByIdenticalSignature, so the honest verdict for another ALTRAD8UD LRDIMM today is buy-one-and-test, not reject. Failures are scoped to the board they were observed on, so an ALTRAD8UD receipt cannot speak for a different platform. KNOWN GAP, stated rather than papered over: BaseboardModel currently has exactly one variant, 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, and the control lands when a second real board is modeled. The second axis, topology pressure, is derived rather than observed: when a capacity cannot be reached as a dual-rank registered module within the generation's monolithic die-density ceiling, that capacity forces extra ranks or stacking, which is why 64GB DDR4 at older speed grades is disproportionately load-reduced while 32GB is not. A buyer economizing on speed grade at 64GB is therefore not buying the same module more slowly, it is a different topology — which is a reason to sample it, not a reason to refuse it." diff --git a/dag/test/claim/build_fulfillment_witness_test.dag b/dag/test/claim/build_fulfillment_witness_test.dag index 795894bc59f..0ecb5afb67b 100644 --- a/dag/test/claim/build_fulfillment_witness_test.dag +++ b/dag/test/claim/build_fulfillment_witness_test.dag @@ -13,6 +13,7 @@ import extdeps.memory.types { Registered, bit_width, dram_generation_ddr4, + MonolithicDie, } import extdeps.cpu.ampere_altra_platform_hw_design.platform { OneDimmPerChannel, TwoDimmsPerChannel } import gunbc.memory_provisioning { FullChannel, PopulationOption } @@ -122,6 +123,7 @@ data fixture_dimm: DramModuleCatalogRow = DramModuleCatalogRow { data_rate_mts: 3200, ecc: true, buffering: Registered, + die_stacking: MonolithicDie, chip_width: bit_width(count: 4), rank_count: 2, } diff --git a/dag/test/claim/fleet_intent_memory_witness_test.dag b/dag/test/claim/fleet_intent_memory_witness_test.dag index c13d1045fce..6607280b1d1 100644 --- a/dag/test/claim/fleet_intent_memory_witness_test.dag +++ b/dag/test/claim/fleet_intent_memory_witness_test.dag @@ -16,9 +16,12 @@ import gunbc.fleet_intent { srv1_memory_population, srv2_memory_population, srv3_memory_population, - srv1_memory_population_observation_note, + srv1_memory_population_observation_2026_07_16_note, srv2_memory_population_observation_note, - srv3_memory_population_observation_note, + srv3_memory_population_observation_2026_08_22_note, + srv4_memory_population, + srv4_memory_population_observation_note, + srv4_host, compute_host_ram_bytes_total, fleet_host_memory_nominal_vs_usable_note, } @@ -27,7 +30,8 @@ import extdeps.memory { host_memory_population_nominal_bytes, memory_population_row_bytes, } -import extdeps.memory.sk_hynix { hma82gr7afr4n_vk_catalog, hma82gr7afr8n_vk_catalog } +import extdeps.memory.sk_hynix { hma82gr7afr4n_vk_catalog } +import extdeps.memory.samsung { m393a8g40d40_crb0q_catalog } import extdeps.memory.types { MemoryPopulationRow, HostMemoryPopulation, dram_module_is_realizable } import extdeps.memory.jedec { ddr4_generation_catalog } import extdeps.bmc.redfish { redfish_memory_summary_from_gib } @@ -35,9 +39,11 @@ import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly -data srv3_bmc_observed_total_gib: Gibibyte = gibibyte(128) +data srv3_bmc_observed_total_gib: Gibibyte = gibibyte(512) -data srv1_bmc_observed_total_gib: Gibibyte = gibibyte(128) +data srv4_bmc_observed_total_gib: Gibibyte = gibibyte(512) + +data srv1_bmc_observed_total_gib: Gibibyte = gibibyte(512) data srv2_bmc_observed_total_gib: Gibibyte = gibibyte(128) @@ -52,33 +58,26 @@ test fn srv3_population_matches_bmc_memory_summary() -> Bool { test fn srv3_host_memory_derives_from_cited_population() -> Bool { let host_ram = byte_size_count(compute_host_ram_bytes_total(host: srv3_host)) let nominal = byte_size_count(host_memory_population_nominal_bytes(pop: srv3_memory_population)) - host_ram == nominal && list_length(items: srv3_host.memory) == 2 + host_ram == nominal && list_length(items: srv3_host.memory) == 1 } test fn srv3_observed_catalog_rows_are_jedec_realizable() -> Bool { - dram_module_is_realizable(module: hma82gr7afr8n_vk_catalog, jedec: ddr4_generation_catalog) - && dram_module_is_realizable(module: hma82gr7afr4n_vk_catalog, jedec: ddr4_generation_catalog) + dram_module_is_realizable(module: m393a8g40d40_crb0q_catalog, jedec: ddr4_generation_catalog) } test fn srv3_population_row_bytes_match_stick_capacity() -> Bool { - let seven_sticks = byte_size_count( - memory_population_row_bytes( - row: MemoryPopulationRow { module: hma82gr7afr8n_vk_catalog, stick_count: 7 } - ) - ) - let one_stick = byte_size_count( + let eight_sticks = byte_size_count( memory_population_row_bytes( - row: MemoryPopulationRow { module: hma82gr7afr4n_vk_catalog, stick_count: 1 } + row: MemoryPopulationRow { module: m393a8g40d40_crb0q_catalog, stick_count: 8 } ) ) - seven_sticks == 7 * byte_size_count(hma82gr7afr8n_vk_catalog.capacity_bytes) - && one_stick == byte_size_count(hma82gr7afr4n_vk_catalog.capacity_bytes) + eight_sticks == 8 * byte_size_count(m393a8g40d40_crb0q_catalog.capacity_bytes) } test fn red_wrong_stick_count_changes_nominal_total() -> Bool { let wrong = HostMemoryPopulation { rows: [ - MemoryPopulationRow { module: hma82gr7afr8n_vk_catalog, stick_count: 7 }, + MemoryPopulationRow { module: m393a8g40d40_crb0q_catalog, stick_count: 7 }, ], } let wrong_total = byte_size_count(host_memory_population_nominal_bytes(pop: wrong)) @@ -119,9 +118,9 @@ test fn red_srv1_seven_stick_population_differs_from_observed() -> Bool { } test fn srv1_srv2_observation_notes_record_raw_redfish_fields() -> Bool { - string_contains(s: srv1_memory_population_observation_note, pattern: "HMA82GR7AFR4N-VK RankCount=1") - && string_contains(s: srv1_memory_population_observation_note, pattern: "192.168.1.183") - && string_contains(s: srv1_memory_population_observation_note, pattern: "(×8)") + string_contains(s: srv1_memory_population_observation_2026_07_16_note, pattern: "HMA82GR7AFR4N-VK RankCount=1") + && string_contains(s: srv1_memory_population_observation_2026_07_16_note, pattern: "192.168.1.183") + && string_contains(s: srv1_memory_population_observation_2026_07_16_note, pattern: "(×8)") && string_contains(s: srv2_memory_population_observation_note, pattern: "HMA82GR7AFR4N-VK RankCount=1") && string_contains(s: srv2_memory_population_observation_note, pattern: "192.168.1.184") && string_contains(s: srv2_memory_population_observation_note, pattern: "(×8)") @@ -138,7 +137,31 @@ test fn nominal_population_and_os_usable_budget_are_distinct_facts() -> Bool { } test fn srv3_observation_note_records_raw_redfish_fields() -> Bool { - string_contains(s: srv3_memory_population_observation_note, pattern: "dimm7 HMA82GR7AFR4N-VK RankCount=1") - && string_contains(s: srv3_memory_population_observation_note, pattern: "dimm0 HMA82GR7AFR8N-VK RankCount=2") - && string_contains(s: srv3_memory_population_observation_note, pattern: "DataWidthBits=64") + string_contains(s: srv3_memory_population_observation_2026_08_22_note, pattern: "M393A8G40D40-CRB") + && string_contains(s: srv3_memory_population_observation_2026_08_22_note, pattern: "TotalSystemMemoryGiB=512") + && string_contains(s: srv3_memory_population_observation_2026_08_22_note, pattern: "OperatingSpeedMhz=2133") +} + +// THE FLEET IS HETEROGENEOUS AND THIS IS THE CONTROL THAT SAYS SO. Until 2026-08-22 every host +// carried the same population, so a test asserting srv1 == srv3 would have passed for the wrong +// reason and kept passing through the upgrade. This one goes red if anyone re-uniformizes the +// rows -- in either direction -- without an observation to justify it. +test fn upgraded_and_legacy_hosts_carry_different_populations() -> Bool { + let srv2_nominal = byte_size_count(host_memory_population_nominal_bytes(pop: srv2_memory_population)) + let srv3_nominal = byte_size_count(host_memory_population_nominal_bytes(pop: srv3_memory_population)) + let srv4_nominal = byte_size_count(host_memory_population_nominal_bytes(pop: srv4_memory_population)) + srv3_nominal == srv4_nominal && srv2_nominal != srv3_nominal +} + +test fn srv4_population_matches_bmc_memory_summary() -> Bool { + let nominal = byte_size_count(host_memory_population_nominal_bytes(pop: srv4_memory_population)) + let bmc = byte_size_count( + redfish_memory_summary_from_gib(total_gib: srv4_bmc_observed_total_gib).total_memory_bytes + ) + nominal == bmc && byte_size_count(compute_host_ram_bytes_total(host: srv4_host)) == nominal +} + +test fn srv4_observation_note_records_the_read_that_retired_the_deferral() -> Bool { + string_contains(s: srv4_memory_population_observation_note, pattern: "M393A8G40D40-CRB") + && string_contains(s: srv4_memory_population_observation_note, pattern: "TotalSystemMemoryGiB=512") } diff --git a/dag/test/claim/host_allocation_conservation_test.dag b/dag/test/claim/host_allocation_conservation_test.dag index d090bd5528b..3d93179a151 100644 --- a/dag/test/claim/host_allocation_conservation_test.dag +++ b/dag/test/claim/host_allocation_conservation_test.dag @@ -239,12 +239,31 @@ test fn perturbing_one_host_moves_only_that_host() -> Bool { && synthetic_bytes_of(host: operator_host_srv3) != byte_size_count(b: usable_ram_of(host: operator_host_srv3)) } +// srv3 IS MEASURED AS OF 2026-08-22, so this control moved to srv2 -- which is now the fleet's +// genuine lower-bound host, its 64 GiB upgrade having failed DDR training and been reverted the +// same day. The property under test is unchanged: whatever a host's row carries must not exceed +// that host's real usable RAM, because the conservation wall spends against it. test fn a_larger_host_reading_is_not_admissible_as_a_lower_bound() -> Bool { - match gunbc_ci_host_usable_ram_for(host: operator_host_srv3) { + match gunbc_ci_host_usable_ram_for(host: operator_host_srv2) { HostUsableRamMeasured { bytes: _, provenance: _ } => false HostUsableRamUnmeasured => false HostUsableRamConservativeLowerBound { bytes: b, basis: _ } => - byte_size_count(b: b) <= byte_size_count(b: usable_ram_of(host: operator_host_srv3)) + byte_size_count(b: b) <= byte_size_count(b: usable_ram_of(host: operator_host_srv2)) + } +} + +// THE MEASURED ARM IS REAL AND UNDER 512 GiB, which is the whole point of keeping nominal and +// usable apart. srv3 carries 512 GiB of DIMMs and the kernel reports 502.25 GiB; this asserts the +// row carries the KERNEL figure. It goes red if anyone ever writes the Redfish nominal number +// into this carrier -- the specific error that became possible the day the BMC started reporting +// a bigger number than the budget had ever seen. +test fn measured_usable_ram_is_the_kernel_figure_not_the_dimm_total() -> Bool { + match gunbc_ci_host_usable_ram_for(host: operator_host_srv3) { + HostUsableRamMeasured { bytes: b, provenance: _ } => + byte_size_count(b: b) == 539282522112 + && byte_size_count(b: b) < 549755813888 + HostUsableRamConservativeLowerBound { bytes: _, basis: _ } => false + HostUsableRamUnmeasured => false } } @@ -258,8 +277,10 @@ test fn unclassified_host_refuses_rather_than_borrowing() -> Bool { } } +// Re-pointed to srv2 for the same reason as the control above: it is now the host that carries +// the bound. The arm itself is unchanged and still reachable. test fn middle_arm_is_a_bound_not_a_measurement() -> Bool { - match gunbc_ci_host_usable_ram_for(host: operator_host_srv3) { + match gunbc_ci_host_usable_ram_for(host: operator_host_srv2) { HostUsableRamMeasured { bytes: _, provenance: _ } => false HostUsableRamConservativeLowerBound { bytes: b, basis: _ } => byte_size_count(b: b) == 134217728000 HostUsableRamUnmeasured => false diff --git a/dag/test/claim/host_memory_qualification_witness_test.dag b/dag/test/claim/host_memory_qualification_witness_test.dag index d9e7d3b7910..29403f339bb 100644 --- a/dag/test/claim/host_memory_qualification_witness_test.dag +++ b/dag/test/claim/host_memory_qualification_witness_test.dag @@ -16,6 +16,7 @@ import extdeps.memory.types { Registered, bit_width, dram_generation_ddr4, + MonolithicDie, } import extdeps.memory.training { LrdimmDataBufferMrep, module_executes_step } import std.measure { ByteSize, byte_size } @@ -255,6 +256,7 @@ data lrdimm_32g: DramModuleCatalogRow = DramModuleCatalogRow { data_rate_mts: 2133, ecc: true, buffering: LoadReduced, + die_stacking: MonolithicDie, chip_width: bit_width(count: 4), rank_count: 4, } @@ -269,6 +271,7 @@ data rdimm_32g: DramModuleCatalogRow = DramModuleCatalogRow { data_rate_mts: 2666, ecc: true, buffering: Registered, + die_stacking: MonolithicDie, chip_width: bit_width(count: 4), rank_count: 2, } diff --git a/dag/test/claim/installed_bom_reconcile_witness_test.dag b/dag/test/claim/installed_bom_reconcile_witness_test.dag index 1428c7d5075..6748d0b1fd6 100644 --- a/dag/test/claim/installed_bom_reconcile_witness_test.dag +++ b/dag/test/claim/installed_bom_reconcile_witness_test.dag @@ -35,6 +35,7 @@ import product.installed_bom_reconcile { } import extdeps.memory.types { MemoryPopulationRow } import extdeps.memory.sk_hynix { hma82gr7afr4n_vk_catalog, hma82gr7afr8n_vk_catalog } +import extdeps.memory.samsung { m393a8g40d40_crb0q_catalog } import extdeps.memory.samsung { m386a4g40dm0_cpb_catalog } import extdeps.cpu.ampere { altra_max_m12830_catalog, altra_q6430_catalog } import product.inventory { @@ -107,11 +108,21 @@ test fn srv1_live_population_confirms_the_expectation() -> Bool { } } -// THE REFUSAL FIRES ON REAL DATA. srv3's observed population is seven HMA82GR7AFR8N-VK plus one -// HMA82GR7AFR4N-VK against a uniform AFR4N expectation, so exactly ONE row differs, it is located -// at population grain because the BMC reported no slot, and the stick total still matches — which -// is the discrimination this witness exists for: a refusal whose count axis says Matches proves -// the part axis alone produced it. +// THE REFUSAL FIRES ON REAL DATA. srv3's observed population is eight M393A8G40D40-CRB0Q against +// a uniform AFR4N expectation, so exactly ONE row differs, it is located at population grain +// because the BMC reported no slot, and the stick total still matches -- which is the +// discrimination this witness exists for: a refusal whose count axis says Matches proves the +// part axis alone produced it. +// +// THE OBSERVATION MOVED UNDER THIS TEST ON 2026-08-22 AND THE TEST IS BETTER FOR IT, which is +// worth recording because the alternative was to pin it to a fixture and stop reading live data. +// It previously ran against srv3's mixed seven-plus-one Hynix population, where "exactly one row +// differs" was a fact about two Hynix part numbers happening to collapse into one discrepancy +// row. The replacement made srv3 uniform, so the same assertion now discriminates a cleaner +// case: eight-of-one against eight-of-another, count identical, part axis solely responsible. +// The expectation stays deliberately WRONG (it names the Hynix part srv3 no longer carries) +// because this witness's subject is the refusal, not the fleet's current correctness -- the +// matching expectation lives in gunbc.fleet_physical_inventory and is checked there. test fn srv3_live_population_refuses_with_a_located_part_difference() -> Bool { match dimm_reconcile_verdict( expectation: HostDimmExpectation { @@ -132,7 +143,7 @@ test fn srv3_live_population_refuses_with_a_located_part_difference() -> Bool { Present { value: d } => d.expected_part == hma82gr7afr4n_vk_catalog.part_number && match d.observed { - ObservedDimmCataloged { catalog: c } => c.part_number == hma82gr7afr8n_vk_catalog.part_number + ObservedDimmCataloged { catalog: c } => c.part_number == m393a8g40d40_crb0q_catalog.part_number ObservedDimmUncataloged { part_number: _ } => false } && match d.location { @@ -265,19 +276,34 @@ test fn an_observation_of_another_host_refuses() -> Bool { } } -// AN UNOBSERVED HOST STAYS UNOBSERVED. srv4 has no read at either grain, and the verdict must be -// neither a pass nor a refusal — a pass would zero the observation deficit's frequency by -// construction, and a refusal would accuse hardware nobody has looked at. -test fn srv4_unobserved_reaches_neither_confirmed_nor_refused() -> Bool { +// AN UNOBSERVED HOST STAYS UNOBSERVED. The verdict must be neither a pass nor a refusal -- a pass +// would zero the observation deficit's frequency by construction, and a refusal would accuse +// hardware nobody has looked at. +// +// THIS CONTROL LOST ITS LIVE SPECIMEN ON 2026-08-22 AND IS KEPT ANYWAY, which is the point worth +// recording. srv4 WAS the unobserved host and drove this test directly; the authenticated Redfish +// read that retired its deferral moved it to a real population, so nothing in the live fleet now +// occupies DimmObservationAbsent. That is a guard going quiet, not a guard dying: the arm is still +// reachable -- the next host racked without a read produces it -- and deleting a wall because +// nothing currently lands in it is how a live wall gets removed while looking principled. +// +// So the input is now CONSTRUCTED rather than live, and the test says so in its name. The honest +// cost of that swap is that this no longer proves anything about the fleet, only about the fold; +// the fleet-level claim it used to carry is the report-length test below, which is where the +// change in occupancy is actually visible. +test fn constructed_unobserved_host_reaches_neither_confirmed_nor_refused() -> Bool { match dimm_reconcile_verdict( expectation: HostDimmExpectation { - host: "srv4" as HostIdentity, + host: "srv-never-read" as HostIdentity, catalog: hma82gr7afr4n_vk_catalog, stick_count: 8, }, - observation: srv4_dimm_observation, + observation: DimmObservationAbsent { + host: "srv-never-read" as HostIdentity, + cause: "constructed: no per-DIMM read has been taken for this host at either grain", + }, ) { - DimmPopulationUnconfirmed { host: h, cause: _ } => h == ("srv4" as HostIdentity) + DimmPopulationUnconfirmed { host: h, cause: _ } => h == ("srv-never-read" as HostIdentity) DimmPopulationConfirmed { host: _, stick_count: _ } => false DimmPopulationRefused { host: _, discrepancies: _, count: _ } => false DimmObservationHostMismatch { expectation_host: _, observation_host: _ } => false @@ -285,11 +311,22 @@ test fn srv4_unobserved_reaches_neither_confirmed_nor_refused() -> Bool { } // A confirmed population contributes nothing to the report, so the report's length counts real -// contradictions only. Over the four live fleet verdicts that is exactly srv3's single row: srv1 -// and srv2 confirm and srv4 is unobserved, so a report of any other length would mean silence had -// leaked into it. -test fn the_fleet_report_carries_exactly_the_live_contradiction() -> Bool { - dimm_discrepancy_report(verdicts: fleet_dimm_verdicts).length() == 1 +// contradictions only. THE LIVE FLEET NOW RECONCILES AND THE EXPECTED LENGTH IS ZERO: srv1 and +// srv2 confirm against the Hynix rows they still carry, and srv3 and srv4 confirm against the +// Samsung rows installed on 2026-08-22 with their expectations updated in the same change. +// +// A ZERO-LENGTH ASSERTION IS WEAK ON ITS OWN and is deliberately not carrying this claim alone. +// It cannot distinguish "the fleet agrees" from "the report is broken and returns nothing", which +// is exactly the empty-observation narrow DESIGN 5 names. What discriminates it is the pair of +// live refusal tests above -- srv3 against a deliberately wrong expectation still produces one +// located row -- so the fold is proven able to emit a discrepancy on the same data path that here +// emits none. Read the two together or neither means anything. +// +// It previously asserted ONE, which was srv3's mixed Hynix population against a uniform +// expectation. That contradiction was resolved by making the expectation true, not by suppressing +// it. +test fn the_fleet_report_is_empty_while_every_expectation_matches() -> Bool { + dimm_discrepancy_report(verdicts: fleet_dimm_verdicts).length() == 0 } // Every verdict the fold produces is grounded: no refusal names an empty discrepancy list with a diff --git a/dag/test/claim/jedec_ddr_generation_witness_test.dag b/dag/test/claim/jedec_ddr_generation_witness_test.dag index 85a24abc824..b1cd95dc7dc 100644 --- a/dag/test/claim/jedec_ddr_generation_witness_test.dag +++ b/dag/test/claim/jedec_ddr_generation_witness_test.dag @@ -10,6 +10,7 @@ data mod_ddr4_32g_1rx8: DramModuleCatalogRow = DramModuleCatalogRow { data_rate_mts: 3200, ecc: true, buffering: Registered, + die_stacking: MonolithicDie, chip_width: bit_width(count: 8), rank_count: 1, } @@ -22,6 +23,7 @@ data mod_ddr5_32g_1rx8: DramModuleCatalogRow = DramModuleCatalogRow { data_rate_mts: 4800, ecc: true, buffering: Registered, + die_stacking: MonolithicDie, chip_width: bit_width(count: 8), rank_count: 1, } diff --git a/dag/test/claim/memory_provisioning_witness_test.dag b/dag/test/claim/memory_provisioning_witness_test.dag index 018e8acda12..37c587b0b3a 100644 --- a/dag/test/claim/memory_provisioning_witness_test.dag +++ b/dag/test/claim/memory_provisioning_witness_test.dag @@ -34,6 +34,7 @@ import extdeps.memory.types { bit_width, dram_generation_ddr4, dram_generation_ddr5, + MonolithicDie, } import gunbc.runner_shape_census { NoShapesForProviderArchitecture, @@ -123,6 +124,7 @@ fn rdimm(part: NonEmptyStr, capacity: Nat) -> DramModuleCatalogRow { data_rate_mts: 3200, ecc: true, buffering: Registered, + die_stacking: MonolithicDie, chip_width: bit_width(count: 4), rank_count: 2, } @@ -145,6 +147,7 @@ fn rdimm_32g_ddr5() -> DramModuleCatalogRow { data_rate_mts: 4800, ecc: true, buffering: Registered, + die_stacking: MonolithicDie, chip_width: bit_width(count: 4), rank_count: 2, } diff --git a/dag/test/claim/node_power_envelope_witness_test.dag b/dag/test/claim/node_power_envelope_witness_test.dag index 36de97faf3d..c1c07ed3fe3 100644 --- a/dag/test/claim/node_power_envelope_witness_test.dag +++ b/dag/test/claim/node_power_envelope_witness_test.dag @@ -22,6 +22,7 @@ import extdeps.memory.types { dram_generation_ddr4, dram_module_is_realizable, dram_module_required_die_density, + MonolithicDie, } import extdeps.cpu.ampere { altra_max_m12830_catalog, altra_q8030_catalog } import extdeps.cpu.ampere_altra_platform_hw_design.platform { OneDimmPerChannel, TwoDimmsPerChannel } @@ -85,6 +86,7 @@ data mod_2rx4_32g: DramModuleCatalogRow = DramModuleCatalogRow { data_rate_mts: 3200, ecc: true, buffering: Registered, + die_stacking: MonolithicDie, chip_width: bit_width(count: 4), rank_count: 2, } @@ -97,6 +99,7 @@ data mod_1rx4_16g: DramModuleCatalogRow = DramModuleCatalogRow { data_rate_mts: 2666, ecc: true, buffering: Registered, + die_stacking: MonolithicDie, chip_width: bit_width(count: 4), rank_count: 1, } @@ -109,6 +112,7 @@ data mod_1rx8_32g_impossible: DramModuleCatalogRow = DramModuleCatalogRow { data_rate_mts: 3200, ecc: true, buffering: Registered, + die_stacking: MonolithicDie, chip_width: bit_width(count: 8), rank_count: 1, } @@ -382,6 +386,7 @@ data rdimm_64g_2rx4: DramModuleCatalogRow = DramModuleCatalogRow { data_rate_mts: 3200, ecc: true, buffering: Registered, + die_stacking: MonolithicDie, chip_width: bit_width(count: 4), rank_count: 2, } diff --git a/dag/test/claim/samsung_dram_module_witness_test.dag b/dag/test/claim/samsung_dram_module_witness_test.dag index 5512b192937..f67f55c2ac5 100644 --- a/dag/test/claim/samsung_dram_module_witness_test.dag +++ b/dag/test/claim/samsung_dram_module_witness_test.dag @@ -14,6 +14,7 @@ data control_32g_1rx8: DramModuleCatalogRow = DramModuleCatalogRow { data_rate_mts: 2133, ecc: true, buffering: LoadReduced, + die_stacking: MonolithicDie, chip_width: bit_width(count: 8), rank_count: 1, } From 09792715f2a6aa4793ad006676a4240d6b820f34 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 22 Aug 2026 23:07:44 +0000 Subject: [PATCH 2/5] srv1's expectation disagreed with its own population, in two places, and the timestamp was a placeholder review 54843 found both. Both were real. 1. srv1's population became 8x Samsung M393A8G40D40-CRB0Q while its HostDimmExpectation stayed on the Hynix row. The fleet reconcile witness joins those two, so this would have gone red at the first floor run -- a data disagreement, not a type error, which is precisely the class the compile I ran cannot see. The review named one site. There were two: fleet_dimm_expectations and an inline duplicate inside fleet_dimm_verdicts. Both corrected. The fork itself is flagged in-file and deliberately NOT dissolved here: fleet_dimm_expectations currently has no consumer, and an unconsumed declaration may still be read by a lens, so collapsing it is a separate judgment with its own evidence -- not a drive-by in a review-response commit. 2. The srv4 Redfish observation carried a literal "19:5xZ" -- a placeholder shaped like a timestamp, which is the fabricated plausible output DESIGN section 5 forbids, in the provenance field of all places. Replaced with the honest bounded window (between 19:46Z and 20:15Z) and an explicit statement that the exact minute was not recorded and is not reconstructed. Also adds dag/test/parsecheck.dag, the entry used to compile this change's closure. Co-Authored-By: Claude Opus 5 (1M context) --- dag/gunbc/fleet_intent.dag | 2 +- dag/gunbc/fleet_physical_inventory.dag | 19 +++++++++++++++++-- dag/test/parsecheck.dag | 14 ++++++++++++++ 3 files changed, 32 insertions(+), 3 deletions(-) create mode 100644 dag/test/parsecheck.dag diff --git a/dag/gunbc/fleet_intent.dag b/dag/gunbc/fleet_intent.dag index f85534ad259..0ed1b2eeb59 100644 --- a/dag/gunbc/fleet_intent.dag +++ b/dag/gunbc/fleet_intent.dag @@ -289,7 +289,7 @@ data srv3_host: ComputeHost = ComputeHost { } -data srv4_memory_population_observation_note: String = "srv4 BMC 192.168.1.195 Redfish observation 2026-08-22T19:5xZ, taken through the rotated credential in Secret Manager (bmc-srv4-admin) -- the authenticated read this host's deferral named as its dissolution condition, so that scaffold is RETIRED by this row rather than carried forward. MemorySummary TotalSystemMemoryGiB=512; per-DIMM dimm0..dimm7 ALL M393A8G40D40-CRB CapacityMiB=65536 OperatingSpeedMhz=2133 RankCount=2 Manufacturer=Samsung, eight distinct serials, banks DDR4_A1 through H1, every module State=Enabled Health=OK and system HealthRollup=OK.\n\nTHE DEFERRAL'S OWN INSTRUCTION SAID TO DECODE AGAINST THE SK HYNIX CATALOG AND THAT INSTRUCTION IS SUPERSEDED, which is worth saying because following it literally would have produced a wrong row. It was written when the expected finding was srv1's uniform Hynix population; what is actually installed is a Samsung part that had no catalog row at all until 2026-08-22. The deferral was right that srv1's population must not be assumed, and wrong about which catalog the answer would come from.\n\nONE CORRECTABLE ECC EVENT IS ON RECORD FOR THIS POPULATION, logged 2026-08-22T19:45:57Z on Socket 0 / Channel 0 / DIMM 0 (bank 13, row 166, column 96), about three minutes after an unclean restart following a power blackout. It was corrected by ECC and no uncorrectable event accompanied it. It is recorded here rather than left in the BMC log because it is the only memory event this population has produced and because a repeat at the same bank/row/column would distinguish a marginal device from a single upset -- see gunbc.host_memory_qualification for the qualification standing this does not by itself change." +data srv4_memory_population_observation_note: String = "srv4 BMC 192.168.1.195 Redfish observation 2026-08-22, taken between 19:46Z and 20:15Z (the exact minute was not recorded at read time and is NOT reconstructed here -- the window is bounded below by the 19:45:57Z correctable-ECC entry this session read first and above by the srv3 read at 20:15:38Z). srv3 carries a precise timestamp because its read was taken against a live boot transition and the clock mattered; this one was not, and a fabricated second would be worth less than an honest window. Taken through the rotated credential in Secret Manager (bmc-srv4-admin) -- the authenticated read this host's deferral named as its dissolution condition, so that scaffold is RETIRED by this row rather than carried forward. MemorySummary TotalSystemMemoryGiB=512; per-DIMM dimm0..dimm7 ALL M393A8G40D40-CRB CapacityMiB=65536 OperatingSpeedMhz=2133 RankCount=2 Manufacturer=Samsung, eight distinct serials, banks DDR4_A1 through H1, every module State=Enabled Health=OK and system HealthRollup=OK.\n\nTHE DEFERRAL'S OWN INSTRUCTION SAID TO DECODE AGAINST THE SK HYNIX CATALOG AND THAT INSTRUCTION IS SUPERSEDED, which is worth saying because following it literally would have produced a wrong row. It was written when the expected finding was srv1's uniform Hynix population; what is actually installed is a Samsung part that had no catalog row at all until 2026-08-22. The deferral was right that srv1's population must not be assumed, and wrong about which catalog the answer would come from.\n\nONE CORRECTABLE ECC EVENT IS ON RECORD FOR THIS POPULATION, logged 2026-08-22T19:45:57Z on Socket 0 / Channel 0 / DIMM 0 (bank 13, row 166, column 96), about three minutes after an unclean restart following a power blackout. It was corrected by ECC and no uncorrectable event accompanied it. It is recorded here rather than left in the BMC log because it is the only memory event this population has produced and because a repeat at the same bank/row/column would distinguish a marginal device from a single upset -- see gunbc.host_memory_qualification for the qualification standing this does not by itself change." data srv4_memory_population: HostMemoryPopulation = HostMemoryPopulation { rows: [ diff --git a/dag/gunbc/fleet_physical_inventory.dag b/dag/gunbc/fleet_physical_inventory.dag index 33a1bd55a1d..cc28cd35973 100644 --- a/dag/gunbc/fleet_physical_inventory.dag +++ b/dag/gunbc/fleet_physical_inventory.dag @@ -313,8 +313,23 @@ fn fleet_nominal_rackmount_arithmetic_holds() -> Bool { // nothing and would have made this divergence invisible. // --------------------------------------------------------------------------- +// TWO SRV1 ROWS HAD TO BE EDITED TO MOVE ONE FACT, AND THAT IS A REPORTED DEFECT RATHER THAN A +// REPAIRED ONE (2026-08-22). This list and the inline expectations inside fleet_dimm_verdicts +// below are byte-identical copies of the same four expectations, and this list has NO consumer +// anywhere in the corpus -- a grep for its name returns only this declaration. So the live +// reconcile reads the copies, the copies drift independently, and the 2026-08-22 srv1 upgrade +// was landed against the verdict copies while this one kept naming the Hynix part. Review caught +// it; the closure compile could not, because a stale-but-well-typed catalog reference is a data +// disagreement rather than a type error. +// +// NOT DISSOLVED HERE, DELIBERATELY. The construction fix is to derive the verdicts FROM this list +// so srv1 has one row and the drift has no representation (DESIGN 5). That is the right change +// and it is not this one: the module uses no map or pipeline idiom anywhere, so deriving would +// mean introducing one on judgement, and an unconsumed declaration in this corpus may still be +// read by a lens over the Node tree, which a name grep cannot rule out. Both questions want an +// answer before the fork is removed, and neither is answerable from inside this diff. data fleet_dimm_expectations: List = [ - HostDimmExpectation { host: operator_host_srv1, catalog: hma82gr7afr4n_vk_catalog, stick_count: 8 }, + HostDimmExpectation { host: operator_host_srv1, catalog: m393a8g40d40_crb0q_catalog, stick_count: 8 }, HostDimmExpectation { host: operator_host_srv2, catalog: hma82gr7afr4n_vk_catalog, stick_count: 8 }, HostDimmExpectation { host: operator_host_srv3, catalog: m393a8g40d40_crb0q_catalog, stick_count: 8 }, HostDimmExpectation { host: operator_host_srv4, catalog: m393a8g40d40_crb0q_catalog, stick_count: 8 }, @@ -342,7 +357,7 @@ data srv4_dimm_observation: HostDimmObservation = DimmPopulationObserved { data fleet_dimm_verdicts: List = [ dimm_reconcile_verdict( - expectation: HostDimmExpectation { host: operator_host_srv1, catalog: hma82gr7afr4n_vk_catalog, stick_count: 8 }, + expectation: HostDimmExpectation { host: operator_host_srv1, catalog: m393a8g40d40_crb0q_catalog, stick_count: 8 }, observation: srv1_dimm_observation, ), dimm_reconcile_verdict( diff --git a/dag/test/parsecheck.dag b/dag/test/parsecheck.dag new file mode 100644 index 00000000000..67954a9025b --- /dev/null +++ b/dag/test/parsecheck.dag @@ -0,0 +1,14 @@ +module test.parsecheck +import std.types { Bool } +import extdeps.memory.samsung { m393a8g40d40_crb0q_catalog } +import extdeps.memory.cisco_ucs { ucs_mr_1x648ru_a } +import gunbc.fleet_intent { srv1_memory_population, srv3_memory_population, srv4_memory_population } +import gunbc.fleet_physical_inventory { fleet_dimm_verdicts, fleet_dimm_expectations } +import gunbc.host_memory_qualification { srv2_failed_64gib_population_standing } +import gunbc.ci_floor_measurement { gunbc_ci_srv3_memtotal_measured } +fn parsecheck_holds() -> Bool { + ucs_mr_1x648ru_a.underlying_module.rank_count == 8 + && fleet_dimm_verdicts.length() == 4 + && fleet_dimm_expectations.length() == 4 + && srv1_memory_population.rows.length() == 1 +} From 51b12a8e433b7552c7aa0ff8e6267ad0e3d46c77 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 22 Aug 2026 23:34:50 +0000 Subject: [PATCH 3/5] The lot's read obligation is discharged by this PR, so stop reciting it as open Three authority notes in this branch described a world that this branch itself had already changed. A note that contradicts the row beside it is worse than a missing note: the next reader takes the prose, because prose is what reads like an explanation. fleet_intent's nominal-vs-usable note still said srv1 and srv2 "still carry 8 x 16 GiB Hynix" and that "no MemTotal read exists for any host in this fleet". Both were falsified by rows in the same commit. Corrected, and while correcting it the srv1 evidence class is now stated explicitly: srv1 is operator-relayed at population grain with no independent read, its row shape is identical to the two measured hosts', and therefore nothing downstream can tell them apart. That is a real rung gap, named where someone will see it rather than left to be inferred. The 64 GiB lot carried CatalogRowUnread whose read_obligation said, in full: read the part number off the delivered sticks, author the cited DramModuleCatalogRow, then replace this arm with CatalogRowExact naming that row. This PR is exactly what does all three. So the arm is now CatalogRowExact citing extdeps.memory.samsung m393a8g40d40_crb0q_catalog. CatalogRowExact means "cited", not "resolved" -- product.inventory says so itself -- so the symbol was checked against the tree by hand. The witness that asserted the lot was UNREAD is inverted in place, not deleted (DESIGN 4b(4)): the evidence stays enrolled and now guards the other direction, so dropping the citation back to an unread family string goes red. It is discriminating by construction -- the same predicate, lot_catalog_is_read, that the old claim asserted false now asserts true. WHAT IS DELIBERATELY NOT AUTHORED, because it would be invention: the LotReceived and QuantityInstalled events. QuantityInstalled needs a PhysicalAssetIdentity per stick; the Redfish reads observed eight distinct serials per host and this session did not record them, so authoring the event means minting identities for physical objects whose real identifiers exist and were not captured. And srv2's eight sticks have no established disposition -- a host failing memory training does not make its modules defective, so available-spare vs quarantined is an operator judgment about parts nobody has retested. Both are stated in-file with a dissolve-on. The balance witness is re-anchored rather than left alone: it still passes, but its comment claimed nothing had arrived, which is now false. It now says what it actually measures -- the ledger's declared lag behind the fleet -- and that reading it as evidence about physical installation is authority substitution. Verified green by execution: parsecheck_holds returns true with both lot witnesses folded into it. Co-Authored-By: Claude Opus 5 (1M context) --- dag/gunbc/fleet_intent.dag | 2 +- dag/gunbc/fleet_physical_inventory.dag | 72 ++++++++++++------- .../installed_bom_reconcile_witness_test.dag | 44 ++++++++---- dag/test/parsecheck.dag | 6 ++ 4 files changed, 87 insertions(+), 37 deletions(-) diff --git a/dag/gunbc/fleet_intent.dag b/dag/gunbc/fleet_intent.dag index 0ed1b2eeb59..13bdad44704 100644 --- a/dag/gunbc/fleet_intent.dag +++ b/dag/gunbc/fleet_intent.dag @@ -228,7 +228,7 @@ data srv4_nvme0: StorageDevice = nvme_storage_device( persistence: Persistent, ) -data fleet_host_memory_nominal_vs_usable_note: String = "Two DISTINCT memory facts for fleet hosts, must not be conflated: (1) NOMINAL DIMM population — every host's memory derives from per-DIMM BMC Redfish observations through HostMemoryPopulation rows (module x stick_count). srv1/srv2 observed 2026-07-16 and still carry 8 x 16 GiB Hynix; srv3/srv4 observed 2026-08-22 at 8 x 64 GiB Samsung (512 GiB each), which retired srv4's deferral scaffold and superseded srv3's 7+1 mixed row. The fleet is HETEROGENEOUS as of that date. (2) OS-USABLE budget — the MemTotal-shaped CI runner budget authority, which is a SEPARATE fact with its own provenance requirement.\n\nTHE UPGRADE MAKES THE SPLIT LOAD-BEARING RATHER THAN PEDANTIC, so it is restated here in the direction the mistake would now be made. The temptation before was to write 128 GiB nominal over a 125 GiB usable figure, a 3 GiB error. The temptation NOW is to write 512 GiB over it, a 387 GiB error, on the two hosts where a conservation wall would spend it. A management controller reports what is installed; only the kernel reports what is usable after firmware and kernel reservations. No MemTotal read exists for any host in this fleet, so gunbc.ci_floor_measurement gunbc_ci_host_usable_ram_for still carries a conservative lower bound on all four — sound, and now very loose on srv3/srv4. It is dissolved by one ordinary /proc/meminfo read per host and by nothing that can be reached over Redfish." +data fleet_host_memory_nominal_vs_usable_note: String = "Two DISTINCT memory facts for fleet hosts, must not be conflated: (1) NOMINAL DIMM population — every host's memory derives from per-DIMM BMC Redfish observations through HostMemoryPopulation rows (module x stick_count). srv1, srv3 and srv4 carry 8 x 64 GiB Samsung (512 GiB each) as of 2026-08-22; srv2 alone still carries 8 x 16 GiB Hynix from its 2026-07-16 observation, because its 64 GiB install failed memory training and was reverted (see gunbc.host_memory_qualification). The srv3/srv4 rows are authenticated Redfish reads taken 2026-08-22; srv1's is operator-relayed at the population grain with no independent read, a WEAKER evidence class carried in prose only -- the row's shape is identical to the measured hosts', so nothing downstream can tell them apart. The fleet is HETEROGENEOUS as of that date, and srv2 must not inherit any widened commitment derived from the other three. (2) OS-USABLE budget — the MemTotal-shaped CI runner budget authority, which is a SEPARATE fact with its own provenance requirement.\n\nTHE UPGRADE MAKES THE SPLIT LOAD-BEARING RATHER THAN PEDANTIC, so it is restated here in the direction the mistake would now be made. The temptation before was to write 128 GiB nominal over a 125 GiB usable figure, a 3 GiB error. The temptation NOW is to write 512 GiB over it, a 387 GiB error, on the two hosts where a conservation wall would spend it. A management controller reports what is installed; only the kernel reports what is usable after firmware and kernel reservations. srv3 and srv4 now carry MEASURED current-boot MemTotal in gunbc.ci_floor_measurement (about 502.25 GiB each, read over SSH 2026-08-22); srv1 and srv2 still carry a conservative lower bound there, because no /proc/meminfo read has been taken on either. THE 512-VERSUS-502 GAP IS THE WHOLE POINT OF THE SPLIT: about 10 GiB per host disappears between what the management controller reports installed and what the kernel reports usable, and a wall spending nominal would overcommit by that much on every upgraded host. The remaining bound is dissolved by one ordinary /proc/meminfo read on srv1 and srv2 and by nothing that can be reached over Redfish." data srv1_memory_population_observation_2026_07_16_note: String = "srv1 BMC 192.168.1.183 Redfish observation 2026-07-16 (rotated cred, operator-supplied): MemorySummary TotalSystemMemoryGiB=128; per-DIMM dimm0..dimm7 all HMA82GR7AFR4N-VK RankCount=1 DataWidthBits=64 BusWidthBits=72 CapacityMiB=16384 OperatingSpeedMhz=2666 (×8). Uniform 8-stick population of the existing cited row hma82gr7afr4n_vk_catalog (AFR4N=x4 1R) totals 128 GiB — dissolves the gibibyte(128) placeholder." diff --git a/dag/gunbc/fleet_physical_inventory.dag b/dag/gunbc/fleet_physical_inventory.dag index cc28cd35973..e134f8b3988 100644 --- a/dag/gunbc/fleet_physical_inventory.dag +++ b/dag/gunbc/fleet_physical_inventory.dag @@ -40,7 +40,7 @@ import gunbc.fleet_intent { srv3_baseboard, srv4_baseboard, srv4_memory_populati import product.cooling_qualification { InstalledCoolingRealization } import std.nat { Nat } import product.inventory { - CatalogRowUnread, + CatalogRowExact, InventoryEvent, InventoryLotAllocator, InventoryLotIdentity, @@ -416,28 +416,49 @@ data fleet_processor_verdicts: List = [ ] // --------------------------------------------------------------------------- -// THE 64 GiB DIMM LOT: thirty-two sticks, in transit, part number unread. +// THE 64 GiB DIMM LOT: thirty-two sticks, delivered, part number read. // -// The lot goes on the ledger before anybody has read its part number, because -// the supply commitment is real now and a planner that could not see it would -// keep treating the current populations as the fleet's memory ceiling. What -// the lot does NOT do is claim anything nobody has established: the catalog -// identity is CatalogRowUnread with the read obligation stated, the landed -// cost is LandedCostUnsettled because the lot has not settled, and the receipt -// is ReceiptHeldPrivately per the operator's 2026-08-19 ruling that purchase -// provenance and money are private-tree facts. No price and no order identity -// appear here, and after the landed-cost split in product.inventory there is -// no field for either to hide in. +// The lot went on the ledger before anybody had read its part number, because +// the supply commitment was real then and a planner that could not see it would +// have kept treating the old populations as the fleet's memory ceiling. THE READ +// OBLIGATION IS NOW DISCHARGED: the sticks arrived, the label was read, and the +// cited catalog row exists, so the catalog identity is CatalogRowExact naming +// extdeps.memory.samsung m393a8g40d40_crb0q_catalog. What the lot still does NOT +// claim is anything nobody has established: the landed cost is LandedCostUnsettled +// because the lot has not settled, and the receipt is ReceiptHeldPrivately per the +// operator's 2026-08-19 ruling that purchase provenance and money are private-tree +// facts. No price and no order identity appear here, and after the landed-cost +// split in product.inventory there is no field for either to hide in. // -// THE LEDGER HAS EXACTLY ONE EVENT, AND THE MISSING ONES ARE THE POINT. The -// intended split is eight sticks per host, but a reservation in this ledger -// moves stock out of Available, and nothing is Available: thirty-two units sit -// in AwaitingReceipt until a LotReceived and a QuantityQualified say otherwise. -// So authoring four QuantityReserved events today would be refused by the -// ledger - correctly, because they would assert that stock on hand had been -// allocated when the stock is on a truck. The per-host figures are therefore -// carried as an INTENT below, which is what they actually are, and they become -// reservations through ordinary ledger events when the sticks arrive. +// CatalogRowExact MEANS 'CITED', NOT 'RESOLVED' -- see product.inventory +// catalog_ref_resolution_is_unchecked_note. The DeclarationRef below was checked +// against the tree by hand when it was authored; nothing in the substrate checks +// it, and that stays true until feature:cited-symbol-resolution lands. +// +// THE LEDGER IS NOW BEHIND PHYSICAL REALITY, AND THAT GAP IS DECLARED RATHER +// THAN GUESSED. It still holds exactly one event, LotAcquired, so it reports +// thirty-two units AwaitingReceipt. What actually happened: all thirty-two +// arrived, eight are installed in each of srv1, srv3 and srv4, and srv2's eight +// were installed, failed memory training, and were removed. So the true event +// sequence is a LotReceived, a QuantityQualified, three QuantityInstalled and a +// QuantityRemoved. +// +// THOSE EVENTS ARE NOT AUTHORED HERE, for two reasons that are obligations and +// not preferences. QuantityInstalled requires a PhysicalAssetIdentity per stick; +// the Redfish reads observed eight distinct serials per host but this session did +// not record them, so authoring the event would mean minting identities for +// physical objects whose real identifiers exist and were not captured -- inventing +// what could have been read (DESIGN section 5). And srv2's eight sticks have no +// established disposition: a host that fails training does not make its modules +// defective, so whether they are available spare or quarantined-for-srv2 is an +// operator judgment about parts nobody has retested, not something to infer from +// the host's failure. QuantityQualified's split depends on that same answer. +// +// DISSOLVE-ON: one Redfish read per upgraded host capturing per-DIMM SerialNumber, +// plus an operator disposition for srv2's eight. Until then the per-host figures +// stay an INTENT below, which is what they still are -- the intent was met for +// three hosts and not the fourth, and the ledger says so by being silent rather +// than by asserting a reservation nobody can back. // --------------------------------------------------------------------------- data fleet_lot_allocation_seed: InventoryLotAllocator = inventory_lot_allocator_initial() @@ -449,9 +470,12 @@ data fleet_lot_allocator_after_dimm_lot: InventoryLotAllocator = mint_inventory_ data dimm_lot_64gib_32x: ProcurementLot = ProcurementLot { identity: dimm_lot_64gib_32x_identity, receipt: ReceiptHeldPrivately, - catalog: CatalogRowUnread { - observed_family: "64 GiB DDR4 DIMM, exact vendor and part unread" as NonEmptyStr, - read_obligation: "read the manufacturer and exact part number off the delivered sticks or the order confirmation, author the cited DramModuleCatalogRow in extdeps.memory against the manufacturer datasheet with the part number decomposed onto chip_width, rank_count and buffering, then replace this arm with CatalogRowExact naming that row" as NonEmptyStr, + catalog: CatalogRowExact { + row: DeclarationRef { + module_path: "extdeps.memory.samsung", + decl_name: "m393a8g40d40_crb0q_catalog", + field: WholeDeclaration, + }, }, display_label: "64 GiB DIMM lot, 32 sticks, fleet memory uplift" as NonEmptyStr, quantity_acquired: 32, diff --git a/dag/test/claim/installed_bom_reconcile_witness_test.dag b/dag/test/claim/installed_bom_reconcile_witness_test.dag index 6748d0b1fd6..1f524ec8b37 100644 --- a/dag/test/claim/installed_bom_reconcile_witness_test.dag +++ b/dag/test/claim/installed_bom_reconcile_witness_test.dag @@ -55,6 +55,7 @@ import product.inventory { ReservationOverRelease, ZeroQuantityEvent, derive_inventory_balance, + lot_catalog_exact_row, lot_catalog_is_read, lot_catalog_read_obligation, lot_landed_cost_reading, @@ -415,29 +416,48 @@ test fn every_fleet_processor_verdict_is_unconfirmed_today() -> Bool { // --- the 64 GiB lot on the ledger -------------------------------------------------------------- -// THE LOT IS COMMITTED, UNREAD, AND UNSETTLED, and each of those is asserted by constructor rather -// than inferred from a total. A lot that reported a read catalog, or a recorded cost, would be -// claiming facts nobody has - and the read obligation is what makes the missing part number -// countable instead of merely absent. -test fn the_dimm_lot_is_committed_with_an_unread_catalog_and_no_public_cost() -> Bool { +// THE LOT IS COMMITTED, READ, AND STILL UNSETTLED, and each of those is asserted by constructor +// rather than inferred from a total. This claim INVERTED on 2026-08-22: it previously asserted the +// catalog was UNREAD and carried a standing read obligation, and it went green by the obligation +// being discharged - the sticks arrived, the label was read, and extdeps.memory.samsung +// m393a8g40d40_crb0q_catalog was authored against the manufacturer's part number. Per DESIGN +// section 4b(4) the claim is INVERTED IN PLACE rather than deleted: it now guards the other +// direction, so a regression that dropped the citation back to an unread family string goes red +// here instead of passing unnoticed. The cost and receipt halves did not move - a lot that reported +// a recorded cost would still be claiming facts nobody has. +test fn the_dimm_lot_is_committed_with_a_read_catalog_and_no_public_cost() -> Bool { let quantity = dimm_lot_64gib_32x.quantity_acquired == 32 - let unread = !lot_catalog_is_read(catalog: dimm_lot_64gib_32x.catalog) - let obligation = match lot_catalog_read_obligation(catalog: dimm_lot_64gib_32x.catalog) { - Present { value: _ } => true + let read = lot_catalog_is_read(catalog: dimm_lot_64gib_32x.catalog) + let cited = match lot_catalog_exact_row(catalog: dimm_lot_64gib_32x.catalog) { + Present { value: r } => r.module_path == "extdeps.memory.samsung" + && r.decl_name == "m393a8g40d40_crb0q_catalog" Absent => false } + let no_obligation = match lot_catalog_read_obligation(catalog: dimm_lot_64gib_32x.catalog) { + Present { value: _ } => false + Absent => true + } let no_public_cost = match lot_landed_cost_reading(lot: dimm_lot_64gib_32x) { LandedCostReadingUnsettled => true LandedCostReadingMicros { micros: _ } => false LandedCostReadingHeldPrivately => false } let no_public_receipt = !lot_receipt_is_recorded(lot: dimm_lot_64gib_32x) - quantity && unread && obligation && no_public_cost && no_public_receipt + quantity && read && cited && no_obligation && no_public_cost && no_public_receipt } -// EVERY STICK IS AWAITING RECEIPT AND NONE IS RESERVED. The intent says eight per host; the ledger -// says nothing is allocated, because nothing has arrived. Asserting both in one claim is what keeps -// the intent from being read as a holding. +// THE LEDGER STILL REPORTS EVERY STICK AWAITING RECEIPT, AND THAT IS NOW A LAG, NOT THE WORLD. +// The sticks arrived: twenty-four are installed across srv1/srv3/srv4 and srv2's eight were +// installed, failed training and were removed. The ledger has not been advanced because the +// receipt events need per-stick PhysicalAssetIdentity that nobody captured, and because srv2's +// eight have no established disposition - both stated as an obligation in +// gunbc.fleet_physical_inventory beside the lot. +// +// SO THIS CLAIM MEASURES THE LEDGER, NOT THE FLEET, and it is kept rather than deleted precisely +// because it makes the lag countable: it goes red the moment the events land, which is the signal +// to re-read this comment and retire it. Reading it as evidence that nothing has arrived is the +// authority-substitution failure DESIGN warns about - the ledger is the authority for allocation, +// never for what is physically installed, and the installed answer lives in fleet_dimm_verdicts. test fn the_dimm_lot_holds_all_thirty_two_sticks_awaiting_receipt() -> Bool { match derive_inventory_balance(lot: dimm_lot_64gib_32x, events: dimm_lot_64gib_32x_ledger) { BalanceRefused { cause: _, event_ordinal: _, event_label: _ } => false diff --git a/dag/test/parsecheck.dag b/dag/test/parsecheck.dag index 67954a9025b..2c94df72cdb 100644 --- a/dag/test/parsecheck.dag +++ b/dag/test/parsecheck.dag @@ -6,9 +6,15 @@ import gunbc.fleet_intent { srv1_memory_population, srv3_memory_population, srv4 import gunbc.fleet_physical_inventory { fleet_dimm_verdicts, fleet_dimm_expectations } import gunbc.host_memory_qualification { srv2_failed_64gib_population_standing } import gunbc.ci_floor_measurement { gunbc_ci_srv3_memtotal_measured } +import test.claim.installed_bom_reconcile_witness_test { + the_dimm_lot_is_committed_with_a_read_catalog_and_no_public_cost, + the_dimm_lot_holds_all_thirty_two_sticks_awaiting_receipt, +} fn parsecheck_holds() -> Bool { ucs_mr_1x648ru_a.underlying_module.rank_count == 8 && fleet_dimm_verdicts.length() == 4 && fleet_dimm_expectations.length() == 4 && srv1_memory_population.rows.length() == 1 + && the_dimm_lot_is_committed_with_a_read_catalog_and_no_public_cost() + && the_dimm_lot_holds_all_thirty_two_sticks_awaiting_receipt() } From 87255a8d43a3faf5158f32f71c711a43826dfb99 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 22 Aug 2026 23:55:44 +0000 Subject: [PATCH 4/5] The note claiming no consumer was falsified by my own later edit, and the drift guard it invites cannot be written review 54874 caught the sentence "a grep for its name returns only this declaration" as false: dag/test/parsecheck.dag imports fleet_dimm_expectations. The claim was true when written and my own later edit falsified it -- the same premise-contamination class this branch already corrected three instances of, arrived at from a new direction. It now says what is actually true and load-bearing: no PRODUCTION consumer reads the list, which is what makes the copies drift. The review offered a second option, promoting parsecheck to a per-row equivalence check. CHECKING IT FIRST SHOWED IT CANNOT BE WRITTEN, and that is worth more than the fix would have been: dimm_reconcile_verdict CONSUMES its expectation, and DimmReconcileVerdict retains only host, counts and discrepancies, so the inline expectation is not recoverable from fleet_dimm_verdicts by any reader. There is nothing to compare against. Validation here is not merely weaker than construction, it is unavailable -- which is the strongest argument yet for the derive-from-the-list fix, so the finding is recorded rather than worked around. A third obstacle to that construction fix is named while it is fresh, because it is the one that decides the shape rather than the effort. The join needs an arm for a host with no matching observation, and the two arms already present are both wrong: DimmObservationAbsent says an observation was sought and the host has none, whereas a lookup that found no row says the join could not be performed. Different owners, opposite repairs -- the not-applicable-versus-malformed conflation DESIGN names, which is exactly what an arm downstream of a lookup returning Absent invites. So the join wants a new typed arm on the product-layer type, not a mechanical rewrite of this module. Also corrects the block header, which still described a uniform SK Hynix expectation refuted on srv3 by a 7+1 mixed population. True of the 2026-07-16 reads; the 2026-08-22 upgrade replaced that population outright. Verified green by execution: parsecheck_holds returns true. Co-Authored-By: Claude Opus 5 (1M context) --- dag/gunbc/fleet_physical_inventory.dag | 66 +++++++++++++++++--------- 1 file changed, 44 insertions(+), 22 deletions(-) diff --git a/dag/gunbc/fleet_physical_inventory.dag b/dag/gunbc/fleet_physical_inventory.dag index e134f8b3988..c23e3cc802a 100644 --- a/dag/gunbc/fleet_physical_inventory.dag +++ b/dag/gunbc/fleet_physical_inventory.dag @@ -296,38 +296,60 @@ fn fleet_nominal_rackmount_arithmetic_holds() -> Bool { // INSTALLED DIMM AND PROCESSOR BILLS OF MATERIALS: what is expected, what has // actually been observed, and the refusal between them. // -// The expectation below is the operator's stated belief that all four hosts -// carry an eight-stick population of the SK Hynix part already cited in -// extdeps.memory.sk_hynix. It is authored as an expectation and nothing else: -// no PhysicalAsset row binds an installed DIMM here, because binding an asset -// would assert that somebody read a part number off a slot, and for the -// per-slot grain nobody has. +// The expectations below are the operator's stated belief about each host's +// population, and they are NO LONGER UNIFORM: srv1, srv3 and srv4 expect the +// eight-stick Samsung population cited in extdeps.memory.samsung, while srv2 +// alone still expects the SK Hynix part, because its 64 GiB install failed +// memory training and was reverted. They are authored as expectations and +// nothing else: no PhysicalAsset row binds an installed DIMM here, because +// binding an asset would assert that somebody read a part number off a slot, +// and for the per-slot grain nobody has. // -// THE EXPECTATION IS ALREADY REFUTED ON ONE HOST, and that is the mechanism -// working rather than an authoring error. srv1 and srv2 confirm it against -// their 2026-07-16 BMC Redfish populations; srv3's population from the same -// read is seven HMA82GR7AFR8N-VK plus one HMA82GR7AFR4N-VK, so the uniform -// expectation reaches DimmPopulationRefused with the exact part difference -// named. The rows stay as authored rather than being quietly edited to match -// srv3, because an expectation rewritten to fit the observation records -// nothing and would have made this divergence invisible. +// THIS BLOCK PREVIOUSLY DESCRIBED A UNIFORM HYNIX EXPECTATION REFUTED ON srv3 +// BY A 7+1 MIXED POPULATION. That was true of the 2026-07-16 reads and is now +// history: the 2026-08-22 upgrade replaced srv3's mixed population outright. +// The description is corrected rather than kept beside the new rows, because +// prose that contradicts the rows under it is what the next reader believes. +// +// The rows are still never edited to match an observation. An expectation +// rewritten to fit what was seen records nothing and makes a divergence +// invisible; when the fleet moved, the expectations moved because the OPERATOR +// changed what is expected, not because the observation disagreed. // --------------------------------------------------------------------------- // TWO SRV1 ROWS HAD TO BE EDITED TO MOVE ONE FACT, AND THAT IS A REPORTED DEFECT RATHER THAN A // REPAIRED ONE (2026-08-22). This list and the inline expectations inside fleet_dimm_verdicts -// below are byte-identical copies of the same four expectations, and this list has NO consumer -// anywhere in the corpus -- a grep for its name returns only this declaration. So the live -// reconcile reads the copies, the copies drift independently, and the 2026-08-22 srv1 upgrade -// was landed against the verdict copies while this one kept naming the Hynix part. Review caught -// it; the closure compile could not, because a stale-but-well-typed catalog reference is a data -// disagreement rather than a type error. +// below are byte-identical copies of the same four expectations, and no PRODUCTION consumer reads +// this list -- the live reconcile reads the inline copies. So the copies drift independently, and +// the 2026-08-22 srv1 upgrade was landed against the verdict copies while this one kept naming the +// Hynix part. Review caught it; the closure compile could not, because a stale-but-well-typed +// catalog reference is a data disagreement rather than a type error. +// +// A DRIFT WITNESS CANNOT BE WRITTEN AGAINST THE VERDICTS, and that is the strongest argument for +// fixing this by construction. The obvious cheap guard -- assert each row here equals the inline +// copy -- has nothing to compare against: dimm_reconcile_verdict CONSUMES its expectation, and +// DimmReconcileVerdict retains only host, counts and discrepancies, so the inline expectation is +// not recoverable from fleet_dimm_verdicts by any reader. Validation is not merely weaker than +// construction here; it is unavailable. // // NOT DISSOLVED HERE, DELIBERATELY. The construction fix is to derive the verdicts FROM this list // so srv1 has one row and the drift has no representation (DESIGN 5). That is the right change // and it is not this one: the module uses no map or pipeline idiom anywhere, so deriving would // mean introducing one on judgement, and an unconsumed declaration in this corpus may still be -// read by a lens over the Node tree, which a name grep cannot rule out. Both questions want an -// answer before the fork is removed, and neither is answerable from inside this diff. +// read by a lens over the Node tree, which a name grep cannot rule out. +// +// AND A THIRD OBSTACLE, WHICH IS THE ONE THAT ACTUALLY DECIDES THE SHAPE: deriving the verdicts +// means joining each expectation to its observation BY HOST, so the join needs an arm for a host +// with no matching observation -- and the two candidate arms already in DimmReconcileVerdict are +// both wrong for it. DimmObservationAbsent says an observation was sought and the host has none; +// a lookup that found no row says the join could not be performed. Those have different owners and +// opposite repairs, and collapsing them is exactly the not-applicable-versus-malformed conflation +// DESIGN names -- an arm downstream of a lookup that returned Absent is not-applicable and needs +// its own reason. So the join wants a new typed arm, which is a modeling decision about the +// product-layer reconcile type and not a mechanical rewrite of this module. +// +// Three questions want an answer before the fork is removed, and none is answerable from inside +// this diff. data fleet_dimm_expectations: List = [ HostDimmExpectation { host: operator_host_srv1, catalog: m393a8g40d40_crb0q_catalog, stick_count: 8 }, HostDimmExpectation { host: operator_host_srv2, catalog: hma82gr7afr4n_vk_catalog, stick_count: 8 }, From 332a92fb7d271f75de06886e64a64cd9116e298d Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 23 Aug 2026 00:22:27 +0000 Subject: [PATCH 5/5] Three qualification receipts were dated four days in the future, and a witness invented srv1's BMC read from the answer under test I checked a claim of future-dated timestamps earlier, found nothing, and said so. The check was wrong: I grepped date STRINGS, and these are EpochMs integers. All three new rows in host_memory_qualification decoded to 2026-08-26 -- right clock time, four days off. Corrected to 08-22. srv4's is now stated for what it is. That read was a bounded window, not an instant, and EpochMs admits only a point, so the row carries the window's LOWER bound (19:45:58Z, the correctable-ECC entry this session read first) with a note saying which bound and why: a consumer computing age from it overestimates elapsed time, never underestimates, which is the safe direction for a staleness question. Fabricating a plausible second to satisfy the carrier is the failure this repository names most often. THE WORST ONE IS THE WITNESS. srv1_bmc_observed_total_gib named a Redfish observation that does not exist -- srv1's upgrade is operator-relayed, as production says in the row's own note -- and the claim fed that 512 GiB through redfish_memory_summary_from_gib and asserted the population matched it. That proves 512 == 512: the answer under test retyped as a receipt, committed inside the witness that exists to catch exactly this. It is now srv1_operator_relayed_total_gib, the claim is split so srv2 (which HAS a BMC read) keeps a real reconcile, and srv1's is named srv1_population_matches_the_operator_relayed_total and deliberately does NOT route through the Redfish shaper -- it is a transcription check and says so. Two adjacent controls repaired. The seven-stick red constructed seven HYNIX sticks against srv1's now-Samsung eight, varying part and count at once, so it could pass on either difference and no longer isolated the count it claims to discriminate; it now holds the module fixed. And the fleet-partition claim omitted srv1 entirely, so srv1 could have drifted to any total -- including back to 128 GiB -- with the claim still green. That is the same drift review 54843 caught by hand, left undetectable in the witness beside it. It now pins srv1 == srv3 == srv4 != srv2. The lot ledger no longer models delivered hardware as awaiting receipt. LotReceived{32} is authored: the sticks demonstrably arrived, and that event needs no per-stick asset identity. Installation and qualification stay unrecorded for the reasons already stated in-file, so the balance reports 32 received and wholly unqualified -- conservative and true, since no stick carries a qualification event whatever three hosts are doing with them. The witness that asserted received == 0 is renamed and re-aimed; it had made a known-false state a condition of staying green, and annotating a false state does not make it acceptable. It is also dropped from parsecheck, where it had become an acceptance condition rather than evidence. Two more stale authority notes corrected, both present-tense beside the capacity ceiling the conservation wall consumes: gunbc_ci_host_usable_ram_kind_note and ci_runner_placement's host_usable_ram_note each still said srv1 was Hynix, that no MemTotal read existed for any host, and that all four rows were bounds -- while the same module defines the measured srv3/srv4 rows. Verified green by execution: parsecheck_holds returns true. Co-Authored-By: Claude Opus 5 (1M context) --- dag/gunbc/ci_floor_measurement.dag | 2 +- dag/gunbc/ci_runner_placement.dag | 2 +- dag/gunbc/fleet_physical_inventory.dag | 17 ++++--- dag/gunbc/host_memory_qualification.dag | 24 +++++---- .../fleet_intent_memory_witness_test.dag | 51 +++++++++++++++---- .../installed_bom_reconcile_witness_test.dag | 29 ++++++----- dag/test/parsecheck.dag | 2 - 7 files changed, 85 insertions(+), 42 deletions(-) diff --git a/dag/gunbc/ci_floor_measurement.dag b/dag/gunbc/ci_floor_measurement.dag index fa0c1382f82..3a57e688161 100644 --- a/dag/gunbc/ci_floor_measurement.dag +++ b/dag/gunbc/ci_floor_measurement.dag @@ -284,7 +284,7 @@ type HostUsableRam | HostUsableRamConservativeLowerBound { bytes: ByteSize, basis: NonEmptyStr } | HostUsableRamUnmeasured -data gunbc_ci_host_usable_ram_kind_note: String = "OS-USABLE RAM IS A PER-HOST FACT AND WAS STORED AS A FLEET CONSTANT, which is the same grain defect gunbc_ci_host_fixed_overhead_kind_note repaired for overhead -- so this carrier is deliberately that carrier's shape rather than a new invention.\n\nTHE DIMM-REPLACEMENT CLAIM HAS NOW BEEN WRONG IN BOTH DIRECTIONS AND IS SETTLED BY MEASUREMENT. An earlier revision said a 2026-08-11 replacement had raised memory on part of the fleet; that was written from an in-flight operator report before any observation existed, and it was wrong (the attempt failed, operator 2026-08-12). This revision records the opposite and does so from a read rather than a report: srv3 and srv4 were each observed at 512 GiB over BMC Redfish on 2026-08-22 -- 8 x Samsung M393A8G40D40-CRB at 64 GiB, one per channel, all Enabled/OK -- while srv1 and srv2 remain at 8 x 16 GiB Hynix pending their own upgrades. The hosts no longer share one nominal population.\n\nTHE ARMS BELOW DO NOT MOVE, AND THAT IS THE POINT RATHER THAN AN OVERSIGHT. What changed is NOMINAL DIMM capacity, which this carrier does not hold and must never be fed. Every host still carries HostUsableRamConservativeLowerBound at 125 GiB, because no MemTotal read exists for any of them -- including the two just upgraded. A lower bound does not become false when the machine gets bigger; it becomes LOOSE. So the wall stays sound and starts badly under-admitting on two hosts, and the remedy is the one this note already named: one ordinary read per host, taken any time, promoting that host's row to MEASURED and leaving the others untouched.\n\nTHREE ARMS BECAUSE THERE ARE THREE FACTS. MEASURED means a read of THIS host produced the number and the row names the read. CONSERVATIVE LOWER BOUND means no such read exists and the carried figure is known not to exceed the host's real usable RAM, with basis stating why. UNMEASURED is the fail-closed floor for a host nobody classified.\n\nTHE MIDDLE ARM IS A BOUND AND NOT A SUBSTITUTION, and the heterogeneity above is exactly why that distinction was worth paying for in advance. While the fleet was uniform an equivalence argument was also available, and naming the arm for equivalence would have licensed the move the wall cannot survive: carrying a reading from a host with MORE memory onto one with less. That move is now AUTHORABLE for the first time -- srv3 and srv4 are the hosts with more -- and the bound's name is what forbids it. The safety property is monotonicity, and it did not have to be re-argued when the fleet's uniformity ended.\n\nWHY ALL FOUR ARE BOUNDS AND NONE IS MEASURED: no MemTotal read exists for any host in this fleet. The closest receipt is gunbc_ci_srv3_memavailable_high_water, whose host_total is MemTotal-shaped but was captured as an arm-time line from a memory governor rather than a read taken to answer this question, only on srv3, and -- now load-bearing -- against srv3's PREVIOUS 128 GiB population, so it is a receipt about hardware that is no longer in that chassis.\n\nDissolving these is CHEAPER THAN THE FIXED-OVERHEAD ROW BESIDE THEM and must not be confused with it. That row needs a QUIESCENT read because it estimates non-reclaimable residency from MemAvailable, which moves with load. MemTotal does not: the kernel reports total usable RAM after firmware and kernel reservations, so an ordinary read while the host serves work is a complete answer. One read per host, taken any time, promotes that host's row to MEASURED and leaves the others untouched -- which is the entire point of the grain." +data gunbc_ci_host_usable_ram_kind_note: String = "OS-USABLE RAM IS A PER-HOST FACT AND WAS STORED AS A FLEET CONSTANT, which is the same grain defect gunbc_ci_host_fixed_overhead_kind_note repaired for overhead -- so this carrier is deliberately that carrier's shape rather than a new invention.\n\nTHE DIMM-REPLACEMENT CLAIM HAS NOW BEEN WRONG IN BOTH DIRECTIONS AND IS SETTLED BY MEASUREMENT. An earlier revision said a 2026-08-11 replacement had raised memory on part of the fleet; that was written from an in-flight operator report before any observation existed, and it was wrong (the attempt failed, operator 2026-08-12). This revision records the opposite and does so from a read rather than a report: srv3 and srv4 were each observed at 512 GiB over BMC Redfish on 2026-08-22 -- 8 x Samsung M393A8G40D40-CRB at 64 GiB, one per channel, all Enabled/OK -- while srv1 was upgraded to the same 8 x Samsung population on operator report and srv2's identical attempt FAILED memory training and was reverted to 8 x 16 GiB Hynix. The hosts no longer share one nominal population.\n\nTWO ARMS HAVE NOW MOVED AND TWO HAVE NOT, WHICH IS THE GRAIN DOING ITS JOB. srv3 and srv4 carry HostUsableRamMeasured from /proc/meminfo reads taken over SSH on 2026-08-22 (about 502.25 GiB each); srv1 and srv2 still carry HostUsableRamConservativeLowerBound at 125 GiB, because no MemTotal read has been taken on either. What promoted the two was a KERNEL read, never the Redfish 512 GiB figure -- that is NOMINAL DIMM capacity, which this carrier does not hold and must never be fed. A lower bound does not become false when the machine gets bigger; it becomes LOOSE, and srv1's is now loose by roughly 4x while remaining sound. The remedy is unchanged and is now half-applied: one ordinary read per host, taken any time, promoting that host's row and leaving the others untouched.\n\nTHREE ARMS BECAUSE THERE ARE THREE FACTS. MEASURED means a read of THIS host produced the number and the row names the read. CONSERVATIVE LOWER BOUND means no such read exists and the carried figure is known not to exceed the host's real usable RAM, with basis stating why. UNMEASURED is the fail-closed floor for a host nobody classified.\n\nTHE MIDDLE ARM IS A BOUND AND NOT A SUBSTITUTION, and the heterogeneity above is exactly why that distinction was worth paying for in advance. While the fleet was uniform an equivalence argument was also available, and naming the arm for equivalence would have licensed the move the wall cannot survive: carrying a reading from a host with MORE memory onto one with less. That move is now AUTHORABLE for the first time -- srv3 and srv4 are the hosts with more -- and the bound's name is what forbids it. The safety property is monotonicity, and it did not have to be re-argued when the fleet's uniformity ended.\n\nWHY srv1 AND srv2 ARE STILL BOUNDS: no MemTotal read has been taken on either. A NEARBY RECEIPT IS NOT ONE, and it is named because it looks like one: gunbc_ci_srv3_memavailable_high_water, whose host_total is MemTotal-shaped but was captured as an arm-time line from a memory governor rather than a read taken to answer this question, only on srv3, and -- now load-bearing -- against srv3's PREVIOUS 128 GiB population, so it is a receipt about hardware that is no longer in that chassis.\n\nDissolving these is CHEAPER THAN THE FIXED-OVERHEAD ROW BESIDE THEM and must not be confused with it. That row needs a QUIESCENT read because it estimates non-reclaimable residency from MemAvailable, which moves with load. MemTotal does not: the kernel reports total usable RAM after firmware and kernel reservations, so an ordinary read while the host serves work is a complete answer. One read per host, taken any time, promotes that host's row to MEASURED and leaves the others untouched -- which is the entire point of the grain." data gunbc_ci_conservative_lower_bound_usable_ram: HostUsableRam = HostUsableRamConservativeLowerBound { bytes: gunbc_ci_srv3_memavailable_high_water.host_total, diff --git a/dag/gunbc/ci_runner_placement.dag b/dag/gunbc/ci_runner_placement.dag index 92716a07854..cac199c506c 100644 --- a/dag/gunbc/ci_runner_placement.dag +++ b/dag/gunbc/ci_runner_placement.dag @@ -265,7 +265,7 @@ fn host_session_slice_bytes(host: HostIdentity) -> ByteSize { } } -data host_usable_ram_note: String = "CONSERVATION IS CHECKED AGAINST OS-USABLE RAM, NOT THE DIMM TOTAL. compute_host_ram_bytes_total sums the populated modules -- nominal capacity -- while the OS sees less after firmware and kernel reservations, and gunbc.ci_fleet fleet_host_memory_nominal_vs_usable_note exists specifically to say these are two facts that must not be conflated. The margin decides admissions rather than being academic: at the 128 GiB nominal / 125 GiB usable population this fleet carried until 2026-08-22, an eighth 14 GiB slot summed to 125.6 GiB, which PASSED against nominal and FAILED against usable -- so checking the nominal figure would admit a width the machine cannot carry, by spending memory that does not exist.\n\nTHE UNIFORM-POPULATION PREMISE HAS NOW ACTUALLY FALSIFIED, AND THIS PARAGRAPH IS THE THIRD REVISION OF THAT CLAIM -- which is itself the finding. The premise was: every host on the same board at the same population, so one figure stands in for all four. It was declared falsified once on an in-flight report of a DIMM replacement, then RESTORED when that replacement was reported failed (operator, 2026-08-12), with a note saying that marking a true statement historical is the same defect as leaving a false one live. Both of those were correct at the time. Both are now superseded by measurement: srv3 and srv4 were each read at 512 GiB over BMC Redfish on 2026-08-22 (8 x Samsung M393A8G40D40-CRB, one per channel), while srv1 and srv2 remain at 8 x 16 GiB Hynix. The fleet is HETEROGENEOUS as of that date and the premise is dead for the first time in this note's history.\n\nWHAT THAT DOES NOT LICENSE, because it is the move this note has always existed to forbid: the 512 GiB figure is NOMINAL DIMM CAPACITY read from a management controller. It is NOT OS-usable RAM and must not be written into gunbc_ci_host_usable_ram_for. No MemTotal read exists for any host in this fleet, including the two that were just upgraded, so every host's usable-RAM row remains a conservative lower bound and the conservation wall keeps admitting the widths it admitted yesterday. That is SOUND and USELESSLY CONSERVATIVE at the same time -- 125 GiB is still a true lower bound for a 512 GiB host -- and the gap between sound and useful is closed by one ordinary /proc/meminfo read per host, not by promoting a Redfish number.\n\nWHAT THE PER-HOST GRAIN RESTS ON is therefore still not this trigger, and the heterogeneity does not retroactively justify the grain. It is that this wall folded over per-host offers and then read RAM from a synthetic machine outside that fold, and that an unclassified host borrowed rather than refused -- see gunbc.ci_floor_measurement gunbc_ci_host_usable_ram_kind_note. A per-host fact belonged at per-host grain when the hosts were identical; it merely became visible when they stopped being." +data host_usable_ram_note: String = "CONSERVATION IS CHECKED AGAINST OS-USABLE RAM, NOT THE DIMM TOTAL. compute_host_ram_bytes_total sums the populated modules -- nominal capacity -- while the OS sees less after firmware and kernel reservations, and gunbc.ci_fleet fleet_host_memory_nominal_vs_usable_note exists specifically to say these are two facts that must not be conflated. The margin decides admissions rather than being academic: at the 128 GiB nominal / 125 GiB usable population this fleet carried until 2026-08-22, an eighth 14 GiB slot summed to 125.6 GiB, which PASSED against nominal and FAILED against usable -- so checking the nominal figure would admit a width the machine cannot carry, by spending memory that does not exist.\n\nTHE UNIFORM-POPULATION PREMISE HAS NOW ACTUALLY FALSIFIED, AND THIS PARAGRAPH IS THE THIRD REVISION OF THAT CLAIM -- which is itself the finding. The premise was: every host on the same board at the same population, so one figure stands in for all four. It was declared falsified once on an in-flight report of a DIMM replacement, then RESTORED when that replacement was reported failed (operator, 2026-08-12), with a note saying that marking a true statement historical is the same defect as leaving a false one live. Both of those were correct at the time. Both are now superseded by measurement: srv3 and srv4 were each read at 512 GiB over BMC Redfish on 2026-08-22 (8 x Samsung M393A8G40D40-CRB, one per channel), srv1 was upgraded to the same population on operator report, and srv2's identical attempt failed memory training and was reverted to 8 x 16 GiB Hynix. The fleet is HETEROGENEOUS as of that date and the premise is dead for the first time in this note's history.\n\nWHAT THAT DOES NOT LICENSE, because it is the move this note has always existed to forbid: the 512 GiB figure is NOMINAL DIMM CAPACITY read from a management controller. It is NOT OS-usable RAM and must not be written into gunbc_ci_host_usable_ram_for. The gap was closed on two hosts the only way it can be: srv3 and srv4 now carry MEASURED usable RAM from /proc/meminfo reads taken over SSH on 2026-08-22, about 502.25 GiB each -- roughly 10 GiB BELOW their nominal 512, which is exactly the firmware-and-kernel reservation this note exists to preserve. srv1 and srv2 have had no such read, so their rows remain conservative lower bounds and the wall keeps admitting the widths it admitted yesterday on those two. srv1's bound is now SOUND and USELESSLY CONSERVATIVE at the same time -- 125 GiB is still a true lower bound for a 512 GiB host -- and it closes with one ordinary /proc/meminfo read, never by promoting a Redfish number.\n\nWHAT THE PER-HOST GRAIN RESTS ON is therefore still not this trigger, and the heterogeneity does not retroactively justify the grain. It is that this wall folded over per-host offers and then read RAM from a synthetic machine outside that fold, and that an unclassified host borrowed rather than refused -- see gunbc.ci_floor_measurement gunbc_ci_host_usable_ram_kind_note. A per-host fact belonged at per-host grain when the hosts were identical; it merely became visible when they stopped being." // The grain here is per host, and the reason is not that the hosts differ. This wall folds over // per-host offers and charges each host its own overhead and session slice, then read RAM from a diff --git a/dag/gunbc/fleet_physical_inventory.dag b/dag/gunbc/fleet_physical_inventory.dag index c23e3cc802a..001aa918c9a 100644 --- a/dag/gunbc/fleet_physical_inventory.dag +++ b/dag/gunbc/fleet_physical_inventory.dag @@ -457,13 +457,15 @@ data fleet_processor_verdicts: List = [ // against the tree by hand when it was authored; nothing in the substrate checks // it, and that stays true until feature:cited-symbol-resolution lands. // -// THE LEDGER IS NOW BEHIND PHYSICAL REALITY, AND THAT GAP IS DECLARED RATHER -// THAN GUESSED. It still holds exactly one event, LotAcquired, so it reports -// thirty-two units AwaitingReceipt. What actually happened: all thirty-two -// arrived, eight are installed in each of srv1, srv3 and srv4, and srv2's eight -// were installed, failed memory training, and were removed. So the true event -// sequence is a LotReceived, a QuantityQualified, three QuantityInstalled and a -// QuantityRemoved. +// THE LEDGER RECORDS RECEIPT AND STOPS THERE, AND THE REMAINING GAP IS DECLARED +// RATHER THAN GUESSED. All thirty-two sticks arrived, so LotReceived is authored: +// modeling delivered hardware as AwaitingReceipt was a known-false state, and a +// known-false state does not become acceptable by being annotated. What is NOT +// yet recorded is qualification and installation -- eight sticks in each of srv1, +// srv3 and srv4, and srv2's eight installed, failed and removed -- so the balance +// reports thirty-two received and unqualified, which is conservative and true: +// no stick carries a recorded qualification event, whatever three hosts are +// currently doing with them. // // THOSE EVENTS ARE NOT AUTHORED HERE, for two reasons that are obligations and // not preferences. QuantityInstalled requires a PhysicalAssetIdentity per stick; @@ -506,6 +508,7 @@ data dimm_lot_64gib_32x: ProcurementLot = ProcurementLot { data dimm_lot_64gib_32x_ledger: List = [ LotAcquired { lot: dimm_lot_64gib_32x_identity }, + LotReceived { lot: dimm_lot_64gib_32x_identity, quantity: 32 }, ] // The intended destination of the lot, one row per host. This is an INTENT and diff --git a/dag/gunbc/host_memory_qualification.dag b/dag/gunbc/host_memory_qualification.dag index 465de6d8ee2..2d03cb88dad 100644 --- a/dag/gunbc/host_memory_qualification.dag +++ b/dag/gunbc/host_memory_qualification.dag @@ -311,9 +311,13 @@ data altrad8ud_mrep_failure_observation: PlatformTrainingFailure = PlatformTrain // WHY THESE ROWS EXIST AT ALL, given that both hosts are up and serving. The 2026-08-11 incident's // whole lesson was that "the memory works" is four questions, and a successful outcome collapses // them just as easily as a failure did -- more easily, because nobody interrogates a green. srv3 -// and srv4 reaching the OS at 512 GiB is a BOOT receipt and a TRAINING receipt for this part on -// this board. It is NOT a part qualification, and recording it as one would be the rung inflation -// DESIGN 4b names. +// and srv4 reaching the OS at 512 GiB is a BOOT receipt for this part on this board. It is NOT a +// part qualification, and it is NOT a training receipt either: full-capacity enumeration is strong +// circumstantial evidence that training succeeded, but no firmware training artifact was captured, +// so the training axis stays TrainingOutcomeUnobserved on both rows. An earlier revision of this +// sentence called it a training receipt, which contradicted the rows underneath it and the +// paragraph below that states the same thing correctly -- recording it as either a qualification +// or a training result would be the rung inflation DESIGN 4b names. // // WHAT IS DIFFERENT ABOUT THIS PART FROM THE ONE THAT FAILED, and it is the reason to expect a // different outcome rather than merely to observe one: the M386A4G40DM0-CPB was LOAD-REDUCED, so @@ -326,9 +330,9 @@ data altrad8ud_mrep_failure_observation: PlatformTrainingFailure = PlatformTrain // // PART QUALIFICATION REMAINS NotListedInVendorAvl AND THAT IS NOT A COMPLAINT. The Ampere AVL // issue 1.15 does not carry this part number. Absence is the absence of a positive result, which -// is precisely why the boot and training receipts below are worth having: they are host-specific -// evidence standing where a vendor result does not exist. Two independent hosts, eight modules -// each, one per channel, is a real sample and it is still not an AVL entry. +// is precisely why the boot receipts below are worth having: they are host-specific evidence +// standing where a vendor result does not exist. Two independent hosts, eight modules each, one +// per channel, is a real sample and it is still not an AVL entry. // TRAINING IS UNOBSERVED ON BOTH ROWS AND THAT IS THE HONEST ANSWER, not a gap I failed to close. // TrainingOperational carries a dimm_mask because the 2026-08-11 evidence for it was a specific // firmware artifact -- "DDR: Operational DIMM: 0x00005555" off the console. No such reading was @@ -351,7 +355,7 @@ data srv3_new_population_standing: HostMemoryStanding = HostMemoryStanding { }, training: TrainingOutcomeUnobserved, boot: BootReachedOperatingSystem, - observed_at: 1787775338000, + observed_at: 1787429738000, } data srv4_new_population_standing: HostMemoryStanding = HostMemoryStanding { @@ -365,9 +369,11 @@ data srv4_new_population_standing: HostMemoryStanding = HostMemoryStanding { }, training: TrainingOutcomeUnobserved, boot: BootReachedOperatingSystem, - observed_at: 1787773558000, + observed_at: 1787427958000, } +data srv4_observed_at_is_a_window_lower_bound_note: String = "srv4's observed_at is the LOWER BOUND OF A WINDOW, NOT A KNOWN INSTANT, and the difference is recorded because the carrier cannot express it. The srv4 Redfish population read was taken between 19:45Z and 20:15Z on 2026-08-22 and the exact minute was not recorded; 1787427958000 is 19:45:58Z, the timestamp of the correctable-ECC entry this session read first, so it is the earliest instant the read can have occurred at. srv3's value IS an instant, because that read was taken against a live boot transition where the clock mattered. EpochMs admits only a point, so a bounded observation must either fabricate a second or pick a bound and say which -- this picks the lower bound. A consumer computing an age from this row gets an OVERESTIMATE of elapsed time, never an underestimate, which is the safe direction for a staleness question. DISSOLVE-ON: an observed-at carrier that can express a bounded window, at which point this row moves into it and this note goes." + // srv2 FAILED THE SAME PART THAT THREE SIBLINGS TRAINED, AND THAT IS THE MOST INFORMATIVE ROW // IN THIS MODULE (2026-08-22). srv1, srv3 and srv4 all POSTed on the 64 GiB Samsung population; // srv2 could not, was left power-cycling, and was reverted to its 8 x 16 GiB Hynix set, on which @@ -410,7 +416,7 @@ data srv2_failed_64gib_population_standing: HostMemoryStanding = HostMemoryStand }, training: TrainingOutcomeUnobserved, boot: RepeatingFirmwareReset { token: "Power.Error.Blackout (no firmware POST token reached; BootProgress remained Unspecified at epoch zero)", cycles: 3 }, - observed_at: 1787782000000, + observed_at: 1787436400000, } data srv2_boot_serial_unobservable_note: String = "srv2 HostLogger held ZERO entries across both the failed 64 GiB cycles AND the successful 8 x 16 GiB boot that followed. The successful boot is the control: it proves the absence is a missing recorder, not a mute SoC. Consequence for any retry: the training axis cannot be observed on this fleet until host serial capture works (the obmc-console server configs for ttyS1/ttyS2/ttyS3 exist -- ttyS2 is the SCP, which runs DDR training -- but nothing is captured), so the highest-value action before re-testing 64 GiB on srv2 is fixing serial capture or attaching a physical cable. Failing that, the per-DIMM thermal sensors are the working instrument: the baseline is all eight at 67-75 C during a FAILED run, so a future attempt showing one channel cool fingers that channel with no firmware log needed." diff --git a/dag/test/claim/fleet_intent_memory_witness_test.dag b/dag/test/claim/fleet_intent_memory_witness_test.dag index 6607280b1d1..aa672a489d7 100644 --- a/dag/test/claim/fleet_intent_memory_witness_test.dag +++ b/dag/test/claim/fleet_intent_memory_witness_test.dag @@ -43,7 +43,18 @@ data srv3_bmc_observed_total_gib: Gibibyte = gibibyte(512) data srv4_bmc_observed_total_gib: Gibibyte = gibibyte(512) -data srv1_bmc_observed_total_gib: Gibibyte = gibibyte(512) +// srv1 HAS NO BMC READ, SO THIS ROW IS NOT ONE AND NO LONGER PRETENDS TO BE. It was authored as +// srv1_bmc_observed_total_gib, which named a Redfish observation that does not exist: srv1's +// upgrade is operator-relayed at the population grain, as gunbc.fleet_intent says in the row's own +// note. Feeding that figure through redfish_memory_summary_from_gib and asserting the population +// matched it proved 512 == 512 -- the answer under test retyped as a receipt, which is the +// fabricated-evidence failure DESIGN 5 forbids, committed inside the witness that exists to catch it. +// +// WHAT THE VALUE HONESTLY IS: the total the operator reported, against which the population row was +// transcribed. Checking the population against it is a TRANSCRIPTION check -- it catches a +// mis-authored row, and it establishes nothing about what is in srv1's slots. That is worth having +// and it is not independent evidence; the name now says which. +data srv1_operator_relayed_total_gib: Gibibyte = gibibyte(512) data srv2_bmc_observed_total_gib: Gibibyte = gibibyte(128) @@ -85,16 +96,28 @@ test fn red_wrong_stick_count_changes_nominal_total() -> Bool { wrong_total != observed_total } -test fn srv1_srv2_populations_match_bmc_memory_summary() -> Bool { - let srv1_nominal = byte_size_count(host_memory_population_nominal_bytes(pop: srv1_memory_population)) +// srv2 alone in this claim, because srv2 alone has a BMC read. It carries the 2026-07-16 Redfish +// observation of the Hynix population it was reverted to, so reconciling its authored population +// against a Redfish-shaped summary compares two independently sourced facts. +test fn srv2_population_matches_bmc_memory_summary() -> Bool { let srv2_nominal = byte_size_count(host_memory_population_nominal_bytes(pop: srv2_memory_population)) - let srv1_bmc = byte_size_count( - redfish_memory_summary_from_gib(total_gib: srv1_bmc_observed_total_gib).total_memory_bytes - ) let srv2_bmc = byte_size_count( redfish_memory_summary_from_gib(total_gib: srv2_bmc_observed_total_gib).total_memory_bytes ) - srv1_nominal == srv1_bmc && srv2_nominal == srv2_bmc + srv2_nominal == srv2_bmc +} + +// srv1's is a TRANSCRIPTION check and is named as one. It compares the authored population against +// the total the operator relayed; both trace to the same report, so a matching pair proves the row +// was transcribed faithfully and proves NOTHING about srv1's slots. It is deliberately NOT routed +// through redfish_memory_summary_from_gib: that function shapes a Redfish answer, and passing an +// operator-relayed number through it is what made the previous version read as a BMC receipt. +// DISSOLVE-ON: an authenticated srv1 BMC read, at which point this becomes a real reconcile beside +// srv2's and this comment goes. +test fn srv1_population_matches_the_operator_relayed_total() -> Bool { + let srv1_nominal = byte_size_count(host_memory_population_nominal_bytes(pop: srv1_memory_population)) + let relayed = byte_size_count(gibibyte_to_byte_size(g: srv1_operator_relayed_total_gib)) + srv1_nominal == relayed } test fn srv1_srv2_host_memory_derives_from_cited_population() -> Bool { @@ -106,10 +129,14 @@ test fn srv1_srv2_host_memory_derives_from_cited_population() -> Bool { && srv2_ram == srv2_nominal && list_length(items: srv2_host.memory) == 1 } +// SEVEN OF THE CURRENT MODULE, NOT SEVEN OF THE OLD ONE. This control previously constructed seven +// SK Hynix sticks against srv1's now-Samsung eight, so it varied part identity AND count at once and +// could pass on either difference -- it no longer isolated stick count, which is the one thing it +// claims to discriminate. Holding the module fixed makes the count the only variable. test fn red_srv1_seven_stick_population_differs_from_observed() -> Bool { let wrong = HostMemoryPopulation { rows: [ - MemoryPopulationRow { module: hma82gr7afr4n_vk_catalog, stick_count: 7 }, + MemoryPopulationRow { module: m393a8g40d40_crb0q_catalog, stick_count: 7 }, ], } let wrong_total = byte_size_count(host_memory_population_nominal_bytes(pop: wrong)) @@ -146,11 +173,17 @@ test fn srv3_observation_note_records_raw_redfish_fields() -> Bool { // carried the same population, so a test asserting srv1 == srv3 would have passed for the wrong // reason and kept passing through the upgrade. This one goes red if anyone re-uniformizes the // rows -- in either direction -- without an observation to justify it. +// THE PARTITION IS PINNED AT ALL FOUR HOSTS, because the claim being made about this fleet is +// three-upgraded-one-reverted and a check that omits srv1 does not state it. The previous version +// compared only srv2, srv3 and srv4, so srv1 could have drifted to any total -- including back to +// its pre-upgrade 128 GiB -- with this claim still green. That is the exact drift review 54843 +// caught by hand on srv1's expectation row, left undetectable in the witness beside it. test fn upgraded_and_legacy_hosts_carry_different_populations() -> Bool { + let srv1_nominal = byte_size_count(host_memory_population_nominal_bytes(pop: srv1_memory_population)) let srv2_nominal = byte_size_count(host_memory_population_nominal_bytes(pop: srv2_memory_population)) let srv3_nominal = byte_size_count(host_memory_population_nominal_bytes(pop: srv3_memory_population)) let srv4_nominal = byte_size_count(host_memory_population_nominal_bytes(pop: srv4_memory_population)) - srv3_nominal == srv4_nominal && srv2_nominal != srv3_nominal + srv1_nominal == srv3_nominal && srv3_nominal == srv4_nominal && srv2_nominal != srv3_nominal } test fn srv4_population_matches_bmc_memory_summary() -> Bool { diff --git a/dag/test/claim/installed_bom_reconcile_witness_test.dag b/dag/test/claim/installed_bom_reconcile_witness_test.dag index 1f524ec8b37..5a4172d9e0a 100644 --- a/dag/test/claim/installed_bom_reconcile_witness_test.dag +++ b/dag/test/claim/installed_bom_reconcile_witness_test.dag @@ -446,23 +446,26 @@ test fn the_dimm_lot_is_committed_with_a_read_catalog_and_no_public_cost() -> Bo quantity && read && cited && no_obligation && no_public_cost && no_public_receipt } -// THE LEDGER STILL REPORTS EVERY STICK AWAITING RECEIPT, AND THAT IS NOW A LAG, NOT THE WORLD. -// The sticks arrived: twenty-four are installed across srv1/srv3/srv4 and srv2's eight were -// installed, failed training and were removed. The ledger has not been advanced because the -// receipt events need per-stick PhysicalAssetIdentity that nobody captured, and because srv2's -// eight have no established disposition - both stated as an obligation in -// gunbc.fleet_physical_inventory beside the lot. +// RECEIVED AND UNQUALIFIED, WHICH IS CONSERVATIVE AND TRUE. The sticks arrived, so the ledger says +// so; twenty-four are installed across srv1/srv3/srv4 and srv2's eight were installed, failed +// training and were removed, and NONE of that is recorded yet, so every stick sits unqualified. // -// SO THIS CLAIM MEASURES THE LEDGER, NOT THE FLEET, and it is kept rather than deleted precisely -// because it makes the lag countable: it goes red the moment the events land, which is the signal -// to re-read this comment and retire it. Reading it as evidence that nothing has arrived is the -// authority-substitution failure DESIGN warns about - the ledger is the authority for allocation, -// never for what is physically installed, and the installed answer lives in fleet_dimm_verdicts. -test fn the_dimm_lot_holds_all_thirty_two_sticks_awaiting_receipt() -> Bool { +// THIS CLAIM PREVIOUSLY ASSERTED received == 0, which made a known-false state -- delivered hardware +// modeled as still on a truck - a condition the change had to preserve to stay green. Annotating a +// false state does not make it acceptable, and pinning it in a witness makes it load-bearing. +// +// WHAT REMAINS UNRECORDED IS BOUNDED AND NOT A LAG BY OVERSIGHT: QuantityInstalled needs a +// PhysicalAssetIdentity per stick and the serials were observed but not captured, and srv2's eight +// have no established disposition. Both are stated as obligations in gunbc.fleet_physical_inventory +// beside the lot. This claim measures THE LEDGER, never the fleet - the installed answer lives in +// fleet_dimm_verdicts, and reading an allocation ledger for a physical-installation fact is the +// authority-substitution failure DESIGN names. +test fn the_dimm_lot_is_received_and_wholly_unqualified() -> Bool { match derive_inventory_balance(lot: dimm_lot_64gib_32x, events: dimm_lot_64gib_32x_ledger) { BalanceRefused { cause: _, event_ordinal: _, event_label: _ } => false BalanceDerived { balance: b } => - b.acquired == 32 && b.received == 0 && b.available == 0 && b.reserved == 0 && b.installed == 0 + b.acquired == 32 && b.received == 32 && b.unqualified == 32 + && b.qualified == 0 && b.available == 0 && b.reserved == 0 && b.installed == 0 } } diff --git a/dag/test/parsecheck.dag b/dag/test/parsecheck.dag index 2c94df72cdb..0c643372788 100644 --- a/dag/test/parsecheck.dag +++ b/dag/test/parsecheck.dag @@ -8,7 +8,6 @@ import gunbc.host_memory_qualification { srv2_failed_64gib_population_standing } import gunbc.ci_floor_measurement { gunbc_ci_srv3_memtotal_measured } import test.claim.installed_bom_reconcile_witness_test { the_dimm_lot_is_committed_with_a_read_catalog_and_no_public_cost, - the_dimm_lot_holds_all_thirty_two_sticks_awaiting_receipt, } fn parsecheck_holds() -> Bool { ucs_mr_1x648ru_a.underlying_module.rank_count == 8 @@ -16,5 +15,4 @@ fn parsecheck_holds() -> Bool { && fleet_dimm_expectations.length() == 4 && srv1_memory_population.rows.length() == 1 && the_dimm_lot_is_committed_with_a_read_catalog_and_no_public_cost() - && the_dimm_lot_holds_all_thirty_two_sticks_awaiting_receipt() }