verify(falcon): v1.122 → verified — NOTCH-P01 + PREARM-P03

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: implemented
+    status: verified
     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: implemented
+    status: verified
     release: falcon-v1.122.0
     description: >
       The pre-arm gate (PREARM-P01/P02) shall be extended toward the

artifacts/verification/FV-FALCON-NOTCH-001.yaml

@@ -0,0 +1,51 @@
+artifacts:
+  - id: FV-FALCON-NOTCH-001
+    type: sw-verification
+    title: "NOTCH-P01 — RPM-tracked harmonic notch filtering: response, tracking, bypass, totality (v1.122)"
+    status: verified
+    release: falcon-v1.122.0
+    description: >
+      Verification of the gyro-path harmonic notch slice per
+      SWREQ-FALCON-NOTCH-P01.
+
+      Frequency response (MEASURED by DFT at the drive frequency, not
+      asserted from arithmetic): >= 20 dB attenuation at the tracked RPM
+      fundamental across the hover-to-full band
+      (relay-notch tests::twenty_db_at_fundamental_across_band); a stepped
+      20-point RPM sweep holds attenuation within 3 dB of nominal
+      (tests::swept_rpm_attenuation_within_3db); added phase lag at the
+      rate-loop crossover with the FULL 4-motor bank engaged measured
+      < 10 degrees (tests::phase_at_crossover_under_10_degrees).
+
+      Bypass: absent RPM telemetry => BIT-EXACT unity passthrough
+      (tests::bypass_is_bit_exact; proven for all inputs by NOTCH-K03).
+      Nyquist clamp: a notch never engages outside [10 Hz, 0.45 fs]
+      (tests::nyquist_clamp_per_notch; the trig-free band_ok gate is
+      Kani-proven over ALL inputs and unit-pinned to set()'s engagement in
+      tests::set_engagement_matches_band_ok).
+
+      Totality (Kani NOTCH-K01..K03): apply() is finite for ANY input bit
+      pattern and ANY poisoned internal state — operand sanitization means
+      no intermediate can even compute a NaN (CBMC's arithmetic
+      side-conditions pass, not just the final assert). The libm lesson is
+      pinned in the harness doc: symbolic trig is CBMC-intractable
+      (rem_pio2_large), hence the band_ok split.
+
+      Closed loop: with narrowband per-motor rotor-line vibration injected
+      on the SimBackend gyro, the tracking notch cuts settled-hover motor
+      thrash (RMS deviation of achieved motor state) to < 60% of the
+      bypass baseline, and the vehicle holds hover either way
+      (falcon-core tests::notch_reduces_rate_loop_noise_under_rotor_vibration
+      — the regression-metric shape for issue #270, whose gz limit-cycle
+      root-cause remains open there).
+    tags: [verification, falcon, filtering, notch, vibration, kani, v1.122]
+    fields:
+      method: automated-test
+      steps:
+        - run: cargo test -p relay-notch
+        - run: cargo test -p relay-notch --release
+        - run: cargo test -p falcon-core
+        - run: cargo kani -p relay-notch
+    links:
+      - type: verifies
+        target: SWREQ-FALCON-NOTCH-P01

artifacts/verification/FV-FALCON-PREARM-003.yaml

@@ -0,0 +1,48 @@
+artifacts:
+  - id: FV-FALCON-PREARM-003
+    type: sw-verification
+    title: "PREARM-P03 — table-driven pre-arm breadth: per-row gating, monotonicity, cold-boot NVM criterion (v1.122)"
+    status: verified
+    release: falcon-v1.122.0
+    description: >
+      Verification of the pre-arm check-table slice per
+      SWREQ-FALCON-PREARM-P03.
+
+      Per-check pair tests, TABLE-DRIVEN (coverage equals the table length
+      by construction — a row added to CheckId::ALL is automatically
+      covered): every one of the 19 rows individually blocks arming with
+      EXACTLY its own id and a DISTINCT operator-readable STATUSTEXT
+      reason, and clears when passed
+      (relay-preflight tests::every_row_blocks_alone_and_clears).
+      Undeclared breadth rows do not gate while the legacy six always do
+      (tests::undeclared_rows_do_not_gate_legacy_always_do).
+
+      Kani (PREFLIGHT-K03/K04, alongside the existing K01/K02 exhaustive
+      legacy-gate proofs): the table gate is EXACT (Allowed iff every
+      required row passes; a Blocked verdict always names a required,
+      failing row) and MONOTONE — failing any single row of an Allowed
+      table can never remain Allowed, i.e. adding a failing check can
+      never permit arming.
+
+      Integration (falcon-core): FlightSupervisor::command(Arm) gates on
+      the table (the legacy six mirrored as rows 0..=5 via set_preflight
+      and update_preflight); self-feedable rows refresh every step
+      (estimator innovation via the spoof CUSUM, GNSS agreement, geofence
+      sanity, battery takeoff margin, no-failsafe-latched, ESC telemetry
+      with declare-on-first-sight semantics). Cold-boot criterion on the
+      REAL PARAM-P03 seam: a defaults-fallback load (blank NVM, two-slot
+      image, LoadOutcome::FreshDefaults) cannot arm and reports
+      "PREARM: params are defaults (no NVM)"; after save + genuine reload
+      (LoadOutcome::Loaded) the same supervisor arms
+      (falcon-core tests::defaults_fallback_params_block_arming).
+    tags: [verification, falcon, prearm, safety, checks, kani, v1.122]
+    fields:
+      method: automated-test
+      steps:
+        - run: cargo test -p relay-preflight
+        - run: cargo test -p relay-preflight --release
+        - run: cargo test -p falcon-core
+        - run: cargo kani -p relay-preflight
+    links:
+      - type: verifies
+        target: SWREQ-FALCON-PREARM-P03