Meld

^{Static WebAssembly component fusion}

 

 

Meld · Loom · Synth · Kiln · Sigil

 

Meld fuses. Loom weaves. Synth transpiles. Kiln fires. Sigil seals.

Meld statically fuses multiple WebAssembly components into a single core module, eliminating the need for runtime linking. Import resolution, index-space merging, and canonical ABI adapter generation happen at build time. The core transformations — resolution, index-space merging, and adapter generation — carry mechanized Rocq proofs, plus local Kani bounded-model-checking harnesses on the Canonical-ABI layout invariants; see Formal Verification for the per-stage coverage (some stages are specified but not yet proved, and the Kani harnesses are run locally, not gated in CI).

Unlike composition tools that produce linked-but-separate component graphs, Meld produces a single monolithic module suitable for whole-program optimization by Loom and native transpilation by Synth.

Quick Start

# From source (Cargo)
cargo install --path meld-cli

# From source (Bazel)
bazel build //meld-cli:meld

# Fuse two components
meld fuse component_a.wasm component_b.wasm -o fused.wasm

Full Pipeline

# 1. Build components
cargo component build --release

# 2. Fuse into single module
meld fuse composed.wasm -o fused.wasm

# 3. Optimize with Loom
loom optimize fused.wasm -o optimized.wasm

# 4. Run
wasmtime run optimized.wasm

Bazel Integration

load("@meld//rules:meld.bzl", "meld_fuse")

meld_fuse(
    name = "my_app",
    components = [
        ":component_a",
        ":component_b",
    ],
)

How It Works

1. Parse — Extract core modules and type information from components
2. Resolve — Build import/export graph, identify cross-component calls
3. Merge — Combine function/memory/table/global index spaces
4. Adapt — Generate Canonical ABI trampolines for cross-component calls
5. Encode — Output single core WebAssembly module

Adapter Generation

Cross-component calls may require adapters that handle string transcoding (UTF-8, UTF-16, Latin-1), memory copying between component memories, list/array serialization, and resource handle transfer. Meld generates these adapters using techniques inspired by Wasmtime's FACT (Fused Adapter Compiler of Trampolines).

Memory Strategies

Auto (Default)

Resolves to shared memory + address rebasing when that is provably sound — no input module contains memory.grow and there are at least two memories to merge — and to multi-memory otherwise. The point: out-of-the-box output flows through wasm-opt → synth with no extra flags whenever soundness permits a single-memory form (issue #172).

meld fuse a.wasm b.wasm -o fused.wasm
wasm-opt -Os fused.wasm -o fused.opt.wasm   # no --enable-multimemory needed

Multi-Memory

Each component retains its own linear memory. Cross-component calls use adapters that allocate in the callee's memory via cabi_realloc and copy data with memory.copy. Requires multi-memory support (WebAssembly Core Spec 3.0) — downstream tools need wasm-opt --enable-multimemory, and single-address-space (MCU) targets have no lowering for it.

meld fuse --memory multi a.wasm b.wasm -o fused.wasm

Shared Memory

All components share a single linear memory; pair with --address-rebase. Unsound if any component uses memory.grow — one component's growth corrupts every other component's address space, which is why auto only selects this form when no input can grow.

meld fuse --memory shared --address-rebase a.wasm b.wasm -o fused.wasm

Supply Chain Security

Meld integrates with Sigil for supply chain attestation. Each fusion operation records input component hashes, tool version and configuration, and transformation metadata. The attestation is embedded in the output module's custom section.

Verifying a Release

Every tagged release ships with a CycloneDX SBOM, a cosign-signed SHA256SUMS.txt, and a SLSA v1 build-provenance attestation. To verify an installed binary against what GitHub Actions actually built:

# 1. Download an archive plus the signed checksum manifest from the release page.
TAG=v0.11.0
TARGET=x86_64-unknown-linux-gnu
gh release download "$TAG" --repo pulseengine/meld \
  --pattern "meld-${TAG}-${TARGET}.tar.gz" \
  --pattern 'SHA256SUMS.txt' \
  --pattern 'SHA256SUMS.txt.cosign.bundle'

# 2. Verify SHA256SUMS.txt was signed by meld's release workflow (Sigstore keyless).
cosign verify-blob \
  --certificate-identity-regexp \
    'https://github.com/pulseengine/meld/.github/workflows/release.yml@.*' \
  --certificate-oidc-issuer \
    'https://token.actions.githubusercontent.com' \
  --bundle SHA256SUMS.txt.cosign.bundle \
  SHA256SUMS.txt

# 3. Verify the archive's digest is in the signed manifest.
sha256sum --ignore-missing -c SHA256SUMS.txt

# 4. (Optional) Verify the SLSA v1 build provenance attestation.
gh attestation verify "meld-${TAG}-${TARGET}.tar.gz" --repo pulseengine/meld

Step 2 proves the checksum file came from this repo's release.yml; step 3 ties the archive on disk to that signed manifest; step 4 independently confirms the archive was built by the same workflow run via GitHub's attestation API. Each release also includes a meld-<version>.cdx.json (CycloneDX SBOM, transitively covered by the signature on SHA256SUMS.txt) and build-env.txt capturing the runner toolchain versions.

Formal Verification

Meld's core transformations carry mechanized Rocq proofs — 350 closed proofs (Qed) across the resolver, merger, adapter, and specification layers (see proofs/STATUS.md for the per-stage coverage matrix). This is real, substantial verification on the core; it is not yet a whole-pipeline proof: the parser, rewriter, segments, and attestation stages are specified but their proofs are placeholders, orchestration (lib.rs) is unproven, and the semantic-preservation result is a forward simulation (the fused module simulates the original graph step-by-step; the reverse direction and the backward half of trap-equivalence are not yet proved).

Proven properties (Rocq):

• Merge correctness — Index remapping preserves function/memory/table references (injectivity, completeness, boundedness); memory-layout disjointness.
• Resolve correctness — Topological sort produces a valid instantiation order; cycle detection terminates.
• Adapter correctness — Canonical-ABI lift/lower roundtrip and crossing-adapter semantics (one FACT parameter-match lemma remains Admitted).
• Forward simulation — The fused module simulates the original component graph step-by-step (forward direction; fully proved).

In addition, the Canonical-ABI layout invariants (size/alignment saturating arithmetic, the #141 stream ring model) carry Kani bounded-model-checking harnesses (abi_proofs.rs, resolver.rs, merger.rs) that were VERIFICATION SUCCESSFUL locally (SR-40); these are not gated in CI (the shared runners do not ship the Kani toolchain), and the ABI size/alignment and aggregate-padding contracts that did not converge in CBMC fall back to unit tests.

Proofs are built via Bazel using rules_rocq_rust:

bazel build //proofs/transformations/merge:merge_spec
bazel build //proofs/spec:fusion_spec

See proofs/ for the full proof tree and PROOF_GUIDE.md for an introduction.

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.

Limitations

• Resources — Resource handle transfer across components is limited
• Async — Async component functions not yet supported
• String transcoding — UTF-8/UTF-16 and Latin-1/UTF-8 are implemented; UTF-8/Latin-1 is not yet supported

Development

cargo build                # Build
cargo test                 # Test
bazel build //...          # Bazel build
RUST_LOG=debug cargo run -- fuse a.wasm b.wasm -o out.wasm

Benchmarks

Criterion benchmarks for the fusion pipeline live in meld-core/benches/fusion_benchmarks.rs and exercise four groups:

• parser — ComponentParser::parse throughput per input byte.
• merger — Merger::merge throughput per component count.
• resolver — Resolver::resolve_with_hints throughput per resolved-symbol count.
• end_to_end — Fuser::fuse_with_stats over small / medium / large graphs.

cargo bench -p meld-core                          # full run
cargo bench -p meld-core --bench fusion_benchmarks -- parser   # one group
cargo bench -p meld-core --no-run                 # compile-only sanity (CI smoke)

CI runs cargo bench --no-run on every PR (.github/workflows/bench.yml) to prevent the bench harness from rotting. Full benches are not run in CI to keep PRs fast and avoid noisy regressions on shared runners.

License

Apache-2.0

---

_{Part of PulseEngine — formally verified WebAssembly toolchain for safety-critical systems}