From 93929b2d6ac3770b73481cc61a47109d301f8e7c Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 15 Jul 2026 20:00:26 +0200 Subject: [PATCH 1/4] =?UTF-8?q?feat(falcon):=20v1.119=20=E2=80=94=20GCS=20?= =?UTF-8?q?telemetry=20streaming=20+=20in-flight=20tuning=20(MAVLINK-P06)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Today the GCS is blind beyond HEARTBEAT; this lands the operator telemetry set and the missing store→core tuning link, budgeted for the real SiK 433 MHz radio: - relay-mavlink telemetry.rs: six encode-only messages (ATTITUDE, SYS_STATUS, GPS_RAW_INT, SERVO_OUTPUT_RAW, VFR_HUD, STATUSTEXT), each wire-conformant against embedded pymavlink 2.4.49 reference vectors (external vectors, not self-round-trip — the DroneCAN bit-order lesson). Generator: scripts/gen-mavlink-telemetry-vectors.py. - relay-mavlink telemetry_sched.rs: rate + priority + byte-budget scheduler. Criticals (HEARTBEAT/STATUSTEXT) are never starved — held exact even at collapse budgets; normals degrade fairly by deferral age (an index-ordered scan starved the tail streams — caught by the no-full-starvation test). Full falcon set fits the 7200 B/s SiK budget with >=20% headroom, measured over 30 s. - falcon-core tuning.rs: register_tuning/apply_tuning — the store→core application link (falcon-param was GCS↔store only). Five MC_* knobs, bounded twice (K01-proven store write + setter clamps). - falcon-param: end-to-end in-flight test — PARAM_SET on the wire handler lands in a core FLYING the analytic plant on the very next control cycle; out-of-range rejected at the store, core never sees it. SWREQ-FALCON-MAVLINK-P06 → implemented (two-commit rule: promotion to verified is the separate verify PR). Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG --- Cargo.lock | 2 + artifacts/swreq/SWREQ-FALCON-MAVLINK-P06.yaml | 2 +- crates/falcon-core/Cargo.toml | 1 + crates/falcon-core/plain/src/lib.rs | 32 ++ crates/falcon-core/plain/src/tuning.rs | 54 +++ crates/falcon-param/Cargo.toml | 1 + crates/falcon-param/plain/src/lib.rs | 70 ++++ crates/relay-mavlink/plain/src/lib.rs | 2 + crates/relay-mavlink/plain/src/telemetry.rs | 368 ++++++++++++++++++ .../plain/src/telemetry_sched.rs | 262 +++++++++++++ scripts/gen-mavlink-telemetry-vectors.py | 63 +++ 11 files changed, 856 insertions(+), 1 deletion(-) create mode 100644 crates/falcon-core/plain/src/tuning.rs create mode 100644 crates/relay-mavlink/plain/src/telemetry.rs create mode 100644 crates/relay-mavlink/plain/src/telemetry_sched.rs create mode 100644 scripts/gen-mavlink-telemetry-vectors.py diff --git a/Cargo.lock b/Cargo.lock index b6d1867..6b400f2 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -279,6 +279,7 @@ dependencies = [ "relay-log", "relay-math", "relay-mix-quad", + "relay-param", "relay-preflight", ] @@ -381,6 +382,7 @@ dependencies = [ name = "falcon-param" version = "0.1.0" dependencies = [ + "falcon-core", "proptest", "relay-mavlink", "relay-param", diff --git a/artifacts/swreq/SWREQ-FALCON-MAVLINK-P06.yaml b/artifacts/swreq/SWREQ-FALCON-MAVLINK-P06.yaml index 65f519c..f051085 100644 --- a/artifacts/swreq/SWREQ-FALCON-MAVLINK-P06.yaml +++ b/artifacts/swreq/SWREQ-FALCON-MAVLINK-P06.yaml @@ -2,7 +2,7 @@ artifacts: - id: SWREQ-FALCON-MAVLINK-P06 type: sw-req title: "MAVLINK-P06 — operator telemetry streaming + in-flight parameter tuning over the SiK link" - status: proposed + status: implemented release: falcon-v1.119.0 description: > The vehicle shall stream continuous state/health telemetry to the GCS diff --git a/crates/falcon-core/Cargo.toml b/crates/falcon-core/Cargo.toml index edba419..e253137 100644 --- a/crates/falcon-core/Cargo.toml +++ b/crates/falcon-core/Cargo.toml @@ -21,6 +21,7 @@ relay-fsm = { path = "../relay-fsm" } relay-preflight = { path = "../relay-preflight" } relay-calib = { path = "../relay-calib" } relay-log = { path = "../relay-log" } +relay-param = { path = "../relay-param" } [lints] workspace = true diff --git a/crates/falcon-core/plain/src/lib.rs b/crates/falcon-core/plain/src/lib.rs index a311291..0ec419f 100644 --- a/crates/falcon-core/plain/src/lib.rs +++ b/crates/falcon-core/plain/src/lib.rs @@ -281,6 +281,37 @@ impl FlightCore { self.yaw_setpoint } + /// Set the hover-thrust feedforward (per-airframe; clamped to [0,1]). + pub fn set_hover_thrust_core(&mut self, t: f32) { + self.hover_thrust = if t.is_finite() { t.clamp(0.0, 1.0) } else { self.hover_thrust }; + } + + /// Set the landing descent rate (m/s, NED +down; clamped to [0.1, 2]). + pub fn set_landing_descent(&mut self, vz: f32) { + self.landing_descent = + if vz.is_finite() { vz.clamp(0.1, 2.0) } else { self.landing_descent }; + } + + /// Current altitude P/D gains (tuning observability, v1.119). + pub fn altitude_gains(&self) -> (f32, f32) { + (self.kp_alt, self.kd_alt) + } + + /// Current altitude integral gain (tuning observability, v1.119). + pub fn altitude_integral_gain(&self) -> f32 { + self.ki_alt + } + + /// Current hover-thrust feedforward (tuning observability, v1.119). + pub fn hover_thrust(&self) -> f32 { + self.hover_thrust + } + + /// Current landing descent rate (tuning observability, v1.119). + pub fn landing_descent(&self) -> f32 { + self.landing_descent + } + /// FDI observability (v1.115): `(rate2, tilt_cos, gate_open, resid[4])` from /// the last single-rotor-out detector evaluation. `gate_open` is the /// near-level/low-rate gate; when it stays false under sensor noise the @@ -1655,6 +1686,7 @@ impl FlightBackend for SimBackend { } pub mod blackbox_backend; +pub mod tuning; #[cfg(test)] mod blackbox_replay_tests { diff --git a/crates/falcon-core/plain/src/tuning.rs b/crates/falcon-core/plain/src/tuning.rs new file mode 100644 index 0000000..bf7bb96 --- /dev/null +++ b/crates/falcon-core/plain/src/tuning.rs @@ -0,0 +1,54 @@ +//! IN-FLIGHT TUNING (MAVLINK-P06, v1.119) — the store→core application link. +//! +//! falcon-param (v1.96) bound the GCS wire to the verified relay-param store +//! (PARAM_SET → bounded write), and PARAM-P03 (v1.117) made the store +//! persistent — but nothing ever APPLIED a stored value to the running +//! [`FlightCore`]. This module is that missing link: a small named schema of +//! tunable knobs and an `apply` that pushes the store's current values into +//! the core. Called once per control cycle by the integration, a GCS +//! PARAM_SET lands in the loop ON THE NEXT TICK — bounded twice over (the +//! K01-proven store write, then the setters' own clamps). + +use crate::FlightCore; +use relay_param::{param_id, ParamDef, ParamStore}; + +/// Register falcon's tunable knobs (schema bounds + current-behavior +/// defaults). Idempotent per store; returns false if the store lacks room. +pub fn register_tuning(store: &mut ParamStore) -> bool { + let defs = [ + // Altitude P-I-D (the gz-reconciled defaults are per-plant; these + // are the analytic-plant baseline the core constructs with). + ParamDef { id: param_id("MC_ALT_P"), min: 0.01, max: 1.0, default: 0.05 }, + ParamDef { id: param_id("MC_ALT_D"), min: 0.0, max: 3.0, default: 0.30 }, + ParamDef { id: param_id("MC_ALT_I"), min: 0.0, max: 0.2, default: 0.0 }, + // Hover-thrust feedforward (per-airframe). + ParamDef { id: param_id("MC_HOVER_THR"), min: 0.2, max: 0.8, default: 0.5 }, + // Landing descent rate (m/s, NED +down). + ParamDef { id: param_id("MC_LAND_VZ"), min: 0.2, max: 1.5, default: 0.5 }, + ]; + for d in defs { + if !store.register(d) { + return false; + } + } + true +} + +/// Push the store's current tuning values into the core. Call once per +/// control cycle (cheap: five bounded reads) — a PARAM_SET applied to the +/// store is live in the loop on the next tick. +pub fn apply_tuning(store: &ParamStore, core: &mut FlightCore) { + let g = |name: &str| store.get(¶m_id(name)); + if let (Some(kp), Some(kd)) = (g("MC_ALT_P"), g("MC_ALT_D")) { + core.set_altitude_gains(kp, kd); + } + if let Some(ki) = g("MC_ALT_I") { + core.set_altitude_integral_gain(ki); + } + if let Some(h) = g("MC_HOVER_THR") { + core.set_hover_thrust_core(h); + } + if let Some(vz) = g("MC_LAND_VZ") { + core.set_landing_descent(vz); + } +} diff --git a/crates/falcon-param/Cargo.toml b/crates/falcon-param/Cargo.toml index 9be0455..bccec36 100644 --- a/crates/falcon-param/Cargo.toml +++ b/crates/falcon-param/Cargo.toml @@ -16,6 +16,7 @@ relay-param = { path = "../relay-param" } relay-mavlink = { path = "../relay-mavlink" } [dev-dependencies] +falcon-core = { path = "../falcon-core" } proptest.workspace = true [lints] diff --git a/crates/falcon-param/plain/src/lib.rs b/crates/falcon-param/plain/src/lib.rs index 450d226..64687d8 100644 --- a/crates/falcon-param/plain/src/lib.rs +++ b/crates/falcon-param/plain/src/lib.rs @@ -113,6 +113,76 @@ pub fn on_param_request_list_item( value_at(store, i) } +#[cfg(test)] +mod tuning_tests { + use super::*; + use falcon_core::tuning::{apply_tuning, register_tuning}; + use falcon_core::{FlightCore, SimBackend}; + use relay_mavlink::param::MAV_PARAM_TYPE_REAL32; + use relay_param::param_id; + + /// MAVLINK-P06 in-flight tuning, end to end: a GCS PARAM_SET on the wire + /// handler lands in the RUNNING core after one apply cycle — bounded by + /// the K01-proven store write AND the setter clamps; an out-of-range set + /// is rejected at the store and the core keeps flying on the old value. + #[test] + fn param_set_applies_to_the_core_within_one_cycle() { + let mut store: ParamStore<8> = ParamStore::new(); + assert!(register_tuning(&mut store)); + // IN FLIGHT: the core is actually stepping against the analytic + // plant while the GCS tunes it — not a parked core. + let dt = 0.004f32; + let level = [[1.0, 0.0, 0.0], [0.0, 1.0, 0.0], [0.0, 0.0, 1.0]]; + let mut plant = SimBackend::new(level, dt); + let mut core = FlightCore::new(0.5, 1.0 / dt); + core.set_altitude(-2.0); + apply_tuning(&store, &mut core); // defaults land + assert_eq!(core.altitude_gains(), (0.05, 0.30)); + for _ in 0..500 { + apply_tuning(&store, &mut core); // the per-cycle call site + core.step(&mut plant); + } + + // GCS tunes the altitude P gain in flight. + let set = ParamSet { + target_system: 1, + target_component: 1, + param_id: param_id("MC_ALT_P"), + param_value: 0.15, + param_type: MAV_PARAM_TYPE_REAL32, + }; + let ack = on_param_set(&mut store, &set).expect("known param"); + assert_eq!(ack.param_value, 0.15); + apply_tuning(&store, &mut core); // the next control cycle + core.step(&mut plant); + assert_eq!(core.altitude_gains().0, 0.15, "live on the very next cycle"); + + // Out-of-range: rejected at the store; the core NEVER sees it. + let bad = ParamSet { param_value: 99.0, ..set }; + let ack = on_param_set(&mut store, &bad).expect("known param"); + assert_eq!(ack.param_value, 0.15, "ack reverts the GCS UI"); + apply_tuning(&store, &mut core); + assert_eq!(core.altitude_gains().0, 0.15, "core unchanged"); + + // The other knobs apply too. + on_param_set(&mut store, &ParamSet { + param_id: param_id("MC_LAND_VZ"), + param_value: 0.8, + ..set + }); + apply_tuning(&store, &mut core); + assert_eq!(core.landing_descent(), 0.8); + + // Keep flying on the new tuning: still sane after 500 more cycles. + for _ in 0..500 { + apply_tuning(&store, &mut core); + core.step(&mut plant); + } + let est = core.state(); + assert!(est.p.iter().all(|v| v.is_finite()), "flight stays finite"); + } +} + #[cfg(test)] mod tests { use super::*; diff --git a/crates/relay-mavlink/plain/src/lib.rs b/crates/relay-mavlink/plain/src/lib.rs index 9015768..2d3cefb 100644 --- a/crates/relay-mavlink/plain/src/lib.rs +++ b/crates/relay-mavlink/plain/src/lib.rs @@ -32,6 +32,8 @@ pub mod global_position_int; pub mod heartbeat; pub mod mission; pub mod param; +pub mod telemetry; +pub mod telemetry_sched; pub use command_long::{ COMMAND_LONG_CRC_EXTRA, COMMAND_LONG_MSG_ID, COMMAND_LONG_PAYLOAD_LEN, CommandLong, diff --git a/crates/relay-mavlink/plain/src/telemetry.rs b/crates/relay-mavlink/plain/src/telemetry.rs new file mode 100644 index 0000000..5ce913f --- /dev/null +++ b/crates/relay-mavlink/plain/src/telemetry.rs @@ -0,0 +1,368 @@ +//! MAVLink TELEMETRY encoders (MAVLINK-P06, v1.119) — the operator stream. +//! +//! Six encode-only messages the falcon streams to the GCS over the SiK +//! radio: ATTITUDE, SYS_STATUS, GPS_RAW_INT, SERVO_OUTPUT_RAW, VFR_HUD and +//! STATUSTEXT. Every payload layout and CRC_EXTRA below is pinned against +//! **pymavlink reference vectors** (scripts/gen-mavlink-telemetry-vectors.py) +//! in the conformance tests — the external-oracle discipline the DroneCAN +//! bit-order bug taught: self-round-trips prove robustness, only the +//! reference implementation proves CONFORMANCE. MAVLink2 truncates trailing +//! zero payload bytes ON THE WIRE; these encoders emit the full declared +//! payload and the frame layer owns truncation, so the vectors here are the +//! canonical fixed-length payloads (pymavlink's `unpacker.size`). + +// ── ATTITUDE (30) ──────────────────────────────────────────────────────────── + +pub const ATTITUDE_MSG_ID: u32 = 30; +/// ATTITUDE CRC_EXTRA (pymavlink reference). +pub const ATTITUDE_CRC_EXTRA: u8 = 39; +pub const ATTITUDE_PAYLOAD_LEN: usize = 28; + +/// Attitude + body rates (rad, rad/s), the 10 Hz operator-attitude stream. +#[derive(Clone, Copy, Debug, PartialEq)] +pub struct Attitude { + pub time_boot_ms: u32, + pub roll: f32, + pub pitch: f32, + pub yaw: f32, + pub rollspeed: f32, + pub pitchspeed: f32, + pub yawspeed: f32, +} + +impl Attitude { + pub fn encode_payload(&self) -> [u8; ATTITUDE_PAYLOAD_LEN] { + let mut out = [0u8; ATTITUDE_PAYLOAD_LEN]; + out[0..4].copy_from_slice(&self.time_boot_ms.to_le_bytes()); + out[4..8].copy_from_slice(&self.roll.to_le_bytes()); + out[8..12].copy_from_slice(&self.pitch.to_le_bytes()); + out[12..16].copy_from_slice(&self.yaw.to_le_bytes()); + out[16..20].copy_from_slice(&self.rollspeed.to_le_bytes()); + out[20..24].copy_from_slice(&self.pitchspeed.to_le_bytes()); + out[24..28].copy_from_slice(&self.yawspeed.to_le_bytes()); + out + } +} + +// ── SYS_STATUS (1) ─────────────────────────────────────────────────────────── + +pub const SYS_STATUS_MSG_ID: u32 = 1; +/// SYS_STATUS CRC_EXTRA (pymavlink reference). +pub const SYS_STATUS_CRC_EXTRA: u8 = 124; +pub const SYS_STATUS_PAYLOAD_LEN: usize = 31; + +/// System health + battery for the 2 Hz status stream. Wire order is +/// size-descending per MAVLink: the three u32 masks, then the u16 block, +/// then the i8 remaining. +#[derive(Clone, Copy, Debug, PartialEq)] +pub struct SysStatus { + pub sensors_present: u32, + pub sensors_enabled: u32, + pub sensors_health: u32, + /// Main-loop load, 0..1000 (‰). + pub load: u16, + /// Battery voltage (mV). + pub voltage_battery_mv: u16, + /// Battery current (10 mA units); -1 = unknown. + pub current_battery_10ma: i16, + pub drop_rate_comm: u16, + pub errors_comm: u16, + pub errors_count1: u16, + pub errors_count2: u16, + pub errors_count3: u16, + pub errors_count4: u16, + /// Remaining battery (%); -1 = unknown. + pub battery_remaining_pct: i8, +} + +impl SysStatus { + pub fn encode_payload(&self) -> [u8; SYS_STATUS_PAYLOAD_LEN] { + let mut out = [0u8; SYS_STATUS_PAYLOAD_LEN]; + out[0..4].copy_from_slice(&self.sensors_present.to_le_bytes()); + out[4..8].copy_from_slice(&self.sensors_enabled.to_le_bytes()); + out[8..12].copy_from_slice(&self.sensors_health.to_le_bytes()); + out[12..14].copy_from_slice(&self.load.to_le_bytes()); + out[14..16].copy_from_slice(&self.voltage_battery_mv.to_le_bytes()); + out[16..18].copy_from_slice(&self.current_battery_10ma.to_le_bytes()); + out[18..20].copy_from_slice(&self.drop_rate_comm.to_le_bytes()); + out[20..22].copy_from_slice(&self.errors_comm.to_le_bytes()); + out[22..24].copy_from_slice(&self.errors_count1.to_le_bytes()); + out[24..26].copy_from_slice(&self.errors_count2.to_le_bytes()); + out[26..28].copy_from_slice(&self.errors_count3.to_le_bytes()); + out[28..30].copy_from_slice(&self.errors_count4.to_le_bytes()); + out[30] = self.battery_remaining_pct as u8; + out + } +} + +// ── GPS_RAW_INT (24) ───────────────────────────────────────────────────────── + +pub const GPS_RAW_INT_MSG_ID: u32 = 24; +/// GPS_RAW_INT CRC_EXTRA (pymavlink reference). +pub const GPS_RAW_INT_CRC_EXTRA: u8 = 24; +/// Full MAVLink2 payload incl. extension fields (alt_ellipsoid…yaw). +pub const GPS_RAW_INT_PAYLOAD_LEN: usize = 52; + +/// Raw GNSS for the 2 Hz stream. Extension fields (h/v/vel/hdg accuracy, +/// ellipsoid alt, GPS yaw) are emitted as 0 = unknown. +#[derive(Clone, Copy, Debug, PartialEq)] +pub struct GpsRawInt { + pub time_usec: u64, + pub lat_e7: i32, + pub lon_e7: i32, + /// MSL altitude (mm). + pub alt_mm: i32, + pub eph_cm: u16, + pub epv_cm: u16, + /// Ground speed (cm/s); u16::MAX = unknown. + pub vel_cms: u16, + /// Course over ground (cdeg); u16::MAX = unknown. + pub cog_cdeg: u16, + /// 0-1 = no fix, 2 = 2D, 3 = 3D, 4 = DGPS, 5/6 = RTK. + pub fix_type: u8, + pub satellites_visible: u8, +} + +impl GpsRawInt { + pub fn encode_payload(&self) -> [u8; GPS_RAW_INT_PAYLOAD_LEN] { + let mut out = [0u8; GPS_RAW_INT_PAYLOAD_LEN]; + out[0..8].copy_from_slice(&self.time_usec.to_le_bytes()); + out[8..12].copy_from_slice(&self.lat_e7.to_le_bytes()); + out[12..16].copy_from_slice(&self.lon_e7.to_le_bytes()); + out[16..20].copy_from_slice(&self.alt_mm.to_le_bytes()); + out[20..22].copy_from_slice(&self.eph_cm.to_le_bytes()); + out[22..24].copy_from_slice(&self.epv_cm.to_le_bytes()); + out[24..26].copy_from_slice(&self.vel_cms.to_le_bytes()); + out[26..28].copy_from_slice(&self.cog_cdeg.to_le_bytes()); + out[28] = self.fix_type; + out[29] = self.satellites_visible; + // bytes 30..52: MAVLink2 extension fields, all 0 = unknown. + out + } +} + +// ── SERVO_OUTPUT_RAW (36) ──────────────────────────────────────────────────── + +pub const SERVO_OUTPUT_RAW_MSG_ID: u32 = 36; +/// SERVO_OUTPUT_RAW CRC_EXTRA (pymavlink reference). +pub const SERVO_OUTPUT_RAW_CRC_EXTRA: u8 = 222; +/// Full MAVLink2 payload incl. servo9..16 extension block. +pub const SERVO_OUTPUT_RAW_PAYLOAD_LEN: usize = 37; + +/// Actuator outputs for the 2 Hz stream: the quad's four motors as +/// servo1..4 (µs), servo5..16 zero. +#[derive(Clone, Copy, Debug, PartialEq)] +pub struct ServoOutputRaw { + /// Timestamp (µs); the wire field is u32 — truncated by the encoder. + pub time_usec: u64, + pub port: u8, + pub servo_us: [u16; 4], +} + +impl ServoOutputRaw { + pub fn encode_payload(&self) -> [u8; SERVO_OUTPUT_RAW_PAYLOAD_LEN] { + let mut out = [0u8; SERVO_OUTPUT_RAW_PAYLOAD_LEN]; + out[0..4].copy_from_slice(&(self.time_usec as u32).to_le_bytes()); + for (i, s) in self.servo_us.iter().enumerate() { + out[4 + i * 2..6 + i * 2].copy_from_slice(&s.to_le_bytes()); + } + // servo5..8 (bytes 12..20) zero. + out[20] = self.port; + // servo9..16 extension block (bytes 21..37) zero. + out + } +} + +// ── VFR_HUD (74) ───────────────────────────────────────────────────────────── + +pub const VFR_HUD_MSG_ID: u32 = 74; +/// VFR_HUD CRC_EXTRA (pymavlink reference). +pub const VFR_HUD_CRC_EXTRA: u8 = 20; +pub const VFR_HUD_PAYLOAD_LEN: usize = 20; + +/// The HUD strip: speeds (m/s), MSL altitude (m), climb (m/s), heading +/// (deg 0..360), throttle (%). +#[derive(Clone, Copy, Debug, PartialEq)] +pub struct VfrHud { + pub airspeed: f32, + pub groundspeed: f32, + pub alt_m: f32, + pub climb: f32, + pub heading_deg: i16, + pub throttle_pct: u16, +} + +impl VfrHud { + pub fn encode_payload(&self) -> [u8; VFR_HUD_PAYLOAD_LEN] { + let mut out = [0u8; VFR_HUD_PAYLOAD_LEN]; + out[0..4].copy_from_slice(&self.airspeed.to_le_bytes()); + out[4..8].copy_from_slice(&self.groundspeed.to_le_bytes()); + out[8..12].copy_from_slice(&self.alt_m.to_le_bytes()); + out[12..16].copy_from_slice(&self.climb.to_le_bytes()); + out[16..18].copy_from_slice(&self.heading_deg.to_le_bytes()); + out[18..20].copy_from_slice(&self.throttle_pct.to_le_bytes()); + out + } +} + +// ── STATUSTEXT (253) ───────────────────────────────────────────────────────── + +pub const STATUSTEXT_MSG_ID: u32 = 253; +/// STATUSTEXT CRC_EXTRA (pymavlink reference). +pub const STATUSTEXT_CRC_EXTRA: u8 = 83; +/// Full MAVLink2 payload incl. id/chunk_seq extension. +pub const STATUSTEXT_PAYLOAD_LEN: usize = 54; + +/// MAV_SEVERITY values (subset falcon emits). +pub const SEVERITY_CRITICAL: u8 = 2; +pub const SEVERITY_WARNING: u8 = 4; +pub const SEVERITY_INFO: u8 = 6; + +/// Operator event text (failsafes, mode changes, pre-arm reasons). Text is +/// NUL-padded/truncated to 50 bytes; multi-chunk texts are out of scope. +#[derive(Clone, Copy, Debug, PartialEq)] +pub struct StatusText { + pub severity: u8, + pub text: [u8; 50], +} + +impl StatusText { + /// Build from a str (truncated to 50 bytes on a char boundary-agnostic + /// byte cut — operator strings here are ASCII). + pub fn new(severity: u8, msg: &str) -> StatusText { + let mut text = [0u8; 50]; + let b = msg.as_bytes(); + let n = if b.len() < 50 { b.len() } else { 50 }; + text[..n].copy_from_slice(&b[..n]); + StatusText { severity, text } + } + + pub fn encode_payload(&self) -> [u8; STATUSTEXT_PAYLOAD_LEN] { + let mut out = [0u8; STATUSTEXT_PAYLOAD_LEN]; + out[0] = self.severity; + out[1..51].copy_from_slice(&self.text); + // id (u16) + chunk_seq (u8) extension = 0 (single-chunk). + out + } +} + +#[cfg(test)] +mod conformance { + //! pymavlink reference vectors (scripts/gen-mavlink-telemetry-vectors.py, + //! pymavlink 2.4.49). The encoder must reproduce the hex EXACTLY. + use super::*; + + fn hex(payload: &[u8]) -> impl core::fmt::Display + '_ { + struct H<'a>(&'a [u8]); + impl core::fmt::Display for H<'_> { + fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result { + for b in self.0 { + write!(f, "{b:02x}")?; + } + Ok(()) + } + } + H(payload) + } + + fn assert_hex(actual: &[u8], expected: &str) { + extern crate std; + assert_eq!(std::format!("{}", hex(actual)), expected); + } + + #[test] + fn attitude_matches_pymavlink() { + let m = Attitude { + time_boot_ms: 123456, + roll: 0.1, + pitch: -0.05, + #[allow(clippy::approx_constant)] // pymavlink vector pinned at 1.5708 exactly + yaw: 1.5708, + rollspeed: 0.01, + pitchspeed: -0.02, + yawspeed: 0.5, + }; + assert_hex( + &m.encode_payload(), + "40e20100cdcccc3dcdcc4cbdf90fc93f0ad7233c0ad7a3bc0000003f", + ); + } + + #[test] + fn sys_status_matches_pymavlink() { + let m = SysStatus { + sensors_present: 0x3F, + sensors_enabled: 0x3F, + sensors_health: 0x3F, + load: 250, + voltage_battery_mv: 15400, + current_battery_10ma: 1250, + drop_rate_comm: 0, + errors_comm: 0, + errors_count1: 0, + errors_count2: 0, + errors_count3: 0, + errors_count4: 0, + battery_remaining_pct: 87, + }; + assert_hex( + &m.encode_payload(), + "3f0000003f0000003f000000fa00283ce20400000000000000000000000057", + ); + } + + #[test] + fn gps_raw_int_matches_pymavlink() { + let m = GpsRawInt { + time_usec: 1234567890, + lat_e7: 473977000, + lon_e7: 85456000, + alt_mm: 488000, + eph_cm: 120, + epv_cm: 180, + vel_cms: 250, + cog_cdeg: 9000, + fix_type: 3, + satellites_visible: 14, + }; + assert_hex( + &m.encode_payload(), + "d202964900000000a850401c80f41705407207007800b400fa002823030e00000000000000000000000000000000000000000000", + ); + } + + #[test] + fn servo_output_raw_matches_pymavlink() { + let m = ServoOutputRaw { + time_usec: 1234567890, + port: 0, + servo_us: [1500, 1520, 1480, 1510], + }; + assert_hex( + &m.encode_payload(), + "d2029649dc05f005c805e60500000000000000000000000000000000000000000000000000", + ); + } + + #[test] + fn vfr_hud_matches_pymavlink() { + let m = VfrHud { + airspeed: 0.0, + groundspeed: 2.5, + alt_m: 2.0, + climb: -0.5, + heading_deg: 90, + throttle_pct: 58, + }; + assert_hex(&m.encode_payload(), "000000000000204000000040000000bf5a003a00"); + } + + #[test] + fn statustext_matches_pymavlink() { + let m = StatusText::new(SEVERITY_CRITICAL, "ROTOR 0 OUT: LANDING"); + assert_hex( + &m.encode_payload(), + "02524f544f522030204f55543a204c414e44494e47000000000000000000000000000000000000000000000000000000000000000000", + ); + } +} diff --git a/crates/relay-mavlink/plain/src/telemetry_sched.rs b/crates/relay-mavlink/plain/src/telemetry_sched.rs new file mode 100644 index 0000000..cccd68d --- /dev/null +++ b/crates/relay-mavlink/plain/src/telemetry_sched.rs @@ -0,0 +1,262 @@ +//! Telemetry STREAM SCHEDULER (MAVLINK-P06, v1.119) — rate + priority + +//! byte-budget arbitration for the GCS link. +//! +//! The SiK 433 MHz radio carries ~57.6 kbit/s ≈ 7200 bytes/s; the telemetry +//! set must fit with measured headroom, and under a DEGRADED link (half +//! budget or worse) the CRITICAL class — HEARTBEAT and STATUSTEXT — must +//! never be starved: a GCS that loses heartbeat declares the vehicle lost, +//! and a failsafe event that never reaches the operator is an invisible +//! emergency. NORMAL streams degrade gracefully instead (a due stream that +//! does not fit stays due and sends when budget allows). +//! +//! Pure, `no_std`, fixed-capacity, total: the scheduler never panics and +//! never emits more bytes per tick than the budget. + +/// Stream priority class. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum Priority { + /// Never starved: emitted whenever due, before any Normal stream. + /// The build-time invariant [`TelemetryScheduler::critical_fits`] must + /// hold (the sum of all critical frame sizes fits the per-tick budget). + Critical, + /// Best-effort at its rate; degrades under link pressure (stays due). + Normal, +} + +/// One periodic stream slot. +#[derive(Clone, Copy, Debug)] +pub struct StreamSlot { + /// Emit every `interval_ticks` scheduler ticks (0 ⇒ disabled). + pub interval_ticks: u32, + /// Full on-wire frame size (header + full payload + crc), bytes. + pub frame_bytes: usize, + pub priority: Priority, +} + +/// Fixed-capacity scheduler over `N` streams. Call [`tick`](Self::tick) once +/// per scheduler period with the byte budget for that period; it returns a +/// bitmask of stream indices to emit NOW. +pub struct TelemetryScheduler { + slots: [StreamSlot; N], + countdown: [u32; N], + /// Ticks each stream has spent DUE-but-deferred (fairness age): the + /// most-starved due stream gets first claim on the remaining budget, so + /// sustained pressure degrades every normal stream proportionally + /// instead of silently starving whichever sorts last. + age: [u32; N], + /// Normal-stream emissions deferred by budget pressure (loud counter). + pub deferred: u32, +} + +impl TelemetryScheduler { + pub fn new(slots: [StreamSlot; N]) -> Self { + let mut countdown = [0u32; N]; + for (c, s) in countdown.iter_mut().zip(slots.iter()) { + *c = s.interval_ticks; // stagger-free start; first emit after one interval + } + TelemetryScheduler { slots, countdown, age: [0; N], deferred: 0 } + } + + /// The no-starvation precondition: every critical frame fits the budget + /// TOGETHER. Check at integration time; `tick` upholds the guarantee + /// whenever this holds. + pub fn critical_fits(&self, budget_bytes: usize) -> bool { + let mut sum = 0usize; + for s in self.slots.iter() { + if s.priority == Priority::Critical && s.interval_ticks != 0 { + sum = sum.saturating_add(s.frame_bytes); + } + } + sum <= budget_bytes + } + + /// Advance one period with `budget_bytes` available; returns a bitmask of + /// streams to emit. Criticals due are ALWAYS in the mask (budget is + /// consumed first-priority); normals fit-or-stay-due (deferred counted). + pub fn tick(&mut self, budget_bytes: usize) -> u32 { + let mut mask = 0u32; + let mut left = budget_bytes; + // Criticals first — unconditionally emitted when due (the caller + // guarantees critical_fits; even if violated, we still emit and + // saturate rather than starve the heartbeat). + for i in 0..N.min(32) { + let s = self.slots[i]; + if s.interval_ticks == 0 || s.priority != Priority::Critical { + continue; + } + if self.countdown[i] <= 1 { + mask |= 1 << i; + self.countdown[i] = s.interval_ticks; + left = left.saturating_sub(s.frame_bytes); + } else { + self.countdown[i] -= 1; + } + } + // Normals, FAIRLY: repeatedly pick the due stream with the highest + // deferral age that FITS the remaining budget (age breaks toward the + // most-starved, so sustained pressure degrades proportionally — an + // index-ordered scan starved the tail streams, caught by test). + let mut due = [false; N]; + for (i, d) in due.iter_mut().enumerate().take(32) { + let s = self.slots[i]; + if s.interval_ticks == 0 || s.priority != Priority::Normal { + continue; + } + if self.countdown[i] <= 1 { + *d = true; + } else { + self.countdown[i] -= 1; + } + } + loop { + let mut best: Option = None; + for (i, d) in due.iter().enumerate().take(32) { + if !*d || self.slots[i].frame_bytes > left { + continue; + } + match best { + Some(b) if self.age[b] >= self.age[i] => {} + _ => best = Some(i), + } + } + let Some(i) = best else { break }; + due[i] = false; + mask |= 1 << i; + self.countdown[i] = self.slots[i].interval_ticks; + self.age[i] = 0; + left -= self.slots[i].frame_bytes; + } + // Whatever is still due did not fit: defer loudly, age for fairness. + for (i, d) in due.iter().enumerate().take(32) { + if *d { + self.deferred = self.deferred.saturating_add(1); + self.age[i] = self.age[i].saturating_add(1); + self.countdown[i] = 1; // stays due + } + } + mask + } +} + +#[cfg(test)] +mod tests { + use super::*; + + // The v1.119 falcon set at a 10 Hz scheduler tick (budget per tick = + // link bytes/s ÷ 10). Frame = 12 B MAVLink2 overhead + full payload. + const HB: usize = 0; // HEARTBEAT 1 Hz, critical (21 B) + const ST: usize = 1; // STATUSTEXT event slot, critical (66 B) + const ATT: usize = 2; // ATTITUDE 10 Hz (40 B) + const GPOS: usize = 3; // GLOBAL_POSITION_INT 5 Hz (40 B) + const VFR: usize = 4; // VFR_HUD 5 Hz (32 B) + const SYS: usize = 5; // SYS_STATUS 2 Hz (43 B) + const GPS: usize = 6; // GPS_RAW_INT 2 Hz (64 B) + const SRV: usize = 7; // SERVO_OUTPUT_RAW 2 Hz (49 B) + + fn falcon_set() -> TelemetryScheduler<8> { + TelemetryScheduler::new([ + StreamSlot { interval_ticks: 10, frame_bytes: 21, priority: Priority::Critical }, + StreamSlot { interval_ticks: 10, frame_bytes: 66, priority: Priority::Critical }, + StreamSlot { interval_ticks: 1, frame_bytes: 40, priority: Priority::Normal }, + StreamSlot { interval_ticks: 2, frame_bytes: 40, priority: Priority::Normal }, + StreamSlot { interval_ticks: 2, frame_bytes: 32, priority: Priority::Normal }, + StreamSlot { interval_ticks: 5, frame_bytes: 43, priority: Priority::Normal }, + StreamSlot { interval_ticks: 5, frame_bytes: 64, priority: Priority::Normal }, + StreamSlot { interval_ticks: 5, frame_bytes: 49, priority: Priority::Normal }, + ]) + } + + /// MAVLINK-P06 rate budget: at the SiK link (7200 B/s ⇒ 720 B per 10 Hz + /// tick) the WHOLE set meets its rates with ≥ 20% headroom — measured + /// over 30 s, not asserted from arithmetic. + #[test] + fn full_set_fits_sik_budget_with_headroom() { + let mut sched = falcon_set(); + let budget = 720usize; + assert!(sched.critical_fits(budget)); + let mut counts = [0u32; 8]; + let mut bytes_total = 0usize; + for _ in 0..300 { + let mask = sched.tick(budget); + for (i, c) in counts.iter_mut().enumerate() { + if mask & (1 << i) != 0 { + *c += 1; + bytes_total += sched.slots[i].frame_bytes; + } + } + } + assert_eq!(sched.deferred, 0, "nothing defers at full budget"); + assert_eq!(counts[HB], 30, "HEARTBEAT 1 Hz"); + assert_eq!(counts[ATT], 300, "ATTITUDE 10 Hz"); + assert_eq!(counts[GPOS], 150, "GPOS 5 Hz"); + assert_eq!(counts[VFR], 150, "VFR 5 Hz"); + assert_eq!(counts[SYS], 60, "SYS_STATUS 2 Hz"); + assert_eq!(counts[GPS], 60, "GPS_RAW 2 Hz"); + assert_eq!(counts[SRV], 60, "SERVO 2 Hz"); + // Headroom: measured bytes over 30 s vs the link capacity. + let capacity = 7200usize * 30; + let used_frac = bytes_total as f32 / capacity as f32; + assert!( + used_frac <= 0.80, + "set must leave >=20% headroom: used {:.0}%", + used_frac * 100.0 + ); + } + + /// The no-starvation precondition is a checkable boundary: the critical + /// set (HEARTBEAT 21 + STATUSTEXT 66 = 87 B) fits budgets >= 87 only. + #[test] + fn critical_fits_is_the_precise_boundary() { + let sched = falcon_set(); + assert!(!sched.critical_fits(60)); + assert!(!sched.critical_fits(86)); + assert!(sched.critical_fits(87)); + assert!(sched.critical_fits(720)); + } + + /// Even when critical_fits is violated (extreme link collapse), criticals + /// are STILL emitted (saturating past budget) rather than starved. + #[test] + fn criticals_emit_even_past_budget() { + let mut sched = falcon_set(); + let budget = 30usize; // < HB+ST + let mut hb = 0; + let mut st = 0; + for _ in 0..100 { + let mask = sched.tick(budget); + if mask & (1 << HB) != 0 { + hb += 1; + } + if mask & (1 << ST) != 0 { + st += 1; + } + } + assert_eq!(hb, 10, "HEARTBEAT held its 1 Hz rate at collapse budget"); + assert_eq!(st, 10, "STATUSTEXT slot held rate at collapse budget"); + assert!(sched.deferred > 0, "normals deferred loudly"); + } + + /// Degraded-but-workable link: normals degrade, criticals exact. + #[test] + fn degraded_link_criticals_exact_normals_degrade() { + let mut sched = falcon_set(); + let budget = 100usize; // fits criticals (87) + a little + let mut counts = [0u32; 8]; + for _ in 0..300 { + let mask = sched.tick(budget); + for (i, c) in counts.iter_mut().enumerate() { + if mask & (1 << i) != 0 { + *c += 1; + } + } + } + assert_eq!(counts[HB], 30, "HEARTBEAT exact under pressure"); + assert_eq!(counts[ST], 30, "STATUSTEXT exact under pressure"); + assert!(counts[ATT] < 300, "ATTITUDE degraded (got {})", counts[ATT]); + assert!(sched.deferred > 0); + // Deferral must not deadlock: every normal stream still progresses. + for (i, c) in counts.iter().enumerate() { + assert!(*c > 0, "stream {i} fully starved"); + } + } +} diff --git a/scripts/gen-mavlink-telemetry-vectors.py b/scripts/gen-mavlink-telemetry-vectors.py new file mode 100644 index 0000000..b50c0c7 --- /dev/null +++ b/scripts/gen-mavlink-telemetry-vectors.py @@ -0,0 +1,63 @@ +#!/usr/bin/env python3 +"""Authoritative MAVLink TELEMETRY reference vectors for relay-mavlink (v1.119). + +Same discipline as gen-mavlink-param-vectors.py (the external-oracle rule that +caught the DroneCAN bit-order bug): pymavlink — the reference implementation — +produces the canonical payload bytes + CRC_EXTRA for the six messages the +MAVLINK-P06 telemetry stream emits: + + SYS_STATUS (1), GPS_RAW_INT (24), ATTITUDE (30), SERVO_OUTPUT_RAW (36), + VFR_HUD (74), STATUSTEXT (253) + +The relay-mavlink ENCODERS must reproduce these hex payloads from the field +values; the CRC_EXTRA constants must come from here, never from memory. + +Run: python3 scripts/gen-mavlink-telemetry-vectors.py +""" +from pymavlink.dialects.v20 import common as m + + +def payload_hex(msg): + mav = m.MAVLink(None, srcSystem=1, srcComponent=1) + mav.seq = 0 + packed = msg.pack(mav) + payload = packed[10:-2] # strip MAVLink2 header (10) + checksum (2) + size = msg.unpacker.size + payload = payload + b"\x00" * (size - len(payload)) # re-inflate truncation + return payload.hex() + + +def show(name, msg): + print(f"== {name} id={msg.id} crc_extra={msg.crc_extra} len={msg.unpacker.size}") + print(f" payload={payload_hex(msg)}") + for f in msg.fieldnames: + print(f" {f} = {getattr(msg, f)}") + print() + + +show("ATTITUDE", m.MAVLink_attitude_message( + time_boot_ms=123456, roll=0.1, pitch=-0.05, yaw=1.5708, + rollspeed=0.01, pitchspeed=-0.02, yawspeed=0.5)) + +show("SYS_STATUS", m.MAVLink_sys_status_message( + onboard_control_sensors_present=0x3F, onboard_control_sensors_enabled=0x3F, + onboard_control_sensors_health=0x3F, load=250, voltage_battery=15400, + current_battery=1250, battery_remaining=87, drop_rate_comm=0, + errors_comm=0, errors_count1=0, errors_count2=0, errors_count3=0, + errors_count4=0)) + +show("GPS_RAW_INT", m.MAVLink_gps_raw_int_message( + time_usec=1234567890, fix_type=3, lat=473977000, lon=85456000, + alt=488000, eph=120, epv=180, vel=250, cog=9000, satellites_visible=14)) + +show("SERVO_OUTPUT_RAW", m.MAVLink_servo_output_raw_message( + time_usec=1234567890, port=0, + servo1_raw=1500, servo2_raw=1520, servo3_raw=1480, servo4_raw=1510, + servo5_raw=0, servo6_raw=0, servo7_raw=0, servo8_raw=0)) + +show("VFR_HUD", m.MAVLink_vfr_hud_message( + airspeed=0.0, groundspeed=2.5, heading=90, throttle=58, + alt=2.0, climb=-0.5)) + +show("STATUSTEXT", m.MAVLink_statustext_message( + severity=2, text=b"ROTOR 0 OUT: LANDING", id=0, chunk_seq=0)) From f9e42b84c374dd243f1bf4aef53bc14eb2204255 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 15 Jul 2026 20:05:28 +0200 Subject: [PATCH 2/4] verify(relay-mavlink): Kani MAV-K01..K03 + matrix enrollment MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The telemetry scheduler's arbitration invariants, proven over ALL slot configurations and budgets at N=4 (8.4 s locally, 539 checks): - MAV-K01: tick() is total; mask bits only name enabled slots below N. - MAV-K02: the NORMAL class never exceeds the per-tick byte budget. - MAV-K03: a due Critical stream is ALWAYS in the mask (never starved), including at budget zero. Also corrects a module-doc over-claim ("never emits more bytes than the budget" — criticals saturate PAST budget by design rather than starve) and enrolls relay-mavlink in the kani.yml matrix — the crate was Kani-orphaned since v1.96 (harness without matrix = unenforced; the recurring-orphan lesson). Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG --- .github/workflows/kani.yml | 1 + crates/relay-mavlink/plain/src/kani_proofs.rs | 84 +++++++++++++++++++ crates/relay-mavlink/plain/src/lib.rs | 3 + .../plain/src/telemetry_sched.rs | 6 +- 4 files changed, 92 insertions(+), 2 deletions(-) create mode 100644 crates/relay-mavlink/plain/src/kani_proofs.rs diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 81998b8..e9d523a 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -61,6 +61,7 @@ jobs: - relay-calib - relay-fsafe - relay-mix-quad + - relay-mavlink # Flight-critical control + estimator proofs. These harnesses were # authored alongside the engines but never added to this matrix, so # CI never ran them (the same orphaned-proof gap that bit relay-rc diff --git a/crates/relay-mavlink/plain/src/kani_proofs.rs b/crates/relay-mavlink/plain/src/kani_proofs.rs new file mode 100644 index 0000000..741de3e --- /dev/null +++ b/crates/relay-mavlink/plain/src/kani_proofs.rs @@ -0,0 +1,84 @@ +//! Kani harnesses for relay-mavlink (plain-only sibling). +//! +//! The verification split (the codebase pattern): the telemetry SCHEDULER's +//! arbitration logic — totality, budget conservation for the normal class, +//! and the critical-class no-starvation guarantee — is proven here over ALL +//! slot configurations and budgets at N=4. The wire ENCODERS are +//! conformance-gated against external pymavlink reference vectors instead +//! (encoding correctness is a spec-agreement question, not an invariant +//! Kani can state — the DroneCAN bit-order lesson). +#![cfg(kani)] + +use crate::telemetry_sched::{Priority, StreamSlot, TelemetryScheduler}; + +fn any_slot() -> StreamSlot { + let interval: u32 = kani::any(); + kani::assume(interval <= 8); + let frame: usize = kani::any(); + kani::assume(frame <= 1024); + let critical: bool = kani::any(); + StreamSlot { + interval_ticks: interval, + frame_bytes: frame, + priority: if critical { Priority::Critical } else { Priority::Normal }, + } +} + +/// MAV-K01 — `tick` is TOTAL and the mask is well-formed: for ANY four-slot +/// configuration and ANY budget, no panic, and every set mask bit names an +/// ENABLED slot (interval != 0) at an index < N. +#[kani::proof] +#[kani::unwind(8)] +fn verify_tick_total_mask_well_formed() { + let slots = [any_slot(), any_slot(), any_slot(), any_slot()]; + let mut sched = TelemetryScheduler::new(slots); + let budget: usize = kani::any(); + let mask = sched.tick(budget); + assert!(mask < (1 << 4), "no bit at or above N"); + for i in 0..4 { + if mask & (1 << i) != 0 { + assert!(slots[i].interval_ticks != 0, "disabled slot never emitted"); + } + } +} + +/// MAV-K02 — NORMAL-class budget conservation: the bytes of all Normal +/// streams emitted in one tick never exceed the budget (criticals may +/// saturate past it BY DESIGN — the heartbeat is never starved — which is +/// why the conserved quantity is the normal class, not the whole mask). +#[kani::proof] +#[kani::unwind(8)] +fn verify_normals_never_exceed_budget() { + let slots = [any_slot(), any_slot(), any_slot(), any_slot()]; + let mut sched = TelemetryScheduler::new(slots); + let budget: usize = kani::any(); + kani::assume(budget <= 1 << 20); + let mask = sched.tick(budget); + let mut normal_bytes = 0usize; + for i in 0..4 { + if mask & (1 << i) != 0 && slots[i].priority == Priority::Normal { + normal_bytes += slots[i].frame_bytes; + } + } + assert!(normal_bytes <= budget, "normal emissions fit the budget"); +} + +/// MAV-K03 — the critical class is NEVER starved: for ANY configuration and +/// ANY budget (including zero), every enabled Critical slot that is due this +/// tick is in the mask. +#[kani::proof] +#[kani::unwind(8)] +fn verify_criticals_never_starved() { + let slots = [any_slot(), any_slot(), any_slot(), any_slot()]; + // Due-this-tick = countdown reaches <= 1; after new(), a slot with + // interval 1 is due on the first tick. + let mut sched = TelemetryScheduler::new(slots); + let budget: usize = kani::any(); + let mask = sched.tick(budget); + for i in 0..4 { + let s = slots[i]; + if s.priority == Priority::Critical && s.interval_ticks == 1 { + assert!(mask & (1 << i) != 0, "due critical always emitted"); + } + } +} diff --git a/crates/relay-mavlink/plain/src/lib.rs b/crates/relay-mavlink/plain/src/lib.rs index 2d3cefb..f7599b6 100644 --- a/crates/relay-mavlink/plain/src/lib.rs +++ b/crates/relay-mavlink/plain/src/lib.rs @@ -35,6 +35,9 @@ pub mod param; pub mod telemetry; pub mod telemetry_sched; +#[cfg(kani)] +mod kani_proofs; + pub use command_long::{ COMMAND_LONG_CRC_EXTRA, COMMAND_LONG_MSG_ID, COMMAND_LONG_PAYLOAD_LEN, CommandLong, MAV_CMD_COMPONENT_ARM_DISARM, MAV_CMD_DO_FLIGHTTERMINATION, MAV_CMD_MISSION_START, diff --git a/crates/relay-mavlink/plain/src/telemetry_sched.rs b/crates/relay-mavlink/plain/src/telemetry_sched.rs index cccd68d..9dd8a2b 100644 --- a/crates/relay-mavlink/plain/src/telemetry_sched.rs +++ b/crates/relay-mavlink/plain/src/telemetry_sched.rs @@ -9,8 +9,10 @@ //! emergency. NORMAL streams degrade gracefully instead (a due stream that //! does not fit stays due and sends when budget allows). //! -//! Pure, `no_std`, fixed-capacity, total: the scheduler never panics and -//! never emits more bytes per tick than the budget. +//! Pure, `no_std`, fixed-capacity, total: the scheduler never panics, the +//! NORMAL class never exceeds the per-tick budget, and criticals saturate +//! PAST the budget rather than starve when `critical_fits` is violated +//! (proven in `kani_proofs.rs`: MAV-K01..K03). /// Stream priority class. #[derive(Clone, Copy, Debug, PartialEq, Eq)] From d5c2dd835a73faef527472188c915a54afc56efe Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 15 Jul 2026 20:13:33 +0200 Subject: [PATCH 3/4] fix(relay-mavlink): opt into workspace lints for cfg(kani) check-cfg MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The workspace declares check-cfg = ['cfg(kani)'] but relay-mavlink never had a [lints] workspace = true section — the new kani_proofs mod tripped unexpected_cfgs under CI's -D warnings. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG --- crates/relay-mavlink/Cargo.toml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/crates/relay-mavlink/Cargo.toml b/crates/relay-mavlink/Cargo.toml index c3cd5e7..545cf19 100644 --- a/crates/relay-mavlink/Cargo.toml +++ b/crates/relay-mavlink/Cargo.toml @@ -25,3 +25,6 @@ crate-type = ["rlib"] [dev-dependencies] proptest.workspace = true + +[lints] +workspace = true From 1861b9972d25b055033042b4646ce40fbd8c8134 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 15 Jul 2026 20:22:08 +0200 Subject: [PATCH 4/4] fix(falcon-core): clamp the altitude-gain setters (clean-room refute) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The clean-room pass refuted "every tuning setter clamps": set_altitude_gains and set_altitude_integral_gain assigned directly, so the "bounded twice over" claim held only for hover thrust and landing descent. Clamp all three gains to the tuning-schema envelope (kp [0,1], kd [0,3], ki [0,0.2]) — every existing call site is inside it. falcon-core 48 + falcon-param 8 tests green. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG --- crates/falcon-core/plain/src/lib.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/crates/falcon-core/plain/src/lib.rs b/crates/falcon-core/plain/src/lib.rs index 0ec419f..0e5b721 100644 --- a/crates/falcon-core/plain/src/lib.rs +++ b/crates/falcon-core/plain/src/lib.rs @@ -357,7 +357,7 @@ impl FlightCore { /// Set the altitude-loop integral gain (v1.22). `0` disables it (P-D only) — /// used to show the altitude offset under thrust lapse the integral removes. pub fn set_altitude_integral_gain(&mut self, ki: f32) { - self.ki_alt = ki; + self.ki_alt = ki.clamp(0.0, 0.2); self.alt_int = 0.0; } @@ -374,8 +374,8 @@ impl FlightCore { /// higher kp to hold altitude firmly and a matched kd to damp the slow /// climb/overshoot oscillation the soft loop leaves. pub fn set_altitude_gains(&mut self, kp: f32, kd: f32) { - self.kp_alt = kp; - self.kd_alt = kd; + self.kp_alt = kp.clamp(0.0, 1.0); + self.kd_alt = kd.clamp(0.0, 3.0); } /// Set the IEKF velocity/position covariance-diagonal floor (m²/s², m²)