Comparison targets: benchmark + differentially validate kiln against the safety-critical Rust interpreter field (NASA spacewasm, DLR-FT/wasm-interpreter), not only wasmtime

[avrabe]

Why

Our differential/perf comparisons currently use wasmtime (a server-grade JIT — the "unverified TCB" foil of #283). But kiln's true peers are the safety-critical Rust interpreters, and those are the engines we should compare against and outcompete:

• NASA spacewasm — https://github.com/nasa/spacewasm — "A flight-compliant WebAssembly interpreter." Ground-up Rust interpreter meant to run Wasm on-board spacecraft; design levied from flight-software standards; deterministic dynamic-memory model, streaming to minimise peak memory, CoreMark benchmarks, libfuzzer. Draws on wasmi, wasm3, and DLR-FT.
• DLR-FT/wasm-interpreter — https://github.com/DLR-FT/wasm-interpreter — minimal in-place Rust interpreter from DLR Institute of Flight Systems for avionics (ED-12C/DO-178C, ED-217/DO-332). Passes the full WebAssembly testsuite (minus unfinished proposals); fuel halt/refill/resume (mirrors kiln's resumable-fuel model); live instance migration. Paper: "On the Design of a WebAssembly Interpreter for Aviation" (DASC 2025). NASA's spacewasm requirements are levied from this work.

Same niche as kiln — no_std-friendly, Rust, fuel-bounded, deterministic, cert-oriented.

Two workstreams

1. Differential correctness (extends #401 / SR-35).
Use spacewasm + DLR-FT as additional differential oracles alongside wasmtime. Both are Rust and embeddable (far cheaper to wire than WasmRef-Isabelle), and being peer safety-critical engines, agreement/disagreement is high-signal. Cross-check the WAST suite + fuzz-generated modules across {kiln, wasmtime, spacewasm, DLR-FT}; a kiln-only disagreement is a bug, an all-interpreters-disagree-with-wasmtime is a JIT/spec-interpretation delta worth a note.

2. Competitive matrix (extends #283 positioning + REQ_ASYNC_BENCH methodology).
Measure kiln vs the field on:

• Conformance — WAST pass rate (kiln's mechanical oracle already; publish the head-to-head).
• Performance — CoreMark-style + the per-poll/micro methodology from the executor-comparison bench.
• Memory — peak + determinism (bounded/no-alloc footprint).
• Resumability/fuel — determinism + migration.
• Verification evidence (kiln's intended lead) — Verus + Lean/Aeneas proofs, witness MC/DC on the real Wasm, sigil attestation, rivet end-to-end traceability. spacewasm/DLR are cert-designed but not proof-carrying / MC/DC-attested to this stack level.

"Outcompete" = lead decisively on the verification-evidence axis while matching or beating on conformance + determinism.

Tracking

Landed in rivet as a roadmap requirement, linked to SR-35 (#401), #283, and REQ_ASYNC_BENCH. Research/benchmark-infrastructure direction, not a defect.

[avrabe]

Offer from gale/gust: the "no interpreter — build-time dissolve" column

For the competitive matrix (#415 point 3), gust is the extreme datapoint beyond spacewasm/DLR-FT/kiln-interpreter: the same Wasm/component, dissolved to native ELF at build time (meld→loom→synth), nothing dynamic in the flight TCB. It's the natural upper bound on the size/cycle/memory axes and the natural lower bound on introspection/migration — so it frames what the interpreter is trading away.

Measured (gale benches/gust, qemu -icount + on-silicon DWT):

axis	gust dissolved-AOT
Performance	gust_mix 1.50× native LLVM (pin), 1.375× proof-carrying (ordeal-LRAT clamp elision), 0.45× floor
Memory	scalar drivers 0 SRAM; buffer-carrying OS node ~5.5 KB / 8 KiB F100
Conformance	N/A at runtime — correctness is the build-time proof chain (Rocq/ordeal-certified lowering + component Kani/Verus), not a WAST pass rate on-device
Resumability/migration	none (native, no serializable instance) — this is the interpreter's win column
Verification evidence	component-level Kani/Verus + synth's Rocq/LRAT lowering proofs + rivet trace + sigil

Concretely useful for this issue: gale already runs the SysTick -icount + DWT harness that produces those numbers. If kiln's no_std interpreter lands (#415 Phase-1 on thumbv7em), I'll wire it into the same harness so {kiln-interp, dissolved-AOT} land in one size/cycle/SRAM table on identical cores — and, if you want, add spacewasm/DLR-FT as the external interpreter columns. That gives you the head-to-head + gale the deployment-fit answer (interpreter footprint vs the 5.5 KB dissolved node) in one place. The verification-evidence axis is where kiln + gust jointly lead the field; worth stating the two TCB shapes (verified-interpreter-on-device vs verified-toolchain-at-build) side by side rather than as competitors.