feat(falcon): v1.122 — RPM-tracked harmonic notches + pre-arm check table (NOTCH-P01 + PREARM-P03)

.github/workflows/ci.yml

@@ -65,7 +65,7 @@ jobs:
             -p falcon-param -p relay-fsm -p relay-preflight -p relay-calib \
             -p falcon-core -p relay-mix-quad \
             -p relay-arm -p relay-adrc -p relay-geo -p relay-iekf \
-            -p relay-batt -p relay-flowrange -p falcon-gnss-ubx \
+            -p relay-batt -p relay-flowrange -p falcon-gnss-ubx -p relay-notch \
             --all-targets -- -D warnings
 
   test:

.github/workflows/kani.yml

@@ -63,6 +63,7 @@ jobs:
           - relay-mix-quad
           - relay-mavlink
           - relay-batt
+          - relay-notch
           # 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

Cargo.toml

@@ -27,6 +27,7 @@ members = [
     "crates/relay-dronecan",
     "crates/relay-param",
     "crates/relay-batt",
+    "crates/relay-notch",
     "crates/relay-calib",
     "crates/relay-log",
     "crates/relay-mix-multi",

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

@@ -2,7 +2,7 @@ artifacts:
   - id: SWREQ-FALCON-NOTCH-P01
     type: sw-req
     title: "NOTCH-P01 — RPM-driven harmonic notch filtering on the gyro path"
-    status: proposed
+    status: implemented
     release: falcon-v1.122.0
     description: >
       The rate-loop gyro path shall attenuate per-motor rotational vibration

artifacts/swreq/SWREQ-FALCON-PREARM-P03.yaml

@@ -2,7 +2,7 @@ artifacts:
   - id: SWREQ-FALCON-PREARM-P03
     type: sw-req
     title: "PREARM-P03 — pre-arm check breadth: configuration, estimator, and hardware consistency"
-    status: proposed
+    status: implemented
     release: falcon-v1.122.0
     description: >
       The pre-arm gate (PREARM-P01/P02) shall be extended toward the

crates/falcon-core/Cargo.toml

@@ -22,6 +22,7 @@ relay-preflight = { path = "../relay-preflight" }
 relay-calib = { path = "../relay-calib" }
 relay-batt = { path = "../relay-batt" }
 relay-flowrange = { path = "../relay-flowrange" }
+relay-notch = { path = "../relay-notch" }
 falcon-gnss-ubx = { path = "../falcon-gnss-ubx" }
 relay-log = { path = "../relay-log" }
 relay-param = { path = "../relay-param" }

crates/relay-notch/Cargo.toml

@@ -0,0 +1,21 @@
+[package]
+name = "relay-notch"
+description = "Relay Notch — RPM-tracked harmonic notch filtering for the rate-loop gyro path (PX4 IMU_GYRO_DNF / ArduPilot INS_HNTCH / Betaflight RPM-filter parity). Per-motor biquad notches at the rotation fundamental + 2nd harmonic, center frequencies tracking achieved eRPM; clean unity bypass when RPM telemetry is absent (no filtering is safer than a mistracked notch); Nyquist-clamped per notch. no_std/no_alloc/forbid(unsafe)."
+version.workspace = true
+edition.workspace = true
+license.workspace = true
+repository.workspace = true
+rust-version.workspace = true
+
+[lib]
+path = "plain/src/lib.rs"
+crate-type = ["rlib"]
+
+[dependencies]
+relay-math = { path = "../relay-math" }
+
+[dev-dependencies]
+proptest.workspace = true
+
+[lints]
+workspace = true

crates/relay-notch/plain/proptest-regressions/lib.txt

@@ -0,0 +1,7 @@
+# Seeds for failure cases proptest has generated in the past. It is
+# automatically read and these particular cases re-run before any
+# novel cases are generated.
+#
+# It is recommended to check this file in to source control so that
+# everyone who runs the test benefits from these saved cases.
+cc bf5228648715f7572e4eedb34ba1a89e48d05b634d7009f2fe9416a6b4648fec # shrinks to xs = [2139095040], rpm = [6751, 0, 6751, 6751]

crates/relay-notch/plain/src/kani_proofs.rs

@@ -0,0 +1,72 @@
+//! Kani harnesses for relay-notch (plain-only sibling).
+//!
+//! The verification split (the relay-rc pattern, plus a libm lesson): the
+//! trig in `set()` is CBMC-intractable on symbolic arguments (libm's
+//! rem_pio2_large unwinds >1500 iterations), so the harnesses keep trig
+//! CONCRETE and prove the trig-free properties over all inputs:
+//! totality of `apply` for any input AND any (poisoned) state, the
+//! never-engage-outside-band safety direction of `set`, and the bank's
+//! bit-exact bypass. The engages-in-band liveness direction and the
+//! frequency-domain depth/phase are test-measured.
+#![cfg(kani)]
+
+use crate::*;
+
+/// NOTCH-K01 — `apply` is TOTAL for ANY input bit pattern and ANY internal
+/// state (all four state words nondet, coefficients from a concrete
+/// engaged tuning): the output is always finite.
+#[kani::proof]
+fn verify_apply_total_any_state() {
+    let mut n = Notch::default();
+    n.set(70.0, 1000.0); // concrete trig — engaged hover-band notch
+    assert!(n.is_engaged());
+    n.poison_state([
+        f32::from_bits(kani::any()),
+        f32::from_bits(kani::any()),
+        f32::from_bits(kani::any()),
+        f32::from_bits(kani::any()),
+    ]);
+    let x = f32::from_bits(kani::any());
+    let y = n.apply(x);
+    assert!(y.is_finite());
+}
+
+/// NOTCH-K02 — the band gate over ALL inputs, trig-free by construction
+/// (`band_ok` is comparisons only; `set` engages exactly when it holds —
+/// the one-line linkage is unit-pinned in set_engagement_matches_band_ok):
+/// any non-finite / below-floor / above-Nyquist / fs ≤ 0 pair is rejected,
+/// and a DISENGAGED notch's `apply` is bit-exact unity for any input.
+#[kani::proof]
+fn verify_band_gate_and_disengaged_unity() {
+    let f0: f32 = kani::any();
+    let fs: f32 = kani::any();
+    if band_ok(f0, fs) {
+        assert!(f0.is_finite() && fs.is_finite());
+        assert!(fs > 0.0);
+        assert!(f0 >= MIN_F0_HZ);
+        assert!(f0 <= MAX_F0_FRAC * fs);
+    }
+    let mut n = Notch::default();
+    let x = f32::from_bits(kani::any());
+    let y = n.apply(x);
+    assert!(y.to_bits() == x.to_bits(), "disengaged is bit-exact unity");
+}
+
+/// NOTCH-K03 — the bank's RPM-absent bypass is bit-exact for ANY input
+/// (concrete prior tuning; the None transition disengages everything).
+#[kani::proof]
+fn verify_bank_bypass_bit_exact() {
+    let mut bank: HarmonicNotchBank<4> = HarmonicNotchBank::new(250.0);
+    bank.update_rpm(Some([4000, 4100, 3950, 4050])); // concrete trig
+    bank.update_rpm(None);
+    assert!(bank.is_bypassed());
+    let x = [
+        f32::from_bits(kani::any()),
+        f32::from_bits(kani::any()),
+        f32::from_bits(kani::any()),
+    ];
+    let y = bank.apply(x);
+    assert!(y[0].to_bits() == x[0].to_bits());
+    assert!(y[1].to_bits() == x[1].to_bits());
+    assert!(y[2].to_bits() == x[2].to_bits());
+}