feat(falcon): v1.123 — float discipline: CI f64 gate + IEKF variance floor - #285
Merged
Conversation
…floor (SWDD-FALCON-FLOAT-001) An external review asked whether the floats should be 64- or 32-bit. The honest answer: f32 in the flight core is the REQUIREMENT (the M4's FPv4-SP has no double-precision hardware; PX4/ArduPilot fly f32 EKFs; f64 would break CBMC tractability), and f64 belongs at exactly one place — geodetic absolutes, where f32 degrees quantize at ~0.6 m. The codebase already followed this everywhere; this slice turns the convention into an enforced rule and closes the one genuine risk the review surfaced. - scripts/check-float-discipline.sh (new, wired into CI): denies the f64 token in the 21 flight-partition crates' non-test code; a file opts out only via a visible header annotation — today exactly one, falcon-mavlink's geodetic boundary (now annotated). Green on the current tree: the flight core was already f64-free. - relay-iekf floor_variances (the review's real finding): the cheap standard-form update P <- (I-KH)P can round an f32 diagonal NEGATIVE; symmetrise() cannot see that. Every measurement update now heals diagonals into [1e-9, 1e6] with corrupt-row correlations zeroed and a LOUD counter (Iekf::variance_floor_hits — zero across all existing campaigns; a guard, not a crutch). The Kani post-condition harness CAUGHT the first version: +infinity passed the naive `d >= FLOOR` check, and an infinite diagonal must heal to the CEILING (maximal uncertainty), never the floor (fabricated certainty). 4/4 harnesses verified; 29 iekf + 56 falcon-core tests green including a 50k-cycle zero-hits healthy-run assertion. - SWDD-FALCON-FLOAT-001 (implemented) records decision + rationale + enforcement. SCOPE MOVE, surfaced: PART-P01/P02 (blocked on synth #708/#369) bumped falcon-v1.123.0 -> v1.124.0; v1.123 is this slice. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG
CI caught what the local run could not: BSD awk has no \y word boundary — the pattern silently matched NOTHING on macOS, so the local "OK" was vacuous while CI's gawk found a real hit (falcon-mavlink keeps its tests in a separate tests.rs, outside the cfg(test)-to-EOF exemption). Portable character-class boundary now; tests.rs skipped like kani_proofs.rs; and the oracle is negative-tested (a seeded f64 at file top FAILS the gate locally, clean tree passes). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG
avrabe
added a commit
that referenced
this pull request
Jul 16, 2026
Code-free promotion per the two-commit rule. Evidence on merged main (be4cac3, impl PR #285 merged on a fully green rollup — including the new float gate itself, which caught its own BSD-awk vacuity and a separate-tests-file gap before landing): - Gate green in CI + negative-tested (seeded f64 fails it); one annotated boundary (falcon-mavlink geodetic). - Kani post-condition proof 4/4 (the harness caught +∞ escaping the naive floor — infinite variance heals to the CEILING, never the floor); 29 iekf + 56 falcon-core tests; 50k-cycle zero-hit run. New SWREQ-FALCON-FLOAT-P01 (the enforced property; FV artifacts verify sw-reqs per schema) + FV-FALCON-FLOAT-001; SWDD-FALCON-FLOAT-001 stays the implemented design record. Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Verify-Filter: (has-tag "v1.123")
Implements SWDD-FALCON-FLOAT-001 (→
implemented; verify PR follows per the two-commit rule) — the f32/f64 review raised by external feedback, turned into an enforced rule plus one real hardening.The decision (now recorded + enforced, not tribal)
f32 in the flight core is the requirement, not the compromise: the estimator partition targets the RT1176 Cortex-M4 (FPv4-SP — no double-precision hardware; f64 = soft-float WCET blow-up), PX4 EKF2 / ArduPilot NavEKF3 fly f32 with the same mitigations we carry, and f64 would push existing CBMC proof suites past tractability. f64 belongs at exactly one class of site: geodetic absolutes (f32 latitude quantizes at ~0.6 m) — already correctly f64 in falcon-mavlink and the gz bridge, casting only local NED deltas down.
scripts/check-float-discipline.shruns in CI: deniesf64in the 21 flight-partition crates' non-test code; opt-out only via a visible file-header annotation (float-discipline: allow-f64 (<why>)— today exactly one: falcon-mavlink's geodetic boundary). Test/kani regions exempt — oracles should be f64. Green on the current tree: the audit confirmed the flight core was already clean.The review's real finding: covariance floor
relay-iekf uses the cheap standard-form update
P ← (I−KH)P; in f32 a strong update can round a diagonal negative, andsymmetrise()can't see it. Newfloor_variances()after every measurement update:[1e-9, 1e6], corrupt-row correlations zeroed, every event counted loudly (variance_floor_hits— zero across all existing campaigns: a guard, not a crutch).d >= FLOORcheck — and the correct heal for an infinite variance is the ceiling (maximal uncertainty), never the floor (fabricated certainty).Gates
relay-iekf 29 (3 new: negative-diag heal + correlation zeroing, NaN heal, 50k-cycle zero-hits healthy run) + falcon-core 56 + falcon-mavlink 16, 0 fail ·
cargo kanirelay-iekf 4/4 (new post-condition harness: any input incl. NaN/±∞ → every diagonal finite, in-range) · clippy-D warningsclean ·rivet validatePASS.Scope move, surfaced: PART-P01/P02 (blocked on synth #708/#369) re-scoped
falcon-v1.123.0 → v1.124.0; v1.123 is this slice.🤖 Generated with Claude Code
https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG