MOTHERBOARD-MVP-0: grounded board interfaces with first SPICE and Verilog emission

[gunbai-bot]

Opens the .dag hardware-compiler program at one board subassembly: a two-rail power-good and reset interlock. One article is the authority, and SPICE and Verilog are projections of it — both emitting byte-exact source, both refusing before emitting a byte when the intent expresses something the target cannot honour.

The shape

                 product.compute_board.article
                 (one root: identity, analog, digital,
                  bonds, firmware, physical, manufacturing)
                        /                    \
        spice_projection                      verilog_projection
        (element letters, node 0,             (module/wire/assign,
         magnitude suffixes)                   identifier admission)

The article imports no projection module. An earlier revision had it holding a BoardSlice imported from the SPICE projection — SPICE NodeRefs, substrate symbols and value_lexeme: "10k" — so the supposed authority was shaped by one of its own emission targets, and "the article feeds every interface" was true only because one interface had already decided what the article looked like. product.compute_board.analog now carries the language-neutral electrical intent, and the model-standing carriers (ModelFidelity, ElectricalModelStanding, ComponentModelBinding) moved with it — they name no deck and no element letter, and an IBIS or Verilog-AMS projection needs the same facts.

Both emissions consume the article itself, not its extracted parts. Every earlier caller passed the identity and the circuit separately, so one article's identity paired with another's circuit was constructible and the receipt would name a board it does not describe. Receipts carry BoardArticleIdentity, not a flattened "name rev 0" label — the label made the join a string comparison over a spelling this repository happened to choose.

What is grounded

• Component values are typed magnitudes on std.measure's existing Resistance/Capacitance/ElectricPotentialDifference. "10k" and "100n" are gone from the model; SPICE derives the suffix, because a scale suffix is target syntax. No new quantity authority was needed.
• Terminals and nets are identities, so "is this terminal on that net" is a decidable join rather than a spelling coincidence between two independently authored strings.
• Electrical references are five relations, not one Ground — power return, signal reference, chassis bond, protective earth, shield termination. A mounting hole bonds to chassis only when a declared relation says so; a chassis bond is Proposed or Observed{observer}, never authored as unqualified fact.
• Core counts and memory ride HardwareThreadCount/ByteSize on both sides of the comparison in requirement_met.
• The Altra pin map is PUBLIC, and an earlier revision of this branch said it was not. That claim was reasoned from the reference board collateral being under NDA and never checked against the datasheet this repo already cited — a well-typed refusal, executed on the real path, defended by a passing witness, and false. What remains open is licensing (every datasheet page is footed Proprietary), not access.

Evidence

36 witnesses green by execution: article 7, readiness 14, SPICE 7, Verilog 8.

Both decks/modules are pinned by full byte equality, not string_contains, each with a discriminating RED that perturbs exactly one typed value and requires the bytes to change. Refusal controls cover: vendor subcircuit fidelity this profile cannot render, a missing binding (distinct from an absent model), a terminal on no net, driving an input, an undeclared signal reference, a reserved-word spelling, and a forbidden character.

The terminal-on-no-net refusal is the one worth naming: a floating terminal and a grounded one are different circuits, and defaulting the first to the second emits a deck that simulates cleanly and describes a different board.

Fixes carried

• spice_text_concat: list_append (free-monoid on String) → concat. This is what made the byte-exact receipt deliverable; an earlier revision of this PR body recorded it as owed.
• first_duplicate_designator was quadratic — 4926² compares at the real package population. Now two linear passes, membership-only maps that are never iterated, so ordering still comes from the designator list and the prior semantics (first designator in source order whose value repeats) are preserved exactly.

Not in this change — named so the gaps stay visible

• Verilog spelling still lives in the product projection. module, output wire, assign and endmodule are rendered in product.compute_board.verilog_projection; dag/extdeps/languages/verilog/ holds only subject.dag. That is a second Verilog authority beside the target layer and a real §3 violation. Identifier admission and the VerilogBinding spelling table are done; moving the bounded AST and serializer into the target layer is not.
• The firmware boundary is typed but half-strung. The trust split (development-unsigned vs production-signing-unavailable, simultaneous standings rather than alternatives) and typed start preconditions landed. boot_storage, reset_owner, console and recovery_path are still bare strings, there is no plane split (system firmware / TF-A / UEFI / BMC / CPLD), and no pinned public Jade source standings.
• No geometry, placement or routing. The pending causes are typed: RequiresSpatialAffineSubstrateLanded, RequiresExactSubMillimeterCoordinateQuantum, RequiresSpatial3ShapeTopology.
• No manufacturing artifact emission, no BOM or pick-and-place, no Ampere contact data.

Correction to an earlier version of this body

Three claims it made are false against this head and are withdrawn: that the byte-exact SPICE receipt was owed, that no Verilog emission existed, and that a coordinate-carrier signedness decision was open for the operator. Signedness is not open — SPATIAL-2 (#8091) decided it: Millimeter stays a nonnegative magnitude, SignedMillimeterComponent is the signed component on an oriented axis, and the coordinate/displacement distinction lives in Point vs Vector and their operations. The blocker is that the carrier has not landed, which is a different fact with a different remedy.

The one operator decision that remains: gunb-ai/gunbc is PUBLIC. NDA collateral cannot land in it and the publication thread records the Stage-0 placement gate as deleted with no replacement ontology selected. That blocks the Altra contact path independently of NDA access — signing is not sufficient.

🤖 Generated with Claude Code

[gunbai-bot]

Correction: the Altra pinout is public — I had this wrong

The PR as opened claimed the Altra per-contact map, power sequencing and admitted memory topologies were NDA-only, and refused on that basis. That was false. Pushed a correction.

I reasoned it from the true fact that Ampere's reference board collateral is under NDA, and never checked it against the datasheet this repository was already citing.

Read from the cited Altra Max Rev A1 datasheet (Issue 1.15, text extracted from the PDF), cross-checked against Issue 1.00 on a second host:

• §3 Mechanical Data — 77.080 mm × 67.000 mm, 4926-pin FCLGA
• §5 Pin Assignment — Sorted by Pin Number, Table 4, 35 sheets of PIN # → SIGNAL NAME (A5 VSS, B54 DDR4_DATA_67, AJ81 JTAG_SOC_TDO, AU69 PCIERCA7_RX13_M, …)
• §6.1 Reserved Pins — all 39 named by designator
• §6.2 Table 6 Signal Descriptions — width, direction, I/O type per signal
• Table 5 Pin Summary — 1960 signal + 2927 power/ground + 39 reserved = 4926
• §7 Electrical Specifications, §9 Power Supply Sequencing (SoC and PCP domains)

Actually NDA-bound: the reference board collateral — Mt. Jade / Mt. Collins / Mt. Bonnell / Mt. Snow motherboard design packages, plus UEFI, OpenBMC and CPLD source. Board designs, not package facts. Conflating the two produced the error.

What changed

The standing splits, and each half lands in the family whose owner can act on it:

standing	family	owner
ContactMapPubliclyAvailableNotIngested	design	us — unfinished ingestion
MissingUpstreamDesignCollateral (reference board)	collateral	business prerequisite

Table 5 is carried as its three parts rather than the total, because it cross-foots — a transcription that drops a group fails the sum instead of quietly shrinking the population it claims to cover.

Still open, and it is not availability

Every datasheet page is footed "Ampere Computing Proprietary", so transcribing its tables into this public repository is a licensing question. Unaffected by the pinout being downloadable. The public-repo decision therefore survives the correction — with a different reason attached, and a much narrower one.

Two reading traps, recorded in the module

• DDR4_/DDR5_/DDR6_/DDR7_ are channel indices 4–7, not memory generations. §6.2 groups them as DDR[0:7] across eight DDR4 channels; the shared rail is VDDQ_DDR4567.
• Table 4 excludes depopulated positions, so a row count from it is not the package population. Table 5 is the completeness authority.

Why I'm flagging this loudly rather than quietly fixing it

The old refusal was typed, located, executed on the real acceptance path, and defended by a passing witness — and false. Every mark of a grounded verdict, none of the grounding. No amount of test discipline catches that class; reading the document did. The module note keeps the incident, because the failure mode is more reusable than the fact.

12 witnesses green, including both corrected standings asserted together and the pin-summary cross-foot.

— sent from zesty-heron-736

[gunbai-bot]

review 51051 — all three findings taken, pushed

All three were correct §3 violations I introduced, two of them in the NDA-correction commit itself.

finding	fix
second ExternalAuthority for a URI extdeps.cpu.ampere already owns	imported and consumed
altra_fclga_4926_declared_contact_count re-authored 4926 beside the CpuSocket row	derived — altra_declared_contact_count() reads altra_max_m12830_catalog.socket.contact_count
AltraPackageFamily / AltraFcLga4926 a parallel package identity	enum deleted; PackageContactMap.socket is a CpuSocket

The floating-island characterisation was exactly right — a pin-map module with no import edge to the CPU catalog it claims to bound, joining its completeness check against a denominator free to drift from the socket fact. There is now a real import edge and one authority for the population. Counts move Nat → Int to join the socket fact without a cross-representation straddle.

SPICE: my diagnosis was wrong twice, and review 51047 repeated the first version back

Worth flagging directly, because the second approval (review 51047) records my spice_emit claim as confirmed. It should not be relied on — not through any fault of that review, but because a reviewer validating an author's framing is how a wrong claim acquires a second signature.

The sequence, all by execution:

1. First report: "spice_emit returns an unwrapped Optional where its signature declares String." Written up as a defect in that module.
2. Second: the real cause looked like my bug — the deck body is a Cons/Empty free monoid and this lane was passing a native [...] literal, so the emitter never saw a foldable deck. That bug was real and is fixed in this push. I then concluded the byte receipt was deliverable.
3. It is not. v2.extdeps.formats.spice's own golden fixture spice_rc_tran_deck passes both its witnesses untouched — and that same fixture returns a value string_contains rejects as a Variant when spice_emit is called on it from another module.

Same input, same function, different calling module, different result. So the seam is cross-module, not the deck and not the emitter's logic — materially different from, and more serious than, either earlier description. Not repaired here; it wants its own change with someone who knows the resolution path.

The witness asserts deck structure. The byte-exact receipt stays owed — it was briefly claimed as delivered in a working revision that never merged, and it is not claimed now.

15 witnesses green.

— sent from zesty-heron-736

[gunbai-bot]

Four side-channel findings: three taken, one declined with reasons

1. Quantity erasure in the satisfaction fold — taken, and it was the worst of the set

Satisfaction matched a component's justification tag against a requirement's capability tag, and never read the requirement's quantity. A one-core part justified as Compute satisfied a 128-core requirement.

What makes this worse than an ordinary bug: intent.dag's own note says "a requirement is the capability PLUS the quantity that makes it checkable" — and the fold discarded exactly that. The module contradicted its stated reason for existing, and every witness passed because they all asserted at tag grain too. A test suite agreeing with the defect it was written to catch.

CapabilityProvision is now separate from ComponentJustification — why a component is earned and what it supplies are different questions, and a component can get one right while getting the other wrong. Numeric requirements sum and compare; boolean-shaped ones demand every declared sub-facility, so a management device with power control and console but no recovery path no longer satisfies a contract asking for recovery.

Discriminating pair: 127 vs 128 cores — same justification, same part label, one core apart. Falsified — restoring the tag-matching arm reds that witness and nothing else.

2. Reference-board collateral fused into the package standing — taken

altra_reference_board_collateral_standing returned MissingUpstreamDesignCollateral as a PackageContactMapStanding, so reference-board absence rendered as a statement about the package contact map.

That is the same fusion I corrected in prose two commits ago and then re-committed at the type level one function down. ReferenceBoardCollateralStanding is now its own type with its own route into the collateral family; neither subject can inhabit the other's type.

The Rev A1 datasheet also joins the module's ExternalModelScope further_citations — it is the authority for the corrected pin/signal/sequencing facts, and leaving it out left them grounded in prose while the scope cited only the brief and the NDA portal.

3. SPICE model wall — already closed in the prior commit

ModelFidelity is explicit and VendorSubcircuit refuses via ModelFidelityNotEmittable, since this projection emits no .SUBCKT/.MODEL binding. The richer shape proposed (analysis/assumptions on the ideal arm) is a reasonable extension but the defect itself is closed.

4. Manufacturing-medium grain — declined, with reasons

Gerber layer data, job metadata and drill already travel as distinct CarriedInCompanionArtifact rows rather than a single yes/no roster — the split is present at carriage grain, which is the grain that decides which artifact set a factory receives. A finer artifact-set model is real future work; it is not a defect in what is here. Happy to be shown otherwise if the intended distinction is finer than carriage location.

19 witnesses green.

— sent from zesty-heron-736

[gunbai-bot]

review 51062 — hard blocker taken, third finding declined with reasons

1 & 2. HardwareThreadCount — correct, fixed

A core count is a hardware thread count, std.measure.HardwareThreadCount already exists for it, and extdeps.cpu.types CpuModelCatalogRow.threads already uses it. Typing the requirement as bare Nat and the provision as bare Int was the parallel representation §3 forbids, with no marker justifying a raw scalar. Both sides of the comparison now carry the measure and the fold runs in Nat.

The paired type-safety point was real and slightly worse than described: ProvidesCores.cores: Int could hold -5, and since provisions are summed, a negative provision would have reduced a board's apparent core count below what its other components legitimately supply — not merely admitted a nonsense value in isolation.

Also fixed, unflagged: ProvidesNetworkPaths and ProvidesBootStoragePaths moved Int → Nat. The argument that condemned the core field condemns these identically, and fixing only the flagged instance would leave the class half-closed.

3. Prose blobs — declined, and here is the boundary as I read it

Taking the finding seriously rather than resting on "you called it defensible":

• The citation is already typed — ExternalAuthority rows, referenced by ExternalModelScope, with the datasheet added to further_citations last commit precisely so the corrected facts aren't grounded in prose alone.
• The counts are already typed — Table 5's 1960/2927/39 are data rows that cross-foot by execution, which is why the witness can assert the sum rather than a reader trusting the sentence.
• What remains in prose is the fetch receipt — verified-on date, which sections were read, what was quoted — and there is no carrier for it. ExternalAuthority is { uri: Uri } and nothing else; no verified_at, no quoted-fact receipt type exists anywhere in std/ or extdeps/.

Minting one here would be a new generic with a single consumer, which is exactly the artifact I deleted from this PR three commits ago on the same reasoning. So the honest state is: a typed fetch-receipt carrier is a real gap, it would have more than one consumer across extdeps/ (every "verified live" note in the corpus wants it), and it belongs in its own change with those consumers.

Worth noting the scale is corpus-normal rather than unusual to this PR — extdeps/external_authority.dag's own external_model_scope_law is a prose blob of comparable size in the citation machinery itself. That's not a defence of the pattern, just evidence that fixing it is a corpus-level move, not a per-PR one.

19 witnesses green.

— sent from zesty-heron-736