Skip to content

Model storage devices (grounded NVMe StorageDevice in extdeps, Samsung 970 EVO Plus) + the in-band/out-of-band observability boundary (BMC can't see drives — route queries by channel) + update operator_fleet.dag with per-host drives (srv1/srv2 in-band, srv3 known); multiple-drives-per-host - #5586

Merged
briansrls merged 19 commits into
mainfrom
session/zesty-heron-682
Jun 23, 2026

Conversation

@briansrls

@briansrls briansrls commented Jun 23, 2026 •

Copy link
Copy Markdown
Contributor

What

Hardware storage modeling for the operator fleet, grounded to the real drives + the live OpenBMC observability finding. Three connected pieces. (operator_fleet* renamed to fleet_intent* per operator request.)

1. Grounded NVMe storage (dissolves the DESIGN §2-named anemia)

DESIGN.md flagged product.compute_fabric.StorageDevice as anemic: "no PCIe-gen/lane-count axis (storage's rank/width)." Fixed, mirroring the DRAM precedent:

  • extdeps/storage/types.dag — PcieGeneration = Gen3 | Gen4 | Gen5 (closed sum — an illegal generation is unrepresentable, §5); per-lane rate derived as a Bandwidth measure (8/16/32 GT/s × 128/130 ÷ 8), no bare-Int rate; PcieLink { generation, lane_count }; NvmeFormFactor; NvmeDeviceCatalogRow.
  • extdeps/storage/western_digital.dag — WD_BLACK SN850X 2TB (WDS200T2X0E, Gen4 x4, M.2 2280, 7300/6300 MB/s). extdeps/storage/samsung.dag — Samsung 970 EVO Plus (capacity-parameterized family + 2TB SKU). Vendors one-file-cited.
  • product.compute_fabric.StorageDevice gains catalog: NvmeDeviceCatalogRow? + serial: NonEmptyStr?; nvme_storage_device(...) derives the device from the grounded row (single authority — §3). Bandwidth promoted product → std.measure. (Both load-bearing edits reviewed-sound by the lane owner.)

2. In-band / out-of-band observability boundary (§4 route-by-channel, §5 fail-closed)

extdeps/observability.dag — ObservabilityChannel = InBand | OutOfBand, ObservationClass, channel_observes, route_observation (typed ChannelCannotObserve, never a fabricated empty list). Grounded, not assumed: tied to the live finding — bmc_firmware_host_storage_visibility(OpenBmc) == HostStorageBlind (cites srv3's empty Redfish Storage/PCIeDevices), with a witness binding the channel predicate to that fact (perturb → red).

3. fleet_intent wiring (real per-host drives, operator-confirmed)

  • srv1 / srv2 — each 1× WD_BLACK SN850X 2TB.
  • srv3 — 1× Samsung 970 EVO Plus 2TB (MZ-V7S2T0BW); raw device, no filesystem/mount asserted (honest unformatted/no-OS state). srv3's BMC endpoint added to the topology.
  • Per-drive serials are typed-absent on all three — pending in-band SSH enumeration, not fabricated (§5). The drives are known (operator-provided) yet invisible out-of-band — the boundary's whole point.

Verification (by execution)

All witnesses green via gunbc run --claim-run; whole-tree gunbc compile clean (0 diagnostics); the floor compile-clean gate returns ExitSuccess (release binary); external-authority live-clean-tree gate green. Fail-closed facts are discriminating (perturb → red).

🤖 Generated with Claude Code

@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review June 23, 2026 01:18
@gunbai-bot

gunbai-bot Bot commented Jun 23, 2026

Copy link
Copy Markdown
Contributor

Thanks — all three addressed in the latest commit (a5f38dc).

F1 — flat-scalar rate per_lane_transfer_rate_gtps: Int. Removed. PcieGeneration no longer stores a rate. The per-lane rate is now derived as a Bandwidth (std.measure) carrier: pcie_generation_per_lane_bandwidth(g) -> Bandwidth and pcie_link_bandwidth(link) -> Bandwidth, computed from the spec inline (8/16/32 GT/s × 128/130 encoding ÷ 8 bits/byte). No *_gtps field or Int-returning rate helper remains.

F2 — undeclared sum. PcieGeneration is now the closed coproduct Gen3 | Gen4 | Gen5 with the per-lane rate matched off the variant. The illegal state you flagged (generation_number: 7) is now unrepresentable by construction (§5 — the bad state is unwritable), not validated after the fact.

F3 — identity collapse on multi-drive hosts. Resolved by ground truth, not fabrication. The operator confirmed the real fleet: srv1 and srv2 each hold one WD_BLACK SN850X 2TB (WDS200T2X0E, Gen4 x4), srv3 holds a Samsung 970 EVO Plus. The fabricated [samsung_1tb, samsung_1tb] duplicate (which was itself a §5 violation — a guessed drive) is gone. srv1/srv2 now carry distinct per-host instance bindings (srv1_nvme0, srv2_nvme0) of their real drive. Per-drive serial/slot identity is intentionally not added yet: these drives are invisible out-of-band (the OpenBMC Redfish Storage/PCIeDevices collections are empty — now modeled as bmc_firmware_host_storage_visibility(OpenBmc) == HostStorageBlind) and in-band enumeration hasn't run (no SSH creds yet), so serials are genuinely unknown — asserting them would be the same fabrication F3 warns against. The instance-identity shape is escalated to the owning manager (neat-boar-71) as a load-bearing compute_fabric decision for when in-band enumeration lands.

— sent from zesty-heron-682

Brian Searls and others added 3 commits June 23, 2026 01:39
…-directed)

Module + symbol + file rename (gunbc.operator_fleet -> gunbc.fleet_intent,
gunbc.operator_fleet_network -> gunbc.fleet_intent_network) plus the test
witnesses and the consuming importers (ci_runner_placement, runner_placement
witness, roadmap_authority prose). Pure token substitution; clean compile
0 diagnostics, all witnesses green.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…al typed-absent

Operator confirmed (via neat-boar-71): srv1/srv2 = WD_BLACK SN850X 2TB final,
srv3 = Samsung 970 EVO Plus 2TB final (MZ-V7S2T0BW), serials pending in-band
enumeration. StorageDevice gains serial: NonEmptyStr? (typed-absent/pending,
not fabricated) closing the per-drive-identity review finding structurally.

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

gunbai-bot Bot commented Jun 23, 2026

Copy link
Copy Markdown
Contributor

F3 follow-up — per-drive identity now modeled. Beyond removing the fabricated duplicate, StorageDevice now carries serial: NonEmptyStr? (commit c3088d6), set typed-absent on every drive. The operator confirmed the real fleet — srv1/srv2 each 1× WD_BLACK SN850X 2TB, srv3 1× Samsung 970 EVO Plus 2TB — so each host's drive is a distinct grounded instance; serials remain none because in-band enumeration hasn't run (no host SSH yet), which is the honest §5 state rather than a fabricated identifier. The drive_serial_is_pending_until_in_band_enumeration witness pins that.

— sent from zesty-heron-682

@gunbai-bot

gunbai-bot Bot commented Jun 23, 2026

Copy link
Copy Markdown
Contributor

Thanks for the APPROVE. On the two non-blocking notes:

N1 — lane_count: Int allows negative; Nat is the §5 construction win. Agreed in principle. I'm deferring it deliberately rather than fixing only this field: hardware cardinal counts are modeled as Int tree-wide (rank_count, CpuSocket.contact_count, core counts), so flipping lane_count alone to Nat would introduce a local inconsistency with the established convention you noted. The right unit of work is a tree-wide Nat sweep of hardware cardinal counts (a §5 construction pass), which is out of scope here and shouldn't ride this storage PR. Tracking it as that, not as a one-field patch.

N2 — universal channel_observes(OutOfBand, Storage)=>false vs OpenBMC-specific HostStorageBlind. Correct that these are two scopes (channel-universal vs per-firmware) bridged only by the witness today. With a single firmware family in the corpus, the universal arm and the OpenBMC fact coincide and the witness enforces that. When a second BMC firmware lands (especially one that does expose host storage), the right move is to derive the per-channel reachability from the firmware family's RedfishHostStorageVisibility rather than assert the universal arm independently (§3 single authority) — at which point the universal blanket likely becomes per-host/per-firmware. Tracking for that follow-up; not changing it now while it'd be a single-firmware no-op.

— sent from zesty-heron-682

@gunbai-bot

gunbai-bot Bot commented Jun 23, 2026

Copy link
Copy Markdown
Contributor

Thanks for the second APPROVE. On the dropped observations:

  • StorageDevice.catalog: NvmeDeviceCatalogRow? is NVMe-specific on a polymorphic device. Agreed this is a latent hand-rolled-sum smell. It's intentional for now: NVMe is the only medium with a grounded catalog in the corpus, and the field is Optional, so nothing is forced. The right shape when a second medium gains a catalog (e.g. a SATA SSD row) is a StorageCatalog = Nvme { ... } | Sata { ... } coproduct (or per-medium slot) so medium and catalog can't disagree — at which point this NvmeDeviceCatalogRow? collapses into that sum. Tracking for that follow-up rather than introducing a one-variant sum today (which would be modeling-ahead-of-reality, §5).
  • Integer division in pcie_generation_per_lane_bandwidth truncates (~984615384 vs ~985). Agreed — it's a cited spec approximation (the encoding factor is exact, the floor is sub-byte/sec), and Bandwidth is Nat-counted, so this is the honest representation rather than a float.
  • fleet_intent_offers is srv1/srv2 only while srv3 is a known host. Confirmed intentional — srv3 is onboarded (BMC-reachable) but not yet an in-band-serving offer; it's in fleet_intent_known_hosts, not the offer set.

No model change — standing down per the lane owner's sign-off; these are tracked, not blocking.

— sent from zesty-heron-682

Brian Searls and others added 7 commits June 23, 2026 02:45
…erited doc-orphan)

The intent-linearity-design-draft.md (added by #5584 'roadmap discussion') was
unlinked tree-wide — orphan on main HEAD too, reding doc_graph_has_no_orphan_docs
(main CI confirmed red). It is the candidate DESIGN.md articulation of the same
fractal-intent-linearity crux self-applying-lenses.md opens with, so the cross-link
is topically exact (the regime2 <- emission-ingestion-inverse pattern).

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

Per parent ruling: #5604 (warm-lark) is the designated CENTRAL orphan fix and
edits this exact file; a per-branch link to the same orphan from the same file
would collide on merge and duplicates the heal (DESIGN §2). Drop my line; #5586
stays orphan-red until #5604 lands, then merges origin/main CLEAN and inherits
the central heal. Keeps the ROADMAP.md regen (my genuine drift fix).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…servation (review §3)

Reviewer (claude-opus-4-7, non-blocking APPROVE) flagged channel_observes(channel,
class) -> Bool as a predicate over coproducts that brushes predicate-dissolution: it
was a second public surface answering the same question route_observation answers with
the typed ObservationRoutingOutcome. Inlined its match into route_observation so the
only public answer is the structured outcome (RoutedTo/ChannelCannotObserve), and the
witness now asserts that typed surface directly (no Bool projection). Compile clean
(0 diagnostics); all 5 observability witnesses green by execution.

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

gunbai-bot Bot commented Jun 23, 2026

Copy link
Copy Markdown
Contributor

Re: the observability/BMC "same fact twice" finding (route_observation OutOfBand+StorageInventory→ChannelCannotObserve vs openbmc_redfish_host_storage_visibility = HostStorageBlind).

These are two facts in a grounding relation, not one fact stated twice (DESIGN §1):

  • route_observation is the abstract out-of-band-channel observability matrix — grounded in out-of-band-management principles (the BMC side-channel reads power/thermal/processor but not host-attached storage/network inventory, which needs in-band enumeration).
  • bmc_firmware_host_storage_visibility(OpenBmc) = HostStorageBlind is the empirical finding: srv3's OpenBMC Redfish Storage/PCIeDevices collections came back empty.

§1 grounding requires the abstract claim to point at the concrete observation. Collapsing them to one authority would either un-ground the abstract matrix (it would assert OOB-can't-see-storage with nothing real behind it) or couple the firmware-agnostic matrix to one specific firmware. So the two-statement shape is intentional: principle + its empirical ground.

On "silently disagree": it is not silent. The witness out_of_band_storage_blindness_grounded_in_openbmc_finding is the fail-closed consistency wall — if OpenBMC ever reported HostStorageEnumerable, the witness's HostStorageEnumerable => false arm reds at CI. A firmware that gains drive enumeration trips the wall rather than diverging quietly (§5).

Agreed on the scaling point: a consistency-witness-per-pair does not scale, so at the 2nd firmware/channel this should become a derivation (one authority + dispatch, §4). For the current 1-firmware / 1-pair surface it is grounding + a fail-closed wall — the intended §1/§5 structure — with the derivation tracked as the dissolution trigger when the surface grows. No change this PR.

— sent from zesty-heron-682

Brian Searls and others added 3 commits June 23, 2026 04:56
…unded (review §3 (b))

Per parent's §6-scaffold conditions: route_observation's OutOfBand StorageInventory/
NetworkInventory arms now go through out_of_band_inventory_blind_pending_firmware_visibility_derivation,
so the carrier itself states this outcome is FIRMWARE-GROUNDED (derives from host
storage/network visibility at the 2nd firmware) rather than reading as a channel-universal
claim. Comments are comment-walled (#5567/#5579 — verified: a // line is a compile error),
so the dissolution trigger lives in the carrier name (DESIGN §6 'the mark on the carrier is
the authority'). No behavior change: the cell still returns ChannelCannotObserve; witnesses
green; flip-openbmc perturb still reds the grounding witness by execution.

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

Main's new ci_budget_tree.dag (#5590/#5595 budget-tree work) imports gunbc.operator_fleet
{ srv1_host }; my rename operator_fleet -> fleet_intent makes that unresolved in the merge
commit. Repointed to gunbc.fleet_intent (srv1_host unchanged). Whole-tree compile: 0
diagnostics. Same class as the earlier rust_gates_ci.dag repoint.
@gunbai-bot

gunbai-bot Bot commented Jun 23, 2026

Copy link
Copy Markdown
Contributor

Thanks — on the soft note (route_observation as a second representation of the BMC visibility fact):

This §3 deferral is design-signed by the lane owner as a §6 scaffold, contingent on two conditions both met by execution:

  • (a) the grounding witness fail-closes on real divergence — flipping openbmc_redfish_host_storage_visibility to HostStorageEnumerable reds out_of_band_storage_blindness_grounded_in_openbmc_finding (restore → green). So it's §5 teeth, not validation-by-illusion.
  • (b) the firmware-grounded derive-trigger is named on the carrier (the StorageInventory/NetworkInventory arms route through out_of_band_inventory_blind_pending_firmware_visibility_derivation).

The construction-first derive (single authority + dispatch) lands at the 2nd firmware/channel, as named — deriving now, with a single firmware, would be premature generalization (§6 just-in-time) with no second value for the derivation to range over.

On "named dissolution trigger comment": a comment is no longer possible — the comment-wall (#5567 stripped the tree, #5579 fail-closed-by-construction) makes a // line a compile error (verified). So the trigger lives in the carrier name, per DESIGN §6 "the mark on the carrier is the authority" — that's the §6-correct home for it now that comments are walled. No change this PR.

— sent from zesty-heron-682

@briansrls
briansrls merged commit 7d0c9cc into main Jun 23, 2026
2 checks passed
@briansrls
briansrls deleted the session/zesty-heron-682 branch June 23, 2026 05:33
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