diff --git a/dag/extdeps/transceiver/sff_8636.dag b/dag/extdeps/transceiver/sff_8636.dag index 905a22aa2cc..c8724f3fac5 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 @@ -25,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 @@ -120,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) } } @@ -159,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 @@ -168,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: [ @@ -180,154 +202,25 @@ 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 } } } -// ================= 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_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, - } -} - -// 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 - = 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 => - [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 } => [] - }) -} - -// 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(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 } - } - } - } - } - } - } -} - 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/dag/gunbc/product/cable_leg_observation.dag b/dag/gunbc/product/cable_leg_observation.dag new file mode 100644 index 00000000000..daac1349ccb --- /dev/null +++ b/dag/gunbc/product/cable_leg_observation.dag @@ -0,0 +1,215 @@ +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. +// 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 { + 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 7f77c4f5a44..4562dfa20eb 100644 --- a/dag/gunbc/product/cable_order_admission.dag +++ b/dag/gunbc/product/cable_order_admission.dag @@ -3,12 +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, CodingContradictsEncoding, - CodingComplianceCodeNotUnderstood, - sff8636_assess_leg_coding, +import product.cable_leg_observation { + CableLegObservation, CableLegFinding, + LegAttestsRequestedMode, LegAttestsRequestedModeSubjectToFec, + LegInsufficientForRequestedMode, LegComplianceCodeNotUnderstood, + assess_cable_leg, } import extdeps.external_authority { ExternalAuthority } @@ -51,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 ================= // @@ -80,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 @@ -89,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 @@ -111,20 +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 } } - CodingContradictsEncoding { encoding_modulation: m, attested_mode: a } => - OrderRefused { - reason: OrderObservedCodingDoesNotAttestRequiredMode { - required: requirement.required_mode, finding: finding } } - CodingComplianceCodeNotUnderstood { code: code } => + LegComplianceCodeNotUnderstood { code: code } => OrderRefused { reason: OrderObservedCodingDoesNotAttestRequiredMode { required: requirement.required_mode, finding: finding } } @@ -145,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 } @@ -168,24 +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 } => - ReceiptDivergesFromAdmittedClaim { - required: requirement.required_mode, - claimed_mode: claimed, - observed_finding: finding } - CodingContradictsEncoding { encoding_modulation: em, attested_mode: am } => + 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 027feb8f9df..e46944ac4e0 100644 --- a/dag/test/claim/cable_leg_coding_witness_test.dag +++ b/dag/test/claim/cable_leg_coding_witness_test.dag @@ -10,18 +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, CodingContradictsEncoding, - CodingComplianceCodeNotUnderstood, - SecondaryNotObserved, SecondaryObservedEmpty, SecondaryObservedCode, - 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 @@ -86,50 +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 - CodingContradictsEncoding { encoding_modulation: m, attested_mode: a } => 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 - CodingContradictsEncoding { encoding_modulation: m, attested_mode: a } => 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 - CodingContradictsEncoding { encoding_modulation: m, attested_mode: a } => 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 - CodingContradictsEncoding { encoding_modulation: m, attested_mode: a } => 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,23 +177,24 @@ 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. 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 } } @@ -199,40 +202,161 @@ 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 } } -// ---------------- 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. `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 +// 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 { + ConsistencyFieldUnread { field: f } => true + ConsistencyInterpretationGap { gap: g } => false + 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_gap_is_encoding_unspecified(c: ProfileConsistency) -> Bool { + match c { + ConsistencyUndecidable { cause: cz } => + match cz { + 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 + } + } +} + +fn consistency_cause_is_scope(c: ProfileConsistency) -> Bool { + match c { + ConsistencyUndecidable { cause: cz } => + match cz { + ConsistencyInterfaceScopeUnestablished => true + ConsistencyFieldUnread { field: f } => false + ConsistencyInterpretationGap { gap: g } => 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( +// 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: 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: CableLegObservation = cable_leg_observation( identifier: transceiver_identifier_from_byte(code: 17), primary_compliance_code: 11, - secondary_compliance: SecondaryObservedEmpty, + secondary_compliance: SecondaryObserved { code: 0 }, 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_gap_is_compliance_unspecified(c: cable_leg_consistency(obs: secondary_unspecified_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)) - && is_insufficient(f: sff8636_assess_leg_coding( - coding: delivered_fs_leg, requested: ieee_100gbase_cr2)) +// 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 { + 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: 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: 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: 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, +// 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: 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. @@ -240,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 } } @@ -247,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 } } 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, 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, },