typed-wasm

Progressive type safety for WebAssembly linear memory — checked L1-L10 core, 0 believe_me in the checked proof package.

Table of Contents

• 1. The Idea
• 2. The Checked Core: 10 Levels
• 3. The Killer Feature: Multi-Module Type Safety
• 4. Architecture
• 5. Quick Tour
• 6. Status
• 7. Related Projects
• 8. GraalVM Implications
• 9. License
• 10. Author

1. The Idea

WebAssembly’s linear memory is an untyped byte array. Programs access it with load/store instructions at byte offsets — structurally identical to a schemaless database where programs issue untyped queries.

TypedQLiser solved this for databases: layer compile-time type safety over existing query languages so that every query is verified against the schema before execution.

typed-wasm applies the same principle to WASM memory. Regions are tables. Loads are SELECT queries. Stores are UPDATE statements. Schemas are the type system. The Idris2 prover verifies safety at compile time. The output is bare WASM instructions with zero overhead.

2. The Checked Core: 10 Levels

Level	Database (TypedQL)	WASM (typed-wasm)
1	Parse-time safety	Instruction validity
2	Schema-binding	Region + field resolution
3	Type compatibility	Load/store type matching
4	Null safety	Nullable pointer tracking
5	Injection-proof	Bounds-proof (compile-time)
6	Result-type	Access return type known
7	Cardinality	Aliasing safety
8	Effect-tracking	Read/Write/Alloc/Free
9	Temporal safety	Lifetime safety (no UAF)
10	Linearity	Linear resource usage

L11-L12 research files exist in the repository, but they are not part of the default checked Idris2 package and are not currently claimed as integrated or machine-checked proof surface.

3. The Killer Feature: Multi-Module Type Safety

When Module A (compiled from Rust) shares memory with Module B (compiled from ReScript), neither source-level type system can verify the boundary.

Rust’s borrow checker types memory within Rust. ReScript’s type system types values within ReScript. If Rust writes a struct at offset 0 and ReScript reads from offset 0 assuming a different layout, you get silent corruption.

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.

// Module A (from Rust) — declares and exports
region Entity[1024] {
    pos_x: f32;
    pos_y: f32;
    hp:    i32;
}
export region Entity;

// Module B (from ReScript) — imports and uses
import region Entity from "physics" {
    pos_x: f32;
    pos_y: f32;
    hp:    i32;
}

fn read_hp(entities: &region<Entity>, idx: i32) -> i32
    effects { ReadRegion(Entity) }
{
    region.get $entities[idx] .hp -> hp;
    return hp;
}

typed-wasm verifies that Module B’s imported fields match Module A’s export in name, type, offset, and alignment.

4. Architecture

Layer	Technology	Role
ABI	Idris2	Dependent types proving region schemas correct
FFI	Zig	C-ABI compatible memory operations
Parser	ReScript (planned)	Parse .twasm syntax to AST
Proofs	Idris2 totality checker	Verify the checked L5-L10 core at compile time
Codegen	Zig → WASM	Emit raw WASM instructions from typed access
Testing	ECHIDNA	Property-based fuzzing of proof soundness

5. Quick Tour

spec/grammar.ebnf              # The grammar — core intellectual artifact
spec/10-levels-for-wasm.adoc    # Checked L1-L10 mapping from DB to WASM
src/abi/*.idr                   # Idris2 formal proofs
ffi/zig/src/main.zig            # Zig C-ABI implementation
examples/01-single-module.twasm # Basic typed regions
examples/02-multi-module.twasm  # THE killer feature demo
examples/03-ownership-linearity.twasm  # Levels 7-10
examples/04-ecs-game.twasm      # ECS as a columnar database
LEVEL-STATUS.md                 # Current claim envelope and audit status
docs/WHITEPAPER.md              # Full academic treatment

6. Status

Pre-alpha / Research. The checked L1-L10 ABI core, Zig FFI, parser tests, and smoke tests are in place. L11-L12 files are experimental drafts: they are not part of the default proof package and are not yet claimable as integrated proofs. The next step is to de-template the release path, expand end-to-end and aspect coverage, and either complete or withdraw the higher-level claims.

7. Related Projects

• TypeLL — Type theory foundation

• TypedQLiser — 10-level safety for query languages

• VQL-UT — 10-level safety for VeriSimDB

• ECHIDNA — Property-based prover testing

8. GraalVM Implications

GraalVM’s Truffle framework has the same multi-language shared state problem. typed-wasm’s approach could give GraalVM compile-time guarantees for cross-language interop, replacing runtime InteropLibrary dispatch with compile-time schema agreement. See docs/WHITEPAPER.md for details.

9. License

PMPL-1.0-or-later

10. Author

Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>