verify(falcon): v1.121 → verified — GNSS-P02 dual-M9N + RANGEDRV-P01 TF02-Pro

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

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

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

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