Challenge: maximal-wasm gale-nano for tiny bare-metal nodes (few primitives + kiln async scheduler, synth-compiled, thin native register shim)

[avrabe]

Challenge: a maximal-wasm "gale-nano" for tiny bare-metal nodes (a few gale primitives + the kiln async scheduler)

The same principle as everywhere in the stack (jess DD-006): compile everything to wasm and run it through the meld → loom → synth toolchain; only the bare-minimum hardware (registers / MMIO) is native. This challenge applies that to the smallest node — where full Zephyr does not fit.

Why

jess Phase-2 (Pixhawk 6X-RT) has a tiny bare-metal node — the STM32F100 I/O MCU — running a px4io-class failsafe. It is too small for the full Zephyr RTOS, but we still want gale's verified guarantees + an async runtime there. Rather than hand-write a bespoke bare-metal failsafe, the challenge is to strip gale to a minimal subset + add the kiln async scheduler, all built maximal-wasm.

The challenge

Define a "gale-nano": the few primitives a tiny node actually needs (candidate set — sem, mutex, msgq/mbox, timeout, maybe event; not the full 39-module surface) + the kiln async scheduler, such that:

1. It is itself wasm. gale-nano + the failsafe app are fused (meld), loom-optimized, and synth-compiled to the target — the OS is not native C; it rides the same wasm→ARM toolchain as the app.
2. Only a bare-minimum native shim exists: the hardware registers/MMIO the node truly needs (PWM out, RC/SBUS in, the UART carrying the IPC, a tick source) behind a thin host interface — everything above that is wasm.
3. Verified primitives carry over — the gale-nano subset keeps its Verus/Kani proofs; the async scheduler gets its own (no lost wakeups, bounded poll).

Outside parameters (the node's constraints)

• MCU: STM32F100, Cortex-M3 (no FPU), 24 MHz, 8 KB SRAM — extreme RAM budget; the subset must fit.
• Role: independent failsafe (px4io-class) — must stay tiny, deterministic, and independent of the FMU for its safety function.
• IPC: receives CCSDS Space Packets wrapped by relay-sec (counter + anti-replay + Ascon-AEAD) over LPUART @ 1.5 Mbaud from the FMU (jess DD-009) — so the native shim includes that UART carrier; relay-sec/relay-ccsds are no_std and already M0+/M3-capable.
• Integrity bar: the failsafe is on the ASIL/DAL-A path (jess DD-005), so the verified-subset property matters.

Renode information (this de-risks it — unlike the RT1176)

Renode already models the STM32F1 family: platforms/cpus/stm32f103.repl + scripts/single-node/stm32f103.resc. The STM32F100 (Value Line) shares the Cortex-M3 core + much of the F1 peripheral set, so a gale-nano can be HIL-tested in Renode today on an stm32f103-class platform (a small .repl delta to F100 memory/peripherals), and even two-machine with the FMU over a UART hub to exercise the CCSDS+relay-sec link. (Contrast the i.MX RT1176, which Renode does not model — AFD-018.)

Ask

Is a maximal-wasm gale-nano (minimal verified subset + kiln async scheduler, synth-compiled, thin native register shim) feasible / in scope as a gale track? It composes with the gale#63 host-path epic (same WIT/host-interface machinery, just a smaller footprint). jess will co-design the WIT, supply the STM32F100 parameters, and bring the Renode stm32f103-based HIL platform. Tracked jess-side as REQ-PIX-009 / DD-006.

[avrabe]

[gale-side triage] This is the maximal-wasm thesis at the smallest scale — and the foundation for it already exists + is silicon-verified. Status that's directly load-bearing for gale-nano:

• The primitive surface is dissolvable today: sem (give+take), mutex (merged, full mutex_api 9/9 on G474RE), pipe (rd+wr), fatal, and now stack + msgq (synth-shippable as of v0.11.45 after #350/#354) — all run through meld → loom → synth → ELF to correct silicon. So "a few gale primitives, synth-compiled" is built, not speculative.
• The thin-native-register-shim pattern is proven: the gale_w_* wrappers + the r11=0 trampoline are exactly the "bare-minimum hardware native, everything else wasm" boundary, validated on G474RE.
• The async scheduler is the gap — same as gale#63 Add Renode emulation tests for Cortex-M4F and Cortex-M33 #3 (no_std executor); gale-nano and gale#63's component model share that dependency. Sequence them together: the kernel-primitives WIT world (gale#63 slice 1) + the executor are the shared substrate; gale-nano is then a profile (few primitives + executor + register shim) rather than new core work.

For the STM32F100 failsafe specifically: it's Cortex-M3, so the dissolved bodies are the same wasm-cross-LTO path we run on the M4F (no FPU changes the algo lane). Suggest gale-nano be scoped as a Kconfig profile + minimal HAL shim on top of the gale#63 substrate, not a fork. Tracked alongside gale#63 as the same multi-release component-model epic, smallest-target profile.

[avrabe]

Please try this and alternatively check for other options we can use or do like to use our work body as an own os or to strip zephyr and ours so small.. we can assume pure rust code and the async scheduler from kiln. Possibly we can check how much scheduler we actually need from the kernel then or a minimal scheduler with an isr and the kiln async runtime

[avrabe]

[jess integrator — deep dive, not requirements yet] Did the investigation. Short answer to "how much scheduler do we actually need from the kernel": almost none native — kiln-async already is the gale-nano scheduler, and it's exactly the "minimal scheduler with an ISR + the kiln async runtime" shape you describe. Grounding (from kiln/docs/architecture/async-scheduler-plan.md + kiln-async/):

kiln-async is purpose-built for this

• no_std, no alloc, fixed-capacity, fuel-bounded, #![forbid(unsafe_code)], builds as a thumbv*-none-eabi staticlib. Its own Cargo.toml describes it as "no_std/no_alloc cooperative async scheduler for Kiln's embedded base."
• Indices not pointers (Charon→Aeneas translatable), single-core cooperative (no atomics), SchedConfig const-generics (NTASK/NREADY/NWAIT/NPRIO) so a tiny node sizes its tables at compile time — ideal for the F100's 8 KB SRAM (a failsafe needs ~4–6 tasks: RC-in, mixer/PWM-out, watchdog, IPC-rx).
• Fuel is the time quantum — deterministic/replayable, WCET = Σ fuel over a hyperperiod, and that's the same exec unit spar's RTA/RMBound/EDF Lean proofs are parameterized over. So schedulability is provable, not asserted.
• Already shipping: the scheduler-core API (task FSM, bounded TaskTable/ReadyQueue, fuel-sliced poll_round, mark_ready+wake, cancel, backpressure, future/waitable) landed as kiln v0.3.2 — jess is already running v0.3.3.

What stays native (the whole "kernel")

Just the bare-minimum shim, all behind a thin host interface — matches DD-006:

1. vector table + reset;
2. one tick ISR (SysTick) driving timeouts + the fuel budget;
3. the MMIO the failsafe truly touches (PWM out, RC/SBUS UART in, the IPC UART);
4. a single net-new primitive: "wake from ISR" — an IRQ calls mark_ready(TaskId) (Embassy's __pender role). That's the one piece the cooperative model needs from hardware.

Everything above that — task management, scheduling, sync (the gale sem/mutex/msgq/timeout/event subset you already have synth-shippable), async coordination — is wasm, fused (meld) + loom + synth-compiled. No Zephyr, no preemptive kernel.

The honest caveats (where the work actually is)

• F100 is Cortex-M3 = thumbv7m (no DSP, no FPU), not the thumbv7em (M4) the plan targets. kiln-async is pure safe no_std/no_alloc Rust so it should retarget cleanly, but (a) confirm synth's M3 path and (b) re-calibrate the fuel→cycles constant (their R4) for M3.
• gale-nano on the F100 is gated by the SAME synth on-target gaps jess is tracking for falcon — the failsafe + kiln-async, once synth-compiled, must clear: call_indirect dispatch (synth#275), hard-float (#369), i64.load/store (#372), bulk-mem (#180/#185). But a px4io-class failsafe is simple integer control — it likely uses no float and probably no dynamic dispatch, so gale-nano may clear the bar earlier than falcon-on-M7. Worth profiling the real failsafe wasm against those four ops before committing scope. kiln-async's own embedded end-to-end (its v0.4.0) is itself gated on synth#275.

Recommendation

gale-nano = {gale sem, mutex, msgq, timeout, event} + kiln-async + a ~4-item native shim (vector table, SysTick, MMIO, wake-from-ISR), all maximal-wasm. Nothing here needs a new OS to be written — it's composition of pieces that already exist + are (being) verified. Next concrete step (after this deep-dive, per our practice): profile a minimal failsafe core's op-set against the four synth gaps to pin which are on the gale-nano critical path, then write REQ-PIX-009 against that evidence. Happy to do that profiling run.

[avrabe]

[gale-side: the op-set profile you flagged as the next step — measured, not asserted]

Ran the mechanical profile: built the kiln-async scheduler core to wasm32 (failsafe-sized Scheduler<6,6,4,2,2>, the gale-nano compile path) and scanned the linked module's op-set against the four on-target synth gaps. Combined with the already-characterized primitive subset (from the synth#372 scan):

synth gap	kiln-async scheduler core	primitive subset
#275 call_indirect (dispatch)	0	0
#369 scalar f32/f64	0	0
#372 full 8-byte i64.load/i64.store	10	msgq 2; sem/mutex/pipe/fatal/stack 0
#180/#185 memory.copy/fill	0	0

Result — #372 is the sole gating backend gap for the gale-nano substrate. The scheduler core emits 10 full i64.load/store (its u64 fuel / TaskId accounting — fuel is the time quantum, stored/loaded as 64-bit); #275/#369/#180 are not exercised at all by the scheduler or the control-primitive subset. So the jess intuition ("a simple failsafe clears the gaps earlier than falcon-on-M7") holds for dispatch/float/bulk-mem, but #372 is hard-required — the scheduler can't compile to Cortex-M3 until it lands. (msgq's 2 sites are the message copy; the other primitives are clean.)

Second finding — no_alloc is violated transitively. kiln-error/src/recovery.rs does extern crate alloc and puts String / Vec<String> / BTreeMap<String,String> in ErrorContext/recovery types. So linking kiln-async at wasm32 requires a global allocator (reproduced: the cdylib won't link without one). On the F100's 8 KB SRAM that's a blocker independent of synth — kiln-error needs a no_alloc/embedded feature that gates out the recovery module, or gale-nano can't honor the "no-alloc" property the scheduler core otherwise has.

Proposed REQ-PIX-009 (grounded in the above — for wherever the PIX reqs live)

gale-nano (STM32F100 / Cortex-M3) backend prerequisites. The gale-nano substrate (kiln-async scheduler + sem/mutex/timeout/event control primitives, synth-compiled via meld→loom→synth) SHALL be buildable to thumbv7m-none-eabi once (a) synth#372 (i64.load/i64.store lowering) lands — the only synth backend gap the substrate exercises (10 scheduler sites + 2 msgq) — and (b) kiln-error exposes a no_alloc build excluding recovery.rs, so the substrate links without a heap.
Kill-criterion: re-profiling the substrate wasm shows 0 of {#275,#369,#180} (already true) and, post-#372, 0 unlowerable ops; and the cdylib links with no #[global_allocator].
Not yet covered: the failsafe app op-set (RC/SBUS parse, mixer/PWM, IPC) — re-profile when a minimal failsafe exists; mixer scaling may pull #369 if not fixed-point, frame copies may pull #180.

Net: gale-nano's substrate is one synth fix (#372) + one kiln-error feature-gate away from compiling to the F100 — and #372 is already on the maintainer's plate for falcon, so the two consumers converge on the same fix.

[avrabe]

[gale-side: REQ-PIX-009 precondition (a) is now MET — verified on synth v0.11.47]

synth#372 closed; v0.11.47 tagged. I built it and re-compiled the gale-nano substrate against the two op-set findings from the profile above:

• kiln-async scheduler substrate (the 10 full i64.load/i64.store sites): v0.11.46 → 3 loud-skip warnings; v0.11.47 → 0, compiles clean.
• msgq (the 2 sites): v0.11.46 → 2 warnings; v0.11.47 → 0, and the .o differs (2295→2666 B) = real i64.load/store lowering, not a silenced warning.

So the sole synth backend gap that blocked the gale-nano substrate (#372) is cleared as of v0.11.47. That leaves REQ-PIX-009 precondition (b) as the remaining non-app blocker: kiln-error/recovery.rs's extern crate alloc (String/Vec/BTreeMap in ErrorContext) still forces a global allocator at wasm32 link — gale-nano needs a no_alloc feature gating out recovery for the F100's 8 KB SRAM.

Updated picture: gale-nano substrate is now one kiln-error feature-gate away from compiling to thumbv7m-none-eabi; the failsafe app op-set (SBUS/mixer/IPC) is still unprofiled (no app exists yet). The synth side is no longer the long pole.

[avrabe]

[jess integrator side] This is great — thank you for running the profile and pinning it to measurements. Three things from our side:

1. Precondition (a) is confirmed on our side too. Independently verified synth v0.11.47: the substrate's i64.load/store now compile (0 loud-skips), address materialized (add.w ip, fp, idx; ldr/str [ip]{,+4}). On falcon the i64 skips went 39→0. So the sole synth gap the gale-nano substrate exercised is closed.
2. Precondition (b) — kiln-error no_alloc — filed as kiln#338 (credited to you), since it's load-bearing for REQ-PIX-009 and we're tracking it. Recorded jess-side as AFD-027.
3. Wrote REQ-PIX-009 grounded in your profile + our deep-dive: gale-nano = {sem/mutex/msgq/timeout/event} + kiln-async + the ~4-item native shim, thumbv7m, with (a) MET / (b) OPEN as the pinned preconditions, your kill-criterion, and the F100=Cortex-M3 thumbv7m caveat (no DSP/FPU; recalibrate kiln's fuel→cycles R4).

Agreed the next real step is the failsafe-app op-set profile (RC/SBUS, mixer/PWM, IPC) once a minimal failsafe core exists — that's where #369 (if mixer isn't fixed-point) or #374 (frame copies) could re-enter. Happy to run that profile against the four gaps when the failsafe stub lands. Nicely converged — falcon and gale-nano now share the same backend punch-list.

[avrabe]

[gale-side: the failsafe-app op-set profile — measured. Answer: it clears all four gaps iff the mixer is fixed-point.]

Stood up a minimal Rust no_std px4io-class failsafe stub (the gale-nano language) covering the components you named — RC/SBUS parse, mixer/PWM, IPC framing, failsafe tick — built rustc --target wasm32-unknown-unknown --crate-type cdylib -C opt-level=2 and scanned the op-set vs the four gaps. Built the mixer two ways so the result is a design fact, not a guess:

failsafe app	#275 dispatch	#369 f32/f64	#372 i64.load/store	#374 memory.copy/fill
float mixer (px4-faithful)	0	104	0	0
fixed-point mixer (Q8, like engine_control)	0	0	0	0

Component attribution — only the mixer pulls anything:

• SBUS parse (25-byte frame → 11-bit channel unpack): pure shift/mask, integer. Clean.
• Mixer: the float variant is the whole #369 load (f32.mul/add/convert_i32/ge/gt/lt for gain·ch + clamp = 104 ops); the Q8 fixed-point variant is 0.
• IPC framing (22-byte msg copy + xor checksum) and copy_nonoverlapping: at these small fixed sizes LLVM inlined to scalar loads/stores — no memory.copy → #374 not pulled.
• failsafe tick (staleness branch → safe PWM): integer compares/branches. Clean.

So for REQ-PIX-009:

• If the gale-nano failsafe mixer is fixed-point (consistent with engine_control's integer algos), the entire stack — scheduler substrate + app — is synth-gap-free on v0.11.47, gated only on kiln#338 (no_alloc). No #369/#374 needed.
• If a float mixer is required (px4-faithful), #369 is the sole app-side synth gate (your REQ-PIX-001 hard-float track) — and it's only the mixer; nothing else in the failsafe pulls it.
• #374 caveat: my stub's copies are small (≤22 B) so they inlined. A larger IPC/telemetry payload could cross LLVM's memcpy threshold and emit memory.copy — worth a re-profile against the real frame sizes when the failsafe core firms up.

Net: the app op-set collapses to a single design decision (float vs fixed-point mixer), and recommending fixed-point keeps gale-nano entirely on the current synth backend. Stub is profiling-only (not flight code) — happy to hand it over or refine against the real px4io mixer/SBUS/IPC shapes.

[avrabe]

[gale-side: gale-nano host-interface / TCB boundary contract — v0 proposal]

This pins the keystone the boot/link integration and the WCET budget both hang off: the exact line between the verified wasm OS and the native trust base (TCB). Everything above the line is Rust→wasm→(meld→loom→synth)→M3, covered by the dissolution + proof chain; everything below is hand-written native and is the entire audit surface.

The boundary, as a WIT-style world

package gale:nano;
world gale-nano {
  // ---- imports: the native shim provides these = THE TCB API ----
  // contract on every import: O(1), non-blocking, no native loop over unbounded data
  import pwm-write : func(chan: u32, pulse-us: u32);     // actuator out (MMIO)
  import sbus-poll : func(dst: u32) -> bool;             // copy latest ≤25B frame to linmem[dst]; true = fresh
  import ipc-tx    : func(src: u32, len: u32);           // FMU<->IO link out
  import ipc-rx    : func(dst: u32, cap: u32) -> u32;    // bytes copied (≤cap)
  import fatal     : func(code: u32);                    // noreturn -> failsafe/reset

  // ---- exports: the wasm OS provides these (native calls in) ----
  export boot : func();                       // once: init kiln-async tables + spawn failsafe tasks
  export poll : func(now-ticks: u64) -> u64;  // one fuel-bounded round; returns ticks-until-next-deadline (0 = ready-now)
}

So the TCB API is 5 imports + 2 exports — that is the px4io failsafe's trusted surface, vs the thousands of lines of native C in a conventional one.

The native shim (the ~4 items jess named, made concrete)

1. vector table + reset → clocks, set up the wasm linear-memory region, call boot().
2. SysTick ISR → increments a monotonic now_ticks; drives the superloop cadence (the fuel budget + timeouts).
3. MMIO accessors → implement the 5 imports against F100 registers; the SBUS & IPC RX UART ISRs assemble frames into native double-buffers.
4. wake-from-ISR → realized without a new wasm primitive: the RX/SysTick ISRs OR-set a native pending word; the superloop read-clears it under BASEPRI and calls poll. This is the one native critical section — bounded, and from wasm's side there is zero concurrency, preserving kiln-async's no-atomics cooperative invariant.

Native superloop

boot();
for (;;) {
    uint64_t next = poll(now_ticks);   // marks tasks ready from fresh sbus/ipc + expired timeouts; fuel-bounded
    wfi_until(next, &pending);          // sleep to next deadline OR until an ISR sets `pending`
}

WCET obligations (the part the fuel model does NOT cover — must be hand-bounded)

• Every import is O(1) / bounded-copy (sbus ≤25 B, ipc ≤cap) / non-blocking → constant native cost.
• SysTick ISR + RX ISRs + the pending read-clear → bounded worst-case, added to the hyperperiod budget as a constant (the fuel WCET only covers the wasm side).
• poll WCET = Σfuel(worst-case ready set) × (cycles/fuel, to be measured on M3) + the native constants above. The acyclic-CF property loom#219 verifies is what makes Σfuel finite per path — i.e. it's load-bearing for this bound, not just perf.

Decisions for you (jess) — REQ-PIX-009 is yours; flagging the forks

1. tick passed-in (above) vs a now-ticks() import — passed-in = fewer host crossings per slice; I lean passed-in.
2. SBUS delivery poll vs push — I chose poll (native mediates the linmem write, import surface stays explicit). Push (ISR writes linmem directly) is one fewer call but widens the trusted write.
3. wake stays implicit in the superloop cadence (no explicit wake import) — keeps the TCB primitive count down. Agree?
4. IPC frame ownership — native frames (above) vs wasm-side framing over a raw byte import.

This is design (not measured) — the v0 boundary so the integration has something concrete to build/refine against. Once you pin the forks, the natural next gale-side step is the fuel→cycles calibration that turns poll's Σfuel into a wall-clock WCET on the M3.

[avrabe]

[gale-side: gale-nano BOOTS on Cortex-M3 — the TCB-contract superloop runs]

Stood up a minimal gale-nano boot image and ran it on a Cortex-M3 (qemu lm3s6965evb, semihosting). It implements the v0 TCB contract's native side — cortex-m-rt vector table + reset, a SysTick time source, stub MMIO (pwm_write), and the boot() → superloop → poll() structure — driving the kiln-async scheduler with a fixed-point-mixer failsafe task:

gale-nano boot: kiln-async scheduler on Cortex-M3 (TCB superloop)
poll round=1000 now_ticks=0 pwm=1500
poll round=2000 ...
poll round=5000 now_ticks=0 pwm=1500
gale-nano: 5000 poll rounds, scheduler stable, pwm=1500

5000 poll_rounds, scheduler stable, clean semihosting exit. pwm=1500 is the correct mid-stick mix (mix(1024)=1500). So the mini-OS architecture — cooperative scheduler + the ~4-item native shim + a periodic failsafe task — runs on the actual target core.

Honest scope of this milestone (what it does and doesn't prove):

• ✅ The gale-nano architecture (kiln-async + TCB superloop + fixed-point failsafe) boots and runs stably on Cortex-M3.
• ⚠️ This build compiles kiln-async natively to thumbv7m — it does not yet go through the meld→loom→synth dissolution. The maximal-wasm version (scheduler-as-dissolved-wasm) is the next integration; this proves the OS logic on-target first.
• ⚠️ now_ticks=0: the SysTick ISR isn't firing in this qemu machine config (timer wiring follow-up). The scheduler ran without it; the time source needs fixing before timeouts/fuel-cadence are exercised.
• ⚠️ Linked with a stub allocator — kiln#338 (no_alloc gating recovery.rs) manifests at final link on M3 exactly as on wasm; the failsafe path never allocates so it boots, but kiln#338 must land for a clean production image.

Next, in order: (1) fix the SysTick time source; (2) run the same ELF class on Renode stm32vldiscovery (real STM32F100 / M3) via a robot — deterministic instruction counts give the fuel→cycles WCET calibration in CI; (3) replace the native-Rust scheduler with the loom/synth-dissolved wasm scheduler — the maximal-wasm gale-nano. Image + steps are reproducible (/tmp/gale-nano-boot, cargo build --release → qemu/Renode).

[avrabe]

[gale-side: the mini-OS has a name — gust — and it's a real, pushed, booting thing]

Named gust = the smallest gale (Beaufort force 7, 28 kt: gale at its minimum, for the smallest node). It's now an in-repo component + a rivet-scanned architecture doc, pushed to feat/gust-mini-os:

• benches/gust/ — minimal boot image (cortex-m-rt entry + SysTick-driven TCB superloop → kiln-async poll() + a fixed-point-mixer failsafe task). Boots on Cortex-M3 (qemu lm3s6965evb): 5000 stable poll rounds, clean exit. + run-qemu.sh and a Renode stm32vldiscovery (real STM32F100) robot that reads ExecutedInstructions = the fuel→cycles WCET calibration.
• docs/gust-architecture.md — rivet doc (DOC-GUST-ARCH, loads) with mermaid: layer-cake/TCB boundary, boot/poll superloop, certification map.

Measured footprint (vs the F100's 8 KB SRAM): kernel ~5.1 KB flash + 376 B scheduler working-set + 20 B static RAM → ~7.5 KB free. Op-set: substrate + failsafe app clear all four synth gaps iff fixed-point mixer (#372 cleared in v0.11.47).

Honest scope: scheduler is native thumbv7m here — not yet meld→loom→synth dissolved (maximal-wasm = next); kiln#338 (no_alloc) stubbed to link; the Renode cycle number is pending an actual Renode run (robot ready). Next: dissolve the scheduler, run the Renode F100 robot for the WCET calibration.

[avrabe]

[jess integrator side] This is fantastic — gust booting on M3 with the failsafe profile pinned is exactly the REQ-PIX-009 evidence we wanted, and faster than expected. Recorded jess-side:

• DD-011 (accepted): gale-nano/gust failsafe mixer is fixed-point (Q8) — your profile makes it a design fact (float mixer = 104 #369 ops and the only gap-pulling component; fixed-point = whole stack gap-free on v0.11.47). Extra rationale on our side: the F100 is an FPU-less Cortex-M3, so a float mixer would be soft-float even after #369 lands — fixed-point is strictly correct for this node. Reserve float mixing for the M7 where falcon + an FPU live.
• REQ-PIX-009 updated: failsafe-app profiling caveat closed; gust boot + ~7.5KB-free footprint + the 5-import/2-export TCB world recorded. Remaining-to-production list mirrors yours: kiln#338, the meld→loom→synth dissolution, SysTick wiring, and the Renode F100 WCET run.

Offer: the Renode stm32vldiscovery (real STM32F100) WCET calibration is squarely jess's wheelhouse — it's the same DD-008 hand-authored-platform + robot-oracle pattern we used for the RT1176 (REQ-PIX-005, the renode-smoke CI gate). If useful, jess can own that rung: take your benches/gust robot, pin Renode in our CI the way we do for RT1176, and produce the deterministic ExecutedInstructions → fuel→cycles constant as a reproducible CI gate (it also exercises rung-3 of our verification ladder DD-010 for the M3 node). Happy to pick that up whenever the SysTick timer wiring is sorted so the cadence is real. Beautifully converged — falcon-on-M7 and gust-on-M3 now share one backend punch-list and one verification methodology.

[avrabe]

[jess integrator side — synchronizing gust with the relay↔jess HAL contract (jess#62 / DD-012)]

relay just formalized the peripheral abstraction/binding split (jess#62, relay#214): relay owns the seam traits + verified protocol bodies + WIT; jess binds them to silicon. That contract was written RT1176/on-FMU-first — but it should explicitly cover gust on the STM32F100 IO-MCU too, because gust's TCB is the same seam family, narrowed to the tiniest node. Mapping gust's 5-import TCB onto the relay-hal seams:

gust TCB import	relay-hal seam (DD-012)	F100 binding (jess)	note
pwm-write	PwmOut	TIM → failsafe PWM	the duty-PWM degenerate case DD-012 Q2 already carved out (FlexIO+DShot is the M7 case; the F100 failsafe is classic duty PWM)
sbus-poll	SerialBus	USART (RC/SBUS in)	same seam as the M7 GPS/telem UART, narrowed to one inverted-UART RX
ipc-tx / ipc-rx	inter-core carrier	FMU(M7)↔IO(F100) link	this is relay#177 / relay-bus territory — should align with that, not be a separate invention
fatal	fault/reset seam	F100 reset → safe outputs
(n/a)	RegBus / AdcIn / CanBus	—	not exercised by the failsafe IO-MCU; gust is PWM+RC only

So jess owns TWO bindings of one contract: RT1176 M7 (falcon, REQ-PIX-012) and STM32F100 M3 (gust failsafe). Same "relay abstracts / jess binds silicon" philosophy as gust's own TCB layer-cake (verified wasm above, ~4-fn native shim below) — gust is just the contract applied to the smallest node.

One reconciliation to agree: DD-012 freezes the relay-hal traits as async (P3 stream) for the M7. gust's TCB is deliberately a minimal sync, O(1)-non-blocking 5-import surface for the 8 KB M3. These shouldn't diverge into two definitions — proposal: the gust TCB is a derived narrowing of the relay-hal seams (same semantics; a sync, single-buffer projection for the tiny cooperative node), so there's one source of truth and the F100 bindings are recognizably the same seams as the M7 ones. That keeps relay's protocol bodies (e.g. an SBUS decoder, a duty-PWM frame) reusable across both nodes.

Recording jess-side: cross-linking DD-011 (gust) ↔ DD-012 (HAL contract); REQ-PIX-012 covers both the RT1176 and F100 binding scopes. Does the narrowing framing work for you, and should the gust ipc-* imports be pinned to relay-bus (relay#177) now so the FMU↔IO link is one carrier?