feat(dronecan): v1.95 node pump — DroneCanNode async loop + NodeStatus heartbeat (DC-P04)

artifacts/features/FEAT-FALCON-rc-dronecan.yaml

@@ -164,12 +164,9 @@ artifacts:
   - id: FEAT-FALCON-v1.95
     type: feature
     title: "v1.95 — DroneCAN node pump (DC-P04): DroneCanNode async loop + NodeStatus heartbeat"
-    status: pending
+    status: implemented
     description: >
-      PLANNED. Also folds in gnss.Fix2 (DTID 1063, the variable covariance-tail
-      message moved from v1.94): decode the flight-relevant fixed fields
-      (lat/lon 1e-8 deg, height, sats, fix status). Then the runtime that ties
-      the transfer layer + decoders to the CanBus seam:
+      The runtime that ties the transfer layer + decoders to the CanBus seam:
       DroneCanNode<C: CanBus> — an async pump (mirrors UbxReader) that
       reads frames, drives the TransferReassembler, dispatches completed
       transfers to the per-DTID decoders, and broadcasts the node's own
@@ -190,3 +187,28 @@ artifacts:
         target: SYSREQ-FALCON-008
       - type: depends-on
         target: FEAT-FALCON-v1.93
+
+  - id: FEAT-FALCON-v1.95g
+    type: feature
+    title: "v1.95g — DroneCAN gnss.Fix2 decoder [backlog: needs real-frame offset validation]"
+    status: pending
+    description: >
+      BACKLOG (deferred from v1.94/95). uavcan.equipment.gnss.Fix2 (DTID 1063):
+      decode the flight-relevant fields (longitude/latitude int37 1e-8 deg,
+      height_msl int27 mm, sats_used, fix status). Why deferred + gated: the DSDL
+      is BIT-PACKED (int37 lat/lon, int27 heights — not byte-aligned) and the
+      leading uavcan.Timestamp width is ambiguous in the summarised spec, so a
+      self-constructed round-trip test would pass even with WRONG offsets. A GPS
+      decoder is flight-critical — it must be validated against a real captured
+      Fix2 frame (or libcanard/pydronecan reference vectors), not just
+      self-tested. Needs a signed-bit-field reader (read_signed_bits) over the
+      v1.94 read_bits primitive + reference-vector tests.
+    tags: [falcon, dronecan, gnss, fix2, backlog, validation-gated, kani, planned]
+    fields:
+      release-target: "decode_gnss_fix2 (int37/int27 fields) validated against a real Fix2 frame / libcanard reference vectors; Kani read_signed_bits bound"
+      px4-equivalent: "DroneCAN GPS (Fix2) ingest — falcon adds a reference-validated, Kani-bounded decoder"
+    links:
+      - type: implements
+        target: SYSREQ-FALCON-008
+      - type: depends-on
+        target: FEAT-FALCON-v1.94

artifacts/swreq/SWREQ-FALCON-DC-P04.yaml

@@ -0,0 +1,49 @@
+artifacts:
+  - id: SWREQ-FALCON-DC-P04
+    type: sw-req
+    title: "DC-P04: DroneCanNode async pump + NodeStatus heartbeat — the runtime over the CanBus seam"
+    status: implemented
+    description: >
+      Falcon shall provide the DroneCAN node runtime that ties the verified
+      transfer layer (DC-P01) to the relay-hal CanBus seam: an async pump that
+      receives CAN frames and dispatches completed transfers to the decoders, and
+      the node's own NodeStatus heartbeat. Static node-id; dynamic node-id
+      allocation is a follow-on.
+
+      Behaviour (crates/relay-dronecan, node.rs + msg.rs):
+        - DroneCanNode<C: CanBus>::poll() awaits one frame on the bus and feeds
+          the verified Reassembler, returning a completed Transfer (or None). The
+          async path adds ONLY the bus await — the dispatch is the v1.92
+          reassembler step (totality + buffer-bound already proven). A bus recv
+          error propagates (the async path is fallible — the health source).
+        - send_heartbeat() encodes the 7-byte NodeStatus and emits a single-frame
+          transfer, advancing the 5-bit transfer id. encode_node_status is the
+          inverse of decode_node_status: decode(encode(s)) == s for in-range
+          fields.
+        - The async pump and a sync reassembler fed the same frame yield an
+          identical Transfer (the runtime preserves the verified reassembler).
+
+      The architecture (spar/dronecan.aadl) already models the Reassemble +
+      Heartbeat threads (v1.92); the pump orchestrates them (no new spar thread).
+
+      SCOPE (deliberate, evidence-backed): gnss.Fix2 (DTID 1063) is DEFERRED. Its
+      DSDL uses int37 lat/lon + int27 heights (bit-packed, NOT byte-aligned) and
+      the uavcan.Timestamp width is ambiguous in the summarised spec — a
+      self-constructed round-trip test would pass even with wrong offsets, so a
+      GPS decoder cannot be shipped without validation against a real captured
+      frame / libcanard. It becomes its own validation-gated slice.
+    tags: [falcon, dronecan, node, heartbeat, async-pump, canbus, kani, v1.95]
+    fields:
+      req-type: safety
+      priority: must
+      verification-criteria: >
+        relay-dronecan: poll() reassembles a frame identically to a sync push;
+        send_heartbeat() emits a frame that reassembles + decodes back to the
+        original NodeStatus; poll propagates a bus error. Kani DC-K09
+        verify_node_status_round_trip: decode(encode(s)) == Some(s) for any
+        in-range NodeStatus (the heartbeat a receiving node decodes byte-identical).
+        The async path is tested via a hand-rolled block_on over a mock CanBus
+        (the falcon-gnss-ubx pattern).
+    links:
+      - type: derives-from
+        target: SYSREQ-FALCON-008

artifacts/verification/FV-FALCON-DC-004.yaml

@@ -0,0 +1,38 @@
+artifacts:
+  - id: FV-FALCON-DC-004
+    type: sw-verification
+    title: "DroneCanNode async pump + NodeStatus heartbeat — sync/async equivalence + round-trip (DC-P04, v1.95)"
+    status: implemented
+    description: >
+      Verifies SWREQ-FALCON-DC-P04. relay-dronecan gains the node runtime
+      (node.rs) and the heartbeat encoder (msg.rs encode_node_status).
+      Test-level evidence (pulseengine.eu#89), each step a real named
+      test/harness:
+        - msg::tests::node_status_encode_decode_round_trips: decode(encode(s)) == s.
+        - node::tests::poll_reassembles_like_sync_push: DroneCanNode::poll over a
+          mock CanBus yields the SAME Transfer as a sync Reassembler fed the same
+          frame (the runtime preserves the verified reassembler).
+        - node::tests::heartbeat_round_trips_through_reassembler: a heartbeat the
+          node emits reassembles + decodes back to the original NodeStatus
+          (TX path round-trips through RX).
+        - node::tests::poll_propagates_bus_error: a bus recv error -> Err (the
+          async path is fallible).
+        - Kani DC-K09 verify_node_status_round_trip: decode(encode(s)) == Some(s)
+          for ANY in-range NodeStatus (integer bit-packing; Kani-tractable).
+      The async path is driven by a hand-rolled block_on over a mock CanBus
+      (the falcon-gnss-ubx test-executor pattern), no_std/no_alloc.
+      ORACLE: `cargo test -p relay-dronecan` green (40 tests); `cargo kani -p
+      relay-dronecan` VERIFICATION SUCCESSFUL for all nine harnesses.
+    tags: [verification, falcon, dronecan, node, heartbeat, async, relay-dronecan, kani, "v1.95"]
+    fields:
+      method: formal-verification
+      steps:
+        - run: "cargo test -p relay-dronecan msg::tests::node_status_encode_decode_round_trips"
+        - run: "cargo test -p relay-dronecan node::tests::poll_reassembles_like_sync_push"
+        - run: "cargo test -p relay-dronecan node::tests::heartbeat_round_trips_through_reassembler"
+        - run: "cargo test -p relay-dronecan node::tests::poll_propagates_bus_error"
+        # Kani DC-K09 — gated by the kani.yml matrix (relay-dronecan entry)
+        - run: "cargo kani -p relay-dronecan --harness verify_node_status_round_trip"
+    links:
+      - type: verifies
+        target: SWREQ-FALCON-DC-P04

crates/relay-dronecan/plain/src/kani_proofs.rs

@@ -7,7 +7,7 @@
 #![cfg(kani)]
 
 use crate::id::{decode_message_id, encode_message_id, MessageId};
-use crate::msg::{decode_node_status, encode_raw_command, MAX_ESC};
+use crate::msg::{decode_node_status, encode_node_status, encode_raw_command, NodeStatus, MAX_ESC};
 use crate::sensors::read_bits;
 use crate::tail::{decode_tail, encode_tail};
 use crate::transfer::{encode_single_frame, CanFrame, Reassembler, MAX_PAYLOAD};
@@ -156,3 +156,19 @@ fn verify_read_bits_bounded() {
         assert!(v < (1u32 << nbits));
     }
 }
+
+/// DC-K09 — the NodeStatus heartbeat round-trips: for ANY in-range NodeStatus,
+/// `decode_node_status(&encode_node_status(s)) == Some(s)`. The TX heartbeat the
+/// DroneCanNode emits is decoded byte-identical by a receiving node. Integer
+/// (bit-packing only) — Kani-tractable.
+#[kani::proof]
+fn verify_node_status_round_trip() {
+    let s = NodeStatus {
+        uptime_sec: kani::any(),
+        health: kani::any::<u8>() & 0x03,
+        mode: kani::any::<u8>() & 0x07,
+        sub_mode: kani::any::<u8>() & 0x07,
+        vendor_status: kani::any(),
+    };
+    assert!(decode_node_status(&encode_node_status(&s)) == Some(s));
+}

crates/relay-dronecan/plain/src/lib.rs

@@ -27,6 +27,7 @@ pub mod crc;
 pub mod float16;
 pub mod id;
 pub mod msg;
+pub mod node;
 pub mod sensors;
 pub mod tail;
 pub mod transfer;

crates/relay-dronecan/plain/src/msg.rs

@@ -53,6 +53,18 @@ pub fn decode_node_status(payload: &[u8]) -> Option<NodeStatus> {
     })
 }
 
+/// Encode a NodeStatus into its 7-byte single-frame payload (the inverse of
+/// [`decode_node_status`]). Each bit-field is masked to its DSDL width, so
+/// `decode_node_status(&encode_node_status(s))` round-trips for in-range fields.
+/// This node's own heartbeat (the DroneCanNode broadcasts it at 1 Hz). Total.
+pub fn encode_node_status(s: &NodeStatus) -> [u8; 7] {
+    let mut p = [0u8; 7];
+    p[..4].copy_from_slice(&s.uptime_sec.to_le_bytes());
+    p[4] = (s.health & 0x03) | ((s.mode & 0x07) << 2) | ((s.sub_mode & 0x07) << 5);
+    p[5..7].copy_from_slice(&s.vendor_status.to_le_bytes());
+    p
+}
+
 /// Pack up to [`MAX_ESC`] int14 throttle commands (LSB-first) into `out`,
 /// returning the number of bytes written (0 if `out` is too small or no
 /// channels). Each value is clamped to the int14 range. Total: never panics;
@@ -137,6 +149,18 @@ mod tests {
         assert_eq!(decode_node_status(&[0; 6]), None);
     }
 
+    #[test]
+    fn node_status_encode_decode_round_trips() {
+        let s = NodeStatus {
+            uptime_sec: 0x0102_0304,
+            health: 2,
+            mode: 5,
+            sub_mode: 3,
+            vendor_status: 0xBEEF,
+        };
+        assert_eq!(decode_node_status(&encode_node_status(&s)), Some(s));
+    }
+
     #[test]
     fn raw_command_round_trips_quad() {
         // a quad: 4 int14 throttles (incl a negative reverse value)

crates/relay-dronecan/plain/src/node.rs

@@ -0,0 +1,181 @@
+//! The DroneCAN node runtime (DC-P04) — the async pump tying the verified
+//! transfer layer to the relay-hal CanBus seam, plus the NodeStatus heartbeat.
+//!
+//! `DroneCanNode<C: CanBus>` mirrors `UbxReader`: `poll` receives one CAN frame
+//! and drives the verified [`Reassembler`], returning a completed [`Transfer`];
+//! `send_heartbeat` encodes + emits this node's own NodeStatus at the
+//! DroneCAN-spec 1 Hz (the caller drives the cadence). Static node-id; dynamic
+//! node-id allocation (uavcan.protocol.dynamic_node_id.Allocation) is a
+//! follow-on. The decode/dispatch step is the verified reassembler — the async
+//! path adds only the await on the bus.
+
+use crate::msg::{encode_node_status, NodeStatus, DTID_NODE_STATUS};
+use crate::transfer::{encode_single_frame, Reassembler, Transfer};
+use relay_hal::CanBus;
+
+/// DroneCAN transfer priority used for the NodeStatus heartbeat (mid priority).
+const HEARTBEAT_PRIORITY: u8 = 16;
+
+/// A static-node-id DroneCAN node over a [`CanBus`] seam (jess binds FlexCAN).
+pub struct DroneCanNode<C> {
+    bus: C,
+    reassembler: Reassembler,
+    node_id: u8,
+    heartbeat_tid: u8,
+}
+
+impl<C: CanBus> DroneCanNode<C> {
+    /// A node with the given static node id, reassembling one message type (its
+    /// 64-bit data-type signature, for the multi-frame transfer CRC).
+    pub fn new(bus: C, node_id: u8, signature: u64) -> Self {
+        Self {
+            bus,
+            reassembler: Reassembler::new(signature),
+            node_id,
+            heartbeat_tid: 0,
+        }
+    }
+
+    /// Receive one CAN frame and feed the verified reassembler. Returns a
+    /// completed [`Transfer`] when an end-of-transfer frame closes a valid one;
+    /// `None` otherwise. The async path adds only the bus await — the dispatch
+    /// is the v1.92 reassembler step (totality + buffer-bound proven).
+    pub async fn poll(&mut self) -> Result<Option<Transfer>, C::Error> {
+        let frame = self.bus.recv().await?;
+        Ok(self.reassembler.push(&frame))
+    }
+
+    /// Broadcast this node's NodeStatus heartbeat: encode the 7-byte payload and
+    /// emit a single-frame transfer, advancing the 5-bit transfer id. The caller
+    /// drives the 1 Hz cadence (spar models the Heartbeat thread's timing).
+    pub async fn send_heartbeat(&mut self, status: &NodeStatus) -> Result<(), C::Error> {
+        let payload = encode_node_status(status);
+        // a 7-byte payload always fits one frame, so encode_single_frame -> Some
+        if let Some(frame) = encode_single_frame(
+            DTID_NODE_STATUS,
+            self.node_id,
+            HEARTBEAT_PRIORITY,
+            self.heartbeat_tid,
+            &payload,
+        ) {
+            self.heartbeat_tid = (self.heartbeat_tid + 1) & 0x1F;
+            self.bus.send(&frame).await?;
+        }
+        Ok(())
+    }
+
+    /// Borrow the underlying bus.
+    pub fn bus(&mut self) -> &mut C {
+        &mut self.bus
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::msg::decode_node_status;
+    use crate::transfer::Reassembler;
+    use relay_hal::CanFrame;
+
+    /// A mock CanBus: yields a preset RX frame sequence and records TX frames.
+    /// no_std/no_alloc — fixed buffers.
+    struct MockCanBus {
+        rx: [CanFrame; 4],
+        rx_len: usize,
+        rx_pos: usize,
+        tx: [CanFrame; 4],
+        tx_len: usize,
+    }
+
+    impl MockCanBus {
+        fn new() -> Self {
+            let empty = CanFrame { id: 0, dlc: 0, data: [0; 8] };
+            Self { rx: [empty; 4], rx_len: 0, rx_pos: 0, tx: [empty; 4], tx_len: 0 }
+        }
+    }
+
+    impl CanBus for MockCanBus {
+        type Error = ();
+        async fn send(&mut self, frame: &CanFrame) -> Result<(), ()> {
+            if self.tx_len < 4 {
+                self.tx[self.tx_len] = *frame;
+                self.tx_len += 1;
+            }
+            Ok(())
+        }
+        async fn recv(&mut self) -> Result<CanFrame, ()> {
+            if self.rx_pos < self.rx_len {
+                let f = self.rx[self.rx_pos];
+                self.rx_pos += 1;
+                Ok(f)
+            } else {
+                Err(())
+            }
+        }
+    }
+
+    /// Drive a future that completes synchronously (the mock delivers in one
+    /// poll). Mirrors falcon-gnss-ubx's test executor.
+    fn block_on<F: core::future::Future>(fut: F) -> F::Output {
+        use core::task::{Context, Poll, Waker};
+        let mut fut = core::pin::pin!(fut);
+        let mut cx = Context::from_waker(Waker::noop());
+        loop {
+            if let Poll::Ready(v) = fut.as_mut().poll(&mut cx) {
+                return v;
+            }
+        }
+    }
+
+    /// The async pump dispatches a frame to the same Transfer the sync
+    /// reassembler produces — the runtime preserves the verified reassembler.
+    #[test]
+    fn poll_reassembles_like_sync_push() {
+        let payload = [1u8, 2, 3];
+        let frame = encode_single_frame(341, 9, 16, 0, &payload).unwrap();
+
+        let mut r = Reassembler::new(0);
+        let sync = r.push(&frame).expect("single-frame completes");
+
+        let mut bus = MockCanBus::new();
+        bus.rx[0] = frame;
+        bus.rx_len = 1;
+        let mut node = DroneCanNode::new(bus, 9, 0);
+        let asyncd = block_on(node.poll()).unwrap().expect("poll yields the transfer");
+
+        assert_eq!(asyncd.data_type_id, sync.data_type_id);
+        assert_eq!(asyncd.len, sync.len);
+        assert_eq!(&asyncd.payload[..asyncd.len], &payload);
+    }
+
+    /// A heartbeat emitted by the node reassembles + decodes back to the original
+    /// NodeStatus — the TX path round-trips through the RX path.
+    #[test]
+    fn heartbeat_round_trips_through_reassembler() {
+        let status = NodeStatus {
+            uptime_sec: 42,
+            health: 1,
+            mode: 0,
+            sub_mode: 0,
+            vendor_status: 7,
+        };
+        let mut node = DroneCanNode::new(MockCanBus::new(), 5, 0);
+        block_on(node.send_heartbeat(&status)).unwrap();
+
+        let sent = node.bus().tx[0];
+        assert!(node.bus().tx_len == 1);
+        let mut r = Reassembler::new(0);
+        let t = r.push(&sent).expect("heartbeat reassembles");
+        assert_eq!(t.data_type_id, DTID_NODE_STATUS);
+        assert_eq!(t.source_node_id, 5);
+        assert_eq!(decode_node_status(&t.payload[..t.len]), Some(status));
+    }
+
+    /// A bus recv error propagates (the async path is fallible — the health
+    /// source).
+    #[test]
+    fn poll_propagates_bus_error() {
+        let mut node = DroneCanNode::new(MockCanBus::new(), 1, 0); // empty rx -> Err
+        assert!(block_on(node.poll()).is_err());
+    }
+}