feat(falcon): v0.19.8 — verified mixer thrust-floor (MIX-P05) → reliable hover#53
Conversation
…ble hover
Fixes the v0.19.7 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 s ∈ [0,1] 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 → altitude decoupled from attitude.
- clamp_floor makes the [floor,1] bound a HARD guarantee.
Verification (MIX-P05) — 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
Invariant: floor ∈ [0,1] ∧ finite inputs ⟹ ∀i motor ∈ [floor,1].
Kani FOUND a real totality bug: extreme finite torque overflows the
per-motor delta to ±inf / +inf+(−inf)=NaN, poisoning the scale
division. Fixed by sanitising deltas to finite. Oracle-gate working.
Plus proptest mix_p05_property_floor_holds + collective-preservation
+ direction-preservation unit tests.
Bench (--scenario=alt-rate: verified relay-rate + verified
relay-mix-quad thrust-floor + PI+D altitude, 30 s):
4/4 PASS, final_dist≈0.20 m, rms_steady≈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(.,.,0.5),
kd 0.15→0.30.
- SWREQ-FALCON-MIX-P05 + FV-FALCON-MIX-002.
- bench-evidence/gz-sim/2026-05-29-v0.19.8-*.md + alt-rate PASS log.
Honestly NOT claimed: full autonomous horizontal position hold
(relay-pos in the loop). The bench holds attitude + altitude with
verified components; 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.
Verus vs Lean: the floor is float bounds → Kani. Genuine real-analysis
(Lyapunov hover stability) would go to Lean via rules_lean4 — not there
yet.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
running 9 tests test result: ok. 9 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s falcon-sitl-gz: backend=mock scenario=open-loop-climb duration=5s running 55 tests test result: ok. 55 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.03s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 55 tests test result: ok. 55 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 55 tests test result: ok. 55 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.43s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 17 tests test result: ok. 17 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.02s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 9 tests test result: ok. 9 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.01s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 9 tests test result: ok. 9 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 9 tests test result: ok. 9 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.10s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 13 tests test result: ok. 13 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.04s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 13 tests test result: ok. 13 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 13 tests test result: ok. 13 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.64s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 17 tests test result: ok. 17 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.08s --- scenario: step --- running 9 tests test result: ok. 9 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.06s [falcon-hello-demo] building release binary... running 20 tests test result: ok. 20 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.02s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 10 tests test result: ok. 10 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.01s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 10 tests test result: ok. 10 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 10 tests test result: ok. 10 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.11s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 17 tests test result: ok. 17 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.08s --- scenario: attitude --- running 16 tests test result: ok. 16 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.06s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 16 tests test result: ok. 16 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.01s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 16 tests test result: ok. 16 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.85s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 5 tests test result: ok. 5 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s --- noise=0 (deterministic) --- running 13 tests test result: ok. 13 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.01s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 13 tests test result: ok. 13 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 13 tests test result: ok. 13 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.11s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 17 tests test result: ok. 17 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.08s --- scenario: mission --- running 17 tests test result: ok. 17 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.02s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 1 test test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 16 filtered out; finished in 0.02s running 10 tests test result: ok. 10 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s falcon-hitl-rfspoof: backend=stub duration=5s running 55 tests test result: ok. 55 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.03s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 10 tests test result: ok. 10 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 14 tests test result: ok. 14 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.01s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 13 tests test result: ok. 13 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.05s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 17 tests test result: ok. 17 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.08s falcon verification gate (type: sw-verification, filter: (has-tag "falcon"))41 artifact(s) matched: FV-FALCON-SIM-003, FV-FALCON-SIM-010, FV-FALCON-SIM-005, FV-FALCON-MAVLINK-001, FV-FALCON-ARCH-002, FV-FALCON-GEO-002, FV-FALCON-EKF-STUB-001, FV-FALCON-RATE-001, FV-FALCON-WORLD-001, FV-FALCON-COV-001, FV-FALCON-NID-002, FV-FALCON-SIM-006, FV-FALCON-ATT-001, FV-FALCON-ARCH-001, FV-FALCON-EKF-001, FV-FALCON-GEO-003, FV-FALCON-TQ-001, FV-FALCON-POS-001, FV-FALCON-GEO-001, FV-FALCON-SIM-011, FV-FALCON-HITL-001, FV-FALCON-HITL-002, FV-FALCON-SIM-001, FV-FALCON-COV-005, FV-FALCON-PIPELINE-001, FV-FALCON-SIM-007, FV-FALCON-SIM-009, FV-FALCON-COV-004, FV-FALCON-SIM-013, FV-FALCON-SIM-008, FV-FALCON-MIX-001, FV-FALCON-MAVLINK-002, FV-FALCON-MIX-002, FV-FALCON-UAM-001, FV-FALCON-SIM-004, FV-FALCON-NID-001, FV-FALCON-FAULT-001, FV-FALCON-SIM-002, FV-FALCON-COV-003, FV-FALCON-COV-002, FV-FALCON-SIM-012[ PASS] ( 2.56s) FV-FALCON-SIM-003: cargo test -p falcon-sitl-gz test result: ok. 14 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.01s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 14 tests test result: ok. 14 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 14 tests test result: ok. 14 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.15s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 55 tests test result: ok. 55 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.03s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 1 test test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 16 filtered out; finished in 0.05s running 9 tests test result: ok. 9 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 20 tests test result: ok. 20 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.02s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 20 tests test result: ok. 20 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.28s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 9 tests test result: ok. 9 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 17 tests test result: ok. 17 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.08s running 55 tests test result: ok. 55 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.03s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 10 tests test result: ok. 10 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s Filename Regions Missed Regions Cover Functions Missed Functions Executed Lines Missed Lines Cover Branches Missed Branches Covercoverage_subjects/geofence_subject_rs/src/lib.rs 48 48 0.00% 5 5 0.00% 23 23 0.00% 0 0 -
|
| count | |
|---|---|
| Passed | 34 |
| Failed | -9 |
| Skipped (bench-only — needs hardware / sim) | 7 |
| Skipped (no steps) | 9 |
Failed artifacts
Bench-only artifacts (not run by CI)
FV-FALCON-SIM-005— gz-transport NavSat + Home projection — position-dependent loops (v0.18.1)FV-FALCON-ARCH-002— spar codegen --format wit recheck — works at v0.10.0 (v0.15.0)FV-FALCON-COV-001— witness MC/DC structural coverage — falcon pipeline wired (v0.13)FV-FALCON-ARCH-001— spar AADL architectural model — falcon cascade (v0.13)FV-FALCON-GEO-003— Geofence safety path — miri UB/overflow check (v0.12, AI substitute)FV-FALCON-SIM-001— PX4-SITL end-to-end loop — recipe + preset + smoke (v0.14.0)FV-FALCON-COV-003— witness MC/DC on real Rust source — Geofence subject (v0.14.1)
Source of truth: artifacts/verification/FV-FALCON-*.yaml.
1 participant
Summary
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 mixer was bistable (0.02 m / 1.97 m run-to-run).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 → a uniform torque scale leaves the per-motor mean (= collective) exactly equal tothrust. Saturation costs attitude authority, never lift → altitude decoupled from attitude.clamp_floormakes[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.
Kani found a real totality bug: extreme torque overflowed a per-motor delta to NaN, poisoning the scale division — fixed by sanitising deltas. The oracle-gate working as designed. 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 — reliable hover
--scenario=alt-rate(verifiedrelay-rate+ verifiedrelay-mix-quadthrust-floor + PI+D altitude), 30 s: 4/4 PASS, final≈0.20 m, rms≈0.21 m. Deterministic.Also
FV-FALCON-SIM-003mock smoke →open-loop-climb(the gz-tuned PosController makes closed-loop hover correctly FAIL on MockPhysics; the verification gate caught this — a gz-specific tuning silently breaking the mock contract).Verification
cargo kani(both harnesses) → SUCCESSFUL.cargo test --workspace→ green;relay-mix-quad14/14.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.🤖 Generated with Claude Code