feat(dronecan): v1.94 sensor ingest — float16 + esc.Status/mag/baro/battery decoders (DC-P03)

artifacts/features/FEAT-FALCON-px4-parity.yaml

@@ -0,0 +1,190 @@
+artifacts:
+  # ════════════════════════════════════════════════════════════════════
+  # PX4 everyday-multicopter parity roadmap (release-planning skill, driven
+  # by the 2026-06 PX4 gap analysis vs docs.px4.io). falcon is ~65-70% of
+  # PX4's everyday-MC feature set today and AHEAD on rigor; the missing ~30%
+  # is configurability + operational breadth, NOT flight capability. This
+  # thread closes the realistic next ~20%. status: pending = committed plan.
+  #
+  # Priority order (from the analysis): the PARAMETER SYSTEM is the keystone
+  # (unblocks autotune/calibration/UX/field-config); then the cheap high-safety
+  # predicate/limiter slices. The harder tier (autotune/multi-EKF/wind-est) is
+  # scope-after-first-flight backlog.
+  #
+  # Numbering: this thread is v1.96+ (after the DroneCAN arc v1.94/95). The
+  # legacy-RC quick wins (v1.90/91) stay low-priority filler. Numbers are
+  # labels; the dependency/priority is in the descriptions.
+  # ════════════════════════════════════════════════════════════════════
+
+  # ---- Tier 1: the committed next-20% (highest leverage × feasibility) ----
+
+  - id: FEAT-FALCON-v1.96
+    type: feature
+    title: "v1.96 — Parameter system (the keystone): typed bounded param store + MAVLink PARAM binding"
+    status: pending
+    description: >
+      PLANNED. The single highest-leverage gap vs PX4 (gap-analysis #1). PX4 has
+      hundreds of typed, persisted, GCS-readable/writable parameters; falcon tunes
+      via code constants. Without a param store you cannot field-tune gains, run
+      calibration, set geofence/battery thresholds, or integrate QGC — autotune,
+      calibration, and UX shaping ALL presuppose it.
+
+      A relay-fit design: a WIT-typed parameter TABLE (named, typed entries with
+      DECLARED bounds), a verified storage/serialization leaf (bounded keys +
+      range-clamped values — exactly Kani's wheelhouse), and a MAVLink
+      PARAM_REQUEST_LIST / PARAM_REQUEST_READ / PARAM_SET / PARAM_VALUE binding
+      (relay-mavlink already carries the codec pattern). The differentiator from
+      PX4: a BOUNDED param system — every value's range is proven, not
+      open-ended live-tuning.
+      Feasibility: medium effort, high leverage. DO THIS FIRST of the PX4 thread.
+    tags: [falcon, px4-parity, parameters, config, mavlink, keystone, kani, v1.96, planned]
+    fields:
+      release-target: "WIT param table + verified bounded storage leaf (Kani: key-in-range, value-clamped) + MAVLink PARAM_SET/VALUE round-trip"
+      px4-equivalent: "PX4 parameter system + QGC param panel — falcon adds proven per-param bounds (bounded, not open-ended)"
+    links:
+      - type: implements
+        target: SYSREQ-FALCON-006
+
+  - id: FEAT-FALCON-v1.97
+    type: feature
+    title: "v1.97 — Pre-arm / commander checks: arm only when preconditions provably hold"
+    status: pending
+    description: >
+      PLANNED. The #1 real-world crash-preventer (gap-analysis #2). falcon's FSM
+      proves the EXIT invariant (never-disarm-airborne); PX4's commander enforces
+      a broad ENTRY gate. Add the pre-arm predicate: gate arming on sensor health,
+      EKF convergence (NIS in-band), calibration-present, GPS-lock-for-mode,
+      battery-min, RC-present.
+      Excellent verified fit: a pure predicate over already-available health
+      signals; Kani proves "arm => all preconditions held". Hangs on the existing
+      relay-fsm. Cheap, highest safety ROI.
+    tags: [falcon, px4-parity, prearm, commander, arming, safety, fsm, kani, v1.97, planned]
+    fields:
+      release-target: "prearm_ok(health) predicate + Kani arm=>preconditions-held; relay-fsm arming gate wired to the health sources"
+      px4-equivalent: "PX4 commander pre-flight checks — falcon adds the Kani-proven arming precondition"
+    links:
+      - type: implements
+        target: SYSREQ-FALCON-011
+
+  - id: FEAT-FALCON-v1.98
+    type: feature
+    title: "v1.98 — Sensor calibration routines: accel/gyro/mag/level offsets the estimator consumes"
+    status: pending
+    description: >
+      PLANNED. An uncalibrated mag/accel diverges even a proven estimator
+      (gap-analysis #3; was under-scoped as 'validation' on the known-gaps list).
+      The guided calibration that solves bias/scale/axis-remap + board-level
+      offsets, landing them in the v1.96 param store.
+      Feasibility: medium, param-system-dependent (needs v1.96). The calibration
+      math (ellipsoid fit for mag, accel 6-orientation bias solve, gyro
+      null-rate) is verifiable leaf work; the verified estimator then consumes
+      the calibrated offsets (replacing the identity-remap placeholder).
+    tags: [falcon, px4-parity, calibration, sensors, estimator, kani, v1.98, planned]
+    fields:
+      release-target: "mag ellipsoid-fit + accel 6-orientation bias solve + gyro null (verified leaf) -> param store; estimator consumes the offsets"
+      px4-equivalent: "PX4 sensor calibration (QGC-guided) — falcon adds verified calibration math"
+    links:
+      - type: implements
+        target: SYSREQ-FALCON-018
+
+  - id: FEAT-FALCON-v1.99
+    type: feature
+    title: "v1.99 — Expanded failsafes: high-wind, motor-failure reallocation, attitude-runaway termination"
+    status: pending
+    description: >
+      PLANNED. Three failsafe responses PX4 has that the unified arbiter lacks
+      (gap-analysis #5), covering the failure classes most likely to be fatal:
+        - high-wind: a wind/tilt-saturation threshold -> RTL/land.
+        - motor-failure: an ESC current/RPM anomaly (from esc.Status, v1.94) ->
+          control-allocation reallocation (the hardest; touches relay-mix-*).
+        - attitude-runaway: a sustained-tilt-beyond-limit -> flight termination.
+      The arbiter is already unified; these are new bounded inputs + actions with
+      Kani-provable response bounds. Easy-to-medium except motor reallocation.
+    tags: [falcon, px4-parity, failsafe, high-wind, motor-failure, termination, safety, kani, v1.99, planned]
+    fields:
+      release-target: "3 new arbiter inputs+actions (high-wind/motor-fail/attitude-runaway) with Kani response-bound proofs"
+      px4-equivalent: "PX4 wind/actuator/lockdown failsafes — falcon adds proven response bounds"
+    links:
+      - type: implements
+        target: SYSREQ-FALCON-011
+
+  - id: FEAT-FALCON-v1.100
+    type: feature
+    title: "v1.100 — Position-mode UX shaping: jerk/slew limits, velocity feedforward, stick expo"
+    status: pending
+    description: >
+      PLANNED. The flight-feel niceties that make position mode professional
+      (gap-analysis #7): jerk/accel-limited smooth trajectories, velocity
+      feedforward, and stick expo/smoothing. Flight quality + pilot acceptance,
+      not safety.
+      Feasibility: easy, verified-friendly — bounded slew/jerk limiters are
+      textbook Kani-boundable leaves; the knobs live in the v1.96 param store.
+    tags: [falcon, px4-parity, position-mode, ux, slew, feedforward, kani, v1.100, planned]
+    fields:
+      release-target: "bounded jerk/slew limiters + velocity-FF + stick-expo (Kani output-bounded); knobs in the param store"
+      px4-equivalent: "PX4 MPC_* trajectory shaping + stick curves — falcon adds Kani-bounded limiters"
+    links:
+      - type: implements
+        target: SYSREQ-FALCON-006
+
+  # ---- Tier 2: harder backlog (scope AFTER first flight; not yet committed) ----
+
+  - id: FEAT-FALCON-v1.101
+    type: feature
+    title: "v1.101 — Multicopter wind estimation (airspeed-less, drag-fusion) [backlog: estimator extension]"
+    status: pending
+    description: >
+      BACKLOG (harder; scope after single-EKF flight is proven). PX4's EKF2
+      estimates MC wind via drag-specific-force fusion (no airspeed sensor);
+      falcon's IEKF carries no wind states (gap-analysis #4). A natural estimator
+      extension — the IEKF can carry wind states + a clean drag model — that
+      improves position hold in wind and ENABLES the v1.99 high-wind failsafe.
+      Medium-hard with a Lyapunov/consistency proof; a credible 'verified wind
+      estimation' differentiator.
+    tags: [falcon, px4-parity, wind-estimation, iekf, drag, backlog, harder, v1.101, planned]
+    fields:
+      release-target: "IEKF wind-state extension + drag-specific-force fusion + consistency proof; feeds the high-wind failsafe"
+      px4-equivalent: "PX4 EKF2 MC wind estimation — falcon adds a verified wind estimator"
+    links:
+      - type: implements
+        target: SYSREQ-FALCON-017
+
+  - id: FEAT-FALCON-v1.102
+    type: feature
+    title: "v1.102 — Multi-EKF instance selector / sensor voting [backlog: redundancy]"
+    status: pending
+    description: >
+      BACKLOG (medium-hard; scope after single-EKF flight). PX4 runs N EKF
+      instances on different IMU/mag combos and votes by consistency, catching
+      GRADUAL sensor degradation single-instance NIS gating sees late
+      (gap-analysis #3g/#8). falcon already has the per-instance consistency
+      metric (NIS); the missing piece is the multi-instance selector + redundant
+      sensor inputs. The selector logic is verifiable; the cost is N x estimator
+      compute + redundant hardware.
+    tags: [falcon, px4-parity, multi-ekf, voting, redundancy, fdi, backlog, harder, v1.102, planned]
+    fields:
+      release-target: "N-instance EKF selector keyed on NIS consistency (verified selector) + redundant sensor wiring"
+      px4-equivalent: "PX4 EKF2 multi-instance + sensor voting — falcon adds a verified selector over its NIS metric"
+    links:
+      - type: implements
+        target: SYSREQ-FALCON-018
+
+  - id: FEAT-FALCON-v1.103
+    type: feature
+    title: "v1.103 — In-flight PID autotune (system identification) [backlog: param-dependent, safety-sensitive]"
+    status: pending
+    description: >
+      BACKLOG (hard; param-system-dependent + safety-sensitive; scope after
+      params + calibration). PX4 runs in-flight SISO sysid (2-pole/2-zero,
+      injecting roll/pitch/yaw disturbances over ~40s) then computes gains
+      (gap-analysis #1/3a) — the single biggest USABILITY gap (lets non-experts
+      get a flyable tune). The sysid/least-squares core is verifiable leaf work,
+      but the in-air excitation + apply-on-land loop is safety-sensitive and
+      needs the v1.96 param store. Worth scoping LAST of the thread.
+    tags: [falcon, px4-parity, autotune, sysid, tuning, backlog, harder, v1.103, planned]
+    fields:
+      release-target: "SISO sysid (verified least-squares) + bounded in-air excitation + apply-on-land; gains -> param store"
+      px4-equivalent: "PX4 multicopter autotune — falcon adds verified sysid + bounded excitation"
+    links:
+      - type: implements
+        target: SYSREQ-FALCON-006

artifacts/features/FEAT-FALCON-rc-dronecan.yaml

@@ -133,8 +133,8 @@ artifacts:
 
   - id: FEAT-FALCON-v1.94
     type: feature
-    title: "v1.94 — DroneCAN sensor ingest (DC-P03): gnss.Fix2 + mag + baro + BatteryInfo decoders"
-    status: pending
+    title: "v1.94 — DroneCAN sensor ingest (DC-P03): float16 + esc.Status + mag + baro + BatteryInfo decoders"
+    status: implemented
     description: >
       PLANNED. The DroneCAN sensor-ingest decoders, completing the peripheral
       family over CAN (the SPI/I2C drivers' CAN-bus counterparts):
@@ -166,8 +166,11 @@ artifacts:
     title: "v1.95 — DroneCAN node pump (DC-P04): DroneCanNode async loop + NodeStatus heartbeat"
     status: pending
     description: >
-      PLANNED. The runtime that ties the transfer layer + decoders to the CanBus
-      seam: DroneCanNode<C: CanBus> — an async pump (mirrors UbxReader) that
+      PLANNED. Also folds in gnss.Fix2 (DTID 1063, the variable covariance-tail
+      message moved from v1.94): decode the flight-relevant fixed fields
+      (lat/lon 1e-8 deg, height, sats, fix status). Then the runtime that ties
+      the transfer layer + decoders to the CanBus seam:
+      DroneCanNode<C: CanBus> — an async pump (mirrors UbxReader) that
       reads frames, drives the TransferReassembler, dispatches completed
       transfers to the per-DTID decoders, and broadcasts the node's own
       NodeStatus heartbeat at 1 Hz. Static node-ID in this slice; the dynamic

artifacts/swreq/SWREQ-FALCON-DC-P03.yaml

@@ -0,0 +1,45 @@
+artifacts:
+  - id: SWREQ-FALCON-DC-P03
+    type: sw-req
+    title: "DC-P03: DroneCAN sensor ingest — esc.Status/mag/baro/battery decoders + float16 primitive"
+    status: implemented
+    description: >
+      Falcon shall decode the DroneCAN v0 sensor-ingest messages (the SPI/I2C
+      drivers' CAN-bus counterparts) on the v1.92 transfer layer, plus the shared
+      IEEE-754 half-precision primitive the telemetry uses:
+        - float16 (binary16) -> f32 decode (f16_to_f32): handles normals,
+          subnormals, ±inf, NaN, ±0. Decode-only (falcon reads sensor float16;
+          it never emits it). Total (pure arithmetic, no panic surface).
+        - esc.Status (DTID 1034): error_count/voltage/current/temperature/rpm/
+          power_rating/esc_index — the FDI source (multi-frame, 14-byte layout).
+        - MagneticFieldStrength (DTID 1002): ahrs_id + 3x float16 (external mag).
+        - StaticPressure (DTID 1028): float32 pressure + float16 variance (baro).
+        - BatteryInfo (DTID 1092) flight-relevant PREFIX: temperature/voltage/
+          current (the BatteryMonitor inputs over CAN; the SoC/model tail is not
+          decoded).
+
+      The architecture (spar/dronecan.aadl) gains the SensorSample data type + a
+      Decode thread; spar RTA confirms its 18us response meets the 2ms telemetry
+      deadline. The node WIT gains the sample-out port + decode export.
+
+      Behaviour (crates/relay-dronecan): every decoder returns None on a short
+      payload and NEVER panics for any bytes; esc.Status bit-fields are masked to
+      width (power_rating <= 127, esc_index <= 31); rpm sign-extends from int18.
+      The read_bits helper (non-byte-aligned esc.Status fields) is total and
+      every result < 2^nbits.
+    tags: [falcon, dronecan, sensors, esc-status, mag, baro, battery, float16, spar, kani, v1.94]
+    fields:
+      req-type: safety
+      priority: must
+      verification-criteria: >
+        relay-dronecan: float16 known-vector decode (0x3C00->1.0, 0xC000->-2.0,
+        ±inf, NaN, subnormals); esc.Status field decode + rpm sign-extend + short
+        reject; mag 3-axis, baro float32, battery prefix decode; short-payload
+        rejects. Kani DC-K08 read_bits bounded (total, result < 2^nbits — the
+        integer floor under esc.Status). The float16 VALUES + full-decoder
+        totality are proptest-fuzzed (f32 Kani-intractable). spar/dronecan.aadl
+        analyzes 0 errors with the Decode thread RTA 18us <= 2ms; node WIT in sync.
+        SCOPE: gnss.Fix2 (variable covariance tail) is the v1.95 follow-on.
+    links:
+      - type: derives-from
+        target: SYSREQ-FALCON-008

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

@@ -0,0 +1,52 @@
+artifacts:
+  - id: FV-FALCON-DC-003
+    type: sw-verification
+    title: "DroneCAN sensor ingest — float16 + esc.Status/mag/baro/battery decoders, Kani read_bits bound (DC-P03, v1.94)"
+    status: implemented
+    description: >
+      Verifies SWREQ-FALCON-DC-P03. relay-dronecan gains the float16 primitive
+      (float16.rs) and the sensor-ingest decoders (sensors.rs). Test-level
+      evidence (pulseengine.eu#89), each step a real named test/harness:
+        - float16::tests::known_half_vectors: canonical IEEE-half patterns decode
+          exactly (0x3C00->1.0, 0x4000->2.0, 0xC000->-2.0, 0x7C00->+inf, NaN).
+        - float16::tests::smallest_normal_and_subnormal: 2^-14 / 2^-24 edges.
+        - float16::proptests::decode_total_and_matches_reference: never panics
+          for ANY bit pattern; inf/NaN/finite classification is consistent.
+        - sensors::tests::esc_status_decodes_fields: error_count/voltage/current/
+          temperature/rpm at the right offsets (float16 + bit-packed rpm).
+        - sensors::tests::esc_status_rpm_negative_sign_extends: int18 rpm sign.
+        - sensors::tests::esc_status_rejects_short / short_payloads_reject_not_panic:
+          short payloads -> None, no panic.
+        - sensors::tests::mag_decodes_three_axes: ahrs_id + 3x float16.
+        - sensors::tests::baro_decodes_pressure_f32: float32 pressure + float16.
+        - sensors::tests::battery_prefix_decodes_voltage_current: the
+          BatteryMonitor inputs (temp/voltage/current) over CAN.
+        - sensors::proptests::sensor_decoders_never_panic: ALL decoders over
+          arbitrary bytes never panic; esc.Status fields within width.
+        - Kani DC-K08 verify_read_bits_bounded: the bit-reader is total and every
+          result < 2^nbits (the integer floor under esc.Status).
+      Architecture: spar analyze --root Falcon_DroneCAN::DroneCanNode.Fmu reports
+      0 errors with the Decode thread RTA 18us <= 2ms telemetry deadline;
+      wit/dronecan/node.wit (now with sample-out + decode export) in sync.
+      ORACLE: `cargo test -p relay-dronecan` green (36 tests); `cargo kani -p
+      relay-dronecan` VERIFICATION SUCCESSFUL for all eight harnesses.
+    tags: [verification, falcon, dronecan, sensors, float16, relay-dronecan, spar, kani, "v1.94"]
+    fields:
+      method: formal-verification
+      steps:
+        - run: "cargo test -p relay-dronecan float16::tests::known_half_vectors"
+        - run: "cargo test -p relay-dronecan float16::tests::smallest_normal_and_subnormal"
+        - run: "cargo test -p relay-dronecan float16::proptests::decode_total_and_matches_reference"
+        - run: "cargo test -p relay-dronecan sensors::tests::esc_status_decodes_fields"
+        - run: "cargo test -p relay-dronecan sensors::tests::esc_status_rpm_negative_sign_extends"
+        - run: "cargo test -p relay-dronecan sensors::tests::esc_status_rejects_short"
+        - run: "cargo test -p relay-dronecan sensors::tests::mag_decodes_three_axes"
+        - run: "cargo test -p relay-dronecan sensors::tests::baro_decodes_pressure_f32"
+        - run: "cargo test -p relay-dronecan sensors::tests::battery_prefix_decodes_voltage_current"
+        - run: "cargo test -p relay-dronecan sensors::tests::short_payloads_reject_not_panic"
+        - run: "cargo test -p relay-dronecan sensors::proptests::sensor_decoders_never_panic"
+        # Kani DC-K08 — gated by the kani.yml matrix (relay-dronecan entry)
+        - run: "cargo kani -p relay-dronecan --harness verify_read_bits_bounded"
+    links:
+      - type: verifies
+        target: SWREQ-FALCON-DC-P03