diff --git a/artifacts/swreq/SWREQ-FALCON-GNSS-P02.yaml b/artifacts/swreq/SWREQ-FALCON-GNSS-P02.yaml index faba59f..1fdd53a 100644 --- a/artifacts/swreq/SWREQ-FALCON-GNSS-P02.yaml +++ b/artifacts/swreq/SWREQ-FALCON-GNSS-P02.yaml @@ -2,7 +2,7 @@ artifacts: - id: SWREQ-FALCON-GNSS-P02 type: sw-req title: "GNSS-P02 — dual-receiver blending and failover (2× u-blox M9N)" - status: implemented + status: verified release: falcon-v1.121.0 description: > The estimator input shall support TWO GNSS receivers (the first diff --git a/artifacts/swreq/SWREQ-FALCON-RANGEDRV-P01.yaml b/artifacts/swreq/SWREQ-FALCON-RANGEDRV-P01.yaml index 78c4cbc..47e31b8 100644 --- a/artifacts/swreq/SWREQ-FALCON-RANGEDRV-P01.yaml +++ b/artifacts/swreq/SWREQ-FALCON-RANGEDRV-P01.yaml @@ -2,7 +2,7 @@ artifacts: - id: SWREQ-FALCON-RANGEDRV-P01 type: sw-req title: "RANGEDRV-P01 — Benewake TF02 Pro rangefinder driver + landing/terrain assist" - status: implemented + status: verified release: falcon-v1.121.0 description: > The stack shall decode the Benewake TF02 Pro LiDAR rangefinder diff --git a/artifacts/verification/FV-FALCON-GNSS-002.yaml b/artifacts/verification/FV-FALCON-GNSS-002.yaml new file mode 100644 index 0000000..d122523 --- /dev/null +++ b/artifacts/verification/FV-FALCON-GNSS-002.yaml @@ -0,0 +1,42 @@ +artifacts: + - id: FV-FALCON-GNSS-002 + type: sw-verification + title: "GNSS-P02 — dual-M9N selection/blending/failover + divergence integrity (v1.121)" + status: verified + release: falcon-v1.121.0 + description: > + Verification of the dual-receiver GNSS slice per SWREQ-FALCON-GNSS-P02. + + Dispersion campaign (CI-sized, 40 LCG-dispersed trials over fault + type and onset — dropout, accuracy collapse, divergence walk, + nominal): the divergence flag fires in 100% of walk trials with ZERO + false flags in the others, and no trial steps the position estimate + discontinuously (max inter-cycle step < 1.5 m at 5000 steps/trial) + (falcon-core tests::dual_gnss_dispersion_campaign). Failover within + one fix interval with the estimate held (< 1 m step, no estimator + reset: tests::dual_gnss_failover_holds_estimate). Divergence latches, + blocks pre-arm, and the selector keeps the estimator-consistent + receiver (tests::gnss_divergence_latches_and_blocks_arming; selector + unit tests in falcon-gnss-ubx dual::tests cover blend weighting, + accuracy-collapse and innovation-jump disqualification, transient + non-latch, dual-loss no-fix). + + Kani GNSS-K05 (falcon-gnss-ubx kani_proofs.rs): selector totality — + every NedFix field nondet including NaN/∞ positions and accuracies — + never panics, never emits a non-finite selection. The harness CAUGHT + a real defect during development: a denormal reported accuracy + overflowed the 1/acc² blend weight into ∞−∞ = NaN; fixed with the + MIN_ACC_M floor + MAX_POS_M sanity bound now in the health gate. + The previously-orphaned relay-iekf SpoofMonitor is wired (position + innovation per GNSS update) and nav_compromised (spoof ∨ divergence) + blocks arming. + tags: [verification, falcon, gnss, dual-receiver, m9n, kani, v1.121] + fields: + method: automated-test + steps: + - run: cargo test -p falcon-gnss-ubx + - run: cargo test -p falcon-core + - run: cargo kani -p falcon-gnss-ubx + links: + - type: verifies + target: SWREQ-FALCON-GNSS-P02 diff --git a/artifacts/verification/FV-FALCON-RANGEDRV-001.yaml b/artifacts/verification/FV-FALCON-RANGEDRV-001.yaml new file mode 100644 index 0000000..088b868 --- /dev/null +++ b/artifacts/verification/FV-FALCON-RANGEDRV-001.yaml @@ -0,0 +1,51 @@ +artifacts: + - id: FV-FALCON-RANGEDRV-001 + type: sw-verification + title: "RANGEDRV-P01 — TF02-Pro wire decode + terrain-relative landing assist (v1.121)" + status: verified + release: falcon-v1.121.0 + description: > + Verification of the rangefinder slice per SWREQ-FALCON-RANGEDRV-P01. + + Decode conformance: the 9-byte Benewake frame layout (0x59 0x59 + header, distance cm LE at bytes 2-3, strength LE at 4-5, checksum = + low 8 bits of sum(bytes 0..7)) is cross-validated against TWO + independent open-source parsers — ArduPilot AP_RangeFinder_Benewake + and PX4 tfmini_parser — whose quoted semantics are pinned in the + module doc, plus a hand-worked concrete vector + (relay-flowrange tf02::tests::decodes_documented_frame_arithmetic; + external-reference rule: self-round-trip proves robustness, not + conformance). Quality gating IN the decoder: low-strength (< 60 or + 65535), sentinel (0xFFFF) and out-of-envelope (outside 10..=4000 cm) + returns never reach the caller (tests::quality_gate_rejects); + streaming resync through garbage and false headers + (tests::scanner_resyncs_through_garbage, scanner_skips_false_header). + + Kani FLOWRANGE-K03/K04: decode totality + gate soundness over ALL + 9-byte patterns; scanner totality with bounded consumption. K03 + CAUGHT a float defect during development: 10 x 0.01f32 = + 0.099999994 escaped the 0.1 m envelope bound; fixed by switching to + division (correctly-rounded quotient makes the bounds exact). + + Landing assist (terrain-relative AGL, the PX4 terrain-estimator + role — deliberately NOT z-state fusion, where three absolute + references would fight): with baro AND GNSS vertical both lying 2 m + high, touchdown fires within 15 cm of TRUE ground with the range + assist and provably does NOT without it (negative control kept: + falcon-core tests::biased_baro_range_assisted_touchdown). An + obstacle overflight's sudden short return is REJECTED by the ±3 m + innovation gate and the altitude estimate does not fold + (tests::obstacle_overflight_does_not_fold_altitude). The previously- + orphaned relay_flowrange::range_to_altitude (tilt compensation + + band gating, Kani FLOWRANGE-K01) is now the consuming path. + tags: [verification, falcon, rangefinder, tf02-pro, landing, kani, v1.121] + fields: + method: automated-test + steps: + - run: cargo test -p relay-flowrange + - run: cargo test -p relay-flowrange --release + - run: cargo test -p falcon-core + - run: cargo kani -p relay-flowrange + links: + - type: verifies + target: SWREQ-FALCON-RANGEDRV-P01