From 683f33bc22e39a77d8c0718c7d2193d404672f87 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 16 Jul 2026 14:22:37 +0200 Subject: [PATCH 1/2] =?UTF-8?q?feat(falcon):=20v1.123=20=E2=80=94=20float?= =?UTF-8?q?=20discipline:=20CI=20f64=20gate=20+=20IEKF=20variance=20floor?= =?UTF-8?q?=20(SWDD-FALCON-FLOAT-001)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit An external review asked whether the floats should be 64- or 32-bit. The honest answer: f32 in the flight core is the REQUIREMENT (the M4's FPv4-SP has no double-precision hardware; PX4/ArduPilot fly f32 EKFs; f64 would break CBMC tractability), and f64 belongs at exactly one place — geodetic absolutes, where f32 degrees quantize at ~0.6 m. The codebase already followed this everywhere; this slice turns the convention into an enforced rule and closes the one genuine risk the review surfaced. - scripts/check-float-discipline.sh (new, wired into CI): denies the f64 token in the 21 flight-partition crates' non-test code; a file opts out only via a visible header annotation — today exactly one, falcon-mavlink's geodetic boundary (now annotated). Green on the current tree: the flight core was already f64-free. - relay-iekf floor_variances (the review's real finding): the cheap standard-form update P <- (I-KH)P can round an f32 diagonal NEGATIVE; symmetrise() cannot see that. Every measurement update now heals diagonals into [1e-9, 1e6] with corrupt-row correlations zeroed and a LOUD counter (Iekf::variance_floor_hits — zero across all existing campaigns; a guard, not a crutch). The Kani post-condition harness CAUGHT the first version: +infinity passed the naive `d >= FLOOR` check, and an infinite diagonal must heal to the CEILING (maximal uncertainty), never the floor (fabricated certainty). 4/4 harnesses verified; 29 iekf + 56 falcon-core tests green including a 50k-cycle zero-hits healthy-run assertion. - SWDD-FALCON-FLOAT-001 (implemented) records decision + rationale + enforcement. SCOPE MOVE, surfaced: PART-P01/P02 (blocked on synth #708/#369) bumped falcon-v1.123.0 -> v1.124.0; v1.123 is this slice. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG --- .github/workflows/ci.yml | 2 + artifacts/swdd/SWDD-FALCON-FLOAT-001.yaml | 58 +++++++++ artifacts/swreq/SWREQ-FALCON-PART-P01.yaml | 2 +- artifacts/swreq/SWREQ-FALCON-PART-P02.yaml | 2 +- crates/falcon-mavlink/plain/src/lib.rs | 1 + crates/relay-iekf/plain/src/lib.rs | 133 ++++++++++++++++++++- scripts/check-float-discipline.sh | 56 +++++++++ 7 files changed, 251 insertions(+), 3 deletions(-) create mode 100644 artifacts/swdd/SWDD-FALCON-FLOAT-001.yaml create mode 100755 scripts/check-float-discipline.sh 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..830f327 --- /dev/null +++ b/scripts/check-float-discipline.sh @@ -0,0 +1,56 @@ +#!/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) continue ;; esac + if head -5 "$f" | grep -q "float-discipline: allow-f64"; then + continue + fi + hits=$(awk '/#\[cfg\((test|kani)\)\]/{exempt=1} !exempt && /\yf64\y/{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 From 63b2ac28f638c478fd2bb450e496ce57b23dc112 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 16 Jul 2026 14:25:34 +0200 Subject: [PATCH 2/2] fix(float-gate): portable word-boundary + separate-tests-file exemption MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit CI caught what the local run could not: BSD awk has no \y word boundary — the pattern silently matched NOTHING on macOS, so the local "OK" was vacuous while CI's gawk found a real hit (falcon-mavlink keeps its tests in a separate tests.rs, outside the cfg(test)-to-EOF exemption). Portable character-class boundary now; tests.rs skipped like kani_proofs.rs; and the oracle is negative-tested (a seeded f64 at file top FAILS the gate locally, clean tree passes). Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG --- scripts/check-float-discipline.sh | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/scripts/check-float-discipline.sh b/scripts/check-float-discipline.sh index 830f327..0253600 100755 --- a/scripts/check-float-discipline.sh +++ b/scripts/check-float-discipline.sh @@ -34,11 +34,14 @@ for crate in "${FLIGHT_CRATES[@]}"; do continue fi while IFS= read -r -d '' f; do - case "$(basename "$f")" in kani_proofs.rs) continue ;; esac + case "$(basename "$f")" in kani_proofs.rs|tests.rs) continue ;; esac if head -5 "$f" | grep -q "float-discipline: allow-f64"; then continue fi - hits=$(awk '/#\[cfg\((test|kani)\)\]/{exempt=1} !exempt && /\yf64\y/{print FILENAME":"FNR": "$0}' "$f") + # 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"