feat(falcon): v0.19.8 — verified mixer thrust-floor (MIX-P05) → reliable hover

artifacts/features/FEAT-FALCON-rollout.yaml

@@ -2060,6 +2060,78 @@ artifacts:
       - type: depends-on
         target: FEAT-FALCON-v0.19.6
 
+  - id: FEAT-FALCON-v0.19.8
+    type: feature
+    title: "v0.19.8 — verified mixer thrust-floor (MIX-P05) → reliable hover"
+    status: approved
+    description: >
+      LANDED. Fixes v0.19.7's hover bistability. A thrust-priority
+      mixing mode, relay-mix-quad::mix_thrust_floor (MIX-P05), reserves
+      a collective-thrust floor so the rate loop's attitude torque can
+      no longer steal lift — the dominant v0.19.7 limit-cycle root
+      cause. Closed-loop hover is now reliable: 4/4 consecutive bench
+      PASS at ~0.20 m, where the v0.19.7 attitude-priority mixer was
+      bistable (0.02 m one run, 1.97 m the next).
+
+      The fix: mix_thrust_floor(torque, thrust, floor) scales TORQUE by
+      a single factor so every motor stays in [floor, 1], leaving
+      collective thrust untouched. The mixer's roll/pitch/yaw columns
+      are zero-sum, so a uniform torque scale leaves the per-motor mean
+      (= collective) exactly equal to thrust → saturation costs
+      attitude authority, never lift. clamp_floor makes [floor,1] a
+      hard guarantee.
+
+      Verification — Kani, not Verus: the mixer is f32; the integer-only
+      Verus track (relay-lc/sc use i32/i64 because SMT float reasoning
+      is impractical) can't discharge float bounds. Kani (CBMC)
+      bit-blasts floats — the correct oracle.
+        cargo kani verify_mix_thrust_floor_bound → 155 checks SUCCESSFUL
+        cargo kani verify_mix_thrust_floor_total → SUCCESSFUL
+      Kani FOUND a real totality bug: extreme torque overflowed a delta
+      to NaN, poisoning the scale division → fixed by sanitising deltas.
+      Plus proptest + collective/direction-preservation unit tests.
+      (Genuine real-analysis — a Lyapunov hover-stability theorem —
+      would go to Lean via rules_lean4; MIX-P05 is a bound → Kani.)
+
+      Bench (--scenario=alt-rate: verified relay-rate + verified
+      relay-mix-quad thrust-floor + PI+D altitude, 30 s): 4/4 PASS,
+      final≈0.20 m, rms≈0.21 m. Deterministic.
+
+      Ships:
+        - crates/relay-mix-quad/plain: mix_thrust_floor + clamp_floor +
+          Kani harnesses + tests (14/14).
+        - examples/falcon-sitl-gz: alt-rate uses mix_thrust_floor; kd
+          0.15→0.30.
+        - SWREQ-FALCON-MIX-P05 + FV-FALCON-MIX-002.
+        - FV-FALCON-SIM-003 mock smoke → open-loop-climb (the gz-tuned
+          PosController makes closed-loop hover correctly FAIL on
+          MockPhysics; the gate caught it).
+        - bench-evidence/gz-sim/2026-05-29-v0.19.8-*.md + PASS log.
+
+      Verification:
+        - cargo kani (both harnesses) → SUCCESSFUL.
+        - cargo test --workspace → green; relay-mix-quad 14/14.
+        - gz bench → 4/4 PASS.
+        - rivet validate → PASS.
+
+      Honestly NOT claimed: full autonomous horizontal position hold
+      (relay-pos in the loop). The bench holds attitude + altitude with
+      verified relay-rate + relay-mix-quad; horizontal station-keeping
+      is the residual (v0.19.7 root causes #1 startup + #3
+      EKF-during-accel). The thrust-floor is the foundation that makes
+      adding it tractable.
+    tags: [falcon, milestone, v0.19.8, mixer, thrust-floor, kani, reliable-hover, landed]
+    fields:
+      release-target: "verified mixer thrust-floor (MIX-P05) → reliable hover"
+      bench-date: "2026-05-29"
+      verification: "Kani BMC (155 checks) — appropriate for f32 bounds; Verus is integer-only"
+      kani-found-bug: "extreme-torque overflow → NaN division; fixed by sanitising"
+      bench-result: "4/4 PASS final≈0.20 m rms≈0.21 m / 30 s (was bistable)"
+      verus-vs-lean: "MIX-P05 is a float bound → Kani; Lyapunov stability math would be Lean/rules_lean4"
+    links:
+      - type: depends-on
+        target: FEAT-FALCON-v0.19.7
+
   - id: FEAT-FALCON-v1.0
     type: feature
     title: "v1.0 — six-domain credit dossier + airframe variants"
@@ -2096,4 +2168,4 @@ artifacts:
       - type: implements
         target: SYSREQ-FALCON-010
       - type: depends-on
-        target: FEAT-FALCON-v0.19.7
+        target: FEAT-FALCON-v0.19.8

artifacts/swreq/SWREQ-FALCON-MIX-P01.yaml

@@ -62,6 +62,42 @@ artifacts:
       - type: derives-from
         target: SYSREQ-FALCON-005
 
+  - id: SWREQ-FALCON-MIX-P05
+    type: sw-req
+    title: "MIX-P05: Thrust-floor (thrust-priority) mixing mode"
+    status: approved
+    description: >
+      The mixer shall provide a thrust-priority mode
+      (`mix_thrust_floor(torque, thrust, floor)`) that reserves a
+      collective-thrust floor: for thrust ≥ floor (floor ∈ [0, 1]),
+      every per-motor PWM output is in [floor, 1] and finite, for ANY
+      torque command. Where MIX-P03's attitude-priority `mix`
+      sacrifices collective thrust to preserve torque ratios at
+      saturation, MIX-P05 scales the torque command by a single factor
+      so the collective is preserved (the mixer's torque columns are
+      zero-sum, so a uniform torque scale leaves the per-motor mean
+      equal to `thrust`). Attitude authority is sacrificed, never lift.
+
+      Rationale: against a real-physics SITL (gz, v0.19.7) the
+      attitude-priority mixer let the rate loop's torque steal thrust
+      near saturation, driving an altitude limit cycle. Reserving the
+      floor decouples attitude from altitude and makes closed-loop
+      hover reliable (v0.19.8: 4/4 bench PASS where the
+      attitude-priority mixer was bistable).
+    tags: [falcon, mixer, thrust-floor, invariant, kani]
+    fields:
+      req-type: safety
+      priority: must
+      verification-criteria: >
+        Kani BMC proof (the mixer is f32; the integer-only Verus track
+        can't discharge float bounds): for floor ∈ [0,1] and any finite
+        torque/thrust, forall i, motor_pwm[i] ∈ [floor, 1] and finite.
+        Harnesses verify_mix_thrust_floor_{bound,total}. Plus proptest
+        mix_p05_property_floor_holds + collective-preservation tests.
+    links:
+      - type: derives-from
+        target: SYSREQ-FALCON-005
+
   - id: SWREQ-FALCON-MIX-P04
     type: sw-req
     title: "MIX-P04: Per-variant motor count exported correctly"

artifacts/verification/FV-FALCON-MIX-002.yaml

@@ -0,0 +1,77 @@
+artifacts:
+  - id: FV-FALCON-MIX-002
+    type: sw-verification
+    title: "MIX-P05 thrust-floor invariant — Kani BMC proof + gz reliable-hover evidence (v0.19.8)"
+    status: approved
+    description: >
+      Verifies SWREQ-FALCON-MIX-P05: the thrust-priority
+      `QuadMixer::mix_thrust_floor(torque, thrust, floor)` reserves a
+      collective-thrust floor so the rate loop can never starve a motor
+      below it. This is what makes closed-loop hover reliable against
+      real gz physics (the v0.19.7 attitude-priority mixer was
+      bistable — limit-cycled or crashed).
+
+      Why Kani, not Verus: the mixer is f32-based. The verified-engine
+      pattern's Verus track is integer-only (relay-lc/sc use i32/i64
+      precisely because SMT float reasoning is impractical), which is
+      why relay-mix-quad was never on the Verus track. Kani (CBMC)
+      bit-blasts floats, so it is the correct mechanical oracle for a
+      float BOUND invariant. (Genuine real-analysis math — e.g. a
+      Lyapunov hover-stability theorem — would go to Lean via
+      rules_lean4; the floor invariant is float bounds, not analysis.)
+
+      Kani proof (cargo kani, crates/relay-mix-quad/plain):
+        - verify_mix_thrust_floor_bound: for floor ∈ [0,1] and finite
+          torque/thrust, forall i motor ∈ [floor,1] and finite.
+          155 checks, VERIFICATION SUCCESSFUL.
+        - verify_mix_thrust_floor_total: same with non-finite inputs
+          allowed (NaN/inf) — total + panic-free. SUCCESSFUL.
+
+      Kani also FOUND a real totality bug: extreme finite torque could
+      overflow the per-motor delta to ±inf or +inf+(−inf)=NaN, poisoning
+      the scale division. Fixed by sanitising each delta to finite (0 if
+      not). This is the oracle-gate working — the proof attempt surfaced
+      a defect a hand-written test missed.
+
+      Supporting evidence:
+        - proptest mix_p05_property_floor_holds (1e3 cases): floor holds.
+        - unit tests: collective-preservation (mean motor == thrust
+          under pure torque, zero-sum columns), direction-preservation,
+          floor-never-starved.
+        - gz bench (bench-evidence/gz-sim/2026-05-29-v0.19.8-*.md):
+          --scenario=alt-rate, 4/4 consecutive PASS at final_dist≈0.20 m,
+          rms_steady≈0.21 m over 30 s — reliable controlled hover, where
+          the v0.19.7 attitude-priority mixer was bistable (0.02 m one
+          run, 1.97 m the next).
+
+      Verification:
+        - cargo kani --harness verify_mix_thrust_floor_bound → SUCCESSFUL.
+        - cargo kani --harness verify_mix_thrust_floor_total → SUCCESSFUL.
+        - cargo test -p relay-mix-quad → 14/14.
+        - cargo test --workspace → green.
+        - gz bench → 4/4 PASS.
+        - rivet validate → PASS.
+
+      Honestly NOT claimed:
+        - That the FULL position-hold cascade (relay-pos horizontal
+          autonomy) hovers — the bench uses the verified relay-rate
+          attitude stabilisation + the verified relay-mix-quad
+          thrust-floor + a PI+D altitude loop. Autonomous horizontal
+          position hold (relay-pos in the loop) remains the residual
+          item (root cause #1, startup/EKF), tracked separately.
+        - That Verus proves this. It can't (floats); Kani does. The
+          claim is BMC-complete over the bounded float domain, not an
+          unbounded SMT proof.
+    tags: [falcon, mixer, thrust-floor, kani, bmc, reliable-hover, v0.19.8]
+    fields:
+      runs:
+        - "cargo kani --harness verify_mix_thrust_floor_bound  (155 checks, SUCCESSFUL)"
+        - "cargo kani --harness verify_mix_thrust_floor_total  (SUCCESSFUL)"
+        - "cargo test -p relay-mix-quad  (14/14)"
+        - "gz bench --scenario=alt-rate  (4/4 PASS, final≈0.20 m)"
+      tool: "Kani (CBMC) — appropriate for f32 bound invariants; Verus is integer-only here"
+      kani-found-bug: "extreme-torque overflow → NaN in scale division; fixed by sanitising deltas"
+      bench-result: "4/4 PASS final_dist≈0.20 m rms≈0.21 m / 30 s (was bistable pre-floor)"
+    links:
+      - type: verifies
+        target: SWREQ-FALCON-MIX-P05

bench-evidence/gz-sim/1780028093-gazebo-alt-rate-harness.log

@@ -0,0 +1,15 @@
+falcon-sitl-gz bench-evidence
+backend: gazebo
+scenario: alt-rate
+timestamp: 1780028093
+
+steps:       3000
+final_dist:  0.205 m
+peak_dist:   2.000 m
+rms_steady:  0.214 m  (last 5 s)
+min_dist:    0.205 m
+wall:        34.904 s
+imu_recv:    7031
+navsat_recv: 1746
+motor_send:  3000
+verdict:    PASS