feat(falcon): v0.19.9 — verified arming sequencer (ARM-P01) + tip-over localization

Cargo.toml

@@ -26,6 +26,7 @@ members = [
     "crates/relay-rate",
     "crates/relay-att",
     "crates/relay-mix-quad",
+    "crates/relay-arm",
     "crates/relay-pos",
     "examples/falcon-hello",
     "examples/falcon-ekf-bench",

artifacts/features/FEAT-FALCON-rollout.yaml

@@ -2132,6 +2132,78 @@ artifacts:
       - type: depends-on
         target: FEAT-FALCON-v0.19.7
 
+  - id: FEAT-FALCON-v0.19.9
+    type: feature
+    title: "v0.19.9 — verified arming sequencer (ARM-P01) + tip-over localization"
+    status: approved
+    description: >
+      LANDED. Ships relay-arm, a Kani-verified startup state machine
+      (Disarmed → SpinUp → LevelHold → Armed) that gates attitude-torque
+      authority: the rate loop's torque reaches the mixer ONLY in Armed,
+      and Armed is reachable ONLY through a confirmed-level window. It
+      replaces the bench's ad-hoc time-only `t < 0.5 s` spawn-hold with
+      verified time+level gating — the "deterministic startup sequencing"
+      called for as fix (1) in the v0.19.7 bistability diagnosis.
+
+      Verification — Kani, not Verus (the tilt compare is f32; like
+      relay-mix-quad this is off the integer Verus track). The gating
+      invariant is INDUCTIVE over one tick(), so the bounded check covers
+      all input sequences:
+        cargo kani verify_arming_torque_gated → 143 checks SUCCESSFUL
+          (torque_authority ⟺ Armed; a new entry into Armed comes only
+           from LevelHold with the level gate satisfied; phase ∈ [0,3];
+           thrust_scale ∈ [0,1] finite)
+        cargo kani verify_arming_total → 137 checks SUCCESSFUL
+          (panic-free + thrust bounded for NaN/∞ tilt, zero spin-up)
+      Plus proptest + unit tests (5/5): torque-gated-until-level,
+      tilt-resets-count, NaN-never-arms, monotonic spin-up ramp.
+
+      FALSIFICATION (the empirical value): I set out to "kill RC#1
+      startup tip-over" — the gz data falsified that framing. With the
+      correct NavSat home, the gated AND ungated startups both hand off a
+      LEVEL body (0° through arming at 0.40 s); the body then holds level
+      ~3.5 s and only tips (~88°) once the position loop dominates. The
+      tip-over is a DOWNSTREAM residual (relay-pos thrust normalisation +
+      RC#3 EKF-attitude-during-accel), not a spawn transient. The arming
+      sequencer is verified, correct, and a prerequisite building block —
+      but it is NOT what unblocks position-hold. Publishing this localizes
+      the v0.19.10+ target precisely.
+
+      Ships:
+        - crates/relay-arm: ArmingSequencer + ArmingConfig + Kani
+          harnesses + tests (new workspace member).
+        - examples/falcon-sitl-gz: sequencer wired into alt-rate AND the
+          full closed-loop cascade (which also adopts mix_thrust_floor);
+          body_tilt_rad helper; `arming` / `arming-ungated` diagnostic
+          scenarios.
+        - SWREQ-FALCON-ARM-P01 + FV-FALCON-ARM-001.
+        - bench-evidence/gz-sim/2026-05-29-v0.19.9-*.md.
+
+      Verification:
+        - cargo kani (both harnesses) → SUCCESSFUL.
+        - cargo test --workspace → green; relay-arm 5/5; falcon-sitl-gz
+          10/10.
+        - gz bench REGRESSION GATE → alt-rate 3/3 PASS at ≈0.20 m (the
+          v0.19.8 reliable hover is unaffected by wiring in the sequencer).
+        - gz bench → arming clean handoff (0° through arming).
+        - rivet validate → PASS.
+
+      Honestly NOT claimed: that arming makes full position-hold hover
+      (it does not — run_peak ~88°), nor that a gz "arming-check PASS"
+      means the quad hovers (the PASS is scoped to the startup handoff).
+      Full position-hold remains the residual, now localized to relay-pos
+      thrust + RC#3 for v0.19.10+.
+    tags: [falcon, milestone, v0.19.9, arming, sequencer, kani, falsification, landed]
+    fields:
+      release-target: "verified arming sequencer + position-hold tip-over localization"
+      bench-date: "2026-05-29"
+      verification: "Kani BMC (143 + 137 checks), inductive per tick — appropriate for the f32 tilt compare"
+      bench-result: "alt-rate 3/3 PASS ≈0.20 m (no regression); arming clean handoff; tip localized to RC#3"
+      falsification: "startup tip-over does not reproduce at spawn; tip is downstream (relay-pos thrust + RC#3)"
+    links:
+      - type: depends-on
+        target: FEAT-FALCON-v0.19.8
+
   - id: FEAT-FALCON-v1.0
     type: feature
     title: "v1.0 — six-domain credit dossier + airframe variants"
@@ -2168,4 +2240,4 @@ artifacts:
       - type: implements
         target: SYSREQ-FALCON-010
       - type: depends-on
-        target: FEAT-FALCON-v0.19.8
+        target: FEAT-FALCON-v0.19.9

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

@@ -0,0 +1,60 @@
+artifacts:
+  - id: SWREQ-FALCON-ARM-P01
+    type: sw-req
+    title: "ARM-P01: Verified arming sequencer gates attitude-torque authority"
+    status: approved
+    description: >
+      The flight stack shall provide an arming sequencer
+      (`relay-arm::ArmingSequencer`) that gates attitude-torque
+      authority through an explicit startup state machine:
+
+        Disarmed → SpinUp → LevelHold → Armed
+
+      Attitude-torque authority (the rate loop's torque applied to the
+      mixer) shall be enabled ONLY in the Armed phase, and the Armed
+      phase shall be reachable ONLY through LevelHold after the measured
+      body tilt has stayed below a configured threshold for a configured
+      number of consecutive ticks (the level gate). Equivalently:
+      torque authority can never be granted unless the body was first
+      confirmed level. A NaN/non-finite tilt estimate shall never count
+      as level (it can never arm the vehicle). The collective-thrust
+      scale output shall be in [0, 1] and finite in every phase.
+
+      Rationale: this replaces the pre-v0.19.9 bench's ad-hoc, time-only
+      `t < 0.5 s` spawn-hold, which engaged the rate loop at a fixed time
+      regardless of body state (a quad that spawned tilted, or was
+      bumped during spin-up, would have torque engaged into a bad
+      attitude). The sequencer gates on time AND confirmed-level, and
+      its gating is mechanically proven. It is the "deterministic
+      startup sequencing (arm → spin-up → release)" called for as fix
+      (1) in the v0.19.7 bistability diagnosis.
+
+      Scope honesty: ARM-P01 is a startup-gating safety property. It is
+      NOT a position-hold guarantee. The v0.19.9 gz bench confirms the
+      gated startup hands off a level body (0° tilt through arming and
+      well beyond), but the full position-hold cascade still tips later
+      (~88° peak) due to a downstream residual (relay-pos thrust
+      normalisation + RC#3 EKF-attitude-during-accel). The arming
+      sequencer cannot fix a downstream cascade instability and does not
+      claim to; that residual is tracked for v0.19.10+.
+    tags: [falcon, arming, sequencer, safety, kani, startup]
+    fields:
+      req-type: safety
+      priority: must
+      verification-criteria: >
+        Kani BMC proof (the tilt compare is f32; like relay-mix-quad the
+        sequencer is off the integer-only Verus track): the torque-gating
+        invariant is inductive over one tick(), so the bounded check
+        covers all input sequences. Harnesses verify_arming_torque_gated
+        (torque_authority ⟺ phase==Armed; a new entry into Armed comes
+        only from LevelHold with the level gate satisfied; phase ∈ [0,3];
+        thrust_scale ∈ [0,1] finite) and verify_arming_total (panic-free
+        + thrust bounded for NaN/∞ tilt and zero spin-up). Plus proptest
+        arm_p01_property_torque_implies_armed and unit tests
+        (torque-gated-until-level, tilt-resets-count, NaN-never-arms,
+        monotonic spin-up ramp). gz: alt-rate reliable hover unaffected
+        (3/3 PASS at ~0.20 m); arming-check clean handoff (0° through
+        arming).
+    links:
+      - type: derives-from
+        target: SYSREQ-FALCON-002

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

@@ -0,0 +1,87 @@
+artifacts:
+  - id: FV-FALCON-ARM-001
+    type: sw-verification
+    title: "ARM-P01 arming-sequencer gating — Kani BMC proof + gz handoff evidence + tip-over localization (v0.19.9)"
+    status: approved
+    description: >
+      Verifies SWREQ-FALCON-ARM-P01: the `relay-arm::ArmingSequencer`
+      gates attitude-torque authority so the rate loop's torque is
+      applied ONLY after a confirmed-level startup, never before.
+
+      Why Kani, not Verus: the only float in the machine is the tilt
+      threshold compare; the rest is integer phase/counter logic. Like
+      relay-mix-quad (f32) this is plain Rust + Kani (CBMC) + proptest,
+      not the integer-only Verus track. The gating invariant is
+      INDUCTIVE over a single tick(), so Kani's bounded check (arbitrary
+      in-invariant state + arbitrary input, prove the invariant is
+      preserved) covers all input sequences of any length.
+
+      Kani proof (cargo kani, crates/relay-arm/plain):
+        - verify_arming_torque_gated (143 checks, SUCCESSFUL):
+            torque_authority ⟺ phase==Armed; a NEW entry into Armed
+            comes only from LevelHold with level_count+1 ≥ required (the
+            RC#1-gate — torque can never engage before confirmed level);
+            phase ∈ [0,3]; thrust_scale ∈ [0,1] and finite.
+        - verify_arming_total (137 checks, SUCCESSFUL): tick() is
+            panic-free and thrust_scale stays in [0,1] finite even for
+            NaN/∞ tilt and a zero spin-up duration.
+
+      Supporting evidence:
+        - proptest arm_p01_property_torque_implies_armed (across
+          arbitrary tick/arm sequences) + unit tests: torque-gated-
+          until-level-confirmed, tilt-resets-level-count, NaN-never-arms,
+          monotonic spin-up ramp. cargo test -p relay-arm → 5/5.
+        - body_tilt_rad geometry unit test (falcon-sitl-gz) → matches
+          atan2(|horizontal|,|vertical|) at 0/45/90°.
+        - gz bench (bench-evidence/gz-sim/2026-05-29-v0.19.9-*.md):
+            * REGRESSION GATE: --scenario=alt-rate, 3/3 consecutive PASS
+              at final_dist≈0.20 m, rms≈0.21 m / 30 s — the v0.19.8
+              reliable hover is unaffected by wiring in the sequencer.
+            * --scenario=arming: clean gated handoff (handoff_peak=0.0°
+              through arming at 0.40 s); whole-run peak ~88° is the
+              DIAGNOSTIC of the downstream residual.
+
+      Falsification finding (the empirical value of this bench):
+        The v0.19.7 "startup tip-over" (RC#1) does NOT reproduce as a
+        startup transient. The gated AND ungated startups both hand off a
+        level body (0° through arming); the body then holds level for
+        ~3.5 s and only tips once the position loop dominates. The
+        tip-over is therefore a DOWNSTREAM position-hold residual
+        (relay-pos thrust normalisation + RC#3 EKF-attitude-during-accel),
+        not a spawn transient. The arming sequencer is verified, correct,
+        and a prerequisite safety building block — but it is NOT what
+        unblocks full position-hold. This sharpens the v0.19.10+ target.
+
+      Verification:
+        - cargo kani --harness verify_arming_torque_gated → SUCCESSFUL.
+        - cargo kani --harness verify_arming_total → SUCCESSFUL.
+        - cargo test -p relay-arm → 5/5.
+        - cargo test -p falcon-sitl-gz → 10/10.
+        - cargo test --workspace → green.
+        - gz bench → alt-rate 3/3 PASS; arming clean handoff.
+        - rivet validate → PASS.
+
+      Honestly NOT claimed:
+        - That the arming sequencer makes full position-hold hover. It
+          does not (run_peak ~88°); the residual is downstream and
+          deferred to v0.19.10+.
+        - That a gz "arming-check PASS" means the quad hovers. The PASS
+          is explicitly scoped to the startup HANDOFF (label
+          "PASS ✓ (handoff)" + a NOTE reporting the whole-run tip).
+        - That Verus proves this. It can't (float tilt compare); Kani
+          does, BMC-complete over the bounded domain, inductive per tick.
+    tags: [falcon, arming, sequencer, kani, bmc, startup, falsification, v0.19.9]
+    fields:
+      runs:
+        - "cargo kani --harness verify_arming_torque_gated  (143 checks, SUCCESSFUL)"
+        - "cargo kani --harness verify_arming_total  (137 checks, SUCCESSFUL)"
+        - "cargo test -p relay-arm  (5/5)"
+        - "cargo test -p falcon-sitl-gz  (10/10)"
+        - "gz bench --scenario=alt-rate  (3/3 PASS, final≈0.20 m — regression gate)"
+        - "gz bench --scenario=arming  (clean handoff 0°; run_peak ~88° = downstream residual)  # bench-only"
+      tool: "Kani (CBMC) — inductive single-tick proof; appropriate for the f32 tilt compare; Verus is integer-only here"
+      bench-result: "alt-rate 3/3 PASS final≈0.20 m (no regression); arming clean handoff, position-hold tip-over localized to RC#3"
+      falsification: "startup tip-over does not reproduce at spawn; tip is downstream (relay-pos thrust + RC#3)"
+    links:
+      - type: verifies
+        target: SWREQ-FALCON-ARM-P01

bench-evidence/gz-sim/2026-05-29-v0.19.9-arming-sequencer-and-tipover-localization.md

@@ -0,0 +1,101 @@
+# v0.19.9 — verified arming sequencer + tip-over localization
+
+Date: 2026-05-29
+Backend: Gazebo Harmonic (gz sim 8.11.0), headless `gz sim -s -r`
+World: `examples/falcon-sitl-gz/worlds/falcon-quad.sdf`
+Home: `--home=47.3977,8.5456,488` (matches the SDF `<spherical_coordinates>`
+elevation — see the methodology note below; omitting it is a -488 m trap).
+
+## What shipped
+
+`relay-arm` — a Kani-verified arming state machine that gates
+attitude-torque authority:
+
+```
+Disarmed ──arm──▶ SpinUp ──spinup_ticks──▶ LevelHold ──level gate──▶ Armed
+(torque off,      (thrust ramp,            (thrust 1,                (torque ON)
+ thrust 0)         torque off)              torque off,
+                                            count consecutive
+                                            below-θ-tilt ticks)
+```
+
+It replaces the bench's ad-hoc time-only `t < 0.5 s` spawn-hold (which
+engaged the rate loop at a fixed time regardless of body state) with
+time AND confirmed-level gating. Wired into the alt-rate path and the
+full closed-loop cascade.
+
+## Verification (Kani — the real gate)
+
+The torque-gating invariant is **inductive over one `tick()`**, so a
+bounded check covers all (unbounded-length) input sequences:
+
+| Harness | Checks | Result |
+|---|---|---|
+| `verify_arming_torque_gated` | 143 | SUCCESSFUL |
+| `verify_arming_total` | 137 | SUCCESSFUL |
+
+`verify_arming_torque_gated` proves: `torque_authority ⟺ phase==Armed`;
+a *new* entry into Armed comes only from LevelHold with the level gate
+satisfied (torque can never engage before confirmed level); `phase ∈
+[0,3]`; `thrust_scale ∈ [0,1]` finite. `verify_arming_total` proves
+panic-freedom + thrust bounds even for NaN/∞ tilt and zero spin-up.
+Plus proptest + 5 unit tests.
+
+## gz bench
+
+### Regression gate — alt-rate reliable hover (must hold)
+
+| Run | final_dist | peak_dist | rms_steady (30 s) |
+|---|---|---|---|
+| 1 | 0.20 m | 1.98 m | 0.21 m |
+| 2 | 0.20 m | 1.98 m | 0.21 m |
+| 3 | 0.21 m | 1.98 m | 0.22 m |
+
+**3/3 PASS** — identical to v0.19.8's 4/4. Wiring in the sequencer does
+not regress the reliable attitude+altitude hover.
+
+### Diagnostic — full-cascade arming
+
+```
+arming-check[gated]:    armed_at=0.40s handoff_peak=0.0° run_peak=88.7° final=25.3°  [PASS ✓ (handoff)]
+arming-check[UNGATED]:  armed_at=0.40s handoff_peak=0.0° run_peak=83.3° final=65.2°
+```
+
+Tilt trajectory (gated): `0.0°` from t=0 through t≈3.5 s, then
+`1.3°→3.7°→7.2°→13.6°→21.6°→…→88°` while drifting horizontally to
+[2.6, −2.9] m.
+
+## The falsification finding
+
+I set out to "kill RC#1 (startup tip-over)." **The data falsified that
+framing.** The gated and ungated startups *both* hand off a perfectly
+level body (0° through arming and for ~3.5 s after). The body tips only
+once the position loop dominates. Therefore:
+
+- The tip-over is **not a startup transient** — it is a **downstream
+  position-hold residual**: `relay-pos` does not command enough thrust
+  to hold altitude on this 2 kg body (it sits, not climbs), and RC#3
+  (EKF attitude during accel) corrupts the "level" reference once it
+  does move.
+- The arming sequencer is **verified, correct, and a prerequisite
+  building block** (the v0.19.7 doc's recommended fix (1)), but it is
+  **not what unblocks position-hold**. It cannot fix a downstream
+  cascade instability and v0.19.9 does not claim it does.
+
+This is the methodology working as intended: publishing the
+wrong-prediction data localizes the v0.19.10+ target far more precisely
+than a fabricated "RC#1 fixed" would have. The next blocker is
+**relay-pos thrust normalisation + RC#3 (EKF innovation gate / accel
+down-weighting)** — the genuinely research-shaped work.
+
+## Methodology note — the −488 m NavSat trap
+
+First runs (mine) omitted `--home` and read `pos_d = −488 m` from t=0
+(the body appeared 488 m underground and inert). Falsified as
+*environmental, not a code regression* by running the committed v0.19.8
+binary through the identical launch — it produced the same −488 m. Root
+cause: the SDF world origin is at `<elevation>488.0</elevation>` (WGS84);
+without `--home=lat,lon,488` the bridge anchors NavSat→NED at
+`Home::ORIGIN` (alt 0), offsetting altitude by the full elevation. Every
+prior PASS supplied `--home=47.3977,8.5456,488`; so must every future
+run. Captured here so the trap is not re-stepped.

crates/relay-arm/Cargo.toml

@@ -0,0 +1,23 @@
+[package]
+name = "relay-arm"
+description = "Relay arming sequencer — verified startup state machine that gates attitude-torque authority until the body is confirmed level + airborne (v0.19.9)"
+version.workspace = true
+edition.workspace = true
+license.workspace = true
+repository.workspace = true
+rust-version.workspace = true
+
+[lib]
+# Cargo tests + Kani use plain/ (no Verus tree: the sequencer's only
+# float touch is the tilt-threshold compare, so it follows relay-mix-quad's
+# plain+Kani+proptest posture rather than the integer-only Verus track).
+path = "plain/src/lib.rs"
+crate-type = ["rlib"]
+
+[dependencies]
+
+[dev-dependencies]
+proptest.workspace = true
+
+[lints]
+workspace = true