feat(falcon): v1.119 — GCS telemetry streaming + in-flight tuning (MAVLINK-P06)

.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

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

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

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
@@ -326,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;
     }
 
@@ -343,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²)
@@ -1655,6 +1686,7 @@ impl FlightBackend for SimBackend {
 }
 
 pub mod blackbox_backend;
+pub mod tuning;
 
 #[cfg(test)]
 mod blackbox_replay_tests {

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<const N: usize>(store: &mut ParamStore<N>) -> 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<const N: usize>(store: &ParamStore<N>, core: &mut FlightCore) {
+    let g = |name: &str| store.get(&param_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);
+    }
+}

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]

crates/falcon-param/plain/src/lib.rs

@@ -113,6 +113,76 @@ pub fn on_param_request_list_item<const N: usize>(
     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::*;

crates/relay-mavlink/Cargo.toml

@@ -25,3 +25,6 @@ crate-type = ["rlib"]
 
 [dev-dependencies]
 proptest.workspace = true
+
+[lints]
+workspace = true

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");
+        }
+    }
+}

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

@@ -32,6 +32,11 @@ pub mod global_position_int;
 pub mod heartbeat;
 pub mod mission;
 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,