Copper realizes nets: a layer reference that cannot name a layer that is not there, and an identity join to the schematic

[briansrls]

The copper lane's second carrier, stacked on #8325.

It consumes product.compute_board.analog's ElectricalNet rather than minting a second net authority. A copper net and a schematic net that disagree would both still compile, which is the expensive kind of fork.

What copper adds that a schematic does not is where the conductor is — a position in the stackup. That join is what this PR makes unforgeable.

The layer reference

The obvious modelling is an Int index into the stackup's layer list, and it is wrong twice over:

• it is a positional citation of something the stackup already names structurally (DESIGN §3);
• it silently survives a stackup edit — insert a ply and every trace below it is now on a different layer, with nothing to notice.

So CopperLayerRef is sole_constructor, its mint is admit_callers-sealed to select_copper_layer, and the only route to one is selecting from an admitted stackup. Measured, not asserted:

sole_constructor type 'CopperLayerRef' cannot be constructed outside its defining module

A selected reference carries the function of the layer actually found, not a restatement of the request. The witness reads ordinals 0, 1 and 2 on a signal/ground/signal board, so a constant could not pass it. Out of range refuses with both the requested ordinal and the layer count rather than clamping to the nearest real layer — a clamp puts copper somewhere nobody asked for, which is fabricated plausible output with a board attached.

Selection is a fold with a counter because the substrate has no list-indexing primitive, and inventing one in a product module would be a std-shaped fact authored in the wrong place.

The schematic join

Admission is an identity join, not a count. The class it catches is quiet: a net is renamed and its copper keeps the old identity, so the board has a conductor belonging to nothing and a net with no conductor — and the count is unchanged, so a cardinality check reports both boards fine.

w_red_copper_naming_a_net_the_schematic_lacks_is_refused asserts count(rs) == count(intent.nets) before asserting the refusal, so the witness fails if the join ever degrades to counting.

A net realized twice refuses as well: two conductors claiming one name. Both offending rows are reported, since fixing one leaves the fork.

Admission and coverage are separate axes

An empty copper set is internally consistent — nothing wrong is realized — and covers nothing. If one arm carried both, an unrouted board would report as admitted-and-therefore-done. That is the completeness-versus-verdict conflation PcbBodyLayoutStanding already had to split into separate arms, and it is not being re-introduced one layer down.

Not yet modelled, so not implied

• Vias — so a net legitimately split across layers has no representation and refuses at this grain. That is the honest state, not a claim that split nets are invalid.
• Trace geometry and pads.

Evidence

9 witnesses green by execution, 4 of them RED controls (ordinal past the last layer; negative ordinal; net absent from the schematic; net realized twice).

Base

Stacked on #8325 (session/pcb-stackup), which is at 2/2 approvals. If #8325 merges first this reduces to the two new files.

[gunbai-bot]

Closed rather than deferred — review 52658 called it non-blocking, but it is the same class the stackup carrier closed one layer up, and leaving it would have meant shipping a seal that proves a reference came from some admitted stackup and never which one.

CopperLayerRef now carries the admitted stackup's declaration, and admit_copper takes the board it is admitting against, refusing any realization selected against another with RealizationSelectedAgainstAnotherStackup.

The control is built so that only the binding can catch it: other_board has the same layer count and the same function at every ordinal as three_layer, differing only in copper thickness and in the declaration admission judged. Ordinal and function therefore cannot distinguish the two references. The witness also asserts the native realization admits against the same board in the same run, so a refusal firing for any other reason fails the positive half.

Two defects surfaced while wiring it, both worth naming:

• A helper returned an AdmittedStackup by recursing on its own refusal arm — a fabricated totality wearing a cannot-happen comment. It is gone; every test now matches the Optional.
• The schematic-lacks control's cause match had gone non-exhaustive against the new variant. The substrate refused it rather than letting the arm silently widen, which is the wall doing its job.

10 witnesses green by execution, 5 of them RED controls.

— sent from zesty-heron-736

[cursor]

Bugbot is not enabled for your account, so this pull request was not reviewed.

Enable Bugbot in the Cursor dashboard to get automatic reviews on future PRs.

[gunbai-bot]

Fixed — the abstraction boundary finding is real, and I confirmed it against the tree before acting.

product.pcb.copper took an AnalogCircuitIntent. That looks harmless because the only field it read was .nets, but the type carries components, and ElectricalComponentInstance is a closed coproduct of resistor, capacitor and independent voltage source. A CPU, a BMC, a DDR slot, a regulator or a connector has no variant there.

So the copper carrier could only ever have acquired the Altra motherboard as a consumer by making the motherboard impersonate a three-part analog board — which is the milestone this lane exists to serve, failed at the type signature.

The correction is smaller than a module extraction, because ElectricalNet is already general: its members are component-and-terminal identities, which say nothing about what kind of component. Only the intent wrapper was specimen-bound. Copper now takes List<ElectricalNet>, and no net authority is forked — the same ElectricalNet is consumed, which was the original design's point.

The witness now depends on the decoupling rather than asserting it. Its fixture is a bare net roster with motherboard rail identities and no analog article at all; if the carrier still required an AnalogCircuitIntent, the file would not compile.

Declared next step, not done here: the homing is still wrong. ElectricalNet, NetIdentity and ElectricalTerminalRef are general concepts living in a specimen module and belong in a connectivity authority that both the analog article and this consume. That migration touches the article and its SPICE projection, so it is its own change rather than a rider on this one.

10 witnesses green by execution here; 15 on the stacked via branch after the same correction.

— sent from zesty-heron-736