Observation
loom optimize panics in the inline_functions pass when given i64-heavy wasm modules. Each function in the gale-ffi crate (which uses u64-packed FFI returns extensively) triggers the panic and gets reverted, so the inliner is effectively a no-op.
Reproducer
# Build gale-ffi as wasm32 staticlib (1MB merged with a shim via wasm-ld is enough)
( cd /Volumes/Home/git/pulseengine/gale-smart-data/ffi && \
cargo rustc --release --target wasm32-unknown-unknown --crate-type=staticlib )
clang --target=wasm32-unknown-unknown -O2 -nostdlib -c shim.c -o shim.wasm.o
wasm-ld --no-entry --export-all --allow-undefined \
--whole-archive .../libgale_ffi.a --no-whole-archive shim.wasm.o \
-o merged.wasm
loom optimize merged.wasm --attestation false -o opt.wasm
Observed panic
🔧 LOOM Optimizer v0.5.0
Input: merged.wasm
✓ Parsed in 6.3ms
⚡ Optimizing...
Running: inline
thread 'main' panicked at z3.rs/src/ast/mod.rs:601:1:
called `Result::unwrap()` on an `Err` value: SortDiffers {
left: (_ BitVec 64),
right: (_ BitVec 32)
}
inline_functions: reverting function: Z3 internal error - optimization rejected (unproven)
(repeats for every function in the gale-ffi module)
inline_functions: reverting function: Verification failed
(inline_functions: Failed to encode optimized: Stack underflow)
The pattern repeats for every gale-ffi function. After all reverts, loom emits the input unchanged.
Root cause hypothesis
The inline_functions pass's Z3 encoding doesn't unify i64 and i32 sorts when checking whether the inlined call is observationally equivalent to the original. gale-ffi's FFI return values are u64 (to satisfy AAPCS register packing and enable LLVM's cross-language inliner — see gale's #10), and the callers immediately mask down to u8 or u32 fields. The Z3 backend tries to compare a BitVec 64 against a BitVec 32 and panics.
Why this matters
Without the inline pass operational, loom's contribution to the wasm-cross-LTO pipeline is lost. meld → loom → synth reduces to meld → synth for verification purposes — we lose the formally-proven inlining step that's loom's distinguishing value vs. binaryen's wasm-opt.
For pulseengine/gale's silicon-anchor protocol (PR #40), this means the wasm-LTO route can't claim "verified-equivalent of LLVM-LTO" until the inline pass works on i64-packed-return functions.
Recommendation
The Z3 encoding for the inline pass needs to accept mixed-width bitvectors and either (a) extend the narrower side to match (zero-extend or sign-extend, depending on the wasm op), or (b) refuse to encode mixed-width comparisons and fall back to a different verification strategy for i64 inlining.
Cross-references
Observation
loom optimizepanics in theinline_functionspass when given i64-heavy wasm modules. Each function in the gale-ffi crate (which uses u64-packed FFI returns extensively) triggers the panic and gets reverted, so the inliner is effectively a no-op.Reproducer
Observed panic
The pattern repeats for every gale-ffi function. After all reverts, loom emits the input unchanged.
Root cause hypothesis
The
inline_functionspass's Z3 encoding doesn't unify i64 and i32 sorts when checking whether the inlined call is observationally equivalent to the original. gale-ffi's FFI return values are u64 (to satisfy AAPCS register packing and enable LLVM's cross-language inliner — see gale's #10), and the callers immediately mask down to u8 or u32 fields. The Z3 backend tries to compare aBitVec 64against aBitVec 32and panics.Why this matters
Without the inline pass operational, loom's contribution to the wasm-cross-LTO pipeline is lost.
meld → loom → synthreduces tomeld → synthfor verification purposes — we lose the formally-proven inlining step that's loom's distinguishing value vs. binaryen's wasm-opt.For pulseengine/gale's silicon-anchor protocol (PR #40), this means the wasm-LTO route can't claim "verified-equivalent of LLVM-LTO" until the inline pass works on i64-packed-return functions.
Recommendation
The Z3 encoding for the inline pass needs to accept mixed-width bitvectors and either (a) extend the narrower side to match (zero-extend or sign-extend, depending on the wasm op), or (b) refuse to encode mixed-width comparisons and fall back to a different verification strategy for i64 inlining.
Cross-references