Fabric switch reader: RouterOS response → typed lane readings

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 } }
+}

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<Crs812EthernetWire> 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<Crs812EthernetWire>) -> List<Crs812LaneReadOutcome> {
+  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<Crs812LaneReading>, so a
+// FabricReadTaken feeds it with no adaptation.
+type Crs812FabricRead
+  = FabricReadTaken { readings: List<Crs812LaneReading> }
+  | FabricReadWireRefused { refused: List<Crs812LaneReadOutcome> }
+
+fn crs812_fabric_read(wires: List<Crs812EthernetWire>) -> 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<Crs812EthernetWire>. 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<Crs812LaneReadOutcome> }
+
+fn fabric_switch_subject_from_wire(
+  switch: NonEmptyStr,
+  intent: Crs812SwitchIntent,
+  wires: List<Crs812EthernetWire>,
+) -> 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) }
+  }
+}

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<Crs812EthernetWire> = [
+  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<Crs812LaneReading> 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
+  }
+}