[Bug][Compiler-v2][Prover] CALL_BORROWED_MUTABLE_REFERENCE_ERROR is raised when there is an inline spec

[rahxephon89]

🐛 Bug

When adding to the following spec block after the while loop in the inline function vector::find

        spec {
           assert find ==> f(self[found_index]);
        };

compiler v2 will generate the following error when compiling the aptos-framework code:

bug: bytecode verification failed with unexpected status code CALL_BORROWED_MUTABLE_REFERENCE_ERROR. This is a compiler bug, consider reporting it.
┌─ /Users/tengzhang/aptos-core/aptos-move/framework/aptos-framework/sources/jwks.move:582:26
│
582 │ option::some(vector::remove(&mut jwks.entries, index))
│ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

[rahxephon89]

This is the minimal example and inline is actually not involved:

module 0xc0ffee::m {
    use std::vector;

    struct S has copy, drop, store {
        i: u8,
    }

    struct T has copy, drop, store {
        entries: vector<S>,
    }

    fun test(t: &mut T) {
        let set: &S = vector::borrow(&t.entries, 0);
        spec {
            assert set.i == 0;
        };
        vector::remove(&mut t.entries, 0);
    }
}

This is the file-format:

// Move bytecode v7
module c0ffee.m {
use 0000000000000000000000000000000000000000000000000000000000000001::vector;


struct T has copy, drop, store {
	entries: vector<S>
}
struct S has copy, drop, store {
	i: u8
}

test(Arg0: &mut T) /* def_idx: 0 */ {
L1:	loc0: &S
B0:
	0: CopyLoc[0](Arg0: &mut T)
	1: ImmBorrowField[0](T.entries: vector<S>)
	2: LdU64(0)
	3: VecImmBorrow(2)
	4: StLoc[1](loc0: &S)
	5: Nop
	6: MoveLoc[0](Arg0: &mut T)
	7: MutBorrowField[0](T.entries: vector<S>)
	8: LdU64(0)
	9: Call vector::remove<S>(&mut vector<S>, u64): S
	10: Pop
	11: Ret
}
}

Note that instead of using set, if we use the following spec, no error will be generated.

        spec {
            assert t.entries[0].i == 0;
        };

[rahxephon89]

Another example with inline function used:

module 0xc0ffee::m {
    use std::vector;

    struct S has copy, drop, store {
        i: u8,
    }

    struct T has copy, drop, store {
        entries: vector<S>,
    }

    inline fun inline_test(t: &mut T) {
        spec {
            assert t.entries[0].i == 0;
        };
    }

    fun test(t: &mut T) {
        inline_test(t);
        vector::remove(&mut t.entries, 0);
    }
}

Unlike the previous example, there is no work around of writing this spec to avoid the error.