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

CHANGELOG.md

@@ -5,6 +5,55 @@ All notable changes to LOOM will be documented in this file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/),
 and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 
+## [1.1.4] - 2026-05-30
+
+**Bug-fix release: verified i64 (and all-type) inlining (#151).** Closes
+the v1.1.3 follow-up where `inline_functions` *reverted every i64 inline*
+— even a trivial `i64.add` callee — because the translation validator
+could not prove i64 inline-equivalence. This unblocks the gale C↔Rust
+seam (`z_impl_k_sem_give` inlining `gale_k_sem_give_decide -> i64`).
+
+### Fixed
+
+- **#151: the verified inliner was a no-op for i64 — and, it turned out,
+  for *every* type.** Ground-truthing the report exposed a deeper cause
+  than "i64-specific": the Z3 translation validator modeled a `call F`
+  as an **opaque uninterpreted function** `pure_call_F(args)`. That
+  encoding can prove two *identical* calls equal (which is what CSE /
+  directize rely on) 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, and *every* inline was reverted as
+  "unproven". i32 inlines happened to be no-ops for the same reason; the
+  report only noticed i64 because that was the gale use case.
+
+  Fix: 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 — instead of an opaque symbol. The original and optimized
+  then compute the identical expression and Z3 proves them equal, so the
+  inline is *kept with a real proof*. Callees outside that whitelist fall
+  back to the conservative opaque encoding (at worst a spurious revert,
+  never an unsound accept). 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.
+
+  A **soundness guard** test
+  (`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 now
+  re-enabled and passing.
+
+- **i64 arithmetic inside nested blocks is now modeled correctly.** The
+  nested-block SMT interpreter (`encode_simple_instruction`) previously
+  handled only i32 arithmetic — every i64 op inside a `block`/`loop`/`if`
+  fell through to an opaque 32-bit symbolic, a latent verification gap
+  beyond inlining. v1.1.4 adds the full i64 arithmetic / bitwise /
+  comparison / `eqz` set plus the total width conversions
+  (`i64.extend_i32_{s,u}`, `i32.wrap_i64`), mirroring the existing i32
+  arms at width 64.
+
 ## [1.1.3] - 2026-05-30
 
 **Bug-fix release: the gale-ffi i64 inline hang (#147).** Closes the

Cargo.toml

@@ -9,7 +9,7 @@ members = [
 ]
 
 [workspace.package]
-version = "1.1.3"
+version = "1.1.4"
 authors = ["PulseEngine <https://github.com/pulseengine>"]
 edition = "2024"
 license = "Apache-2.0"

loom-core/src/lib.rs

@@ -13281,6 +13281,14 @@ pub mod optimize {
             // Clone functions to avoid borrow checker issues
             let all_functions = module.functions.clone();
 
+            // loom#151: build the verification signature context (with
+            // callee bodies) ONCE per iteration, before the mutable loop.
+            // This lets the translation validator model `call F(args)` by
+            // F's own body and thereby PROVE the inline sound — without it
+            // the validator falls back to an opaque uninterpreted call and
+            // reverts every inline (no-op for i64 and every other type).
+            let verify_sig_ctx = crate::verify::VerificationSignatureContext::from_module(module);
+
             // Did this iteration KEEP any inline (verified, not reverted)?
             // Only kept inlines are progress; an iteration that reverts
             // everything must not loop again (loom#147 livelock guard).
@@ -13295,7 +13303,11 @@ pub mod optimize {
                 let before = func.instructions.clone();
 
                 let guard = ValidationGuard::with_context(func, "inline_functions", ctx.clone());
-                let translator = TranslationValidator::new(func, "inline_functions");
+                let translator = TranslationValidator::new_with_context(
+                    func,
+                    "inline_functions",
+                    verify_sig_ctx.clone(),
+                );
 
                 func.instructions = inline_calls_in_block(
                     &func.instructions,
@@ -18257,17 +18269,14 @@ mod tests {
     }
 
     #[test]
-    #[ignore = "loom#147 follow-up: asserts the i64 helper is INLINED, but \
-    the Z3 verifier currently REVERTS the i64 inline (cannot prove i64 \
-    inline-equivalence) — a sound, conservative outcome. The #147 livelock \
-    that hung the pass is fixed and the other four i64 inline tests are \
-    re-enabled; this one needs real verified i64 inlining (or a reworked \
-    assertion) before it can pass."]
     fn test_inline_pass_actually_inlines_i64_helper() {
-        // Past the panic-prevention bar: confirm the pass does its job
-        // on i64 helpers — the call must be replaced by the helper's
-        // body. Pre-fix this test would also fail because every function
-        // reverted under the panic-catch.
+        // loom#151: the verifier now models a pure, no-trap, leaf,
+        // straight-line callee by its OWN BODY (not an opaque
+        // uninterpreted call), so it can PROVE the i64 inline sound and
+        // KEEP it. Before #151 every i64 inline (even `x + x`) reverted
+        // because the opaque call model could never equal the inlined
+        // body. Confirm the pass does its job on i64 helpers — the call
+        // must be replaced by the helper's body.
         let wat = r#"(module
             (func $double (param i64) (result i64)
                 local.get 0
@@ -18305,6 +18314,64 @@ mod tests {
         wasmparser::validate(&wasm_bytes).expect("output validates");
     }
 
+    #[cfg(feature = "verification")]
+    #[test]
+    fn test_inline_verifier_proves_correct_and_rejects_wrong_i64_inline() {
+        // loom#151 SOUNDNESS GUARD. The by-body call model must do BOTH:
+        //   (a) PROVE a correct i64 inline equivalent (so inlining works), and
+        //   (b) REJECT a semantically WRONG inline (so it stays sound).
+        // add1(x) = x + 1. Modeled by its body, `call add1(x)` becomes the
+        // expression `x + 1`, so:
+        //   - a caller inlined to `x + 1` MUST verify (Ok(true));
+        //   - a caller "inlined" to `x + 2` MUST NOT verify (Ok(false)).
+        // If (b) ever returns Ok(true), by-body modeling has become unsound
+        // and this test fails loudly — exactly the gate we want.
+        use crate::verify::{
+            VerificationSignatureContext, verify_function_equivalence_with_context,
+        };
+        let wat = r#"(module
+            (func $add1 (param i64) (result i64)
+                local.get 0
+                i64.const 1
+                i64.add
+            )
+            (func $caller (param i64) (result i64)
+                local.get 0
+                call 0
+            )
+        )"#;
+        let module = parse::parse_wat(wat).expect("parse");
+        let ctx = VerificationSignatureContext::from_module(&module);
+        // Original: `local.get 0; call $add1`.
+        let orig = module.functions[1].clone();
+
+        // (a) Correct inline of add1: x + 1 — must be PROVEN equivalent.
+        let mut correct = orig.clone();
+        correct.instructions = vec![
+            Instruction::LocalGet(0),
+            Instruction::I64Const(1),
+            Instruction::I64Add,
+        ];
+        assert!(
+            verify_function_equivalence_with_context(&orig, &correct, "test", &ctx)
+                .expect("verify ok"),
+            "correct i64 inline (x+1) must be proven equivalent to call add1",
+        );
+
+        // (b) WRONG inline: x + 2 — must be REJECTED (counterexample).
+        let mut wrong = orig.clone();
+        wrong.instructions = vec![
+            Instruction::LocalGet(0),
+            Instruction::I64Const(2),
+            Instruction::I64Add,
+        ];
+        assert!(
+            !verify_function_equivalence_with_context(&orig, &wrong, "test", &ctx)
+                .expect("verify ok"),
+            "SOUNDNESS: wrong i64 inline (x+2) must NOT verify against call add1",
+        );
+    }
+
     #[test]
     fn test_inline_i64_loop_kinduction_no_panic() {
         // loom#145 regression: the prior i64 inline tests are loopless, so