| FazBrowse GitHub Viewer | Trending | | Home |
| Tools: [Download Repo ZIP] [Original HTTPS Page] |
| Name | Name | Last commit date | ||
|---|---|---|---|---|
Meld fuses. Loom weaves. Synth transpiles. Kiln fires. Sigil seals.
WebAssembly optimization pipeline built on Cranelift's ISLE pattern-matching engine. Constant folding, strength reduction, CSE, inlining, dead code elimination — each pass translation-validated by Z3 SMT: semantic equivalence is proved per function, per run (this validates each output, not a once-and-for-all proof of the optimizer itself). Includes a fused mode purpose-built for Meld output.
Loom consistently achieves 80-95% binary size reduction with 10-30 microsecond optimization times. The entire pipeline is pure Rust with minimal dependencies.
# Build from source
git clone https://github.com/pulseengine/loom
cd loom
cargo build --release
# Optimize a WebAssembly module
loom optimize input.wasm -o output.wasm
# With statistics
loom optimize input.wasm -o output.wasm --stats
# With Z3 verification
loom optimize input.wasm -o output.wasm --verifyTwo pipeline surfaces:
See docs/architecture.md for the full pipeline design.
Z3 SMT translation validation is on by default (default = ["verification", "attestation"] in loom-core / loom-cli Cargo.toml). Each optimization pass proves semantic equivalence per function before accepting the transform; on counterexample, the function is reverted to its pre-pass state.
# Default build — Z3 verification on
cargo build --release
loom optimize input.wasm -o output.wasm --verify
# Disable Z3 (faster, no semantic proofs)
cargo build --release --no-default-featuresSee docs/guides/formal-verification.md for details.
Note
Cross-cutting verification — Rocq mechanized proofs, Kani bounded model checking, Z3 SMT verification, and Verus Rust verification are used across the PulseEngine toolchain. Sigil attestation chains bind it all together.
cargo build --release # Standard build (Z3 on by default)
cargo build --release --no-default-features # Without Z3 verification
cargo test # Run tests
cargo bench # Run benchmarks
# WASM build (CI uses these exact steps)
rustup target add wasm32-wasip2
cargo build --release --target wasm32-wasip2 --package loom-cliApache-2.0
Part of PulseEngine — WebAssembly verification toolchain for safety-critical systems
| Back | FazBrowse Home | New Git URL |