Phase 3: Runtime-side enforcement

[hyperpolymath]

Tracking issue for Phase 3 of the production path. See docs/PRODUCTION-PATH.adoc §Phase 3.

Theme

Today the 10 levels are compile-time guarantees against the verifier. Once wasm runs on Wasmtime/Wasmer/V8, those runtimes know nothing about regions. Levels 7-10 (aliasing, effects, lifetimes, linearity) only hold if the producer was honest. Phase 3 is the difference between linting and memory safety.

Options (load-bearing decision)

Pick one (or hybrid) before starting Phase 3 work:

1. Wasmtime extension — host functions for region operations; runtime tracks region metadata. Fork the runtime; smallest blast radius. (Recommended)
2. Wasmer plugin — more flexible plugin model; smaller adoption.
3. Compile to native via typed-wasm-aware lowering — Rust/Zig backend consuming typed-wasm. Loses portability; gains enforcement.
4. Custom wasm proposal to the CG — multi-year standardization. Needs Mozilla/Google/Apple/Microsoft champion. Not realistic for solo/small team.

Deliverables (assuming option 1)

• Wasmtime fork with region-tracking host functions
• Runtime metadata: region maps, ownership tracking, lifetime markers per allocation
• Demonstration: an L7+ violation that the producer lied about, detected at runtime by the forked runtime
• Long-term goal: upstream the interface (let runtimes register region-tracking hooks) rather than the specific levels — gives a standardization story
• Performance characterisation: overhead of runtime tracking vs. plain wasm

Gate to Phase 4

At least one runtime demonstrates runtime detection of an L7+ violation that the verifier missed because the producer lied.

Depends on

• Phase 2 complete — issue Phase 2: Multi-producer adoption #50
• Decision D2 from docs/PRODUCTION-PATH.adoc §"Load-bearing decisions" — producer-side-only vs. runtime-aware

Status when this issue closes

typed-wasm becomes one of a small set of memory-safe wasm-class platforms with both producer- and runtime-side enforcement. Peer set: CHERI/Morello+wasm (hardware-level), wasmGC (managed-types). typed-wasm's distinguishing claim is the machine-checked end-to-end proof of soundness (Idris2) — unique in this set.

Next phase

• Phase 4 — Tooling + developer experience: issue Phase 4: Tooling + developer experience #52