From 6d3f6615f315dcad87d33314a6352853bf60abcc Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 16 Jul 2026 14:56:30 +0200 Subject: [PATCH] =?UTF-8?q?verify(falcon):=20v1.123=20=E2=86=92=20verified?= =?UTF-8?q?=20=E2=80=94=20float=20discipline=20(FLOAT-P01)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG --- artifacts/swreq/SWREQ-FALCON-FLOAT-P01.yaml | 32 +++++++++++++ .../verification/FV-FALCON-FLOAT-001.yaml | 45 +++++++++++++++++++ 2 files changed, 77 insertions(+) create mode 100644 artifacts/swreq/SWREQ-FALCON-FLOAT-P01.yaml create mode 100644 artifacts/verification/FV-FALCON-FLOAT-001.yaml diff --git a/artifacts/swreq/SWREQ-FALCON-FLOAT-P01.yaml b/artifacts/swreq/SWREQ-FALCON-FLOAT-P01.yaml new file mode 100644 index 0000000..64d1681 --- /dev/null +++ b/artifacts/swreq/SWREQ-FALCON-FLOAT-P01.yaml @@ -0,0 +1,32 @@ +artifacts: + - id: SWREQ-FALCON-FLOAT-P01 + type: sw-req + title: "FLOAT-P01 — f32 flight core with enforced f64 boundary discipline + covariance numerical health" + status: verified + release: falcon-v1.123.0 + description: > + (a) Flight-partition code (the M4/M7 crates) shall contain no f64 + arithmetic outside explicitly annotated geodetic/API boundary + modules — the M4's FPv4-SP FPU has no double-precision hardware, so + unintended f64 is a WCET hazard, while absolute lat/lon in f32 would + quantize at ~0.6 m (the boundary modules exist precisely for that). + The rule shall be CI-enforced, not conventional. (b) The estimator's + error covariance shall remain numerically healthy under f32 + arithmetic for ANY input: every diagonal finite and within + [1e-9, 1e6] after each measurement update, with corrupt-row + correlations cleared and every healing event counted loudly. + Raised by external design review (2026-07); design rationale in + SWDD-FALCON-FLOAT-001. + tags: [falcon, float-discipline, f32, iekf, numerical-health, v1.123] + fields: + req-type: non-functional + priority: must + verification-criteria: > + Gate green in CI on every PR and negative-tested (a seeded f64 + fails it). Kani post-condition proof over all covariance contents + incl. NaN/±∞. Unit tests for negative/NaN diagonal healing and + correlation clearing. A 50k-cycle healthy run with ZERO floor + hits (behavior-neutral); pre-existing estimator suites unchanged. + links: + - type: derives-from + target: SYSREQ-FALCON-002 diff --git a/artifacts/verification/FV-FALCON-FLOAT-001.yaml b/artifacts/verification/FV-FALCON-FLOAT-001.yaml new file mode 100644 index 0000000..63c76ec --- /dev/null +++ b/artifacts/verification/FV-FALCON-FLOAT-001.yaml @@ -0,0 +1,45 @@ +artifacts: + - id: FV-FALCON-FLOAT-001 + type: sw-verification + title: "Float discipline: CI f64 gate + IEKF variance floor/ceiling (v1.123)" + status: verified + release: falcon-v1.123.0 + description: > + Verification of SWDD-FALCON-FLOAT-001. + + Gate: scripts/check-float-discipline.sh runs as a CI step (ci.yml, + ahead of clippy) over the 21 flight-partition crates; green on main. + The oracle itself is negative-tested: a seeded f64 at a flight-crate + file top FAILS the gate; the clean tree passes. The gate already + caught two of its own defects before landing: BSD awk's missing \y + word boundary made local runs vacuous (portable character-class + boundary now), and falcon-mavlink's separate tests.rs sat outside + the cfg(test) exemption (test files skipped explicitly). Exactly one + annotated boundary exists (falcon-mavlink: geodetic — absolute + lat/lon must be f64; f32 degrees quantize at ~0.6 m). + + Variance floor (the review's finding): floor_variances runs after + every relay-iekf measurement update. Kani proves the post-condition + for ANY covariance content including NaN/±∞ — every diagonal finite + and within [1e-9, 1e6] (4/4 harnesses; the harness CAUGHT the first + implementation: +∞ passed the naive floor-only check, and an + infinite variance must heal to the CEILING — maximal uncertainty — + never the floor). Unit tests: negative-diagonal heal with stale- + correlation zeroing, NaN heal, healthy-matrix no-op + (variance_floor_tests::*). Behavior-neutrality: a 50k-cycle healthy + run asserts ZERO floor hits + (variance_floor_tests::floor_never_fires_on_healthy_long_run), and + the pre-existing relay-iekf (26) and falcon-core (56) suites are + unchanged. The event counter (Iekf::variance_floor_hits) is public + and LOUD. + tags: [verification, falcon, float-discipline, iekf, kani, v1.123] + fields: + method: automated-test + steps: + - run: ./scripts/check-float-discipline.sh + - run: cargo test -p relay-iekf + - run: cargo test -p falcon-core + - run: cargo kani -p relay-iekf + links: + - type: verifies + target: SWREQ-FALCON-FLOAT-P01