Routing is not population, and copper is the ceiling

[gunbai-bot]

MOBO-X-2 selects a routed topology. ActiveDdrTopology could only say which channels are populated.

The gap

A design reading "four channels" could not distinguish:

• a board that routed four — permanently, in fabrication; from
• a board that routed eight and shipped four populated.

Those are different products with different escape problems, different layer counts, and different upgrade stories. The difference is invisible at the moment it is decided and expensive afterwards.

The subset law is the point

A board may leave a routed slot empty. It can never fill a slot it did not route. Stating the population as a topology in its own right is what makes the violating case writable, and therefore refusable — identity where cardinality was standing in, applied one level up.

What this PR corrected about itself

An earlier revision of this branch qualified the ROUTED topology by the active-channel authority, and that was a fail-open. The datasheet qualifies active channels; it says nothing of the form "a production motherboard may route exactly four, six or eight channel interfaces". Judging copper by that sentence produced two defects at once:

• a board routing eight and shipping two active under Production was ADMITTED — exactly what the predicate exists to refuse;
• a board routing five interfaces and operating a supported four-channel population was refused, which nothing in the source supports.

The routed side now carries a reachability law instead: every subset of a two-channel routed set has at most two active channels, and both are non-production, so no production-qualified population is reachable from it. That refuses the two-route board and leaves the five-route/four-active board admitted.

The old law was restored from c0333745f7 and run against the new counterexample to confirm the fail-open was real rather than theoretical.

Three further fail-opens closed, each proven by execution

Counterexamples were run against the previous module; each returned admitted.

1. A repeated active channel. [DDR0, DDR0, DDR1, DDR2] has list length four, so it reached the production-qualified arm, and every identity in it is routed, so the subset law could not see the repeat. A board naming four channels while populating three.
2. An active population with no DIMM positions at all. The empty-position refusal was applied only to the routed topology, and the position subset fold succeeds vacuously on an empty list.
3. The derived minimum's zero fallback. smallest_production_channel_count folded from init: 0 returning Int. Had no count been production-qualified, it would return 0, and routed_count >= 0 would admit every routed topology at precisely the moment no production population existed. It now returns Int?, and absence refuses through NoProductionQualifiedChannelCountExists.

Duplicate and empty-position refusal is now one law over the identity lists, so both carriers are judged by it rather than only the one it was first written for.

Routing and population now have two carriers

Both fields previously had type ActiveDdrTopology, so the same type — and a field spelled populated_channels — meant copper under routed and shipped memory under initially_populated. Meaning that depends on which field a value was stored in cannot be read locally, and nothing refuses the two being swapped at a call site. RoutedDdrTopology now carries its own field names.

A board is a population over time

MemoryPopulationLifecycle is ShipsWithProductionPopulation | BringUpThenFill. One production board may route eight channels, come up on two under bring-up intent, and ship on four. A single topology under a single intent cannot say that: judging it once as EngineeringBringUp establishes nothing about the shipped product, and judging it separately as Production yields a second verdict with no structural relation to the first. Both populations are judged under their own intent against one routed ceiling — and a lifecycle cannot launder a debug-only shipped population through the bring-up arm.

The admitted value retains its routing

The previous success constructor built a motherboard carrying only the initial active population, discarding the exact routed copper the admission had just checked. A downstream selector could not consume that result at all: it would have to keep the original input beside it and assert the two belong together — the adjacent-but-unbound shape this module exists to remove. RoutedDesignAdmission retains the admitted design, and a witness reads the routed set back out of it.

The routed path has its own admission coproduct rather than changing DesignAdmitted, so the legacy admit_design path (27 production references) is untouched and remains scheduled for its own delete-first migration.

Witnesses

14, up from 8 — including discriminating reds for all three proven fail-opens, both lifecycle arms, a control proving bring-up intent excuses the channel count but never the subset law, and a non-vacuity control.

Nothing was re-minted

Steps 2 and 3 of the reworked rung — active-count candidates from ActiveDdrChannelCount under production qualification, and the DPC axis as positions rather than a quantity — were already built here.

I had been about to author channels_per_socket: Nat and dimms_per_channel: Nat in the private strategy layer, which is exactly the error this module's own annotation warns about:

a generated range cannot express getting it wrong, because every count produces exactly one answer and it always looks correct.

Note on review

Two dashboard approvals landed on this file's earlier revisions: one ratifying the intent-on-routed law that turned out to be a fail-open, and one describing the revision containing the three fail-opens above as having no observed violations. Both were caught in side-chat review instead. Recorded here because the approvals are on the record and should not be read as evidence the laws were right.

[gunbai-bot]

Fixed in c0333745f7.

Review 58503 is correct and I want to be explicit that my first instinct — "but the probe ran green, so list_length resolved" — was the wrong rebuttal.

It did resolve, and w_RED_a_clean_routed_design_yields_no_subset_causes did execute. But it resolved through bare-name ambient lookup, not through a declared dependency. product.altra_motherboard.minimal_design:3 imports list_length from std.types explicitly, and so does every peer witness (altra_memory_controller_witness_test.dag:4, advertising_interface_witness_test.dag:21). This file was the outlier.

That matters for exactly the reasons a declared import exists: an undeclared name is free to bind to a different declaration when the namespace shifts, and it can be admitted by one entry point while another refuses it. Green by execution is not a substitute for the program stating what it depends on.

Re-verified after the change: the six witnesses still return exit 0 with list_length declared, and fold needs no import (it is a builtin — minimal_design.dag uses it without one).

On the three red checks — not addressed by this commit, because no commit can

All three failures on 788c4a4 are byte-identical rustup errors across three different runner slots:

error: $HOME differs from euid-obtained home directory: you may be using sudo
error: $HOME directory: /opt/actions-runner/srv1-NN/_work/_temp
error: euid-obtained home directory: /home/ghrunner

fabric-evidence on srv1-12, required-witnesses-build on srv1-10, rust-unit-tests on srv1-09.

#10011 shows the same signature on srv1-09, plus a related one on srv1-16 where the build lane refused with spawn rustfmt: No such file or directory — and that refusal explicitly records that rustfmt --version had executed successfully moments earlier from the same PATH, so it was removed mid-run rather than missing.

That is the toolchain-isolation hazard these jobs' own preamble warns about: runner slots sharing CARGO_HOME/RUSTUP_HOME on one host, where a concurrent install corrupts a run in flight. It is infrastructure, it will keep failing content-independently on those hosts, and it needs operator attention on the runner fleet rather than a diff.

Worth noting the substrate behaved well here — the regen phase refused with a located, typed cause naming the exact binary and the exact PATH it was resolved from, which is what let me separate a real finding from an ambient one instead of spending the afternoon "fixing" my own diff.

— sent from snappy-crab-469

[gunbai-bot]

Correcting the admission law — the previous version had a fail-open

Pushed in 25e3359ca3. This supersedes the law that review 58512 approved, and I want to be explicit that the approval endorsed a rule that was wrong.

The misreading

The previous admit_routed_design applied channel_count_is_production_qualified to the routed topology. The datasheet qualifies "active channels", the type is named **Active**DdrChannelCount, and the predicate's own comment says it is "a property of the CONFIGURATION". None of that licenses judging copper. There is no sentence of the form "a production motherboard may route exactly four, six or eight channel interfaces."

The fail-open, proven by execution

routed: 8 channels
initially active: 2 channels
intent: Production

The old law admitted this. Two active channels are debug/bring-up only — precisely what the predicate exists to refuse — and it passed, because the routed count was 8 and the populated count was never production-qualified at all.

Discriminating evidence, not assertion: restoring the old minimal_design.dag from c0333745f7 and running the new counterexample against it exits 1, while the corrected law exits 0 across all eight witnesses. The defect was real.

The over-refusal

A board routing five channel interfaces and operating a supported four-channel active population was refused, because five is not an admitted active count. Nothing in the source refuses that board. Unearned copper is a minimality question, not a vendor refusal. Now admitted, with its own witness.

My justification was answered, not overruled

I argued that qualifying only the population would let a board route two channels and pass by shipping a legal subset. It cannot: every subset of a two-channel routed set has at most two active channels, and 1 and 2 are both non-production, so no production-qualified population is reachable from it.

So the routed side gets a reachability law. Same verdict for the two-route board, from a true premise — and it stops producing the wrong verdict for five-route/four-active.

smallest_production_channel_count is folded out of the vendor roster rather than written as a literal 4, so if the datasheet ever admits a smaller production population this law follows it instead of disagreeing with it.

Two axes, two laws

axis	judged for
routed	named identities, duplicate-freedom, processor ceiling, positions, every active identity routed, production reachability
active	admitted count, declared intent, the vendor predicate under Production

On the approval

Review 58512 called the old behaviour "correctly qualifies the routed topology against intent" and cited altra_routed_vs_populated_witness_test.dag:80 as locking it in. That test was faithful to a rule derived from the wrong reading. The suite was green while admitting a design the datasheet refuses — which is the case for treating an approval as a hygiene floor rather than evidence the law is right. I flagged this placement in the PR body as the call I most wanted challenged; it needed the challenge.

Eight witnesses now, including the counterexample the previous suite could not express.

— sent from snappy-crab-469

[gunbai-bot]

On the non-blocking note about admit_design / AltraMinimalMotherboard standing alongside the new path — agreed, and I measured it rather than deferring on reflex, because DESIGN §3 is explicit that a surviving X is an attractor and delete-first is the default.

The census

Production (non-test) references to AltraMinimalMotherboard / altra_1p_minimum / admit_design, excluding minimal_design.dag itself:

15  dag/gunbc/product/altra_motherboard/placement.dag
12  dag/gunbc/product/altra_motherboard/pcb_world.dag

Plus altra_minimal_design_witness_test.dag (6 admit_design call sites) and altra_placement_witness_test.dag (which builds AltraMinimalMotherboard fixtures directly and drives admit_placement / placement_causes from altra_1p_minimum).

So AltraMinimalMotherboard is not a vestigial type — it is the carrier the placement and PCB-world modules consume. Retiring it is a replacement migration across three production modules and two witness suites, with admit_placement and placement_causes needing to take the routed/populated pair instead. That is its own cut program, not a tidy-up rider on a PR about the admission axis.

Why the additive state is defensible in the interim

The attractor risk DESIGN warns about is that nearby questions keep getting answered in the old vocabulary. The specific consumer that matters here is the reworked MOBO-X-2, and it consumes the new path only — RevARoutedMemoryDesign and admit_routed_design. So the decision this PR exists to inform is not being taken in the old vocabulary.

What is genuinely true and worth stating: admit_design still applies the vendor predicate to whatever topology it is handed, and AltraMinimalMotherboard carries a single topology that cannot distinguish routed from populated. A caller reaching for it today gets the pre-correction semantics. That is the real content of the debt, and it is a reason to sequence the migration rather than to widen this diff.

Not doing it here

Folding a three-module carrier migration into this PR would make the fail-open correction — which is the change under review and the one with executing evidence behind it — harder to review, and would mix a semantic fix with a mechanical one. I would rather land the corrected law and take the cut as its own change with its own census and its own witnesses.

— sent from snappy-crab-469

[gunbai-bot]

The remaining red — rust-unit-tests / compiler_tests::shell_service_unmodeled_output_key_refuses — is inherited from main, not caused here.

Attribution

Main's last fully-green run is fb481ae0f. The failure first appears at 4059156e49, which is #9886 — "XL-0-SERVICE: the service-emission path in 05_emit_rust binds stdout to every declared output field and does not box the error arm — it emits non-compiling Rust". The failing test is shell_service_unmodeled_output_key_refuses. Service emission changed; the shell-service test broke.

Main currently fails it on consecutive runs, e.g. 33603503036 (at ecda07108) and 33603137801 (at 4605989cf), both showing:

test compiler_tests::compiler_tests::shell_service_unmodeled_output_key_refuses ... FAILED
test result: FAILED. 644 passed; 1 failed; 141 ignored

This branch is merged with current main and reproduces it identically. This PR's diff is minimal_design.dag plus one witness test and cannot reach shell-service emission.

One caveat rather than a clean bisect: run 52aac48b6 reports the test not failing, but that run died in an earlier lane, so the test most likely never executed. Absence of the diagnostic is not evidence it passed, so I am not claiming 52aac48b6 as a green point.

A correction to my earlier comment

I said merging #10017 would clear this. That was wrong, and I stated it with more confidence than the evidence supported.

#10017 repaired the regen drift on compiler_tests.rs, and it did work — required-witnesses-build passes on this branch now, where it previously failed with regen FAIL generated surface drift: compiler_tests.rs, std_realization_schedule.rs. But the drift and this failing test are two different defects that happen to name the same artifact, and I conflated them. The merge was still worth doing; it just did not do the thing I said.

Status of this PR on its merits

required-witnesses-build passes and, on the previous run, required-witnesses-floor and witnesses both passed — so the eight witnesses for the corrected admission law, including the 8-routed/2-active fail-open counterexample, have executed in CI rather than only locally.

— sent from snappy-crab-469

[briansrls]

REQUEST_CHANGES at exact head 6190046fc44a6056505dd95f56aa6c183925326b.

The original intent-axis fail-open and five-route over-refusal are closed, but five source blockers remain:

1. RevARoutedMemoryDesign.routed still has type ActiveDdrTopology, whose own vocabulary is populated_channels. Routing and active population therefore remain one semantic carrier interpreted by field position. Introduce a routed wrapper or a neutral shared set with distinct routed/active wrappers.

2. The admitted arm erases the routed design: admit_routed_design returns DesignAdmitted { design: AltraMinimalMotherboard { memory: d.initially_populated, ... } }. The exact copper topology that was judged is absent from the accepted value. The success constructor must preserve the admitted RevARoutedMemoryDesign (and its lifecycle/intent), or downstream selection can no longer bind the routed fact this PR exists to expose.

3. There is still one initially_populated topology plus one intent, so the model cannot express one product that routes eight, brings up with two, then ships with a four/six/eight-channel production population. Add an explicit bring-up-versus-production lifecycle; judge the former under EngineeringBringUp, the latter under Production, and require both to be subsets of routed copper.

4. active_population_causes checks only count and intent. It does not run duplicate-channel, duplicate-position, or no-position validation on the active topology. Thus [DDR0, DDR0, DDR1, DDR2] counts as production four and an active topology with zero positions passes the positional subset vacuously. Apply structural topology validation to every active population and add discriminating REDs.

5. smallest_production_channel_count() uses numeric 0 as absence. If the vendor roster ever contains no production-qualified count, production_population_is_reachable becomes routed_count >= 0 and admits every route exactly when no production population exists. Return an Optional/coproduct and refuse the no-qualified-population arm; no numeric absence.

Refresh the PR body, which still describes the superseded intent-on-routed law and six-witness state. Current main is 7f71ee34094d9879ea06a69d25ac9f6186c3acb5; this head is one commit behind with merge base ecda0710810f6fca89b39a3fc808f42d8a9717fe. Compose after source repair and obtain terminal exact-head CI. Run 33604829516 is still in progress.