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. Two Roles (ADR-004)
  • 1.1. Pipeline Position
• 2. The Idea
• 3. The Checked Core: 10 Levels
• 4. The Killer Feature: Multi-Module Type Safety
• 5. Architecture
• 6. Quick Tour
• 7. Status
• 8. Related Projects
• 9. GraalVM Implications
• 10. License
• 11. Author

1. Two Roles (ADR-004)

typed-wasm has two first-class purposes that share the same Idris2 ABI infrastructure:

1. TypeLL type safety for WasmGC linear memory — the primary research project. WASM linear memory is a schemaless database; typed-wasm adds schemas (regions) and type-safe access operations, verified through a progression of type properties. Proofs live in TypedWasm/ABI/ (the checked L1-L10 core).

2. Aggregate library — the convergence infrastructure for languages that compile to typed WasmGC. AffineScript and Ephapax are independent languages that both target WasmGC; they need agreed binary conventions (type layout, ABI, stdlib types, linking). The Idris2 ABI infrastructure that typed-wasm already uses for role 1 is exactly the right tool for formally verifying the cross-language layout contracts. These proofs live in src/abi/layout/.

The two roles are documented separately: * TypedWasm/ABI/ — TypeLL level proofs (primary role) * src/abi/layout/ — cross-language layout contracts (aggregate library role) * docs/architecture/AGGREGATE-LIBRARY-VISION.adoc — human-readable design doc for role 2

1.1. Pipeline Position

katagoria  →  typell  →  typed-wasm  →  PanLL
(research)   (kernel)     (target)    (eNSAID env)

typed-wasm sits downstream of the TypeLL verification kernel. Type theory ideas originate in katagoria (research), are promoted to typell (the open-ended progressive verification kernel), and are applied here to WASM memory and to the cross-language binary conventions for AffineScript and Ephapax.

2. 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.

3. 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.

4. 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.

5. 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

6. 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

7. 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.

8. Related Projects

• TypeLL — Type theory foundation (open-ended progressive kernel; typed-wasm is one application)

• TypedQLiser — Progressive type safety for query languages

• VCL-total — Progressive type safety for VeriSimDB

• ECHIDNA — Property-based prover testing

• AffineScript — Compiles to WasmGC; uses this repo as aggregate library

• Ephapax — Compiles to WasmGC; uses this repo as aggregate library

9. 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.

10. License

PMPL-1.0-or-later

11. Author

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