From 3e8ea308b294ae285c3697cd159b2a1671000146 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 5 Sep 2026 21:58:50 +0000 Subject: [PATCH 01/11] Model the Ethernet link mode and the SFF-8636 leg coding: a part number is not a link contract Two 400G QSFP-DD to 4x100G breakout cables (FS order FS260902769849, part QDD-400G-4QPC015) link and run stably at half their purchased rate between a MikroTik CRS812 and ConnectX-7 NICs. The legs' EEPROMs report extended compliance 0x0B, which attests 25G-per-lane modes; nothing in them attests 100GBASE-CR2, so the NIC refuses to enable 100G_2X. The corpus could not state any of that. "100G" was one Bandwidth, so 100GBASE-CR4 (4x25G NRZ) and 100GBASE-CR2 (2x50G PAM4) were indistinguishable -- one spelling, two contracts, DESIGN section 3's meaning fork. And a cable leg's coding, which is what actually decides the negotiated rate, was unmodelled entirely. extdeps.ethernet.link_mode makes the aggregate DERIVED and never authored, so "100G" is unsayable as a primitive fact. A lane carries three distinct numbers -- service rate, encoded rate, symbol rate -- and they are three fields, not one. std.measure gains SymbolRate for the baud axis, because the first draft of this work typed a baud field as Bandwidth: the module written to prevent the units conflation committed it. extdeps.transceiver.sff_8636 owns the EEPROM field layout, reading BOTH extended-compliance codes (bytes 192 and 116), because SFF-8024 lets a multi-application module report the encoding of its primary application -- a predicate over one code and one encoding byte is not a soundness proof. Its assessment is relative to a REQUESTED mode and splits three ways: contradictory under the observed profile, insufficient evidence for the requested mode, or not understood by this decoder. The delivered cable lands on the second, which is strictly weaker and strictly more defensible than calling its EEPROM self-contradictory. NOT ESTABLISHED, recorded rather than guessed: no clause attribution is carried on any mode row, since an unread clause number is a fabricated citation; the SFF-8024 code that attests 100GBASE-CR2 is not authored here for the same reason; byte 140 may hold the 0xFF escape rather than a rate, which needs the raw dump to settle; and stable 50G operation is evidence about 50G only -- it does not certify the 26.5625 GBd PAM4 path. NOT VERIFIED LOCALLY. Six attempts to typecheck this failed on the toolchain, never on the source: a pipeline-clobbered exit code, an installed gunbc that reds every section 4c annotation in the corpus, two memory-admission refusals, an OOM through the --entry path, and a dispatch that returned no output. CI is the instrument for this branch. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01AigrH3JpxgSJBmqHMBAr6W --- dag/extdeps/ethernet/link_mode.dag | 242 ++++++++++++++++++++++++++ dag/extdeps/transceiver/sff_8636.dag | 249 +++++++++++++++++++++++++++ dag/std/measure.dag | 21 +++ 3 files changed, 512 insertions(+) create mode 100644 dag/extdeps/ethernet/link_mode.dag create mode 100644 dag/extdeps/transceiver/sff_8636.dag diff --git a/dag/extdeps/ethernet/link_mode.dag b/dag/extdeps/ethernet/link_mode.dag new file mode 100644 index 00000000000..62001e47b3b --- /dev/null +++ b/dag/extdeps/ethernet/link_mode.dag @@ -0,0 +1,242 @@ +module extdeps.ethernet.link_mode + +import std.nat { Nat } +import std.types { Bool, String } +import std.measure { Bandwidth, bandwidth, bandwidth_count, SymbolRate, symbol_rate, symbol_rate_count } +import std.decl_ref { DeclarationRef, WholeDeclaration } +import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef } +import extdeps.uri { Uri, Https } + +// AN ETHERNET LINK MODE IS A LANE COUNT, A PER-LANE RATE AND A MODULATION -- NEVER AN AGGREGATE. +// +// This module exists because of a measured loss. Two 400G QSFP-DD to 4x100G QSFP56 breakout cables +// (FS order FS260902769849, part QDD-400G-4QPC015) were bought to carry 100G per leg between a +// MikroTik CRS812 and ConnectX-7 NICs. Each leg links, is stable, passes a jumbo ping -- and runs at +// HALF the purchased rate. The cause is that "100G" names two materially different link modes: +// +// 100GBASE-CR4 -- 4 lanes x 25G, NRZ +// 100GBASE-CR2 -- 2 lanes x 50G, PAM4 +// +// Both aggregate to 100 Gb/s. A model carrying only the aggregate cannot tell them apart, so it +// cannot state what was bought, what arrived, or that the two disagree. That is the DESIGN section 3 +// meaning fork exactly: one spelling, two contracts, and the difference is invisible in the field +// because the wrong one still links. +// +// SO THE AGGREGATE IS DERIVED AND NEVER AUTHORED. `link_mode_aggregate` is the only way to get a +// total rate, which makes "100G" unsayable as a primitive fact. A consumer that wants to compare +// capability must compare MODES; comparing aggregates is the defect this module makes unwritable. +// +// WHAT IS NOT ESTABLISHED, recorded rather than guessed: the per-mode IEEE clause attribution. The +// CR4 and CR2 rows below are confidently 802.3bj Clause 92 and 802.3cd Clause 136 respectively, but +// the remaining rows were not read against a copy of the standard in this lane, so NO row carries a +// clause field at all -- an unread clause number is a fabricated citation. Binding each mode to its +// clause is owed work and its trigger is one reading of IEEE 802.3. + +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "ieee802.org/3/" + } +} + +// MODULATION, CLOSED. A third scheme is a row added here, and adding it makes every match below fail +// to compile until the new case is answered. +type Modulation = Nrz | Pam4 + +// BITS PER SYMBOL IS WHAT MODULATION MEANS, and it is the reason a lane's data rate and its baud +// rate are different numbers. A PAM4 lane carries two bits per symbol, so 50 Gb/s of data rides +// ~26.5625 GBd; an NRZ lane at 25 Gb/s rides ~25.78125 GBd. The EEPROM field that started this +// investigation reports a rate in Mb/s, so the modelled per-lane figure below is DATA rate. +fn modulation_bits_per_symbol(m: Modulation) -> Nat { + match m { + Nrz => 1 + Pam4 => 2 + } +} + +fn modulation_label(m: Modulation) -> String { + match m { + Nrz => "NRZ" + Pam4 => "PAM4" + } +} + +fn modulation_eq(a: Modulation, b: Modulation) -> Bool { + match a { + Nrz => match b { Nrz => true, Pam4 => false } + Pam4 => match b { Nrz => false, Pam4 => true } + } +} + +// LANE COUNT IS CLOSED, NOT A BARE INT. Ethernet copper PMDs are specified at 1, 2, 4 and 8 lanes; +// a bare Int admits 3 and 7, which name nothing and would have to be validated after the fact rather +// than refused by construction (DESIGN section 5). +type LaneCount = Lanes1 | Lanes2 | Lanes4 | Lanes8 + +fn lane_count_value(l: LaneCount) -> Nat { + match l { + Lanes1 => 1 + Lanes2 => 2 + Lanes4 => 4 + Lanes8 => 8 + } +} + +fn lane_count_eq(a: LaneCount, b: LaneCount) -> Bool { + lane_count_value(l: a) == lane_count_value(l: b) +} + +// A LANE CARRIES THREE DIFFERENT NUMBERS AND THEY MUST NOT BE ONE FIELD. +// +// The first version of this type had a single `per_lane_data_rate`, which is the very conflation the +// module was written to prevent -- caught in review, not by me. For one 100GBASE-CR2 lane: +// +// service rate 50 Gb/s what the PMD is NAMED for, after FEC and encoding overhead +// encoded rate 53.125 Gb/s bits actually on the wire, DERIVED below +// symbol rate 26.5625 GBd what the EEPROM's byte 140 is denominated in +// +// Only the first two are bits; the third is baud. Carrying one field forced a choice between them +// and silently made every consumer read whichever the author happened to mean. The symbol rate is +// authored rather than derived because it is the figure the specification tabulates and the figure +// the transceiver reports; deriving it would invert the direction of the citation. +type LinkMode sole_constructor { + lane_count: LaneCount + per_lane_service_rate: Bandwidth + per_lane_symbol_rate: SymbolRate + modulation: Modulation +} + +fn link_mode( + lane_count: LaneCount, + per_lane_service_rate: Bandwidth, + per_lane_symbol_rate: SymbolRate, + modulation: Modulation, +) -> LinkMode { + LinkMode { + lane_count: lane_count, + per_lane_service_rate: per_lane_service_rate, + per_lane_symbol_rate: per_lane_symbol_rate, + modulation: modulation, + } +} + +// THE ENCODED BIT RATE OF ONE LANE, derived from baud and modulation -- the bridge between the two +// units, stated once so no consumer has to multiply by hand and get the modulation factor wrong. +fn link_mode_lane_encoded_rate(m: LinkMode) -> Bandwidth { + bandwidth(symbol_rate_count(r: m.per_lane_symbol_rate) + * modulation_bits_per_symbol(m: m.modulation)) +} + +// THE DERIVED TOTAL. This is the only source of an aggregate rate in the corpus, and it is a +// function rather than a field so that no row can carry an aggregate that disagrees with its lanes. +fn link_mode_aggregate(m: LinkMode) -> Bandwidth { + bandwidth(lane_count_value(l: m.lane_count) * bandwidth_count(b: m.per_lane_service_rate)) +} + +// MODE EQUALITY IS ON ALL THREE AXES, WHICH IS THE WHOLE POINT. Two modes with the same aggregate +// are not the same mode, and `link_mode_eq` is what a compatibility check must call. A check written +// against `link_mode_aggregate` would pass the CR4-for-CR2 substitution that cost this fleet half its +// fabric -- see `hundred_gig_aggregate_collision` below, which exists to make that concrete. +fn link_mode_eq(a: LinkMode, b: LinkMode) -> Bool { + lane_count_eq(a: a.lane_count, b: b.lane_count) + && bandwidth_count(b: a.per_lane_service_rate) == bandwidth_count(b: b.per_lane_service_rate) + && symbol_rate_count(r: a.per_lane_symbol_rate) == symbol_rate_count(r: b.per_lane_symbol_rate) + && modulation_eq(a: a.modulation, b: b.modulation) +} + +// ================= THE NAMED COPPER MODES ================= +// +// Per-lane data rates are the nominal figures the PMDs are named for (25G, 50G), not the exact baud +// rates. The exact signalling rates -- 25.78125 GBd, 26.5625 GBd -- belong with the clause binding +// this module does not yet carry, and stating them as data rates here would conflate baud with bits. + +// SERVICE RATES: the figure the PMD name carries. +data lane_rate_25g: Bandwidth = bandwidth(25000000000) +data lane_rate_50g: Bandwidth = bandwidth(50000000000) + +// SYMBOL RATES: the figures the standard tabulates, exact rather than rounded. 25.78125 GBd is the +// 25G NRZ lane; 26.5625 GBd is the 50G PAM4 lane, which at 2 bits per symbol is the 53.125 Gb/s +// encoded rate. These are the numbers an EEPROM's byte 140 is expressing, and stating them exactly +// is what lets a decoded byte be compared to a mode instead of eyeballed. +data lane_baud_25g78125_nrz: SymbolRate = symbol_rate(25781250000) +data lane_baud_26g5625_pam4: SymbolRate = symbol_rate(26562500000) + +// 25GBASE-CR: one NRZ lane. What the ConnectX-7 falls back to. +data ieee_25gbase_cr: LinkMode = link_mode( + lane_count: Lanes1, per_lane_service_rate: lane_rate_25g, + per_lane_symbol_rate: lane_baud_25g78125_nrz, modulation: Nrz) + +// 50GBASE-CR2: two NRZ lanes. THIS IS THE MODE THE DELIVERED CABLE ACTUALLY NEGOTIATES, and it is +// stable -- which is precisely why the defect is expensive: it links, it pings clean at MTU 9000, +// and it tests green everywhere the fleet looks. +// +// WHAT THAT STABILITY DOES *NOT* ESTABLISH, corrected here after the claim was made too strongly +// once: operating in this mode does not certify operation in 100GBASE-CR2. These are different +// lanes at different bauds -- 25.78125 GBd NRZ against 26.5625 GBd PAM4 -- with a different +// insertion-loss budget, so a working 50G link is evidence about 50G and nothing else. The +// defensible record is that the tested configuration runs this mode and refuses the requested one; +// EEPROM coding is a CANDIDATE explanation, and the higher-rate path has never been demonstrated on +// this assembly. If the legs are recoded and still fail, this sentence is what stops that outcome +// from being a surprise. +data ieee_50gbase_cr2: LinkMode = link_mode( + lane_count: Lanes2, per_lane_service_rate: lane_rate_25g, + per_lane_symbol_rate: lane_baud_25g78125_nrz, modulation: Nrz) + +// 50GBASE-CR: one PAM4 lane. Same aggregate as 50GBASE-CR2, different mode -- the collision one +// rung down from the 100G one, and the reason lane count is carried rather than inferred. +data ieee_50gbase_cr: LinkMode = link_mode( + lane_count: Lanes1, per_lane_service_rate: lane_rate_50g, + per_lane_symbol_rate: lane_baud_26g5625_pam4, modulation: Pam4) + +// 100GBASE-CR4: four NRZ lanes. IEEE 802.3bj Clause 92. This is the mode the delivered cable's +// EEPROM claims (extended compliance byte 192 = 0x0B). +data ieee_100gbase_cr4: LinkMode = link_mode( + lane_count: Lanes4, per_lane_service_rate: lane_rate_25g, + per_lane_symbol_rate: lane_baud_25g78125_nrz, modulation: Nrz) + +// 100GBASE-CR2: two PAM4 lanes. IEEE 802.3cd Clause 136. This is the mode the breakout leg was +// PURCHASED to provide and the mode the ConnectX-7 requires before it will enable 100G_2X. +data ieee_100gbase_cr2: LinkMode = link_mode( + lane_count: Lanes2, per_lane_service_rate: lane_rate_50g, + per_lane_symbol_rate: lane_baud_26g5625_pam4, modulation: Pam4) + +// 200GBASE-CR4 and 400GBASE-CR8: the QSFP-DD trunk side of a breakout. +data ieee_200gbase_cr4: LinkMode = link_mode( + lane_count: Lanes4, per_lane_service_rate: lane_rate_50g, + per_lane_symbol_rate: lane_baud_26g5625_pam4, modulation: Pam4) + +data ieee_400gbase_cr8: LinkMode = link_mode( + lane_count: Lanes8, per_lane_service_rate: lane_rate_50g, + per_lane_symbol_rate: lane_baud_26g5625_pam4, modulation: Pam4) + +// THE COLLISION, STATED AS A COMPUTATION RATHER THAN A COMMENT. +// +// A DESIGN section 4c annotation cannot be checked -- no Accepted program reads one -- so the claim +// that these two modes collide on aggregate is made here as something a witness can execute. It is +// true today and must stay true: it is the reason `link_mode_eq` compares three axes, and if it ever +// went false the justification for this module's shape would have silently evaporated. +fn hundred_gig_aggregate_collision() -> Bool { + bandwidth_count(b: link_mode_aggregate(m: ieee_100gbase_cr4)) + == bandwidth_count(b: link_mode_aggregate(m: ieee_100gbase_cr2)) + && !link_mode_eq(a: ieee_100gbase_cr4, b: ieee_100gbase_cr2) +} + +fn render_link_mode(m: LinkMode) -> String { + to_string(lane_count_value(l: m.lane_count)) + + "x" + + to_string(bandwidth_count(b: m.per_lane_service_rate)) + + " " + + modulation_label(m: m.modulation) +} + +data extdeps_model_scope: ExternalModelScope = ExternalModelScope { + subject: ExternalSubjectRef { + declaration: DeclarationRef { + module_path: "extdeps.ethernet.link_mode", + decl_name: "LinkMode", + field: WholeDeclaration + } + }, + first_citation: extdeps_external_authority_anchor, + further_citations: [] +} diff --git a/dag/extdeps/transceiver/sff_8636.dag b/dag/extdeps/transceiver/sff_8636.dag new file mode 100644 index 00000000000..e408746290b --- /dev/null +++ b/dag/extdeps/transceiver/sff_8636.dag @@ -0,0 +1,249 @@ +module extdeps.transceiver.sff_8636 + +import std.nat { Nat } +import std.types { Bool, String, List } +import std.measure { SymbolRate, symbol_rate, symbol_rate_count } +import std.decl_ref { DeclarationRef, WholeDeclaration } +import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef } +import extdeps.uri { Uri, Https } +import extdeps.ethernet.link_mode { + LinkMode, Modulation, Nrz, Pam4, modulation_eq, link_mode_eq, + ieee_25gbase_cr, ieee_100gbase_cr4, +} + +// THE MANAGEMENT EEPROM OF A QSFP MODULE OR CABLE LEG -- AND THE REASON A PART NUMBER IS NOT A LINK +// CONTRACT. +// +// The fact this module exists to carry is one nobody in this fleet knew until it cost half a fabric: +// a passive copper breakout cable is FIELD-PROGRAMMED. What rate a leg negotiates is decided by bytes +// in its EEPROM, not by the SKU on the invoice and not by the copper. Two legs of the same part +// number, flashed differently, are two different products. So an order placed against a part number +// alone is an order with the contract left blank. +// +// This is a SPECIFICATION module: it owns the SFF-8636 field layout and what the bytes mean. It owns +// no cable. A specific part is its own subject in its own vendor module, per DESIGN section 3's +// external upstream decomposition, and it carries a reading of these fields rather than redefining +// them. +// +// WHAT THIS MODULE MAY AND MAY NOT CONCLUDE. It reads bytes and reports findings about bytes. It +// does not certify hardware: no reading here establishes that a given assembly will carry a given +// mode, and a leg whose coding is impeccable can still fail electrically. +// +// THE OBSERVED DEFECT MUST STAY REPRESENTABLE. An earlier head said the delivered cable "would have +// had no constructor", which is backwards: a model that cannot record a contradictory EEPROM cannot +// record the incident it exists to handle. Inventory and receipt reconciliation must be able to hold +// missing, malformed and rejected components. What loses its constructor is an ADMITTED PURCHASE +// lacking sufficient evidence -- never the observation of a bad part. + +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "snia.org/technology-communities/sff/specifications" + } +} + +// ================= BYTE 128: IDENTIFIER ================= +// +// Unmodelled codes are CARRIED, not refused. An identifier this lane has not read from SFF-8024 is a +// gap in our reading, not a defect in the module -- refusing it would make the corpus unable to +// record a part it can plainly observe. This is a typed, located carrier and not a widening +// fallback: nothing downstream may treat `IdentifierUnmodelled` as any particular module type. +type TransceiverIdentifier + = QsfpPlus + | Qsfp28 + | QsfpDd + | IdentifierUnmodelled { code: Nat } + +fn transceiver_identifier_from_byte(code: Nat) -> TransceiverIdentifier { + if code == 13 { + QsfpPlus + } else if code == 17 { + Qsfp28 + } else if code == 24 { + QsfpDd + } else { + IdentifierUnmodelled { code: code } + } +} + +// ================= BYTE 139: ENCODING ================= +// +// The encoding byte is what carries modulation. SFF-8636 added the PAM4 value (0x08) when 50G-per- +// lane PMDs arrived; the older 64B/66B value (0x05) implies NRZ line signalling. +type Sff8636Encoding + = EncodingUnspecified + | Encoding64b66b + | EncodingPam4 + | EncodingUnmodelled { code: Nat } + +fn sff8636_encoding_from_byte(code: Nat) -> Sff8636Encoding { + if code == 0 { + EncodingUnspecified + } else if code == 5 { + Encoding64b66b + } else if code == 8 { + EncodingPam4 + } else { + EncodingUnmodelled { code: code } + } +} + +// The modulation an encoding implies, or Absent where the byte does not decide one. Absent is a +// refusal to guess, not a default: a coding whose modulation is undecidable cannot be checked for +// consistency, and the constructor below treats that as unverifiable rather than as agreement. +fn sff8636_encoding_modulation(e: Sff8636Encoding) -> Modulation? { + match e { + Encoding64b66b => Present { value: Nrz } + EncodingPam4 => Present { value: Pam4 } + EncodingUnspecified => none + EncodingUnmodelled { code: c } => none + } +} + +// ================= BYTE 140: NOMINAL SIGNALLING RATE (BAUD) ================= +// +// BYTE 140 IS DENOMINATED IN 100 MBd -- SYMBOLS, NOT BITS. The first version of this module typed it +// as Bandwidth, which is the same units conflation the sibling link_mode module exists to prevent, +// authored inside the module written to prevent it. It carries SymbolRate now, so the mistake is a +// type error rather than a reading error. +// +// The trap is partly upstream: `ethtool -m` labels this field "BR, nominal" and prints Mb/s, so a +// reader who trusts the tool's unit inherits the conflation. The specification's unit governs here. +// +// 0xFF IS AN ESCAPE, NOT A RATE. SFF-8636 specifies that 255 means the nominal rate exceeds what one +// byte can express and the real figure lives in byte 222, in units of 250 MBd. +// +// THIS MATTERS FOR THE CABLE THAT PROMPTED THE MODULE, and is flagged as a hypothesis rather than a +// finding. `ethtool -m` reported "BR, nominal: 25500 Mb/s" on the delivered legs. 25500 is exactly +// 255 x 100 -- the escape value multiplied out and rendered as though it were a measurement. Whether +// byte 140 actually holds 0xFF, and what byte 222 then says, was NOT read in this lane: it needs the +// raw dump (`ethtool -m raw on`), not the decoded view. Until that is read, a leg whose byte +// 140 is 255 carries NominalRateEscaped and NOT a 25.5 GBd claim, because recording an escape marker +// as a measurement is the fabrication this whole subject exists to catch. +type Sff8636NominalRate + = NominalRateDirect { rate: SymbolRate } + | NominalRateEscaped + +fn sff8636_nominal_rate_from_byte140(code: Nat) -> Sff8636NominalRate { + if code == 255 { + NominalRateEscaped + } else { + NominalRateDirect { rate: symbol_rate(code * 100000000) } + } +} + +// Byte 222, the extended field the escape points at, in units of 250 MBd. +fn sff8636_nominal_rate_from_byte222(code: Nat) -> SymbolRate { + symbol_rate(code * 250000000) +} + +// ================= BYTE 192: EXTENDED SPECIFICATION COMPLIANCE ================= +// +// This is the byte the ConnectX-7 reads to decide which rates to enable, so it is the byte the whole +// incident turns on. The code is carried as its raw value with the modes it attests, where this lane +// has read them. +// +// WHAT IS NOT ESTABLISHED: the code that WOULD attest 100GBASE-CR2. SFF-8024 assigns one, this lane +// did not read it against a copy of the specification, and writing a plausible value here would be a +// fabricated citation of exactly the kind that caused the problem being modelled. The refusal below +// does not need it -- internal inconsistency is decidable without knowing the right answer -- so the +// gap blocks nothing except the eventual positive control. Its trigger is one reading of SFF-8024 +// Table 4-4. +type ExtendedCompliance sole_constructor { + code: Nat + attested_modes: List +} + +// 0x0B. Read from the delivered cable, and its meaning read from the ethtool decode the operator +// captured: "100GBASE-CR4 or 25GBASE-CR CA-L". Both attested modes are NRZ at 25G per lane, which is +// what makes the PAM4 encoding byte beside it a contradiction rather than a nuance. +data ext_compliance_0x0b: ExtendedCompliance = ExtendedCompliance { + code: 11, + attested_modes: [ieee_100gbase_cr4, ieee_25gbase_cr], +} + +// ================= THE LEG CODING, AND WHAT ITS BYTES CAN AND CANNOT DECIDE ================= +// +// A coding carries BOTH extended-compliance codes. SFF-8636 provides a secondary code at byte 116 +// beside the primary at byte 192, and SFF-8024 permits a module supporting several encodings to +// report the one belonging to its PRIMARY PRODUCT APPLICATION. The first version of this module read +// only byte 192 and byte 139 and declared their disagreement a contradiction; that predicate is not +// sound over a multi-application module, and the overreach was caught in review. +type Sff8636LegCoding sole_constructor { + identifier: TransceiverIdentifier + primary_compliance: ExtendedCompliance + secondary_compliance: ExtendedCompliance? + encoding: Sff8636Encoding + nominal_rate: Sff8636NominalRate +} + +// THREE FINDINGS, NOT ONE REFUSAL. Collapsing these would let the strongest claim absorb the weakest +// evidence, which is how a decoder's ignorance turns into an accusation against a part. +// +// Contradictory -- every attested mode under the OBSERVED profile disagrees with the +// encoding byte. A claim about these bytes, not about the hardware. +// InsufficientEvidence -- nothing in the observed bytes attests the mode the operator requires. +// THIS IS WHERE THE DELIVERED FS CABLE LANDS: 0x0B attests 25G-per-lane +// modes and nothing attests 100GBASE-CR2, which is why the ConnectX-7 +// refuses to enable 100G_2X. It is a strictly weaker and strictly more +// defensible finding than "this EEPROM is self-contradictory". +// NotUnderstood -- the decoder has no row for what it read. An unknown code must never +// become a proven contradiction merely because this model lacks a row for +// it; that is the decoder's gap, not the module's defect. +type Sff8636CodingFinding + = CodingConsistentWithRequest { coding: Sff8636LegCoding } + | CodingContradictsEncoding { encoding_modulation: Modulation, attested_mode: LinkMode } + | CodingInsufficientForRequestedMode { requested: LinkMode, coding: Sff8636LegCoding } + | CodingNotUnderstood { encoding: Sff8636Encoding } + +// Every mode attested by either compliance code. The union is the observable profile; reading only +// the primary is what made the earlier predicate unsound. +fn sff8636_attested_modes(coding: Sff8636LegCoding) -> List { + match coding.secondary_compliance { + Present { value: sec } => + concat(coding.primary_compliance.attested_modes, sec.attested_modes) + Absent => coding.primary_compliance.attested_modes + } +} + +// THE QUESTION IS ALWAYS RELATIVE TO A REQUESTED MODE. There is no such thing as a coding that is +// "correct" in the abstract -- only one that does or does not attest what this endpoint pair needs. +// Asking it without a request is what let the earlier version imagine it could judge a part alone. +fn sff8636_assess_leg_coding( + coding: Sff8636LegCoding, + requested: LinkMode, +) -> Sff8636CodingFinding { + let attested = sff8636_attested_modes(coding: coding) + if any(attested, m => link_mode_eq(a: m, b: requested)) { + CodingConsistentWithRequest { coding: coding } + } else { + match sff8636_encoding_modulation(e: coding.encoding) { + Absent => CodingInsufficientForRequestedMode { requested: requested, coding: coding } + Present { value: enc_mod } => { + let agreeing = filter(attested, m => modulation_eq(a: m.modulation, b: enc_mod)) + match agreeing.first() { + Absent => + match attested.first() { + Present { value: bad } => + CodingContradictsEncoding { encoding_modulation: enc_mod, attested_mode: bad } + Absent => CodingNotUnderstood { encoding: coding.encoding } + } + Present { value: ok } => + CodingInsufficientForRequestedMode { requested: requested, coding: coding } + } + } + } + } +} + +data extdeps_model_scope: ExternalModelScope = ExternalModelScope { + subject: ExternalSubjectRef { + declaration: DeclarationRef { + module_path: "extdeps.transceiver.sff_8636", + decl_name: "Sff8636LegCoding", + field: WholeDeclaration + } + }, + first_citation: extdeps_external_authority_anchor, + further_citations: [] +} diff --git a/dag/std/measure.dag b/dag/std/measure.dag index 3ef836d4999..ba08b24b297 100644 --- a/dag/std/measure.dag +++ b/dag/std/measure.dag @@ -1135,6 +1135,27 @@ fn packet_rate_count(r: PacketRate) -> Nat { measure_count(r) } +// A SYMBOL RATE (BAUD): SYMBOLS PER SECOND, NOT BITS PER SECOND. On the same Frequency axis as +// PacketRate and at the same One scale, and distinct from Bandwidth for the reason the whole family +// exists: a modulated lane carries more than one bit per symbol, so baud and bits/s are different +// numbers about the same wire. A PAM4 lane at 26.5625 GBd carries 53.125 Gb/s; assigning one to the +// other understates or overstates the link by the modulation factor. +// +// Added 2026-09-05 after that exact conflation was authored and caught in review: SFF-8636 specifies +// transceiver EEPROM byte 140 in units of 100 MBd and byte 222 in units of 250 MBd, and the first +// model of those fields typed them as Bandwidth. `ethtool -m` renders the field labelled "BR, +// nominal" in Mb/s, so the conflation is partly upstream and a reader cannot rely on the tool's own +// unit to be the specification's. First consumer: extdeps.transceiver.sff_8636. +type SymbolRate = Measure + +fn symbol_rate(count: Nat) -> SymbolRate { + Measure { count: count } +} + +fn symbol_rate_count(r: SymbolRate) -> Nat { + measure_count(r) +} + type Nanosecond = Measure fn nanosecond(count: Nat) -> Nanosecond { From 3662f4e3016f1671060cfa089f0dd30b48c08667 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 5 Sep 2026 22:13:02 +0000 Subject: [PATCH 02/11] Enrol the cable-coding evidence: the discriminating RED is the real delivered leg The modules typechecked and executed nothing. hundred_gig_aggregate_collision and sff8636_assess_leg_coding had no consumer, which is specification-without-execution -- DESIGN section 5's deepest trap, and the shape that looks finished precisely because it type-checks. A scheduled review approved the diff without noting it; an approval reports no blocking defect, it does not establish that evidence exists. The discriminating subject is the real delivered part: the EEPROM reading from FS order FS260902769849 (part QDD-400G-4QPC015, leg SN S2630771509-4) is a fixture, and the central test asserts that this leg does NOT attest 100GBASE-CR2. That is the failure that shipped a half-rate fabric which links, pings clean at MTU 9000 and tests green everywhere else the fleet looks. Three arms keep it from being vacuous. The same leg IS admitted for 100GBASE-CR4, the mode it is actually coded for, so a decoder that refused everything would not pass. A synthetic correctly-coded leg is admitted for the requested mode -- and it is marked synthetic, because it validates the DECODER and establishes nothing about whether any physical cable works. A leg whose attestation arrives only via the byte-116 secondary code is still admitted, so a collapse back to reading only byte 192 reds here rather than being caught by inspection a second time. The units separation executes too: a PAM4 lane is asserted at 26.5625 GBd carrying 53.125 Gb/s encoded against a 50 Gb/s service rate, so re-fusing those fields or assigning a baud figure to a bits/s carrier stops the arithmetic from holding. The synthetic row's compliance code is deliberately 0 and says so: the real SFF-8024 assignment for 100GBASE-CR2 has not been read in this lane, and inventing the byte would be the fabricated citation this whole subject exists to catch. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01AigrH3JpxgSJBmqHMBAr6W --- .../claim/cable_leg_coding_witness_test.dag | 178 ++++++++++++++++++ 1 file changed, 178 insertions(+) create mode 100644 dag/test/claim/cable_leg_coding_witness_test.dag diff --git a/dag/test/claim/cable_leg_coding_witness_test.dag b/dag/test/claim/cable_leg_coding_witness_test.dag new file mode 100644 index 00000000000..db9b57ffa5b --- /dev/null +++ b/dag/test/claim/cable_leg_coding_witness_test.dag @@ -0,0 +1,178 @@ +module test.claim.cable_leg_coding_witness + +import std.types { Bool } +import std.measure { bandwidth_count, symbol_rate_count } +import extdeps.ethernet.link_mode { + LinkMode, Nrz, Pam4, Lanes2, Lanes4, + link_mode_eq, link_mode_aggregate, link_mode_lane_encoded_rate, + modulation_bits_per_symbol, lane_count_value, + hundred_gig_aggregate_collision, + ieee_25gbase_cr, ieee_50gbase_cr2, ieee_100gbase_cr4, ieee_100gbase_cr2, +} +import extdeps.transceiver.sff_8636 { + Sff8636LegCoding, Sff8636CodingFinding, + CodingConsistentWithRequest, CodingInsufficientForRequestedMode, + CodingContradictsEncoding, CodingNotUnderstood, + ExtendedCompliance, Qsfp28, EncodingPam4, Encoding64b66b, EncodingUnspecified, + NominalRateEscaped, NominalRateDirect, + ext_compliance_0x0b, + sff8636_assess_leg_coding, sff8636_nominal_rate_from_byte140, + transceiver_identifier_from_byte, sff8636_encoding_from_byte, +} +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } + +// GREEN BY EXECUTION FOR THE CABLE-CODING SUBJECT, and the reason it exists rather than being +// implied by a typecheck: DESIGN section 5 says a typecheck is not a consumer. Without this module +// `hundred_gig_aggregate_collision` and `sff8636_assess_leg_coding` are functions nothing calls -- +// specification without execution, which is the shape that looks finished and proves nothing. +// +// THE DISCRIMINATING SUBJECT IS A REAL DELIVERED PART. The negative case below is the actual EEPROM +// reading from FS order FS260902769849 (part QDD-400G-4QPC015, leg SN S2630771509-4), captured with +// `ethtool -m` on a ConnectX-7. It is authorable as a fixture precisely because the bytes were +// observed, and it goes red if the assessment ever starts admitting this coding for 100GBASE-CR2 -- +// which is the defect that cost this fleet half its fabric. +// +// The positive control beside it is a leg coded the way the part was PURCHASED to be coded. It is +// SYNTHETIC and says so: it validates the decoder, and it establishes nothing about whether any +// physical cable works. Those are different claims and this module never lets one stand for the +// other. +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// ---------------- the link-mode decomposition ---------------- + +// THE COLLISION THAT JUSTIFIES THE WHOLE MODULE SHAPE. If this ever went false, carrying lanes and +// modulation separately would have lost its reason, and a single aggregate would be sufficient. +test fn one_hundred_gig_names_two_different_modes() -> Bool { + hundred_gig_aggregate_collision() +} + +// AND THE SAME COLLISION ONE RUNG DOWN, which is why lane count is carried rather than inferred from +// an aggregate and a modulation. +test fn fifty_gig_also_collides_across_lane_counts() -> Bool { + bandwidth_count(b: link_mode_aggregate(m: ieee_50gbase_cr2)) + == bandwidth_count(b: link_mode_aggregate(m: ieee_25gbase_cr)) * 2 +} + +// THE UNITS SEPARATION, ASSERTED RATHER THAN TRUSTED. A 50G PAM4 lane is 26.5625 GBd carrying +// 53.125 Gb/s encoded -- three numbers that a single field would have collapsed. This test is the +// executing form of the correction that produced SymbolRate: if the fields are ever re-fused, or a +// baud figure is ever assigned to a bits/s carrier, the arithmetic here stops holding. +test fn a_pam4_lane_carries_two_bits_per_symbol() -> Bool { + modulation_bits_per_symbol(m: Pam4) == 2 + && modulation_bits_per_symbol(m: Nrz) == 1 + && symbol_rate_count(r: ieee_100gbase_cr2.per_lane_symbol_rate) == 26562500000 + && bandwidth_count(b: link_mode_lane_encoded_rate(m: ieee_100gbase_cr2)) == 53125000000 + && bandwidth_count(b: ieee_100gbase_cr2.per_lane_service_rate) == 50000000000 +} + +// The aggregate is derived, so it must equal lanes times the service rate for every named mode. +test fn the_aggregate_is_derived_from_lanes_and_service_rate() -> Bool { + bandwidth_count(b: link_mode_aggregate(m: ieee_100gbase_cr2)) + == lane_count_value(l: Lanes2) * bandwidth_count(b: ieee_100gbase_cr2.per_lane_service_rate) + && bandwidth_count(b: link_mode_aggregate(m: ieee_100gbase_cr4)) + == lane_count_value(l: Lanes4) * bandwidth_count(b: ieee_100gbase_cr4.per_lane_service_rate) +} + +// ---------------- the delivered cable: the discriminating RED ---------------- + +// The bytes as read from the delivered leg. Identifier 0x11, extended compliance 0x0B, encoding 0x08 +// (PAM4). The nominal-rate byte is carried as the ESCAPE it appears to be rather than as the +// 25.5 figure ethtool renders -- see the module's own note on why that distinction is not cosmetic. +data delivered_fs_leg: Sff8636LegCoding = Sff8636LegCoding { + identifier: transceiver_identifier_from_byte(code: 17), + primary_compliance: ext_compliance_0x0b, + secondary_compliance: none, + encoding: sff8636_encoding_from_byte(code: 8), + nominal_rate: sff8636_nominal_rate_from_byte140(code: 255), +} + +fn is_insufficient(f: Sff8636CodingFinding) -> Bool { + match f { + CodingInsufficientForRequestedMode { requested: r, coding: c } => true + CodingConsistentWithRequest { coding: c } => false + CodingContradictsEncoding { encoding_modulation: m, attested_mode: a } => false + CodingNotUnderstood { encoding: e } => false + } +} + +fn is_consistent(f: Sff8636CodingFinding) -> Bool { + match f { + CodingConsistentWithRequest { coding: c } => true + CodingInsufficientForRequestedMode { requested: r, coding: c } => false + CodingContradictsEncoding { encoding_modulation: m, attested_mode: a } => false + CodingNotUnderstood { encoding: e } => false + } +} + +// THE CENTRAL ASSERTION OF THIS PR. The delivered leg does not attest 100GBASE-CR2, so a fleet that +// needs 100G_2X must not be told this part supplies it. This reds if the assessment ever admits the +// coding -- the failure that shipped a half-rate fabric that links, pings clean and tests green. +test fn the_delivered_leg_does_not_attest_the_purchased_mode() -> Bool { + is_insufficient(f: sff8636_assess_leg_coding( + coding: delivered_fs_leg, requested: ieee_100gbase_cr2)) +} + +// AND THE SAME LEG IS FINE FOR WHAT IT ACTUALLY ATTESTS. Without this arm the test above would pass +// for a decoder that refuses everything, which is a wall that carries no information. +test fn the_delivered_leg_does_attest_the_mode_it_is_coded_for() -> Bool { + is_consistent(f: sff8636_assess_leg_coding( + coding: delivered_fs_leg, requested: ieee_100gbase_cr4)) +} + +// The escape is not a measurement. This is the executing form of the byte-140 correction. +test fn the_escape_value_is_not_recorded_as_a_rate() -> Bool { + match sff8636_nominal_rate_from_byte140(code: 255) { + NominalRateEscaped => true + NominalRateDirect { rate: r } => false + } +} + +test fn an_ordinary_byte140_is_read_as_a_symbol_rate() -> Bool { + match sff8636_nominal_rate_from_byte140(code: 255 - 1) { + NominalRateDirect { rate: r } => symbol_rate_count(r: r) == 25400000000 + NominalRateEscaped => false + } +} + +// ---------------- the positive control ---------------- + +// A SYNTHETIC leg coded for what the part was bought to do. Its compliance code is NOT the real +// SFF-8024 assignment for 100GBASE-CR2 -- this lane has not read that table, and inventing the byte +// would be the fabricated citation the whole subject exists to catch. What this row proves is that +// the ASSESSMENT admits a leg whose attested modes include the requested one; it deliberately proves +// nothing about which byte value carries that attestation in the real world. +data synthetic_cr2_compliance: ExtendedCompliance = ExtendedCompliance { + code: 0, + attested_modes: [ieee_100gbase_cr2], +} + +data synthetic_correctly_coded_leg: Sff8636LegCoding = Sff8636LegCoding { + identifier: transceiver_identifier_from_byte(code: 17), + primary_compliance: synthetic_cr2_compliance, + secondary_compliance: none, + encoding: sff8636_encoding_from_byte(code: 8), + nominal_rate: sff8636_nominal_rate_from_byte140(code: 255), +} + +// THE POSITIVE CONTROL. A decoder that said "insufficient" to everything would satisfy every +// negative assertion above; this is what makes those assertions discriminating rather than vacuous. +test fn a_correctly_coded_leg_is_admitted_for_the_requested_mode() -> Bool { + is_consistent(f: sff8636_assess_leg_coding( + coding: synthetic_correctly_coded_leg, requested: ieee_100gbase_cr2)) +} + +// AND THE SECONDARY CODE IS ACTUALLY READ. Byte 116 was added because reading only byte 192 is +// unsound over a multi-application module; this reds if the union ever collapses back to the +// primary, which is the exact regression the review caught by inspection. +data secondary_coded_leg: Sff8636LegCoding = Sff8636LegCoding { + identifier: transceiver_identifier_from_byte(code: 17), + primary_compliance: ext_compliance_0x0b, + secondary_compliance: Present { value: synthetic_cr2_compliance }, + encoding: sff8636_encoding_from_byte(code: 8), + nominal_rate: sff8636_nominal_rate_from_byte140(code: 255), +} + +test fn a_mode_attested_only_by_the_secondary_code_is_still_attested() -> Bool { + is_consistent(f: sff8636_assess_leg_coding( + coding: secondary_coded_leg, requested: ieee_100gbase_cr2)) +} From ae566ad0908f4dffe341c9c00edc1437135a2b6e Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 6 Sep 2026 01:21:46 +0000 Subject: [PATCH 03/11] Make the compliance byte the evidence, and stop proving contradiction from an unread field Review found the central witness DETERMINISTICALLY FALSE. For the delivered leg, every attested mode is NRZ while the encoding byte says PAM4, so the assessor returned CodingContradictsEncoding -- while the test, the commit message and the PR body all said CodingInsufficientForRequestedMode. Behaviour was documented and never executed, in the PR whose thesis is that unexecuted claims are worthless. The floor had died earlier on generated-artifact drift, so nothing had contradicted it; the witness could not even compile, because it constructed a sole_constructor type outside its defining module. The repair is to the PRECONDITION, not the expectation. Widening the test to accept any refusal would have been the absorbing fallback. A contradiction is a claim that the WHOLE declared profile disagrees with the encoding byte, and byte 116 was never read on this cable, so that claim is unavailable: SecondaryNotObserved is now distinct from SecondaryObservedEmpty, and an unread field can no longer stand as evidence of absence. THE COMPLIANCE BYTE NOW DECIDES. ExtendedCompliance previously carried an author-supplied `attested_modes` beside `code`, and the assessor read only the former, so the byte was decorative -- the synthetic fixture passed code 0 with a hand-written CR2 list and was admitted on its own say-so. Interpretation is now a function of the byte, an unmodelled code interprets to UNKNOWN rather than to an empty attestation, and the discriminating control this enables -- mutate only the code, hold every other field fixed, require the unknown result -- was structurally unwritable before. 0x0B carries a third entry: 50GBASE-CR2 subject to Clause 91 FEC, found by an external standards cross-check rather than by anything in this repository. The condition is retained, not flattened: it yields CodingAttestsRequestedModeSubjectToFec, and a test asserts it is attested AND not attested outright, because promoting a conditional entry to unconditional support is the silent widening the qualification exists to prevent. The stage0 mirror for std_measure.rs is regenerated from its authority (first_generation_equal=true, 157/157 adjudicated); the candidate diff was exactly the 13-line SymbolRate addition and nothing else. EXECUTED, not asserted: claim_executor --required-floor built from this tree reports verdict=FloorClean, claims_failed=0, with all 14 cable-coding claims in the executed population. The prior run of the same instrument red on this file with three located errors, so the pair discriminates rather than a green standing alone. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01AigrH3JpxgSJBmqHMBAr6W --- dag/extdeps/transceiver/sff_8636.dag | 244 ++++++++++++------ .../claim/cable_leg_coding_witness_test.dag | 203 ++++++++++----- src/v1/stage0/src/std_measure.rs | 13 + 3 files changed, 319 insertions(+), 141 deletions(-) diff --git a/dag/extdeps/transceiver/sff_8636.dag b/dag/extdeps/transceiver/sff_8636.dag index e408746290b..9461ba7fa35 100644 --- a/dag/extdeps/transceiver/sff_8636.dag +++ b/dag/extdeps/transceiver/sff_8636.dag @@ -8,7 +8,7 @@ import extdeps.external_authority { ExternalAuthority, ExternalModelScope, Exter import extdeps.uri { Uri, Https } import extdeps.ethernet.link_mode { LinkMode, Modulation, Nrz, Pam4, modulation_eq, link_mode_eq, - ieee_25gbase_cr, ieee_100gbase_cr4, + ieee_25gbase_cr, ieee_100gbase_cr4, ieee_50gbase_cr2, } // THE MANAGEMENT EEPROM OF A QSFP MODULE OR CABLE LEG -- AND THE REASON A PART NUMBER IS NOT A LINK @@ -137,102 +137,194 @@ fn sff8636_nominal_rate_from_byte222(code: Nat) -> SymbolRate { symbol_rate(code * 250000000) } -// ================= BYTE 192: EXTENDED SPECIFICATION COMPLIANCE ================= +// ================= BYTE 192 / BYTE 116: EXTENDED SPECIFICATION COMPLIANCE ================= // -// This is the byte the ConnectX-7 reads to decide which rates to enable, so it is the byte the whole -// incident turns on. The code is carried as its raw value with the modes it attests, where this lane -// has read them. +// THE BYTE IS THE EVIDENCE; THE MODE LIST IS AN INTERPRETATION OF IT. An earlier head carried +// `ExtendedCompliance { code, attested_modes }` and let the caller author both. The assessor then +// read only `attested_modes` and never consulted `code`, so the compliance byte was decorative: a +// caller could supply an unmodelled code beside any capability list it liked and be admitted on its +// own say-so. The synthetic positive fixture proved it -- code 0 with an authored CR2 list was +// accepted -- and a decoder that is handed its own answer decodes nothing. // -// WHAT IS NOT ESTABLISHED: the code that WOULD attest 100GBASE-CR2. SFF-8024 assigns one, this lane -// did not read it against a copy of the specification, and writing a plausible value here would be a -// fabricated citation of exactly the kind that caused the problem being modelled. The refusal below -// does not need it -- internal inconsistency is decidable without knowing the right answer -- so the -// gap blocks nothing except the eventual positive control. Its trigger is one reading of SFF-8024 -// Table 4-4. -type ExtendedCompliance sole_constructor { - code: Nat - attested_modes: List -} - -// 0x0B. Read from the delivered cable, and its meaning read from the ethtool decode the operator -// captured: "100GBASE-CR4 or 25GBASE-CR CA-L". Both attested modes are NRZ at 25G per lane, which is -// what makes the PAM4 encoding byte beside it a contradiction rather than a nuance. -data ext_compliance_0x0b: ExtendedCompliance = ExtendedCompliance { - code: 11, - attested_modes: [ieee_100gbase_cr4, ieee_25gbase_cr], -} - -// ================= THE LEG CODING, AND WHAT ITS BYTES CAN AND CANNOT DECIDE ================= +// So interpretation is a FUNCTION OF THE BYTE, and an unmodelled code interprets to UNKNOWN rather +// than to an empty capability list. Those are different facts: "this code attests nothing" and "this +// decoder cannot read this code" must not both arrive as `[]`, or the decoder's ignorance becomes an +// accusation against the part. + +// A mode attested by a compliance code, together with any condition the standard attaches to it. +// The condition is retained rather than promoted: an entry that holds only under a named FEC is not +// the same claim as an unconditional one, and flattening the two would silently widen what the byte +// attests. +type FecCondition = FecUnconditional | RequiresClause91Fec + +type AttestedMode sole_constructor { + mode: LinkMode + fec: FecCondition +} + +type ComplianceInterpretation + = ComplianceUnderstood { code: Nat, modes: List } + | ComplianceCodeUnmodelled { code: Nat } + +// THE DECODER. Rows are read from SFF-8024's extended-compliance table; a code with no row here +// interprets to Unmodelled, never to an empty attestation. // -// A coding carries BOTH extended-compliance codes. SFF-8636 provides a secondary code at byte 116 -// beside the primary at byte 192, and SFF-8024 permits a module supporting several encodings to -// report the one belonging to its PRIMARY PRODUCT APPLICATION. The first version of this module read -// only byte 192 and byte 139 and declared their disagreement a contradiction; that predicate is not -// sound over a multi-application module, and the overreach was caught in review. +// 0x0B carries THREE entries, not two. The first head modelled 100GBASE-CR4 and 25GBASE-CR CA-L and +// omitted 50GBASE-CR2 with Clause 91 FEC, which changes behaviour: a 50GBASE-CR2 request against +// this code returned "insufficient" when the standard's entry does include that mode, subject to its +// FEC condition. The omission was found by an external standards cross-check (SFF-8024 Rev 4.14, +// Table 4-6) rather than by anything in this repository, and the FEC qualification is carried rather +// than dropped so the conditional entry cannot be read as unconditional support. +fn sff8636_interpret_extended_compliance(code: Nat) -> ComplianceInterpretation { + if code == 11 { + ComplianceUnderstood { + code: code, + modes: [ + AttestedMode { mode: ieee_100gbase_cr4, fec: FecUnconditional }, + AttestedMode { mode: ieee_25gbase_cr, fec: FecUnconditional }, + AttestedMode { mode: ieee_50gbase_cr2, fec: RequiresClause91Fec }, + ], + } + } else { + ComplianceCodeUnmodelled { code: code } + } +} + +// ================= THE OBSERVED SECONDARY FIELD ================= +// +// AN UNREAD FIELD IS NOT AN ABSENT ONE, and the distinction decides a verdict. Contradiction is a +// claim about a COMPLETE profile: it says every application this module declares disagrees with its +// encoding byte. That claim cannot be made while byte 116 has not been read, because the unread +// field may carry the very application the encoding belongs to. The earlier head used `Absent` for +// both and therefore proved contradiction from a gap in its own observation. +type SecondaryComplianceObservation + = SecondaryNotObserved + | SecondaryObservedEmpty + | SecondaryObservedCode { code: Nat } + +// ================= THE LEG CODING ================= +// +// The coding carries RAW BYTES. Nothing here lets a caller supply a capability directly. type Sff8636LegCoding sole_constructor { identifier: TransceiverIdentifier - primary_compliance: ExtendedCompliance - secondary_compliance: ExtendedCompliance? + primary_compliance_code: Nat + secondary_compliance: SecondaryComplianceObservation encoding: Sff8636Encoding nominal_rate: Sff8636NominalRate } -// THREE FINDINGS, NOT ONE REFUSAL. Collapsing these would let the strongest claim absorb the weakest -// evidence, which is how a decoder's ignorance turns into an accusation against a part. -// -// Contradictory -- every attested mode under the OBSERVED profile disagrees with the -// encoding byte. A claim about these bytes, not about the hardware. -// InsufficientEvidence -- nothing in the observed bytes attests the mode the operator requires. -// THIS IS WHERE THE DELIVERED FS CABLE LANDS: 0x0B attests 25G-per-lane -// modes and nothing attests 100GBASE-CR2, which is why the ConnectX-7 -// refuses to enable 100G_2X. It is a strictly weaker and strictly more -// defensible finding than "this EEPROM is self-contradictory". -// NotUnderstood -- the decoder has no row for what it read. An unknown code must never -// become a proven contradiction merely because this model lacks a row for -// it; that is the decoder's gap, not the module's defect. +// THE CONSTRUCTOR, because `sole_constructor` means this module owns construction and a consumer -- +// including a witness -- may not mint the type itself. That is the same rule R2 asked for one level +// down: the caller supplies OBSERVED BYTES, and the module decides what they mean. +fn sff8636_leg_coding( + identifier: TransceiverIdentifier, + primary_compliance_code: Nat, + secondary_compliance: SecondaryComplianceObservation, + encoding: Sff8636Encoding, + nominal_rate: Sff8636NominalRate, +) -> Sff8636LegCoding { + Sff8636LegCoding { + identifier: identifier, + primary_compliance_code: primary_compliance_code, + secondary_compliance: secondary_compliance, + encoding: encoding, + nominal_rate: nominal_rate, + } +} + +// FIVE FINDINGS. Each says something different about what the bytes establish, and collapsing any +// pair would let a stronger claim absorb weaker evidence. type Sff8636CodingFinding - = CodingConsistentWithRequest { coding: Sff8636LegCoding } - | CodingContradictsEncoding { encoding_modulation: Modulation, attested_mode: LinkMode } + = CodingAttestsRequestedMode { coding: Sff8636LegCoding } + | CodingAttestsRequestedModeSubjectToFec { coding: Sff8636LegCoding, fec: FecCondition } | CodingInsufficientForRequestedMode { requested: LinkMode, coding: Sff8636LegCoding } - | CodingNotUnderstood { encoding: Sff8636Encoding } + | CodingContradictsEncoding { encoding_modulation: Modulation, attested_mode: LinkMode } + | CodingComplianceCodeNotUnderstood { code: Nat } -// Every mode attested by either compliance code. The union is the observable profile; reading only -// the primary is what made the earlier predicate unsound. -fn sff8636_attested_modes(coding: Sff8636LegCoding) -> List { +// The interpretations of both observed codes. A not-observed secondary contributes nothing AND is +// remembered as unobserved by `sff8636_profile_is_complete` below. +fn sff8636_interpretations(coding: Sff8636LegCoding) -> List { match coding.secondary_compliance { - Present { value: sec } => - concat(coding.primary_compliance.attested_modes, sec.attested_modes) - Absent => coding.primary_compliance.attested_modes + SecondaryObservedCode { code: sc } => [ + sff8636_interpret_extended_compliance(code: coding.primary_compliance_code), + sff8636_interpret_extended_compliance(code: sc), + ] + SecondaryObservedEmpty => + [sff8636_interpret_extended_compliance(code: coding.primary_compliance_code)] + SecondaryNotObserved => + [sff8636_interpret_extended_compliance(code: coding.primary_compliance_code)] } } -// THE QUESTION IS ALWAYS RELATIVE TO A REQUESTED MODE. There is no such thing as a coding that is -// "correct" in the abstract -- only one that does or does not attest what this endpoint pair needs. -// Asking it without a request is what let the earlier version imagine it could judge a part alone. +fn sff8636_attested(coding: Sff8636LegCoding) -> List { + flat_map(sff8636_interpretations(coding: coding), i => + match i { + ComplianceUnderstood { code: c, modes: ms } => ms + ComplianceCodeUnmodelled { code: c } => [] + }) +} + +// Any code this decoder could not read. Its presence blocks both the acceptance and the +// contradiction claims: an unread code may attest the requested mode, and it may carry the +// application whose encoding is on the wire. +fn sff8636_unmodelled_codes(coding: Sff8636LegCoding) -> List { + flat_map(sff8636_interpretations(coding: coding), i => + match i { + ComplianceCodeUnmodelled { code: c } => [c] + ComplianceUnderstood { code: c, modes: ms } => [] + }) +} + +// A CONTRADICTION NEEDS A COMPLETE, FULLY DECODED PROFILE. Both conditions are necessary: every +// declared field read, and every read code understood. +fn sff8636_profile_is_complete(coding: Sff8636LegCoding) -> Bool { + match coding.secondary_compliance { + SecondaryNotObserved => false + SecondaryObservedEmpty => length(sff8636_unmodelled_codes(coding: coding)) == 0 + SecondaryObservedCode { code: sc } => length(sff8636_unmodelled_codes(coding: coding)) == 0 + } +} + +// THE ASSESSMENT, ALWAYS RELATIVE TO A REQUESTED MODE. fn sff8636_assess_leg_coding( coding: Sff8636LegCoding, requested: LinkMode, ) -> Sff8636CodingFinding { - let attested = sff8636_attested_modes(coding: coding) - if any(attested, m => link_mode_eq(a: m, b: requested)) { - CodingConsistentWithRequest { coding: coding } - } else { - match sff8636_encoding_modulation(e: coding.encoding) { - Absent => CodingInsufficientForRequestedMode { requested: requested, coding: coding } - Present { value: enc_mod } => { - let agreeing = filter(attested, m => modulation_eq(a: m.modulation, b: enc_mod)) - match agreeing.first() { - Absent => - match attested.first() { - Present { value: bad } => - CodingContradictsEncoding { encoding_modulation: enc_mod, attested_mode: bad } - Absent => CodingNotUnderstood { encoding: coding.encoding } - } - Present { value: ok } => - CodingInsufficientForRequestedMode { requested: requested, coding: coding } - } + let attested = sff8636_attested(coding: coding) + let matching = filter(attested, a => link_mode_eq(a: a.mode, b: requested)) + match matching.first() { + Present { value: hit } => + match hit.fec { + FecUnconditional => CodingAttestsRequestedMode { coding: coding } + RequiresClause91Fec => + CodingAttestsRequestedModeSubjectToFec { coding: coding, fec: hit.fec } + } + Absent => + match sff8636_unmodelled_codes(coding: coding).first() { + Present { value: unknown } => CodingComplianceCodeNotUnderstood { code: unknown } + Absent => + match sff8636_encoding_modulation(e: coding.encoding) { + Absent => CodingInsufficientForRequestedMode { requested: requested, coding: coding } + Present { value: enc_mod } => + if !sff8636_profile_is_complete(coding: coding) { + CodingInsufficientForRequestedMode { requested: requested, coding: coding } + } else { + let agreeing = filter(attested, a => modulation_eq(a: a.mode.modulation, b: enc_mod)) + match agreeing.first() { + Present { value: ok } => + CodingInsufficientForRequestedMode { requested: requested, coding: coding } + Absent => + match attested.first() { + Present { value: bad } => + CodingContradictsEncoding { + encoding_modulation: enc_mod, attested_mode: bad.mode } + Absent => + CodingInsufficientForRequestedMode { requested: requested, coding: coding } + } + } + } + } } - } } } diff --git a/dag/test/claim/cable_leg_coding_witness_test.dag b/dag/test/claim/cable_leg_coding_witness_test.dag index db9b57ffa5b..027feb8f9df 100644 --- a/dag/test/claim/cable_leg_coding_witness_test.dag +++ b/dag/test/claim/cable_leg_coding_witness_test.dag @@ -11,12 +11,15 @@ import extdeps.ethernet.link_mode { } import extdeps.transceiver.sff_8636 { Sff8636LegCoding, Sff8636CodingFinding, - CodingConsistentWithRequest, CodingInsufficientForRequestedMode, - CodingContradictsEncoding, CodingNotUnderstood, - ExtendedCompliance, Qsfp28, EncodingPam4, Encoding64b66b, EncodingUnspecified, + CodingAttestsRequestedMode, CodingAttestsRequestedModeSubjectToFec, + CodingInsufficientForRequestedMode, CodingContradictsEncoding, + CodingComplianceCodeNotUnderstood, + SecondaryNotObserved, SecondaryObservedEmpty, SecondaryObservedCode, + ComplianceUnderstood, ComplianceCodeUnmodelled, + FecUnconditional, RequiresClause91Fec, NominalRateEscaped, NominalRateDirect, - ext_compliance_0x0b, - sff8636_assess_leg_coding, sff8636_nominal_rate_from_byte140, + sff8636_assess_leg_coding, sff8636_nominal_rate_from_byte140, sff8636_leg_coding, + sff8636_interpret_extended_compliance, transceiver_identifier_from_byte, sff8636_encoding_from_byte, } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } @@ -75,104 +78,174 @@ test fn the_aggregate_is_derived_from_lanes_and_service_rate() -> Bool { // ---------------- the delivered cable: the discriminating RED ---------------- -// The bytes as read from the delivered leg. Identifier 0x11, extended compliance 0x0B, encoding 0x08 -// (PAM4). The nominal-rate byte is carried as the ESCAPE it appears to be rather than as the -// 25.5 figure ethtool renders -- see the module's own note on why that distinction is not cosmetic. -data delivered_fs_leg: Sff8636LegCoding = Sff8636LegCoding { +// The bytes as read from the delivered leg: identifier 0x11, primary extended compliance 0x0B, +// encoding 0x08 (PAM4), nominal-rate byte 255. +// +// BYTE 116 WAS NOT READ, and that is recorded as SecondaryNotObserved rather than as an empty +// secondary. The distinction is load-bearing here: an unread field cannot participate in a proof +// that the WHOLE profile disagrees with the encoding byte, because the unread field may carry the +// application the encoding belongs to. An earlier head modelled the unread field as absent and +// therefore proved a contradiction out of a gap in its own observation. +data delivered_fs_leg: Sff8636LegCoding = sff8636_leg_coding( identifier: transceiver_identifier_from_byte(code: 17), - primary_compliance: ext_compliance_0x0b, - secondary_compliance: none, + primary_compliance_code: 11, + secondary_compliance: SecondaryNotObserved, encoding: sff8636_encoding_from_byte(code: 8), - nominal_rate: sff8636_nominal_rate_from_byte140(code: 255), -} + nominal_rate: sff8636_nominal_rate_from_byte140(code: 255)) fn is_insufficient(f: Sff8636CodingFinding) -> Bool { match f { CodingInsufficientForRequestedMode { requested: r, coding: c } => true - CodingConsistentWithRequest { coding: c } => false + CodingAttestsRequestedMode { coding: c } => false + CodingAttestsRequestedModeSubjectToFec { coding: c, fec: x } => false CodingContradictsEncoding { encoding_modulation: m, attested_mode: a } => false - CodingNotUnderstood { encoding: e } => false + CodingComplianceCodeNotUnderstood { code: c } => false } } -fn is_consistent(f: Sff8636CodingFinding) -> Bool { +fn attests_outright(f: Sff8636CodingFinding) -> Bool { match f { - CodingConsistentWithRequest { coding: c } => true + CodingAttestsRequestedMode { coding: c } => true + CodingAttestsRequestedModeSubjectToFec { coding: c, fec: x } => false CodingInsufficientForRequestedMode { requested: r, coding: c } => false CodingContradictsEncoding { encoding_modulation: m, attested_mode: a } => false - CodingNotUnderstood { encoding: e } => false + CodingComplianceCodeNotUnderstood { code: c } => false } } -// THE CENTRAL ASSERTION OF THIS PR. The delivered leg does not attest 100GBASE-CR2, so a fleet that -// needs 100G_2X must not be told this part supplies it. This reds if the assessment ever admits the -// coding -- the failure that shipped a half-rate fabric that links, pings clean and tests green. +fn attests_subject_to_fec(f: Sff8636CodingFinding) -> Bool { + match f { + CodingAttestsRequestedModeSubjectToFec { coding: c, fec: x } => true + CodingAttestsRequestedMode { coding: c } => false + CodingInsufficientForRequestedMode { requested: r, coding: c } => false + CodingContradictsEncoding { encoding_modulation: m, attested_mode: a } => false + CodingComplianceCodeNotUnderstood { code: c } => false + } +} + +fn code_not_understood(f: Sff8636CodingFinding) -> Bool { + match f { + CodingComplianceCodeNotUnderstood { code: c } => true + CodingAttestsRequestedMode { coding: c } => false + CodingAttestsRequestedModeSubjectToFec { coding: c, fec: x } => false + CodingInsufficientForRequestedMode { requested: r, coding: c } => false + CodingContradictsEncoding { encoding_modulation: m, attested_mode: a } => false + } +} + +// THE CENTRAL ASSERTION. The delivered leg does not attest 100GBASE-CR2, so a fleet needing 100G_2X +// must not be told this part supplies it. +// +// The finding is INSUFFICIENCY, not contradiction, and the previous head asserted exactly this while +// the implementation returned contradiction -- a documented behaviour that no execution had ever +// checked. It is insufficiency because byte 116 was never read: with the profile incomplete, the +// strong claim is unavailable and the honest one is that nothing OBSERVED attests the request. test fn the_delivered_leg_does_not_attest_the_purchased_mode() -> Bool { is_insufficient(f: sff8636_assess_leg_coding( coding: delivered_fs_leg, requested: ieee_100gbase_cr2)) } -// AND THE SAME LEG IS FINE FOR WHAT IT ACTUALLY ATTESTS. Without this arm the test above would pass -// for a decoder that refuses everything, which is a wall that carries no information. +// AND THE SAME LEG DOES ATTEST WHAT IT IS CODED FOR. Without this arm the assertion above would pass +// for a decoder that refused everything, which is a wall carrying no information. test fn the_delivered_leg_does_attest_the_mode_it_is_coded_for() -> Bool { - is_consistent(f: sff8636_assess_leg_coding( + attests_outright(f: sff8636_assess_leg_coding( coding: delivered_fs_leg, requested: ieee_100gbase_cr4)) } -// The escape is not a measurement. This is the executing form of the byte-140 correction. -test fn the_escape_value_is_not_recorded_as_a_rate() -> Bool { - match sff8636_nominal_rate_from_byte140(code: 255) { - NominalRateEscaped => true - NominalRateDirect { rate: r } => false - } +// THE CLAUSE 91 ENTRY, WHICH THIS MODULE FIRST OMITTED. 0x0B also covers 50GBASE-CR2 subject to +// Clause 91 FEC. It must be attested -- returning "insufficient" would understate the byte -- and it +// must NOT be attested outright, because promoting a conditional entry to unconditional support is +// exactly the silent widening the standard's qualification exists to prevent. +test fn the_conditional_entry_is_attested_but_not_unconditionally() -> Bool { + let f = sff8636_assess_leg_coding(coding: delivered_fs_leg, requested: ieee_50gbase_cr2) + attests_subject_to_fec(f: f) && !attests_outright(f: f) } -test fn an_ordinary_byte140_is_read_as_a_symbol_rate() -> Bool { - match sff8636_nominal_rate_from_byte140(code: 255 - 1) { - NominalRateDirect { rate: r } => symbol_rate_count(r: r) == 25400000000 - NominalRateEscaped => false - } +// ---------------- the code IS the evidence ---------------- + +// THE DISCRIMINATING CONTROL FOR THE DECODER ITSELF: mutate ONLY the compliance byte and hold every +// other observation fixed. An earlier head could not express this test at all, because the caller +// authored the capability list beside the byte -- so changing the byte changed nothing and the +// decoder was decorative. This reds if interpretation ever migrates back out of the byte. +data leg_with_unmodelled_code: Sff8636LegCoding = sff8636_leg_coding( + identifier: transceiver_identifier_from_byte(code: 17), + primary_compliance_code: 254, + secondary_compliance: SecondaryNotObserved, + encoding: sff8636_encoding_from_byte(code: 8), + nominal_rate: sff8636_nominal_rate_from_byte140(code: 255)) + +test fn an_unmodelled_code_is_not_understood_rather_than_attesting_nothing() -> Bool { + code_not_understood(f: sff8636_assess_leg_coding( + coding: leg_with_unmodelled_code, requested: ieee_100gbase_cr2)) } -// ---------------- the positive control ---------------- +// An unread code must not become a proven contradiction. Same bytes, PAM4 encoding, NRZ-only +// understood modes -- but one code the decoder cannot read, so no contradiction may be claimed. +test fn an_unreadable_code_blocks_the_contradiction_claim() -> Bool { + !is_insufficient(f: sff8636_assess_leg_coding( + coding: leg_with_unmodelled_code, requested: ieee_100gbase_cr4)) + && code_not_understood(f: sff8636_assess_leg_coding( + coding: leg_with_unmodelled_code, requested: ieee_100gbase_cr4)) +} + +// The interpretation is a function of the byte, asserted directly. +test fn the_interpretation_is_derived_from_the_byte() -> Bool { + match sff8636_interpret_extended_compliance(code: 11) { + ComplianceUnderstood { code: c, modes: ms } => c == 11 && count(ms) == 3 + ComplianceCodeUnmodelled { code: c } => false + } +} -// A SYNTHETIC leg coded for what the part was bought to do. Its compliance code is NOT the real -// SFF-8024 assignment for 100GBASE-CR2 -- this lane has not read that table, and inventing the byte -// would be the fabricated citation the whole subject exists to catch. What this row proves is that -// the ASSESSMENT admits a leg whose attested modes include the requested one; it deliberately proves -// nothing about which byte value carries that attestation in the real world. -data synthetic_cr2_compliance: ExtendedCompliance = ExtendedCompliance { - code: 0, - attested_modes: [ieee_100gbase_cr2], +test fn an_unknown_byte_interprets_to_unknown_not_to_an_empty_attestation() -> Bool { + match sff8636_interpret_extended_compliance(code: 254) { + ComplianceCodeUnmodelled { code: c } => c == 254 + ComplianceUnderstood { code: c, modes: ms } => false + } } -data synthetic_correctly_coded_leg: Sff8636LegCoding = Sff8636LegCoding { +// ---------------- contradiction requires a complete profile ---------------- + +// A leg whose byte 116 WAS read and found empty, whose primary code is understood, and whose every +// attested mode is NRZ while the encoding byte says PAM4. Only here is the profile complete enough +// for the strong claim, and this is the one fixture that may produce it. +data complete_profile_contradictory_leg: Sff8636LegCoding = sff8636_leg_coding( identifier: transceiver_identifier_from_byte(code: 17), - primary_compliance: synthetic_cr2_compliance, - secondary_compliance: none, + primary_compliance_code: 11, + secondary_compliance: SecondaryObservedEmpty, encoding: sff8636_encoding_from_byte(code: 8), - nominal_rate: sff8636_nominal_rate_from_byte140(code: 255), + nominal_rate: sff8636_nominal_rate_from_byte140(code: 255)) + +fn is_contradiction(f: Sff8636CodingFinding) -> Bool { + match f { + CodingContradictsEncoding { encoding_modulation: m, attested_mode: a } => true + CodingAttestsRequestedMode { coding: c } => false + CodingAttestsRequestedModeSubjectToFec { coding: c, fec: x } => false + CodingInsufficientForRequestedMode { requested: r, coding: c } => false + CodingComplianceCodeNotUnderstood { code: c } => false + } } -// THE POSITIVE CONTROL. A decoder that said "insufficient" to everything would satisfy every -// negative assertion above; this is what makes those assertions discriminating rather than vacuous. -test fn a_correctly_coded_leg_is_admitted_for_the_requested_mode() -> Bool { - is_consistent(f: sff8636_assess_leg_coding( - coding: synthetic_correctly_coded_leg, requested: ieee_100gbase_cr2)) +// THE PAIR THAT MAKES THE COMPLETENESS CONDITION REAL. Identical bytes except that byte 116 is read +// in one and unread in the other: the read one may claim contradiction, the unread one may not. +// Without both arms, "contradiction requires a complete profile" would be prose no execution checks. +test fn contradiction_is_claimed_only_when_the_profile_was_fully_observed() -> Bool { + is_contradiction(f: sff8636_assess_leg_coding( + coding: complete_profile_contradictory_leg, requested: ieee_100gbase_cr2)) + && is_insufficient(f: sff8636_assess_leg_coding( + coding: delivered_fs_leg, requested: ieee_100gbase_cr2)) } -// AND THE SECONDARY CODE IS ACTUALLY READ. Byte 116 was added because reading only byte 192 is -// unsound over a multi-application module; this reds if the union ever collapses back to the -// primary, which is the exact regression the review caught by inspection. -data secondary_coded_leg: Sff8636LegCoding = Sff8636LegCoding { - identifier: transceiver_identifier_from_byte(code: 17), - primary_compliance: ext_compliance_0x0b, - secondary_compliance: Present { value: synthetic_cr2_compliance }, - encoding: sff8636_encoding_from_byte(code: 8), - nominal_rate: sff8636_nominal_rate_from_byte140(code: 255), +// The escape is not a measurement. +test fn the_escape_value_is_not_recorded_as_a_rate() -> Bool { + match sff8636_nominal_rate_from_byte140(code: 255) { + NominalRateEscaped => true + NominalRateDirect { rate: r } => false + } } -test fn a_mode_attested_only_by_the_secondary_code_is_still_attested() -> Bool { - is_consistent(f: sff8636_assess_leg_coding( - coding: secondary_coded_leg, requested: ieee_100gbase_cr2)) +test fn an_ordinary_byte140_is_read_as_a_symbol_rate() -> Bool { + match sff8636_nominal_rate_from_byte140(code: 254) { + NominalRateDirect { rate: r } => symbol_rate_count(r: r) == 25400000000 + NominalRateEscaped => false + } } diff --git a/src/v1/stage0/src/std_measure.rs b/src/v1/stage0/src/std_measure.rs index 0ff83f787cb..69874f8cedb 100644 --- a/src/v1/stage0/src/std_measure.rs +++ b/src/v1/stage0/src/std_measure.rs @@ -1174,6 +1174,19 @@ pub fn packet_rate_count(r: PacketRate) -> Nat { measure_count(r.clone()) } +pub type SymbolRate = Rc>; + +pub fn symbol_rate(count: Nat) -> SymbolRate { + Rc::new(Measure { + count: count.clone(), + _phantom: std::marker::PhantomData, + }) +} + +pub fn symbol_rate_count(r: SymbolRate) -> Nat { + measure_count(r.clone()) +} + pub type Nanosecond = Rc>; pub fn nanosecond(count: Nat) -> Nanosecond { From 5578aeecb1b50708a028fce9abaa42482bc18040 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 6 Sep 2026 02:02:52 +0000 Subject: [PATCH 04/11] Remove the unconsumed helpers, and the two more the first removal killed A review noted render_link_mode has no in-tree consumer and judged it too small to flag. DESIGN section 6 disagrees: an artifact with no final consumer is a scaffold tell, and the reviewer's own stated test is whether the thing survives into the terminal architecture and is consumed by it. So this censuses every function the PR added rather than fixing the one item spotted -- which found a cascade the single fix would have left behind: modulation_label was consumed only by render_link_mode, and the String import only by modulation_label. sff8636_nominal_rate_from_byte222 also goes. It is CORRECT -- byte 222 is the escape target in units of 250 MBd -- but nothing reads it, because nobody has taken the raw dump yet. Writing a witness whose only purpose was to consume it would make the test its own justification rather than a final consumer. It returns with the ethtool raw reading that needs it. Verified by execution, and the verification earned its keep: the first attempt at this deletion cut at the match block's closing brace instead of the function's and left an orphaned brace, so the module did not parse and the floor refused with ZERO claims executed. A deletion needs the same evidence as an addition; "it only removed dead code" is how a file that cannot parse gets pushed. Floor now verdict=FloorClean, claims_failed=0, all 14 cable-coding claims in the executed population. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01AigrH3JpxgSJBmqHMBAr6W --- dag/extdeps/ethernet/link_mode.dag | 17 +---------------- dag/extdeps/transceiver/sff_8636.dag | 5 ----- 2 files changed, 1 insertion(+), 21 deletions(-) diff --git a/dag/extdeps/ethernet/link_mode.dag b/dag/extdeps/ethernet/link_mode.dag index 62001e47b3b..0205f1a7cf7 100644 --- a/dag/extdeps/ethernet/link_mode.dag +++ b/dag/extdeps/ethernet/link_mode.dag @@ -1,7 +1,7 @@ module extdeps.ethernet.link_mode import std.nat { Nat } -import std.types { Bool, String } +import std.types { Bool } import std.measure { Bandwidth, bandwidth, bandwidth_count, SymbolRate, symbol_rate, symbol_rate_count } import std.decl_ref { DeclarationRef, WholeDeclaration } import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef } @@ -54,13 +54,6 @@ fn modulation_bits_per_symbol(m: Modulation) -> Nat { } } -fn modulation_label(m: Modulation) -> String { - match m { - Nrz => "NRZ" - Pam4 => "PAM4" - } -} - fn modulation_eq(a: Modulation, b: Modulation) -> Bool { match a { Nrz => match b { Nrz => true, Pam4 => false } @@ -221,14 +214,6 @@ fn hundred_gig_aggregate_collision() -> Bool { && !link_mode_eq(a: ieee_100gbase_cr4, b: ieee_100gbase_cr2) } -fn render_link_mode(m: LinkMode) -> String { - to_string(lane_count_value(l: m.lane_count)) - + "x" - + to_string(bandwidth_count(b: m.per_lane_service_rate)) - + " " - + modulation_label(m: m.modulation) -} - data extdeps_model_scope: ExternalModelScope = ExternalModelScope { subject: ExternalSubjectRef { declaration: DeclarationRef { diff --git a/dag/extdeps/transceiver/sff_8636.dag b/dag/extdeps/transceiver/sff_8636.dag index 9461ba7fa35..905a22aa2cc 100644 --- a/dag/extdeps/transceiver/sff_8636.dag +++ b/dag/extdeps/transceiver/sff_8636.dag @@ -132,11 +132,6 @@ fn sff8636_nominal_rate_from_byte140(code: Nat) -> Sff8636NominalRate { } } -// Byte 222, the extended field the escape points at, in units of 250 MBd. -fn sff8636_nominal_rate_from_byte222(code: Nat) -> SymbolRate { - symbol_rate(code * 250000000) -} - // ================= BYTE 192 / BYTE 116: EXTENDED SPECIFICATION COMPLIANCE ================= // // THE BYTE IS THE EVIDENCE; THE MODE LIST IS AN INTERPRETATION OF IT. An earlier head carried From df7aef897b14090b98ca833527b4d7c7a8bec3d8 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 6 Sep 2026 02:55:46 +0000 Subject: [PATCH 05/11] Two procurement gates: a purchase admits on a vendor claim, a receipt reconciles against a reading The substrate that landed in #10614 models the cable. It would not have stopped this order, because nothing consumes its findings at purchase time. These are the gates that do. THE ORDER WAS CORRECTLY ADMITTED, and the witness says so out loud because the opposite is the intuitive and wrong belief -- one this lane already published once and had to retract. FS's listing promises 4x100G legs of 2x50G PAM4, which is exactly the requirement, so a pre-purchase gate reading it ADMITS. A gate that refused would be reasoning from EEPROM bytes nobody could have had before delivery. So the two gates consume different evidence and may never share a carrier. Order admission takes a VENDOR CLAIM and refuses a purchase whose per-leg coding is undeclared -- the loud failure the subject exists to produce, since a part number does not determine a link contract and the EEPROM is field-programmed. Receipt reconciliation takes an OBSERVATION and joins it against the admitted claim; that is the gate that catches this class, an hour after delivery rather than after installation. The second is what keeps the first honest: a gate treating a claim as a reading would have greened here. CableLegCodingEvidence makes the grade structural rather than a flag, following the LandedCost split in product.inventory -- the arm IS the grade, so no path can promote a claim to a reading by forgetting to check something. ReceiptNotYetObserved is its own arm because SILENCE IS NOT AGREEMENT. A delivered assembly nobody has read must not reconcile as matching; that is exactly the state this fleet sat in while the fabric ran at half rate, and a model scoring it clean would have certified the outage. What the NIC requires is DECLARED BY THE FLEET, not derived from firmware. The ConnectX-7 was observed refusing 100G_2X; that rule has never been read here, and modelling an inferred algorithm as NVIDIA authority would turn a diagnosis into an invented specification. NOT VERIFIED: the seven claims in this witness have NOT been observed to execute. Local --required-floor reports FloorClean with planned unchanged at 3525 and zero of them in the population -- the module compiles and resolves, and something in floor discovery still does not offer it. A module-path fix (gunbc/product/X.dag declares `product.X`, not `gunbc.product.X`) was necessary but not sufficient. Reporting the gap rather than the green: a verdict whose population excludes its subject is not evidence, and this branch has already shipped one claim that no execution had ever checked. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01AigrH3JpxgSJBmqHMBAr6W --- dag/gunbc/product/cable_order_admission.dag | 208 ++++++++++++++++++ .../cable_order_admission_witness_test.dag | 159 +++++++++++++ 2 files changed, 367 insertions(+) create mode 100644 dag/gunbc/product/cable_order_admission.dag create mode 100644 dag/test/claim/cable_order_admission_witness_test.dag diff --git a/dag/gunbc/product/cable_order_admission.dag b/dag/gunbc/product/cable_order_admission.dag new file mode 100644 index 00000000000..7f77c4f5a44 --- /dev/null +++ b/dag/gunbc/product/cable_order_admission.dag @@ -0,0 +1,208 @@ +module product.cable_order_admission + +import std.types { Bool, List, NonEmptyStr } +import std.nat { Nat } +import extdeps.ethernet.link_mode { LinkMode, link_mode_eq } +import extdeps.transceiver.sff_8636 { + Sff8636LegCoding, Sff8636CodingFinding, + CodingAttestsRequestedMode, CodingAttestsRequestedModeSubjectToFec, + CodingInsufficientForRequestedMode, CodingContradictsEncoding, + CodingComplianceCodeNotUnderstood, + sff8636_assess_leg_coding, +} +import extdeps.external_authority { ExternalAuthority } + +// WHY A CABLE ORDER NEEDS AN ADMISSION GATE, AND WHAT THAT GATE CAN HONESTLY SEE. +// +// The subject is a purchase, not a part. Two 400G QSFP-DD breakout cables were bought to carry 100G +// per leg, arrived coded for 25G-per-lane modes, and now run at half the purchased rate on a link +// that is stable, pings clean at MTU 9000 and tests green on every instrument the fleet owns. The +// loss was not detected by anything; it was noticed by a person reading `ethtool -m`. +// +// THE GATE CANNOT OBSERVE AN UNDELIVERED CABLE. This is the correction that shaped the module, and +// it was got wrong first: an earlier account claimed this order would have refused before purchase +// because the observed EEPROM contradicts the listing. That reasons from bytes nobody could have +// had. FS's listing promises exactly the right thing -- 4x100G legs of 2x50G PAM4 -- so a +// pre-purchase gate reading the listing ADMITS this order, correctly, and the defect is invisible +// until the part is in hand. +// +// So there are two gates and they consume different evidence: +// +// ORDER ADMISSION consumes a VENDOR CLAIM. It refuses a purchase whose per-leg coding is +// undeclared, and admits one whose declared coding covers the requested mode -- +// as a PURCHASE, never as deployment acceptance. +// RECEIPT RECONCILE consumes an OBSERVATION. It joins the read EEPROM against the admitted claim. +// This is the gate that catches the class: an hour after delivery, rather than +// after installation. +// +// The second is what makes the first honest. A gate that treated a vendor claim as a reading would +// be satisfied by an assumption, and would have greened on this exact order. + +// ================= EVIDENCE, GRADED BY WHERE IT CAME FROM ================= +// +// A CLAIM AND A READING ARE DIFFERENT FACTS AND MAY NEVER SHARE A CARRIER. This follows the +// sibling LandedCost split in gunbc.product.inventory: the arm IS the grade, so no consumer parses +// a string to find out whether anyone actually looked at the hardware, and no code path can promote +// a claim to a reading by forgetting to check a flag. +// +// The vendor arm carries its citation because an unattributed claim is not evidence at all -- if +// nobody can say where the assertion came from, there is nothing to hold the vendor to later, which +// is precisely what an RMA needs. +type CableLegCodingEvidence + = LegCodingUndeclared + | LegCodingVendorAsserted { asserted_mode: LinkMode, citation: ExternalAuthority } + | LegCodingObserved { coding: Sff8636LegCoding } + +// ================= THE ENDPOINT PAIR THE CABLE MUST SERVE ================= +// +// A cable is not correct in the abstract; it is correct FOR two endpoints and a mode. Modelling the +// requirement as a fact about the link rather than about the part is what stops "is this a good +// cable" being askable at all -- the question has no answer without its endpoints. +// +// WHAT THE NIC REQUIRES IS OUR DIAGNOSIS, NOT NVIDIA'S SPECIFICATION. The ConnectX-7 was observed +// refusing 100G_2X with "Cable speed not enabled" against the delivered coding. That is an +// observation of behaviour, not a published rule, and this module deliberately does not model a +// firmware algorithm it has never read. `required_mode` is therefore declared by the fleet as what +// the link must carry, and the NIC's agreement with it is evidence to be gathered, never derived. +type CableLinkRequirement sole_constructor { + required_mode: LinkMode + purpose: NonEmptyStr +} + +fn cable_link_requirement(required_mode: LinkMode, purpose: NonEmptyStr) -> CableLinkRequirement { + CableLinkRequirement { required_mode: required_mode, purpose: purpose } +} + +// ================= ORDER ADMISSION ================= + +type CableOrderRefusalReason + = OrderCodingUndeclared { required: LinkMode } + | OrderClaimedModeIsNotRequiredMode { claimed: LinkMode, required: LinkMode } + | OrderObservedCodingDoesNotAttestRequiredMode { + required: LinkMode + finding: Sff8636CodingFinding + } + +// ADMISSION RECORDS WHAT IT WAS SATISFIED BY. `AdmittedOnVendorClaim` is a purchase authorisation +// and NOT an acceptance: it says the paperwork covers the requirement, and it carries the claim +// forward so receipt reconciliation has something to compare a reading against. Flattening the two +// admitted arms into one would erase exactly the distinction the incident turned on. +type CableOrderAdmission + = AdmittedOnVendorClaim { claimed_mode: LinkMode, citation: ExternalAuthority } + | AdmittedOnObservedCoding { coding: Sff8636LegCoding } + | OrderRefused { reason: CableOrderRefusalReason } + +// The gate. An undeclared coding REFUSES -- that is the loud failure the whole subject exists to +// produce, and it is the one this class of order actually needs, because a part number does not +// determine a link contract and the EEPROM is field-programmed. +fn admit_cable_order( + evidence: CableLegCodingEvidence, + requirement: CableLinkRequirement, +) -> CableOrderAdmission { + match evidence { + LegCodingUndeclared => + OrderRefused { reason: OrderCodingUndeclared { required: requirement.required_mode } } + LegCodingVendorAsserted { asserted_mode: claimed, citation: cite } => + if link_mode_eq(a: claimed, b: requirement.required_mode) { + AdmittedOnVendorClaim { claimed_mode: claimed, citation: cite } + } else { + OrderRefused { + reason: OrderClaimedModeIsNotRequiredMode { + claimed: claimed, required: requirement.required_mode } } + } + LegCodingObserved { coding: c } => { + let finding = sff8636_assess_leg_coding(coding: c, requested: requirement.required_mode) + match finding { + CodingAttestsRequestedMode { coding: ok } => AdmittedOnObservedCoding { coding: ok } + CodingAttestsRequestedModeSubjectToFec { coding: ok, fec: f } => + AdmittedOnObservedCoding { coding: ok } + CodingInsufficientForRequestedMode { requested: r, coding: bad } => + OrderRefused { + reason: OrderObservedCodingDoesNotAttestRequiredMode { + required: requirement.required_mode, finding: finding } } + CodingContradictsEncoding { encoding_modulation: m, attested_mode: a } => + OrderRefused { + reason: OrderObservedCodingDoesNotAttestRequiredMode { + required: requirement.required_mode, finding: finding } } + CodingComplianceCodeNotUnderstood { code: code } => + OrderRefused { + reason: OrderObservedCodingDoesNotAttestRequiredMode { + required: requirement.required_mode, finding: finding } } + } + } + } +} + +// ================= RECEIPT RECONCILIATION ================= +// +// THE GATE THAT WOULD HAVE CAUGHT THIS ORDER. It joins what arrived against what was admitted, and +// its divergence arm is the RMA evidence: the admitted claim, the observed finding, and the +// requirement they disagree about, all in one carrier so the correspondence with the vendor cites +// the same facts the model holds. +// +// A LOT NOT YET READ IS ITS OWN ARM. Silence is not agreement: a delivered assembly whose EEPROMs +// nobody has read must not reconcile as matching, because that is precisely the state this fleet +// was in for the weeks the fabric ran at half rate. +type CableReceiptReconciliation + = ReceiptNotYetObserved { admitted: CableOrderAdmission } + | ReceiptHonoursAdmittedClaim { coding: Sff8636LegCoding } + | ReceiptDivergesFromAdmittedClaim { + required: LinkMode + claimed_mode: LinkMode + observed_finding: Sff8636CodingFinding + } + | ReceiptReconciliationNotApplicable { admitted: CableOrderAdmission } + +fn reconcile_cable_receipt( + admitted: CableOrderAdmission, + observed: CableLegCodingEvidence, + requirement: CableLinkRequirement, +) -> CableReceiptReconciliation { + match admitted { + OrderRefused { reason: r } => ReceiptReconciliationNotApplicable { admitted: admitted } + AdmittedOnObservedCoding { coding: c } => + ReceiptReconciliationNotApplicable { admitted: admitted } + AdmittedOnVendorClaim { claimed_mode: claimed, citation: cite } => + match observed { + LegCodingUndeclared => ReceiptNotYetObserved { admitted: admitted } + LegCodingVendorAsserted { asserted_mode: m, citation: c2 } => + ReceiptNotYetObserved { admitted: admitted } + LegCodingObserved { coding: obs } => { + let finding = sff8636_assess_leg_coding( + coding: obs, requested: requirement.required_mode) + match finding { + CodingAttestsRequestedMode { coding: ok } => + ReceiptHonoursAdmittedClaim { coding: ok } + CodingAttestsRequestedModeSubjectToFec { coding: ok, fec: f } => + ReceiptHonoursAdmittedClaim { coding: ok } + CodingInsufficientForRequestedMode { requested: rq, coding: bad } => + ReceiptDivergesFromAdmittedClaim { + required: requirement.required_mode, + claimed_mode: claimed, + observed_finding: finding } + CodingContradictsEncoding { encoding_modulation: em, attested_mode: am } => + ReceiptDivergesFromAdmittedClaim { + required: requirement.required_mode, + claimed_mode: claimed, + observed_finding: finding } + CodingComplianceCodeNotUnderstood { code: code } => + ReceiptDivergesFromAdmittedClaim { + required: requirement.required_mode, + claimed_mode: claimed, + observed_finding: finding } + } + } + } + } +} + +// A divergence is the RMA trigger, named once so a consumer does not re-derive the predicate. +fn receipt_requires_supplier_remedy(r: CableReceiptReconciliation) -> Bool { + match r { + ReceiptDivergesFromAdmittedClaim { + required: rq, claimed_mode: cm, observed_finding: f } => true + ReceiptHonoursAdmittedClaim { coding: c } => false + ReceiptNotYetObserved { admitted: a } => false + ReceiptReconciliationNotApplicable { admitted: a } => false + } +} diff --git a/dag/test/claim/cable_order_admission_witness_test.dag b/dag/test/claim/cable_order_admission_witness_test.dag new file mode 100644 index 00000000000..d36eab4f3a0 --- /dev/null +++ b/dag/test/claim/cable_order_admission_witness_test.dag @@ -0,0 +1,159 @@ +module test.claim.cable_order_admission_witness + +import std.types { Bool, NonEmptyStr } +import extdeps.ethernet.link_mode { ieee_100gbase_cr2, ieee_100gbase_cr4 } +import extdeps.transceiver.sff_8636 { + Sff8636LegCoding, + SecondaryNotObserved, sff8636_leg_coding, sff8636_nominal_rate_from_byte140, + transceiver_identifier_from_byte, sff8636_encoding_from_byte, +} +import extdeps.external_authority { ExternalAuthority } +import extdeps.uri { Uri, Https } +import product.cable_order_admission { + CableLegCodingEvidence, CableOrderAdmission, CableReceiptReconciliation, + CableLinkRequirement, + LegCodingUndeclared, LegCodingVendorAsserted, LegCodingObserved, + AdmittedOnVendorClaim, AdmittedOnObservedCoding, OrderRefused, + ReceiptNotYetObserved, ReceiptHonoursAdmittedClaim, + ReceiptDivergesFromAdmittedClaim, ReceiptReconciliationNotApplicable, + cable_link_requirement, admit_cable_order, reconcile_cable_receipt, + receipt_requires_supplier_remedy, +} +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } + +// GREEN BY EXECUTION FOR THE TWO PROCUREMENT GATES, and the central case is the real order: it is +// ADMITTED at purchase and CAUGHT at receipt. Anyone reasoning about this incident wants to believe +// the order should have been refused up front; it should not have been, and the witness says so out +// loud so the belief cannot quietly return. +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +data fs_listing: ExternalAuthority = ExternalAuthority { + uri: Uri { scheme: Https, locator: "fs.com/products/139217.html" } +} + +data spark_rail_requirement: CableLinkRequirement = cable_link_requirement( + required_mode: ieee_100gbase_cr2, + purpose: "Spark fabric rail leg, CRS812 QSFP-DD breakout to ConnectX-7" as NonEmptyStr) + +// ---------------- gate 1: order admission ---------------- + +// THE LOUD FAILURE THE WHOLE SUBJECT EXISTS TO PRODUCE. A part whose per-leg coding nobody declared +// cannot be bought for a link that needs a specific mode, because a part number does not determine +// a link contract. +test fn an_undeclared_coding_refuses_the_purchase() -> Bool { + match admit_cable_order(evidence: LegCodingUndeclared, requirement: spark_rail_requirement) { + OrderRefused { reason: r } => true + AdmittedOnVendorClaim { claimed_mode: m, citation: c } => false + AdmittedOnObservedCoding { coding: c } => false + } +} + +// THE CENTRAL CASE, AND THE ONE MOST LIKELY TO BE MISREMEMBERED. FS's listing promises 4x100G legs +// of 2x50G PAM4 -- exactly the requirement -- so the real order is ADMITTED here. A gate that +// refused it would be reasoning from bytes nobody could have had before delivery. +test fn the_real_order_is_admitted_on_the_vendor_claim() -> Bool { + match admit_cable_order( + evidence: LegCodingVendorAsserted { + asserted_mode: ieee_100gbase_cr2, citation: fs_listing }, + requirement: spark_rail_requirement) { + AdmittedOnVendorClaim { claimed_mode: m, citation: c } => true + AdmittedOnObservedCoding { coding: c } => false + OrderRefused { reason: r } => false + } +} + +// A claim for the WRONG mode still refuses, so admission is not merely "the vendor said something". +test fn a_claim_for_a_different_mode_refuses() -> Bool { + match admit_cable_order( + evidence: LegCodingVendorAsserted { + asserted_mode: ieee_100gbase_cr4, citation: fs_listing }, + requirement: spark_rail_requirement) { + OrderRefused { reason: r } => true + AdmittedOnVendorClaim { claimed_mode: m, citation: c } => false + AdmittedOnObservedCoding { coding: c } => false + } +} + +// ---------------- gate 2: receipt reconciliation ---------------- + +// The delivered leg, as read. Byte 116 unread, primary 0x0B, PAM4 encoding, escape rate byte. +data delivered_leg: Sff8636LegCoding = sff8636_leg_coding( + identifier: transceiver_identifier_from_byte(code: 17), + primary_compliance_code: 11, + secondary_compliance: SecondaryNotObserved, + encoding: sff8636_encoding_from_byte(code: 8), + nominal_rate: sff8636_nominal_rate_from_byte140(code: 255)) + +data admitted_purchase: CableOrderAdmission = admit_cable_order( + evidence: LegCodingVendorAsserted { asserted_mode: ieee_100gbase_cr2, citation: fs_listing }, + requirement: spark_rail_requirement) + +// THE GATE THAT WOULD HAVE CAUGHT THIS ORDER, an hour after delivery instead of after installation. +test fn the_delivered_leg_diverges_from_the_admitted_claim() -> Bool { + match reconcile_cable_receipt( + admitted: admitted_purchase, + observed: LegCodingObserved { coding: delivered_leg }, + requirement: spark_rail_requirement) { + ReceiptDivergesFromAdmittedClaim { + required: rq, claimed_mode: cm, observed_finding: f } => true + ReceiptHonoursAdmittedClaim { coding: c } => false + ReceiptNotYetObserved { admitted: a } => false + ReceiptReconciliationNotApplicable { admitted: a } => false + } +} + +// AND THAT DIVERGENCE IS THE RMA TRIGGER, named once rather than re-derived by each consumer. +test fn a_divergence_requires_a_supplier_remedy() -> Bool { + receipt_requires_supplier_remedy(r: reconcile_cable_receipt( + admitted: admitted_purchase, + observed: LegCodingObserved { coding: delivered_leg }, + requirement: spark_rail_requirement)) +} + +// SILENCE IS NOT AGREEMENT. A delivered assembly nobody has read must NOT reconcile as matching -- +// that is exactly the state this fleet sat in while the fabric ran at half rate, and a model that +// scored it as clean would have certified the outage. +test fn an_unread_delivery_does_not_reconcile_as_matching() -> Bool { + match reconcile_cable_receipt( + admitted: admitted_purchase, + observed: LegCodingUndeclared, + requirement: spark_rail_requirement) { + ReceiptNotYetObserved { admitted: a } => true + ReceiptHonoursAdmittedClaim { coding: c } => false + ReceiptDivergesFromAdmittedClaim { required: rq, claimed_mode: cm, observed_finding: f } => false + ReceiptReconciliationNotApplicable { admitted: a } => false + } +} + +// THE POSITIVE CONTROL. A leg coded for the required mode reconciles as honouring the claim and +// needs no remedy -- without this arm every assertion above would pass for a gate that refused +// everything, which is a wall carrying no information. +data correctly_coded_leg: Sff8636LegCoding = sff8636_leg_coding( + identifier: transceiver_identifier_from_byte(code: 17), + primary_compliance_code: 11, + secondary_compliance: SecondaryNotObserved, + encoding: sff8636_encoding_from_byte(code: 8), + nominal_rate: sff8636_nominal_rate_from_byte140(code: 255)) + +// The CR4 requirement is one 0x0B genuinely attests, so this exercises the honouring path against +// the same decoder the divergence path uses. +data cr4_requirement: CableLinkRequirement = cable_link_requirement( + required_mode: ieee_100gbase_cr4, + purpose: "control: a link whose required mode this coding does attest" as NonEmptyStr) + +data admitted_cr4_purchase: CableOrderAdmission = admit_cable_order( + evidence: LegCodingVendorAsserted { asserted_mode: ieee_100gbase_cr4, citation: fs_listing }, + requirement: cr4_requirement) + +test fn a_leg_coded_for_the_required_mode_honours_the_claim() -> Bool { + let r = reconcile_cable_receipt( + admitted: admitted_cr4_purchase, + observed: LegCodingObserved { coding: correctly_coded_leg }, + requirement: cr4_requirement) + match r { + ReceiptHonoursAdmittedClaim { coding: c } => !receipt_requires_supplier_remedy(r: r) + ReceiptDivergesFromAdmittedClaim { required: rq, claimed_mode: cm, observed_finding: f } => false + ReceiptNotYetObserved { admitted: a } => false + ReceiptReconciliationNotApplicable { admitted: a } => false + } +} From 42d3b4481fa13cca20d99e66f44a8dd3c95d9049 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 6 Sep 2026 16:16:46 +0000 Subject: [PATCH 06/11] Retire the contradiction arm rather than keep it unreachable; 00h is specified ignorance Three repairs to the merged substrate, all from external review against the primary SFF tables. BYTE 116 AT 00h MEANS "UNSPECIFIED", NOT "NO SECONDARY APPLICATION". The merged profile_is_complete treated SecondaryObservedEmpty as completing the profile, which licensed a verdict the bytes do not support -- the same defect as using an UNREAD field as evidence of absence, arrived at from the other side. Two axes were hiding inside that one boolean and are now separate: for 00h the field WAS observed (required_fields_observed) while its interpretation is still not exhaustive (interpretation_is_exhaustive). Collapsing them is what made the defect recur one level down. SELF-CONSISTENCY IS NOW A DIFFERENT FUNCTION FROM REQUESTED-MODE ASSESSMENT. The merged assessor reached its contradiction branch only when the requested mode was unattested, so whether a module was called self-contradictory depended on what the reader asked for. sff8636_profile_consistency takes no requested mode, so the law holds mechanically rather than by discipline. AND THE CONTRADICTION ARM IS RETIRED, NOT KEPT UNREACHABLE. Deciding one requires establishing that the encoding byte and the compliance codes describe the SAME INTERFACE. SFF-8024 says encoding primarily concerns the HOST interface while compliance codes concern the media application; those are one signal only for an unretimed passive assembly, and disagree BY DESIGN in a module converting NRZ host lanes to a PAM4 media channel (NVIDIA's MMS1V70-CM presents four 25G NRZ host lanes and one 100G PAM4 optical channel, both true at once). Nothing this decoder reads settles that scope: identifier 0x11 is carried by optical modules as readily as by copper, and the field that would settle it -- SFF-8636's transmitter-technology nibble -- has not been read here. Authoring its code values from memory would be the fabricated citation this subject exists to catch. A result variant belongs in the operational codomain only if some valid input can produce it under the stated evidence rules. So the concept survives as a typed undecidable naming its cause -- unread field, unspecified field, unmodelled code, or the standing interface-scope frontier -- and the next-rung trigger is written down: read the transmitter-technology field, then reintroduce the arm WITH a standards-supported positive fixture and its inverse control. 0x40 IS MODELLED WITH ITS PRIMARY CITATION (SFF-8024 Rev 4.14, Table 4-4, row 40h: 50GBASE-CR, 100GBASE-CR2, 200GBASE-CR4), which retires the placeholder code 0 the first head used as a stand-in for a byte it had not read. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01AigrH3JpxgSJBmqHMBAr6W --- dag/extdeps/transceiver/sff_8636.dag | 169 +++++++++++++----- dag/gunbc/product/cable_order_admission.dag | 12 +- .../claim/cable_leg_coding_witness_test.dag | 124 ++++++++++--- 3 files changed, 223 insertions(+), 82 deletions(-) diff --git a/dag/extdeps/transceiver/sff_8636.dag b/dag/extdeps/transceiver/sff_8636.dag index 905a22aa2cc..b1a8ae7c070 100644 --- a/dag/extdeps/transceiver/sff_8636.dag +++ b/dag/extdeps/transceiver/sff_8636.dag @@ -7,8 +7,9 @@ import std.decl_ref { DeclarationRef, WholeDeclaration } import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef } import extdeps.uri { Uri, Https } import extdeps.ethernet.link_mode { - LinkMode, Modulation, Nrz, Pam4, modulation_eq, link_mode_eq, + LinkMode, Modulation, Nrz, Pam4, link_mode_eq, ieee_25gbase_cr, ieee_100gbase_cr4, ieee_50gbase_cr2, + ieee_50gbase_cr, ieee_100gbase_cr2, ieee_200gbase_cr4, } // THE MANAGEMENT EEPROM OF A QSFP MODULE OR CABLE LEG -- AND THE REASON A PART NUMBER IS NOT A LINK @@ -180,6 +181,15 @@ fn sff8636_interpret_extended_compliance(code: Nat) -> ComplianceInterpretation AttestedMode { mode: ieee_50gbase_cr2, fec: RequiresClause91Fec }, ], } + } else if code == 64 { + ComplianceUnderstood { + code: code, + modes: [ + AttestedMode { mode: ieee_50gbase_cr, fec: FecUnconditional }, + AttestedMode { mode: ieee_100gbase_cr2, fec: FecUnconditional }, + AttestedMode { mode: ieee_200gbase_cr4, fec: FecUnconditional }, + ], + } } else { ComplianceCodeUnmodelled { code: code } } @@ -194,7 +204,7 @@ fn sff8636_interpret_extended_compliance(code: Nat) -> ComplianceInterpretation // both and therefore proved contradiction from a gap in its own observation. type SecondaryComplianceObservation = SecondaryNotObserved - | SecondaryObservedEmpty + | SecondaryObservedUnspecified | SecondaryObservedCode { code: Nat } // ================= THE LEG CODING ================= @@ -227,24 +237,130 @@ fn sff8636_leg_coding( } } -// FIVE FINDINGS. Each says something different about what the bytes establish, and collapsing any -// pair would let a stronger claim absorb weaker evidence. +// ================= TWO QUESTIONS, TWO FUNCTIONS ================= +// +// "Is this profile self-contradictory" and "does it attest the mode I need" are different +// propositions, and the first must not depend on the second. An earlier head answered both from one +// decision, reaching the contradiction branch only when the requested mode was unattested -- so +// whether a module was called self-contradictory depended on what the reader happened to ask for. +// Self-consistency is a property of the observation alone, which is now true MECHANICALLY rather +// than by discipline: `sff8636_profile_consistency` takes no requested mode, so it cannot vary with +// one. +// +// WHY THERE IS NO OPERATIONAL CONTRADICTION ARM, AND WHY THAT IS THE HONEST OUTCOME. +// +// A contradiction between the encoding byte and the attested modes requires three things: every +// field the comparison needs actually READ, every read code UNDERSTOOD including sentinel meanings, +// and -- the one this module cannot supply -- the compared facts CONCERNING THE SAME INTERFACE. +// SFF-8024 says the encoding value primarily concerns the HOST interface, while the compliance codes +// concern the media application. Those are the same signal only for an unretimed passive assembly. +// For a module that converts between them the two disagree BY DESIGN: NVIDIA's MMS1V70-CM presents +// four 25G NRZ host lanes and one 100G PAM4 optical channel, and both descriptions are meant to be +// true at once. +// +// Nothing this module reads establishes that scope. The identifier does not: QSFP28 is carried by +// optical modules as readily as by copper. The field that would is SFF-8636's transmitter-technology +// nibble, which has not been read in this lane, and authoring its code values from memory is the +// fabricated citation this whole subject exists to catch. +// +// So the arm is RETIRED rather than kept unreachable. A result variant belongs in the operational +// codomain only if some valid input can actually produce it under the stated evidence rules; a +// branch that requires evidence nobody here can produce is precisely the apparent guarantee that +// later gets cited as stronger than it is. The DISTINCTION survives as a typed undecidable that says +// WHY it cannot be decided, so the frontier is named rather than silently absent. +// +// NEXT-RUNG TRIGGER: read SFF-8636's transmitter-technology field (byte 147 upper nibble) so +// passive-copper scope is established from the module's own bytes. At that point +// `ConsistencyInterfaceScopeUnestablished` becomes discharged for copper assemblies and a +// contradiction arm may be introduced WITH a positive fixture whose premises are standards-supported +// and an inverse control holding the same profile at SecondaryObservedUnspecified. + +// TWO AXES HID INSIDE ONE `profile_is_complete`, and collapsing them is what made the R1 defect +// recur one level down. For byte 116 at 00h the fields WERE observed and their interpretation is +// still not exhaustive, so a single boolean cannot say what is known. +fn sff8636_required_fields_observed(coding: Sff8636LegCoding) -> Bool { + match coding.secondary_compliance { + SecondaryNotObserved => false + SecondaryObservedUnspecified => true + SecondaryObservedCode { code: sc } => true + } +} + +// 00h IS SPECIFIED IGNORANCE, NOT ESTABLISHED ABSENCE. SFF-8636 gives byte 116 the value +// "Unspecified" at zero, so reading a zero tells you what the byte contains and NOT that the module +// declares no secondary application. An earlier head treated it as absence and thereby licensed a +// verdict the bytes do not support -- the same defect as using an UNREAD field as evidence of +// absence, arrived at from the other side. +fn sff8636_interpretation_is_exhaustive(coding: Sff8636LegCoding) -> Bool { + match coding.secondary_compliance { + SecondaryNotObserved => false + SecondaryObservedUnspecified => false + SecondaryObservedCode { code: sc } => length(sff8636_unmodelled_codes(coding: coding)) == 0 + } +} + +type ConsistencyUndecidableCause + = ConsistencySecondaryFieldUnread + | ConsistencySecondaryFieldUnspecified + | ConsistencyComplianceCodeNotUnderstood { code: Nat } + | ConsistencyInterfaceScopeUnestablished + +type ProfileConsistency + = ConsistencyUndecidable { cause: ConsistencyUndecidableCause } + +// The causes are ordered by what a reader could do about them: an unread field is a probe away, an +// unspecified one cannot be improved by reading harder, an unmodelled code is a decoder gap here, +// and the scope arm is the standing frontier above. +fn sff8636_profile_consistency(coding: Sff8636LegCoding) -> ProfileConsistency { + if !sff8636_required_fields_observed(coding: coding) { + ConsistencyUndecidable { cause: ConsistencySecondaryFieldUnread } + } else if !sff8636_interpretation_is_exhaustive(coding: coding) { + match sff8636_unmodelled_codes(coding: coding).first() { + Present { value: unknown } => + ConsistencyUndecidable { + cause: ConsistencyComplianceCodeNotUnderstood { code: unknown } } + Absent => ConsistencyUndecidable { cause: ConsistencySecondaryFieldUnspecified } + } + } else { + ConsistencyUndecidable { cause: ConsistencyInterfaceScopeUnestablished } + } +} + +// THE CONSTRUCTOR, because `sole_constructor` means this module owns construction and a consumer -- +// including a witness -- may not mint the type itself. +fn sff8636_leg_coding( + identifier: TransceiverIdentifier, + primary_compliance_code: Nat, + secondary_compliance: SecondaryComplianceObservation, + encoding: Sff8636Encoding, + nominal_rate: Sff8636NominalRate, +) -> Sff8636LegCoding { + Sff8636LegCoding { + identifier: identifier, + primary_compliance_code: primary_compliance_code, + secondary_compliance: secondary_compliance, + encoding: encoding, + nominal_rate: nominal_rate, + } +} + +// ================= THE REQUESTED-MODE QUESTION ================= +// +// Four findings, and no contradiction arm: this function answers only what the observed bytes +// attest about a mode someone needs. type Sff8636CodingFinding = CodingAttestsRequestedMode { coding: Sff8636LegCoding } | CodingAttestsRequestedModeSubjectToFec { coding: Sff8636LegCoding, fec: FecCondition } | CodingInsufficientForRequestedMode { requested: LinkMode, coding: Sff8636LegCoding } - | CodingContradictsEncoding { encoding_modulation: Modulation, attested_mode: LinkMode } | CodingComplianceCodeNotUnderstood { code: Nat } -// The interpretations of both observed codes. A not-observed secondary contributes nothing AND is -// remembered as unobserved by `sff8636_profile_is_complete` below. fn sff8636_interpretations(coding: Sff8636LegCoding) -> List { match coding.secondary_compliance { SecondaryObservedCode { code: sc } => [ sff8636_interpret_extended_compliance(code: coding.primary_compliance_code), sff8636_interpret_extended_compliance(code: sc), ] - SecondaryObservedEmpty => + SecondaryObservedUnspecified => [sff8636_interpret_extended_compliance(code: coding.primary_compliance_code)] SecondaryNotObserved => [sff8636_interpret_extended_compliance(code: coding.primary_compliance_code)] @@ -259,9 +375,6 @@ fn sff8636_attested(coding: Sff8636LegCoding) -> List { }) } -// Any code this decoder could not read. Its presence blocks both the acceptance and the -// contradiction claims: an unread code may attest the requested mode, and it may carry the -// application whose encoding is on the wire. fn sff8636_unmodelled_codes(coding: Sff8636LegCoding) -> List { flat_map(sff8636_interpretations(coding: coding), i => match i { @@ -270,17 +383,6 @@ fn sff8636_unmodelled_codes(coding: Sff8636LegCoding) -> List { }) } -// A CONTRADICTION NEEDS A COMPLETE, FULLY DECODED PROFILE. Both conditions are necessary: every -// declared field read, and every read code understood. -fn sff8636_profile_is_complete(coding: Sff8636LegCoding) -> Bool { - match coding.secondary_compliance { - SecondaryNotObserved => false - SecondaryObservedEmpty => length(sff8636_unmodelled_codes(coding: coding)) == 0 - SecondaryObservedCode { code: sc } => length(sff8636_unmodelled_codes(coding: coding)) == 0 - } -} - -// THE ASSESSMENT, ALWAYS RELATIVE TO A REQUESTED MODE. fn sff8636_assess_leg_coding( coding: Sff8636LegCoding, requested: LinkMode, @@ -297,28 +399,7 @@ fn sff8636_assess_leg_coding( Absent => match sff8636_unmodelled_codes(coding: coding).first() { Present { value: unknown } => CodingComplianceCodeNotUnderstood { code: unknown } - Absent => - match sff8636_encoding_modulation(e: coding.encoding) { - Absent => CodingInsufficientForRequestedMode { requested: requested, coding: coding } - Present { value: enc_mod } => - if !sff8636_profile_is_complete(coding: coding) { - CodingInsufficientForRequestedMode { requested: requested, coding: coding } - } else { - let agreeing = filter(attested, a => modulation_eq(a: a.mode.modulation, b: enc_mod)) - match agreeing.first() { - Present { value: ok } => - CodingInsufficientForRequestedMode { requested: requested, coding: coding } - Absent => - match attested.first() { - Present { value: bad } => - CodingContradictsEncoding { - encoding_modulation: enc_mod, attested_mode: bad.mode } - Absent => - CodingInsufficientForRequestedMode { requested: requested, coding: coding } - } - } - } - } + Absent => CodingInsufficientForRequestedMode { requested: requested, coding: coding } } } } diff --git a/dag/gunbc/product/cable_order_admission.dag b/dag/gunbc/product/cable_order_admission.dag index 7f77c4f5a44..d4b7b2b5e8b 100644 --- a/dag/gunbc/product/cable_order_admission.dag +++ b/dag/gunbc/product/cable_order_admission.dag @@ -6,8 +6,7 @@ import extdeps.ethernet.link_mode { LinkMode, link_mode_eq } import extdeps.transceiver.sff_8636 { Sff8636LegCoding, Sff8636CodingFinding, CodingAttestsRequestedMode, CodingAttestsRequestedModeSubjectToFec, - CodingInsufficientForRequestedMode, CodingContradictsEncoding, - CodingComplianceCodeNotUnderstood, + CodingInsufficientForRequestedMode, CodingComplianceCodeNotUnderstood, sff8636_assess_leg_coding, } import extdeps.external_authority { ExternalAuthority } @@ -120,10 +119,6 @@ fn admit_cable_order( OrderRefused { reason: OrderObservedCodingDoesNotAttestRequiredMode { required: requirement.required_mode, finding: finding } } - CodingContradictsEncoding { encoding_modulation: m, attested_mode: a } => - OrderRefused { - reason: OrderObservedCodingDoesNotAttestRequiredMode { - required: requirement.required_mode, finding: finding } } CodingComplianceCodeNotUnderstood { code: code } => OrderRefused { reason: OrderObservedCodingDoesNotAttestRequiredMode { @@ -180,11 +175,6 @@ fn reconcile_cable_receipt( required: requirement.required_mode, claimed_mode: claimed, observed_finding: finding } - CodingContradictsEncoding { encoding_modulation: em, attested_mode: am } => - ReceiptDivergesFromAdmittedClaim { - required: requirement.required_mode, - claimed_mode: claimed, - observed_finding: finding } CodingComplianceCodeNotUnderstood { code: code } => ReceiptDivergesFromAdmittedClaim { required: requirement.required_mode, diff --git a/dag/test/claim/cable_leg_coding_witness_test.dag b/dag/test/claim/cable_leg_coding_witness_test.dag index 027feb8f9df..5e2306a9a1c 100644 --- a/dag/test/claim/cable_leg_coding_witness_test.dag +++ b/dag/test/claim/cable_leg_coding_witness_test.dag @@ -12,9 +12,13 @@ import extdeps.ethernet.link_mode { import extdeps.transceiver.sff_8636 { Sff8636LegCoding, Sff8636CodingFinding, CodingAttestsRequestedMode, CodingAttestsRequestedModeSubjectToFec, - CodingInsufficientForRequestedMode, CodingContradictsEncoding, - CodingComplianceCodeNotUnderstood, - SecondaryNotObserved, SecondaryObservedEmpty, SecondaryObservedCode, + CodingInsufficientForRequestedMode, CodingComplianceCodeNotUnderstood, + SecondaryNotObserved, SecondaryObservedUnspecified, SecondaryObservedCode, + ProfileConsistency, ConsistencyUndecidable, + ConsistencySecondaryFieldUnread, ConsistencySecondaryFieldUnspecified, + ConsistencyComplianceCodeNotUnderstood, ConsistencyInterfaceScopeUnestablished, + sff8636_profile_consistency, + sff8636_required_fields_observed, sff8636_interpretation_is_exhaustive, ComplianceUnderstood, ComplianceCodeUnmodelled, FecUnconditional, RequiresClause91Fec, NominalRateEscaped, NominalRateDirect, @@ -98,7 +102,6 @@ fn is_insufficient(f: Sff8636CodingFinding) -> Bool { CodingInsufficientForRequestedMode { requested: r, coding: c } => true CodingAttestsRequestedMode { coding: c } => false CodingAttestsRequestedModeSubjectToFec { coding: c, fec: x } => false - CodingContradictsEncoding { encoding_modulation: m, attested_mode: a } => false CodingComplianceCodeNotUnderstood { code: c } => false } } @@ -108,7 +111,6 @@ fn attests_outright(f: Sff8636CodingFinding) -> Bool { CodingAttestsRequestedMode { coding: c } => true CodingAttestsRequestedModeSubjectToFec { coding: c, fec: x } => false CodingInsufficientForRequestedMode { requested: r, coding: c } => false - CodingContradictsEncoding { encoding_modulation: m, attested_mode: a } => false CodingComplianceCodeNotUnderstood { code: c } => false } } @@ -118,7 +120,6 @@ fn attests_subject_to_fec(f: Sff8636CodingFinding) -> Bool { CodingAttestsRequestedModeSubjectToFec { coding: c, fec: x } => true CodingAttestsRequestedMode { coding: c } => false CodingInsufficientForRequestedMode { requested: r, coding: c } => false - CodingContradictsEncoding { encoding_modulation: m, attested_mode: a } => false CodingComplianceCodeNotUnderstood { code: c } => false } } @@ -129,7 +130,6 @@ fn code_not_understood(f: Sff8636CodingFinding) -> Bool { CodingAttestsRequestedMode { coding: c } => false CodingAttestsRequestedModeSubjectToFec { coding: c, fec: x } => false CodingInsufficientForRequestedMode { requested: r, coding: c } => false - CodingContradictsEncoding { encoding_modulation: m, attested_mode: a } => false } } @@ -203,34 +203,104 @@ test fn an_unknown_byte_interprets_to_unknown_not_to_an_empty_attestation() -> B } } -// ---------------- contradiction requires a complete profile ---------------- +// ---------------- self-consistency is its own question ---------------- +// +// THE LAW, MADE MECHANICAL RATHER THAN OBSERVED. Changing the requested mode must not change whether +// a profile contradicts itself. `sff8636_profile_consistency` takes no requested mode, so the law +// holds by construction and this test records WHY the shape is what it is. +// +// THE ARM THAT IS NOT HERE. There is no operational contradiction verdict, because deciding one +// requires establishing that the encoding byte and the compliance codes describe the SAME +// INTERFACE -- true for an unretimed passive assembly, false by design for a module converting NRZ +// host lanes to a PAM4 media channel. Nothing this decoder reads settles that. Rather than keep a +// branch no valid input can reach, the distinction survives as a typed undecidable naming its cause. + +fn consistency_cause_is_unread(c: ProfileConsistency) -> Bool { + match c { + ConsistencyUndecidable { cause: cz } => + match cz { + ConsistencySecondaryFieldUnread => true + ConsistencySecondaryFieldUnspecified => false + ConsistencyComplianceCodeNotUnderstood { code: k } => false + ConsistencyInterfaceScopeUnestablished => false + } + } +} + +fn consistency_cause_is_unspecified(c: ProfileConsistency) -> Bool { + match c { + ConsistencyUndecidable { cause: cz } => + match cz { + ConsistencySecondaryFieldUnspecified => true + ConsistencySecondaryFieldUnread => false + ConsistencyComplianceCodeNotUnderstood { code: k } => false + ConsistencyInterfaceScopeUnestablished => false + } + } +} -// A leg whose byte 116 WAS read and found empty, whose primary code is understood, and whose every -// attested mode is NRZ while the encoding byte says PAM4. Only here is the profile complete enough -// for the strong claim, and this is the one fixture that may produce it. -data complete_profile_contradictory_leg: Sff8636LegCoding = sff8636_leg_coding( +fn consistency_cause_is_scope(c: ProfileConsistency) -> Bool { + match c { + ConsistencyUndecidable { cause: cz } => + match cz { + ConsistencyInterfaceScopeUnestablished => true + ConsistencySecondaryFieldUnread => false + ConsistencySecondaryFieldUnspecified => false + ConsistencyComplianceCodeNotUnderstood { code: k } => false + } + } +} + +// THE DELIVERED CABLE: byte 116 was never read, so the cause is the unread field and nothing +// stronger. This is the arm that used to be a contradiction accusation. +test fn the_delivered_leg_consistency_is_undecidable_for_want_of_a_reading() -> Bool { + consistency_cause_is_unread(c: sff8636_profile_consistency(coding: delivered_fs_leg)) +} + +// THE INVERSE CONTROL, and the specific bug it guards. A leg whose byte 116 WAS read and found 00h +// must NOT become decidable: 00h is "Unspecified", so reading it improves observation coverage while +// leaving interpretation non-exhaustive. An earlier head treated this exact case as establishing +// absence and licensed a verdict the bytes do not support. +data secondary_unspecified_leg: Sff8636LegCoding = sff8636_leg_coding( identifier: transceiver_identifier_from_byte(code: 17), primary_compliance_code: 11, - secondary_compliance: SecondaryObservedEmpty, + secondary_compliance: SecondaryObservedUnspecified, encoding: sff8636_encoding_from_byte(code: 8), nominal_rate: sff8636_nominal_rate_from_byte140(code: 255)) -fn is_contradiction(f: Sff8636CodingFinding) -> Bool { - match f { - CodingContradictsEncoding { encoding_modulation: m, attested_mode: a } => true - CodingAttestsRequestedMode { coding: c } => false - CodingAttestsRequestedModeSubjectToFec { coding: c, fec: x } => false - CodingInsufficientForRequestedMode { requested: r, coding: c } => false - CodingComplianceCodeNotUnderstood { code: c } => false - } +test fn reading_an_unspecified_secondary_does_not_make_the_profile_decidable() -> Bool { + consistency_cause_is_unspecified(c: sff8636_profile_consistency(coding: secondary_unspecified_leg)) +} + +// THE TWO AXES ARE SEPARATE, asserted directly: for 00h the field WAS observed and the +// interpretation is still not exhaustive. Collapsing these into one boolean is what made the defect +// recur, so the split is the thing under test. +test fn an_unspecified_secondary_is_observed_but_not_exhaustively_interpreted() -> Bool { + sff8636_required_fields_observed(coding: secondary_unspecified_leg) + && !sff8636_interpretation_is_exhaustive(coding: secondary_unspecified_leg) + && !sff8636_required_fields_observed(coding: delivered_fs_leg) +} + +// A FULLY READ, FULLY UNDERSTOOD PROFILE still cannot be decided -- and the cause names the frontier +// rather than going quiet. This is what stops the retired arm from reading as "nothing left to do". +data fully_understood_leg: Sff8636LegCoding = sff8636_leg_coding( + identifier: transceiver_identifier_from_byte(code: 17), + primary_compliance_code: 11, + secondary_compliance: SecondaryObservedCode { code: 64 }, + encoding: sff8636_encoding_from_byte(code: 8), + nominal_rate: sff8636_nominal_rate_from_byte140(code: 255)) + +test fn a_fully_read_profile_is_undecidable_only_for_interface_scope() -> Bool { + consistency_cause_is_scope(c: sff8636_profile_consistency(coding: fully_understood_leg)) } -// THE PAIR THAT MAKES THE COMPLETENESS CONDITION REAL. Identical bytes except that byte 116 is read -// in one and unread in the other: the read one may claim contradiction, the unread one may not. -// Without both arms, "contradiction requires a complete profile" would be prose no execution checks. -test fn contradiction_is_claimed_only_when_the_profile_was_fully_observed() -> Bool { - is_contradiction(f: sff8636_assess_leg_coding( - coding: complete_profile_contradictory_leg, requested: ieee_100gbase_cr2)) +// AND THE 0x40 ROW EARNS ITS CITATION. SFF-8024 Rev 4.14 Table 4-4 row 40h attests 50GBASE-CR, +// 100GBASE-CR2 and 200GBASE-CR4, so a leg carrying it in byte 116 DOES attest the mode the Spark +// rail needs -- which the delivered leg, carrying only 0x0B, does not. This is also the positive +// control that retires the placeholder code 0 the first head used. +test fn the_secondary_code_0x40_attests_the_mode_the_primary_does_not() -> Bool { + attests_outright(f: sff8636_assess_leg_coding( + coding: fully_understood_leg, requested: ieee_100gbase_cr2)) && is_insufficient(f: sff8636_assess_leg_coding( coding: delivered_fs_leg, requested: ieee_100gbase_cr2)) } From b285cf75f3d487579a8de9ee28c58694b397c525 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 6 Sep 2026 16:48:38 +0000 Subject: [PATCH 07/11] One constructor, not two: the rewrite left a duplicate sff8636_leg_coding The previous commit's rewrite added a constructor while the original survived in a preserved section, and the compiler refused the whole floor rather than letting the second silently replace the first: "duplicate declaration 'sff8636_leg_coding' -- a second declaration of one name silently replaced the first". That is the single-authority rule enforced at the language level, and the diagnostic names the HARM rather than only the fact. It is also the fourth self-inflicted break in this lane from doing a structural edit with text slicing, and every one was caught by execution rather than by reading. The rule the lane keeps relearning: a change that feels mechanical -- removing a helper, splitting a function, renaming an arm -- earns the same verification as a new feature, and a dirty tree verifies nothing because the floor plans its changed set from COMMITTED state. Floor now verdict=FloorClean, claims_failed=0, with all six changed cable claims planned-and-passed: the delivered leg's consistency undecidable for want of a reading, the inverse control holding an unspecified secondary undecidable, the two completeness axes asserted separately, the fully-read profile undecidable only for interface scope, and the cited 0x40 row attesting the mode the primary does not. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01AigrH3JpxgSJBmqHMBAr6W --- dag/extdeps/transceiver/sff_8636.dag | 18 ------------------ 1 file changed, 18 deletions(-) diff --git a/dag/extdeps/transceiver/sff_8636.dag b/dag/extdeps/transceiver/sff_8636.dag index b1a8ae7c070..f6695dffa2a 100644 --- a/dag/extdeps/transceiver/sff_8636.dag +++ b/dag/extdeps/transceiver/sff_8636.dag @@ -326,24 +326,6 @@ fn sff8636_profile_consistency(coding: Sff8636LegCoding) -> ProfileConsistency { } } -// THE CONSTRUCTOR, because `sole_constructor` means this module owns construction and a consumer -- -// including a witness -- may not mint the type itself. -fn sff8636_leg_coding( - identifier: TransceiverIdentifier, - primary_compliance_code: Nat, - secondary_compliance: SecondaryComplianceObservation, - encoding: Sff8636Encoding, - nominal_rate: Sff8636NominalRate, -) -> Sff8636LegCoding { - Sff8636LegCoding { - identifier: identifier, - primary_compliance_code: primary_compliance_code, - secondary_compliance: secondary_compliance, - encoding: encoding, - nominal_rate: nominal_rate, - } -} - // ================= THE REQUESTED-MODE QUESTION ================= // // Four findings, and no contradiction arm: this function answers only what the observed bytes From ab25aeab6d7b9c824c2e7cfe13dc7d96d5a1503d Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 6 Sep 2026 17:06:39 +0000 Subject: [PATCH 08/11] wip: rehome observation layer --- dag/extdeps/transceiver/sff_8636.dag | 217 +++--------------- dag/gunbc/product/cable_leg_observation.dag | 207 +++++++++++++++++ dag/gunbc/product/cable_order_admission.dag | 42 ++-- .../claim/cable_leg_coding_witness_test.dag | 194 ++++++++++------ .../cable_order_admission_witness_test.dag | 10 +- 5 files changed, 383 insertions(+), 287 deletions(-) create mode 100644 dag/gunbc/product/cable_leg_observation.dag diff --git a/dag/extdeps/transceiver/sff_8636.dag b/dag/extdeps/transceiver/sff_8636.dag index f6695dffa2a..44bd2878563 100644 --- a/dag/extdeps/transceiver/sff_8636.dag +++ b/dag/extdeps/transceiver/sff_8636.dag @@ -26,9 +26,19 @@ import extdeps.ethernet.link_mode { // external upstream decomposition, and it carries a reading of these fields rather than redefining // them. // -// WHAT THIS MODULE MAY AND MAY NOT CONCLUDE. It reads bytes and reports findings about bytes. It -// does not certify hardware: no reading here establishes that a given assembly will carry a given -// mode, and a leg whose coding is impeccable can still fail electrically. +// WHAT THIS MODULE MAY AND MAY NOT CONCLUDE. It owns BYTE MEANINGS and nothing else: given a value, +// what does the specification say it denotes. It does not certify hardware, and no reading here +// establishes that a given assembly will carry a given mode. +// +// IN PARTICULAR IT OWNS NO OBSERVATION. An earlier head authored `SecondaryNotObserved` and a +// completeness predicate here, which is the layer inversion DESIGN section 3 names outright: +// "Observations produced by this repository are receipts in the observing product or workflow +// layer, not facts owned by the observed upstream. Missing observations are coverage obligations +// downstream, never `Unobserved` properties authored inside an upstream module." Whether anyone +// read byte 116 is a fact about THIS FLEET's probing, not about SFF-8636, and a specification that +// carried it would be asserting something the standard never says. The observation model, its +// coverage, its consistency assessment and the requested-mode join all live in +// `product.cable_leg_observation`. // // THE OBSERVED DEFECT MUST STAY REPRESENTABLE. An earlier head said the delivered cable "would have // had no constructor", which is backwards: a model that cannot record a contradictory EEPROM cannot @@ -121,13 +131,21 @@ fn sff8636_encoding_modulation(e: Sff8636Encoding) -> Modulation? { // raw dump (`ethtool -m raw on`), not the decoded view. Until that is read, a leg whose byte // 140 is 255 carries NominalRateEscaped and NOT a 25.5 GBd claim, because recording an escape marker // as a measurement is the fabrication this whole subject exists to catch. +// 00h AND FFh ARE BOTH SENTINELS AND NEITHER IS A RATE. SFF-8636 gives 0 the meaning "not +// specified; determine from module technology" and FFh the meaning "exceeds one byte; read the +// extended field". An earlier head multiplied 0 out to 0 baud, which is a fabricated measurement +// wearing a unit -- a consumer comparing it to a required rate would read the module as infinitely +// slow rather than as silent. type Sff8636NominalRate - = NominalRateDirect { rate: SymbolRate } + = NominalRateUnspecified + | NominalRateDirect { rate: SymbolRate } | NominalRateEscaped fn sff8636_nominal_rate_from_byte140(code: Nat) -> Sff8636NominalRate { if code == 255 { NominalRateEscaped + } else if code == 0 { + NominalRateUnspecified } else { NominalRateDirect { rate: symbol_rate(code * 100000000) } } @@ -160,6 +178,7 @@ type AttestedMode sole_constructor { type ComplianceInterpretation = ComplianceUnderstood { code: Nat, modes: List } + | ComplianceUnspecified { code: Nat } | ComplianceCodeUnmodelled { code: Nat } // THE DECODER. Rows are read from SFF-8024's extended-compliance table; a code with no row here @@ -169,10 +188,12 @@ type ComplianceInterpretation // omitted 50GBASE-CR2 with Clause 91 FEC, which changes behaviour: a 50GBASE-CR2 request against // this code returned "insufficient" when the standard's entry does include that mode, subject to its // FEC condition. The omission was found by an external standards cross-check (SFF-8024 Rev 4.14, -// Table 4-6) rather than by anything in this repository, and the FEC qualification is carried rather +// Table 4-4) rather than by anything in this repository, and the FEC qualification is carried rather // than dropped so the conditional entry cannot be read as unconditional support. fn sff8636_interpret_extended_compliance(code: Nat) -> ComplianceInterpretation { - if code == 11 { + if code == 0 { + ComplianceUnspecified { code: code } + } else if code == 11 { ComplianceUnderstood { code: code, modes: [ @@ -202,190 +223,6 @@ fn sff8636_interpret_extended_compliance(code: Nat) -> ComplianceInterpretation // encoding byte. That claim cannot be made while byte 116 has not been read, because the unread // field may carry the very application the encoding belongs to. The earlier head used `Absent` for // both and therefore proved contradiction from a gap in its own observation. -type SecondaryComplianceObservation - = SecondaryNotObserved - | SecondaryObservedUnspecified - | SecondaryObservedCode { code: Nat } - -// ================= THE LEG CODING ================= -// -// The coding carries RAW BYTES. Nothing here lets a caller supply a capability directly. -type Sff8636LegCoding sole_constructor { - identifier: TransceiverIdentifier - primary_compliance_code: Nat - secondary_compliance: SecondaryComplianceObservation - encoding: Sff8636Encoding - nominal_rate: Sff8636NominalRate -} - -// THE CONSTRUCTOR, because `sole_constructor` means this module owns construction and a consumer -- -// including a witness -- may not mint the type itself. That is the same rule R2 asked for one level -// down: the caller supplies OBSERVED BYTES, and the module decides what they mean. -fn sff8636_leg_coding( - identifier: TransceiverIdentifier, - primary_compliance_code: Nat, - secondary_compliance: SecondaryComplianceObservation, - encoding: Sff8636Encoding, - nominal_rate: Sff8636NominalRate, -) -> Sff8636LegCoding { - Sff8636LegCoding { - identifier: identifier, - primary_compliance_code: primary_compliance_code, - secondary_compliance: secondary_compliance, - encoding: encoding, - nominal_rate: nominal_rate, - } -} - -// ================= TWO QUESTIONS, TWO FUNCTIONS ================= -// -// "Is this profile self-contradictory" and "does it attest the mode I need" are different -// propositions, and the first must not depend on the second. An earlier head answered both from one -// decision, reaching the contradiction branch only when the requested mode was unattested -- so -// whether a module was called self-contradictory depended on what the reader happened to ask for. -// Self-consistency is a property of the observation alone, which is now true MECHANICALLY rather -// than by discipline: `sff8636_profile_consistency` takes no requested mode, so it cannot vary with -// one. -// -// WHY THERE IS NO OPERATIONAL CONTRADICTION ARM, AND WHY THAT IS THE HONEST OUTCOME. -// -// A contradiction between the encoding byte and the attested modes requires three things: every -// field the comparison needs actually READ, every read code UNDERSTOOD including sentinel meanings, -// and -- the one this module cannot supply -- the compared facts CONCERNING THE SAME INTERFACE. -// SFF-8024 says the encoding value primarily concerns the HOST interface, while the compliance codes -// concern the media application. Those are the same signal only for an unretimed passive assembly. -// For a module that converts between them the two disagree BY DESIGN: NVIDIA's MMS1V70-CM presents -// four 25G NRZ host lanes and one 100G PAM4 optical channel, and both descriptions are meant to be -// true at once. -// -// Nothing this module reads establishes that scope. The identifier does not: QSFP28 is carried by -// optical modules as readily as by copper. The field that would is SFF-8636's transmitter-technology -// nibble, which has not been read in this lane, and authoring its code values from memory is the -// fabricated citation this whole subject exists to catch. -// -// So the arm is RETIRED rather than kept unreachable. A result variant belongs in the operational -// codomain only if some valid input can actually produce it under the stated evidence rules; a -// branch that requires evidence nobody here can produce is precisely the apparent guarantee that -// later gets cited as stronger than it is. The DISTINCTION survives as a typed undecidable that says -// WHY it cannot be decided, so the frontier is named rather than silently absent. -// -// NEXT-RUNG TRIGGER: read SFF-8636's transmitter-technology field (byte 147 upper nibble) so -// passive-copper scope is established from the module's own bytes. At that point -// `ConsistencyInterfaceScopeUnestablished` becomes discharged for copper assemblies and a -// contradiction arm may be introduced WITH a positive fixture whose premises are standards-supported -// and an inverse control holding the same profile at SecondaryObservedUnspecified. - -// TWO AXES HID INSIDE ONE `profile_is_complete`, and collapsing them is what made the R1 defect -// recur one level down. For byte 116 at 00h the fields WERE observed and their interpretation is -// still not exhaustive, so a single boolean cannot say what is known. -fn sff8636_required_fields_observed(coding: Sff8636LegCoding) -> Bool { - match coding.secondary_compliance { - SecondaryNotObserved => false - SecondaryObservedUnspecified => true - SecondaryObservedCode { code: sc } => true - } -} - -// 00h IS SPECIFIED IGNORANCE, NOT ESTABLISHED ABSENCE. SFF-8636 gives byte 116 the value -// "Unspecified" at zero, so reading a zero tells you what the byte contains and NOT that the module -// declares no secondary application. An earlier head treated it as absence and thereby licensed a -// verdict the bytes do not support -- the same defect as using an UNREAD field as evidence of -// absence, arrived at from the other side. -fn sff8636_interpretation_is_exhaustive(coding: Sff8636LegCoding) -> Bool { - match coding.secondary_compliance { - SecondaryNotObserved => false - SecondaryObservedUnspecified => false - SecondaryObservedCode { code: sc } => length(sff8636_unmodelled_codes(coding: coding)) == 0 - } -} - -type ConsistencyUndecidableCause - = ConsistencySecondaryFieldUnread - | ConsistencySecondaryFieldUnspecified - | ConsistencyComplianceCodeNotUnderstood { code: Nat } - | ConsistencyInterfaceScopeUnestablished - -type ProfileConsistency - = ConsistencyUndecidable { cause: ConsistencyUndecidableCause } - -// The causes are ordered by what a reader could do about them: an unread field is a probe away, an -// unspecified one cannot be improved by reading harder, an unmodelled code is a decoder gap here, -// and the scope arm is the standing frontier above. -fn sff8636_profile_consistency(coding: Sff8636LegCoding) -> ProfileConsistency { - if !sff8636_required_fields_observed(coding: coding) { - ConsistencyUndecidable { cause: ConsistencySecondaryFieldUnread } - } else if !sff8636_interpretation_is_exhaustive(coding: coding) { - match sff8636_unmodelled_codes(coding: coding).first() { - Present { value: unknown } => - ConsistencyUndecidable { - cause: ConsistencyComplianceCodeNotUnderstood { code: unknown } } - Absent => ConsistencyUndecidable { cause: ConsistencySecondaryFieldUnspecified } - } - } else { - ConsistencyUndecidable { cause: ConsistencyInterfaceScopeUnestablished } - } -} - -// ================= THE REQUESTED-MODE QUESTION ================= -// -// Four findings, and no contradiction arm: this function answers only what the observed bytes -// attest about a mode someone needs. -type Sff8636CodingFinding - = CodingAttestsRequestedMode { coding: Sff8636LegCoding } - | CodingAttestsRequestedModeSubjectToFec { coding: Sff8636LegCoding, fec: FecCondition } - | CodingInsufficientForRequestedMode { requested: LinkMode, coding: Sff8636LegCoding } - | CodingComplianceCodeNotUnderstood { code: Nat } - -fn sff8636_interpretations(coding: Sff8636LegCoding) -> List { - match coding.secondary_compliance { - SecondaryObservedCode { code: sc } => [ - sff8636_interpret_extended_compliance(code: coding.primary_compliance_code), - sff8636_interpret_extended_compliance(code: sc), - ] - SecondaryObservedUnspecified => - [sff8636_interpret_extended_compliance(code: coding.primary_compliance_code)] - SecondaryNotObserved => - [sff8636_interpret_extended_compliance(code: coding.primary_compliance_code)] - } -} - -fn sff8636_attested(coding: Sff8636LegCoding) -> List { - flat_map(sff8636_interpretations(coding: coding), i => - match i { - ComplianceUnderstood { code: c, modes: ms } => ms - ComplianceCodeUnmodelled { code: c } => [] - }) -} - -fn sff8636_unmodelled_codes(coding: Sff8636LegCoding) -> List { - flat_map(sff8636_interpretations(coding: coding), i => - match i { - ComplianceCodeUnmodelled { code: c } => [c] - ComplianceUnderstood { code: c, modes: ms } => [] - }) -} - -fn sff8636_assess_leg_coding( - coding: Sff8636LegCoding, - requested: LinkMode, -) -> Sff8636CodingFinding { - let attested = sff8636_attested(coding: coding) - let matching = filter(attested, a => link_mode_eq(a: a.mode, b: requested)) - match matching.first() { - Present { value: hit } => - match hit.fec { - FecUnconditional => CodingAttestsRequestedMode { coding: coding } - RequiresClause91Fec => - CodingAttestsRequestedModeSubjectToFec { coding: coding, fec: hit.fec } - } - Absent => - match sff8636_unmodelled_codes(coding: coding).first() { - Present { value: unknown } => CodingComplianceCodeNotUnderstood { code: unknown } - Absent => CodingInsufficientForRequestedMode { requested: requested, coding: coding } - } - } -} - data extdeps_model_scope: ExternalModelScope = ExternalModelScope { subject: ExternalSubjectRef { declaration: DeclarationRef { diff --git a/dag/gunbc/product/cable_leg_observation.dag b/dag/gunbc/product/cable_leg_observation.dag new file mode 100644 index 00000000000..f5c3e902742 --- /dev/null +++ b/dag/gunbc/product/cable_leg_observation.dag @@ -0,0 +1,207 @@ +module product.cable_leg_observation + +import std.nat { Nat } +import std.types { Bool, List } +import extdeps.ethernet.link_mode { LinkMode, link_mode_eq } +import extdeps.transceiver.sff_8636 { + TransceiverIdentifier, Sff8636Encoding, Sff8636NominalRate, + EncodingUnspecified, Encoding64b66b, EncodingPam4, EncodingUnmodelled, + AttestedMode, FecCondition, FecUnconditional, RequiresClause91Fec, + ComplianceInterpretation, ComplianceUnderstood, ComplianceUnspecified, + ComplianceCodeUnmodelled, + sff8636_interpret_extended_compliance, +} + +// WHAT THIS FLEET READ OFF A CABLE LEG, AND WHAT FOLLOWS FROM IT. +// +// THE LAYER IS THE POINT. `extdeps.transceiver.sff_8636` owns byte MEANINGS -- given a value, what +// the specification says it denotes. It does not and may not own whether anyone here pointed +// `ethtool -m` at a module. An earlier head authored `SecondaryNotObserved` and a completeness +// predicate inside that specification module, which is the inversion DESIGN section 3 names in +// terms: observations are receipts in the OBSERVING layer, and "missing observations are coverage +// obligations downstream, never `Unobserved` properties authored inside an upstream module." +// +// The tell was available and was missed twice, because this lane raised the identical objection +// against another module's `..._observed` row in extdeps hours before committing its own. A rule +// stated generally and applied locally is the recurring shape of this whole subject. +// +// So: an observation is a fleet receipt. It records the bytes read from one leg, WHICH bytes were +// read, and nothing about what the standard means -- every meaning is asked of the extdeps decoder. + +// A SECONDARY FIELD EITHER WAS READ OR WAS NOT, and if it was, the RAW BYTE is what is carried. +// There is deliberately no `ObservedUnspecified` variant: 00h already means "Unspecified" in the +// SFF-8024 table that governs this byte, so offering an authored variant beside the raw value would +// let the caller choose the interpretation -- the decorative-byte defect, one field over. +type SecondaryComplianceObservation + = SecondaryNotObserved + | SecondaryObserved { code: Nat } + +type CableLegObservation sole_constructor { + identifier: TransceiverIdentifier + primary_compliance_code: Nat + secondary_compliance: SecondaryComplianceObservation + encoding: Sff8636Encoding + nominal_rate: Sff8636NominalRate +} + +fn cable_leg_observation( + identifier: TransceiverIdentifier, + primary_compliance_code: Nat, + secondary_compliance: SecondaryComplianceObservation, + encoding: Sff8636Encoding, + nominal_rate: Sff8636NominalRate, +) -> CableLegObservation { + CableLegObservation { + identifier: identifier, + primary_compliance_code: primary_compliance_code, + secondary_compliance: secondary_compliance, + encoding: encoding, + nominal_rate: nominal_rate, + } +} + +// ================= COVERAGE: WHICH FIELDS THIS FLEET ACTUALLY READ ================= +// +// ONE FOLD OVER THE FIELDS, NOT A PREDICATE PER VARIANT. The previous shape was a +// variant-to-Boolean function per question, which is the non-fold residue DESIGN section 6 asks to +// be routed through a canonical accessor. The coverage census is a fold producing the list of +// UNREAD fields, and every coverage question is asked of that one list -- so a new field is one row +// here rather than a new predicate at every call site. +type CableLegField = SecondaryComplianceField + +fn cable_leg_unread_fields(obs: CableLegObservation) -> List { + match obs.secondary_compliance { + SecondaryNotObserved => [SecondaryComplianceField] + SecondaryObserved { code: sc } => [] + } +} + +// ================= INTERPRETABILITY: WHICH READ VALUES THE DECODER UNDERSTOOD ================= +// +// Coverage and interpretability are different axes and must not collapse into one boolean. For a +// secondary byte of 00h the field WAS read and its value is still a gap: SFF-8024 assigns 00h the +// meaning "Unspecified", which is specified ignorance rather than established absence. Collapsing +// the two is what made this defect recur once already. +// +// A GAP NAMES ITS FIELD. An earlier head asked only about compliance codes, so an observation whose +// ENCODING byte was unspecified still reported the interface-scope frontier -- blaming a field whose +// reading would not have made the observation decidable. +type InterpretationGap + = GapComplianceUnspecified { code: Nat } + | GapComplianceNotUnderstood { code: Nat } + | GapEncodingUnspecified + | GapEncodingNotUnderstood { code: Nat } + +fn cable_leg_interpretations(obs: CableLegObservation) -> List { + match obs.secondary_compliance { + SecondaryObserved { code: sc } => [ + sff8636_interpret_extended_compliance(code: obs.primary_compliance_code), + sff8636_interpret_extended_compliance(code: sc), + ] + SecondaryNotObserved => + [sff8636_interpret_extended_compliance(code: obs.primary_compliance_code)] + } +} + +fn cable_leg_attested(obs: CableLegObservation) -> List { + flat_map(cable_leg_interpretations(obs: obs), i => + match i { + ComplianceUnderstood { code: c, modes: ms } => ms + ComplianceUnspecified { code: c } => [] + ComplianceCodeUnmodelled { code: c } => [] + }) +} + +fn cable_leg_encoding_gaps(obs: CableLegObservation) -> List { + match obs.encoding { + EncodingUnspecified => [GapEncodingUnspecified] + EncodingUnmodelled { code: c } => [GapEncodingNotUnderstood { code: c }] + Encoding64b66b => [] + EncodingPam4 => [] + } +} + +fn cable_leg_compliance_gaps(obs: CableLegObservation) -> List { + flat_map(cable_leg_interpretations(obs: obs), i => + match i { + ComplianceUnspecified { code: c } => [GapComplianceUnspecified { code: c }] + ComplianceCodeUnmodelled { code: c } => [GapComplianceNotUnderstood { code: c }] + ComplianceUnderstood { code: c, modes: ms } => [] + }) +} + +// The single census every interpretability question is asked of. +fn cable_leg_interpretation_gaps(obs: CableLegObservation) -> List { + concat(cable_leg_compliance_gaps(obs: obs), cable_leg_encoding_gaps(obs: obs)) +} + +// ================= SELF-CONSISTENCY ================= +// +// TAKES NO REQUESTED MODE, so "does this observation contradict itself" cannot vary with what a +// reader happened to ask for. The law holds by construction rather than by discipline. +// +// THERE IS NO OPERATIONAL CONTRADICTION ARM. Deciding one requires the encoding byte and the +// compliance codes to describe the SAME INTERFACE -- true for an unretimed passive assembly, false +// by design for a module converting NRZ host lanes to a PAM4 media channel. Nothing observed here +// settles that: the identifier does not distinguish copper from optical, and the field that would -- +// SFF-8636's transmitter-technology nibble -- has not been read. A result variant belongs in the +// operational codomain only if some valid input can produce it, so the arm is retired and the +// distinction survives as a typed undecidable naming its cause. +// +// NEXT-RUNG TRIGGER: model the transmitter-technology field in extdeps and read it here, then +// reintroduce the arm WITH a standards-supported positive fixture and an inverse control holding the +// same observation at a secondary byte of 00h. +type ConsistencyUndecidableCause + = ConsistencyFieldUnread { field: CableLegField } + | ConsistencyInterpretationGap { gap: InterpretationGap } + | ConsistencyInterfaceScopeUnestablished + +type ProfileConsistency + = ConsistencyUndecidable { cause: ConsistencyUndecidableCause } + +fn cable_leg_consistency(obs: CableLegObservation) -> ProfileConsistency { + match cable_leg_unread_fields(obs: obs).first() { + Present { value: f } => ConsistencyUndecidable { cause: ConsistencyFieldUnread { field: f } } + Absent => + match cable_leg_interpretation_gaps(obs: obs).first() { + Present { value: gap } => + ConsistencyUndecidable { cause: ConsistencyInterpretationGap { gap: gap } } + Absent => ConsistencyUndecidable { cause: ConsistencyInterfaceScopeUnestablished } + } + } +} + +// ================= THE REQUESTED-MODE JOIN ================= +// +// A join of an OBSERVATION against a DEMAND, which is why it lives here and not in extdeps: the +// specification has no opinion about what this fleet needs. +type CableLegFinding + = LegAttestsRequestedMode { obs: CableLegObservation } + | LegAttestsRequestedModeSubjectToFec { obs: CableLegObservation, fec: FecCondition } + | LegInsufficientForRequestedMode { requested: LinkMode, obs: CableLegObservation } + | LegComplianceCodeNotUnderstood { code: Nat } + +fn assess_cable_leg(obs: CableLegObservation, requested: LinkMode) -> CableLegFinding { + let matching = filter(cable_leg_attested(obs: obs), a => link_mode_eq(a: a.mode, b: requested)) + match matching.first() { + Present { value: hit } => + match hit.fec { + FecUnconditional => LegAttestsRequestedMode { obs: obs } + RequiresClause91Fec => + LegAttestsRequestedModeSubjectToFec { obs: obs, fec: hit.fec } + } + Absent => { + let unknown = flat_map(cable_leg_interpretation_gaps(obs: obs), g => + match g { + GapComplianceNotUnderstood { code: c } => [c] + GapComplianceUnspecified { code: c } => [] + GapEncodingUnspecified => [] + GapEncodingNotUnderstood { code: c } => [] + }) + match unknown.first() { + Present { value: k } => LegComplianceCodeNotUnderstood { code: k } + Absent => LegInsufficientForRequestedMode { requested: requested, obs: obs } + } + } + } +} diff --git a/dag/gunbc/product/cable_order_admission.dag b/dag/gunbc/product/cable_order_admission.dag index d4b7b2b5e8b..4562dfa20eb 100644 --- a/dag/gunbc/product/cable_order_admission.dag +++ b/dag/gunbc/product/cable_order_admission.dag @@ -3,11 +3,11 @@ module product.cable_order_admission import std.types { Bool, List, NonEmptyStr } import std.nat { Nat } import extdeps.ethernet.link_mode { LinkMode, link_mode_eq } -import extdeps.transceiver.sff_8636 { - Sff8636LegCoding, Sff8636CodingFinding, - CodingAttestsRequestedMode, CodingAttestsRequestedModeSubjectToFec, - CodingInsufficientForRequestedMode, CodingComplianceCodeNotUnderstood, - sff8636_assess_leg_coding, +import product.cable_leg_observation { + CableLegObservation, CableLegFinding, + LegAttestsRequestedMode, LegAttestsRequestedModeSubjectToFec, + LegInsufficientForRequestedMode, LegComplianceCodeNotUnderstood, + assess_cable_leg, } import extdeps.external_authority { ExternalAuthority } @@ -50,7 +50,7 @@ import extdeps.external_authority { ExternalAuthority } type CableLegCodingEvidence = LegCodingUndeclared | LegCodingVendorAsserted { asserted_mode: LinkMode, citation: ExternalAuthority } - | LegCodingObserved { coding: Sff8636LegCoding } + | LegCodingObserved { coding: CableLegObservation } // ================= THE ENDPOINT PAIR THE CABLE MUST SERVE ================= // @@ -79,7 +79,7 @@ type CableOrderRefusalReason | OrderClaimedModeIsNotRequiredMode { claimed: LinkMode, required: LinkMode } | OrderObservedCodingDoesNotAttestRequiredMode { required: LinkMode - finding: Sff8636CodingFinding + finding: CableLegFinding } // ADMISSION RECORDS WHAT IT WAS SATISFIED BY. `AdmittedOnVendorClaim` is a purchase authorisation @@ -88,7 +88,7 @@ type CableOrderRefusalReason // admitted arms into one would erase exactly the distinction the incident turned on. type CableOrderAdmission = AdmittedOnVendorClaim { claimed_mode: LinkMode, citation: ExternalAuthority } - | AdmittedOnObservedCoding { coding: Sff8636LegCoding } + | AdmittedOnObservedCoding { coding: CableLegObservation } | OrderRefused { reason: CableOrderRefusalReason } // The gate. An undeclared coding REFUSES -- that is the loud failure the whole subject exists to @@ -110,16 +110,16 @@ fn admit_cable_order( claimed: claimed, required: requirement.required_mode } } } LegCodingObserved { coding: c } => { - let finding = sff8636_assess_leg_coding(coding: c, requested: requirement.required_mode) + let finding = assess_cable_leg(obs: c, requested: requirement.required_mode) match finding { - CodingAttestsRequestedMode { coding: ok } => AdmittedOnObservedCoding { coding: ok } - CodingAttestsRequestedModeSubjectToFec { coding: ok, fec: f } => + LegAttestsRequestedMode { obs: ok } => AdmittedOnObservedCoding { coding: ok } + LegAttestsRequestedModeSubjectToFec { obs: ok, fec: f } => AdmittedOnObservedCoding { coding: ok } - CodingInsufficientForRequestedMode { requested: r, coding: bad } => + LegInsufficientForRequestedMode { requested: r, obs: bad } => OrderRefused { reason: OrderObservedCodingDoesNotAttestRequiredMode { required: requirement.required_mode, finding: finding } } - CodingComplianceCodeNotUnderstood { code: code } => + LegComplianceCodeNotUnderstood { code: code } => OrderRefused { reason: OrderObservedCodingDoesNotAttestRequiredMode { required: requirement.required_mode, finding: finding } } @@ -140,11 +140,11 @@ fn admit_cable_order( // was in for the weeks the fabric ran at half rate. type CableReceiptReconciliation = ReceiptNotYetObserved { admitted: CableOrderAdmission } - | ReceiptHonoursAdmittedClaim { coding: Sff8636LegCoding } + | ReceiptHonoursAdmittedClaim { coding: CableLegObservation } | ReceiptDivergesFromAdmittedClaim { required: LinkMode claimed_mode: LinkMode - observed_finding: Sff8636CodingFinding + observed_finding: CableLegFinding } | ReceiptReconciliationNotApplicable { admitted: CableOrderAdmission } @@ -163,19 +163,19 @@ fn reconcile_cable_receipt( LegCodingVendorAsserted { asserted_mode: m, citation: c2 } => ReceiptNotYetObserved { admitted: admitted } LegCodingObserved { coding: obs } => { - let finding = sff8636_assess_leg_coding( - coding: obs, requested: requirement.required_mode) + let finding = assess_cable_leg( + obs: obs, requested: requirement.required_mode) match finding { - CodingAttestsRequestedMode { coding: ok } => + LegAttestsRequestedMode { obs: ok } => ReceiptHonoursAdmittedClaim { coding: ok } - CodingAttestsRequestedModeSubjectToFec { coding: ok, fec: f } => + LegAttestsRequestedModeSubjectToFec { obs: ok, fec: f } => ReceiptHonoursAdmittedClaim { coding: ok } - CodingInsufficientForRequestedMode { requested: rq, coding: bad } => + LegInsufficientForRequestedMode { requested: rq, obs: bad } => ReceiptDivergesFromAdmittedClaim { required: requirement.required_mode, claimed_mode: claimed, observed_finding: finding } - CodingComplianceCodeNotUnderstood { code: code } => + LegComplianceCodeNotUnderstood { code: code } => ReceiptDivergesFromAdmittedClaim { required: requirement.required_mode, claimed_mode: claimed, diff --git a/dag/test/claim/cable_leg_coding_witness_test.dag b/dag/test/claim/cable_leg_coding_witness_test.dag index 5e2306a9a1c..728ea3bad34 100644 --- a/dag/test/claim/cable_leg_coding_witness_test.dag +++ b/dag/test/claim/cable_leg_coding_witness_test.dag @@ -10,22 +10,24 @@ import extdeps.ethernet.link_mode { ieee_25gbase_cr, ieee_50gbase_cr2, ieee_100gbase_cr4, ieee_100gbase_cr2, } import extdeps.transceiver.sff_8636 { - Sff8636LegCoding, Sff8636CodingFinding, - CodingAttestsRequestedMode, CodingAttestsRequestedModeSubjectToFec, - CodingInsufficientForRequestedMode, CodingComplianceCodeNotUnderstood, - SecondaryNotObserved, SecondaryObservedUnspecified, SecondaryObservedCode, - ProfileConsistency, ConsistencyUndecidable, - ConsistencySecondaryFieldUnread, ConsistencySecondaryFieldUnspecified, - ConsistencyComplianceCodeNotUnderstood, ConsistencyInterfaceScopeUnestablished, - sff8636_profile_consistency, - sff8636_required_fields_observed, sff8636_interpretation_is_exhaustive, - ComplianceUnderstood, ComplianceCodeUnmodelled, - FecUnconditional, RequiresClause91Fec, - NominalRateEscaped, NominalRateDirect, - sff8636_assess_leg_coding, sff8636_nominal_rate_from_byte140, sff8636_leg_coding, - sff8636_interpret_extended_compliance, + NominalRateUnspecified, NominalRateDirect, NominalRateEscaped, + ComplianceUnderstood, ComplianceUnspecified, ComplianceCodeUnmodelled, + sff8636_nominal_rate_from_byte140, sff8636_interpret_extended_compliance, transceiver_identifier_from_byte, sff8636_encoding_from_byte, } +import product.cable_leg_observation { + CableLegObservation, CableLegFinding, + LegAttestsRequestedMode, LegAttestsRequestedModeSubjectToFec, + LegInsufficientForRequestedMode, LegComplianceCodeNotUnderstood, + SecondaryNotObserved, SecondaryObserved, + ProfileConsistency, ConsistencyUndecidable, + ConsistencyFieldUnread, ConsistencyInterpretationGap, + ConsistencyInterfaceScopeUnestablished, + InterpretationGap, GapComplianceUnspecified, GapComplianceNotUnderstood, + GapEncodingUnspecified, GapEncodingNotUnderstood, + cable_leg_observation, assess_cable_leg, cable_leg_consistency, + cable_leg_unread_fields, cable_leg_interpretation_gaps, +} import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } // GREEN BY EXECUTION FOR THE CABLE-CODING SUBJECT, and the reason it exists rather than being @@ -90,46 +92,46 @@ test fn the_aggregate_is_derived_from_lanes_and_service_rate() -> Bool { // that the WHOLE profile disagrees with the encoding byte, because the unread field may carry the // application the encoding belongs to. An earlier head modelled the unread field as absent and // therefore proved a contradiction out of a gap in its own observation. -data delivered_fs_leg: Sff8636LegCoding = sff8636_leg_coding( +data delivered_fs_leg: CableLegObservation = cable_leg_observation( identifier: transceiver_identifier_from_byte(code: 17), primary_compliance_code: 11, secondary_compliance: SecondaryNotObserved, encoding: sff8636_encoding_from_byte(code: 8), nominal_rate: sff8636_nominal_rate_from_byte140(code: 255)) -fn is_insufficient(f: Sff8636CodingFinding) -> Bool { +fn is_insufficient(f: CableLegFinding) -> Bool { match f { - CodingInsufficientForRequestedMode { requested: r, coding: c } => true - CodingAttestsRequestedMode { coding: c } => false - CodingAttestsRequestedModeSubjectToFec { coding: c, fec: x } => false - CodingComplianceCodeNotUnderstood { code: c } => false + LegInsufficientForRequestedMode { requested: r, obs: c } => true + LegAttestsRequestedMode { obs: c } => false + LegAttestsRequestedModeSubjectToFec { obs: c, fec: x } => false + LegComplianceCodeNotUnderstood { code: c } => false } } -fn attests_outright(f: Sff8636CodingFinding) -> Bool { +fn attests_outright(f: CableLegFinding) -> Bool { match f { - CodingAttestsRequestedMode { coding: c } => true - CodingAttestsRequestedModeSubjectToFec { coding: c, fec: x } => false - CodingInsufficientForRequestedMode { requested: r, coding: c } => false - CodingComplianceCodeNotUnderstood { code: c } => false + LegAttestsRequestedMode { obs: c } => true + LegAttestsRequestedModeSubjectToFec { obs: c, fec: x } => false + LegInsufficientForRequestedMode { requested: r, obs: c } => false + LegComplianceCodeNotUnderstood { code: c } => false } } -fn attests_subject_to_fec(f: Sff8636CodingFinding) -> Bool { +fn attests_subject_to_fec(f: CableLegFinding) -> Bool { match f { - CodingAttestsRequestedModeSubjectToFec { coding: c, fec: x } => true - CodingAttestsRequestedMode { coding: c } => false - CodingInsufficientForRequestedMode { requested: r, coding: c } => false - CodingComplianceCodeNotUnderstood { code: c } => false + LegAttestsRequestedModeSubjectToFec { obs: c, fec: x } => true + LegAttestsRequestedMode { obs: c } => false + LegInsufficientForRequestedMode { requested: r, obs: c } => false + LegComplianceCodeNotUnderstood { code: c } => false } } -fn code_not_understood(f: Sff8636CodingFinding) -> Bool { +fn code_not_understood(f: CableLegFinding) -> Bool { match f { - CodingComplianceCodeNotUnderstood { code: c } => true - CodingAttestsRequestedMode { coding: c } => false - CodingAttestsRequestedModeSubjectToFec { coding: c, fec: x } => false - CodingInsufficientForRequestedMode { requested: r, coding: c } => false + LegComplianceCodeNotUnderstood { code: c } => true + LegAttestsRequestedMode { obs: c } => false + LegAttestsRequestedModeSubjectToFec { obs: c, fec: x } => false + LegInsufficientForRequestedMode { requested: r, obs: c } => false } } @@ -141,15 +143,15 @@ fn code_not_understood(f: Sff8636CodingFinding) -> Bool { // checked. It is insufficiency because byte 116 was never read: with the profile incomplete, the // strong claim is unavailable and the honest one is that nothing OBSERVED attests the request. test fn the_delivered_leg_does_not_attest_the_purchased_mode() -> Bool { - is_insufficient(f: sff8636_assess_leg_coding( - coding: delivered_fs_leg, requested: ieee_100gbase_cr2)) + is_insufficient(f: assess_cable_leg( + obs: delivered_fs_leg, requested: ieee_100gbase_cr2)) } // AND THE SAME LEG DOES ATTEST WHAT IT IS CODED FOR. Without this arm the assertion above would pass // for a decoder that refused everything, which is a wall carrying no information. test fn the_delivered_leg_does_attest_the_mode_it_is_coded_for() -> Bool { - attests_outright(f: sff8636_assess_leg_coding( - coding: delivered_fs_leg, requested: ieee_100gbase_cr4)) + attests_outright(f: assess_cable_leg( + obs: delivered_fs_leg, requested: ieee_100gbase_cr4)) } // THE CLAUSE 91 ENTRY, WHICH THIS MODULE FIRST OMITTED. 0x0B also covers 50GBASE-CR2 subject to @@ -157,7 +159,7 @@ test fn the_delivered_leg_does_attest_the_mode_it_is_coded_for() -> Bool { // must NOT be attested outright, because promoting a conditional entry to unconditional support is // exactly the silent widening the standard's qualification exists to prevent. test fn the_conditional_entry_is_attested_but_not_unconditionally() -> Bool { - let f = sff8636_assess_leg_coding(coding: delivered_fs_leg, requested: ieee_50gbase_cr2) + let f = assess_cable_leg(obs: delivered_fs_leg, requested: ieee_50gbase_cr2) attests_subject_to_fec(f: f) && !attests_outright(f: f) } @@ -167,7 +169,7 @@ test fn the_conditional_entry_is_attested_but_not_unconditionally() -> Bool { // other observation fixed. An earlier head could not express this test at all, because the caller // authored the capability list beside the byte -- so changing the byte changed nothing and the // decoder was decorative. This reds if interpretation ever migrates back out of the byte. -data leg_with_unmodelled_code: Sff8636LegCoding = sff8636_leg_coding( +data leg_with_unmodelled_code: CableLegObservation = cable_leg_observation( identifier: transceiver_identifier_from_byte(code: 17), primary_compliance_code: 254, secondary_compliance: SecondaryNotObserved, @@ -175,17 +177,17 @@ data leg_with_unmodelled_code: Sff8636LegCoding = sff8636_leg_coding( nominal_rate: sff8636_nominal_rate_from_byte140(code: 255)) test fn an_unmodelled_code_is_not_understood_rather_than_attesting_nothing() -> Bool { - code_not_understood(f: sff8636_assess_leg_coding( - coding: leg_with_unmodelled_code, requested: ieee_100gbase_cr2)) + code_not_understood(f: assess_cable_leg( + obs: leg_with_unmodelled_code, requested: ieee_100gbase_cr2)) } // An unread code must not become a proven contradiction. Same bytes, PAM4 encoding, NRZ-only // understood modes -- but one code the decoder cannot read, so no contradiction may be claimed. test fn an_unreadable_code_blocks_the_contradiction_claim() -> Bool { - !is_insufficient(f: sff8636_assess_leg_coding( - coding: leg_with_unmodelled_code, requested: ieee_100gbase_cr4)) - && code_not_understood(f: sff8636_assess_leg_coding( - coding: leg_with_unmodelled_code, requested: ieee_100gbase_cr4)) + !is_insufficient(f: assess_cable_leg( + obs: leg_with_unmodelled_code, requested: ieee_100gbase_cr4)) + && code_not_understood(f: assess_cable_leg( + obs: leg_with_unmodelled_code, requested: ieee_100gbase_cr4)) } // The interpretation is a function of the byte, asserted directly. @@ -206,7 +208,7 @@ test fn an_unknown_byte_interprets_to_unknown_not_to_an_empty_attestation() -> B // ---------------- self-consistency is its own question ---------------- // // THE LAW, MADE MECHANICAL RATHER THAN OBSERVED. Changing the requested mode must not change whether -// a profile contradicts itself. `sff8636_profile_consistency` takes no requested mode, so the law +// a profile contradicts itself. `cable_leg_consistency` takes no requested mode, so the law // holds by construction and this test records WHY the shape is what it is. // // THE ARM THAT IS NOT HERE. There is no operational contradiction verdict, because deciding one @@ -219,21 +221,41 @@ fn consistency_cause_is_unread(c: ProfileConsistency) -> Bool { match c { ConsistencyUndecidable { cause: cz } => match cz { - ConsistencySecondaryFieldUnread => true - ConsistencySecondaryFieldUnspecified => false - ConsistencyComplianceCodeNotUnderstood { code: k } => false + ConsistencyFieldUnread { field: f } => true + ConsistencyInterfaceScopeUnestablished => false + } + } +} + +fn consistency_gap_is_compliance_unspecified(c: ProfileConsistency) -> Bool { + match c { + ConsistencyUndecidable { cause: cz } => + match cz { + ConsistencyInterpretationGap { gap: g } => + match g { + GapComplianceUnspecified { code: k } => true + GapComplianceNotUnderstood { code: k } => false + GapEncodingUnspecified => false + GapEncodingNotUnderstood { code: k } => false + } + ConsistencyFieldUnread { field: f } => false ConsistencyInterfaceScopeUnestablished => false } } } -fn consistency_cause_is_unspecified(c: ProfileConsistency) -> Bool { +fn consistency_gap_is_encoding_unspecified(c: ProfileConsistency) -> Bool { match c { ConsistencyUndecidable { cause: cz } => match cz { - ConsistencySecondaryFieldUnspecified => true - ConsistencySecondaryFieldUnread => false - ConsistencyComplianceCodeNotUnderstood { code: k } => false + ConsistencyInterpretationGap { gap: g } => + match g { + GapEncodingUnspecified => true + GapComplianceUnspecified { code: k } => false + GapComplianceNotUnderstood { code: k } => false + GapEncodingNotUnderstood { code: k } => false + } + ConsistencyFieldUnread { field: f } => false ConsistencyInterfaceScopeUnestablished => false } } @@ -244,9 +266,7 @@ fn consistency_cause_is_scope(c: ProfileConsistency) -> Bool { ConsistencyUndecidable { cause: cz } => match cz { ConsistencyInterfaceScopeUnestablished => true - ConsistencySecondaryFieldUnread => false - ConsistencySecondaryFieldUnspecified => false - ConsistencyComplianceCodeNotUnderstood { code: k } => false + ConsistencyFieldUnread { field: f } => false } } } @@ -254,44 +274,44 @@ fn consistency_cause_is_scope(c: ProfileConsistency) -> Bool { // THE DELIVERED CABLE: byte 116 was never read, so the cause is the unread field and nothing // stronger. This is the arm that used to be a contradiction accusation. test fn the_delivered_leg_consistency_is_undecidable_for_want_of_a_reading() -> Bool { - consistency_cause_is_unread(c: sff8636_profile_consistency(coding: delivered_fs_leg)) + consistency_cause_is_unread(c: cable_leg_consistency(obs: delivered_fs_leg)) } // THE INVERSE CONTROL, and the specific bug it guards. A leg whose byte 116 WAS read and found 00h // must NOT become decidable: 00h is "Unspecified", so reading it improves observation coverage while // leaving interpretation non-exhaustive. An earlier head treated this exact case as establishing // absence and licensed a verdict the bytes do not support. -data secondary_unspecified_leg: Sff8636LegCoding = sff8636_leg_coding( +data secondary_unspecified_leg: CableLegObservation = cable_leg_observation( identifier: transceiver_identifier_from_byte(code: 17), primary_compliance_code: 11, - secondary_compliance: SecondaryObservedUnspecified, + secondary_compliance: SecondaryObserved { code: 0 }, encoding: sff8636_encoding_from_byte(code: 8), nominal_rate: sff8636_nominal_rate_from_byte140(code: 255)) test fn reading_an_unspecified_secondary_does_not_make_the_profile_decidable() -> Bool { - consistency_cause_is_unspecified(c: sff8636_profile_consistency(coding: secondary_unspecified_leg)) + consistency_gap_is_compliance_unspecified(c: cable_leg_consistency(obs: secondary_unspecified_leg)) } // THE TWO AXES ARE SEPARATE, asserted directly: for 00h the field WAS observed and the // interpretation is still not exhaustive. Collapsing these into one boolean is what made the defect // recur, so the split is the thing under test. test fn an_unspecified_secondary_is_observed_but_not_exhaustively_interpreted() -> Bool { - sff8636_required_fields_observed(coding: secondary_unspecified_leg) - && !sff8636_interpretation_is_exhaustive(coding: secondary_unspecified_leg) - && !sff8636_required_fields_observed(coding: delivered_fs_leg) + length(cable_leg_unread_fields(obs: secondary_unspecified_leg)) == 0 + && length(cable_leg_interpretation_gaps(obs: secondary_unspecified_leg)) > 0 + && length(cable_leg_unread_fields(obs: delivered_fs_leg)) > 0 } // A FULLY READ, FULLY UNDERSTOOD PROFILE still cannot be decided -- and the cause names the frontier // rather than going quiet. This is what stops the retired arm from reading as "nothing left to do". -data fully_understood_leg: Sff8636LegCoding = sff8636_leg_coding( +data fully_understood_leg: CableLegObservation = cable_leg_observation( identifier: transceiver_identifier_from_byte(code: 17), primary_compliance_code: 11, - secondary_compliance: SecondaryObservedCode { code: 64 }, + secondary_compliance: SecondaryObserved { code: 64 }, encoding: sff8636_encoding_from_byte(code: 8), nominal_rate: sff8636_nominal_rate_from_byte140(code: 255)) test fn a_fully_read_profile_is_undecidable_only_for_interface_scope() -> Bool { - consistency_cause_is_scope(c: sff8636_profile_consistency(coding: fully_understood_leg)) + consistency_cause_is_scope(c: cable_leg_consistency(obs: fully_understood_leg)) } // AND THE 0x40 ROW EARNS ITS CITATION. SFF-8024 Rev 4.14 Table 4-4 row 40h attests 50GBASE-CR, @@ -299,10 +319,40 @@ test fn a_fully_read_profile_is_undecidable_only_for_interface_scope() -> Bool { // rail needs -- which the delivered leg, carrying only 0x0B, does not. This is also the positive // control that retires the placeholder code 0 the first head used. test fn the_secondary_code_0x40_attests_the_mode_the_primary_does_not() -> Bool { - attests_outright(f: sff8636_assess_leg_coding( - coding: fully_understood_leg, requested: ieee_100gbase_cr2)) - && is_insufficient(f: sff8636_assess_leg_coding( - coding: delivered_fs_leg, requested: ieee_100gbase_cr2)) + attests_outright(f: assess_cable_leg( + obs: fully_understood_leg, requested: ieee_100gbase_cr2)) + && is_insufficient(f: assess_cable_leg( + obs: delivered_fs_leg, requested: ieee_100gbase_cr2)) +} + +// R2's DEFECT, MADE EXECUTABLE. A profile whose compliance codes are all understood but whose +// ENCODING byte is unspecified must not reach the interface-scope frontier: reading the +// transmitter-technology field would not make such an observation decidable, so reporting the +// frontier there is a false diagnosis. The gap names the field that actually defeated the decoder. +data encoding_unspecified_leg: CableLegObservation = cable_leg_observation( + identifier: transceiver_identifier_from_byte(code: 17), + primary_compliance_code: 11, + secondary_compliance: SecondaryObserved { code: 64 }, + encoding: sff8636_encoding_from_byte(code: 0), + nominal_rate: sff8636_nominal_rate_from_byte140(code: 255)) + +test fn an_unspecified_encoding_is_named_rather_than_blamed_on_interface_scope() -> Bool { + consistency_gap_is_encoding_unspecified(c: cable_leg_consistency( + obs: encoding_unspecified_leg)) + && !consistency_cause_is_scope(c: cable_leg_consistency( + obs: encoding_unspecified_leg)) +} + +// R3: A ZERO BAUD BYTE IS A SENTINEL, NOT A MEASUREMENT. SFF-8636 gives 0 the meaning "not +// specified; determine from module technology". Multiplying it out to 0 baud is a fabricated +// measurement wearing a unit, and a consumer comparing it against a required rate would read the +// module as infinitely slow rather than as silent. +test fn a_zero_nominal_rate_byte_is_unspecified_not_zero_baud() -> Bool { + match sff8636_nominal_rate_from_byte140(code: 0) { + NominalRateUnspecified => true + NominalRateDirect { rate: r } => false + NominalRateEscaped => false + } } // The escape is not a measurement. diff --git a/dag/test/claim/cable_order_admission_witness_test.dag b/dag/test/claim/cable_order_admission_witness_test.dag index d36eab4f3a0..28e69c954b5 100644 --- a/dag/test/claim/cable_order_admission_witness_test.dag +++ b/dag/test/claim/cable_order_admission_witness_test.dag @@ -3,10 +3,12 @@ module test.claim.cable_order_admission_witness import std.types { Bool, NonEmptyStr } import extdeps.ethernet.link_mode { ieee_100gbase_cr2, ieee_100gbase_cr4 } import extdeps.transceiver.sff_8636 { - Sff8636LegCoding, - SecondaryNotObserved, sff8636_leg_coding, sff8636_nominal_rate_from_byte140, + sff8636_nominal_rate_from_byte140, transceiver_identifier_from_byte, sff8636_encoding_from_byte, } +import product.cable_leg_observation { + CableLegObservation, SecondaryNotObserved, cable_leg_observation, +} import extdeps.external_authority { ExternalAuthority } import extdeps.uri { Uri, Https } import product.cable_order_admission { @@ -77,7 +79,7 @@ test fn a_claim_for_a_different_mode_refuses() -> Bool { // ---------------- gate 2: receipt reconciliation ---------------- // The delivered leg, as read. Byte 116 unread, primary 0x0B, PAM4 encoding, escape rate byte. -data delivered_leg: Sff8636LegCoding = sff8636_leg_coding( +data delivered_leg: CableLegObservation = cable_leg_observation( identifier: transceiver_identifier_from_byte(code: 17), primary_compliance_code: 11, secondary_compliance: SecondaryNotObserved, @@ -128,7 +130,7 @@ test fn an_unread_delivery_does_not_reconcile_as_matching() -> Bool { // THE POSITIVE CONTROL. A leg coded for the required mode reconciles as honouring the claim and // needs no remedy -- without this arm every assertion above would pass for a gate that refused // everything, which is a wall carrying no information. -data correctly_coded_leg: Sff8636LegCoding = sff8636_leg_coding( +data correctly_coded_leg: CableLegObservation = cable_leg_observation( identifier: transceiver_identifier_from_byte(code: 17), primary_compliance_code: 11, secondary_compliance: SecondaryNotObserved, From f3f6b1909b951dda81104f8ec06f6d9299510cf2 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 6 Sep 2026 17:18:02 +0000 Subject: [PATCH 09/11] wip: field census + exhaustive matches --- dag/gunbc/product/cable_leg_observation.dag | 10 +++++++++- dag/test/claim/cable_leg_coding_witness_test.dag | 3 +++ 2 files changed, 12 insertions(+), 1 deletion(-) diff --git a/dag/gunbc/product/cable_leg_observation.dag b/dag/gunbc/product/cable_leg_observation.dag index f5c3e902742..daac1349ccb 100644 --- a/dag/gunbc/product/cable_leg_observation.dag +++ b/dag/gunbc/product/cable_leg_observation.dag @@ -67,7 +67,15 @@ fn cable_leg_observation( // be routed through a canonical accessor. The coverage census is a fold producing the list of // UNREAD fields, and every coverage question is asked of that one list -- so a new field is one row // here rather than a new predicate at every call site. -type CableLegField = SecondaryComplianceField +// THE FIELDS THIS OBSERVATION CAN CARRY, named so the coverage census reports WHICH one is missing +// rather than a bare count. Only the secondary compliance byte is optional in the carrier today -- +// the others are required to construct an observation at all -- so the census reports only that one +// now, and a field that becomes optional later is a row here rather than a new predicate. +type CableLegField + = SecondaryComplianceField + | PrimaryComplianceField + | EncodingField + | NominalRateField fn cable_leg_unread_fields(obs: CableLegObservation) -> List { match obs.secondary_compliance { diff --git a/dag/test/claim/cable_leg_coding_witness_test.dag b/dag/test/claim/cable_leg_coding_witness_test.dag index 728ea3bad34..714ad5c954c 100644 --- a/dag/test/claim/cable_leg_coding_witness_test.dag +++ b/dag/test/claim/cable_leg_coding_witness_test.dag @@ -194,6 +194,7 @@ test fn an_unreadable_code_blocks_the_contradiction_claim() -> Bool { test fn the_interpretation_is_derived_from_the_byte() -> Bool { match sff8636_interpret_extended_compliance(code: 11) { ComplianceUnderstood { code: c, modes: ms } => c == 11 && count(ms) == 3 + ComplianceUnspecified { code: c } => false ComplianceCodeUnmodelled { code: c } => false } } @@ -201,6 +202,7 @@ test fn the_interpretation_is_derived_from_the_byte() -> Bool { test fn an_unknown_byte_interprets_to_unknown_not_to_an_empty_attestation() -> Bool { match sff8636_interpret_extended_compliance(code: 254) { ComplianceCodeUnmodelled { code: c } => c == 254 + ComplianceUnspecified { code: c } => false ComplianceUnderstood { code: c, modes: ms } => false } } @@ -222,6 +224,7 @@ fn consistency_cause_is_unread(c: ProfileConsistency) -> Bool { ConsistencyUndecidable { cause: cz } => match cz { ConsistencyFieldUnread { field: f } => true + ConsistencyInterpretationGap { gap: g } => false ConsistencyInterfaceScopeUnestablished => false } } From dfbf638614a50b46d119f5be3e637b60ca486767 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 6 Sep 2026 17:29:44 +0000 Subject: [PATCH 10/11] wip: remaining exhaustive arms --- dag/test/claim/cable_leg_coding_witness_test.dag | 3 +++ 1 file changed, 3 insertions(+) diff --git a/dag/test/claim/cable_leg_coding_witness_test.dag b/dag/test/claim/cable_leg_coding_witness_test.dag index 714ad5c954c..e46944ac4e0 100644 --- a/dag/test/claim/cable_leg_coding_witness_test.dag +++ b/dag/test/claim/cable_leg_coding_witness_test.dag @@ -270,6 +270,7 @@ fn consistency_cause_is_scope(c: ProfileConsistency) -> Bool { match cz { ConsistencyInterfaceScopeUnestablished => true ConsistencyFieldUnread { field: f } => false + ConsistencyInterpretationGap { gap: g } => false } } } @@ -363,6 +364,7 @@ test fn the_escape_value_is_not_recorded_as_a_rate() -> Bool { match sff8636_nominal_rate_from_byte140(code: 255) { NominalRateEscaped => true NominalRateDirect { rate: r } => false + NominalRateUnspecified => false } } @@ -370,5 +372,6 @@ test fn an_ordinary_byte140_is_read_as_a_symbol_rate() -> Bool { match sff8636_nominal_rate_from_byte140(code: 254) { NominalRateDirect { rate: r } => symbol_rate_count(r: r) == 25400000000 NominalRateEscaped => false + NominalRateUnspecified => false } } From 37c96038ab3a7e86346b1804bf8dc164cb72b655 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 6 Sep 2026 18:21:42 +0000 Subject: [PATCH 11/11] Repoint the SFF-8636 model scope off the moved observation carrier; admit the four rehomed bindings MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit cursor/composer-2.5 (review 61439) found that `extdeps_model_scope` still names `Sff8636LegCoding` — the observation carrier this branch moved to `product.cable_leg_observation`. The declarations phase of required CI agrees: CITED-DECLARATION-ABSENT, one finding, and it is the same symbol. Repointed the scope subject at `ComplianceInterpretation`, a byte-meaning declaration this module still declares, and deleted the orphaned annotation above it: that prose describes the observation carrier and already lives beside `SecondaryComplianceObservation` in the product module, so keeping a copy here was a §4c annotation about a type no longer in the file. The namespace wave-admission phase blocked on four `TargetChanged` bindings — the fixture constructors that spell `SecondaryNotObserved`, whose declarer moved between modules. Rostered with the layer-split reasoning and their own dissolution trigger. Touching that roster makes its consumed rows due, so the thirty gunbc#10639 rows are deleted here, adjudicated by the join they asked for rather than by their sentence: 8769167dd05 is an ancestor of this base and main declares `SparkServingProbeCapture` in `gunbc.spark.training_ready`, so no run can produce those deltas. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01AigrH3JpxgSJBmqHMBAr6W --- dag/extdeps/transceiver/sff_8636.dag | 9 +- src/v1/stage0/src/namespace_wave_admission.rs | 355 +++--------------- 2 files changed, 51 insertions(+), 313 deletions(-) diff --git a/dag/extdeps/transceiver/sff_8636.dag b/dag/extdeps/transceiver/sff_8636.dag index 44bd2878563..c8724f3fac5 100644 --- a/dag/extdeps/transceiver/sff_8636.dag +++ b/dag/extdeps/transceiver/sff_8636.dag @@ -216,18 +216,11 @@ fn sff8636_interpret_extended_compliance(code: Nat) -> ComplianceInterpretation } } -// ================= THE OBSERVED SECONDARY FIELD ================= -// -// AN UNREAD FIELD IS NOT AN ABSENT ONE, and the distinction decides a verdict. Contradiction is a -// claim about a COMPLETE profile: it says every application this module declares disagrees with its -// encoding byte. That claim cannot be made while byte 116 has not been read, because the unread -// field may carry the very application the encoding belongs to. The earlier head used `Absent` for -// both and therefore proved contradiction from a gap in its own observation. data extdeps_model_scope: ExternalModelScope = ExternalModelScope { subject: ExternalSubjectRef { declaration: DeclarationRef { module_path: "extdeps.transceiver.sff_8636", - decl_name: "Sff8636LegCoding", + decl_name: "ComplianceInterpretation", field: WholeDeclaration } }, diff --git a/src/v1/stage0/src/namespace_wave_admission.rs b/src/v1/stage0/src/namespace_wave_admission.rs index 64bd684ebb5..e86dfb6078a 100644 --- a/src/v1/stage0/src/namespace_wave_admission.rs +++ b/src/v1/stage0/src/namespace_wave_admission.rs @@ -1531,332 +1531,77 @@ pub struct TransitionAdmission { /// entry above records happened once and is not re-recorded here: this branch had deleted the same /// eight rows independently, the two deletions agree, and main's entry is the one authority. /// -/// THE PROBE CAPTURE MOVES TO THE DECODER THAT READS IT (2026-09-06, gunbc#10639). No ordinal is -/// claimed, for the reason the entries above give. The Ollama-era Spark serving tree is deleted at -/// the root in that change, and `gunbc.spark.serving_terminal_health` went with it. One type it -/// declared, `SparkServingProbeCapture` with its three arms `ProbeNeverRan`, `ProbeFailed` and -/// `ProbeAnswered`, had a consumer outside the tree: `gunbc.spark.training_ready`, which decodes -/// probe captures into retirement observations and pool readings. The type is rehomed there. It -/// is not a serving fact; it is the shape of a probe result, and the decoder was its only reader. -/// -/// THIRTY BINDINGS ACROSS TWO MODULES resolve to the new declarer, which is `TargetChanged` and is -/// not auto-admitted: nine in `gunbc.spark.training_ready` (the three decoders that match on the -/// capture) and twenty-one in `test.claim.spark.spark_training_ready_witness_test` (the fixture -/// constructors and the claims that read them). Every spelling is identical on both sides; only -/// the declaring module differs, which is the membership motion this roster exists to adjudicate. +/// THE gunbc#10639 ROWS DISSOLVED HERE (2026-09-06), BY THEIR OWN TRIGGER AND ON THE ROSTER TOUCH +/// THEY NAMED. gunbc#10639 merged as 8769167dd05, which is an ancestor of this change's base. +/// Adjudicated by the join those rows asked for rather than by their sentence: on main, +/// `gunbc.spark.training_ready` declares `SparkServingProbeCapture` itself, so base and head bind +/// every one of the thirty spellings to the same declaration, no run can produce the delta, and +/// all thirty report CONSUMED -- due on this touch, which is this change. +/// +/// THE OBSERVATION CARRIER MOVES OUT OF THE SPEC MODULE (2026-09-06, gunbc#10671). No ordinal is +/// claimed, for the reason the entries above give. `extdeps.transceiver.sff_8636` models what +/// SFF-8636 bytes MEAN. It had also come to declare what THIS REPOSITORY READ off a delivered +/// cable, which DESIGN section 3 refuses in terms: "Observations produced by this repository are +/// receipts in the observing product or workflow layer, not facts owned by the observed upstream." +/// The observation carrier and its unread/observed distinction are rehomed to +/// `product.cable_leg_observation`, whose subject is a leg this repository holds. +/// +/// FOUR BINDINGS ACROSS TWO TEST MODULES resolve to the new declarer, which is `TargetChanged` and +/// is not auto-admitted: the four fixture constructors that spell `SecondaryNotObserved`. The +/// spelling is identical on both sides; only the declaring module differs, which is the membership +/// motion this roster exists to adjudicate. The three membership additions the same run reported +/// are `ExplicitlyEvaluatedZeroDelta` and the one removal is `SameDeclarationIdentityRebind`, so +/// they are auto-admitted and are deliberately not rostered here. /// /// ONE CHANGE CLASS. Nothing is requalified; every spelling is imported under the leaf it always -/// had, and the declaration behind it moved. The twenty-one `NewUnresolvedness` deltas the same -/// run reported are not admitted here: they came from `v2.test.claim.spark_observation_scope`, -/// whose whole subject was a deleted module, and that test is deleted in the same change, so no -/// run against its head can produce them. -/// -/// TRIGGER, AND IT IS THESE ROWS' OWN DEATH: they go when gunbc#10639 merges. Main then declares -/// the capture in `gunbc.spark.training_ready`, base and head bind each spelling identically, and -/// all thirty report CONSUMED, coming due on this roster's next touch. Adjudicate that deletion by -/// joining each row against main's tree on its own tuple, not by trusting this sentence. -const PROBE_CAPTURE_REHOME_LABEL: &str = - "gunbc#10639 serving-tree cut: SparkServingProbeCapture and its arms move from the deleted \ - gunbc.spark.serving_terminal_health to their only reader, gunbc.spark.training_ready"; +/// had, and the declaration behind it moved. +/// +/// TRIGGER, AND IT IS THESE ROWS' OWN DEATH: they go when gunbc#10671 merges. Main then declares +/// the carrier in `product.cable_leg_observation`, base and head bind each spelling identically, +/// and all four report CONSUMED, coming due on this roster's next touch. Adjudicate that deletion +/// by joining each row against main's tree on its own tuple, not by trusting this sentence. +const LEG_OBSERVATION_REHOME_LABEL: &str = + "gunbc#10671 transceiver layer split: the cable-leg observation carrier moves from the \ + SFF-8636 byte-meaning module extdeps.transceiver.sff_8636 to product.cable_leg_observation"; pub const NAMESPACE_TRANSITION_ADMISSIONS: &[TransitionAdmission] = &[ TransitionAdmission { - label: PROBE_CAPTURE_REHOME_LABEL, - subject: AdmissionSubject::Binding { - module: "gunbc.spark.training_ready", - in_declaration: "spark_serving_absence_from_probe", - spelling: "ProbeAnswered", - target: "gunbc.spark.training_ready", - }, - disposition: NamespaceDeltaDisposition::TargetChanged, - }, - TransitionAdmission { - label: PROBE_CAPTURE_REHOME_LABEL, - subject: AdmissionSubject::Binding { - module: "gunbc.spark.training_ready", - in_declaration: "spark_serving_absence_from_probe", - spelling: "ProbeFailed", - target: "gunbc.spark.training_ready", - }, - disposition: NamespaceDeltaDisposition::TargetChanged, - }, - TransitionAdmission { - label: PROBE_CAPTURE_REHOME_LABEL, - subject: AdmissionSubject::Binding { - module: "gunbc.spark.training_ready", - in_declaration: "spark_serving_absence_from_probe", - spelling: "ProbeNeverRan", - target: "gunbc.spark.training_ready", - }, - disposition: NamespaceDeltaDisposition::TargetChanged, - }, - TransitionAdmission { - label: PROBE_CAPTURE_REHOME_LABEL, - subject: AdmissionSubject::Binding { - module: "gunbc.spark.training_ready", - in_declaration: "spark_serving_absence_from_probe", - spelling: "SparkServingProbeCapture", - target: "gunbc.spark.training_ready", - }, - disposition: NamespaceDeltaDisposition::TargetChanged, - }, - TransitionAdmission { - label: PROBE_CAPTURE_REHOME_LABEL, - subject: AdmissionSubject::Binding { - module: "gunbc.spark.training_ready", - in_declaration: "spark_serving_retirement_observation_from_probes", - spelling: "SparkServingProbeCapture", - target: "gunbc.spark.training_ready", - }, - disposition: NamespaceDeltaDisposition::TargetChanged, - }, - TransitionAdmission { - label: PROBE_CAPTURE_REHOME_LABEL, - subject: AdmissionSubject::Binding { - module: "gunbc.spark.training_ready", - in_declaration: "spark_unified_pool_observation_from_capture", - spelling: "ProbeAnswered", - target: "gunbc.spark.training_ready", - }, - disposition: NamespaceDeltaDisposition::TargetChanged, - }, - TransitionAdmission { - label: PROBE_CAPTURE_REHOME_LABEL, - subject: AdmissionSubject::Binding { - module: "gunbc.spark.training_ready", - in_declaration: "spark_unified_pool_observation_from_capture", - spelling: "ProbeFailed", - target: "gunbc.spark.training_ready", - }, - disposition: NamespaceDeltaDisposition::TargetChanged, - }, - TransitionAdmission { - label: PROBE_CAPTURE_REHOME_LABEL, - subject: AdmissionSubject::Binding { - module: "gunbc.spark.training_ready", - in_declaration: "spark_unified_pool_observation_from_capture", - spelling: "ProbeNeverRan", - target: "gunbc.spark.training_ready", - }, - disposition: NamespaceDeltaDisposition::TargetChanged, - }, - TransitionAdmission { - label: PROBE_CAPTURE_REHOME_LABEL, - subject: AdmissionSubject::Binding { - module: "gunbc.spark.training_ready", - in_declaration: "spark_unified_pool_observation_from_capture", - spelling: "SparkServingProbeCapture", - target: "gunbc.spark.training_ready", - }, - disposition: NamespaceDeltaDisposition::TargetChanged, - }, - TransitionAdmission { - label: PROBE_CAPTURE_REHOME_LABEL, - subject: AdmissionSubject::Binding { - module: "test.claim.spark.spark_training_ready_witness_test", - in_declaration: "w_a_capture_whose_body_is_not_a_count_is_refused", - spelling: "ProbeAnswered", - target: "gunbc.spark.training_ready", - }, - disposition: NamespaceDeltaDisposition::TargetChanged, - }, - TransitionAdmission { - label: PROBE_CAPTURE_REHOME_LABEL, - subject: AdmissionSubject::Binding { - module: "test.claim.spark.spark_training_ready_witness_test", - in_declaration: "w_a_connect_failure_never_establishes_endpoint_absence", - spelling: "ProbeFailed", - target: "gunbc.spark.training_ready", - }, - disposition: NamespaceDeltaDisposition::TargetChanged, - }, - TransitionAdmission { - label: PROBE_CAPTURE_REHOME_LABEL, - subject: AdmissionSubject::Binding { - module: "test.claim.spark.spark_training_ready_witness_test", - in_declaration: "w_a_pool_number_without_a_read_is_refused", - spelling: "ProbeNeverRan", - target: "gunbc.spark.training_ready", - }, - disposition: NamespaceDeltaDisposition::TargetChanged, - }, - TransitionAdmission { - label: PROBE_CAPTURE_REHOME_LABEL, - subject: AdmissionSubject::Binding { - module: "test.claim.spark.spark_training_ready_witness_test", - in_declaration: "w_a_pool_over_an_unestablished_retirement_is_refused", - spelling: "ProbeAnswered", - target: "gunbc.spark.training_ready", - }, - disposition: NamespaceDeltaDisposition::TargetChanged, - }, - TransitionAdmission { - label: PROBE_CAPTURE_REHOME_LABEL, - subject: AdmissionSubject::Binding { - module: "test.claim.spark.spark_training_ready_witness_test", - in_declaration: "w_a_still_serving_endpoint_refuses", - spelling: "ProbeAnswered", - target: "gunbc.spark.training_ready", - }, - disposition: NamespaceDeltaDisposition::TargetChanged, - }, - TransitionAdmission { - label: PROBE_CAPTURE_REHOME_LABEL, - subject: AdmissionSubject::Binding { - module: "test.claim.spark.spark_training_ready_witness_test", - in_declaration: "w_an_enumeration_that_never_ran_establishes_no_endpoint_absence", - spelling: "ProbeNeverRan", - target: "gunbc.spark.training_ready", - }, - disposition: NamespaceDeltaDisposition::TargetChanged, - }, - TransitionAdmission { - label: PROBE_CAPTURE_REHOME_LABEL, - subject: AdmissionSubject::Binding { - module: "test.claim.spark.spark_training_ready_witness_test", - in_declaration: "w_endpoint_absence", - spelling: "SparkServingProbeCapture", - target: "gunbc.spark.training_ready", - }, - disposition: NamespaceDeltaDisposition::TargetChanged, - }, - TransitionAdmission { - label: PROBE_CAPTURE_REHOME_LABEL, - subject: AdmissionSubject::Binding { - module: "test.claim.spark.spark_training_ready_witness_test", - in_declaration: "w_endpoint_absent_capture", - spelling: "ProbeAnswered", - target: "gunbc.spark.training_ready", - }, - disposition: NamespaceDeltaDisposition::TargetChanged, - }, - TransitionAdmission { - label: PROBE_CAPTURE_REHOME_LABEL, - subject: AdmissionSubject::Binding { - module: "test.claim.spark.spark_training_ready_witness_test", - in_declaration: "w_endpoint_absent_capture", - spelling: "SparkServingProbeCapture", - target: "gunbc.spark.training_ready", - }, - disposition: NamespaceDeltaDisposition::TargetChanged, - }, - TransitionAdmission { - label: PROBE_CAPTURE_REHOME_LABEL, - subject: AdmissionSubject::Binding { - module: "test.claim.spark.spark_training_ready_witness_test", - in_declaration: "w_only_a_completed_empty_enumeration_establishes_endpoint_absence", - spelling: "ProbeAnswered", - target: "gunbc.spark.training_ready", - }, - disposition: NamespaceDeltaDisposition::TargetChanged, - }, - TransitionAdmission { - label: PROBE_CAPTURE_REHOME_LABEL, - subject: AdmissionSubject::Binding { - module: "test.claim.spark.spark_training_ready_witness_test", - in_declaration: "w_pool_or_refused", - spelling: "ProbeAnswered", - target: "gunbc.spark.training_ready", - }, - disposition: NamespaceDeltaDisposition::TargetChanged, - }, - TransitionAdmission { - label: PROBE_CAPTURE_REHOME_LABEL, - subject: AdmissionSubject::Binding { - module: "test.claim.spark.spark_training_ready_witness_test", - in_declaration: "w_process_absent_capture", - spelling: "ProbeFailed", - target: "gunbc.spark.training_ready", - }, - disposition: NamespaceDeltaDisposition::TargetChanged, - }, - TransitionAdmission { - label: PROBE_CAPTURE_REHOME_LABEL, - subject: AdmissionSubject::Binding { - module: "test.claim.spark.spark_training_ready_witness_test", - in_declaration: "w_process_absent_capture", - spelling: "SparkServingProbeCapture", - target: "gunbc.spark.training_ready", - }, - disposition: NamespaceDeltaDisposition::TargetChanged, - }, - TransitionAdmission { - label: PROBE_CAPTURE_REHOME_LABEL, - subject: AdmissionSubject::Binding { - module: "test.claim.spark.spark_training_ready_witness_test", - in_declaration: "w_silent_capture", - spelling: "ProbeNeverRan", - target: "gunbc.spark.training_ready", - }, - disposition: NamespaceDeltaDisposition::TargetChanged, - }, - TransitionAdmission { - label: PROBE_CAPTURE_REHOME_LABEL, - subject: AdmissionSubject::Binding { - module: "test.claim.spark.spark_training_ready_witness_test", - in_declaration: "w_silent_capture", - spelling: "SparkServingProbeCapture", - target: "gunbc.spark.training_ready", - }, - disposition: NamespaceDeltaDisposition::TargetChanged, - }, - TransitionAdmission { - label: PROBE_CAPTURE_REHOME_LABEL, - subject: AdmissionSubject::Binding { - module: "test.claim.spark.spark_training_ready_witness_test", - in_declaration: "w_the_refusal_carries_a_cause_rather_than_a_bare_negative", - spelling: "ProbeFailed", - target: "gunbc.spark.training_ready", - }, - disposition: NamespaceDeltaDisposition::TargetChanged, - }, - TransitionAdmission { - label: PROBE_CAPTURE_REHOME_LABEL, - subject: AdmissionSubject::Binding { - module: "test.claim.spark.spark_training_ready_witness_test", - in_declaration: "w_the_unit_axis_establishes_absence_by_answering_not_by_failing", - spelling: "ProbeAnswered", - target: "gunbc.spark.training_ready", - }, - disposition: NamespaceDeltaDisposition::TargetChanged, - }, - TransitionAdmission { - label: PROBE_CAPTURE_REHOME_LABEL, + label: LEG_OBSERVATION_REHOME_LABEL, subject: AdmissionSubject::Binding { - module: "test.claim.spark.spark_training_ready_witness_test", - in_declaration: "w_the_unit_axis_establishes_absence_by_answering_not_by_failing", - spelling: "ProbeFailed", - target: "gunbc.spark.training_ready", + module: "test.claim.cable_leg_coding_witness", + in_declaration: "delivered_fs_leg", + spelling: "SecondaryNotObserved", + target: "product.cable_leg_observation", }, disposition: NamespaceDeltaDisposition::TargetChanged, }, TransitionAdmission { - label: PROBE_CAPTURE_REHOME_LABEL, + label: LEG_OBSERVATION_REHOME_LABEL, subject: AdmissionSubject::Binding { - module: "test.claim.spark.spark_training_ready_witness_test", - in_declaration: "w_unit_absence", - spelling: "SparkServingProbeCapture", - target: "gunbc.spark.training_ready", + module: "test.claim.cable_leg_coding_witness", + in_declaration: "leg_with_unmodelled_code", + spelling: "SecondaryNotObserved", + target: "product.cable_leg_observation", }, disposition: NamespaceDeltaDisposition::TargetChanged, }, TransitionAdmission { - label: PROBE_CAPTURE_REHOME_LABEL, + label: LEG_OBSERVATION_REHOME_LABEL, subject: AdmissionSubject::Binding { - module: "test.claim.spark.spark_training_ready_witness_test", - in_declaration: "w_unit_absent_capture", - spelling: "ProbeAnswered", - target: "gunbc.spark.training_ready", + module: "test.claim.cable_order_admission_witness", + in_declaration: "correctly_coded_leg", + spelling: "SecondaryNotObserved", + target: "product.cable_leg_observation", }, disposition: NamespaceDeltaDisposition::TargetChanged, }, TransitionAdmission { - label: PROBE_CAPTURE_REHOME_LABEL, + label: LEG_OBSERVATION_REHOME_LABEL, subject: AdmissionSubject::Binding { - module: "test.claim.spark.spark_training_ready_witness_test", - in_declaration: "w_unit_absent_capture", - spelling: "SparkServingProbeCapture", - target: "gunbc.spark.training_ready", + module: "test.claim.cable_order_admission_witness", + in_declaration: "delivered_leg", + spelling: "SecondaryNotObserved", + target: "product.cable_leg_observation", }, disposition: NamespaceDeltaDisposition::TargetChanged, },