diff --git a/dag/extdeps/mikrotik/crs812.dag b/dag/extdeps/mikrotik/crs812.dag index be8ba91c850..f56575b0160 100644 --- a/dag/extdeps/mikrotik/crs812.dag +++ b/dag/extdeps/mikrotik/crs812.dag @@ -115,3 +115,66 @@ data crs812_rest_neighbor_path: NonEmptyStr = "/rest/ip/neighbor" as NonEmptyStr data crs812_rest_discovery_settings_path: NonEmptyStr = "/rest/ip/neighbor/discovery-settings" as NonEmptyStr data crs812_rest_identity_path: NonEmptyStr = "/rest/system/identity" as NonEmptyStr data crs812_rest_monitor_path: NonEmptyStr = "/rest/interface/ethernet/monitor" as NonEmptyStr + +// ================= READING THE LANE STATE BACK (the inverse of the wire encodings above) ================= +// +// The wire ENCODINGS above (crs812_lane_speed_wire, crs812_fec_mode_wire) turn a domain value into +// the string RouterOS accepts. Reading the switch is the same grammar in the other direction +// (DESIGN §4): the REST GET of /rest/interface/ethernet returns these same strings, so the inverse +// is a decode of a value RouterOS OWNS, not a new fact. It is partial and fail-closed: a wire value +// this module does not model decodes to an explicit Unmodelled arm carrying the string, never to a +// silent default, so a switch that reports a speed or FEC the corpus has not seen refuses loudly at +// the boundary rather than being coerced into the nearest known value. + +// The fields the reader CONSUMES, and only those: name (the lane), speed and fec-mode (the two +// values a lane intent constrains), disabled (admin state), comment (the fabric-leg marker the +// filter reads). The RouterOS response also carries auto-negotiation and running; they are NOT +// modeled here because nothing reads them yet (DESIGN §3c: a field no fold reads is red). They +// return with their consumers -- auto-negotiation with the autoneg axis (gap G1), running with the +// live link-state outcome (gap G3) -- not before. +type Crs812EthernetWire { + name: NonEmptyStr + speed: String + fec_mode: String + disabled: String + comment: String +} + +type Crs812LaneSpeedFromWire + = LaneSpeedParsed { speed: Crs812LaneSpeed } + | LaneSpeedWireUnmodelled { wire: String } + +fn crs812_lane_speed_from_wire(w: String) -> Crs812LaneSpeedFromWire { + if w == (crs812_lane_speed_wire(s: Lane50GCr2) as String) { LaneSpeedParsed { speed: Lane50GCr2 } } + else if w == (crs812_lane_speed_wire(s: Lane100GCr2) as String) { LaneSpeedParsed { speed: Lane100GCr2 } } + else if w == (crs812_lane_speed_wire(s: Lane100GCr4) as String) { LaneSpeedParsed { speed: Lane100GCr4 } } + else if w == (crs812_lane_speed_wire(s: Lane200GCr4) as String) { LaneSpeedParsed { speed: Lane200GCr4 } } + else if w == (crs812_lane_speed_wire(s: Lane400GCr8) as String) { LaneSpeedParsed { speed: Lane400GCr8 } } + else { LaneSpeedWireUnmodelled { wire: w } } +} + +type Crs812FecModeFromWire + = FecModeParsed { fec: Crs812FecMode } + | FecModeWireUnmodelled { wire: String } + +fn crs812_fec_mode_from_wire(w: String) -> Crs812FecModeFromWire { + if w == (crs812_fec_mode_wire(f: FecAuto) as String) { FecModeParsed { fec: FecAuto } } + else if w == (crs812_fec_mode_wire(f: FecOff) as String) { FecModeParsed { fec: FecOff } } + else if w == (crs812_fec_mode_wire(f: Fec74) as String) { FecModeParsed { fec: Fec74 } } + else if w == (crs812_fec_mode_wire(f: Fec91) as String) { FecModeParsed { fec: Fec91 } } + else { FecModeWireUnmodelled { wire: w } } +} + +// RouterOS renders booleans as the strings "true"/"false" in the REST JSON. A value that is neither +// is not coerced: the caller that needs a Bool gets a typed refusal, so a wire the switch never +// sends (or a schema change) is caught rather than read as false. +type Crs812WireBool + = WireBoolTrue + | WireBoolFalse + | WireBoolUnmodelled { wire: String } + +fn crs812_wire_bool(w: String) -> Crs812WireBool { + if w == "true" { WireBoolTrue } + else if w == "false" { WireBoolFalse } + else { WireBoolUnmodelled { wire: w } } +} diff --git a/dag/gunbc/spark/fabric_switch_read.dag b/dag/gunbc/spark/fabric_switch_read.dag new file mode 100644 index 00000000000..2a4b6d662f5 --- /dev/null +++ b/dag/gunbc/spark/fabric_switch_read.dag @@ -0,0 +1,135 @@ +module gunbc.spark.fabric_switch_read + +import std.types { String, Bool, List, NonEmptyStr } +import extdeps.mikrotik.crs812 { + Crs812EthernetWire, + Crs812LaneSpeedFromWire, LaneSpeedParsed, LaneSpeedWireUnmodelled, crs812_lane_speed_from_wire, + Crs812FecModeFromWire, FecModeParsed, FecModeWireUnmodelled, crs812_fec_mode_from_wire, + Crs812WireBool, WireBoolTrue, WireBoolFalse, WireBoolUnmodelled, crs812_wire_bool, +} +import gunbc.spark.fabric_switch_assessment { + Crs812LaneReading, LaneReadingTaken, + Crs812SwitchSubject, crs812_switch_subject, +} +import gunbc.spark.fabric_switch_desired { Crs812SwitchIntent } + +// TURNING THE SWITCH'S REST RESPONSE INTO ASSESSMENT READINGS. This is the workflow-layer decode: +// extdeps.mikrotik.crs812 owns what each wire STRING means (the inverse parsers this consumes), and +// this module owns the POLICY facts -- which interfaces are our fabric legs, and how a per-lane +// wire record becomes the Crs812LaneReading the assessment already consumes. It is the producer +// gunbc.spark.fabric_switch_assessment was written to receive: `fabric_switch_subject` passes +// `readings: []` today, so every lane resolves to unknown; this closes that gap on the READ side. +// +// THE PURE READ CHAIN LANDS HERE; ONLY THE FETCH IS A FRONTIER. Everything from wire records to a +// built Crs812SwitchSubject is pure and network-free, so it lands now and is consumed end to end: +// crs812_fabric_lane_read_outcomes -> crs812_fabric_read -> fabric_switch_subject_from_wire. What is +// NOT here is the one step that needs the network -- producing the List by +// fetching and decoding the switch's REST response -- which is blocked on the same capability +// extdeps.bmc.http declared as debt (redfish_http_hardwired_transport_dissolution_trigger: the +// shared `transport rest` machinery does not yet realize transport-level basic auth). So +// fabric_switch_subject_from_wire is the terminal of the pure chain and a DECLARED FRONTIER: its one +// consumer is that live-read entry, which lands when the basic-auth REST transport does. Splitting +// the fetch from the join is also the right seam -- the same join serves a live read and a replayed +// fixture without branching. + +// THE COMMENT ROUTEROS CARRIES ON EACH FABRIC LEG, set on the switch to mark the eight breakout +// lanes. It is the discriminator between our legs and every other interface in the GET response. +data crs812_fabric_leg_comment: NonEmptyStr = "gunbc fabric leg" as NonEmptyStr + +fn crs812_wire_is_fabric_leg(w: Crs812EthernetWire) -> Bool { + w.comment == (crs812_fabric_leg_comment as String) +} + +// A LANE EITHER DECODES TO A READING OR REFUSES AT THE FIELD THAT DID NOT PARSE. There is no third +// arm that guesses: an unmodelled speed, FEC or boolean is a located refusal naming the interface, +// the field and the raw wire, so a switch that reports something the corpus has not seen stops the +// read loudly instead of being coerced to the nearest known value (DESIGN §5, fail-closed). +type Crs812LaneReadOutcome + = LaneReadOk { reading: Crs812LaneReading } + | LaneReadWireRefused { interface: NonEmptyStr, field: NonEmptyStr, wire: String } + +fn crs812_lane_read_one(w: Crs812EthernetWire) -> Crs812LaneReadOutcome { + match crs812_lane_speed_from_wire(w: w.speed) { + LaneSpeedWireUnmodelled { wire: s } => + LaneReadWireRefused { interface: w.name, field: "speed" as NonEmptyStr, wire: s } + LaneSpeedParsed { speed: sp } => + match crs812_fec_mode_from_wire(w: w.fec_mode) { + FecModeWireUnmodelled { wire: f } => + LaneReadWireRefused { interface: w.name, field: "fec-mode" as NonEmptyStr, wire: f } + FecModeParsed { fec: fc } => + match crs812_wire_bool(w: w.disabled) { + WireBoolUnmodelled { wire: d } => + LaneReadWireRefused { interface: w.name, field: "disabled" as NonEmptyStr, wire: d } + WireBoolTrue => + LaneReadOk { reading: LaneReadingTaken { interface: w.name, speed: sp, fec: fc, enabled: false } } + WireBoolFalse => + LaneReadOk { reading: LaneReadingTaken { interface: w.name, speed: sp, fec: fc, enabled: true } } + } + } + } +} + +// The fabric legs of a full ethernet GET, each decoded. Filtering by the leg comment is what keeps +// the denominator OUR eight lanes rather than every interface the switch has -- the same expected +// roster the assessment's intent declares, read from the switch's own marking rather than a second +// hardcoded interface list. +fn crs812_fabric_lane_read_outcomes(wires: List) -> List { + map(filter(wires, w => crs812_wire_is_fabric_leg(w: w)), w => crs812_lane_read_one(w: w)) +} + +fn crs812_lane_read_outcome_refused(o: Crs812LaneReadOutcome) -> Bool { + match o { + LaneReadWireRefused { interface: _, field: _, wire: _ } => true + LaneReadOk { reading: _ } => false + } +} + +// THE JOIN: wire records -> the readings the assessment already consumes, or a whole-read refusal. +// It is fail-closed at the read grain: if ANY lane's wire did not parse, the read refuses and names +// the offending lanes rather than handing the assessment a denominator quietly short of the legs +// the switch actually reported. crs812_switch_subject takes exactly List, so a +// FabricReadTaken feeds it with no adaptation. +type Crs812FabricRead + = FabricReadTaken { readings: List } + | FabricReadWireRefused { refused: List } + +fn crs812_fabric_read(wires: List) -> Crs812FabricRead { + let outcomes = crs812_fabric_lane_read_outcomes(wires: wires) + let refused = filter(outcomes, o => crs812_lane_read_outcome_refused(o: o)) + if refused.length() == 0 { + FabricReadTaken { + readings: flat_map(outcomes, o => match o { + LaneReadOk { reading: r } => [r] + LaneReadWireRefused { interface: _, field: _, wire: _ } => [] + }), + } + } else { + FabricReadWireRefused { refused: refused } + } +} + +// THE TERMINAL OF THE PURE READ CHAIN, AND A DECLARED FRONTIER (DESIGN §3c). It builds the exact +// Crs812SwitchSubject the assessment's inspect_fabric_switch consumes, from a switch identity, a lane +// intent, and the wire records a read produced -- or refuses as a whole if the read did. Its ONE +// consumer is the live-read entry that fetches /rest/interface/ethernet and decodes the JSON body +// into List. That entry is NOT in this diff: it needs transport-level basic auth, +// the capability extdeps.bmc.http declared as debt. TRIGGER: the `transport rest` machinery realizes +// basic-auth GET (extdeps.bmc.http redfish_http_hardwired_transport_dissolution_trigger); the fetch +// entry then produces the wires this consumes, at which point fabric_switch_subject() can read live +// instead of passing readings: []. SUFFICIENT FOR: replacing the empty-readings subject on a live +// converge with a subject read from the switch. +type Crs812FabricSubjectRead + = FabricSubjectBuilt { subject: Crs812SwitchSubject } + | FabricSubjectReadRefused { refused: List } + +fn fabric_switch_subject_from_wire( + switch: NonEmptyStr, + intent: Crs812SwitchIntent, + wires: List, +) -> Crs812FabricSubjectRead { + match crs812_fabric_read(wires: wires) { + FabricReadWireRefused { refused: rs } => FabricSubjectReadRefused { refused: rs } + FabricReadTaken { readings: rd } => + FabricSubjectBuilt { subject: crs812_switch_subject(switch: switch, intent: intent, readings: rd) } + } +} diff --git a/dag/test/claim/spark/fabric_switch_read_witness_test.dag b/dag/test/claim/spark/fabric_switch_read_witness_test.dag new file mode 100644 index 00000000000..fe5fcab3d9a --- /dev/null +++ b/dag/test/claim/spark/fabric_switch_read_witness_test.dag @@ -0,0 +1,155 @@ +module test.claim.spark.fabric_switch_read_witness + +import std.types { Bool, String, List, NonEmptyStr } +import extdeps.mikrotik.crs812 { + Crs812EthernetWire, Lane50GCr2, Lane100GCr2, Fec91, +} +import gunbc.spark.fabric_switch_assessment { + Crs812LaneReading, LaneReadingTaken, LaneNeverRead, + crs812_lane_speed_eq, crs812_fec_mode_eq, +} +import gunbc.spark.fabric_switch_assessment { Crs812SwitchSubject } +import gunbc.spark.fabric_switch_desired { Crs812SwitchIntent, fabric_switch_intent } +import gunbc.spark.fabric_switch_read { + Crs812LaneReadOutcome, LaneReadOk, LaneReadWireRefused, + crs812_lane_read_one, crs812_fabric_lane_read_outcomes, + crs812_lane_read_outcome_refused, crs812_fabric_leg_comment, + Crs812FabricRead, FabricReadTaken, FabricReadWireRefused, crs812_fabric_read, + Crs812FabricSubjectRead, FabricSubjectBuilt, FabricSubjectReadRefused, + fabric_switch_subject_from_wire, +} + +// A fabric-leg wire record as the switch actually returned it (captured 2026-09-17 from +// GET /rest/interface/ethernet on gunbc-fabric-switch, 192.168.1.240). All eight legs were +// byte-identical in these fields, so one shape stands for the fleet and the interface name varies. +fn leg_wire(name: String, speed: String, fec: String, disabled: String) -> Crs812EthernetWire { + Crs812EthernetWire { + name: name as NonEmptyStr, + speed: speed, + fec_mode: fec, + disabled: disabled, + comment: crs812_fabric_leg_comment as String, + } +} + +data captured_fabric_legs: List = [ + leg_wire(name: "qsfp56-dd-1-1", speed: "50G-baseCR2", fec: "fec91", disabled: "false"), + leg_wire(name: "qsfp56-dd-1-3", speed: "50G-baseCR2", fec: "fec91", disabled: "false"), + leg_wire(name: "qsfp56-dd-1-5", speed: "50G-baseCR2", fec: "fec91", disabled: "false"), + leg_wire(name: "qsfp56-dd-1-7", speed: "50G-baseCR2", fec: "fec91", disabled: "false"), + leg_wire(name: "qsfp56-dd-2-1", speed: "50G-baseCR2", fec: "fec91", disabled: "false"), + leg_wire(name: "qsfp56-dd-2-3", speed: "50G-baseCR2", fec: "fec91", disabled: "false"), + leg_wire(name: "qsfp56-dd-2-5", speed: "50G-baseCR2", fec: "fec91", disabled: "false"), + leg_wire(name: "qsfp56-dd-2-7", speed: "50G-baseCR2", fec: "fec91", disabled: "false"), +] + +// A non-fabric interface the GET also returns (management port), which the leg filter must drop. +data ether1_wire: Crs812EthernetWire = Crs812EthernetWire { + name: "ether1" as NonEmptyStr, + speed: "", + fec_mode: "", + disabled: "false", + comment: "", +} + +fn outcome_is_ok_5050(o: Crs812LaneReadOutcome) -> Bool { + match o { + LaneReadWireRefused { interface: _, field: _, wire: _ } => false + LaneReadOk { reading: r } => match r { + LaneNeverRead { interface: _ } => false + LaneReadingTaken { interface: _, speed: sp, fec: fc, enabled: en } => + crs812_lane_speed_eq(a: sp, b: Lane50GCr2) && crs812_fec_mode_eq(a: fc, b: Fec91) && en + } + } +} + +// THE READ PATH TURNS THE FABRIC-LEG WIRE RECORDS INTO EIGHT 50G READINGS. The records are +// hand-authored here, TRANSCRIBED from the field values GET /rest/interface/ethernet returned on +// 2026-09-17 -- they are supplied inputs, not captured bytes: the real producer (a JSON body decoded +// into Crs812EthernetWire) does not exist in this diff and is the declared frontier named on +// fabric_switch_subject_from_wire. So what this claim discriminates is the DECODE (wire strings -> +// typed speed/FEC/enabled), not the fetch; describing it as executing over captured bytes would be +// the rung inflation DESIGN §4b(1) forbids. The inhabitance pairing -- that the real producer emits +// this shape -- lands with that fetch, not here. +test fn reads_the_eight_fabric_legs_as_50g_fec91_enabled() -> Bool { + let outcomes = crs812_fabric_lane_read_outcomes(wires: captured_fabric_legs) + outcomes.length() == 8 && all(outcomes, o => outcome_is_ok_5050(o: o)) +} + +// The management port is not a fabric leg and must not appear in the readings. +test fn a_non_fabric_interface_is_filtered_out() -> Bool { + let outcomes = crs812_fabric_lane_read_outcomes(wires: [ether1_wire, leg_wire(name: "qsfp56-dd-1-1", speed: "50G-baseCR2", fec: "fec91", disabled: "false")]) + outcomes.length() == 1 +} + +// DISCRIMINATING RED 1: a speed the corpus does not model refuses at the speed field rather than +// decoding to the nearest known value. This is the fail-closed boundary the reader exists to hold; +// without it a schema change or an unexpected speed would be silently mis-read. +test fn an_unmodelled_speed_refuses_at_the_speed_field() -> Bool { + match crs812_lane_read_one(w: leg_wire(name: "qsfp56-dd-1-1", speed: "800G-baseCR8", fec: "fec91", disabled: "false")) { + LaneReadWireRefused { interface: _, field: f, wire: w } => + (f as String) == "speed" && w == "800G-baseCR8" + LaneReadOk { reading: _ } => false + } +} + +// DISCRIMINATING RED 2: an unmodelled FEC refuses at the fec-mode field. +test fn an_unmodelled_fec_refuses_at_the_fec_field() -> Bool { + match crs812_lane_read_one(w: leg_wire(name: "qsfp56-dd-1-1", speed: "50G-baseCR2", fec: "fec134", disabled: "false")) { + LaneReadWireRefused { interface: _, field: f, wire: _ } => (f as String) == "fec-mode" + LaneReadOk { reading: _ } => false + } +} + +// A disabled lane reads as not-enabled, so the assessment can tell a leg that should carry traffic +// but is administratively down from one that is up. +test fn a_disabled_lane_reads_as_not_enabled() -> Bool { + match crs812_lane_read_one(w: leg_wire(name: "qsfp56-dd-1-2", speed: "50G-baseCR2", fec: "fec91", disabled: "true")) { + LaneReadOk { reading: r } => match r { + LaneReadingTaken { interface: _, speed: _, fec: _, enabled: en } => !en + LaneNeverRead { interface: _ } => false + } + LaneReadWireRefused { interface: _, field: _, wire: _ } => false + } +} + +// The whole captured response has no refusals -- every fabric leg decoded. +test fn the_captured_response_has_no_wire_refusals() -> Bool { + !any(crs812_fabric_lane_read_outcomes(wires: captured_fabric_legs), o => crs812_lane_read_outcome_refused(o: o)) +} + +// THE JOIN PRODUCES THE READINGS THE ASSESSMENT CONSUMES. crs812_fabric_read over the captured legs +// is a FabricReadTaken of eight readings -- the List crs812_switch_subject takes. +test fn the_join_produces_eight_readings_for_the_subject() -> Bool { + match crs812_fabric_read(wires: captured_fabric_legs) { + FabricReadTaken { readings: rd } => rd.length() == 8 + FabricReadWireRefused { refused: _ } => false + } +} + +// DISCRIMINATING RED: one unparseable lane makes the WHOLE read refuse rather than silently handing +// the assessment seven readings where the switch reported eight. Fail-closed at the read grain. +test fn one_bad_lane_refuses_the_whole_read() -> Bool { + let mixed = [ + leg_wire(name: "qsfp56-dd-1-1", speed: "50G-baseCR2", fec: "fec91", disabled: "false"), + leg_wire(name: "qsfp56-dd-1-3", speed: "800G-baseCR8", fec: "fec91", disabled: "false"), + ] + match crs812_fabric_read(wires: mixed) { + FabricReadWireRefused { refused: rs } => rs.length() == 1 + FabricReadTaken { readings: _ } => false + } +} + +// THE FRONTIER BUILDS A REAL SUBJECT. fabric_switch_subject_from_wire over a clean read yields a +// FabricSubjectBuilt -- the Crs812SwitchSubject inspect_fabric_switch consumes -- proving the pure +// chain reaches the assessment's own input type, with only the live fetch left to land. +test fn the_frontier_builds_a_switch_subject_from_a_clean_read() -> Bool { + match fabric_switch_subject_from_wire( + switch: "gunbc-fabric-switch" as NonEmptyStr, + intent: fabric_switch_intent(), + wires: captured_fabric_legs, + ) { + FabricSubjectBuilt { subject: _ } => true + FabricSubjectReadRefused { refused: _ } => false + } +}