typed-wasm: Progressive Type Safety for WebAssembly Linear Memory

Abstract

WebAssembly linear memory is an untyped byte array shared across module boundaries. When independently compiled modules — potentially from different source languages — read and write the same memory regions, no existing type system covers the cross-module interface. We present typed-wasm, a type system that applies a 12-level progressive type safety framework, originally developed for database query languages, to Wasm linear memory. The system treats contiguous memory segments as typed region schemas and load/store operations as typed projections verified against those schemas at compile time. We formalise the system in Idris 2 using Quantitative Type Theory (QTT), providing proofs of bounds safety, aliasing freedom, effect purity, lifetime validity, linearity, cost boundedness, and epistemic freshness — all erased before code generation, yielding zero runtime overhead. Our principal contribution is multi-module schema agreement: a static verification that independently compiled Wasm modules agree on the layout, types, alignment, and invariants of shared memory regions — a property that no source-level type system, and no existing Wasm proposal, can express. We further extend the framework with two novel levels: tropical cost-tracking (Level 11), which proves that memory access patterns have bounded cost via a min-plus semiring, and epistemic safety (Level 12), which prevents modules from acting on stale knowledge of shared state.