-
-
Notifications
You must be signed in to change notification settings - Fork 0
Home
TypeLL's 10-level type safety for WebAssembly linear memory.
See the main README for installation and usage.
cd ffi/zig && zig build test # Zig FFI tests
cd src/abi && idris2 --check Proofs.idr # Idris2 ABI proofs- WASM memory as a database -- WebAssembly's linear memory is an untyped byte array, structurally identical to a schemaless database. typed-wasm adds schemas (regions) and type-safe queries (typed access operations), verified by the Idris2 prover at compile time with zero runtime overhead.
- 10 progressive safety levels -- From instruction validity (L1) through bounds-proofs (L5) to full linearity (L10), each level adds compile-time guarantees that eliminate a class of memory errors.
- Multi-module type safety -- When Module A (Rust) shares WASM memory with Module B (ReScript), neither source-level type system can verify the boundary. typed-wasm declares the shared schema once and verifies structural agreement at compile time.
Follows the hyperpolymath ABI-FFI standard: Idris2 for formal ABI definitions (src/abi/), Zig for C-compatible FFI implementation (ffi/zig/), with a .twasm surface syntax defined in spec/grammar.ebnf.
See spec/ for the full specification.
For multi-producer adoption, the verifier needs to re-derive type-safety levels from emitted wasm bytes without trusting any single producer's source-level checker. This is the carrier ABI -- producer-neutral custom sections that travel with the module:
-
Proposal 0001 --
typedwasm.regions(schema for L2-L6) +typedwasm.capabilities(L15 capability lattice). Status:[draft], cross-repo review under way (affinescript#402, ephapax#165). -
Proposal 0002 --
typedwasm.access-sites(per-instruction(func_idx, byte_offset) → (region_id, field_id)mapping for L2-the-enforcement). Wire format adopts Encoding B (LEB128 per field, ~5B/access) per the issue #78 prototype measurement. Status:[draft], gated on proposal 0001 acceptance.
Proposals graduate to ADRs under docs/decisions/ on owner acceptance. The verifier's verify_region_binding pass is gated on proposal 0002's acceptance.
- TypeLL -- Type theory foundation (typed-wasm implements TypeLL's levels for WASM)
- TypedQLiser -- Same principle applied to database queries
- Ephapax -- Linear type language targeting WASM
- ECHIDNA -- Property-based testing of proof soundness
See CONTRIBUTING.md.