TMLM: Experimental Data, Test Cases, and Formal Proofs for Type-Driven Lowering Bugs in WebAssembly JIT Compilers

This dataset contains the complete experimental artifacts accompanying the paper "TMLM: A Taxonomy of Type-Driven Lowering Bugs in WebAssembly JIT Compilers." It includes: Experimental results (JSON): 512-test AArch64 exhaustive TMLM-Shift scan (CVE-2026-34971, CVSS 9.0); 384-test x86-64 cross-architecture validation; Pattern H Winch scan (CVE-2026-34987, CVSS 9.9); TES formal framework validation (13 checks, 11 passed); fuzzing comparison (3×300 random trials vs 8 TMLM-guided tests); full audit coverage report (25 ISLE rules, 6 code paths).Test cases (CLIF/WAT): Exhaustive AArch64 and x86-64 shift test programs; 12 Winch Pattern H exploitability WAT cases; ALU shift pattern tests; end-to-end PoC for sandbox escape.Formal proofs (Isabelle/HOL): Cranelift_IR.thy — 12 machine-checked theorems including the TES Universal Theorem and Pattern Classification Theorem.Reproduction scripts (Python 3.8+): Automated scan, validation, and fuzzing comparison pipelines.All code is MIT-licensed; all data (JSON/CLIF/WAT) is CC0. Requires Wasmtime v42.0.0 and v42.0.2, Rust toolchain, and Isabelle2024+ (for formal proofs).