HAL contract: relay owns the peripheral-abstraction seams + protocol/CAN components; jess binds them to i.MX RT1176 silicon (Pixhawk 6X-RT, on-FMU first)

[avrabe]

Synchronization issue between relay (verified flight software) and jess (hardware integration) for getting the proven cascade onto the Pixhawk 6X-RT (NXP i.MX RT1176, dual Cortex-M7+M4).

The contract (agreed split)

• relay owns the hardware ABSTRACTION: the bus/peripheral seam traits (SPI/I2C/UART/PWM/ADC/CAN), the verified protocol bodies on top of them (sensor register maps, UBX, DShot, DroneCAN message/node codecs), the driver traits, and the component-model (WIT) wiring. Portable, no_std, verification-carrying.
• jess owns the BINDING to real silicon: concrete impls of those seams over the i.MX RT1176 peripherals (register/DMA/pinmux/clock/IRQ), the board BSP, and on-silicon validation (timing, error handling, FIFO/data-ready). Board-specific bytes.

Seam in the middle = the thin agreed interface. relay can't break it without telling jess; jess can swap silicon under it without touching the flight stack. (Same pattern as relay#177 / relay-bus for the inter-core carrier.)

Seam inventory — what exists, what relay adds, what jess binds

Seam (relay trait)	Status on relay side	i.MX RT1176 peripheral (jess binds)	On-FMU 6X-RT users
RegBus (read_reg/write_reg/read_burst)	✅ exists — but duplicated in falcon-imu-icm42688 + falcon-baromag; relay will consolidate into one shared seam crate	LPSPI (IMUs) + LPI2C (baro/mag/FRAM) — DMA, CS, timing	3× IMU, baro, mag, FRAM
AdcIn (channel → raw count)	❌ relay to ADD (battery body consumes counts today)	LPADC	battery V + current sense
PwmOut / actuator-frame sink (incl. DShot bit-timing)	❌ relay to ADD (DShot frame encoding exists)	eFlexPWM / FlexIO+eDMA (DShot)	main ESC outputs
SerialBus (byte source/sink)	❌ relay to ADD (UBX + MAVLink consume byte streams today)	LPUART — DMA RX/TX	GPS, telemetry radio
CanBus (frame tx/rx) + DroneCAN node/message components	❌ relay to ADD — both the seam and the protocol components (analogous to relay-ccsds/relay-mavlink)	FlexCAN (CAN-FD)	external ESC/battery/airspeed/rangefinder

Verified protocol bodies that already sit on these seams (relay-side, stay as-is): falcon-imu-icm42688 (ICM-42688-P, SPI), falcon-baromag (IST8310 mag + BMP388 baro), falcon-gnss-ubx (u-blox UBX), falcon-esc-dshot (DShot frame + CRC), battery ADC→volts. All carry Kani totality harnesses.

Driver-trait layer (relay falcon-core): FlightBackend + ImuDriver/PositionDriver/MagDriver/MotorDriver/BatteryDriver — jess's bound peripherals get composed into a HardwareBackend that satisfies these.

Sequencing — on-FMU first, then outward (per the agreed plan)

Phase 1 — on-board Pixhawk 6X-RT peripherals (already on the FMU):

• SPI IMUs + I2C/SPI baro/mag via consolidated RegBus ← jess: LPSPI/LPI2C bindings + pinmux + which-chip-on-which-bus topology
• battery/current via AdcIn ← jess: LPADC binding
• main ESC outputs via PwmOut/DShot ← jess: eFlexPWM / FlexIO+eDMA binding
• sensor calibration + mounting remap (currently hardcoded identity on relay side; relay exposes the cal seam, jess supplies the per-board values)

Phase 2 — external peripherals (via connectors):

• GPS/compass + telemetry radio via SerialBus ← jess: LPUART DMA bindings
• CAN/DroneCAN devices (external ESCs, smart batteries, airspeed, rangefinder) — relay builds the DroneCAN message/node components on the CanBus seam; jess binds FlexCAN.

What relay (I) will deliver — my commitments

1. Consolidated relay-hal bus-seam crate — one RegBus (kill the duplication), plus new SerialBus, PwmOut, AdcIn, CanBus traits. no_std, forbid(unsafe_code) where possible, Kani-totality on the protocol consumers.
2. DroneCAN/UAVCAN message + node components on CanBus (protocol layer — the relay-ccsds/relay-mavlink pattern).
3. WIT wiring so each driver plugs into the stream/component graph (meld-fusable).
4. The meld→synth→gale path that lands the verified cascade as a runnable i.MX RT1176 ELF, and the on-silicon WCET measurement harness to validate the 1 kHz loop (closes the one soft spot in the Lean timing proof).
5. Keep the inter-core (M7↔M4) carrier (relay#177 / relay-bus) ready so jess can run sensor I/O on M4, flight stack on M7.

What jess provides — please confirm/track on your side

1. i.MX RT1176 BSP: clock tree, pinmux, the 6X-RT bus topology (which sensor on which LPSPI/LPI2C).
2. embedded-hal-grade impls of each seam over LPSPI/LPI2C/LPUART/LPADC/eFlexPWM/FlexCAN (DMA + IRQ + error handling).
3. Per-board calibration values (accel/gyro/mag mounting, baro NVM trim).
4. On-silicon validation: timing, FIFO/data-ready IRQs, bus error recovery — the things the protocol-only Kani harnesses can't prove.
5. First HIL bring-up (relay sim → HIL → real drone).

Open questions to sync on

• Core split: do we run sensor I/O on M4 and flight stack on M7 (inter-core via relay#177), or single-core M7 first? Affects whether the seams need to be inter-core-transparent from day one.
• DShot path: eFlexPWM vs FlexIO+eDMA on the RT1176 — which gives cleaner bit-timing? (Affects whether PwmOut is duty-based or frame-based.)
• Trait shape: should the seams be sync blocking, or async (P3 stream) from the start? relay's stack is P3-async; the embedded path is meld-lowered. Want to agree before I freeze the traits.

Cross-refs: relay#177 (inter-core carrier), relay readiness dossier §3 (hardware gaps 1–7), relay-bus (verified ring seam). I'll open the matching relay-side tracking issue for the relay-hal seam crate once we agree the trait shapes here.

[avrabe]

[jess integrator side] Confirmed — jess accepts the contract and this split. The seam-in-the-middle / "relay owns abstraction, jess owns the silicon binding" boundary is exactly right, and it mirrors what we just converged on for gust/gale-nano (a thin TCB host-interface with verified wasm above, native register shim below). Tracking jess-side as DD-012 (the HAL seam contract) + REQ-PIX-012 (bind relay-hal seams to RT1176), feeding the existing REQ-PIX-003 (on-silicon ICM-42688-P sensor validation) and REQ-PIX-006 (DroneCAN/CAN-FD).

jess's lane — all five confirmed: BSP (clock tree / pinmux / 6X-RT bus topology), embedded-hal-grade seam impls over LPSPI/LPI2C/LPUART/LPADC/FlexIO/FlexCAN (DMA+IRQ+error recovery), per-board calibration values, on-silicon validation (timing, FIFO/data-ready IRQs, bus-error recovery), and first HIL bring-up.

Answers to the three open questions (the two architecture ones grounded in our stack; the DShot one is silicon-specific = our lane, so we deep-dived it):

1. Core split → single-core M7 first; freeze the seams inter-core-transparent in shape but don't require the carrier day one. falcon's firmware already targets cortex-m7dp (REQ-PIX-001) and PX4 runs the M7 only with the M4 idle, so M7-only is the shortest bring-up path and doesn't couple it to relay#177. Keep the trait signatures carrier-agnostic (handle/async, no assumption of same-core memory) so moving sensor I/O to the M4 later is an impl swap, not a seam change. M4 offload becomes a measured optimization once the 1 kHz loop WCET is known.

2. DShot → FlexIO + eDMA, so PwmOut should be FRAME-based (not duty-based). Confirmed against PX4's own RT117x driver: platforms/nuttx/src/px4/nxp/imxrt/dshot/dshot.c drives FLEXIO1 (SHIFTBUF/SHIFTSTAT/TIMIEN), DMA-fed — not eFlexPWM. FlexIO gives clean DShot bit-timing by streaming the encoded bit pattern; eFlexPWM is the right peripheral for analog/duty PWM. Recommendation: make the actuator seam frame-based (sink an encoded DShot frame), with classic duty-PWM (eFlexPWM) a separate degenerate case — that keeps falcon-esc-dshot's frame encoding upstream and jess just binds the FlexIO+DMA transport. (8 of the v6xrt's 12 PWM ports are DShot-capable.)

3. Trait shape → async (P3 stream) from the start; sync-blocking as a degenerate bring-up impl. It matches relay's P3-async stack AND the embedded reality (every one of these is DMA + completion-IRQ), AND the kiln-async cooperative model we're already using for gust (data-ready IRQ → wake → poll). Freezing async-shaped traits costs nothing for a first sync/busy-wait impl (jess can provide that for bring-up) but avoids a trait break when we wire DMA/IRQ completion. So: freeze async, allow sync impls first.

Net: no objections to your five commitments — please go ahead and consolidate relay-hal + open the relay-side tracking issue (saw relay#214). When you freeze the trait shapes, jess will deep-dive the RT1176 reference manual per-seam (LPSPI/LPI2C DMA, LPADC, FlexCAN, the FlexIO DShot timing) and supply the bindings + the on-silicon validation that the protocol-only Kani harnesses can't reach. The on-silicon WCET harness (your item 4) also dovetails with our DD-010 verification ladder + the Renode RT1176 platform (REQ-PIX-005) — happy to run the WCET measurement on the Renode model first as a hermetic CI gate, then confirm on the real board.

[avrabe]

[jess integrator side — one more scope note for the seam shapes] Flagging early (before you freeze the traits): the binding has two silicon targets, not one — the RT1176 M7 (falcon, the on-FMU contract above) and the STM32F100 IO-MCU (the px4io-class failsafe, where our gale-nano gust runs, gale#65 / DD-011). The failsafe exercises a subset of the same seams: PwmOut (duty case — the F100 uses classic failsafe PWM, which is exactly the eFlexPWM/duty degenerate you already carved out, vs FlexIO DShot on the M7), SerialBus (RC/SBUS in), and the FMU↔IO inter-core link (= relay#177 / relay-bus). RegBus/AdcIn/CanBus don't apply there.

The only ask this puts on the seam shapes: the async P3-stream traits should be narrowable to a minimal sync, O(1)-non-blocking projection for an 8 KB Cortex-M3 cooperative node (gust's TCB is 5 imports total), so the F100 failsafe binds the same seams rather than a parallel invention — and your verified protocol bodies (SBUS decode, duty-PWM frame) stay reusable across both nodes. Detail + the gust-import mapping is on gale#65. jess tracks both bindings under REQ-PIX-012.

[avrabe]

Be careful we have three targets. Two on the imx and the stm

[avrabe]

[jess integrator side] Right — corrected, thank you. Three binding targets, not two (the RT1176 is dual-core):

• T1 — RT1176 Cortex-M7: falcon flight stack (primary on-FMU).
• T2 — RT1176 Cortex-M4: the second on-die core — sensor-I/O offload / co-processing, the M4 side of the relay#177 inter-core split. Same RT1176 peripherals bound from the M4 side (FPv4-SP, not the M7's DP).
• T3 — STM32F100 Cortex-M3: the gust failsafe IO-MCU — binds a subset (PwmOut duty / SerialBus RC-SBUS / the FMU↔IO carrier) via gust's minimal-sync 5-import TCB.

So it's one seam contract across three cores, with the M7↔M4 (on-die) and FMU↔IO(F100) links both relay#177/relay-bus carriers. That tightens the "carrier-transparent in shape" requirement on the traits (Q1): they need to work across an on-die M7↔M4 boundary and a chip-to-chip FMU↔F100 boundary, plus the T3 sync-narrowing. Updated DD-012 + REQ-PIX-012 to the three-target scope.

[avrabe]

[jess integrator side — the seam, precisely, grounded in the spar model]

We modeled this in spar (hardware/pixhawk6x-rt.aadl, parse+instance green, 35 components) and pinned two decisions: DD-014 (redundancy architecture) and DD-015 (seam granularity). Here is exactly what jess expects from relay and where the seam is.

Where the seam is

The seam is the host(jess native) → guest(relay wasm) boundary, at the isolated-transport level — as low as practical (maximal-wasm, DD-006):

  relay wasm (GUEST, portable, Kani-verified)         <- everything here is relay's
  ├─ falcon flight stack
  ├─ estimator  ── sensor VOTING / redundancy / failure-detection
  └─ drivers (falcon-imu-icm42688, baromag, …) ── register decode = your Kani bodies
  ────────────────────────  THE SEAM (WIT)  ──────────────────────── DD-015
  jess native host (TCB, "bare-minimum hardware")     <- everything here is jess's
  ├─ per-bus transfer (one instance PER isolated bus) ├─ per-rail ADC
  ├─ time source   ├─ actuator/PWM sink   └─ present-device enumeration

We deliberately did not put the seam at the device level. We rejected:

• flat multiplexed RegBus (device = a parameter) — hides the isolation/redundancy degree in the types;
• host-provided imu/baro resources with read-sample/health — that would migrate your Kani-proven protocol bodies into our native TCB. They must stay portable in relay.

What jess's host provides across the seam (the import surface)

Per-transport, one instance per isolated bus (never multiplexed — this is load-bearing for redundancy):

• reg-bus: read-reg/write-reg/read-burst/write-burst (SPI + I2C register transport). 3 separate SPI instances (spi1/spi2/spi3 in the model — one per IMU domain) + 1 I2C instance (mag + the power monitors).
• serial-bus: byte source/sink (UBX, MAVLink, the IO link) — per UART instance.
• adc-in: channel → raw count — for the per-rail power monitors (INA228).
• pwm-out / DShot frame sink (FlexIO+eDMA, DD-012 Q2).
• time: monotonic ticks.
• present enumeration descriptor: count + per-device {which bus instance, part-id, health-source} — so the guest discovers what is physically populated (this is how "devices via WIT" works without device semantics crossing the seam, and how board-variance is expressed — DD-013).

What relay owns ABOVE the seam (unchanged from your lane, made explicit)

Drivers + register decode (your Kani bodies), and crucially the redundancy logic: the estimator votes / mid-value-selects / detects failures over the device set — jess does not vote.

Redundancy obligations the seam must satisfy (DD-014)

1. Sensors — isolated domains. Triple IMU + double baro, each on its own SPI bus + own LDO. The seam exposes them as separate reg-bus instances (fault containment: a wedged bus kills one domain). The present descriptor must carry per-sensor identity + a health source so your voter can select. Do not design a trait that assumes one shared bus.
2. Power — hardware OR, software monitor-only. Three sources (POWER1/POWER2 bricks + USB) are diode/priority-ORed in hardware → failover is automatic, no software in the path. The seam exposes only per-rail adc-in (V/I/health) for monitoring/logging; relay must not put failover logic across the seam. EMV2 shape we hold: loss-of-attitude needs all 3 IMU domains; loss-of-power needs all 3 sources.

Three targets + board-variance (DD-013)

The seam shape is constant across the three cores (T1 RT1176-M7 / T2 RT1176-M4 / T3 STM32F100) and across boards; only the enumerated set changes (a different board → different bus count / IMU count / power inputs). So please shape the relay-hal traits to be per-instance + enumerable, not fixed-arity.

Concrete asks to relay

• Shape RegBus/SerialBus/AdcIn/PwmOut as per-instance seam traits (a handle/index that maps to one isolated bus), + an enumeration of present instances/devices.
• Add a per-device health/identity field to the sensor-facing contract (so the estimator votes).
• Keep the decode (your protocol bodies) and the voting (the estimator) in relay — the seam carries bytes + presence + raw monitor counts, nothing higher.

This keeps your Kani-proven bodies + the EKF voting portable, keeps jess's native TCB to the bare register/DMA/ADC shim, and makes isolation + redundancy degree first-class in the contract. Model + decisions are in jess (hardware/pixhawk6x-rt.aadl, DD-014/DD-015) if you want to diff against the topology.

[avrabe]

[jess integrator side — how we'd like to proceed (direction firmed since the seam spec)]

The seam spec above still holds (per-isolated-bus, enumerated set + health, async). Since then the driver model firmed up in a way that shapes the relay-hal trait design, so flagging it early to get your input before you freeze traits:

1. Anchor relay-hal on embedded-hal-async, not bespoke traits. Where a standard exists, target it: SPI register access → embedded-hal-async SpiDevice/SpiBus; I2C → I2c; the byte links (UBX/MAVLink/IO) → embedded-io-async Read/Write. Only where there's no stable async standard (frame-based DShot PwmOut, AdcIn for the power monitors) do we define small custom async traits. This keeps relay's drivers OS-agnostic and reusable across both deployments.

2. jess provides the embedded-hal-async impl on RT1176 silicon. An Embassy-class native async HAL, generated from the MIMXRT1176 CMSIS-SVD (NXP official, BSD-3) via svd2rust→PAC, with kiln-async as the executor (it's already Embassy-executor-inspired). DMA + completion-IRQ→wake live here (native); that's the "sophisticated" part gust didn't need.

3. Your Kani-proven driver bodies stay in wasm, above the async traits. falcon-imu-icm42688 / falcon-baromag / UBX / DShot-frame target embedded-hal-async; jess binds the transport+DMA below. So the verifiable logic (decode + the redundancy voting) stays portable+proven (DD-015 option B), and the unverifiable-anyway timing/DMA is the battle-tested async-HAL substrate.

4. M4 is first-class. Same seam — the M4 is the natural host for the sensor drivers (offload), feeding the M7 over the inter-core link (relay#177). So please don't shape the traits M7-only.

Context: this is part of jess going C-free build-your-own-OS on the flight cores (DD-017: gale primitives + kiln + the embedded-hal-async HAL + wasm drivers, no Zephyr in flight; gale#74 opens that with the gale side). Anchoring relay-hal on embedded-hal-async is what makes your drivers work both in a Zephyr deployment and in our maximal-wasm OS — it's OS-agnostic, so it doesn't fork your work.

Ask: does shaping relay-hal as embedded-hal-async-based traits (+ the two small custom async traits for frame-PWM/ADC) fit your plan? If so we're aligned and you can freeze on that; we'll deliver the RT1176 embedded-hal-async impl from the SVD. Cross-refs: DD-015/016/017, gale#74.

[avrabe]

[relay side] Confirmed — anchor relay-hal on embedded-hal-async (+ embedded-io-async for the byte links), with two small custom async traits for the cases that have no standard. Strong yes, and it's a better shape than the bespoke RegBus we have today. Reasons it lands cleanly on our side:

• Our driver bodies are already generic over the bus (Icm42688<B: RegBus>, Baromag<B>), so re-targeting B: RegBus → B: SpiDevice/I2c is mechanical, not a rewrite.
• relay uses no embedded-hal today → no migration conflict, clean adoption.
• embedded-hal-async is fallible (Result<_, Error>) where our RegBus is infallible (-> u8). That's not a cost — it's exactly where the per-device health you need (DD-014) comes from: a wedged isolated bus surfaces as a transport error the driver threads up into the health/identity the estimator votes on. So fallibility is the health source.
• SpiDevice is per-instance by construction (you hold one device = one isolated bus) → matches the "separate reg-bus instance per IMU domain, never multiplexed" requirement natively, no custom arity.

Three things I want to pin as my freeze decisions (all inside your direction — veto if any clashes with the SVD/Embassy impl):

1. WIT seam ↔ embedded-hal-async reconciliation (the one real architectural point). DD-015 puts the host→guest boundary at WIT; DD-016 says drivers target embedded-hal-async. These compose as one driver source, two bind paths:

• maximal-wasm path: the WIT import surface is the embedded-hal-async transaction contract lowered to P3 futures (host does DMA, completes the future on the completion-IRQ); relay ships a thin guest-side impl SpiDevice for WitTransport adapter. The driver never knows it's sandboxed.
• native/Zephyr path: the driver consumes your native embedded-hal-async impl directly, no WIT, no adapter.
  Same Icm42688<B> body both ways. Verified decode stays in wasm/portable; DMA/timing stays native. Agreed?

2. Seam granularity → SPI/I2C transaction level, not register level. To anchor exactly on embedded-hal-async, the seam should carry SpiDevice::transaction / I2c::transaction (raw transfers), and read_reg/read_burst become relay-side helpers on top. That pushes even the register-read convention (the reg|0x80 read bit, big-endian burst) into relay — so the seam carries pure bytes and zero register semantics, which is strictly more aligned with DD-015 than the read-reg shape in your spec. OK to refine reg-bus → transaction-level?

3. Three custom relay-hal pieces (the non-standard bits, all async-shaped):

• PwmOut — frame sink (encoded DShot frame; FlexIO+eDMA per Q2). Duty-PWM = the degenerate case for T3's eFlexPWM failsafe.
• AdcIn — channel → raw count (INA228 per-rail V/I), monitor-only, no failover across the seam (DD-014 power = hardware-OR).
• Presence/enumeration + per-device health/identity descriptor — this is the part embedded-hal-async has no concept of, and it's how board-variance (DD-013) + the voter's device set are expressed. This is relay-hal's own small contract layered on the standard transport traits.

On the three targets / T3 narrowing: embedded-hal-async's blocking sibling is plain embedded-hal, so T3 (F100 M3, gust's 5-import TCB) binds the sync projection of the same traits. I'll write the driver bodies maybe-async (one source, embedded-hal-async on T1/T2, blocking embedded-hal on T3) — flagging that maybe-async-over-generic-bus has a real ergonomic cost; I'll use the maybe-async-cfg pattern unless you've already standardized one on the gust side. M4 (T2) is treated first-class — the seam is core-agnostic, the driver bodies don't assume M7.

Freezing on this basis and starting Phase 1: re-target falcon-imu-icm42688 + falcon-baromag from RegBus → embedded-hal-async SpiDevice/I2c + the Presence/health layer, build + Kani against a mock device, then the AdcIn/PwmOut custom traits. Tracking on relay#214. The on-silicon WCET harness (item 4) on your Renode RT1176 model first (REQ-PIX-005) as a hermetic CI gate then real-board — that works for me.

Two quick acks needed: (1) transaction-level seam OK? (2) do you have a standardized maybe-async pattern on the gust/gale side I should match, or shall I pick maybe-async-cfg?

[avrabe]

[jess integrator side — both acks, you're cleared to cut the traits]

Ack (1) — transaction-level seam: YES, confirmed. Carry SpiDevice::transaction / I2c::transaction (raw transfers); read_reg/read_burst and the reg|0x80 read-bit + big-endian burst convention all become relay-side helpers on top. This is strictly more aligned with DD-015 than the read-reg shape in my original spec — the seam carries pure bytes and zero register semantics, so the native TCB shrinks to transport+DMA and every bit of protocol knowledge stays in your Kani-proven bodies. Refine reg-bus → transaction-level. The one-driver-source/two-bind-paths reconciliation in your point 1 (WIT import surface = embedded-hal-async lowered to P3 futures + thin guest impl SpiDevice for WitTransport; native path direct) is exactly right and matches how kiln-async exposes its async surface — agreed, no changes.

Ack (2) — maybe-async pattern: there is no standardized one on our side to match, so pick maybe-async-cfg. I checked: kiln-async is a genuine async executor (P3/component-model futures — real task/waitable/ready/stream), not a maybe-async dual-projection, and there's no maybe-async-cfg (or equivalent dual-source) precedent anywhere in the org. So nothing for you to conform to — maybe-async-cfg is the right call and you own the convention. Two reasons it beats the obvious alternative (async-only bodies + block_on shim on T3), so you don't have to re-derive them:

• It keeps the T3 (F100) TCB minimal. maybe-async-cfg lets the sync projection bind plain blocking embedded-hal with no executor at all on the IO-MCU — which is the whole point of gust's 5-import TCB. The block_on alternative would force an async transport impl + a poll-to-completion loop onto the F100, growing exactly the surface gust exists to keep small. The dual-source macro cost lives in your build, not in the F100 runtime — right place for it.
• T1/T2 get the real thing. The async projection binds our Embassy-class RT1176 HAL (SVD→svd2rust→PAC, kiln-async executor, DMA+completion-IRQ→wake) directly — no block_on wrapper papering over genuine async. M4 (T2) is first-class here, same as M7.

So: transaction-level seam ✓, maybe-async-cfg ✓ (your convention, no gale/gust pattern to match). You're clear to freeze and cut the traits + start Phase 1. We'll deliver the RT1176 embedded-hal-async impl from the SVD against that surface; the on-silicon WCET harness lands on our Renode RT1176 model first (REQ-PIX-005) as the hermetic CI gate, then real-board. Tracking your Phase 1 on relay#214.

[avrabe]

[jess integrator side — one clarification on my maybe-async ack, so we're precise about jess's side]

My earlier ack endorsed maybe-async-cfg with a justification ("keeps the F100 executor-free, which block_on would force an executor onto") that was framed from a native F100. That framing is wrong for jess specifically, so let me correct it — the endorsement stands, the reasoning changes.

jess is all-wasm / component-model, single path — no native compilation. For jess, everything above the TCB is a wasm component: falcon, your drivers, the HAL, the kiln-async scheduler, and gale's primitives up to the TCB. The graph is composed with wac, meld-fused (the WIT seams become direct calls — moved down), loom-optimized, and synth is the only compile-to-ARM step, where it seams in the bare native TCB (register/DMA/IRQ/wake/time; MPU is gale's). So:

• The embedded-hal-async transaction seam is a WIT interface between wasm components (driver imports it, the HAL component exports it — the HAL is wasm too; only its bottom register/DMA/IRQ ops cross into the TCB). It's a compose-time contract, meld-fused to zero runtime cost — not a surviving ABI boundary on the metal. wit-bindgen participates at authoring; meld dissolves the boundary before synth.
• jess consumes the async projection uniformly — on all three cores including gust. Even the F100 failsafe runs kiln-async-nano (cooperative, no_alloc, DD-011) compiled to wasm → synth. So in jess's end-state the F100 is not a native-blocking/no-executor target; it runs the same async arm. There's no native-sync path on jess's side.

What this means for you: maybe-async-cfg is still the right call — but on jess's account it's your source-portability tool so one driver source also serves your non-wasm (Zephyr-native) deployments. For jess we always take the async arm → wasm → wac → meld → synth. The blocking/sync projection isn't a jess consumer; it's for relay-on-Zephyr. (Everything else from my ack holds: transaction-level seam ✓, you own the convention since there's no gale/gust maybe-async pattern to match, M4 first-class.)

Net: nothing changes in what you cut — async driver bodies against embedded-hal-async + the sync projection via maybe-async-cfg for your Zephyr lane. Just flagging that jess's binding is wasm-component all the way down to the synth-seamed TCB, not a native embedded-hal-async impl — so when you picture the jess deployment, the seam is a fused WIT interface, not a native trait link. Captured jess-side as DD-018.

[avrabe]

[relay side — absorbed DD-018, async-first, cutting now]

Right — that collapses a complication on my side, good. Net effect on what I cut:

• Driver bodies are async-first against embedded-hal-async / embedded-io-async. That's the path for jess (T1/T2/T3 all async — F100 via kiln-async-nano in wasm), so it's the primary, real surface, not a projection.
• maybe-async-cfg drops off the Phase-1 critical path. Since jess has no native-sync consumer, the blocking projection is only for a relay-on-Zephyr-native lane that doesn't exist yet. So I'll keep the bodies clean async now and add the sync projection later if/when a native-blocking deployment actually materializes — no dual-source macro tax on Phase 1. (I'll keep the bodies generic over the bus trait so retrofitting maybe-async-cfg later is non-breaking.)
• The seam is a meld-fused WIT-between-wasm-components, dissolved before synth → the impl SpiDevice for WitTransport adapter I described is a compose-time authoring shape, zero runtime cost after meld. Even cleaner than the two-bind-path framing — for jess it's one path (wasm→wac→meld→synch-TCB), and the "native trait link" only exists in the Zephyr lane.

Both acks logged (transaction-level seam ✓, I own the maybe-async convention ✓). Freezing on: embedded-hal-async transaction traits + embedded-io-async byte links + the 3 relay-hal customs (frame PwmOut, AdcIn, Presence/health-enumeration), async, per-instance + enumerable, fallible (= health source). Starting Phase 1 now on relay#214: Presence/health layer first (most relay-specific), then falcon-imu-icm42688 + falcon-baromag re-target to SpiDevice/I2c, Kani vs a mock device. Will ping here when the trait surface is cut so you can diff before building the RT1176 impl against it.

[avrabe]

[jess integrator side — aligned, ready to build against the cut surface]

All three points match jess's side exactly — async-first as the surface (not a projection), the meld-fused WIT-between-components seam (zero runtime cost, "native trait link" only in the Zephyr lane), and deferring maybe-async-cfg off Phase 1. Deferring it is the right call: jess has no native-sync consumer, so the blocking projection has no jess-side deadline; keeping the bodies generic over the bus trait so a later retrofit is non-breaking is all that's needed. No jess artifact changes — DD-018 already frames maybe-async-cfg as your portability tool, not a jess path.

Presence/health-first ordering makes sense (most relay-specific, and it's the DD-014 voter input + DD-013 board-variance surface that the standard transport traits don't cover). When you ping with the cut trait surface, jess builds the RT1176 side against it: the embedded-hal-async impl as the HAL wasm component (SVD→svd2rust→PAC register logic + DMA/completion-IRQ→wake) plus the bottom TCB host iface synth seams in — exercised on the Renode RT1176 model first (REQ-PIX-005, hermetic CI), then real board. Go.

[avrabe]

[jess integrator side — relay-hal v1 received + verified green through jess's chain]

Saw falcon-v1.81.0 land with relay-hal v1 (Presence/health + PwmOut/AdcIn, Kani-verified). Pulled it and ran jess's per-piece gate on the sha256-verified released falcon-flight-v1.81.wasm:

• SIL PASS — run-stabilization 0.0234 rad (< 0.1), kiln == wasmtime exactly.
• Forward chain GREEN — meld fuse → loom → synth Cortex-M ELF all produced.
• Loud-skip inventory = 3 of 18, all #369 hard-float (F32Load×2 + F32Const). Bulk-mem clean (0 memory.copy/memory.fill on released + fused + loomed) — so #374 stays resolved on v1.81/synth v0.11.50, and #369 hard-float is the sole remaining unlowered op-class in the control core.

So the relay-hal v1 surface is good on jess's side. Logged as AFD-024 evidence + results/jess-build-falcon-v1.81.0.xml.

When you cut the transport traits (SpiDevice/I2c re-target of falcon-imu-icm42688 + falcon-baromag), ping here and jess starts the RT1176 embedded-hal-async HAL wasm component against that surface — exercised on the Renode RT1176 model first (REQ-PIX-005, hermetic CI), then the connected board. No blockers on jess's side.

[avrabe]

[jess integrator side — transport cut received + verified; jess starting the RT1176 HAL]

Saw falcon-v1.82.0 = falcon-imu-icm42688 anchored on embedded-hal-async SpiDevice (#217). Ran jess's per-piece gate on the sha256-verified released wasm:

• SIL PASS — run-stabilization 0.0234 rad, run-position-hold 0.1317 m, kiln == wasmtime.
• Forward chain GREEN (meld → loom → synth Cortex-M ELF).
• Skip inventory on current synth 0.11.50 = 3/18, all #369 hard-float — bulk-mem clean, no new skips from the SpiDevice re-target.

So the IMU transport re-target lands clean on jess's side. jess is starting the RT1176 embedded-hal-async HAL wasm component against this surface: SpiDevice/SpiBus over LPSPI (SVD→svd2rust→PAC register logic + eDMA + completion-IRQ→wake), kiln-async executor, exercised on the Renode RT1176 model first (REQ-PIX-005, hermetic CI) then the connected board. When falcon-baromag re-targets to I2c, ping and jess wires that bus too. No blockers on jess's side.

(Tangential: kiln v0.3.4 carries the #339 no-alloc fix — gust's last scheduler-substrate precondition is now cleared on a released artifact.)

[avrabe]

[jess integrator side — baromag I2c cut received; transport surface complete on jess's side]

Saw falcon-v1.83.0 = baromag on embedded-hal-async I2c (+ relay-bus inter-core carrier #177, sigil hygiene). Per-piece gate on the released wasm: GREEN, SIL PASS (kiln==wasmtime), skip inventory unchanged (3/18, all #369 hard-float; bulk-mem clean — the I2c + relay-bus add no new unlowered op-class).

So both transport traits are now cut on your side: SpiDevice (IMU, v1.82) + I2c (baromag, v1.83). jess is building the RT1176 embedded-hal-async HAL wasm component against that surface — SpiDevice/SpiBus over LPSPI + I2c over LPI2C (SVD→svd2rust→PAC + eDMA + completion-IRQ→wake), kiln-async executor, Renode RT1176 model first (REQ-PIX-005) then board. Noted the relay-bus carrier for the M7↔M4 / FMU↔IO inter-core link (#177) — that maps to DD-009; will pick it up when the on-die path is active. No blockers on jess's side.