From b460a63dff8ce0b25315051013c67fb193006247 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 24 Jun 2026 20:50:58 +0200 Subject: [PATCH] =?UTF-8?q?feat(dronecan):=20v1.95=20node=20pump=20?= =?UTF-8?q?=E2=80=94=20DroneCanNode=20async=20loop=20+=20NodeStatus=20hear?= =?UTF-8?q?tbeat=20(DC-P04)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The runtime that ties the verified transfer layer to the relay-hal CanBus seam, completing the DroneCAN arc. - node.rs: DroneCanNode (mirrors UbxReader). poll() awaits one frame and drives the verified Reassembler -> Transfer; the async path adds ONLY the bus await (dispatch is the v1.92 reassembler step). send_heartbeat() encodes + emits this node's NodeStatus single-frame transfer (static node-id; dynamic allocation a follow-on). A bus recv error propagates (fallible-as-health). - msg.rs: encode_node_status (inverse of decode_node_status, the heartbeat encoder). No spar change: dronecan.aadl already models the Reassemble + Heartbeat threads (v1.92); the pump orchestrates them. Verification: - 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). 9/9 relay-dronecan harnesses SUCCESSFUL. - 40 tests: NodeStatus encode/decode round-trip; poll() reassembles identically to a sync push (async==sync equivalence over a mock CanBus + hand-rolled block_on, the falcon-gnss-ubx pattern); heartbeat TX round-trips through RX; bus error propagates. rivet: SWREQ-FALCON-DC-P04 + FV-FALCON-DC-004 (test-level, 5 steps). validate PASS, 0 gaps. Clean-room 10/10. SCOPE (deliberate, evidence-backed): gnss.Fix2 DEFERRED to FEAT-FALCON-v1.95g (backlog). Its DSDL is bit-packed (int37 lat/lon, int27 heights) 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 flight-critical GPS decoder must be validated against a real captured frame / libcanard, not self-tested. Fetched the DSDL (which corrected my int64 assumption) before making this call. Falsification: this release is wrong if the async poll dispatches a frame differently from the sync reassembler, if a heartbeat the node emits fails to decode back to its NodeStatus, or if a bus recv error is swallowed instead of propagated. Co-Authored-By: Claude Opus 4.8 --- .../features/FEAT-FALCON-rc-dronecan.yaml | 32 +++- artifacts/swreq/SWREQ-FALCON-DC-P04.yaml | 49 +++++ artifacts/verification/FV-FALCON-DC-004.yaml | 38 ++++ .../relay-dronecan/plain/src/kani_proofs.rs | 18 +- crates/relay-dronecan/plain/src/lib.rs | 1 + crates/relay-dronecan/plain/src/msg.rs | 24 +++ crates/relay-dronecan/plain/src/node.rs | 181 ++++++++++++++++++ 7 files changed, 337 insertions(+), 6 deletions(-) create mode 100644 artifacts/swreq/SWREQ-FALCON-DC-P04.yaml create mode 100644 artifacts/verification/FV-FALCON-DC-004.yaml create mode 100644 crates/relay-dronecan/plain/src/node.rs diff --git a/artifacts/features/FEAT-FALCON-rc-dronecan.yaml b/artifacts/features/FEAT-FALCON-rc-dronecan.yaml index 95d494d..fe3bc97 100644 --- a/artifacts/features/FEAT-FALCON-rc-dronecan.yaml +++ b/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 — 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 diff --git a/artifacts/swreq/SWREQ-FALCON-DC-P04.yaml b/artifacts/swreq/SWREQ-FALCON-DC-P04.yaml new file mode 100644 index 0000000..270f5a7 --- /dev/null +++ b/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::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 diff --git a/artifacts/verification/FV-FALCON-DC-004.yaml b/artifacts/verification/FV-FALCON-DC-004.yaml new file mode 100644 index 0000000..447b309 --- /dev/null +++ b/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 diff --git a/crates/relay-dronecan/plain/src/kani_proofs.rs b/crates/relay-dronecan/plain/src/kani_proofs.rs index 441cb54..8e82c75 100644 --- a/crates/relay-dronecan/plain/src/kani_proofs.rs +++ b/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::() & 0x03, + mode: kani::any::() & 0x07, + sub_mode: kani::any::() & 0x07, + vendor_status: kani::any(), + }; + assert!(decode_node_status(&encode_node_status(&s)) == Some(s)); +} diff --git a/crates/relay-dronecan/plain/src/lib.rs b/crates/relay-dronecan/plain/src/lib.rs index 33b6cc3..d2ecc68 100644 --- a/crates/relay-dronecan/plain/src/lib.rs +++ b/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; diff --git a/crates/relay-dronecan/plain/src/msg.rs b/crates/relay-dronecan/plain/src/msg.rs index e8b7073..9f7b605 100644 --- a/crates/relay-dronecan/plain/src/msg.rs +++ b/crates/relay-dronecan/plain/src/msg.rs @@ -53,6 +53,18 @@ pub fn decode_node_status(payload: &[u8]) -> Option { }) } +/// 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) diff --git a/crates/relay-dronecan/plain/src/node.rs b/crates/relay-dronecan/plain/src/node.rs new file mode 100644 index 0000000..65950a8 --- /dev/null +++ b/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` 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 { + bus: C, + reassembler: Reassembler, + node_id: u8, + heartbeat_tid: u8, +} + +impl DroneCanNode { + /// 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, 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 { + 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(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()); + } +}