The README makes claims. This file backs them up with evidence from real code.
From README:
Progressive type safety for WebAssembly linear memory — checked L1-L10 core, 0 believe_me in the checked proof package. L11 (tropical cost-tracking) and L12 (epistemic safety) are formally specified and published.
-blue){kind=icon}
Evidence: /var/mnt/eclipse/repos/typed-wasm/src/abi/Levels.idr defines Idris2 dependent types for all 10 checked levels: L1 (instruction validity), L2 (region binding), L3 (type compatibility), …, L10 (linearity). src/abi/TypedWasm/ABI/Proofs.idr contains zero believe_me, assert_total, or escape hatches. LEVEL-STATUS.md confirms "checked L1-L10 core."
L11 and L12 are formally specified in src/abi/TypedWasm/ABI/Tropical.idr (L11: AllPairsCosts + Level11KleeneProof) and src/abi/TypedWasm/ABI/Epistemic.idr (L12: Level12Proof + freshness witnesses). The full 12-level type hierarchy is given by the fullCert12 top-level certificate type in Proofs.idr.
Published: Zenodo 10.5281/zenodo.19535653 — "typed-wasm: Progressive Type Safety for WebAssembly Linear Memory" (v1.1.0-paper, 2026-04-12).
Caveat: L11-L12 type-check in Idris2 but are NOT integrated into the default checked build. The fullCert12 certificate exists as a type; producing concrete witnesses for arbitrary programs requires additional toolchain work. Claims cite the paper; do not assert machine-checked L11-L12 coverage.
From README:
When Module A (compiled from Rust) shares memory with Module B (compiled from AffineScript), neither source-level type system can verify the boundary.
typed-wasm declares the shared schema once. Both modules import it. The typed-wasm checker verifies structural agreement at compile time, before any module runs.
Evidence: examples/02-multi-module.twasm demonstrates: Module A exports a region Entity with fields (pos_x, pos_y, hp); Module B imports the same region and defines typed load/store operations. src/abi/TypedWasm/ABI/Proofs.idr proves field offset and alignment agreement.
Caveat: Schema agreement proof is type-level (compile-time). Does NOT verify that actual Rust/AffineScript compiled code respects field layout — correspondence is manual. Runtime behavior depends on correct field packing across compilers.
Evidence: spec/type-safety-levels-for-wasm.adoc maps each level from database (TypedQL) to WASM. The Idris2 proofs live under src/abi/TypedWasm/ABI/: Region.idr + TypedAccess.idr define L1-L3 schema and access typing; Pointer.idr defines L4 nullability kinds; Levels.idr enumerates Level1_InstructionValidity through Level10_Linear as data types; Effects.idr covers L8; Lifetime.idr covers L9; Linear.idr covers L10; Proofs.idr carries the composed certificates.
Caveat: Proofs are about abstract WASM models, not actual WebAssembly instruction sequences. Translation from .twasm (typed-wasm surface syntax) to WASM bytecode is NOT mechanically verified.
Uses the hyperpolymath type safety stack (Idris2 + TypeLL + 12-level verification). Same pattern across:
-
TypedQLiser — 12 levels for database query languages (origin)
-
VCL-total — 12 levels for VeriSimDB
-
TypeLL — Type theory foundation (shared)
-
ECHIDNA — Property-based prover testing (integrated)
All share: Progressive safety levels, mechanized proofs in Idris2, no escape hatches in checked core.
| Path | Contents & Purpose |
|---|---|
|
The |
|
Mapping document: each of the 12 levels from TypedQL (database) → typed-wasm (WASM), with rationale and examples |
|
Schema type, field accessors ( |
|
Load/store typing: |
|
The canonical L1-L10 data types — |
|
L4 nullability + L7 aliasing kinds: |
|
Cross-language layout contracts (aggregate-library role): |
|
Cross-module sharing (the killer feature): |
|
L8 effect tracking: |
|
L9 lifetime tracking: |
|
L10 linearity: |
|
L11: tropical cost-tracking — AllPairsCosts + Level11KleeneProof (min-plus semiring, bounded memory access cost) |
|
L12: epistemic safety — Level12Proof + freshness witnesses (prevents stale-state reads across modules) |
|
Machine-checked proofs for L1-L10. |
|
Zig FFI implementation: runtime region management, typed load/store operations, C-ABI compatible interface |
|
Zig FFI integration tests: memory layout verification, cross-module region sharing |
|
Single-module typed-wasm program: region declaration, typed access |
|
THE killer feature demo: Module A exports region, Module B imports and uses with type safety across language boundary |
|
Advanced example: Levels 7-10 (aliasing, effect tracking, lifetime, linearity) |
|
Real-world example: Entity Component System as columnar database with typed-wasm regions |
|
L11 demo: particle system with bounded memory access cost via tropical semiring |
|
L12 demo: game server/renderer with freshness enforcement across module boundaries |
|
Preprint source: "typed-wasm: Progressive Type Safety for WebAssembly Linear Memory" (12-level) |
|
Current claim envelope: which levels are checked (L1-L10), which are published-but-not-integrated (L11-L12), audit status |
|
Full mapping of paper theorems to source locations, including Zero-Overhead Property, tropical semiring laws, epistemic freshness theorems |
Honest Assessment: Pre-alpha / Research. The checked L1-L10 ABI core and Zig FFI are in place. L11-L12 are formally specified and published (Zenodo 10.5281/zenodo.19535653). End-to-end codegen (.twasm → WASM bytecode) is NOT yet implemented.
What Works:
- L1-L10 proof core in Idris2 (zero unsound axioms)
- L11-L12 type specifications in Idris2 (fullCert12 certificate type)
- Zig FFI layer (C-compatible, tested)
- Multi-module schema agreement verification
- Published preprint with formal inference rules
What’s Missing:
- Parser for .twasm syntax (spec exists, implementation partial)
- Codegen: .twasm → WASM bytecode
- L11-L12 concrete witness generation (type hierarchy complete; toolchain integration pending)
- End-to-end examples (design only)
Open an issue or reach out at j.d.a.jewell@open.ac.uk — happy to explain the 12-level hierarchy, multi-module type safety, or proof structure.