From 1e710d863b9e49414b3a6f8ce80b61d98c66d1e2 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 16 Jul 2026 10:15:12 +0200 Subject: [PATCH] =?UTF-8?q?verify(falcon):=20v1.122=20=E2=86=92=20verified?= =?UTF-8?q?=20=E2=80=94=20NOTCH-P01=20+=20PREARM-P03?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Code-free promotion per the two-commit rule. Evidence on merged main (fe29d37, impl PR #282 merged on a fully green rollup) plus a clean-room pass: 8 falsifiable claims verified cold, 8/8 CONFIRMED (suites, both Kani sets, gate wiring, the control-path filter placement, and the cold-boot NVM criterion's LoadOutcome assertions all independently re-checked). New FV-FALCON-NOTCH-001 + FV-FALCON-PREARM-003 (ids grepped free). SWREQ-FALCON-NOTCH-P01 + SWREQ-FALCON-PREARM-P03: implemented → verified. This closes the v1.117–v1.122 infrastructure ladder. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG --- artifacts/swreq/SWREQ-FALCON-NOTCH-P01.yaml | 2 +- artifacts/swreq/SWREQ-FALCON-PREARM-P03.yaml | 2 +- .../verification/FV-FALCON-NOTCH-001.yaml | 51 +++++++++++++++++++ .../verification/FV-FALCON-PREARM-003.yaml | 48 +++++++++++++++++ 4 files changed, 101 insertions(+), 2 deletions(-) create mode 100644 artifacts/verification/FV-FALCON-NOTCH-001.yaml create mode 100644 artifacts/verification/FV-FALCON-PREARM-003.yaml diff --git a/artifacts/swreq/SWREQ-FALCON-NOTCH-P01.yaml b/artifacts/swreq/SWREQ-FALCON-NOTCH-P01.yaml index cd09b51..2a0ebe4 100644 --- a/artifacts/swreq/SWREQ-FALCON-NOTCH-P01.yaml +++ b/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 diff --git a/artifacts/swreq/SWREQ-FALCON-PREARM-P03.yaml b/artifacts/swreq/SWREQ-FALCON-PREARM-P03.yaml index 4b59e41..37a610b 100644 --- a/artifacts/swreq/SWREQ-FALCON-PREARM-P03.yaml +++ b/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 diff --git a/artifacts/verification/FV-FALCON-NOTCH-001.yaml b/artifacts/verification/FV-FALCON-NOTCH-001.yaml new file mode 100644 index 0000000..30d9246 --- /dev/null +++ b/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 diff --git a/artifacts/verification/FV-FALCON-PREARM-003.yaml b/artifacts/verification/FV-FALCON-PREARM-003.yaml new file mode 100644 index 0000000..8f1a896 --- /dev/null +++ b/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