fix(verify): prove i64 (and all-type) inlining via by-body call modeling — closes #151 (v1.1.4)

[avrabe]

gale #151 — verified i64 inlining

Bug-fix release v1.1.4. On v1.1.3, loom optimize --passes inline reverted every i64 inline — even a trivial i64.add callee — as "unproven", making the verified inliner a no-op for i64 modules and blocking the gale C↔Rust seam (z_impl_k_sem_give inlining gale_k_sem_give_decide -> i64).

Root cause (deeper than reported)

Ground-truthing falsified the "i64-specific" framing — an i32 control reverted too. The Z3 translation validator modeled call F as an opaque uninterpreted function pure_call_F(args). That encoding proves two identical calls equal (CSE / directize depend on it) but can never prove a call equal to its own inlined body. So the original (with the call) and the optimized (with F inlined) never matched → every inline reverted. i32 was a no-op for the same reason; the report only noticed i64 because that was the gale use case.

Fix

• By-body call modeling: when F is a pure, no-trap, leaf, straight-line, single-result callee, model call F(args) by symbolically executing F's own body on the argument bit-vectors instead of an opaque symbol. Original and optimized then compute the identical expression → Z3 proves them equal → the inline is kept with a real proof. Callees outside the whitelist fall back to the conservative opaque encoding (at worst a spurious revert, never an unsound accept); a defensive width check rejects any wrong-width result.
• Consistency: both the direct call F and the resolved call_indirect paths use the by-body model, keeping directize's call_indirect ⇔ call F equivalence intact.
• i64 in nested blocks: encode_simple_instruction now models the full i64 arithmetic / bitwise / comparison / eqz set + total width conversions (extend_i32_{s,u}, wrap_i64) — previously every i64 op inside a block/loop/if was an opaque BV32 (latent gap beyond inlining).

Soundness

test_inline_verifier_proves_correct_and_rejects_wrong_i64_inline locks in both directions: a correct x+1 inline of add1 is proven equivalent, and a deliberately wrong x+2 "inline" is rejected (counterexample). The previously-#[ignore]'d test_inline_pass_actually_inlines_i64_helper (#147 follow-up) is re-enabled and passing.

Validation

• 385 lib tests pass (incl. soundness guard + directize consistency)
• trivial i64 + i32 repros now inline (call eliminated, valid output, 0 reverts)
• real gale wasm + full default pipeline dogfood clean (valid output)

Known-red gates (pre-existing, not introduced here)

• Rocq Formal Proofs — upstream toolchain breakage (tracked).
• Test matrix — the 7 pre-existing LICM/DCE failures (7 pre-existing LICM/DCE integration tests fail (loop body not hoisted) — exposed once the Test matrix completes #150); they fail identically on v1.1.1 and are untouched by this change (it modifies call-modeling + i64 arithmetic, not LICM/DCE).

Closes #151.

🤖 Generated with Claude Code