inline_functions reverts ALL i64 inlines (even trivial i64.add) — verifier can't prove i64 inline soundness; no-op for i64 modules

[avrabe]

Summary

On loom v1.1.3 (550d3c0b, post-#147), inline_functions reverts every i64 function inline — even a trivial one — because the translation validator can't prove i64 inlines sound. The hang from #147 is fixed (it now terminates and reverts cleanly), but the net effect is that the verified inliner is a no-op for any i64-returning function.

This blocks the use case #147 was meant to re-enable: dissolving the gale C↔Rust seam, where gale_k_sem_give_decide(...) -> i64 must inline into z_impl_k_sem_give.

Minimal reproduction

(module
  (func $add1 (param i64) (result i64) (i64.add (local.get 0) (i64.const 1)))
  (func $c (export "c") (param i64) (result i64) (call $add1 (local.get 0))))

loom optimize i64inline.wat --passes inline --stats -o /dev/null

Instructions: 5 → 5 (0.0% reduction)
  (no effect: inline)
🔁 Verification Reverts
  inline_functions               1 function(s) reverted
  Total: 1 revert(s)
✅ Optimization complete!

$add1 is as simple as an i64 callee gets (one i64.add of a constant), and it is still reverted. Same result on the real gale seam (merged.both.wasm: z_impl inlining gale_k_sem_give_decide -> i64) → 1 revert, no inline.

Ask

#147 added the Z3 per-query timeout so i64 inline verification terminates (thank you — confirmed, 9 ms now). The follow-up is to make it succeed: teach the validator to prove i64 inlines sound (width-correct i64 substitution / equality under the inlined body) so they aren't reverted. Until then the verified inliner can't optimize any i64-bearing module, and the LTO-parity seam-dissolution path stays closed.

If the i64 inline verification is known-incomplete by design for now, a note in --stats (e.g. "reverted: i64 inline unproven") vs a generic revert would make it clear the revert is a verifier-capability gap rather than an unsound-inline rejection.

Environment

• loom v1.1.3 (550d3c0b), --passes inline
• trivial repro above; real case = merged.both.wasm (WAT in synth#167 gist)

[avrabe]

Fixed in v1.1.4 (https://github.com/pulseengine/loom/releases/tag/v1.1.4, commit cc66f398).

Your trivial repro now inlines (verified, not reverted):

$ loom optimize i64inline.wat --passes inline --stats -o /dev/null
Instructions: 5 → 8 (-60.0% reduction)
  inline                  5 →    8 (-3 instructions)
✅ Optimization complete!      # 0 reverts; the `call $add1` is gone

Root cause was deeper than i64. Ground-truthing your report showed an i32 control reverted too: the translation validator modeled call F as an opaque uninterpreted function pure_call_F(args). That's exactly right for proving two identical calls equal (CSE / directize) but can never prove a call equal to its own inlined body — so every inline was reverted as "unproven". You only saw it on i64 because that was the gale seam.

The fix isn't the diagnostic-only fallback you offered — it's the real thing you asked for first. When F is a pure, no-trap, leaf, straight-line, single-result callee, the validator now models call F(args) by symbolically executing F's own body on the argument bit-vectors (i.e. by F's definition). The original (with the call) and the optimized (with F inlined) then compute the identical expression, Z3 proves them equal, and the inline is kept with a real proof. Callees outside that whitelist fall back to the conservative opaque encoding (spurious revert at worst, never an unsound accept).

A soundness guard locks in both directions: a correct x+1 inline of add1 is proven equivalent, a wrong x+2 "inline" is rejected (counterexample).

For the real seam (merged.both.wasm, z_impl inlining gale_k_sem_give_decide -> i64): the u64-unpack shape (shr_u/and/or/xor/shifts) is inside the whitelist, so it should inline now — please re-test and confirm. If the decider uses ops outside the current straight-line integer whitelist (rotates, popcount, control flow, memory/global reads), those are gated follow-up additions — tell me which and I'll widen the whitelist with a soundness argument per op.