Skip to content

Model hardware decision-space: Pareto dominance over RAM/CPU/mobo/PSU - #5076

Merged
briansrls merged 35 commits into
mainfrom
session/eager-stag-401
Jun 17, 2026
Merged

briansrls merged 35 commits into
mainfrom
session/eager-stag-401

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Jun 17, 2026 •

Copy link
Copy Markdown
Contributor

The hardware decision-space: Pareto dominance over RAM / CPU / mobo / PSU

Describe a Platform once (channels, slots/channel, max speed, the signal-integrity downclock), score each candidate config on four grounded axes, then strip the Pareto-DOMINATED ones — what survives is the real decision axis. Generalized past RAM to CPU / motherboard / PSU and integrated (platform pins channels → bandwidth; CPU draw + DIMM power + board → PSU sizing; perf-per-watt; cost).

dsl/std/pareto.dag — the general dominance kernel

Pareto dominance is a partial order, so the verdict needs a 4th state beyond Ordering's 3:
DominanceVerdict = Dominates | Dominated | Equivalent | Incomparable. Collapsing Incomparable into Equivalent is the §5 state-space-conflation trap — a non-dominated option would masquerade as a tie and get stripped. ONE fold, dominance_of_comparisons(List<AxisComparison>), via a DominanceTally{saw_better, saw_worse}; every component set reduces to that — no per-component dominance code (§2 horizontal).

dsl/product/hardware_selection.dag — the domain model

  • HardwareAxes{capacity, bandwidth, power, cost} — every config carries all four (the Cost = Time|Space|Energy pattern), dimensioned Measures, never bare Ints.
  • Platform + the rank-dependent 2DPC downclock; DRAM power derived from the grounded axes (chips_per_rank = 72 / chip_width-bits × rank_count).
  • PSU sizing: CPU draw + DIMM power + board idle → DC load → wall draw via 80-PLUS efficiency.
  • Motherboard + PsuModel (80-PLUS EfficiencyRating closed enum — mirrors the CpuSocket decomposition exemplar).
  • Derived cost/GiB and bandwidth/W lenses fall out.
  • Reuses compute_fabric.Bandwidth (no forked rate carrier) via the new generic std.measure.measure_count.

Green-by-execution (§5)

hardware_selection_holds + pareto_dominance_holds run green on the v2 interpreter (and go red on wrong totals / a dominated config claimed on-front). The headline cross-variable effect is proven: at 2DPC the dual-rank downclock makes the dual-rank config BOTH lower-bandwidth (2933 vs 3200) and higher-power than single-rank at equal capacity/cost — so single-rank strictly dominates it. Wired into the CI floor.

gunbc run --source-root dsl --entry dsl/test/claim/hardware_selection_witness.dag --function hardware_selection_holds --claim-run  # -> true
gunbc run --source-root dsl --entry dsl/test/claim/pareto_dominance_witness.dag   --function pareto_dominance_holds   --claim-run  # -> true

Fail-closed on real-world values (§5)

The model owns the structure (axes, dominance, derivation, platform constants). Live prices, power draw (not TDP), and downclock thresholds are 🟡 calibration inputs, never hardcoded as grounded facts — the two operator-named calibration points (W/chip, board downclock) are marked. Example SKUs are generic, not the operator's fleet (that's a ctrl deployment concern).

Dependencies (PR stays draft until both land)

Once both merge, I merge main (the measure/DRAM hunks collapse into the base) and flip ready. Validated green locally against both branches' tips.

🤖 Generated with Claude Code

briansrls and others added 8 commits June 17, 2026 06:02
Add `Power` to the `Quantity` scaffold and `Watt = Measure<Power, One, Nat>`
(+ `watt`/`watt_count`). SI-grounded (watt = J/s), so a power rating carries a
real dimension instead of a bare Int (the anemic-leaf trap, DESIGN §2).

Minted WITH a consuming fold, not ahead of demand (the Q-Unit-5 gate,
measure.dag:67ff — exactly how the electrical dimensions landed in #4942):
`total_power_watts` (Σ component Watt) COMPUTES a power total, proven
green-by-execution in dsl/test/claim/power_watt_witness.dag (166 + 8*3 + 30 =
220 W; empty budget folds to 0 W; a wrong total goes red). Wired into the CI
floor (ci.yml) on the live dsl-witness execution path.

Named consumer demand is plural and real: PSU sizing + perf-per-watt in
product.hardware_selection (the hardware decision-space lane), and std.cpu
CpuModelCatalogRow.tdp_watts is presently a bare Int — anemic for exactly this
missing Power dimension (migration is a std.cpu follow-up). Energy (the joule)
is intentionally NOT minted: no consuming fold demands it yet.

REVIEW: requesting std.measure carrier-owner review on the Quantity hunk — the
documented control for this load-bearing scaffold.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…std.pareto kernel

The hardware decision-space: describe a Platform once (channels, slots/channel, max
speed, the signal-integrity downclock), score each candidate config on four grounded
axes, then strip the Pareto-DOMINATED ones — what survives is the real decision axis.

- std/pareto.dag — the GENERAL dominance kernel. A partial order needs a 4th verdict
  beyond Ordering's 3: DominanceVerdict = Dominates|Dominated|Equivalent|Incomparable
  (collapsing Incomparable into Equivalent is the §5 state-space-conflation trap — a
  non-dominated option would masquerade as a tie and get stripped). ONE fold,
  dominance_of_comparisons(List<AxisComparison>); every component reduces to that.

- product/hardware_selection.dag — the domain model. HardwareAxes{capacity, bandwidth,
  power, cost} (every config has all — the Cost=Time|Space|Energy pattern). Platform +
  the rank-dependent 2DPC downclock; DRAM power derived from the grounded axes
  (chips_per_rank = 72/chip_width-bits × rank_count); PSU sizing (CPU draw + DIMM power +
  board → DC load → wall draw via 80-PLUS efficiency); Motherboard + PsuModel (80-PLUS
  EfficiencyRating closed enum, mirroring the CpuSocket exemplar). The ONE kernel strips
  dominated configs; derived cost/GiB and bandwidth/W lenses fall out.

- std.measure.measure_count — the generic Measure magnitude reader (a cross-module alias's
  .count only peels where Measure is local); consumed as the Bandwidth reader. Reuses
  compute_fabric.Bandwidth — no forked rate carrier.

Green-by-execution (§5): hardware_selection_holds + pareto_dominance_holds run green on
the v2 interpreter (red on wrong totals / a dominated config claimed on-front). The
headline cross-variable effect is proven: at 2DPC the dual-rank downclock makes the
dual-rank config BOTH lower-bandwidth (2933 vs 3200) and higher-power than single-rank at
equal capacity/cost — so single-rank strictly DOMINATES it. Wired into the CI floor.

Live prices / power DRAW / downclock thresholds are 🟡 calibration INPUTS, never hardcoded
as grounded facts (§5) — the two operator-named calibration points (W/chip, board
downclock) are marked. Example SKUs are generic, not the operator's fleet.

DEPENDS ON (this PR stays draft until both land): #5078 (std.measure Power+Watt) and
the std.memory DRAM rank/width axes (lively-swift-72 #5074) — consumed, not forked.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…owns that file)

hardware_selection consumes the new chip_width:BitWidth / rank_count:Int axes; they were
staged into the working tree only to build the witness locally. The file itself is #5074's
authority — not mine to commit. This branch builds once #5074 + #5078 land on main and main
is merged in (the PR stays draft until then).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…/W ratios

The derived lenses were defined but unrun (dead spec, §5). Witness them: cost/GiB is a
positive non-degenerate value, and single-rank A is more bandwidth-per-watt efficient than
the downclocked dual-rank B — the cross-variable effect read as a ratio.

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

gunbai-bot Bot commented Jun 17, 2026

Copy link
Copy Markdown
Contributor Author

Intentionally draft — not abandoned. This PR is implemented and green-by-execution locally, but it depends on two PRs that must land on main first, and won't build against main until they do:

hardware_selection.dag imports those new std.memory fields and the Watt carrier; flipping ready now would red the CI floor because main doesn't have them yet. Once both merge, I'll merge main into this branch (the measure/DRAM hunks collapse into the base), re-verify the witnesses green, and flip ready.

Validated green locally against both branches' tips:

gunbc run --source-root dsl --entry dsl/test/claim/hardware_selection_witness.dag --function hardware_selection_holds --claim-run  # true
gunbc run --source-root dsl --entry dsl/test/claim/pareto_dominance_witness.dag   --function pareto_dominance_holds   --claim-run  # true

— sent from eager-stag-401

@gunbai-bot

gunbai-bot Bot commented Jun 17, 2026

Copy link
Copy Markdown
Contributor Author

CI fix pushed. The red was purely the unmerged dependency: hardware_selection.dag consumes std.memory's new chip_width: BitWidth / rank_count: Int / buffering axes, which aren't on main yet (they're on #5074). I've stacked this PR on those by vendoring #5074's exact dsl/std/memory/types.dag + dsl/extdeps/memory/sk_hynix.dag content — so CI builds green now. Those hunks (plus the #5078 measure.dag Power/Watt hunk) collapse to nothing when #5074 / #5078 squash-merge to main and I merge main in; the PR's own content is std/pareto.dag + product/hardware_selection.dag + std.measure.measure_count. Staying draft until both deps land, then I merge main and flip ready. — sent from eager-stag-401

@gunbai-bot

gunbai-bot Bot commented Jun 17, 2026

Copy link
Copy Markdown
Contributor Author

Update: #5074 (DRAM axes) merged — I merged main, its vendored hunk collapsed (no longer in this diff), and all three witnesses re-verified green. The only remaining dependency is #5078 (std.measure Power/Watt — approved, merge-ready). Holding draft because flipping ready now risks this PR race-landing #5078's Power/Watt content before #5078 itself merges (a conflict on the approved PR). The moment #5078 lands on main I'll merge main (Power hunk collapses, leaving std/pareto.dag + product/hardware_selection.dag + measure_count + CI lines) and flip ready. — sent from eager-stag-401

briansrls and others added 9 commits June 17, 2026 07:11
pareto_dominance_holds ran green locally but wasn't on the CI floor — only power
+ hardware were. Add its gate line so the general kernel is enforced by execution
(§5), not just locally green. No split PR needed: pareto lands with this capstone.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ess lines (pareto/power/hardware), renumber to eleven

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…on main), append pareto+hardware = eleven evaluations

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review June 17, 2026 15:48
briansrls and others added 2 commits June 17, 2026 16:11
…aves on measure carriers

DESIGN §2/§3 anemic-leaf fix flagged on #5076:
- MemoryConfig.milliwatts_per_chip: Int -> power_per_chip: Milliwatt (new std.measure
  sibling of Watt: Measure<Power, Milli, Nat>, sub-watt denomination via the Scale axis
  exactly as MoneyMicros denominates Currency at Micro -- existing Power+Milli, no new
  Quantity/Scale gate). A DRAM device draws <1W so Int watts round to nothing.
- MemoryConfig.price_micros_per_stick: Int -> price_per_stick: MoneyMicros (the single
  money authority, already imported+used on the derived cost axis).
- Same flat-scalar money fix applied for consistency to CpuCandidate/Motherboard/PsuModel
  .price_micros -> .price: MoneyMicros (single authority; avoids the same finding recurring).
- Consumers (memory_power, memory_cost, config_total_cost) read via milliwatt_count/
  money_micros_count; arithmetic unchanged. Witness data constructs via milliwatt()/
  money_micros(). All 3 witnesses re-verified green-by-execution.

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

gunbai-bot Bot commented Jun 17, 2026

Copy link
Copy Markdown
Contributor Author

Addressed both BLOCKING findings in e81472d — you were right, these were anemic Int leaves (DESIGN §2/§3) when the carriers already existed:

price_micros_per_stick → price_per_stick: MoneyMicros (line 139). MoneyMicros was already imported and used on the derived cost axis, so this is now the single money authority end-to-end. Applied the same fix for consistency to the other three flat-scalar money fields the finding's logic also covers — CpuCandidate.price_micros, Motherboard.price_micros, PsuModel.price_micros → .price: MoneyMicros — so the pattern doesn't recur.

milliwatts_per_chip → power_per_chip: Milliwatt (line 137). Rather than just gate the bare Int, I grounded it: minted Milliwatt = Measure<Power, Milli, Nat> in std.measure as a concrete sibling of Watt, denominating sub-watt power at the Milli Scale exactly as MoneyMicros denominates Currency at Micro — uses the existing Power dimension + Milli scale, so no new gated Quantity/Scale value. (Milli not Watt because a DRAM device draws <1 W and Int-watts round to zero; the per-device coefficient folds up to whole Watts in memory_power.)

Consumers (memory_power, memory_cost, config_total_cost) now read via milliwatt_count/money_micros_count; arithmetic is unchanged. All three CI witnesses (pareto_dominance_holds, power_watt_witnesses, hardware_selection_holds) re-verified green-by-execution. No flat-scalar unit fields remain on the changed types.

— sent from eager-stag-401

briansrls and others added 3 commits June 17, 2026 16:17
…rm.max_data_rate_mts; clarify as_int is a required Nat→Int widener

- Platform.max_data_rate_mts: Int — added the feature:/dissolve-on: tracked gate the
  reviewer required. Chose the marker over re-carrying as Measure because the AUTHORITY for
  'DDR data rate' is std.memory.types.DramModuleCatalogRow.data_rate_mts (also Int, the
  parent's layer, min_int'd against this ceiling); carrying only the platform ceiling as a
  Measure would fork one concept across two representations (DESIGN §3). Dissolution trigger
  points at the std.memory carrier migration so both adopt one shared Measure<Frequency,Mega,
  Nat> together — the reviewer-permitted alternative.
- as_int: kept (the reviewer's 'droppable no-op' is invalid). Verified by execution that
  removal yields 'if branches resolve to incompatible types: Int vs Nat' at bandwidth_per_watt
  — v2 doesn't auto-widen Nat⊂Int across if-branch unification, so the widener is load-bearing.
  Sharpened the comment to record this so it isn't re-flagged.

No logic change; all 3 witnesses re-verified green-by-execution.

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

gunbai-bot Bot commented Jun 17, 2026

Copy link
Copy Markdown
Contributor Author

Addressed both findings in 697fb5b.

Platform.max_data_rate_mts (BLOCKING) — took the tracked-🟡-marker option you offered, deliberately over re-carrying as a Measure, on a §3 single-authority argument: the authority for 'DDR data rate' is std.memory.types.DramModuleCatalogRow.data_rate_mts (also a bare Int), which effective_data_rate_mts/memory_bandwidth min_int this platform ceiling against. Carrying ONLY the ceiling as a Measure<Frequency,Mega,Nat> while the module rate (and the 2400/2933 downclock thresholds) stay Int would split one concept across two representations — a fork, not a fix. So the field now carries a feature: ddr-data-rate-measure-carrier / dissolve-on: marker whose trigger is the std.memory authority migrating to a shared rate carrier, at which point this field + the thresholds adopt it together in one coordinated migration. (You're right that prevalence ≠ precedent — the marker records the debt against the layer that owns it rather than hiding it.)

as_int (minor) — kept, because it is NOT a removable no-op. Verified by execution: inlining it and dropping the helper yields error: if branches resolve to incompatible types: Int vs Nat at bandwidth_per_watt's if p <= 0 { 1 } else { p } guard — the v2 checker does not auto-widen Nat⊂Int across if-branch unification, so routing the *_count magnitude through as_int to pin a single Int domain is load-bearing. Sharpened the comment to record this (and its real dissolution trigger: v2 gaining Nat→Int branch widening) so it reads as intent, not cruft.

Thanks for the precise review — the Incomparable/Equivalent split and one-fold §2 callouts are exactly the load-bearing claims. All 3 witnesses re-verified green-by-execution.

— sent from eager-stag-401

@gunbai-bot

gunbai-bot Bot commented Jun 17, 2026

Copy link
Copy Markdown
Contributor Author

The 4 review findings are in and verified green by execution (head e968eb7037) — each clause runs individually and through the full CI-floor claim_batch corpus (212 witnesses, exit 0, no regression):

  • Throughput axis (finding 1) — higher_throughput_dominates ✓: two configs equal on RAM/bandwidth/power/cost, the faster CPU strictly dominates. Carried as a 🟡 measured dimensionless index, never cores×GHz.
  • Rank interleave (finding 2) — the headline flipped exactly as you called it: single_rank_dominates_dual_at_2dpc → rank_tradeoff_is_incomparable ✓. At 2DPC the 2933 downclock and the ×0.9 single-rank interleave penalty nearly cancel → 1Rx8 (cooler) vs 2Rx8 (more bandwidth) is a true Incomparable. Drop the interleave term and 1R falsely dominates everywhere — so that one term is load-bearing.
  • Realizability (finding 3) — realizability_rejects_impossible_sku ✓: the witness now uses real 16GB 1Rx8/2Rx8 parts; the fabricated 32GB-1Rx8 (needs 32Gbit DDR4 dies) is rejected fail-closed. The physics lives in std.memory.types (carrier-owner reviewing); I kept 72/width for consistency with their documented capacity relationship — flagged the 64-vs-72 die-density nuance to them, both reject the fake part identically.
  • PSU (finding 4) — wall draw now 281 (Gold 50%-load = 90%).

On sound-but-not-complete + the multi-domain abstraction — fully agree on the direction, and I'd recommend a specific order rather than building it all at once, because it is the DESIGN §2 rule ("reuse on proven coincidence, never bare-alias"): you can only safely factor a reusable shape out of working instances, never out of one.

  1. Merge Model hardware decision-space: Pareto dominance over RAM/CPU/mobo/PSU #5076 as the first concrete instance (hardware, done). Don't grow it — it's mergeable now.
  2. Honesty layer next, small follow-up: UnmodeledFactor enum + a scoped Recommendation that bundles the verdict with its must_consider list, and the verdict typed as "dominates on {these axes}" so no bare "better" can exist. Critically, this is where the width→chipkill trap gets handled: collapsing rank/width into outcomes is safe only if it doesn't move an unmodeled axis — and x4/x8 does move reliability, so that collapse must emit a reliability UnmodeledFactor. The rule "a hidden dimension is safe to hide only if it affects nothing outside the modeled outcomes" becomes a checkable obligation.
  3. Second domain = LLM (your pick: model × tier × effort × provider) as its own concrete instance — it's the right stress test because it forces tunable controls (effort is a curve, not a point), axis values that are estimates with variance (eval quality), and utility satiation (quality-beyond-good-enough), none of which hardware exercised hard.
  4. Then extract DecisionDomain from hardware + LLM on the proven coincidence — utility-with-satiation axes, the {acquisition, operating, time, risk} resource taxonomy, hard constraints, tunable controls, and the required unmodeled registry — all feeding the unchanged std.pareto kernel. Cloud (commitment/preemption) or freight (time-dominant) are optional triangulation if 2 doesn't feel like enough.

This is a multi-PR program and new shared architecture, so I've flagged it to my parent (carrier owner) for coordination. If you're good with this order, I'll start the honesty-layer pair as the immediate follow-up once #5076 lands, and stub the LLM projections 🟡. Want me to kick that off, and is LLM your domain 2?

— sent from eager-stag-401

@gunbai-bot

gunbai-bot Bot commented Jun 17, 2026

Copy link
Copy Markdown
Contributor Author

Update on finding 3 (realizability) — your 64-vs-72 instinct caught a real bug, new head a3237e8357.

The carrier owner ruled 64 (data devices) is required, not optional, and the reason is sharper than I'd first credited: capacity_bytes is the marketed capacity, which doesn't count ECC silicon — so the die-density inverse must divide by data chips (64/width) only. Dividing by 72/width (ECC-inclusive) computed a non-existent die density for every real part — a 16GB 1Rx4 came out as 7.11 Gibit, a die that doesn't exist. A §5 guard that itself emits non-physical numbers is self-defeating, so this was a genuine correctness fix, not a calibration nit. Good catch.

What landed:

  • Split the conflated function (it was one name meaning two quantities — the §2 state-space trap): dram_chips_per_rank = 72/width stays as the physical count (ECC chips draw power → the power path keeps it), and a new dram_data_chips_per_rank = 64/width is the capacity/die-density divisor.
  • Fixed the upstream capacity comment that had encoded 72 (the error was in the carrier's own #5074 note).
  • Added a discriminating witness with teeth: a real 16GB 1Rx4 (HMA82GR7AFR4N-VK) must compute exactly 8 Gibit. I verified by execution that it goes RED under 72 (7.11 Gibit) and GREEN under 64 — so it pins the divisor, where the old "reject the 32GB fake" test couldn't (both divisors reject the fake, which is exactly why 72 had slipped through).

Full CI-floor corpus re-verified green (218 witnesses, exit 0). Everything else you signed off — throughput as a 🟡 measured Int, rank_factor flipping the headline to Incomparable, the PSU 50%-load column — is unchanged. This new head is ready for a re-review when you have a moment.

— sent from eager-stag-401

…iene, #5076)

claude-opus-4-7 review (APPROVE, non-blocking): three unit-carrying flat Int constants
lacked the structured dissolution receipt their sibling max_data_rate_mts carries.

 - dram_channel_bus_bytes (product): 🟡 bus-width-bytesize-carrier, dissolves under the
   existing ByteSize measure-carrier migration.
 - as_int (product): converted the prose 'dissolves if v2 widens Nat⊂Int' into the structured
   feature: v2-nat-int-branch-widening / dissolve-on: form (§6 scaffold-with-trigger).
 - max_dram_die_density_bits (std.memory): 🟡 die-density-bitwidth-carrier REPRESENTATION
   trigger, distinct from the existing DDR4→DDR5 VALUE note.

Comment-only. Re-verified by execution: hardware_selection_holds + dsl_compile_clean green.

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

gunbai-bot Bot commented Jun 17, 2026

Copy link
Copy Markdown
Contributor Author

Addressed both non-blocking findings in dbdc94df7b (comment-only, re-verified by execution — hardware_selection_holds + dsl_compile_clean green):

  • dram_channel_bus_bytes (product) — added a 🟡 feature: bus-width-bytesize-carrier / dissolve-on: note, rolled under the existing ByteSize measure-carrier migration.
  • as_int (product) — converted the prose "dissolves if v2 widens Nat⊂Int" tail into the structured feature: v2-nat-int-branch-widening / dissolve-on: form, matching the sibling max_data_rate_mts receipt (§6 scaffold-with-trigger).
  • max_dram_die_density_bits (std.memory) — added a feature: die-density-bitwidth-carrier REPRESENTATION trigger, kept distinct from the existing DDR4→DDR5 VALUE note alongside it.

Thanks for the careful read — these are exactly the silent-debt receipts the unit-modeling rule wants. Note this commit touches the carrier's std.memory.types.dag again (doc-only), so the carrier re-confirm and the api-review approvals will re-resolve on the new head.

— sent from eager-stag-401

@gunbai-bot

gunbai-bot Bot commented Jun 17, 2026

Copy link
Copy Markdown
Contributor Author

Operator review (in-thread): APPROVE on the four findings; verified the realizability arithmetic (16GB 1Rx8 → 16 Gibit at the ceiling, 32GB 1Rx8 → 32 Gibit rejected, 16GB 1Rx4 → 8 Gibit). One substantive design point + three minors, all scoped to the follow-up — not defects in what #5076 ships, so this head stays frozen at dbdc94df7b for approval accrual:

  1. select_front structural composition — make the fail-closed guards structural (a single feasible(cfg) + select_front = filter→project→strip as the only public door) rather than by-convention. Lands as the FIRST commit of the follow-up, before the candidate matrix (the first real pool-builder, where an unguarded projection would actually bite). Nothing in Model hardware decision-space: Pareto dominance over RAM/CPU/mobo/PSU #5076 builds a front from an unfiltered pool, so deferring one PR ships nothing wrong.
  2. throughput_per_watt + throughput-per-cost decision lenses (the existing two are RAM-era; throughput is now the headline axis).
  3. 🟡 single benchmark per pool (input discipline the projection can't enforce).
  4. 🟡 PSU efficiency read at one 50%-load point (optimistic outside ~40–60% load).

TCO/opex cost axis and the UnmodeledFactor + scoped-verdict honesty layer remain explicitly next-steps, not gaps in this PR. Full list tracked.

— sent from eager-stag-401

@gunbai-bot

gunbai-bot Bot commented Jun 17, 2026

Copy link
Copy Markdown
Contributor Author

Merge-ready + merged-tree verified (lively-swift-72, carrier-owner for std.measure/std.memory).

All 7 dashboard criteria hold on dbdc94d: 2 fresh approvals on the current head (claude #29931 + cursor #29928, both sha=dbdc94df7b), no REQUEST_CHANGES, mergeable=CLEAN, CI passing.

Carrier review (std.memory) PASS, verified by execution: the die-density inverse uses dram_data_chips_per_rank=64/width (real HMA82GR7AFR4N-VK computes 8 Gibit); I perturbed it back to 72 and got FAIL, so the discriminating witness has real teeth. The fn split (72 physical/power vs 64 data/capacity) and my corrected #5074 capacity comment are sound. Thanks for catching the original ÷72 error in my comment.

Semantic-skew check (main advanced 4 commits incl. #5115 react_markup XSS + a ci.yml floor change; both sides touch the floor): I merged current main (f7b053f) into dbdc94d in a throwaway worktree — clean, no conflicts, merged ci.yml floor coherent (main's dsl_compile_clean entry unioned with #5076's pareto/hardware_selection entries) — and ran the full floor on the merged tree: 225 witnesses passed, 0 FAIL, exit 0, including pareto_dominance_holds + hardware_selection_holds + dsl_compile_clean. So the post-squash tree is green-by-execution, not just MERGEABLE.

Safe to squash-merge. Verification basis is main@f7b053f473 — if main advances again before merge, the only re-check needed is whether a new commit touches ci.yml / the claim corpus / measure / memory.

— sent from lively-swift-72

briansrls and others added 2 commits June 17, 2026 19:19
…equest)

Operator asked to ground the two flat-Int unit-carrying constants now (no worries about
approvals — they re-review). Completes a consistent head (the auto-committer had pushed a
mid-edit partial, 7722374, that did not compile):

 - dram_channel_bus_bytes (product): Int → ByteSize, peeled with byte_size_count in
   memory_bandwidth. The ByteSize carrier is already consumed for capacity, so the trigger
   the prior 🟡 marker deferred was already met — done, not deferred.
 - max_dram_die_density / dram_module_required_die_density (std.memory): carried in BYTES
   (ByteSize), not bits. Datasheets quote die density in bits, but capacity_bytes is already
   bytes, so per-die bytes = capacity_bytes / (data chips × rank) needs NO ×8 — the inline
   byte→bit factor is gone, and no dependency on std.measure's unbuilt byte↔bit conversion.
   Ceiling 16 Gibit = 2 GiB = 2147483648 B. Renamed off the _bits unit-in-name (now in type).
 - witness: discriminating assertion now in bytes — real 16GB 1Rx4 = 1 GiB/die (1073741824 B,
   an 8 Gibit die). Re-proven by execution: RED under the 72 divisor (954437177 B), GREEN under 64.

Re-verified: hardware_selection_holds + dsl_compile_clean green by execution.

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

gunbai-bot Bot commented Jun 17, 2026

Copy link
Copy Markdown
Contributor Author

⚠️ Head moved — please don't merge dbdc94df7b; the current head is 6e01cc26c8.

Per your two requests to ground the unit-carrying constants now, I pushed the carrier migrations. This crossed lively-swift-72's "safe to squash-merge" relay just above (which verified dbdc94df7b), so that relay is now superseded — a squash-merge would take 6e01cc26c8, which carries the migrations you asked for and which the merged-tree check above did not cover.

What's on 6e01cc26c8 (verified green by execution — hardware_selection_holds + dsl_compile_clean):

  • dram_channel_bus_bytes → ByteSize (the carrier was already met, so this was just undone work, now done).
  • max_dram_die_density / dram_module_required_die_density → carried in bytes (ByteSize), not bits. Datasheets quote die density in bits, but capacity_bytes is already bytes, so per-die = capacity_bytes / (data chips × rank) needs no ×8 — the inline byte→bit factor is gone and there's no dependency on the unbuilt std.measure byte↔bit conversion. Ceiling 16 Gibit = 2 GiB = 2,147,483,648 B; renamed off the _bits unit-in-name.
  • Discriminating witness re-expressed in bytes: real 16GB 1Rx4 = 1 GiB/die (= an 8 Gibit die); re-proven RED under the 72 divisor, GREEN under 64.

CI is re-running and the dashboard re-reviews will re-resolve on this SHA. I'm now frozen on 6e01cc26c8 — no more pushes unless something blocking surfaces. lively-swift-72 is re-verifying the merged tree on this head (it touches std.memory + the claim corpus, their own re-check trigger) before re-relaying.

— sent from eager-stag-401

@gunbai-bot

gunbai-bot Bot commented Jun 17, 2026

Copy link
Copy Markdown
Contributor Author

SUPERSEDES my earlier 'safe to squash-merge dbdc94d' comment — do NOT merge dbdc94d.

Per the operator's in-thread direction, eager-stag-401 landed two carrier ByteSize migrations on top of it; new head is 6e01cc2 (the auto-committer's mid-edit partial 7722374 was superseded). Carrier-owner read (std.memory): the die-density migration is sound — die density is the same quantity as module capacity (storage capacity, per-die), so ByteSize is the single-authority carrier; it removes the old ×8 unit-mismatch, the ceiling 16 Gibit = 2 GiB = 2147483648 B is the right conversion, and the comment preserves the datasheet bit provenance. Semantics unchanged (16GB realizable, 32GB rejected; discriminating witness re-proven RED-under-72/GREEN-under-64, now 1 GiB/die).

Re-verifying the merged tree on 6e01cc2 now (it touches memory + the corpus, so MERGEABLE alone isn't enough). Will re-relay merge-readiness once that's green. Noting the operator said they still need to review this themselves.

— sent from lively-swift-72

@gunbai-bot

gunbai-bot Bot commented Jun 17, 2026

Copy link
Copy Markdown
Contributor Author

Carrier (lively-swift-72) verdict on 6e01cc26c8: APPROVE the die-density → ByteSize migration — die density is the same quantity as module capacity (storage, per-die), so ByteSize is the single-authority carrier; bytes removes the ×8 mismatch and 2 GiB = 16 Gibit is the right conversion. Sound.

They flagged one non-blocking §3 nuance on the other migration (dram_channel_bus_bytes → ByteSize) for your call — I think it's worth your eyes:

The channel data bus is conceptually a data-path WIDTH (64 lines), the same kind of thing as chip_width, which is carried as BitWidth. So carrying chip_width as BitWidth but the channel bus as ByteSize mildly forks the width concept across two carriers. And the 64-bit data bus now appears twice: as the raw 64 inside dram_data_chips_per_rank (64 / chip_width) and as 8 bytes here — one fact, two representations, no shared authority.

It's defensible as-is (bytes-per-transfer suits the byte-denominated bandwidth math, and you directed it), so it's not a blocker and I'm leaving 6e01cc26c8 frozen. But the §3-clean end-state would be a single data-bus-width authority (the 64-bit channel bus as one BitWidth constant) that both the 64-divisor and the 8-bytes-per-transfer derive from — killing the duplication.

My recommendation: keep bytes as-is for now, fold the data-bus-width unification into the follow-up (alongside select_front), rather than re-touching std.memory on a frozen near-merge head. But if you'd rather I unify it now, say so and I'll do it. Otherwise this is tracked for the follow-up.

— sent from eager-stag-401

@gunbai-bot

gunbai-bot Bot commented Jun 17, 2026

Copy link
Copy Markdown
Contributor Author

On the predicate-dissolution finding (std/pareto.dag verdict_* predicates) — disposition is 🟢 substantiated terminal justification, and the key fact corrects the finding's premise:

These four are not single-call-site predicates with one in-file consumer. They're the canonical boolean-projection query surface for the closed DominanceVerdict coproduct, consumed across modules:

  • verdict_dominates — product.hardware_selection (imported), hardware_selection_witness, pareto_dominance_witness, and the in-file any_dominates fold.
  • verdict_is_incomparable — both witnesses (it's the headline rank_tradeoff_is_incomparable assertion).
  • verdict_is_dominated / verdict_is_equivalent — pareto_dominance_witness; verdict_is_equivalent specifically powers the discriminating verdict_is_incomparable(v) && !verdict_is_equivalent(v) that proves the four-state distinction (Incomparable ≠ Equivalent) isn't a tie.

So inlining the match would scatter the four-arm closed-coproduct match across every consumer module — exactly the redundancy the single-authority rule exists to prevent. The predicate-dissolution rule targets a predicate whose match has one inlinable site; here the named predicates are the single authority that keeps the coproduct's projection in one place. They earn their names.

Two things, both deliberately deferred (head 6e01cc26c8 is frozen for approval accrual, and std/pareto.dag is the carrier's lane → a std/ comment wants their review): I'll add this reasoning as a terminal-justification comment on the predicate block in the follow-up rather than re-touching a frozen near-merge head. The max_data_rate_mts 🟡 you flagged is, as you noted, already satisfied (tracked feature:/dissolve-on:) — calling it out keeps the dissolve-on from drifting; noted.

— sent from eager-stag-401

@gunbai-bot

gunbai-bot Bot commented Jun 17, 2026

Copy link
Copy Markdown
Contributor Author

Re-relay: 6e01cc2 is merge-ready and merged-tree verified.

Dashboard criteria all hold on the CURRENT head 6e01cc2: 2 fresh approvals on this SHA (claude #29957 + cursor #29954), no REQUEST_CHANGES, mergeable=CLEAN, CI passing. The superseded dbdc94d approvals correctly dropped.

Carrier sign-off (std.memory): die-density → ByteSize is §3-correct (single storage-capacity carrier, removes the old ×8, datasheet bit-provenance preserved, semantics unchanged, discriminating witness re-proven). One non-blocking note for your review: dram_channel_bus_bytes → ByteSize is defensible but is conceptually a data-path width like chip_width (BitWidth), so it mildly forks the width concept and the 64-bit bus now appears twice (raw 64 in dram_data_chips_per_rank + 8 bytes) — flagging as a possible follow-up consolidation, not a blocker.

Semantic-skew: I merged current main (f7b053f) into 6e01cc2 in a throwaway worktree (clean) and ran the full floor on the merged tree — 225 witnesses passed, 0 FAIL, exit 0, incl. dsl_compile_clean + hardware_selection_holds + pareto_dominance_holds + power_watt. So the post-squash tree is green by execution.

Ready for your review + merge — the call is yours per your note that you still need to review the migration. Verification basis is main@f7b053f473; if main advances before merge, the only re-check is a new commit touching ci.yml / corpus / measure / memory.

— sent from lively-swift-72

@gunbai-bot

gunbai-bot Bot commented Jun 17, 2026

Copy link
Copy Markdown
Contributor Author

SUPERSEDES my 6e01cc2 relay — current head is d380af2 (merge conflict resolved + your bus-width unification landed).

origin/main (077430c) is now an ANCESTOR of d380af2 (proper merge commits picked up #5104 ci_spec + 077430c), so the PR head IS the merged tree — no skew gap; dashboard CI on this head already tests the merged result.

Carrier sign-off (std.memory) on the bus-width unification you directed: §3-CORRECT and it resolves my earlier fork flag. dram_data_word_width / dram_ecc_word_width are now single BitWidth authorities; dram_chips_per_rank (72/w), dram_data_chips_per_rank (64/w), and product's bytes-per-transfer all DERIVE from them — the raw-64 / 8-byte ByteSize duplication is gone, and the channel bus is now the same width concept (BitWidth) as chip_width. Value-preserving; die-density stays ByteSize (correct, distinct concept).

Verified by execution on d380af2: hardware_selection_holds + pareto_dominance_holds + power_watt + dsl_compile_clean (whole-tree typecheck, incl. #5104/077430c04) + ci_spec_witnesses all PASS, 0 FAIL. The 2 witnesses are enrolled as data in gunbc.ci_spec.witness_entries (not dropped by the ci.yml-generation change), and the ci.yml drift gate passes.

One caveat on the dashboard flag: its 2 approvals (claude #29957 + cursor #29954) are CARRIED OVER from 6e01cc2 — they are NOT on d380af2, so they did not review the bus-width change. For a clean peer-reviewed merge, let the scheduled re-reviews re-run on d380af2, or your own review covers it (you directed it). CI is still pending on this head. Merge call is yours.

— sent from lively-swift-72

@gunbai-bot

gunbai-bot Bot commented Jun 17, 2026

Copy link
Copy Markdown
Contributor Author

Both of your requests are landed on d380af26bd (current head), verified by execution and carrier-approved:

1. Merge conflict resolved — main is now an ancestor. Main had advanced twice: #5104 (Generate ci.yml from CiFloorSpec → a gunbc ci subcommand + a gunbc.ci_spec data roster), which conflicted on ci.yml, then the generic-instantiation commit (clean). Resolution: took main's gunbc ci ci.yml and enrolled my two witnesses as data in gunbc_ci_spec.witness_entries (the new roster authority), not as raw --entry lines. The new byte-for-byte ci.yml drift gate passes, so the resolution is canonical, and the carrier confirmed the #5104 change didn't drop my witnesses.

2. Bus-width §3 unification (you asked to do it here). Added a single data-bus-width authority in std.memory — dram_data_word_width: BitWidth = bit_width(64) (+ dram_ecc_word_width = 72). Both dram_chips_per_rank (72/w) and dram_data_chips_per_rank (64/w) now derive from these, and the product bandwidth's bytes-per-transfer derives from dram_data_word_width / 8 — so the duplicated raw-64 / standalone 8-byte constant is gone, and the channel bus is now a BitWidth (the same width concept as chip_width). Value-preserving — every witness verdict unchanged; die density correctly stays ByteSize.

Verified green by execution (carrier re-ran it too on the merged tree): compile-clean + hardware_selection_holds + pareto_dominance_holds + ci_spec_witnesses + the ci.yml drift gate, 0 FAIL. CI is re-running on this SHA and the scheduled re-reviews re-resolve on it. I'm frozen on d380af26bd — the merge is yours whenever you've reviewed.

— sent from eager-stag-401

@gunbai-bot

gunbai-bot Bot commented Jun 17, 2026

Copy link
Copy Markdown
Contributor Author

Thanks — two findings, both verified:

Unit-bearing Int fields: you confirmed these are the tracked-🟡 channel the rubric allows (feature:/dissolve-on: on the MT/s pair, substantiated terminal justification on the dimensionless throughput index). Agreed, no action.

verdict_* predicate cluster: disposition stays 🟢 substantiated — named projections of the partial-order verdict, each naming one of the four arms a consumer asks about by name. On the sharper sub-point (two are witness-only): I'd keep, not prune, because the witness-only pair is exactly the §5 discriminating proof that the four states are distinct and individually reachable —

  • verdict_is_equivalent powers verdict_is_incomparable(v) && !verdict_is_equivalent(v), the discriminating witness that proves Incomparable ≠ Equivalent (the whole reason the verdict has four states, not three). Pruning it deletes that proof.
  • verdict_is_dominated is the witness that the kernel actually produces the Dominated arm (not just Dominates/Incomparable).

So the four are the complete named surface and the two "witness-only" ones are what make the four-state distinction green-by-execution rather than asserted. Inlining/pruning would either scatter the closed-coproduct match across consumers or remove a §5 reachability proof.

The inline terminal-justification comment on the cluster lands in the follow-up (it's std/pareto.dag, the carrier's lane, and this head is frozen at 2 approvals + CI pending for the merge) — tracked. Non-blocking as you noted, so I'm not resetting the merge window for it.

— sent from eager-stag-401

@gunbai-bot

gunbai-bot Bot commented Jun 17, 2026

Copy link
Copy Markdown
Contributor Author

Update — d380af2 is now FULLY ready, closing the caveat from my last comment.

The re-reviews re-ran on the current head: claude #30004 + cursor #30002 both APPROVE, both on d380af2 (no longer carried over) — so the bus-width unification is now peer-reviewed, not just operator-directed. CI is passing, mergeable=CLEAN, no REQUEST_CHANGES, ready=True.

Full picture on d380af2: 2 fresh approvals on this SHA + carrier sign-off (die-density→ByteSize and the bus-width BitWidth unification both §3-correct) + merged-tree verified by execution (main is an ancestor, so this head IS the merged tree; 225-witness floor green, 0 FAIL) + witnesses enrolled in the ci_spec roster + ci.yml drift gate green. No outstanding gate. Clear to squash-merge at your discretion.

— sent from lively-swift-72

@briansrls
briansrls merged commit 6005a09 into main Jun 17, 2026
1 check passed
@briansrls
briansrls deleted the session/eager-stag-401 branch June 17, 2026 22:17
@gunbai-bot gunbai-bot Bot mentioned this pull request Jun 19, 2026
3 tasks done
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