The same code that runs on wasmtime and dissolves to a Cortex-M3 (no runtime), here live in a browser wasm engine. Formally-verified gale components (Verus/Rocq/Lean/Kani) + the kiln-async scheduler that boots gust, the engine_control algorithm, and the meld-fused Component-Model composition that dissolves to a 668 B native object. Same code, three runtimes: browser · wasmtime/kiln · dissolved-native. booting…
The composed component (gale-app-demo imports gale:kernel; gale-kiln provides it over the verified gale::* deciders) meld-fused into one merged-memory core. This exact module runs here in the browser, runs on wasmtime, and synth-dissolves to a 668 B Cortex-M3 object (fused.o) that boots bare-metal — all returning the identical packed result.
The realistic control step from benches/engine_control (ignition/fuel table lookups + integer coolant enrichment + knock retard) — the same maps as the C bench and the WIT component. Verified byte-identical here to control.step on wasmtime. Dissolves to a 378 B Cortex-M3 .text.
These call gale's proven decision functions directly (gale::sem::give_decide, gale::msgq::put_decide, …). The browser is just the “apply” shell; the decision is the machine-checked component — exactly what runs on the MCU.
gale::sem) — count limit 3gale::msgq) — ring depth 4gale::mutex) — ownership + reentrancygale::event) — bitmask post / waitThe cooperative fuel-bounded scheduler that boots gust on Cortex-M3 and dissolves to native via wasm→loom→synth. Driving one failsafe task (fixed-point mixer). Not a verified gale primitive — it's the executor leg of the OS.
The leg you can't run natively in a browser: the same wasm above, lowered straight to a Cortex-M .text by synth — no interpreter, no runtime. Sizes vs the LLVM-native build of the same source. The synth codegen gap (vs LLVM) is the optimization surface being driven down (synth#390 / loom#226).
| function | native (LLVM) | dissolved (synth) | ratio |
|---|---|---|---|
gust_poll (scheduler hot path) | 208 B | 816 B | 3.9× |
gust_mix (Q8 failsafe mixer) | 12 B | 44 B | 3.7× |
control_step (engine_control) | 180 B | 378 B | 2.1× |
run-demo (fused CM composition) | — | 668 B | one image, no runtime |
whole dissolved gust kernel .text | — | 1402 B | the entire kernel |
vs a wasm interpreter on the MCU (WAMR): ~50–64 KB of engine + per-module RAM + 10–50× interpreter energy. Dissolving removes all of it.
404 / blank? wasm needs HTTP — cd web && python3 -m http.server, open http://localhost:8000/.