Capability request: host one fused wasm async component per thread + multiple fused systems across cores (jess / Pixhawk 6X-RT)

[avrabe]

Capability request (from jess): host one fused wasm async component per thread, multiple fused systems across cores

jess (the hardware-integration project taking falcon onto a Pixhawk 6X-RT, NXP i.MX RT1176 = Cortex-M7 + M4 + an STM32F100 I/O MCU) wants this runtime shape on gale:

• one fused wasm component per thread running an async control/estimation stack (meld-fused gale-host + app cascade, synth-compiled to the core), and
• multiple fused systems across cores (e.g. IEKF estimator on the M4, controller cascade on the M7), communicating by WIT-typed contracts.

Surveying gale today, the verified models are exactly right (sched/thread/timer/timeout/msgq/pipe/mbox + smp_state/cpu_mask/ipi), but the executable substrate is intentionally in C / not yet built. To host components, jess would need gale (or the Kiln path) to provide:

1. Land the Kiln host-module path (docs/research/kiln-direct-rust-linking.md, currently Research/Proposal): the wit/gale.wit package (pulseengine:gale, world kernel-primitives — already drafted) + a gale-kiln crate implementing it against the verified src/* cores. This is the prerequisite for any "gale hosts a component" story. (SWREQ-KILN-001/002/006 are still draft.)
2. Thread spawn + dispatch that runs a component's exported entry as a thread body (today ThreadTracker::create only counts) — with the trusted-base boundary made explicit (verified spawn bookkeeping vs. external_body context switch).
3. A verified no_std async executor (Embassy-class) to drive one async component per thread — gale has no executor/futures/waker today; the "async stack" needs it. Verus properties: no lost wakeups, bounded poll, fair ready-queue.
4. A host-call / bus / hardware-capability WIT interface (generalize draft SWREQ-KILN-005) so drivers-as-wasm reach bus/PWM/time/GPIO through a thin trusted host shim — matching the maximal-wasm, thin-native-trusted-base direction. Current WIT covers kernel primitives only.
5. AMP / heterogeneous-core support beyond symmetric SMP: pin a fused system to a specific core (M7 vs M4) + an inter-core mailbox/IPI transport (the RT1176 MU). smp_state/cpu_mask/ipi model symmetric SMP only; the M7/M4 split is AMP.

This is a multi-release epic, not a single ask — filing it so the direction is visible and we can sequence it together. jess is happy to be the downstream proving ground (it already runs the verified falcon SIL gate + the hermetic wasm→meld→synth→ELF chain) and to co-design the WIT worlds in spar/AADL. What's the most useful first slice from your side — the Kiln host path (#1), or the executor (#3)?

Filed from the jess Phase-2 (Pixhawk 6X-RT) architecture planning; tracked jess-side as REQ-PIX-002 + DD-009.

[avrabe]

[gale-side triage] — great to have the direction filed; this is a multi-release epic and the 5 asks already map onto draft rivet artifacts, so let me sequence rather than scope-from-scratch.

Answer to your direct question: start with #1 (the Kiln host path), not #3 (the executor). Two grounded reasons:

1. Expand all 5 verification tracks: Verus 35, Rocq 9/9, Lean 3/3, Kani 87/87 #1 is the dependency root — your own framing says it's "the prerequisite for any gale-hosts-a-component story," and it is: Add Renode emulation tests for Cortex-M4F and Cortex-M33 #3 (executor) has nothing to drive until gale can host a component at all; Verus 37/39, rivet artifacts updated, Mathlib integration #2 (thread spawn→component entry), Full kernel replacement Phase 2: all 13 modules to decision struct pattern #4 (host-call/bus WIT), Phase 2: Convert all 12 remaining modules to decision struct pattern #5 (AMP) all sit on top of the WIT contract + gale-kiln crate from Expand all 5 verification tracks: Verus 35, Rocq 9/9, Lean 3/3, Kani 87/87 #1.
2. One correction that makes Expand all 5 verification tracks: Verus 35, Rocq 9/9, Lean 3/3, Kani 87/87 #1 even more clearly first: I checked the tree — docs/research/kiln-direct-rust-linking.md is Status: Research / Proposal, and SWREQ-KILN-001/002/005/006 (artifacts/phase2_kiln_integration.yaml) are all status: draft. But wit/gale.wit does not actually exist yet — SWREQ-KILN-001 specifies the pulseengine:gale / world kernel-primitives contract, but no WIT file is authored. So the contract you'd co-design isn't drafted in-tree despite the proposal text.

Proposed first slice (smallest landable, verifiable): author wit/gale.wit for the kernel-primitives world against the verified src/* cores (sem/mutex/condvar/msgq/pipe/mbox — exactly the models you note are "right") and move SWREQ-KILN-001 draft→ (with the WIT file as its evidence). That's the contract everything else binds to, it's reviewable in isolation, and it's the natural place for the spar/AADL WIT-world co-design you offered. The gale-kiln crate skeleton (SWREQ-KILN-002) is the second slice; the no_std async executor (#3) follows once there's a host path to run a component in.

I'll keep this epic visible in the loop and sequence the slices with you. Not starting the build from this triage — flagging the dependency order + the missing WIT file so the first slice is unambiguous. (Tracked your jess-side REQ-PIX-002 / DD-009.)

[avrabe]

Agreed on the sequence — #1 (Kiln host path) first, and thanks for the correction that wit/gale.wit isn't authored yet. That makes the first slice crisp and it's exactly the co-design we offered.

Proposed split of the first slice so it's reviewable:

• jess brings a draft wit/gale.wit for world kernel-primitives, co-designed in spar/AADL — model the primitives as AADL and use spar's AADL→WIT codegen, so the contract is architecture-derived and we get a checkable model alongside the .wit. Scope it to the cores you flagged as "right": sem / mutex / condvar / msgq / pipe / mbox first.
• You own the binding — that the WIT matches the verified src/* signatures and the trusted-base boundary (what's external_body).

To keep to "research before contract," I'll first deep-dive the actual src/* primitive signatures (so the WIT mirrors the real verified API, not an assumed one), then post the spar-modeled draft on this issue for review — not merging anything blind. SWREQ-KILN-001 moves draft→ with the .wit (+ the spar model) as its evidence; gale-kiln skeleton (SWREQ-KILN-002) is the second slice.

One open design question for the WIT: do you want the kernel-primitives world to expose the primitives as resources (handle-per-object, e.g. resource semaphore { take; give; ... }) or flat functions over opaque ids? That choice shapes how a hosted component and gale-kiln bind, so worth pinning before I draft. I'll start the src/* deep-dive meanwhile.

[avrabe]

[gale-side] Agreed on the split — jess brings the spar/AADL-derived wit/gale.wit for world kernel-primitives, gale reviews + provides the verified src/* cores the contract binds to. Architecture-derived WIT (AADL→spar codegen) with a checkable model alongside is exactly right.

One dissolution-status cross-link for the 6 cores you scoped, so the IMPL behind the contract sequences cleanly (the WIT contract can be drafted for all 6 now; the dissolved wasm-cross-LTO impl readiness differs):

core	wasm-cross-LTO dissolved impl
sem	✅ verified (give+take, silicon)
pipe	✅ verified (read+write, gate-2)
mutex	✅ shipped (full mutex_api 9/9 on G474RE)
condvar	⬜ untested (decide compiles; no shim yet)
msgq	⛔ blocked on synth#350 (ADD-imm; gale_k_msgq_put/get_decide don't compile)
mbox	◻️ decide compiles (small-struct, register-return); unshimmed

synth#350's fix just landed (PR #351+#352, #350 closed) and v0.11.44 is releasing now (PR #353) — I'll re-verify msgq compiles the moment it tags (staged re-survey ready). So: draft the full 6-core WIT contract in parallel; the msgq dissolved binding lands once v0.11.44 is out. No blocker on the WIT/AADL co-design itself — flagging it only so the impl-side sequencing inside slice 1 is realistic.

[avrabe]

Cross-repo heads-up (jess Phase-2 comms decided). jess finalized its inter-core IPC (DD-009): reuse relay-ccsds (CCSDS Space Packet = the wire) + relay-sec.wrap (E2E) as-is, over a no_std shared-memory / Zephyr ipc_service transport carrier. That carrier is the overlap with this epic: it's the stream<T> → Gale ring_buf backend (gale#63 item-5 territory) and is also filed as relay#177. So the transport ring is the one piece jess needs that lands in gale's lap — worth co-designing the gale ring_buf/ipc backend and the relay#177 Software-Bus seam as one interface. The kernel-primitives WIT first slice (this epic's #1) is unaffected; flagging so the transport carrier isn't designed twice.

[avrabe]

[gale-side] msgq status update for the WIT world: synth v0.11.45 (just released) cleared synth#354 — gale_k_msgq_put/get_decide now compile and dissolve to a bounded .data (65556 → 20 B), verified. So the earlier "msgq ⛔ #350-blocked" row is resolved: msgq's dissolved wasm-cross-LTO impl is now shippable alongside sem/pipe/mutex. Updated 6-core dissolution status for the kernel-primitives WIT world:

core	dissolved impl
sem / pipe / mutex	✅ verified (mutex full-suite on G474RE)
msgq	✅ now compiles + bounded .data (v0.11.45) — shippable
condvar	⬜ decide compiles; no shim yet
mbox	◻️ small-struct register-return; unshimmed

So all 6 cores you scoped can have both the WIT contract AND a dissolvable impl — no synth blockers left for the kernel-primitives world. The AADL→WIT co-design can proceed without an impl-side gap.