fix(supv): a failsafe event must ESCALATE, not re-fire — RTL lasted one tick (#562)

[avrabe]

Fixes the defect reproduced in #562.

Every trigger in FlightSupervisor::step is level-triggered, and a vehicle flying home is by definition still outside the fence. So the breach re-sent Event::Failsafe every tick, and the FSM did exactly as told:

(Takeoff | Loiter | Mission, Failsafe) => if have_position { Rtl } else { Land },
(Rtl, Failsafe) => Land,

Measured — home 2 m out, fence 0.5 m:

tick 0:  Takeoff -> Rtl        breach=true
tick 1:  Rtl     -> Disarmed   breach=true

RTL never got a tick to fly. Landing where you are after a fence breach means landing outside the fence you were recovering from — inverting SWREQ-FALCON-SUPV-P01's "geofence → RTL ACTUATION" and SYSREQ-FALCON-014. The battery failsafe shares that expression and relay-batt's flags latch (Kani verify_latch_never_clears), so it was equally persistent.

The fix

mode_rank gives each mode a severity, and each send now asks "would this escalate?" rather than "is the condition true?":

trigger	wants	behaviour
geofence / low battery / wind	rank 2 (Rtl)	commands RTL from flight; no longer re-sent while in RTL
critical battery / motor-out	rank 3 (Land)	still escalates out of RTL
attitude runaway	Terminate	untouched — absorbing

That last row is why the naive fix is wrong: guarding on != Mode::Rtl would have silently broken critical-battery escalation, because geofence and battery flow through the same expression at :1935.

Why not wire relay-fsafe instead

This is relay-fsafe's most-severe-wins + monotone-latch semantics applied at the send, and that crate is deliberately not used here: its Triggers has no runaway, wind, motor-out or battery-silence field, and policy_action cannot reach Terminate — the action this path uses to cut motors. Wiring it is a trigger-set merge plus a re-proof of four exhaustive Kani harnesses, which should not ride on a defect fix. Worth doing as its own piece (ORPHAN-P01).

Why no test saw it

Five assertions accept the whole recovery family — Mode::Rtl | Mode::Land | Mode::Disarmed — which cannot distinguish "RTL flew home" from "RTL lasted 4 ms". And relay-fsm's verify_failsafe_recovers is single-step, so it cannot see re-invocation by construction.

The new test asserts RTL survives 50 ticks of continuing breach. Its geometry is load-bearing, and my first attempt got it wrong: with a 1 cm fence, "breached" and "arrived home" (dist_home < 0.4) are true simultaneously, RTL ends via the arrival handoff, and the demotion is invisible — I reported a non-reproduction off exactly that. Home 2 m away separates them.

Verified to fail without the fix (RTL was demoted 1 ticks in) and pass with it.

Checks

• cargo test -p falcon-core --all-targets → 70 passed, 0 failed, including the existing wind and battery campaigns.
• Shadow-stack budget holds — no new state, only a fn.
• cargo kani -p falcon-core is a no-op: this crate has no cfg(kani) code at all, which is itself part of what A sustained geofence breach actuates RTL for ONE 4 ms tick, then demotes it — the breach re-fires Failsafe every tick #562 records.

Not fixed here, deliberately

rtl_latched is still never cleared, so NoFailsafeLatched blocks re-arming permanently. FSAFE-P01 says the latch resets "on disarm"; choosing that reset point is a separate behaviour decision, not a drive-by.

Refs #562, #558

🤖 Generated with Claude Code

https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG

[github-actions]

✅ Rivet verification gate — falcon

174/174 passed

count
Passed	174
Failed	0
Skipped (bench-only — needs hardware / sim)	21
Skipped (no steps)	12

Bench-only artifacts (not run by CI)

• FV-FALCON-ARCH-001 — spar AADL architectural model — falcon cascade (v0.13)
• 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-COV-002 — cargo-llvm-cov statement coverage — workspace-wide (v0.14.0)
• FV-FALCON-COV-003 — witness MC/DC on real Rust source — Geofence subject (v0.14.1)
• FV-FALCON-GEO-003 — Geofence safety path — miri UB/overflow check (v0.12, AI substitute)
• FV-FALCON-LYAP-002 — Strict (cross-term) Lyapunov — exponential-decay inequality + CI-gated Lean proofs (v1.105)
• FV-FALCON-LYAP-004 — Lyapunov exponential convergence — the deferred 'trajectory ⇒ converges' step, discharged (v1.107)
• FV-FALCON-MATHF32-003 — MATHF32-P03 — machine-checked (Gappa→Flocq→coqc) rounding bound for the f32 sin polynomial (v1.127)
• FV-FALCON-MATHF32-004 — MATHF32-P04 — machine-checked (Coq-Interval) approximation bound for the f32 sin polynomial (v1.128)
• FV-FALCON-MATHF32-005 — MATHF32-P05 — machine-checked rounding + approximation bounds for the f32 cosine kernel (v1.129)
• FV-FALCON-MELD-001 — meld-fuse the verified cascade into a single module (v1.5.0)
• FV-FALCON-OCI-001 — OCI-P01 — signed per-component publish, WASI-free build, and through-wasm closed-loop proof (v1.129)
• FV-FALCON-SIM-001 — PX4-SITL end-to-end loop — recipe + preset + smoke (v0.14.0)
• FV-FALCON-SIM-005 — gz-transport NavSat + Home projection — position-dependent loops (v0.18.1)
• FV-FALCON-TARGET-001 — Verified flight core as a bare-metal ARM Cortex-M ELF + sim backend (v1.6.0)
• FV-FALCON-WASMCM-001 — Verified flight core runs in wasmtime as a CM component (v1.26.0)
• FV-FALCON-WASMCM-002 — All 8 falcon CM components build and bundle script emits versioned dist/ (v1.56)
• FV-FALCON-WCET-001 — Compositional WCET + flight-cascade schedulability, kernel-checked (v1.10.0)
• FV-FALCON-WIT-001 — Verified IEKF componentized + plugged into the composed cascade (v1.4.0)
• FV-RELAY-KANICI-003 — Orphaned-proof sweep completed — flight-support + HAL + infra Kani harnesses enforced in CI (v1.108)

Source of truth: artifacts/verification/FV-FALCON-*.yaml.