Direction: give kiln a no_std interpreter mode for on-board embedded execution (hybrid with synth-AOT) — amends RFC #46

[avrabe]

Decision

Pursue a hybrid embedded story: keep meld + synth AOT→native ELF for the certified hot path, and make kiln's interpreter no_std-capable so it can run on-board (gale/gust), competing head-to-head with the safety-critical interpreter field (#413: NASA spacewasm, DLR-FT/wasm-interpreter) instead of ceding that niche.

This amends RFC #46, which currently states "there is no no_std interpreter" and routes all embedded execution through synth-AOT. RFC #46's build-time component lowering (meld) and AOT-for-perf (synth) stay — this adds an interpreter deployment target, it does not remove synth.

Why (from the #413 peer comparison)

• spacewasm (NASA) and DLR-FT interpret on-board — no AOT. DLR states explicitly they chose an interpreter because a compiler defies DO-178C/DO-332 design principles. A compiler (synth) in the embedded cert TCB is a materially harder cert story than an interpreter; the incumbents avoided it deliberately.
• kiln already has the ingredients. Capability-bounded memory + per-instruction fuel are exactly what a cert-friendly on-board interpreter needs. kiln-runtime is already categorized no-std with a std feature and a (currently no-op) no_std stub — the no_std gate is a choice, not a limitation.
• Live migration gap. DLR-FT can serialize + move a running instance → maps onto gale/gust checkpoint-restart/failover. Native AOT code can't migrate easily; an interpreter can.

Feasibility (measured)

kiln-runtime std-dependence is moderate and localized:

• Sync primitives (~90 Mutex/RwLock/thread hits) → port to kiln-sync no_std equivalents. Main blocker.
• Collections (~55 std:: hits, few std::collections) → alloc (BTreeMap etc.).
• I/O (only ~5 std::fs/std::io hits) → platform callbacks (the existing kiln-builtins pattern).

Not a rewrite; a focused port centered on sync + collections. Target shape: DLR-FT's "in-place, almost no external deps."

Phasing (proposed)

1. Feasibility spike — run a minimal core module through the interpreter under no_std + alloc on thumbv7em; measure binary size + that fuel/bounded-memory still hold. Go/no-go gate.
2. Sync + collections port — kiln-sync abstractions; alloc collections behind the std feature boundary.
3. Platform-callback I/O — WASI/host imports via the kiln-builtins callback surface on embedded.
4. Live migration — execution-state serialize/restore (DLR-FT parity; gale/gust checkpoint). Can be its own track.
5. Cert-evidence parity — the no_std interpreter carries the same Verus/Lean/witness-MC-DC/sigil evidence (kiln's differentiator vs the peers).

Cross-repo

Amends RFC #46 (doc update + BA sign-off), and touches positioning for meld/synth (interpreter is no longer only std/reference) and gale/gust (new on-board deployment target + migration). Loop those in before committing beyond the Phase-1 spike.

Tracked in kiln rivet as a design-decision + REQ_NOSTD_INTERP. Relates to #283 (positioning vs Wasmtime TCB), #413 (peer comparison), #401/SR-35 (verified oracle).

[avrabe]

Refinement — deploy kiln AS a wasm module via synth; on-board Component Model as the unique angle

Two sharpening insights (captured in AD-NOSTD-INTERP-001 + REQ_NOSTD_INTERP, PR #416):

1. Deployment mechanism: kiln-as-wasm → synth → native.
Rather than a separate no_std-Rust→native cross-compile, kiln itself (no_std/no_alloc) is compiled to a wasm module, and synth AOT-compiles that to native for gale/gust — the same pipeline as user code. Consequences:

• wasm is the universal IR; synth is the single compiler in the TCB. No second toolchain.
• kiln-as-wasm is itself attestable — witness MC/DC on the kiln wasm, scry invariants, sigil — exactly like any payload it will later run.
• The synth-compiled kiln then loads and interprets wasm on-board.

2. The unique differentiator: Component Model on-board.
kiln already does direct runtime component hosting (AD-COMPONENT-HOST-001; the #344/#364/#405 work), today scoped QM/std-reference only with embedded staying meld-dissolve. This direction extends direct hosting to the embedded target, so on-board kiln can run the full Component Model (or plain core wasm) where AOT of the payload isn't wanted — spacewasm and DLR-FT are core-module-only. That's the "compete as something unique."

3. Gale (OS) requirement (cross-repo).
gale must (a) load + run the synth-compiled kiln image, and (b) support runtime wasm loading on-target (dynamic module/component load). Needs a gale-side requirement before Phase 3.

Open questions the Phase-1 spike must settle: does synth accept/correctly AOT a module as large as the kiln interpreter; interpreter-in-wasm-AOT'd-to-native perf (vs a direct no_std-Rust build and vs the peers); bootstrapping/toolchain-trust. Fallback if wasm→synth is impractical: a direct no_std-Rust build of kiln-runtime — the porting work is identical, only the final codegen path differs.

[avrabe]

gust/gale perspective (looping in per the cross-repo ask)

Strong +1 on the hybrid, with one important framing correction and the on-board numbers you'll want for the go/no-go.

gust is NOT "a compiler in the embedded cert TCB" — that's the on-board-JIT foil, not us

The #413 DLR argument ("a compiler defies DO-178C/DO-332 design principles") is decisive against an on-board JIT, but gust/synth-AOT sits at a different, cert-favorable point: synth runs at BUILD time; the device ships a pure native ELF with no compiler and no interpreter on it. The on-device TCB is the dissolved code + a ~3-atom bridge (read32/write32), and the trust is in the build-time chain (synth's Rocq/ordeal-certified lowering + the component's own Kani/Verus proofs), verified off-target. So the design space is really three points, not two:

1. on-board JIT (wasmtime) — compiler in the flight TCB. The foil.
2. on-board interpreter (spacewasm/DLR-FT/kiln no_std) — interpreter in the flight TCB; migratable, introspectable.
3. build-time dissolve (gust: meld→loom→synth→native) — nothing dynamic in the flight TCB; smallest/fastest; but can't migrate or introspect a running instance.

The hybrid you're proposing = 2 + 3 behind one WIT contract, which is exactly right.

The gust:os WIT seam already makes it per-tenant

gust tenants import a single capability world (gust:os {time, log, spawn, channel, io}; gust:hal for drivers). Whether a tenant is dissolved (hot path, certified, tiny) or interpreted (dynamic/migratable) is an implementation choice under the same contract — the app is byte-identical either way. So the hybrid doesn't fork the programming model; it's a deployment axis.

Measured AOT baseline for the #413 matrix (the "point 3" column)

From gale benches/gust (qemu -icount + on-silicon DWT), current numbers:

• Dissolved vs native LLVM: gust_mix 1.50× (shipped pin), 1.375× with proof-carrying clamp-elision (synth 0.40.0 SYNTH_FACT_SPEC, ordeal-LRAT-certified), floor 0.45×. So AOT is ~parity-to-sub-native on the hot path.
• SRAM: scalar thin-seam drivers 0 SRAM; the first buffer-carrying OS node (time+log, list<u8>) dissolves to ~5.5 KB total, fits the STM32F100 8 KiB budget.
• Flight TCB: native .text + a 2–3 fn bridge; no runtime, no allocator for the scalar path.

That's the "no interpreter at all" extreme to put beside spacewasm/DLR-FT/kiln-interpreter — and it sets the bar the no_std interpreter has to justify against on size + cycles.

What gust actually WANTS from the interpreter (the real motivation)

The migration/introspection gap is exactly gust's — dissolved native can't checkpoint/serialize a running instance, and the gust-OS north star includes multi-tenant + failover. So gust wants the hybrid precisely for the migratable / dynamically-loaded tenant case (a tenant you didn't dissolve at build time, or one you want to move on fault). Certified hot path = dissolved; dynamic/migratable tenants = interpreted.

The go/no-go number that matters for gust specifically

Phase-1 targets thumbv7em — but gust's tightest part is the F100 = 8 KiB SRAM / thumbv7m. The gating question isn't "does it run" but "what's the interpreter's code + RAM footprint, and does a useful tenant + interpreter co-fit an 8 KiB / small-flash part?" If the interpreter alone dwarfs the 5.5 KB a dissolved OS node needs, the interpreted path is a bigger-part deployment (M4/M7, more RAM) while F100-class stays dissolve-only — which is a fine and honest split, but worth pinning in the Phase-1 gate. Happy to wire the gust bench harness (SysTick -icount + DWT) so the interpreter lands in the same size/cycle/SRAM table as the dissolved baseline — that gives you the competitive matrix and gale the deployment-fit answer in one shot.

Tagging for the RFC #46 amendment. If you cut REQ_NOSTD_INTERP, link it against gust's REQ-OS-* so the hybrid is one traced story.