feat(falcon): v0.2.0 — Mahony complementary filter EKF#13
Conversation
Replaces the v0.1 stub with a real attitude estimator based on Mahony, Hamel & Pflimlin (2008) on SO(3), gravity-only correction. no_std + libm, suitable for the embedded synth→gale path. What lands: Crates - relay-ekf — Ekf::tick(ImuSample) → VehicleState. Defaults Kp=2.0, Ki=0.05 tuned for 200 Hz–1 kHz consumer IMU. Bias bounded ±0.5 rad/s. Pure-math helpers (quat_mul, quat_conj, rotate_body_to_ned_inverse, cross, normalise, is_unit_quaternion) exported for the controller layer. Example - examples/falcon-ekf-bench — runnable accuracy bench. 25 s × 200 Hz synthetic trajectory (rest at 20° pitch → roll 0.3 rad/s → rest → yaw 0.5 rad/s → rest). Achieved: RMS-steady 3.31°, final 3.02°, convergence 0.68 s, peak 19.8°. PASS budget: ≤ 5° RMS-steady, ≤ 5° final, no NaN/∞. Rivet - FV-FALCON-EKF-001 — v0.2 verification artifact with extractable fields.steps (cargo test + release rerun + 4 k proptest fuzz + bench tests + bench binary smoke). - FEAT-FALCON-v0.2 bumped pending → approved with achieved metrics inline in the description. Verification posture - cargo test --workspace: 52 test suites green (was 49 in v0.1) - relay-ekf: 16 unit + proptest cases covering EKF-P01..P05 surrogates - falcon-ekf-bench: 5 unit + integration tests - python3 scripts/run-falcon-verification.py: ✅ 4/4 artifacts, 13/13 steps green - rivet validate: 0 broken cross-references Cross-product convention - e = cross(measured, predicted) — the body-frame rotation Δq that maps predicted ŷ onto measured y has axis y × ŷ (right-hand rule, shorter arc). Initial implementation had cross(predicted, measured) which rotates the estimator away from truth; caught by the deterministic bench when the test reported 179° RMS error instead of the expected <5°. Documented in the source comment. Honestly deferred - Magnetometer fusion → v0.4 with relay-att (residual yaw drift is fundamental for an accel-only Mahony) - Verus SMT proofs on quaternion algebra → v0.4 with src/ track - Lean WCET proof → v0.4 with rules_lean wiring - WASM-component compilation → v0.3 with wit-bindgen Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
running 33 tests test result: ok. 33 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.03s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 33 tests test result: ok. 33 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 33 tests test result: ok. 33 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.40s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 16 tests test result: ok. 16 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.05s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 16 tests test result: ok. 16 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.01s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 16 tests test result: ok. 16 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.80s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 5 tests test result: ok. 5 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s --- noise=0 (deterministic) --- running 9 tests test result: ok. 9 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.01s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 9 tests test result: ok. 9 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 9 tests test result: ok. 9 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.09s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 9 tests test result: ok. 9 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.06s [falcon-hello-demo] building release binary... falcon verification gate (filter: (has-tag "falcon"))4 artifact(s) matched: FV-FALCON-MAVLINK-001, FV-FALCON-EKF-001, FV-FALCON-EKF-STUB-001, FV-FALCON-WORLD-001[ PASS] ( 9.07s) FV-FALCON-MAVLINK-001: cargo test -p relay-mavlink ✅ Rivet verification gate — falcon4/4 passed
Source of truth: |
1 participant
Summary
Replaces the v0.1 EKF stub with a real attitude estimator: Mahony, Hamel & Pflimlin (2008) complementary filter on SO(3), gravity-only correction. no_std + libm, embedded-ready. Adds a runnable accuracy bench that doubles as the v0.2 acceptance test.
What's in
crates/relay-ekf— the estimator. 16 unit + proptest cases covering EKF-P01..P05 surrogates.examples/falcon-ekf-bench— 25 s × 200 Hz synthetic IMU trajectory (rest → roll → rest → yaw → rest), reports RMS attitude error vs ground truth in degrees, exits 0/1 on budget.FV-FALCON-EKF-001— v0.2 verification artifact with extractablefields.steps.FEAT-FALCON-v0.2bumpedpending→approvedwith achieved metrics inline.CHANGELOG.mdentry forfalcon-v0.2.0.Achieved on this branch
cargo test --workspaceTest plan
cargo run -p falcon-ekf-bench --releaselocally prints PASScargo run -p falcon-ekf-bench --release -- --noise 0.2still PASSesAfter merge
Triggers
release.ymlto build 5 binaries (linux x86_64/aarch64, macOS x86_64/aarch64, windows x86_64), cosign-keyless-sign each via Fulcio OIDC, compute SHA-256, publish the GitHub Release.Honestly deferred
relay-att(heading is unobservable from gravity alone; residual yaw drift after the trajectory's yaw phase is fundamental)src/Verus-annotated track + Bazelverus_testrulesEkf::tick→ v0.4 withrules_leanwiring (empirically ≤ 1 µs/tick; formal proof later)🤖 Generated with Claude Code