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