feat(seam): the published component becomes a SUPERVISED vehicle, not a stabiliser (#414)

[avrabe]

Verify-Filter: (has-tag "supervisor")

Closes the seam half of #414. wasm/cm/cascade wrapped FlightCore, so the artifact a consumer pulls would hold attitude and position and would not stop for anything — the geofence RTL, the low-battery failsafe, the attitude-runaway motor cut, the mode machine and all 20 pre-arm rows were implemented, tested, in places Kani-proven, and unreachable from the shipped seam. That is why this week's failsafe fixes (#563, #565) are absent from anything anyone can actually run.

Seam goes pulseengine:falcon-cascade@0.11.0 → @0.12.0.

⚠️ BREAKING: an existing host that only calls step now gets zero motors

This is the requirement's own clause (5) and it is not a side effect — it is the correct behaviour, so read this before merging.

FlightSupervisor::step returns early through step_estimate_only (estimator warm, motors commanded zero) while the mode is Disarmed, Armed or Terminated. The FSM starts Disarmed. So a host that drives controller.step and nothing else now gets [0,0,0,0] forever until it calls pilot.command(arm, ..) and reaches Loiter.

That motors-off behaviour must not be weakened, and falcon-core's own comment records why: on the analytic plant the ground quietly held the vehicle so an always-stepping core was invisible, but on the gz plant a post-touchdown Disarmed kept the altitude loop live and flew the vehicle away — and "Terminate = motors cut" had been an FSM claim with no actuator behind it. An auto-arm inside step would make arming unobservable and bypass the 20 pre-arm rows that are the entire point of having a supervisor. So the seam gains a way to arm instead.

Affected in-tree consumers, named: the wasm SITL harness that holds 2.00 m, and the rotor-out verdict that isolates in 2 ticks. Both drive step only and will need an arm sequence.

Three measurements, each of which changed the design

1. Where the supervisor's configuration goes — and the record near the cliff was not the one anyone flagged.

The stakeholder refused growing sensor-frame (pulseengine/jess#167) because the canonical ABI's flattening boundary is live in this module: crossing MAX_FLAT_PARAMS = 16 silently changes the calling convention, and the ABI passes garbage rather than erroring when a caller assumed the other form. Correct in general. So I counted the real record rather than arguing:

contributor	flat
imu: imu-sample	6
dt-s: f32	1
position-ned: option<vec3>	4
mag-body: option<vec3>	4
heading-rad: option<f32>	2
motor-rpm: option<rotor-rpm>	5
sensor-frame	22
target: waypoint	4
controller#step	26

controller#step is already INDIRECT by 10 — it cannot cross a boundary it is a decade past, and battery-v takes it to 28. Independently confirmed: kiln lowered the shipped component at "26 flattened args" (pulseengine/jess#287), agreeing with a field-by-field count off the WIT. Two derivations, different routes.

The hazard was elsewhere. configure(cfg: vehicle-config) is 9 flat params (nine bare f32s), and the draft's six supervisor fields took it to 15 — one field of margin, with clause (4) still wanting RC/datalink liveness. So the supervisor's configuration went into the new pilot interface and vehicle-config stays at 9, byte-identical.

Also: sensor-frame and vehicle-config are used by interface controller alone, which only world cascade exports. The five per-stage worlds share none of those records, so the two exports the stakeholder measured either side of the line (rate#tick 18, ekf#estimate 6) cannot be moved by this change at all.

2. battery-v is a prerequisite, not a feature.

read_battery_v and read_battery_i are the only two backend methods the supervisor calls that FlightCore did not — and both default to None in a 12-method trait whose doc says None means "absent, not healthy". The cascade backend overrides 7 and not those. Then update_preflight sets battery_ok = batt_present && .. with batt_present == false, PreflightChecks::all_pass() ANDs it, and arm_check returns Blocked(CheckFail::Battery) forever.

So wiring the supervisor without a battery field would have shipped a vehicle that can never arm. Cleared as free by (1).

3. The supervisor still fits the 8 KiB shadow stack.

The by-value form of FlightCore::new already trapped there as an out-of-bounds access. FlightSupervisor is 3208 B against the core's 2688 B (1.19×), under the half-stack budget — #513's test holds that number. Same construct-into-slot mitigation, 19% more pressure, not a blocker. It is also entirely stack-allocated ([Vec3; MAX_WAYPOINTS], [KeepoutZone; MAX_KEEPOUT_ZONES], no Vec/Box/String), so the arena-as-#[global_allocator] reset at export entry cannot free supervisor state — which is what made #544/#566 a live question here.

An unconfigured supervisor cannot arm

FlightSupervisor::new defaults the first six pre-arm rows true for bring-up back-compat, update_preflight never writes the FailsafeConfigured row, and arm_check_table is read in command() — not in step(). So that default is exactly what a host's first arm would be judged against. The component therefore declares the row on every entry through pilot, from ensure_supervisor.

Unconfigured, the configuration-dependent failsafes are inactive rather than wrong (fence 1e9, low-batt 0.0): a 0 m geofence about a (0,0,0) home latches an RTL on tick one, which is the "worse than no supervisor" case the requirement names. And guessing a cell count is not the safer choice — 14 V fires far too late on a 6S pack and reads permanently low on a 3S one.

target is now a mission leg, not a position command

The one semantic change a host must notice. The supervisor owns the position setpoint: it derives one per mode (RTL flies home at cruise-alt, Land descends, Mission flies the active leg) and calls core.set_position itself at the end of its own step. Writing the core's setpoint from the component would be overwritten inside the same tick, so the honest wiring makes the frame's target the mission. A supervised vehicle sometimes declines to go where it is sent — that is the point.

The command enum is deliberately narrower than relay_fsm::Event

pilot-command offers 8 of the 12 variants. The four withheld — reached-altitude, reached-home, touchdown, failsafe — are physical observations the supervisor derives from its own estimated state, not requests. A host able to inject touchdown could disarm a vehicle in the air; one able to inject failsafe could raise a diversion with no cause recorded in failsafe. The seam does not offer a host the ability to lie to the mode machine about physics. The mapping match is exhaustive with no _ arm, so a new variant on either side has to be considered rather than silently absorbed.

Oracle, run the way CI runs it

cargo test -p falcon-core --all-targets      73 passed / 0 failed
  new seam-contract suite                     5 passed / 0 failed
  shadow-stack budget (#513)                  2 passed / 0 failed
cargo test -p falcon-core --doc               0 failed
cargo fmt --all --check                       clean
rivet validate                                PASS (405 warnings — unchanged)

Built for the shipped target, wasm32-unknown-unknown with -zstack-size=8192 as scripts/build-components.sh does: 0 errors, component created, and memory.grow count 0 so OCI-P02 still holds.

Read back from the artifact, not the source — which is the requirement's own stated criterion (wasm-tools component wit):

export pulseengine:falcon-cascade/controller@0.12.0;
export pulseengine:falcon-cascade/observer@0.12.0;
export pulseengine:falcon-cascade/pilot@0.12.0;
  battery-v: option<f32>
  mode: u8
  failsafe: u32
  configure-supervisor: func(cfg: supervisor-config)
  command: func(cmd: pilot-command, level: bool, throttle-low: bool)

Offsets: failed-rotor u8 at 72 → mode u8 at 73 (padding that already existed, so mode costs zero bytes) → failsafe u32 aligns to 76 → valid 80 → tick-tail 84 → record 84 → 88. That is the layout the consumer accepted.

Falsified, twice, each in the direction that proves something

• Swapped the declaration order of two fieldless Mode variants (Land/Rtl). Zero compile errors anywhere — every match stays exhaustive — and the wire values silently renumbered. mode_discriminants_are_the_published_wire_values FAILED on mode 5 is land. That is precisely the hazard the pin exists for: relay_fsm::Mode carries no #[repr] and no explicit discriminants, so its wire values are its declaration order, and a consumer has shipped a decoder against them.
• Made arm_check_table skip the FailsafeConfigured row. an_unconfigured_supervisor_refuses_to_arm FAILED with "it reported Armed". That test also carries its own control: flipping only that row lets the identical arm through, so the refusal is attributable to the row and not to the supervisor being unarmable for some unrelated reason.

Known gaps — named, not left to be discovered

• The HITL wire binding still serves the @0.11.0 shape. SENSOR_PAYLOAD_LEN is 76 and the binding carries no battery element, so a host driving the component through crates/falcon-hitl/src/wire.rs gets battery_v = None and cannot arm the supervised component. The stakeholder predicted this exact dependency on jess#167. Changing a Kani-verified wire format is its own slice.
• have_position: true is hardcoded in FlightSupervisor::command (crates/falcon-core/plain/src/lib.rs:1805), so FSAFE-P01's "never RTL when position is lost" ships unreachable through this seam. A core limitation this interface exposes rather than introduces.
• The warm-up count does not resync. FlightSupervisor::new hardcodes FlightCore::new(0.5, 1000.0). The loop rate self-corrects — resync_loop_rate re-derives it and the gyro LPF and notch bank from the backend's own dt past a 2% tolerance — but warmup = (loop_hz * 0.2).max(10) = 200 does not, so at a real 250 Hz frame the FDI is held off 0.8 s instead of 0.2 s. Longer, therefore conservative, but a behaviour change and it belongs in falcon-core.
• Clause (4)'s RC/datalink liveness has no consumer. FlightSupervisor reads no liveness input anywhere, so a seam field for it would be a field nothing reads. The clause is satisfied for battery and geofence configuration only.

Why this is implemented and not verified

SUPERVISOR-P01 moves proposed → implemented. Its criteria additionally require a wasm SITL harness driving a geofence breach, a draining pack and an attitude runaway with an observed mode change each time, plus FV-FALCON-FAULT-005's disarm clause on gz over three pristine-server trials. None of that is in this PR. The two-commit rule caps an implementation PR at implemented, and that promotion is a separate code-free PR.

Clause (6) is satisfied: the @0.12.0 design was announced to the consumer before any tag carries it, including the measurement above and an open offer to move battery-v to pilot instead if they would rather measure than accept it.

Still owed to the consumer by clause (6): the byte-identity re-measurement of the five per-stage components across the @0.12.0 bump. Argued structurally above (those worlds share none of the changed records) — but the requirement demands measurement, not assertion, so it is owed as a number.

Refs #414, #145, pulseengine/jess#167

🤖 Generated with Claude Code

https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG

[avrabe]

Clause (6)'s owed measurement — run, and it holds

I argued structurally in the PR body that the per-stage worlds share none of the changed records, so their byte-identity baselines could not move. The requirement asks for a measurement, not an argument. Run it:

One tree, one toolchain, only the WIT swapped (git checkout origin/main -- wit/falcon-cascade/cascade.wit, rebuild, restore). Shipped target and flags from scripts/build-components.sh: wasm32-unknown-unknown, --no-default-features, per-component -zstack-size.

component	size @0.11.0	size @0.12.0	differing disasm lines	of which name a version
iekf	23223	23223	12	12
attitude	13829	13829	12	12
rate	13647	13647	12	12
position	17656	17656	12	12
falcon-mixer	12312	12312	12	12

Identical length byte-for-byte — what a length-preserving 0.11.0→0.12.0 edit predicts — and every differing line carries a version string. Nothing else moved in any of the five, so rate#tick is still 18 flat params and ekf#estimate still 6; neither crossed MAX_FLAT_PARAMS = 16.

Caveat, stated because it would be easy to over-read the table: this covers the five per-stage components only. cascade itself changed enormously and deliberately — it wraps FlightSupervisor now, gained the pilot export, and flight-state grew 84 → 88 B. No cascade baseline carries across this bump. Reported to the consumer at pulseengine/jess#167 with the same caveat attached.

Working tree verified clean after the swap-and-restore.

[avrabe]

Two corrections, both found by continuing to check rather than by CI

1. I documented cruise-alt's sign backwards — and it was the dangerous direction

The WIT comment said "NED metres — NEGATIVE IS UP, as everywhere else in this package". It is the one altitude in this seam that is not NED-signed: falcon-core documents the constructor argument as cruise_alt m AGL and the supervisor negates it itself when deriving the setpoint — [p0, p1, -cruise_alt] for Takeoff, Loiter, Rtl and Land. Every in-tree call site passes a positive value.

A consumer following my comment and passing -30.0 to mean 30 m up would have commanded +30.0 NED — thirty metres below the ground, as an RTL cruise altitude. I inferred the convention from the surrounding fields instead of checking this one, which is exactly the error the integrator asked me not to repeat (their AFD-127), committed about an hour after agreeing.

Prose is not a sufficient fix for a sign error on a safety seam, so the behaviour is pinned and falsified: deleting the negation in falcon-core flew the vehicle to +1.87 m NED — 1.87 m underground — and a_positive_cruise_alt_commands_a_climb_not_a_descent caught it. sane(c.cruise_alt, .., positive) also goes false → true: zero or negative is not a conservative cruise altitude, it is a commanded descent into terrain.

2. The SITL harness could not have passed, and would have taken a required gate with it

I predicted in the PR body that tests/cascade-sitl-wasm would break. Reading it rather than waiting showed it was broken two ways, and the first would not even have produced a useful error:

• Its inline wasmtime world pinned controller@0.11.0/observer@0.11.0, so it would have failed to instantiate against @0.12.0 — a version mismatch, not a behaviour report.
• Past that, it only called step, so it would have measured a vehicle sitting on the ground for 4000 ticks and reported a 2.00 m hold error — which reads like a control regression rather than a missing arm.

It now behaves like a real host: configure_supervisor, then Arm → RequestTakeoff before the first step (where the pre-arm table is actually judged, since arm_check_table is read inside command), and it supplies 16.8 V against a 14.0 V LOW threshold — without a pack the component cannot arm at all. Geofence configured at 100 m rather than the 1e9 inactive sentinel, so the vehicle still flies with a real geofence armed instead of one switched off for convenience.

It also turns out the existing native test geofence_breach_actuates_rtl_home arms successfully with no battery supplied — because it arms before the first step refreshes the table. That independently confirms the hole this PR closes with the FailsafeConfigured declaration.

Gate after both commits

cargo test -p falcon-core --all-targets   73 passed / 0 failed
  seam contract (now 6)                    6 passed / 0 failed
  shadow-stack budget                      2 passed / 0 failed
cargo fmt --all --check                    clean
cargo check tests/cascade-sitl-wasm        0 errors against the @0.12.0 seam
component, wasm32-unknown-unknown -zstack-size=8192:
  0 errors · memory.grow count 0 (OCI-P02 holds)

Not verified locally, and I will not imply otherwise: the harness's runtime arming sequence needs the composed wasm plus a plant, so its oracle is the Component Model cascade and Gazebo SITL gates. It type-checks against the real seam and the sequence mirrors the native supervisor tests — but whether the vehicle reaches Loiter and holds 2.00 m through the component is CI's answer, not mine. Those are the two checks to read first.

Auto-merge deliberately not armed: this is a breaking seam change and those two gates are the point.

[avrabe]

Correction: I mis-attributed the arming blocker, and chasing it down found a larger gap

I published "without battery-v the component cannot arm" in the WIT doc, the first commit, the PR body above, #414, #572 and pulseengine/jess#167. It is mis-attributed. One correction here with the whole picture rather than six partial ones.

What is actually true

Battery absence does refuse arming — that part holds, and battery-v remains a prerequisite. But a host that warms its estimator before arming — what step_estimate_only exists for, and what a real GCS does — is refused first by CalibrationPresent. Measured, with a control:

warm 1500 ticks, supply everything the @0.12.0 seam carries, then Arm
  -> mode = Disarmed,  arm_blocked_check = Some(CalibrationPresent)
install a CalParams, re-arm            (the control)
  -> mode = Armed,     arm_blocked_check = None

So battery-v is necessary but not sufficient, and adding it does not make the component armable.

The larger gap

update_preflight derives calibration_present from core.calibration() != CalParams::identity(), and nothing in this seam carries a calibration: vehicle-config has none, supervisor-config has none, and the component never calls set_calibration because it has nothing to pass.

So the published component can presently be armed only on the arm-before-first-step path, where the pre-arm table still holds FlightSupervisor::new's deliberate bring-up defaults (the legacy six forced true).

That is SUPERVISOR-P01's own falsification condition — "the supervisor runs against default inputs the host cannot supply."

And it means a green SITL gate is not the evidence I implied it was. It shows the defaults path works end to end through the Component Model ABI; it does not show that the 20-row pre-arm table gates arming through the seam. The harness now says that in place so nobody cites it that way at promotion time. Two of you flagged the general shape of this before I measured it; the specific row was mine to find and I found it late.

Why my census missed it

The census enumerated FlightBackend's read_* methods and diffed them against what the cascade backend overrides. Calibration does not arrive through the backend — it arrives through a setter. Censusing one input channel and then concluding about arming was the error. The census has to cover every input update_preflight consumes, setters included.

And a defect of mine, found by the same re-reading

I wrote that "update_preflight never writes the FailsafeConfigured row". It does — as a multi-line t.set(\n CheckId::FailsafeConfigured,\n ..) that the single-line grep I used cannot see, sourced from a field that defaults true and is never refreshed from a real signal.

So every tick clobbered the component's declaration. Arming stayed correct, because nothing steps between ensure_supervisor and command reading the table — but the published failsafe bit 7 did not: an unconfigured host would have seen arm-blocked clear in telemetry while actually being refused. An observer disagreeing with the thing it observes, which is the exact defect class this seam exists to remove. Fixed: re-declared after step, before the state is published.

Status of this PR

Still implemented, and now for a second reason as well. Gate after three commits:

cargo test -p falcon-core --all-targets   73 passed / 0 failed
  seam contract (now 7)                    7 passed / 0 failed
  shadow-stack budget                      2 passed / 0 failed
cargo fmt --all --check                    clean
cargo check tests/cascade-sitl-wasm        0 errors
component, wasm32-unknown-unknown -zstack-size=8192: 0 errors

The new test asserts a limitation, with its own control, so it fails usefully in both directions: if the seam gains a calibration path the first assert breaks (delete it, verify the real thing), and if a different row starts refusing first then the gap has moved and the justification is stale again.

What is a decision rather than a fix

Not mine to take alone, so it is not taken:

• (a) The seam gains a calibration input. Then a host warms, arms against the real 20-row table, and the defaults path stops being the only route. It is a seam change, so the shape is the integrator's call.
• (b) The supervisor refreshes preflight at construction, so arming is always judged on real signals. Sound, and it leaves the published component visibly unarmable until (a) lands — which is honest but ships a component no host can fly.

Either way the SITL harness should end up warming first and arming only once the observer's failsafe bit 7 clears, the way a real GCS would. It cannot do that today, which is why it still arms on defaults.

Auto-merge remains off.

[avrabe]

Decision: land this, calibration as the immediate next slice

Maintainer call taken on the question in the correction above. Rationale recorded so the trade is visible rather than inferred from a merge:

This PR is a strict improvement on the current state. Today the published component has no mode machine at all — it will hold attitude and position and will not stop for anything. After this it runs the supervisor, publishes mode and failsafe, and makes the geofence RTL, the battery failsafe, the attitude-runaway cut and the 20 pre-arm rows reachable through the seam. The defaults-arming limitation is narrower than what it replaces, not a new hole, and it is now documented in the WIT, in the harness, in a test that asserts it, and on #414.

The alternative — refreshing preflight at construction so arming is always judged on real signals — is sound but ships a component no host can arm, and would break both the SITL harness and the in-tree native supervisor tests that arm before stepping. Holding this PR until a calibration input lands would park the whole supervisor wiring behind a seam round-trip.

So: calibration input next, shape pending the integrator's answer on pulseengine/jess#167 (my lean is a configure-calibration func on pilot, since vehicle-config has one field of flat-param margin and pilot is new so it has no baseline to break).

Auto-merge is now armed, and the gate that matters is a required check. Gazebo SITL (real gz bridge) and Closed-loop simulation + Monte-Carlo campaigns are both in main's required contexts — so this cannot land until the harness's runtime arming sequence, the one thing I could not verify locally, has actually run against a real plant. If it goes red there, the fix is in tests/cascade-sitl-wasm, not an auto-arm inside step: the requirement forbids that, and the reason is on record — on the gz plant a post-touchdown Disarmed kept the altitude loop live and flew the vehicle away.

#414 stays open until a tag carries this. SUPERVISOR-P01 stays implemented; promotion needs the wasm SITL legs (geofence breach, draining pack, attitude runaway) and FAULT-005's disarm clause, and it must not be promoted on the strength of a green defaults-path gate.

[avrabe]

The gz gate caught it in 7 minutes, and not where I predicted

commanded  : Arm -> RequestTakeoff (supervised; Disarmed commands zero motors)
Error: FAIL: wasm and native disagree by 0.069364190 (tick 6249).
       The same Rust reached two ways must compute the same answer.

I flagged the harness's arming sequence as the unverified risk. It worked — the run reached tick 6249. What broke is the differential: this harness runs the same flight core natively alongside the component and asserts they agree, and I had switched only the wasm side to FlightSupervisor. It compared a supervised vehicle against an unsupervised one and reported a real difference about two different programs, not about the boundary.

Classified before acting (./scripts/ci-triage.rs 571): steps=19, log=present → REAL. Not the Kani cancellation flake, so not re-run and hoped.

This is the second time this file has had to learn the same lesson — #393's note already says keeping the old five-stage mirror "would have compared two different programs and reported a difference meaning nothing". The module doc now records both instances.

Mirroring took more than swapping the type

Each of these was load-bearing:

• the supervisor's configuration (home / fence / cruise / low-batt);
• a battery reading, since read_battery_v defaults to None and the pre-arm table ANDs BatteryOk;
• the arm + takeoff commands — FlightSupervisor::step commands zero motors while Disarmed, so an unarmed mirror sits on the ground while the wasm side flies and reports that as a Component Model failure;
• construction through FlightSupervisor::new, not FlightCore::new. This one would have left a residual disagreement after the obvious fixes: the supervisor hardcodes FlightCore::new(0.5, 1000.0) and the warm-up count is seeded (loop_hz * 0.2).max(10) = 200, while the old mirror built at 1/dt — 80 at 400 Hz. Warm-up does not resync from the backend; only the loop rate does.

Two comments that had become false

• The judged-window rationale said "the component wraps FlightCore, so there is no failsafe to disarm it". The window stays, but now because this harness does not fly long enough or command Land to reach a touchdown — not because disarming is impossible.
• The rotor-out verdict said there is "deliberately NO disarm term" because there is "no mode machine to disarm". That reason is gone — FV-FALCON-FAULT-005's fourth clause becomes reachable on the wasm leg for the first time. I did not add the term: putting a new bar on a required gate in the same change that makes it possible is ratcheting past the evidence, since nothing here has yet measured a supervised rotor-out reaching touchdown through the component. It belongs with SUPERVISOR-P01's promotion. The absence is now a choice rather than an impossibility, and the comment says so.

Auto-merge was disarmed before pushing and re-armed after — arming a branch you are still pushing to is how #478 squashed at an intermediate commit.

Whether the two sides now agree within tolerance is gz's answer, not mine; the gate is required, so it has to give it before this lands.