perf(cascade): measure the flight cascade — 1.2413 µs/tick, estimator is 91% (PERF-P01)

Cargo.toml

@@ -20,6 +20,7 @@ members = [
     "crates/relay-ccsds",
     "crates/relay-cfdp",
     "benches/engine-throughput",
+    "benches/cascade-throughput",
     "crates/relay-sec",
     "crates/relay-offboard",
     "crates/relay-fsafe",

artifacts/swreq/SWREQ-FALCON-PERF-P01.yaml

@@ -0,0 +1,69 @@
+artifacts:
+  - id: SWREQ-FALCON-PERF-P01
+    type: sw-req
+    title: "PERF-P01 — the flight cascade has a measured per-cycle baseline, and a regression guard on it"
+    status: implemented
+    release: falcon-v1.135.0
+    description: >
+      The falcon control cascade shall have a recorded per-cycle timing
+      baseline, per stage and for the full tick, guarded against regression.
+
+      WHY IT EXISTS — performance was the one axis on which this project could
+      make NO claim at all. `engine-throughput` has guarded the cFS-lineage
+      engines (LC/SCH/SC/HS/CFDP) since v1.56, but the control path that
+      actually flies — iekf, position, attitude, rate, mixer — had no timing
+      baseline of any kind. The `examples/*-bench` binaries measure estimator
+      ACCURACY, not time. A compositional WCET proof exists in Lean; no
+      measurement had ever been taken against it.
+
+      That gap mattered strategically, not just tidily. The architecture has
+      real structural reasons to be fast — no RTOS on the control path, no
+      dynamic allocation, a bounded arena, fused single address space — and
+      none of it was evidenced. "Proven correct AND measurably faster on the
+      same silicon" is a claim no open-source, verified-systems or commercial
+      alternative can answer; it was also entirely unsubstantiated here.
+
+      MEASURED (2026-08-25, Apple-silicon dev host, release profile):
+
+        iekf_propagate      1.1256 us    91.0 % of the cascade
+        position_tick      73.40   ns     5.9 %
+        attitude_tick      15.47   ns     1.2 %
+        rate_tick          10.25   ns     0.8 %
+        mixer_mix           9.45   ns     0.8 %
+        full_cascade_tick   1.2413 us    <- the per-tick control-loop cost
+
+      TWO FINDINGS FALL OUT.
+
+      (i) THE ESTIMATOR IS THE CASCADE. IEKF is 91 % of per-tick cost; the other
+      four stages together are ~108 ns. Any cascade performance work that is not
+      estimator work is rounding error. This agrees with an independent
+      measurement — jess's scry static stack bounds put iekf at 4 192 B against
+      16-112 B for the others — so two unrelated methods identify the same stage
+      as carrying the mass.
+
+      (ii) THE 1 kHz BUDGET IS NOT CLOSE. 1.2413 us against a 1 ms period is
+      0.12 % of budget, ~806x margin on this host. Even allowing an order of
+      magnitude for a Cortex-M7 at a fraction of the clock, the control math is
+      not what will bound the loop — the HAL, scheduler and sensor I/O will.
+
+      `full_cascade_tick` is the honest per-tick figure rather than a synthetic
+      sum, because the cascade is SINGLE-RATE: `cascade.step()` executes every
+      stage once per tick with no divider (verified in
+      wasm/cm/cascade/src/lib.rs).
+    tags: [falcon, performance, wcet, cascade, benchmark, v1.135]
+    fields:
+      req-type: performance
+      priority: shall
+      verification-criteria: >
+        (a) A criterion benchmark exists covering all five cascade stages AND
+        the full tick, with a recorded baseline in
+        benches/cascade-throughput/BASELINE.md. (b) The baseline states its
+        host and explicitly disclaims being a cross-machine SLA or an
+        on-silicon figure. (c) A catastrophic-regression ceiling is recorded
+        per bench. (d) NOT DISCHARGEABLE BY (a)-(c): a head-to-head against
+        PX4's equivalent loop on the SAME board. Until that runs, this
+        requirement establishes what our cascade costs, NOT that it costs less
+        than the alternative — and the second half is the claim worth having.
+    links:
+      - type: derives-from
+        target: SYSREQ-FALCON-001

artifacts/verification/FV-FALCON-PERF-002.yaml

@@ -0,0 +1,70 @@
+artifacts:
+  - id: FV-FALCON-PERF-002
+    type: sw-verification
+    title: "PERF-P01 — flight cascade per-cycle baseline: 1.2413 us/tick, estimator 91% (v1.135)"
+    status: implemented
+    release: falcon-v1.135.0
+    description: >
+      Verification of SWREQ-FALCON-PERF-P01.
+
+      (a) CONFIGURATION (CI-runnable, below). The benchmark crate exists, covers
+      all five stages plus the full tick, and a baseline with per-bench
+      regression ceilings is recorded. These steps fail if the bench is deleted,
+      if a stage stops being covered, or if the baseline file goes missing —
+      which is the regression worth catching, since nothing else in CI would
+      notice the flight path losing its only timing evidence.
+
+      (b) MEASURED, by execution — `cargo bench -p cascade-throughput-bench`,
+      Apple-silicon dev host, release profile, 2026-08-25:
+
+        iekf_propagate      [1.1249  1.1256  1.1263] us
+        position_tick       [73.359  73.403  73.451] ns
+        attitude_tick       [15.456  15.465  15.476] ns
+        rate_tick           [10.245  10.252  10.261] ns
+        mixer_mix           [ 9.4437  9.4491  9.4549] ns
+        full_cascade_tick   [1.2406  1.2413  1.2421] us
+
+      Confidence intervals are tight (<0.1 % spread), so these are stable
+      measurements rather than noise.
+
+      CROSS-CHECK, and it is the useful part: the timing split identifies iekf
+      as 91 % of the cascade, and jess's scry STATIC STACK bounds independently
+      put iekf at 4 192 B against 16-112 B for the other four. Two unrelated
+      methods — dynamic timing here, static analysis there — agree on which
+      stage carries the mass. Neither was derived from the other.
+
+      SCOPE (honest, and the limits are the point):
+
+      - NOT an on-silicon number. aarch64 dev host with a warm cache and a
+        branch predictor a Cortex-M7 does not have. The Lean compositional WCET
+        proof bounds cycle counts; this does not measure them.
+      - NOT a comparison. The PX4 head-to-head on the same board is criterion
+        (d) of the requirement and has not been run. We can currently say what
+        our cascade costs, not that it costs less.
+      - NOT a tight SLA. No persisted baseline history, so the ceilings are
+        coarse catastrophic-regression guards (~10x) chosen to survive hardware
+        variance — the same limitation FV-FALCON-PERF-001 records for the
+        engine benches.
+
+      This artifact therefore stays `implemented`. Criterion (d) is what would
+      make it `verified`, and it is a measurement nobody has taken yet.
+    tags: [verification, falcon, performance, wcet, cascade, benchmark, v1.135]
+    fields:
+      method: test
+      steps:
+        # (a) the bench exists and covers every stage plus the full tick
+        - run: "test -f benches/cascade-throughput/benches/cascade_throughput.rs"
+        - run: "grep -q 'full_cascade_tick' benches/cascade-throughput/benches/cascade_throughput.rs"
+        - run: "test \"$(grep -c 'c.bench_function' benches/cascade-throughput/benches/cascade_throughput.rs)\" -eq 6"
+        # (b) a baseline with regression ceilings is recorded
+        - run: "grep -q 'full_cascade_tick' benches/cascade-throughput/BASELINE.md"
+        - run: "grep -q 'Catastrophic-regression ceiling' benches/cascade-throughput/BASELINE.md"
+        # (c) execution evidence — this one genuinely RUNS in the gate (~62s).
+        # NOT marked bench-only: `cargo bench` is not in BENCH_PATTERNS, so a
+        # "# bench-only" comment here would claim something untrue. It executes,
+        # which is better evidence than a skip, and FV-FALCON-PERF-001 already
+        # pays the same cost for the engine benches.
+        - run: "cargo bench -p cascade-throughput-bench"
+    links:
+      - type: verifies
+        target: SWREQ-FALCON-PERF-P01

benches/cascade-throughput/BASELINE.md

@@ -0,0 +1,81 @@
+# Flight cascade throughput — per-cycle baseline (PERF-P01, #8)
+
+Per-cycle wall-time for each stage of the falcon control cascade, and for the
+whole cascade in sequence. `engine-throughput/BASELINE.md` covers the
+cFS-lineage engines (LC/SCH/SC/HS/CFDP); **this file covers the control path
+that actually flies**, which had no timing baseline of any kind before v1.135.
+
+Run: `cargo bench -p cascade-throughput-bench`
+Traced by **FV-FALCON-PERF-002**.
+
+## Baseline (2026-08-25)
+
+Apple-silicon dev host, release profile. **Absolute numbers are
+hardware-specific** — treat them as a relative regression baseline on
+like-for-like hardware, not as a cross-machine SLA and not as an on-silicon
+figure.
+
+| Stage | Hot path | Median | Share of cascade |
+|---|---|---|---|
+| `iekf_propagate` | one propagate at dt = 1 ms | **1.1256 µs** | **91 %** |
+| `position_tick` | NED pos/vel → attitude setpoint | 73.40 ns | 5.9 % |
+| `attitude_tick` | geometric SO(3), quat error → rate setpoint | 15.47 ns | 1.2 % |
+| `rate_tick` | body-rate PID → torque | 10.25 ns | 0.8 % |
+| `mixer_mix` | torque + thrust → 4 motor commands | 9.45 ns | 0.8 % |
+| **`full_cascade_tick`** | **all five in sequence, one tick** | **1.2413 µs** | — |
+
+## What the numbers say
+
+**The estimator is the cascade.** IEKF is 91 % of per-tick cost; the other four
+stages together are ~108 ns. Any work on cascade performance that is not work on
+the estimator is rounding error. This matches the independent evidence from
+jess's scry static bounds, which put iekf at 4 192 B of stack against 16–112 B
+for the other four — two unrelated measurements agreeing on which stage carries
+the mass.
+
+**The 1 kHz budget is not close.** `full_cascade_tick` is 1.2413 µs against a
+1 ms rate-loop period — **0.12 % of budget, ~806× margin** on this host. Even
+allowing an order of magnitude for a Cortex-M7 at a fraction of the clock, the
+control math is not what will bound the loop; the HAL, the scheduler and sensor
+I/O will.
+
+**`full_cascade_tick` is the honest per-tick figure** because the cascade is
+single-rate: `cascade.step()` executes every stage once per tick, with no
+divider (verified in `wasm/cm/cascade/src/lib.rs`). It is not a synthetic sum.
+
+## What this does NOT establish
+
+- **Not an on-silicon number.** This is an aarch64 dev host with a warm cache
+  and a branch predictor a Cortex-M7 does not have. The compositional WCET proof
+  in `proofs/lean/` bounds the cycle count; this bench does not measure it.
+- **Not yet a comparison.** The PX4 head-to-head on the same board is the second
+  half of PERF-P01 and is not done. Until it is, we can say what our cascade
+  costs, not that it costs less than the alternative.
+- **Not a tight SLA.** No persisted baseline history, so CI can only guard
+  against catastrophic regression, not drift. Same limitation the
+  engine-throughput bench records.
+
+## Regression guard
+
+A 10× regression in `full_cascade_tick` — or any stage crossing 10× its median
+here — is an early warning that the control path is drifting toward the WCET
+ceiling the Lean proofs bound. The ceilings are deliberately coarse so they
+survive hardware variance between this host and CI runners.
+
+| Bench | Baseline | Catastrophic-regression ceiling |
+|---|---|---|
+| `full_cascade_tick` | 1.2413 µs | 15 µs |
+| `iekf_propagate` | 1.1256 µs | 15 µs |
+| `position_tick` | 73.40 ns | 1 µs |
+| `attitude_tick` | 15.47 ns | 500 ns |
+| `rate_tick` | 10.25 ns | 500 ns |
+| `mixer_mix` | 9.45 ns | 500 ns |
+
+## Deferred
+
+- **PX4 head-to-head on the same board** — the claim this bench exists to make
+  possible.
+- **On-silicon cycle counts** (Cortex-M7), which is what the WCET proof wants
+  confronting with reality.
+- **Persisted baseline history** for a tight per-runner SLA, rather than the
+  coarse ceilings above.

benches/cascade-throughput/Cargo.toml

@@ -0,0 +1,20 @@
+[package]
+name = "cascade-throughput-bench"
+version = "0.1.0"
+edition = "2021"
+publish = false
+description = "Per-cycle throughput benchmarks for the falcon FLIGHT CASCADE (iekf/position/attitude/rate/mixer). The engine-throughput bench guards the cFS engines; this one guards the control path that actually flies."
+
+[dependencies]
+relay-iekf = { path = "../../crates/relay-iekf" }
+relay-pos = { path = "../../crates/relay-pos" }
+relay-att = { path = "../../crates/relay-att" }
+relay-rate = { path = "../../crates/relay-rate" }
+relay-mix-quad = { path = "../../crates/relay-mix-quad" }
+
+[dev-dependencies]
+criterion = { version = "0.7", default-features = false, features = ["cargo_bench_support"] }
+
+[[bench]]
+name = "cascade_throughput"
+harness = false