wasm-num

Formally verified WebAssembly numeric semantics, 128-bit SIMD, and linear memory model in Lean 4.

Overview

wasm-num is a comprehensive Lean 4 formalization of the WebAssembly numeric layer — covering integer and floating-point operations, type conversions, 128-bit SIMD (including relaxed SIMD), and linear memory semantics. Every definition is backed by machine-checked proofs that verify conformance to the WebAssembly specification.

Why wasm-num?

• Spec-Complete Numerics — All Wasm numeric instructions: integer arithmetic, bitwise, shifts, comparisons, conversions, floating-point operations, and NaN propagation.
• Full SIMD Coverage — V128 operations, 6 lane shapes, lanewise integer/float ops, shuffle, swizzle, narrowing/widening, and all relaxed SIMD proposals.
• Linear Memory Model — FlatMemory with page management, scalar/packed/SIMD loads and stores, memory.grow/copy/fill/init, multi-memory, and Memory64 support.
• Machine-Checked Proofs — Load–store roundtrip, lane bijections, NaN propagation correctness, deterministic-implies-spec, bounds safety, overlap correctness, and more.
• IEEE 754 Independence — The WasmFloat typeclass abstracts over any IEEE 754 implementation via ADR-001. Plug in your own float library.
• Non-determinism as Sets — Spec-level non-determinism (NaN payloads, relaxed SIMD, memory.grow) is modeled as Set α, enabling both proof reasoning and deterministic runtime instantiation via profiles.
• Built on Mathlib — Leverages BitVec, Finset, and Mathlib's algebraic infrastructure.

At a Glance

Component	Definitions	Proofs	Tests
Foundation (types, BitVec, WasmFloat, profiles)	6 modules	—	1 module
Numerics (NaN, float, integer, conversions)	21 modules	6 modules	3 modules
SIMD (V128, lanewise, relaxed)	19 modules	4 modules	3 modules
Memory (core, load/store, ops, multi-memory)	13 modules	4 modules	3 modules
Integration (profiles, runtime)	2 modules	—	1 module
Total	~70 modules	14 modules	11 modules

Quick Start

Prerequisites

• Lean 4 (v4.29.0-rc6 or compatible — pinned via lean-toolchain)
• Lake (bundled with Lean 4)

Build

# Clone the repository
git clone https://github.com/Provenance-Works/wasm-num.git
cd wasm-num

# Fetch and cache Mathlib (first build takes a while)
lake exe cache get

# Build all definitions and proofs
lake build

Verify

# Build definitions only
lake build WasmNum

# Build definitions + proofs
lake build WasmNumProofs

# Run tests
lake build TestAll

Architecture

wasm-num uses a strict layered architecture with no circular dependencies:

Layer 4: Integration
         WasmFloat instances · GrowthPolicy · Runtime adapter
         │
Layer 3: Memory
         FlatMemory · Load/Store · SIMD Memory Ops · Multi-Memory · Memory64
         │
Layer 2: SIMD
         V128 · Shapes · Lanewise Ops · Shuffle/Swizzle · Relaxed SIMD
         │
Layer 1: Wasm Numerics
         NaN Propagation · fmin/fmax/fnearest · Conversions · Integer Ops
         │
Layer 0: Foundation
         BitVec · WasmFloat typeclass · Profiles · Core types

All numeric types use BitVec N as the universal representation (integers and floats alike). Floating-point semantics are decoupled through the WasmFloat typeclass, allowing any IEEE 754 implementation to be plugged in without modifying wasm-num.

Non-deterministic operations return Set α at the spec level. The WasmProfile (= NaNProfile + RelaxedProfile) narrows these sets, and the Integration layer provides fully deterministic wrappers for runtime use.

For more details, see:

• Architecture
• Design Decisions (ADRs)
• Full Documentation (English / 日本語)

Module Map

WasmNum/
├── Foundation/          # Layer 0 — Types, BitVec utils, WasmFloat, Profiles
├── Numerics/
│   ├── NaN/             # NaN propagation (spec + deterministic)
│   ├── Float/           # fmin, fmax, rounding, sign, comparisons
│   ├── Integer/         # Arithmetic, bitwise, shifts, saturating, etc.
│   └── Conversion/      # trunc, trunc_sat, promote, demote, reinterpret, extend
├── SIMD/
│   ├── V128/            # V128 type, shapes, lane access
│   ├── Ops/             # Bitwise, int/float lanewise, shuffle, swizzle, bitmask, etc.
│   └── Relaxed/         # madd, relaxed min/max, relaxed trunc, laneselect, dot, q15
├── Memory/
│   ├── Core/            # FlatMemory, Address, Bounds, Page
│   ├── Load/            # Scalar, Packed, SIMD loads
│   ├── Store/           # Scalar, Packed, SIMD stores
│   └── Ops/             # size, grow, fill, copy, init, data.drop
├── Integration/         # Deterministic wrappers, runtime adapter
└── Proofs/              # Machine-checked proofs (parallel hierarchy)

WasmTest/                # Executable tests (#eval)

Usage as a Dependency

Add wasm-num to your lakefile.toml:

[[require]]
name = "wasm-num"
scope = "Provenance-Works"

Then import what you need:

-- All definitions (no proofs)
import WasmNum

-- Definitions + all proofs
import WasmNumProofs

-- Specific modules
import WasmNum.Numerics.Integer.Arithmetic
import WasmNum.SIMD.V128.Lanes
import WasmNum.Memory.Core.FlatMemory

Key Design Decisions

ADR	Decision
ADR-001	IEEE 754 independence via WasmFloat typeclass
ADR-002	BitVec N as universal representation for all numeric types
ADR-003	Non-determinism modeled as Set α
ADR-004	V128 shape system for SIMD lane types
ADR-005	FlatMemory parameterized by address width
ADR-006	Strict separation of definitions and proofs
ADR-007	No C FFI — pure Lean only

Contributing

Contributions are welcome! Please read CONTRIBUTING.md before getting started.

All contributors must follow our Code of Conduct.

Security

To report a security vulnerability, please see SECURITY.md. Do not open a public issue.

License

Copyright 2026 Provenance Works

Licensed under the Apache License, Version 2.0. See LICENSE for the full text.

Acknowledgments

• Lean 4 — the proof assistant and programming language
• Mathlib4 — the community mathematics library
• WebAssembly Specification — the formal specification this project formalizes