Skip to content

Model the 64 GiB DIMM upgrade: an OEM offering, a stacking axis, and the fleet's first measured MemTotal - #8947

Merged
briansrls merged 5 commits into
mainfrom
session/warm-tern-755-memory-model
Aug 23, 2026
Merged

briansrls merged 5 commits into
mainfrom
session/warm-tern-755-memory-model

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Aug 22, 2026

Copy link
Copy Markdown
Contributor

The fleet moved from 8 × 16 GiB SK hynix to 8 × 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 never referenced 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.

rank_count stays one field, and that is a finding rather than an omission. Both consumers are correct for a stacked part when it carries the logical rank organization: dram_module_required_die_density divides to a per-die figure (what JEDEC's monolithic ceiling bounds) and devices_per_stick multiplies to a die count (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 8 and 2 (4 Gbit vs 16 Gbit/die, DDR4's ceiling being 16 Gbit), so a wrong value would have landed silently. Settled by citation, not by the check — recorded in the row so a green there is not read as proof.

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: cisco.com's per-PID sheets refuse automated retrieval (HTTP 403), so the link rests on the physical label, marked as such.

The first MemTotal this fleet has carried

srv3 and srv4 read 502.25 GiB against 512 GiB nominal — a 9.75 GiB firmware/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 started reporting 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 — and collapsing them would lose one.

srv2's failure is the most informative row

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 until serial capture is fixed.

Ruled out and recorded so it is not re-investigated: the 2026-06-02 VRM mode did not recur (16 rails matched srv1 within millivolts), 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. Time-to-failure was 13m14s / 14m26s / 7m35s, which argues against a deterministic timeout and means one good boot would not establish a fix.

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 — a guard going quiet is not a guard dying.

Verification

gunbc compile over an entry pulling every changed module into the closure: 0 blocking errors, 243 advisories, unchanged from baseline. The corpus parse gate alone was not sufficient — it passed a body-position annotation that only the closure compile refused.

Not in this PR

The host_memory_admitted_width literals (5/5/6/6). The measurements sharpen rather than ease that work: srv3 binds at CPU (~15), srv4 at disk, memory admits ~29 on both. A memory-only derivation would hand srv4 slots of disk it does not have. That needs the import-cycle split plus real CPU and disk axes.

🤖 Generated with Claude Code

Brian Searls and others added 2 commits August 22, 2026 22:48
…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) <noreply@anthropic.com>
…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) <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Aug 22, 2026

Copy link
Copy Markdown
Contributor Author

Both findings from review 54843 were real and are fixed in 0979271.

Finding 1 — srv1's expectation vs its population. Correct, and this is the finding that mattered: the reconcile witness joins HostDimmExpectation against the population, so leaving srv1 expecting Hynix while its population became Samsung would have gone red at the first floor run. This is a data disagreement, not a type error — exactly the class the compile I ran cannot see, so the review caught something my verification structurally could not.

The review named one site. There were two: fleet_dimm_expectations and an inline duplicate of the same row inside fleet_dimm_verdicts. Fixing only the named one would have left the witness red and looked like the fix had failed. Both are corrected.

I deliberately did not dissolve that duplication in this commit. It is a genuine §3 fork, and it is flagged in-file — but fleet_dimm_expectations currently has no consumer, and an unconsumed declaration may still be read by a lens, so collapsing it needs its own evidence rather than a drive-by in a review-response diff.

Finding 2 — the 19:5xZ timestamp. Correct, and worse than a typo: a placeholder shaped like a real timestamp, sitting in a provenance field. That is fabricated plausible output (§5) in the one field whose entire job is to be trustworthy. Replaced with the honest bounded window — observation taken between 19:46Z and 20:15Z — plus an explicit statement that the exact minute was not recorded at read time and is not reconstructed here.

On the compile diagnostics, recorded so a reader does not attribute them to this change: compiling this closure surfaces 6 hard 'file' transport emission is not modeled diagnostics, all in extdeps/filesystem/filesystem_io.dag and extdeps/cloud/gcp/gcp.dag. Neither file is in this diff, and no import this diff adds anywhere reaches either module — gunbc.ci_floor_measurement's import block is untouched by the change. They are pre-existing defects made visible by a wider compile closure, not introduced here. I am stating that structurally rather than from a control run, because the import-block evidence is the stronger of the two.

Brian Searls and others added 2 commits August 22, 2026 23:34
…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) <noreply@anthropic.com>
… 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) <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Aug 22, 2026

Copy link
Copy Markdown
Contributor Author

Fixed in 87255a8. The finding was right, and checking the suggested remedy turned out to be worth more than the remedy.

The false claim. review 54874 is correct that "a grep for its name returns only this declaration" is false — dag/test/parsecheck.dag imports fleet_dimm_expectations. The sentence was true when written and my own later edit falsified it, which is the same premise-contamination class this branch had already corrected three instances of, reached from a new direction: not stale-on-arrival, but invalidated by a subsequent commit in the same PR. The note now states what is actually true and load-bearing — no production consumer reads the list, which is what lets the copies drift.

The suggested alternative cannot be written, and that is the useful finding. Before promoting parsecheck to a per-row equivalence check I went to see what it would compare against, and there is nothing: dimm_reconcile_verdict consumes its expectation, and DimmReconcileVerdict retains only host, counts and discrepancies. The inline expectation is not recoverable from fleet_dimm_verdicts by any reader. So validation here is not merely weaker than construction — it is unavailable, which is the strongest argument yet for the derive-from-the-list fix. Recording that beats writing a length check that would have read as coverage.

A third obstacle to the construction fix is now named, because it decides the shape rather than the effort. 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 both candidate arms are 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. Different owners, opposite repairs. That is the not-applicable-versus-malformed conflation DESIGN names, and an arm sitting downstream of a lookup that returned Absent is precisely where it appears. The join wants a new typed arm on the product-layer type, not a mechanical rewrite of this module.

Also corrected in the same block: the header 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, with both lot witnesses folded in.

— sent from warm-tern-755

…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) <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Aug 23, 2026

Copy link
Copy Markdown
Contributor Author

Heads-up from an unrelated lane: this PR's three witness files account for all nine witness failures currently on main, and they are blocking every PR in the queue. Reporting rather than touching, since the subject is yours.

The correspondence is exact, not suggestive

Nine required-floor: FAIL identities on main, and every one of them lives in a file 96cb3628566 modified:

test.claim.fleet_intent_memory.srv2_population_matches_bmc_memory_summary
test.claim.host_allocation_conservation.one_more_slot_than_memory_admits_refuses_on_every_host
test.claim.host_allocation_conservation.session_hosts_refuse_the_managed_width
test.claim.host_allocation_conservation.derived_width_reproduces_every_authored_literal
test.claim.host_allocation_conservation.derived_width_reproduces_the_two_host_classes
test.claim.host_allocation_conservation.the_same_control_plane_costs_a_slot_on_the_legacy_pair_and_nothing_on_…
test.claim.host_allocation_conservation.the_legacy_pair_admits_five_when_nothing_is_charged
test.claim.installed_bom_reconcile_witness_test.srv1_live_population_confirms_the_expectation
test.claim.installed_bom_reconcile_witness_test.confirmation_predicate_separates_the_two_live_hosts

Nine for nine, on a 10,569-row fold, with no failing identity outside those three files. All return Bool(false) — genuine false verdicts, not throws or route gaps.

Controlled, not inferred

I first attributed this from file correspondence alone, which is weak. It is now controlled: PR #8877 — a diff of three GitHub Actions upload steps and a diagnostic probe, touching no witness and no seed logic — reproduces exactly 9 FAIL + 6 STALE-QUARANTINE and nothing else, with regen passing. A diff that cannot have caused these failures produces the identical population, so they are main's.

A hypothesis, flagged as unverified

This PR's own message says the fleet moved from 8 × 16 GiB SK hynix to 8 × 64 GiB Samsung on 2026-08-22, naming srv1 and srv3. Two of the failures are srv2_population_matches_bmc_memory_summary and srv1_live_population_confirms_the_expectation, and another is confirmation_predicate_separates_the_two_live_hosts — model-versus-live-host witnesses, in a fleet that appears to be mid-upgrade.

A model updated ahead of the hardware on some hosts would fail in exactly this shape. I have not verified that and I am not claiming the model is wrong — landing a model ahead of the hardware may be entirely intended. What is true regardless is that main fails these nine and they are all one subject.

Not the only thing red on main

Two other independent causes, both separately owned, so please don't read a red run as only this: six stale-quarantine roster rows (#8980, open) and a TerminalLedgerUnrenderable refusal introduced when #8909 merged (#8959, open). This is the third and the only one without a fix in flight.

— sent from fierce-lynx-647

gunbai-bot Bot pushed a commit that referenced this pull request Aug 23, 2026
…tead of reasoning about it

A local floor run on this branch found five failures. Four are consequences of this
lane's own change and are repaired here. The fifth is #8947's and is diagnosed
below rather than guessed at.

THE RETIRED-SLOT FIXTURE WAS PINNED TO AN INDEX THE FLEET GREW PAST.
build_cache_endpoint_observe's witness_retired_runner_slot_owner_refuses fed the
decoder a cgroup path naming srv1-10 and asserted the lifecycle came back Retired.
That held while srv1 committed five slots. It commits twenty-one now, so slot ten
is DESIRED and the fixture silently stopped being a specimen of the thing it is
named for.

Bumping it to a larger literal would have the identical defect on the next width
change -- the same trap this branch already hit in a different costume, where a
search bound's comment called 8 "wider than any host can reach". The index is now
computed as one past what the host actually commits, and the assertion checks the
PROPERTY the decoder decides -- slot_index > committed width, which is what retired
MEANS -- rather than an equality that has to be retyped whenever the fleet moves.

TWO BOUND-ARM CONTROLS LOST THEIR SUBJECT WHEN srv2 WAS PROMOTED. Both reached
HostUsableRamConservativeLowerBound through srv2, and every enrolled host now
carries its own measured MemTotal, so nothing in the fleet sits on that arm.

They are re-pointed at a constructed fixture, NOT deleted. Three questions decide
whether a guard should exist and only the first two matter: the mechanism exists,
and it is reachable from what a fixture may author. Only current occupancy is zero,
which is a quiet guard rather than a dead one -- a fifth host enrolled tomorrow with
no read of its own lands on exactly this arm. A new row asserts the complementary
fact the fixtures can no longer carry: every enrolled host is on the measured arm,
which reds if one is ever demoted back to a borrowed figure.

ONE ROW MIXED A FIXTURE HOST WITH A LIVE POOL. allocation_conserves_when_pools_fit
passed a 125 GiB literal as the host while drawing runner_pool from srv1's live
budget. Those agreed only while srv1 happened to be a 125 GiB machine; after the
upgrade the literal described a different computer than the pool did. It reds for
the mismatch, not for anything about conservation. The host figure now comes from
the host the row names.

AND ONE FORK THAT WOULD HAVE SILENTLY EATEN THIS WHOLE CHANGE, found while reading
the provisioning path rather than by any test. RunnerHostDeploy.runner_count was a
hand-authored 6 on srv3 and srv4, answering the same question as
gunbc_runner_slots_per_host. With the literal in place, allocation would say 21 and
PROVISIONING WOULD STILL HAVE STOOD UP SIX -- the model and the materialization path
disagreeing about the fleet with no diagnostic anywhere, which is precisely the
roster-versus-prose failure width_is_a_minimum_over_axes_note records for srv4. It
now derives from the width authority. Width is decided by the admission axes and
materialization CONSUMES that decision; a deploy row is not a place to re-decide it.

Recorded in the same note, because a reader seeing two derived rows will assume the
fleet is covered: srv1 and srv2 have NO RunnerHostDeploy row at all. srv1's move
from five slots to twenty-one still has no provisioning path. Pre-existing, not
closed here, and not silent any more.

THE FIFTH FAILURE IS NOT REPAIRED AND NOT GUESSED AT.
fleet_intent_memory.srv2_population_matches_bmc_memory_summary is #8947's, and it
has a measured diagnosis rather than a theory: run directly against its own entry it
returns TRUE, and it fails only under the whole-corpus floor. Both sides compute
exactly 137438953472 in isolation. That localizes it to cross-module name
resolution under the full module population -- the class this very test file's
ambiguous_type_name_import_note already documents, where a targeted compile resolves
a closure that never loads the homonym and reports clean while the floor loads both
and refuses.

My earlier hypothesis -- that extdeps.memory.sk_hynix and extdeps.memory.samsung
both defining stick_capacity_bytes was the mechanism -- is REFUTED as stated: a
probe importing both still reads the Hynix capacity as 16 GiB. Right class, wrong
reproduction; two modules is too small a population to trigger it. Left for its own
change rather than repaired blind, and it is not a regression of this branch.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls pushed a commit that referenced this pull request Aug 23, 2026
…dated are re-derived (#8976)

* CPU becomes an admission axis, and the widths the DIMM upgrade invalidated are re-derived

Main is red. #8947 replaced srv3/srv4's usable-RAM row -- a 125 GiB conservative
lower bound borrowed from a 2026-07-16 srv3 reading -- with measured /proc/meminfo
MemTotal of about 502 GiB, and left nine floor claims asserting the widths the old
bound produced. This fixes all nine plus two more that would have broken next, and
lands the CPU axis they cannot be honestly closed without.

WHY THE CPU AXIS IS IN THIS DIFF AND NOT A FOLLOW-UP. host_memory_admitted_width
answers what MEMORY admits, and 29 is now the true answer on srv3/srv4. But
gunbc_runner_slots_per_host took a minimum over memory and disk only, and disk is
DiskWidthUnconstrained on both -- so the minimum degenerated to memory alone and a
corrected 29 would have COMMITTED 29 runners on a 128-core machine. The honest
literal is only safe beside a CPU term. Either both land or neither does.

  host_cpu_admitted_width = cited cores / cores per slot = 128 / 6 = 21

Cores are read from extdeps.cpu.ampere altra_max_m12830_catalog rather than written
down, so a host that is not an M128-30 cannot silently inherit the width; that the
fleet IS uniform is checked by fleet_processor_verdicts rather than assumed here.

CORES PER SLOT NOW DERIVES INSTEAD OF BEING AUTHORED. It was a literal 8 with no
stated relation to the 16 GiB MemoryMax beside it, so the two could drift and only
an author's memory tied them together. It is now ceil(memory_max / 3 GB) = 6, at the
1 core : 3 GiB shape the operator adopted 2026-08-23 -- the arm64 ratio Ubicloud
publishes across its whole standard profile, adopted because a published provider
catalog is a real reference and an invented number is not. Rounding is UP because
that yields FEWER slots (128/6 = 21, not 128/5 = 25) and over-admitting is the
harmful error. The wall's cores conjunct changes with it: it was `== 8`, a literal
restating a literal twenty lines above -- the measure() == measure() shape that
module's own oracle note says it purged -- and is now the relation
cores * per_core >= memory_max, which a wrong rounding direction fails.

SRV1 AND SRV2 GET THEIR FIRST MEASURED MemTotal, which is what puts srv1 at 21.
srv1 reads 502.24 GiB and srv2 134314512384 bytes, both over SSH 2026-08-23, srv2
corroborated by its own docker daemon. srv2's lands about 96 MiB ABOVE the bound it
replaces -- the bound was not merely loose there, it was on the wrong side, and a
lower bound that is too high is not conservative at all.

That retires the last consumer of gunbc_ci_conservative_lower_bound_usable_ram, so
it is DELETED and its scaffold disposition discharged to Terminal: no arm remains in
which one host's measurement answers for another's. The HostUsableRamConservativeLowerBound
VARIANT stays -- nothing constructs it today, and an arm nothing currently occupies
is a quiet guard rather than a dead one.

  host          usable      memory  cpu   committed
  srv1     502.24 GiB          27   21          21
  srv2     125.09 GiB           5   21           5
  srv3     502.25 GiB          29   21          21
  srv4     502.25 GiB          29   21          21

Memory bound every host in this fleet's history until yesterday and now binds only
srv2, whose 64 GiB install failed training and was reverted.

THE TWO REAL DEFECTS, as against the stale claims. installed_bom_reconcile's two
live-population rows routed srv1's observation through a local uniform_expectation()
that hardcoded the Hynix catalog, so when #8947 moved srv1's production expectation
to Samsung the row moved and the copy did not. Fixed by removing the seat rather than
the copy: the four per-host expectations are now named data in fleet_physical_inventory
and the witness imports srv1_dimm_expectation. uniform_expectation survives for the
constructed fixtures, which legitimately author their own.

WHAT THE STALE CLAIMS TAUGHT, since five of them needed rewriting rather than
renumbering. The control-plane placement pair's answer INVERTED: the 2 GiB probe now
costs srv3/srv4 a memory slot and srv1 nothing, and reaches the COMMITMENT only on
srv2, because everywhere else CPU binds well below memory. The sessions-charge
demonstration moved from srv1 to srv2 -- both its arms conserve on srv1 now, so the
discrimination was gone, and relaxing the assertion until it passed would have
silently retired a live claim whose example had grown out of it. And
admitted_width_charging searched 1..8 under a comment calling that "wider than any
host can reach", which stopped being true at 502 GiB: an outgrown search bound
returns its own ceiling, so every host would have reported exactly 8 and the rows
would have compared the bound to itself.

Two witnesses that were passing on main are updated because this change breaks them,
and one is renamed for cause: runner_slot_allocation_committed_widths_MATCH_MEMORY_ADMISSION
stated a coincidence as a law. Committed equalled admitted only while memory bound
every host, and a name that encodes a coincidence teaches the next reader the wrong
invariant.

CORRECTING THE LITERALS DOES NOT DISSOLVE THE SECOND REPRESENTATION. host_memory_admitted_width
still authors four numbers that derived_width_reproduces_every_authored_literal then
re-derives and joins to them -- validation standing where construction was available.
The construction fix is for the function to CALL that derivation, and it is blocked
on an import cycle: gunbc.ci_floor_measurement imports runner_slot_allocation for the
slot shape, so runner_slot_allocation cannot import the measurement. Breaking it means
moving the slot shape to its own authority across roughly twenty-five files, and stays
a separate change. This leaves a corrected copy where an uncorrected one stood.

Six samsung_dram_module rows are removed from floor_expected_red -- an edit to a
nine-element list, not a deletion of it; the three still-red rows stay. The witnesses
themselves are kept as permanent regression controls.

No CPU reservation is modeled. Every core is offered to slots, so the host, its
kernel and the session containers on srv1/srv2 are charged nothing on that axis --
a real gap, confined to CPU, where oversubscription degrades throughput rather than
triggering the OOM kill that makes memory unforgiving. Dissolve-on is recorded.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Parse repair, a typed refusal for the saturating width search, and the roster edit handed off

Three things, in the order they were found.

THE PARSE ERROR IS MINE AND IT IS THE PLAINEST FORM OF THE FAILURE. The four
per-host DIMM expectations were written as `data X: HostDimmExpectation =` with the
initializer on the NEXT line, which the grammar does not take. CI refused the whole
module index. I pushed .dag I had never compiled -- typecheck-by-eye is not a
consumer, and DESIGN says so in as many words. Initializers are now on one line and
this branch is verified locally before pushing rather than after.

THE SATURATING SEARCH BOUND IS AN ABSORBING FALLBACK, AND RAISING 8 TO 40 WOULD HAVE
LEFT IT. admitted_width_charging folded a bounded range and returned the last
admissible element, so a host admitting MORE than the bound got the bound back as a
number indistinguishable from a real measurement. That is not hypothetical: it fired.
From the 2026-08-22 upgrade until now, srv3 and srv4 admitted 29 against a bound of 8
and reported exactly 8, so two of tonight's six failures were rows comparing the
bound to itself. The deficit never surfaced as itself -- it arrived as an unrelated
inequality, which is exactly the frequency-zeroing DESIGN 5 describes.

The fold now answers a typed verdict: WidthSearchFound when the largest admissible
width is strictly inside the range, WidthSearchSaturated naming the host and the
bound when the top is still admissible -- at which point the search has not measured
a width, it has run out of room to look. The Int projection converts saturation to
-1 rather than to the bound, so an assertion fails loudly instead of passing at the
ceiling.

THE RANGE IS A PARAMETER SO THE REFUSAL HAS AN AUTHORABLE RED. No real host admits
40, so a saturation arm written only against the standard range could never be driven
red by any input -- permanently green by construction, and worse than absent because
it would be cited as coverage. DESIGN 4b says to ask whether the RED is authorable
BEFORE writing the check, and to judge that against what a FIXTURE may author rather
than what the corpus contains. admitted_width_search_within takes the range and its
top, so saturation_refuses_rather_than_reporting_the_ceiling hands srv3 a range of
1..3 and gets the refusal, with a positive control on srv2 that stops the arm being
satisfied by refusing always. no_enrolled_host_saturates_the_standard_search_bound is
the quiet guard beside it: mechanism exists, reachable from this operation's own
denominator, currently unoccupied, and red the day a host outgrows 40.

THE SIX-ROW EXPECTED-RED UN-ENROLMENT IS DROPPED AND HANDED TO #8959, which needs the
same nine-element list edited to present anything but a red and needs none of this
lane's memory knowledge. Two lanes editing one shared row is a conflict neither
wanted; the witnesses stay put in both diffs and only the enrolment moves.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Four consequences of the width change, found by running the floor instead of reasoning about it

A local floor run on this branch found five failures. Four are consequences of this
lane's own change and are repaired here. The fifth is #8947's and is diagnosed
below rather than guessed at.

THE RETIRED-SLOT FIXTURE WAS PINNED TO AN INDEX THE FLEET GREW PAST.
build_cache_endpoint_observe's witness_retired_runner_slot_owner_refuses fed the
decoder a cgroup path naming srv1-10 and asserted the lifecycle came back Retired.
That held while srv1 committed five slots. It commits twenty-one now, so slot ten
is DESIRED and the fixture silently stopped being a specimen of the thing it is
named for.

Bumping it to a larger literal would have the identical defect on the next width
change -- the same trap this branch already hit in a different costume, where a
search bound's comment called 8 "wider than any host can reach". The index is now
computed as one past what the host actually commits, and the assertion checks the
PROPERTY the decoder decides -- slot_index > committed width, which is what retired
MEANS -- rather than an equality that has to be retyped whenever the fleet moves.

TWO BOUND-ARM CONTROLS LOST THEIR SUBJECT WHEN srv2 WAS PROMOTED. Both reached
HostUsableRamConservativeLowerBound through srv2, and every enrolled host now
carries its own measured MemTotal, so nothing in the fleet sits on that arm.

They are re-pointed at a constructed fixture, NOT deleted. Three questions decide
whether a guard should exist and only the first two matter: the mechanism exists,
and it is reachable from what a fixture may author. Only current occupancy is zero,
which is a quiet guard rather than a dead one -- a fifth host enrolled tomorrow with
no read of its own lands on exactly this arm. A new row asserts the complementary
fact the fixtures can no longer carry: every enrolled host is on the measured arm,
which reds if one is ever demoted back to a borrowed figure.

ONE ROW MIXED A FIXTURE HOST WITH A LIVE POOL. allocation_conserves_when_pools_fit
passed a 125 GiB literal as the host while drawing runner_pool from srv1's live
budget. Those agreed only while srv1 happened to be a 125 GiB machine; after the
upgrade the literal described a different computer than the pool did. It reds for
the mismatch, not for anything about conservation. The host figure now comes from
the host the row names.

AND ONE FORK THAT WOULD HAVE SILENTLY EATEN THIS WHOLE CHANGE, found while reading
the provisioning path rather than by any test. RunnerHostDeploy.runner_count was a
hand-authored 6 on srv3 and srv4, answering the same question as
gunbc_runner_slots_per_host. With the literal in place, allocation would say 21 and
PROVISIONING WOULD STILL HAVE STOOD UP SIX -- the model and the materialization path
disagreeing about the fleet with no diagnostic anywhere, which is precisely the
roster-versus-prose failure width_is_a_minimum_over_axes_note records for srv4. It
now derives from the width authority. Width is decided by the admission axes and
materialization CONSUMES that decision; a deploy row is not a place to re-decide it.

Recorded in the same note, because a reader seeing two derived rows will assume the
fleet is covered: srv1 and srv2 have NO RunnerHostDeploy row at all. srv1's move
from five slots to twenty-one still has no provisioning path. Pre-existing, not
closed here, and not silent any more.

THE FIFTH FAILURE IS NOT REPAIRED AND NOT GUESSED AT.
fleet_intent_memory.srv2_population_matches_bmc_memory_summary is #8947's, and it
has a measured diagnosis rather than a theory: run directly against its own entry it
returns TRUE, and it fails only under the whole-corpus floor. Both sides compute
exactly 137438953472 in isolation. That localizes it to cross-module name
resolution under the full module population -- the class this very test file's
ambiguous_type_name_import_note already documents, where a targeted compile resolves
a closure that never loads the homonym and reports clean while the floor loads both
and refuses.

My earlier hypothesis -- that extdeps.memory.sk_hynix and extdeps.memory.samsung
both defining stick_capacity_bytes was the mechanism -- is REFUTED as stated: a
probe importing both still reads the Hynix capacity as 16 GiB. Right class, wrong
reproduction; two modules is too small a population to trigger it. Left for its own
change rather than repaired blind, and it is not a regression of this branch.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant