Gazebo flight-core revival + rotor-out recovery that actually holds (v1.113–v1.114)

artifacts/verification/FV-FALCON-FAULT-003.yaml

@@ -0,0 +1,108 @@
+artifacts:
+  - id: FV-FALCON-FAULT-003
+    type: sw-verification
+    title: "Single-rotor-out FULL-LOOP recovery — parasitic-free rank-3 allocation + production-core spin-descent oracle (v1.114)"
+    status: implemented
+    release: falcon-v1.114.0
+    description: >
+      Strengthens FV-FALCON-FAULT-002. That artifact verified the
+      rotor-out chain only in an IDEALISED attitude-only harness
+      (falcon-sitl-gz fault_tolerance_chain_recovers_from_rotor_loss:
+      constant hover thrust, TRUE-state feedback, level b3_d) — under
+      which the recovery merely leans and stays < 80°. The FULL
+      production loop (IEKF estimator + altitude loop + the FDI
+      attitude/rate gate) was never exercised, and it did NOT actually
+      recover: it flipped to ~180° (reproduced on the real gz plant and,
+      now, offline). v1.114 finds the cause, fixes it, and adds the
+      first full-loop recovery oracle.
+
+      ROOT CAUSE (mechanically proven, no sim needed).
+      The reconfigured allocator reused the 4-rotor MIXER_X rows with the
+      failed rotor zeroed. Zeroing one rotor breaks the zero-sum property
+      of each torque column, so the collective THRUST leaks into
+      roll/pitch — a parasitic body moment ≈ collective toward the dead
+      corner. At hover (collective 0.585) that is roll +0.585 / pitch
+      −0.585 (58% of full authority) at ZERO commanded torque. The
+      reduced-attitude law can only oppose it from a growing tilt; once
+      the altitude loop raises thrust to replace the lost lift the
+      parasitic grows too → runaway → flip.
+        - Test: relay-mix-quad mix_p08_rotor_out_zero_torque_has_no_parasitic_moment
+          (asserts produced roll/pitch ≈ 0 at zero command, for every
+          failed index — the guard that would have caught this).
+
+      FIX — RANK-3 allocation (MIX-P08, v1.114).
+      mix_rotor_out now SOLVES the 3×3 system for the three healthy rotor
+      commands that produce exactly (collective, roll, pitch), yaw free,
+      via a collective base + a zero-collective moment delta scaled by the
+      existing scale_to_fit desaturation (so moment DIRECTION and
+      collective are preserved and a clamp cannot flip a moment's sign).
+      This kills the diagonal-opposite rotor and drives the through-CoM
+      pair: pure lift, zero parasitic tilt, controlled yaw spin. Floor
+      lowered to 0 (the opposite rotor legitimately rests at 0). A
+      TAU_BOUND input clamp keeps the Cramer solve below f32 overflow.
+        - Kani: verify_mix_rotor_out_bound VERIFICATION SUCCESSFUL
+          (0 of 377 checks failed) — the MIX-P08 bound (failed rotor 0,
+          healthy ∈ [floor,1], all finite, yaw relinquished) still holds
+          for ANY input and ANY failed index < 4 under the new solve.
+        - Tests: relay-mix-quad
+          mix_p08_rotor_out_preserves_moment_direction (produced moment is
+          s·commanded for s∈[0,1] — parallel, no sign flip, no overshoot),
+          mix_p08_rotor_out_small_command_is_exact (feasible small command
+          realised exactly), mix_p08_rotor_out_pins_failed_and_bounds_healthy.
+
+      FULL-LOOP RECOVERY ORACLE (the gap FV-002 left).
+      falcon-core survives_single_rotor_failure_without_flipping flies the
+      PRODUCTION FlightCore (verified IEKF → geometric SE(3) →
+      reduced-attitude + rank-3 allocation, driven by the real FDI on ESC
+      RPM) on the analytic rigid-body plant. After a rotor-0 loss from a
+      settled hover the FDI isolates within a step, and the vehicle holds
+      the thrust axis near-level (peak tilt < 0.5 rad; steady descent
+      < ~6°), keeps the relinquished-yaw spin bounded (< 10 rad/s), and
+      lands near-upright (touchdown tilt < 0.35 rad) — a controlled
+      spin-descent, not a tumble.
+
+      DISPERSED GUARD — closing the campaign blind spot (v1.114).
+      The Monte-Carlo `run_motor_out_campaign` dispersed over the SAME
+      idealised attitude-only sim as FV-002 (its header says so), so
+      thousands of trials could not falsify the flip — dispersion adds
+      breadth, not fidelity. New `run_fullloop_motor_out_campaign` disperses
+      200 trials over the FULL production FlightCore (IEKF + altitude + FDI +
+      rank-3 allocation, rot_drag plant) across failed-rotor, hover altitude,
+      rotational drag, and sensor-noise axes, asserting no-flip + bounded
+      spin + correct FDI + no-NaN. Measured worst case: peak tilt 0.274 rad,
+      yaw 5.7 rad/s, FDI detect 5 steps, 0/200 failures. A parasitic-moment
+      regression drives peak tilt toward π and trips this guard — the guard
+      the idealised campaign could not provide. (Altitude after the loss is
+      the FlightSupervisor's LAND job — reported, not gated, here.)
+
+      PLANT FIDELITY (v1.114).
+      SimBackend gains quadratic ROTATIONAL aero drag (rot_drag, τ =
+      −c·ω·|ω|, opt-in like drag_quad/wind/turbulence, default off).
+      Without it the analytic plant has no torque to oppose the rotor-out
+      yaw reaction (both surviving lift rotors share a spin sense), so the
+      spin runs away and corrupts the estimator; real air bounds it. This
+      is why the idealised FV-002 harness (no estimator, constant thrust)
+      never saw the failure. SimBackend also gains fail_rotor + a
+      read_motor_rpm implementation so the same rigid-body plant now
+      exercises the FDI + recovery end to end.
+
+      FALSIFICATION: this recovery is wrong if a single-rotor-out from a
+      settled hover is observed to exceed ~45° tilt, spin past ~10 rad/s,
+      or fail to reach a near-upright landing — on the analytic plant
+      (this oracle) or the gz plant.
+    tags: [verification, falcon, fault-tolerance, rotor-loss, control-allocation, kani, full-loop, v1.114]
+    fields:
+      method: formal-verification
+      steps:
+        - run: cargo kani -p relay-mix-quad --harness verify_mix_rotor_out_bound
+        - run: cargo test -p relay-mix-quad mix_p08_rotor_out_zero_torque_has_no_parasitic_moment
+        - run: cargo test -p relay-mix-quad mix_p08_rotor_out_preserves_moment_direction
+        - run: cargo test -p relay-mix-quad mix_p08_rotor_out_small_command_is_exact
+        - run: cargo test -p falcon-core survives_single_rotor_failure_without_flipping
+        - run: cargo test -p falcon-sitl-gz fullloop_motor_out_monte_carlo_campaign
+        - run: cargo test -p falcon-sitl-gz fault_tolerance_chain_recovers_from_rotor_loss
+    links:
+      - type: verifies
+        target: SWREQ-FALCON-FAULT-P02
+      - type: refines
+        target: FV-FALCON-FAULT-002

artifacts/verification/FV-FALCON-SITLCORE-001.yaml

@@ -0,0 +1,74 @@
+artifacts:
+  - id: FV-FALCON-SITLCORE-001
+    type: sw-verification
+    title: "FlightCore-in-the-loop — the production core flies the SITL plant through the FlightBackend seam (v1.113)"
+    status: implemented
+    release: falcon-v1.113.0
+    description: >
+      Closes the orphaned-core gap in the Gazebo SITL bench: every prior
+      `run_*` scenario re-implemented the flight cascade by hand against the
+      example's `Physics` plant, so the sim exercised a PARALLEL controller, not
+      the one that ships. This verification flies the PRODUCTION
+      `falcon_core::FlightCore` (the verified IEKF → geometric-SE(3) → ADRC →
+      mixer cascade with the single-rotor-out FDI + degraded-allocator recovery)
+      through the SITL plant via an ADAPTER — `SitlBackend`
+      (examples/falcon-sitl-gz/src/flightcore.rs), which implements
+      falcon-core's `FlightBackend` seam on top of a `&mut dyn Physics` plant.
+      The same byte-for-byte core that targets real hardware now flies the sim
+      (mock today; the real Gazebo 6-DOF plant under `--features gazebo`,
+      `--scenario=flightcore`).
+
+      Seam reconciliation: `FlightBackend` is a sensor/actuator port (the core
+      pulls sensors, pushes motors); `Physics` is a plant (push motor PWMs +
+      step(dt), then measure()). The adapter advances the plant inside
+      write_motors — the tail of one FlightCore::step — so each control tick is
+      exactly one physics step in causal order (sense state(t) → decide →
+      actuate-and-advance to state(t+dt)). GNSS fixes are offered at 5 Hz
+      (divisor 50 @ 250 Hz), so the core dead-reckons on the IMU between fixes
+      exactly as against a real receiver.
+
+      SUPPORTING CORRECTNESS FIX (MockPhysics): the toy plant previously
+      reported a CONSTANT [0,0,−g] accelerometer, which starves a full IEKF's
+      vertical-velocity estimate (the filter's process model says "not
+      accelerating" while GNSS says "climbing" → the two fight into a lag →
+      runaway climb, measured 704 m off before the fix). An accelerometer
+      measures SPECIFIC FORCE (a_kinematic − g_gravity); MockPhysics now reports
+      the true NED specific force (thrust − drag) rotated into the body frame —
+      faithful, and backward-compatible at hover/level where it reduces to the
+      old [0,0,−g] constant (the near-level hand-cascade scenarios and the
+      existing IMU unit tests are unchanged).
+
+      GATE 1 (production_flightcore_holds_altitude_through_sitl_plant): the
+      shipping FlightCore commanded a 2 m altitude hold through the plant and
+      settled within 0.5 m with < 1.0 m steady RMS — the same bar as the
+      hand-rolled altitude scenario, met by the code that flies rather than a
+      bench re-implementation. Measured: final 0.04 m, steady RMS 0.06 m, no
+      NaN/divergence.
+
+      GATE 2 (production_flightcore_fdi_isolates_failed_rotor_through_sitl_seam):
+      the single-rotor-out FDI fires THROUGH the SITL seam. The seam gained a
+      per-rotor RPM channel (Physics::motor_rpm) + a fault-injection hook
+      (Physics::fail_rotor), and the adapter now forwards read_motor_rpm — before
+      this the FDI was INERT in SITL (no ESC telemetry reached the core). A rotor
+      is failed mid-flight; the mock reports it at 0 RPM; the core's
+      commanded-vs-achieved CUSUM (relay-iekf RotorFaultDetector) isolates
+      EXACTLY the failed rotor (verified for rotors 0 and 2). This gates the
+      telemetry PLUMBING the recovery depends on. Full falcon-sitl-gz suite
+      29/29 green.
+
+      Honest scope: the mock plant responds to collective thrust only
+      (differential-motor torque is approximated as zero), so it can prove FDI
+      ISOLATION (the RPM residual) but NOT the 3D tilt-recovery or a post-failure
+      altitude hold — those need the full-physics `--features gazebo` backend
+      (the recordable `--scenario=flightcore-rotorout` flight, now reachable via
+      this seam, is the next slice).
+    tags: [verification, falcon, simulation, sitl, flightcore, hal, seam, v1.113]
+    fields:
+      method: simulation
+      steps:
+        - run: "cargo test -p falcon-sitl-gz production_flightcore  # bench-only (builds the campaign suite; runs in the closed-loop-sim CI job + workspace test)"
+    links:
+      - type: verifies
+        target: SWREQ-FALCON-HAL-P01
+      - type: verifies
+        target: SWREQ-FALCON-FAULT-P02