Skip to content

feat(falcon): v1.120 — sag-compensated coulomb-counted battery state (BATTERY-P02) - #278

Merged
avrabe merged 1 commit into
mainfrom
feat/falcon-v1120-battery
Jul 16, 2026
Merged

feat(falcon): v1.120 — sag-compensated coulomb-counted battery state (BATTERY-P02)#278
avrabe merged 1 commit into
mainfrom
feat/falcon-v1120-battery

Conversation

@avrabe

@avrabe avrabe commented Jul 16, 2026

Copy link
Copy Markdown
Contributor

Verify-Filter: (has-tag "v1.120")

Implements BATTERY-P02 (→ implemented; verify PR follows per the two-commit rule) — the PX4 BAT1_R_INTERNAL / ArduPilot sag-compensated-failsafe parity gap: today the supervisor failsafe compares raw voltage, so a throttle punch can false-trigger RTL and a rebounding spent pack can hide.

What lands

New engine relay-batt (no_std, pure, forbid(unsafe)):

  • Coulomb-counted consumption (mAh, drift-bounded to [0, capacity]).
  • Online internal-resistance estimate from correlated V/I steps → sag-compensated resting voltage (v + i·R).
  • Conservative min-fusion of coulomb-SoC and OCV-SoC — either signal low pulls the estimate down.
  • Debounced (2 s sustained), latched low/critical flags — a pack does not un-discharge in flight.
  • Flagged voltage-only fallback when current sensing is absent: wider per-cell margins + degraded flag, surfaced via the SYS_STATUS mapping helper (health bit clears).
  • Kani BATT-K01..K03: sanitize totality (any f32 incl. NaN/∞ → finite, in-range), latch-never-clears, no-trip-without-excursion. Enrolled in the kani.yml matrix at birth. f32 arithmetic paths proptest-gated (the relay-rc split).

falcon-core wiring:

  • FlightBackend::read_battery_i seam (default None — no breakage; jess binds the PM02D ADC).
  • SimBackend current sense physically consistent with its own sag model (I = 12.5·collective A at R = 24 mΩ) + scriptable battery_i for tests.
  • FlightSupervisor runs the estimator every step; the low-battery failsafe trigger and the pre-arm battery check are now estimator-driven; battery() getter is the telemetry seam.
  • LoggingBackend forwards the current sense; TickRecord schema-v2 (logging battery samples for replay-exact failsafes) deferred to Blackbox TickRecord schema v2: log battery samples (v, i) for replay-exact BATTERY-P02 #277 — it would regenerate the shipped v1.118 golden mid-slice.

Requirement criteria → oracles

  • Sag test: 60C/300 A punch on a half-full pack sags the terminal to 8.2 V — no trip, at estimator level AND through the whole supervisor (sag_punch_does_not_trip_supervisor_failsafe); the same voltage at rest trips.
  • Integration bound: mAh error measured < 2% over a simulated 20-min flight with ±2 A zero-mean sensor noise.
  • Fallback: wider margins apply, degraded flagged, SYS_STATUS health bit clears.
  • Kani totality: BATT-K01..K03 verified (plus proptest finiteness over arbitrary bit patterns).

Existing endurance-drain and pre-arm tests now run through the estimator (compensated and fallback paths respectively); the fixed-voltage failsafe test extended past the 2 s debounce — the sustained-excursion requirement is the point of the slice.

Gates

  • cargo test -p relay-batt -p falcon-core: 9 + 49 pass, 0 fail.
  • cargo kani (relay-batt): 3/3 harnesses verified.
  • clippy -D warnings clean; rivet validate PASS.

🤖 Generated with Claude Code

https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG

…(BATTERY-P02)

Raw pack voltage lies in both directions: a throttle punch sags a
half-full pack through the failsafe threshold, and a rebounding spent
pack hides a genuine emergency. New relay-batt engine + supervisor
wiring make the failsafe act on the ESTIMATED state instead:

- relay-batt: coulomb-counted consumption (drift-bounded), online
  internal-resistance estimate from V/I steps, sag-compensated resting
  voltage, conservative min-fusion of coulomb and OCV SoC, debounced
  LATCHED low/critical flags, and a FLAGGED voltage-only fallback with
  wider per-cell margins when current sensing is absent. SYS_STATUS
  battery mapping helper (mV/cA/%, health bit). Kani BATT-K01..K03
  (sanitize totality; latch never clears; no trip without excursion);
  f32 arithmetic proptest-gated per the relay-rc split. In kani.yml.
- falcon-core: FlightBackend::read_battery_i seam (default None);
  SimBackend exposes a current sense physically consistent with its
  sag model (I = 12.5·collective A at R = 24 mΩ) plus a scriptable
  battery_i for tests; FlightSupervisor runs the estimator every step
  — failsafe trigger and pre-arm battery_ok are estimator-driven;
  battery() getter is the telemetry seam. LoggingBackend forwards the
  current sense (TickRecord schema-v2 follow-up: #277).
- Supervisor-level sag oracle: a 300 A punch sagging the terminal to
  8.2 V (far below the old 14 V raw threshold) does NOT trip; the same
  voltage sustained at rest DOES. Endurance-drain + pre-arm tests now
  run through the estimator (compensated and fallback paths).

falcon-core 49 + relay-batt 9 tests green; clippy -D warnings clean;
rivet validate PASS. SWREQ-FALCON-BATTERY-P02 → implemented (verify
PR follows per the two-commit rule).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG
@avrabe
avrabe merged commit 6bb6ebd into main Jul 16, 2026
58 checks passed
@avrabe
avrabe deleted the feat/falcon-v1120-battery branch July 16, 2026 00:44
avrabe added a commit that referenced this pull request Jul 16, 2026
…ry state (#279)

Code-free promotion per the two-commit rule. Evidence on merged main
(6bb6ebd, impl PR #278 merged on a 58/58 green rollup):
- Sag criterion at estimator AND supervisor level (300 A punch to
  8.2 V: no trip; same voltage at rest: trips).
- Coulomb error measured < 2% over a simulated 20-min noisy flight.
- Flagged voltage-only fallback with wider margins; SYS_STATUS health
  bit clears.
- Kani BATT-K01..K03 verified; relay-batt enrolled in kani.yml at birth.

New FV-FALCON-BATTERY-002 (id-grepped free; -001 taken).
SWREQ-FALCON-BATTERY-P02: implemented → verified.


Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG

Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant