diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index cf86a6d..3bc4569 100644 --- a/.github/workflows/ci.yml +++ b/.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 \ diff --git a/artifacts/swdd/SWDD-FALCON-FLOAT-001.yaml b/artifacts/swdd/SWDD-FALCON-FLOAT-001.yaml new file mode 100644 index 0000000..ab4abb6 --- /dev/null +++ b/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 ()"; 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 diff --git a/artifacts/swreq/SWREQ-FALCON-PART-P01.yaml b/artifacts/swreq/SWREQ-FALCON-PART-P01.yaml index 9c240df..c520068 100644 --- a/artifacts/swreq/SWREQ-FALCON-PART-P01.yaml +++ b/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 / diff --git a/artifacts/swreq/SWREQ-FALCON-PART-P02.yaml b/artifacts/swreq/SWREQ-FALCON-PART-P02.yaml index a2cc566..0c49846 100644 --- a/artifacts/swreq/SWREQ-FALCON-PART-P02.yaml +++ b/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 diff --git a/crates/falcon-mavlink/plain/src/lib.rs b/crates/falcon-mavlink/plain/src/lib.rs index 54212a3..caf0f52 100644 --- a/crates/falcon-mavlink/plain/src/lib.rs +++ b/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. //! diff --git a/crates/relay-iekf/plain/src/lib.rs b/crates/relay-iekf/plain/src/lib.rs index c42552c..f50281b 100644 --- a/crates/relay-iekf/plain/src/lib.rs +++ b/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); + } + } } diff --git a/scripts/check-float-discipline.sh b/scripts/check-float-discipline.sh new file mode 100755 index 0000000..0253600 --- /dev/null +++ b/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 ()' 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