[Bug][Prover] Inline Borrow Mut issue verifying spec invariants

[JakeSilverman]

🐛 Bug

There is an issue with how the prover handles inline functions that return mutable references.

To reproduce

attempt to prove following. Note that get_s_no_error is fine but get_s_error has error. The only difference is whether returned reference is mutable or not.

module 0x42::M {
    use std::option;

    spec S {
        invariant x > 20;
    }

    struct IsolatedPosition has key {
        position: S
    }

    struct CrossedPosition has key {
        positions: vector<S>
    }

    struct S has store {
        x: u64
    }

    struct Foo has key {
        x: u64
    }

    public(package) fun bar(x: u64): option::Option<Foo> {
        if (x > 20) {
            option::some(Foo { x: x })
        } else {
            option::none()
        }
    }

    inline fun must_find_position_mut(
        address: address, x: u64
    ): &mut S acquires IsolatedPosition, CrossedPosition {
        if (exists<IsolatedPosition>(address)) {
            &mut borrow_global_mut<IsolatedPosition>(address).position
        } else {
            let positions = &mut CrossedPosition[address].positions;
            let (is_found, index) = positions.find(|position| &position.x == &x);
            if (is_found) {
                positions.borrow_mut(index)
            } else {
                abort 1
            }
        }
    }

    inline fun must_find_position(
        address: address, x: u64
    ): &S acquires IsolatedPosition, CrossedPosition {
        if (exists<IsolatedPosition>(address)) {
            &borrow_global<IsolatedPosition>(address).position
        } else {
            let positions = &mut CrossedPosition[address].positions;
            let (is_found, index) = positions.find(|position| &position.x == &x);
            if (is_found) {
                positions.borrow(index)
            } else {
                abort 1
            }
        }
    }

    fun get_s_error(
        address: address, x: u64
    ): option::Option<Foo> acquires IsolatedPosition, CrossedPosition {
        let s = must_find_position_mut(address, x);
        bar(s.x)
    }

    fun get_s_no_error(
        address: address, x: u64
    ): option::Option<Foo> acquires IsolatedPosition, CrossedPosition {
        let s = must_find_position(address, x);
        bar(s.x)
    }
}

error: data invariant does not hold
  ┌─ /...:5:9
  │
5 │         invariant x > 20;

Expected Behavior

Both versions of these functions should verify fine.

System information

Please complete the following information:

• Aptos Core Version: a52d9c0 (Jul 21 latest commit)
• Rust Version: 1.87.0
• Computer OS: macOS 15.5
• Boogie version: 3.5.1.0

Additional context

Add any other context about the problem here.

[rahxephon89]

@JakeSilverman, what is the behavior if you directly inline them?