feat(falcon): v1.123 — float discipline: CI f64 gate + IEKF variance floor

.github/workflows/ci.yml

@@ -59,6 +59,8 @@ jobs:
       # Scope tight: only the v0.1 falcon crates. Workspace-wide
       # clippy lights up pre-existing warnings in cFS crates that
       # are out of v0.1 scope.
+      - name: Float discipline (f32 flight core; f64 only at annotated boundaries)
+        run: ./scripts/check-float-discipline.sh
       - name: Clippy on v0.1 falcon crates
         run: |
           cargo clippy -p relay-mavlink -p relay-ekf-stub -p falcon-hello \

artifacts/swdd/SWDD-FALCON-FLOAT-001.yaml

@@ -0,0 +1,58 @@
+artifacts:
+  - id: SWDD-FALCON-FLOAT-001
+    type: sw-detail-design
+    title: "Float discipline: f32 flight core, f64 only at annotated geodetic/API boundaries"
+    status: implemented
+    release: falcon-v1.123.0
+    description: >
+      DESIGN DECISION (raised by external review, 2026-07): the flight core
+      is f32 BY REQUIREMENT, not convenience. Rationale, in force order:
+      (1) HARDWARE — the estimator partition runs on the i.MX RT1176
+      Cortex-M4, whose FPv4-SP FPU has no double-precision hardware; every
+      f64 op is soft-float (order-of-magnitude slower — a WCET blow-up on
+      the hottest loop). Pinned with jess (jess#144: estimator crates
+      f64-free for M4). (2) PRACTICE — PX4 EKF2 and ArduPilot NavEKF3 fly
+      f32 filters with the same mitigations relay-iekf carries
+      (local-frame navigation + covariance hygiene). (3) VERIFICATION —
+      f32 is already at CBMC's tractability edge; f64 would render several
+      existing proof suites intractable.
+
+      f64 is REQUIRED at exactly one class of site: geodetic absolutes.
+      An f32 latitude quantizes at ~0.6 m (24-bit mantissa at mid
+      latitudes); absolute lat/lon math is f64 (falcon-mavlink NED->LLH;
+      the gz bridge's LLH->NED projection), casting only the small local
+      NED delta down to f32. Wire formats stay integer (UBX 1e-7 deg i32).
+      Test oracles deliberately use f64 (more precise than the article
+      under test).
+
+      ENFORCEMENT (this release): scripts/check-float-discipline.sh runs in
+      CI — denies the f64 token in the flight-partition crates' non-test
+      code; a file may opt out only via a visible header annotation
+      ("float-discipline: allow-f64 (<why>)"; today exactly one:
+      falcon-mavlink's geodetic boundary).
+
+      HARDENING (this release, from the same review): the relay-iekf
+      standard-form covariance update `P <- (I-KH)P` can in f32 round a
+      diagonal negative — symmetrise() cannot see that. floor_variances()
+      now runs after every measurement update: diagonals healed into
+      [VAR_FLOOR, VAR_CEIL] (an infinite diagonal heals to the CEILING —
+      maximal uncertainty — never the floor, which would fabricate
+      certainty; the Kani harness caught +infinity passing the naive
+      floor-only check), stale correlations of corrupt rows zeroed, every
+      event counted LOUDLY in Iekf::variance_floor_hits (zero across all
+      existing campaigns — a guard, not a crutch).
+    tags: [falcon, float-discipline, f32, wcet, iekf, numerical-health, v1.123]
+    fields:
+      verification-criteria: >
+        Gate: check-float-discipline.sh green in CI on every PR; seeding an
+        f64 into a flight crate fails the gate. Floor: Kani proves the
+        post-condition (every diagonal finite and within [floor, ceil] for
+        ANY input including NaN/+-inf); unit tests cover negative-diagonal
+        heal + correlation zeroing + NaN; a 50k-cycle healthy run asserts
+        ZERO floor hits (behavior-neutral on healthy inputs); the full
+        relay-iekf suite (29) and falcon-core suite are unchanged.
+    links:
+      - type: refines
+        target: SWARCH-FALCON-001
+      - type: implements
+        target: SYSREQ-FALCON-002

artifacts/swreq/SWREQ-FALCON-PART-P01.yaml

@@ -3,7 +3,7 @@ artifacts:
     type: sw-req
     title: "PART-P01 — separable estimator partition (M4) with transport-delay-robust cascade (M7)"
     status: proposed
-    release: falcon-v1.123.0
+    release: falcon-v1.124.0
     description: >
       The flight stack shall decompose into an ESTIMATOR partition and a
       CASCADE partition matching the agreed RT1176 core mapping (jess#144 /

artifacts/swreq/SWREQ-FALCON-PART-P02.yaml

@@ -3,7 +3,7 @@ artifacts:
     type: sw-req
     title: "PART-P02 — actuator-path constraints on the F100 failsafe partition (relay specifies, gale implements)"
     status: proposed
-    release: falcon-v1.123.0
+    release: falcon-v1.124.0
     description: >
       The F100 I/O-failsafe partition (gale/gust-owned per jess#144 — NOT a
       relay component) shall satisfy two constraints that relay's verified

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

@@ -1,4 +1,5 @@
 //! Falcon MAVLink bridge — the translation seam between the MAVLink v2
+//! float-discipline: allow-f64 (geodetic boundary: absolute lat/lon must be f64 — f32 degrees quantize at ~0.6 m; only local NED deltas are cast down)
 //! wire (QGroundControl / MAVSDK / PX4-ecosystem GCS) and falcon's flight
 //! supervisor.
 //!

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

@@ -224,6 +224,49 @@ fn symmetrise(p: &mut Mat) {
     }
 }
 
+/// Diagonal variance floor (v1.123, the f32-discipline audit): the
+/// measurement update is the cheap standard form `P ← (I−KH)P`, which in
+/// f32 can round a small diagonal NEGATIVE under a strong update —
+/// `symmetrise` cannot see that, and a non-positive variance corrupts
+/// every later gain. Floor each diagonal at `VAR_FLOOR` and, when a
+/// non-positive one is caught, zero its row/column correlations (they are
+/// no longer trustworthy) — the PX4-style practical mitigation, kept
+/// LOUD via the returned hit count (surfaced as `variance_floor_hits`).
+const VAR_FLOOR: f32 = 1.0e-9;
+/// Variance ceiling: an over-ceiling or +∞ diagonal is healed to MAXIMAL
+/// uncertainty, not the floor — flooring it would CLAIM certainty exactly
+/// where there is none (the Kani harness caught +∞ passing `d >= FLOOR`).
+const VAR_CEIL: f32 = 1.0e6;
+
+fn floor_variances(p: &mut Mat) -> u32 {
+    let mut hits = 0u32;
+    for i in 0..N {
+        let d = p[i][i];
+        let healthy = d.is_finite() && (VAR_FLOOR..=VAR_CEIL).contains(&d);
+        if !healthy {
+            // negative, NaN or infinite: the row/column correlations are no
+            // longer trustworthy either.
+            if !(d.is_finite() && d > 0.0) {
+                for j in 0..N {
+                    if j != i {
+                        p[i][j] = 0.0;
+                        p[j][i] = 0.0;
+                    }
+                }
+            }
+            p[i][i] = if d.is_finite() {
+                d.clamp(VAR_FLOOR, VAR_CEIL)
+            } else if d == f32::INFINITY {
+                VAR_CEIL
+            } else {
+                VAR_FLOOR // NaN / −∞: no usable information — smallest honest value
+            };
+            hits += 1;
+        }
+    }
+    hits
+}
+
 /// Write a (scaled) 3×3 block into `m` at top-left `(r0, c0)`.
 fn set_block3(m: &mut Mat, r0: usize, c0: usize, b: &[[f32; 3]; 3], scale: f32) {
     for i in 0..3 {
@@ -365,6 +408,11 @@ pub struct Iekf {
     /// campaigns are unchanged). Set via `set_process_floor`.
     q_vel_extra: f32,
     q_pos_extra: f32,
+    /// LOUD diagnostic (v1.123): how many times a covariance diagonal had
+    /// to be floored (an f32 roundoff event in the standard-form update).
+    /// Zero in every campaign to date; a nonzero value in the field is a
+    /// numerical-health signal, not routine.
+    pub variance_floor_hits: u32,
 }
 
 impl Iekf {
@@ -383,7 +431,7 @@ impl Iekf {
                 p[blk * 3 + i][blk * 3 + i] = v[blk];
             }
         }
-        Iekf { state, p, cfg, q_vel_extra: 0.0, q_pos_extra: 0.0 }
+        Iekf { state, p, cfg, q_vel_extra: 0.0, q_pos_extra: 0.0, variance_floor_hits: 0 }
     }
 
     pub fn level() -> Self {
@@ -553,6 +601,7 @@ impl Iekf {
             self.p[6 + i][6 + i] += self.q_pos_extra * dt; // δp
         }
         symmetrise(&mut self.p);
+        self.variance_floor_hits += floor_variances(&mut self.p);
     }
 
     /// Right-invariant NED **position** measurement update (e.g. GPS, or
@@ -675,6 +724,7 @@ impl Iekf {
         }
         self.p = mat_mul(&imkh, &self.p);
         symmetrise(&mut self.p);
+        self.variance_floor_hits += floor_variances(&mut self.p);
         true
     }
 
@@ -730,6 +780,7 @@ impl Iekf {
             }
         }
         symmetrise(&mut self.p);
+        self.variance_floor_hits += floor_variances(&mut self.p);
         true
     }
 
@@ -904,6 +955,7 @@ impl Iekf {
         }
         self.p = mat_mul(&imkh, &self.p);
         symmetrise(&mut self.p);
+        self.variance_floor_hits += floor_variances(&mut self.p);
         true
     }
 
@@ -1850,6 +1902,63 @@ mod tests {
     }
 }
 
+#[cfg(test)]
+mod variance_floor_tests {
+    extern crate std;
+    use super::*;
+
+    /// A negative diagonal (the f32 standard-form-update failure mode) is
+    /// floored, its stale correlations zeroed, and the event COUNTED.
+    #[test]
+    fn negative_diagonal_floored_loudly() {
+        let mut p = mat_zero();
+        for i in 0..N {
+            p[i][i] = 0.01;
+        }
+        p[4][4] = -1.0e-6; // roundoff casualty
+        p[4][7] = 5.0e-4; // stale correlation
+        p[7][4] = 5.0e-4;
+        let hits = floor_variances(&mut p);
+        assert_eq!(hits, 1);
+        assert!(p[4][4] >= VAR_FLOOR);
+        assert_eq!(p[4][7], 0.0, "stale correlation cleared");
+        assert_eq!(p[7][4], 0.0);
+        assert_eq!(p[0][0], 0.01, "healthy entries untouched");
+    }
+
+    /// NaN diagonals are healed too (totality), and a healthy matrix is a
+    /// strict no-op with zero hits.
+    #[test]
+    fn nan_healed_healthy_untouched() {
+        let mut p = mat_zero();
+        for i in 0..N {
+            p[i][i] = 0.5;
+        }
+        assert_eq!(floor_variances(&mut p), 0, "healthy P: no hits");
+        p[2][2] = f32::NAN;
+        let hits = floor_variances(&mut p);
+        assert_eq!(hits, 1);
+        assert!(p[2][2] >= VAR_FLOOR && p[2][2].is_finite());
+    }
+
+    /// Long-run health: 50k propagate+update cycles on a static vehicle —
+    /// the floor NEVER fires on healthy inputs (it is a guard, not a
+    /// crutch), and every diagonal stays at/above the floor throughout.
+    #[test]
+    fn floor_never_fires_on_healthy_long_run() {
+        let mut f = Iekf::level();
+        let imu = Imu { gyro: [0.0; 3], accel: [0.0, 0.0, -9.81] };
+        for k in 0..50_000 {
+            f.propagate(imu, 0.004);
+            f.update_gravity(imu.accel, 0.5);
+            if k % 50 == 0 {
+                f.update_position([0.0, 0.0, -2.0], 0.25);
+            }
+        }
+        assert_eq!(f.variance_floor_hits, 0, "healthy run must never floor");
+    }
+}
+
 #[cfg(kani)]
 mod kani_harness {
     use super::*;
@@ -1907,4 +2016,26 @@ mod kani_harness {
         assert!(d2 >= 0.0);
         assert!(d2.is_finite() || d2 == f32::INFINITY);
     }
+
+    /// IEKF-K: `floor_variances` is TOTAL and establishes its post-condition
+    /// for ANY covariance content (every entry nondet incl. NaN/±∞): after
+    /// the call every diagonal is finite and >= VAR_FLOOR. Pure comparisons
+    /// and assignments — fully tractable. (N=15 full-nondet matrix is 225
+    /// symbols; restrict to nondet DIAGONAL + one nondet off-diagonal pair,
+    /// which is the entire behavior surface of the function.)
+    #[kani::proof]
+    fn verify_variance_floor_postcondition() {
+        let mut p = mat_zero();
+        for i in 0..N {
+            p[i][i] = f32::from_bits(kani::any());
+        }
+        p[1][3] = f32::from_bits(kani::any());
+        p[3][1] = p[1][3];
+        let _hits = floor_variances(&mut p);
+        for i in 0..N {
+            assert!(p[i][i].is_finite());
+            assert!(p[i][i] >= VAR_FLOOR);
+            assert!(p[i][i] <= VAR_CEIL);
+        }
+    }
 }

scripts/check-float-discipline.sh

@@ -0,0 +1,59 @@
+#!/usr/bin/env bash
+# Float discipline gate (v1.123, SWDD-FALCON-FLOAT-001).
+#
+# The flight core is f32 BY REQUIREMENT: the estimator partition runs on the
+# i.MX RT1176's Cortex-M4, whose FPU (FPv4-SP) has no double-precision
+# hardware — every f64 op there is soft-float, an order of magnitude slower
+# (a WCET blow-up on the hottest loop). f64 belongs at exactly one place:
+# the geodetic/API boundary, where absolute latitude/longitude in f32 would
+# quantize at ~0.6 m (24-bit mantissa at mid-latitudes).
+#
+# This gate denies the `f64` token in the flight-path crates' non-test code.
+# A file whose header carries the marker
+#     //! float-discipline: allow-f64
+# is an ANNOTATED boundary module (say why on the same line) and is exempt.
+# Test / kani regions (`#[cfg(test)]` / `#[cfg(kani)]` to end-of-file, the
+# repo's layout convention) are exempt — test oracles SHOULD be f64.
+set -u
+
+# The M4/M7 flight-partition crates (estimator, cascade, failsafe, drivers).
+FLIGHT_CRATES=(
+  relay-math relay-iekf relay-geo relay-adrc relay-mix-quad
+  relay-fsm relay-preflight relay-calib relay-fsafe relay-rc
+  relay-param relay-batt relay-notch relay-flowrange relay-log
+  relay-mavlink falcon-mavlink falcon-core falcon-gnss-ubx falcon-baromag
+  falcon-imu-icm42688 falcon-esc-dshot
+)
+
+fail=0
+for crate in "${FLIGHT_CRATES[@]}"; do
+  for src in "crates/$crate/plain/src" "crates/$crate/src"; do
+    [ -d "$src" ] || continue
+    # skip the verus twin when a plain tree exists (plain is what ships)
+    if [ "$src" = "crates/$crate/src" ] && [ -d "crates/$crate/plain/src" ]; then
+      continue
+    fi
+    while IFS= read -r -d '' f; do
+      case "$(basename "$f")" in kani_proofs.rs|tests.rs) continue ;; esac
+      if head -5 "$f" | grep -q "float-discipline: allow-f64"; then
+        continue
+      fi
+      # portable word-boundary (BSD awk has no \y — a \y pattern silently
+      # matches NOTHING there, which made the gate pass vacuously on macOS;
+      # caught when CI's gawk found a hit the local run missed)
+      hits=$(awk '/#\[cfg\((test|kani)\)\]/{exempt=1} !exempt && /(^|[^A-Za-z0-9_])f64([^A-Za-z0-9_]|$)/{print FILENAME":"FNR": "$0}' "$f")
+      if [ -n "$hits" ]; then
+        echo "FLOAT-DISCIPLINE FAIL — f64 in flight-path code (annotate the"
+        echo "file '//! float-discipline: allow-f64 (<why>)' ONLY if it is a"
+        echo "genuine geodetic/API boundary; the M4 has no f64 hardware):"
+        echo "$hits"
+        fail=1
+      fi
+    done < <(find "$src" -name '*.rs' -print0)
+  done
+done
+
+if [ "$fail" = "0" ]; then
+  echo "float discipline: OK (f32 flight core; f64 only at annotated boundaries)"
+fi
+exit $fail