v1.1.1 inline_functions: Z3 SortDiffers (BitVec 64 vs 32) + new unwrap-None panics still trip on i64 (was #98, fixed in v1.0.0)

[avrabe]

Summary

On loom v1.1.1 (7311c8a8), loom optimize on an i64-heavy module reproduces the Z3 SortDiffers { left: (_ BitVec 64), right: (_ BitVec 32) } failure in inline_functions — the same root cause as the previously-closed #98 ("Z3 SortDiffers panic in inline_functions on i64"), which was reported fixed in v1.0.0. In addition, two new Z3-binding panics now appear:

• z3/src/ast/bool.rs:70:18: called Option::unwrap() on a None value
• z3/src/ast/bv.rs:174:5: called Option::unwrap() on a None value

Good news / the v1.1.x improvement: these no longer hang or kill the run (v1.0.3 hung indefinitely after Running: inline). Each is now caught and the function is reverted:

inline_functions: reverting function: inline_functions: Z3 internal error - optimization rejected (unproven)

So the optimizer makes progress and finishes. But on an i64-heavy module the inliner reverts essentially every function, so:

1. inline_functions is effectively a no-op for i64-heavy modules (no verified inlining, the LLVM-LTO-equivalent shape we want is never produced), and
2. it emits a panic line per reverted function — on a ~1 MB merged module this produced 21 MB+ of stderr (tally below) before we stopped it.

Panic tally (single run, ~1 MB merged wasm, 824+ functions, ~30% compiler_builtins)

5796 ×  z3/src/ast/bool.rs:70:18   unwrap() on None
2511 ×  z3/src/ast/bv.rs:174:5     unwrap() on None
 773 ×  z3/src/ast/mod.rs:601:1    SortDiffers { left: (_ BitVec 64), right: (_ BitVec 32) }

Reproduction

# gale-ffi (Rust) built as wasm32 staticlib, merged with a C host shim via wasm-ld:
wasm-ld --no-entry --export-all --allow-undefined \
  --whole-archive libgale_ffi.a --no-whole-archive shim.wasm.o -o merged.wasm   # ~1 MB
loom optimize merged.wasm -o merged.opt.wasm --stats

🔧 LOOM Optimizer v1.1.1
✓ Parsed in 5.16ms
⚡ Optimizing...
  Running: directize
  Running: inline
thread 'main' panicked at z3/src/ast/bool.rs:70:18: called `Option::unwrap()` on a `None` value
inline_functions: reverting function: ... Z3 internal error - optimization rejected (unproven)
... (repeats thousands of times) ...

Two requests

1. The i64 SortDiffers bit-width mismatch is back (or was never fully fixed for this shape). When inline_functions builds the Z3 equality, an i64 (BitVec 64) operand is being compared against an i32 (BitVec 32) operand without a zero/sign-extend or i32.wrap_i64 bridge. The bool.rs:70 / bv.rs:174 unwrap()-on-None panics look like the same underlying width/None issue surfacing through different binding call sites.

2. Panic-as-control-flow is very noisy. Reverting per function via caught panics emits thousands of panicked at … lines (21 MB+). Could the i64 case that's known-unprovable be detected up front and skipped quietly (one summary line, e.g. inline: skipped N functions with unsupported i64 width-mismatch), rather than panicking + catching per function?

Why it matters

We're using wasm-ld merge → loom → synth as a verified cross-language-LTO route (dissolve a C↔Rust FFI seam at wasm-IR level with loom providing verified inlining). With every i64 function reverted, loom can't deliver the verified-inliner shape on this class of module — the exact gale-ffi modules we care about are i64-heavy (u64-packed FFI returns, compiler_builtins).

Environment

• loom v1.1.1 (7311c8a8)
• input: 1,025,783-byte wasm-ld merge of a Rust wasm32-unknown-unknown staticlib + a clang wasm32 host shim

[avrabe]

WAT reproducer attached as a gist (3.2 MB / 64k lines — the i64-heavy ~1 MB merged module):

https://gist.github.com/avrabe/3dcece1071717a5f8b54b0045cdc730e

loom optimize merged.wat -o out.wasm --stats reproduces the SortDiffers { BitVec 64 vs 32 } + unwrap()-on-None panic flood (each caught + function reverted).