Repository: aptos-labs/aptos-core (language: python)

Issue:
[Bug][Compiler-v2][Prover] CALL_BORROWED_MUTABLE_REFERENCE_ERROR is raised when there is an inline spec
# 🐛 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))
    │                          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^


Discussion / hints:
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;
        };
```

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. 



Fix patch:
diff --git a/third_party/move/move-compiler-v2/src/pipeline/livevar_analysis_processor.rs b/third_party/move/move-compiler-v2/src/pipeline/livevar_analysis_processor.rs
index 36e22429ee40a..c888d9e67bec2 100644
--- a/third_party/move/move-compiler-v2/src/pipeline/livevar_analysis_processor.rs
+++ b/third_party/move/move-compiler-v2/src/pipeline/livevar_analysis_processor.rs
@@ -198,9 +198,7 @@ impl FunctionTargetProcessor for LiveVarAnalysisProcessor {
 impl LiveVarAnalysisProcessor {
     /// Create a new instance of live variable analysis.
     /// `track_all_usages` determines whether both primary and secondary usages of a variable are
-    /// tracked (when true), or only the primary usages (when false). Also, if set, all usages
-    /// of temporaries in specifications are tracked, which are considered as secondary because
-    /// they are not part of the execution semantics.
+    /// tracked (when true), or only the primary usages (when false).
     /// Unless all usages are needed, it is recommended to set `track_all_usages` to false.
     pub fn new(track_all_usages: bool) -> Self {
         Self { track_all_usages }
@@ -373,14 +371,22 @@ impl<'a> TransferFunctions for LiveVarAnalysis<'a> {
             Branch(id, _, _, src) => {
                 state.insert_or_update(*src, self.livevar_info(id, offset), self.track_all_usages);
             },
-            Prop(id, _, exp) if self.track_all_usages => {
+            Prop(id, _, exp) => {
                 for idx in exp.used_temporaries() {
-                    state.insert_or_update(idx, self.livevar_info(id, offset), true);
+                    state.insert_or_update(
+                        idx,
+                        self.livevar_info(id, offset),
+                        self.track_all_usages,
+                    );
                 }
             },
-            SpecBlock(id, spec) if self.track_all_usages => {
+            SpecBlock(id, spec) => {
                 for idx in spec.used_temporaries() {
-                    state.insert_or_update(idx, self.livevar_info(id, offset), true);
+                    state.insert_or_update(
+                        idx,
+                        self.livevar_info(id, offset),
+                        self.track_all_usages,
+                    );
                 }
             },
             _ => {},


Test patch:
diff --git a/third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.exp b/third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.exp
new file mode 100644
index 0000000000000..9d0f6f655fbc9
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.exp
@@ -0,0 +1,114 @@
+
+============ disassembled file-format ==================
+// Move bytecode v7
+module c0ffee.m {
+use 0000000000000000000000000000000000000000000000000000000000000001::option;
+use 0000000000000000000000000000000000000000000000000000000000000001::vector;
+
+
+struct T has copy, drop, store {
+	issuer: vector<u8>,
+	version: u64
+}
+struct J has copy, drop, store {
+	variant: u64
+}
+struct S has copy, drop, store {
+	entries: vector<T>
+}
+
+test(Arg0: &mut S, Arg1: vector<u8>): Option<T> /* def_idx: 0 */ {
+L2:	loc0: &vector<T>
+L3:	loc1: bool
+L4:	loc2: u64
+L5:	loc3: u64
+L6:	loc4: u64
+L7:	loc5: &T
+L8:	loc6: &T
+L9:	loc7: u64
+L10:	loc8: bool
+L11:	loc9: u64
+L12:	loc10: Option<T>
+L13:	loc11: Option<T>
+B0:
+	0: CopyLoc[0](Arg0: &mut S)
+	1: ImmBorrowField[0](S.entries: vector<T>)
+	2: StLoc[2](loc0: &vector<T>)
+	3: LdFalse
+	4: StLoc[3](loc1: bool)
+	5: LdU64(0)
+	6: StLoc[4](loc2: u64)
+	7: LdU64(0)
+	8: CopyLoc[2](loc0: &vector<T>)
+	9: VecLen(2)
+	10: StLoc[5](loc3: u64)
+	11: StLoc[6](loc4: u64)
+B1:
+	12: CopyLoc[6](loc4: u64)
+	13: CopyLoc[5](loc3: u64)
+	14: Lt
+	15: BrFalse(41)
+B2:
+	16: CopyLoc[2](loc0: &vector<T>)
+	17: CopyLoc[6](loc4: u64)
+	18: VecImmBorrow(2)
+	19: StLoc[7](loc5: &T)
+	20: MoveLoc[7](loc5: &T)
+	21: StLoc[8](loc6: &T)
+	22: MoveLoc[8](loc6: &T)
+	23: ImmBorrowField[1](T.issuer: vector<u8>)
+	24: ReadRef
+	25: CopyLoc[1](Arg1: vector<u8>)
+	26: Eq
+	27: BrFalse(34)
+B3:
+	28: LdTrue
+	29: StLoc[3](loc1: bool)
+	30: MoveLoc[6](loc4: u64)
+	31: StLoc[4](loc2: u64)
+	32: Branch(43)
+B4:
+	33: Branch(34)
+B5:
+	34: LdU64(1)
+	35: StLoc[9](loc7: u64)
+	36: MoveLoc[6](loc4: u64)
+	37: MoveLoc[9](loc7: u64)
+	38: Add
+	39: StLoc[6](loc4: u64)
+	40: Branch(42)
+B6:
+	41: Branch(43)
+B7:
+	42: Branch(12)
+B8:
+	43: Nop
+	44: MoveLoc[2](loc0: &vector<T>)
+	45: Pop
+	46: MoveLoc[3](loc1: bool)
+	47: StLoc[10](loc8: bool)
+	48: MoveLoc[4](loc2: u64)
+	49: StLoc[11](loc9: u64)
+	50: MoveLoc[10](loc8: bool)
+	51: BrFalse(59)
+B9:
+	52: MoveLoc[0](Arg0: &mut S)
+	53: MutBorrowField[0](S.entries: vector<T>)
+	54: MoveLoc[11](loc9: u64)
+	55: Call vector::remove<T>(&mut vector<T>, u64): T
+	56: Call option::some<T>(T): Option<T>
+	57: StLoc[12](loc10: Option<T>)
+	58: Branch(63)
+B10:
+	59: MoveLoc[0](Arg0: &mut S)
+	60: Pop
+	61: Call option::none<T>(): Option<T>
+	62: StLoc[12](loc10: Option<T>)
+B11:
+	63: MoveLoc[12](loc10: Option<T>)
+	64: StLoc[13](loc11: Option<T>)
+	65: MoveLoc[13](loc11: Option<T>)
+	66: Ret
+}
+}
+============ bytecode verification succeeded ========
diff --git a/third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.move b/third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.move
new file mode 100644
index 0000000000000..687c39ecd04be
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.move
@@ -0,0 +1,54 @@
+module 0xc0ffee::m {
+    use std::vector;
+    use std::option;
+    use std::option::Option;
+
+    struct J has copy, drop, store {
+        variant: u64,
+    }
+
+
+    struct T has copy, drop, store {
+        issuer: vector<u8>,
+        version: u64,
+    }
+
+    struct S has copy, drop, store {
+        entries: vector<T>,
+    }
+
+    public inline fun find<Element>(v: &vector<Element>, f: |&Element|bool): (bool, u64) {
+        let find = false;
+        let found_index = 0;
+        let i = 0;
+        let len = vector::length(v);
+        while (i < len) {
+            if (f(vector::borrow(v, i))) {
+                find = true;
+                found_index = i;
+                break
+            };
+            i = i + 1;
+        };
+        spec {
+            assert find ==> f(v[found_index]);
+        };
+        (find, found_index)
+    }
+
+    fun test(s: &mut S, issuer: vector<u8>): Option<T> {
+        let (found, index) = find(&s.entries, |obj| {
+            let set: &T = obj;
+            set.issuer == issuer
+        });
+
+        let ret = if (found) {
+            option::some(vector::remove(&mut s.entries, index))
+        } else {
+            option::none()
+        };
+
+        ret
+    }
+
+}
diff --git a/third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.opt.exp b/third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.opt.exp
new file mode 100644
index 0000000000000..cce956293c50f
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/file-format-generator/bug_14762.opt.exp
@@ -0,0 +1,100 @@
+
+============ disassembled file-format ==================
+// Move bytecode v7
+module c0ffee.m {
+use 0000000000000000000000000000000000000000000000000000000000000001::option;
+use 0000000000000000000000000000000000000000000000000000000000000001::vector;
+
+
+struct T has copy, drop, store {
+	issuer: vector<u8>,
+	version: u64
+}
+struct J has copy, drop, store {
+	variant: u64
+}
+struct S has copy, drop, store {
+	entries: vector<T>
+}
+
+test(Arg0: &mut S, Arg1: vector<u8>): Option<T> /* def_idx: 0 */ {
+L2:	loc0: &vector<T>
+L3:	loc1: bool
+L4:	loc2: u64
+L5:	loc3: u64
+L6:	loc4: u64
+L7:	loc5: bool
+L8:	loc6: u64
+L9:	loc7: Option<T>
+L10:	loc8: Option<T>
+B0:
+	0: CopyLoc[0](Arg0: &mut S)
+	1: ImmBorrowField[0](S.entries: vector<T>)
+	2: StLoc[2](loc0: &vector<T>)
+	3: LdFalse
+	4: StLoc[3](loc1: bool)
+	5: LdU64(0)
+	6: StLoc[4](loc2: u64)
+	7: LdU64(0)
+	8: StLoc[5](loc3: u64)
+	9: CopyLoc[2](loc0: &vector<T>)
+	10: VecLen(2)
+	11: StLoc[6](loc4: u64)
+B1:
+	12: CopyLoc[5](loc3: u64)
+	13: CopyLoc[6](loc4: u64)
+	14: Lt
+	15: BrFalse(28)
+B2:
+	16: CopyLoc[2](loc0: &vector<T>)
+	17: CopyLoc[5](loc3: u64)
+	18: VecImmBorrow(2)
+	19: ImmBorrowField[1](T.issuer: vector<u8>)
+	20: ReadRef
+	21: CopyLoc[1](Arg1: vector<u8>)
+	22: Eq
+	23: BrFalse(52)
+B3:
+	24: LdTrue
+	25: StLoc[3](loc1: bool)
+	26: MoveLoc[5](loc3: u64)
+	27: StLoc[4](loc2: u64)
+B4:
+	28: Nop
+	29: MoveLoc[2](loc0: &vector<T>)
+	30: Pop
+	31: MoveLoc[3](loc1: bool)
+	32: StLoc[7](loc5: bool)
+	33: MoveLoc[4](loc2: u64)
+	34: StLoc[8](loc6: u64)
+	35: MoveLoc[7](loc5: bool)
+	36: BrFalse(47)
+B5:
+	37: MoveLoc[0](Arg0: &mut S)
+	38: MutBorrowField[0](S.entries: vector<T>)
+	39: MoveLoc[8](loc6: u64)
+	40: Call vector::remove<T>(&mut vector<T>, u64): T
+	41: Call option::some<T>(T): Option<T>
+	42: StLoc[9](loc7: Option<T>)
+B6:
+	43: MoveLoc[9](loc7: Option<T>)
+	44: StLoc[10](loc8: Option<T>)
+	45: MoveLoc[10](loc8: Option<T>)
+	46: Ret
+B7:
+	47: MoveLoc[0](Arg0: &mut S)
+	48: Pop
+	49: Call option::none<T>(): Option<T>
+	50: StLoc[9](loc7: Option<T>)
+	51: Branch(43)
+B8:
+	52: LdU64(1)
+	53: StLoc[8](loc6: u64)
+	54: MoveLoc[5](loc3: u64)
+	55: MoveLoc[8](loc6: u64)
+	56: Add
+	57: StLoc[5](loc3: u64)
+	58: Branch(12)
+}
+}
+============ bytecode verification succeeded ========
diff --git a/third_party/move/move-compiler-v2/transactional-tests/tests/no-v1-comparison/bug_14762.exp b/third_party/move/move-compiler-v2/transactional-tests/tests/no-v1-comparison/bug_14762.exp
new file mode 100644
index 0000000000000..5d92c423f3fd8
--- /dev/null
+++ b/third_party/move/move-compiler-v2/transactional-tests/tests/no-v1-comparison/bug_14762.exp
@@ -0,0 +1,1 @@
+processed 2 tasks
diff --git a/third_party/move/move-compiler-v2/transactional-tests/tests/no-v1-comparison/bug_14762.move b/third_party/move/move-compiler-v2/transactional-tests/tests/no-v1-comparison/bug_14762.move
new file mode 100644
index 0000000000000..eede6c62f227f
--- /dev/null
+++ b/third_party/move/move-compiler-v2/transactional-tests/tests/no-v1-comparison/bug_14762.move
@@ -0,0 +1,79 @@
+//# publish
+module 0x42::m {
+    use std::vector;
+    use std::option;
+    use std::option::Option;
+
+    struct J has copy, drop, store {
+        variant: u64,
+    }
+
+    struct T has copy, drop, store {
+        issuer: vector<u8>,
+        version: u64,
+    }
+
+    struct S has copy, drop, store {
+        entries: vector<T>,
+    }
+
+    public inline fun find<Element>(v: &vector<Element>, f: |&Element|bool): (bool, u64) {
+        let find = false;
+        let found_index = 0;
+        let i = 0;
+        let len = vector::length(v);
+        while (i < len) {
+            if (f(vector::borrow(v, i))) {
+                find = true;
+                found_index = i;
+                break
+            };
+            i = i + 1;
+        };
+        spec {
+            assert find ==> f(v[found_index]);
+        };
+        (find, found_index)
+    }
+
+    fun test(s: &mut S, issuer: vector<u8>): Option<T> {
+        let (found, index) = find(&s.entries, |obj| {
+            let set: &T = obj;
+            set.issuer == issuer
+        });
+
+        let ret = if (found) {
+            option::some(vector::remove(&mut s.entries, index))
+        } else {
+            option::none()
+        };
+
+        ret
+    }
+
+    fun test1() {
+        let t0 = T {
+            issuer: vector[1],
+            version: 1
+        };
+        let t1 = T {
+            issuer: vector[2],
+            version: 0
+        };
+        let s = S {
+            entries: vector[t0, t1]
+        };
+        let opt_t = test(&mut s, vector[0]);
+        assert!(option::is_none(&opt_t), 0);
+        let opt_t = test(&mut s, vector[1]);
+        assert!(option::is_some(&opt_t), 0);
+        assert!(option::borrow(&opt_t).issuer == vector[1], 0);
+        let opt_t = test(&mut s, vector[2]);
+        assert!(option::is_some(&opt_t), 0);
+        assert!(option::borrow(&opt_t).issuer == vector[2], 0);
+
+    }
+
+}
+
+//# run 0x42::m::test1
diff --git a/third_party/move/move-prover/tests/sources/functional/ModifiesErrorTest.v2_exp b/third_party/move/move-prover/tests/sources/functional/ModifiesErrorTest.v2_exp
index a4c827857f788..620e4ee6a4e64 100644
--- a/third_party/move/move-prover/tests/sources/functional/ModifiesErrorTest.v2_exp
+++ b/third_party/move/move-prover/tests/sources/functional/ModifiesErrorTest.v2_exp
@@ -1,64 +1,4 @@
 Move prover returns: exiting with verification errors
-warning: Unused assignment to `x0`. Consider removing or prefixing with an underscore: `_x0`
-   ┌─ tests/sources/functional/ModifiesErrorTest.move:37:18
-   │
-37 │         let x0 = A::read_at(addr2);
-   │                  ^^^^^^^^^^^^^^^^^
-
-warning: Unused assignment to `x1`. Consider removing or prefixing with an underscore: `_x1`
-   ┌─ tests/sources/functional/ModifiesErrorTest.move:40:18
-   │
-40 │         let x1 = A::read_at(addr2);
-   │                  ^^^^^^^^^^^^^^^^^
-
-warning: Unused assignment to `x0`. Consider removing or prefixing with an underscore: `_x0`
-   ┌─ tests/sources/functional/ModifiesErrorTest.move:51:18
-   │
-51 │         let x0 = A::read_at(addr2);
-   │                  ^^^^^^^^^^^^^^^^^
-
-warning: Unused assignment to `x1`. Consider removing or prefixing with an underscore: `_x1`
-   ┌─ tests/sources/functional/ModifiesErrorTest.move:53:18
-   │
-53 │         let x1 = A::read_at(addr2);
-   │                  ^^^^^^^^^^^^^^^^^
-
-warning: Unused assignment to `x0`. Consider removing or prefixing with an underscore: `_x0`
-   ┌─ tests/sources/functional/ModifiesErrorTest.move:64:18
-   │
-64 │         let x0 = A::read_at(addr2);
-   │                  ^^^^^^^^^^^^^^^^^
-
-warning: Unused assignment to `x1`. Consider removing or prefixing with an underscore: `_x1`
-   ┌─ tests/sources/functional/ModifiesErrorTest.move:66:18
-   │
-66 │         let x1 = A::read_at(addr2);
-   │                  ^^^^^^^^^^^^^^^^^
-
-warning: Unused assignment to `x0`. Consider removing or prefixing with an underscore: `_x0`
-   ┌─ tests/sources/functional/ModifiesErrorTest.move:78:18
-   │
-78 │         let x0 = A::read_at(addr2);
-   │                  ^^^^^^^^^^^^^^^^^
-
-warning: Unused assignment to `x1`. Consider removing or prefixing with an underscore: `_x1`
-   ┌─ tests/sources/functional/ModifiesErrorTest.move:80:18
-   │
-80 │         let x1 = A::read_at(addr2);
-   │                  ^^^^^^^^^^^^^^^^^
-
-warning: Unused assignment to `x0`. Consider removing or prefixing with an underscore: `_x0`
-   ┌─ tests/sources/functional/ModifiesErrorTest.move:91:18
-   │
-91 │         let x0 = A::read_at(addr);
-   │                  ^^^^^^^^^^^^^^^^
-
-warning: Unused assignment to `x1`. Consider removing or prefixing with an underscore: `_x1`
-   ┌─ tests/sources/functional/ModifiesErrorTest.move:93:18
-   │
-93 │         let x1 = A::read_at(addr);
-   │                  ^^^^^^^^^^^^^^^^
-
 error: caller does not have permission to modify `B::T` at given address
    ┌─ tests/sources/functional/ModifiesErrorTest.move:38:17
    │
diff --git a/third_party/move/move-prover/tests/sources/functional/ModifiesTest.v2_exp b/third_party/move/move-prover/tests/sources/functional/ModifiesTest.v2_exp
deleted file mode 100644
index 66abe10c08bf4..0000000000000
--- a/third_party/move/move-prover/tests/sources/functional/ModifiesTest.v2_exp
+++ /dev/null
@@ -1,11 +0,0 @@
-warning: Unused assignment to `x0`. Consider removing or prefixing with an underscore: `_x0`
-   ┌─ tests/sources/functional/ModifiesTest.move:67:18
-   │
-67 │         let x0 = A::read_at(addr2);
-   │                  ^^^^^^^^^^^^^^^^^
-
-warning: Unused assignment to `x1`. Consider removing or prefixing with an underscore: `_x1`
-   ┌─ tests/sources/functional/ModifiesTest.move:69:18
-   │
-69 │         let x1 = A::read_at(addr2);
-   │                  ^^^^^^^^^^^^^^^^^
diff --git a/third_party/move/move-prover/tests/sources/functional/bitset.v2_exp b/third_party/move/move-prover/tests/sources/functional/bitset.v2_exp
deleted file mode 100644
index e50ba75b20d2e..0000000000000
--- a/third_party/move/move-prover/tests/sources/functional/bitset.v2_exp
+++ /dev/null
@@ -1,11 +0,0 @@
-warning: Unused assignment to `s2`. Consider removing or prefixing with an underscore: `_s2`
-   ┌─ tests/sources/functional/bitset.move:59:18
-   │
-59 │         let s2 = intersect(s, s);
-   │                  ^^^^^^^^^^^^^^^
-
-warning: Unused assignment to `s3`. Consider removing or prefixing with an underscore: `_s3`
-   ┌─ tests/sources/functional/bitset.move:60:18
-   │
-60 │         let s3 = union(s, s);
-   │                  ^^^^^^^^^^^
diff --git a/third_party/move/move-prover/tests/sources/functional/bitwise_features.v2_exp b/third_party/move/move-prover/tests/sources/functional/bitwise_features.v2_exp
deleted file mode 100644
index 7c523ceea6767..0000000000000
--- a/third_party/move/move-prover/tests/sources/functional/bitwise_features.v2_exp
+++ /dev/null
@@ -1,5 +0,0 @@
-warning: Unused assignment to `old_features`. Consider removing or prefixing with an underscore: `_old_features`
-   ┌─ tests/sources/functional/bitwise_features.move:50:28
-   │
-50 │         let old_features = *features; // ghost var
-   │                            ^^^^^^^^^
diff --git a/third_party/move/move-prover/tests/sources/functional/bug_14762.exp b/third_party/move/move-prover/tests/sources/functional/bug_14762.exp
new file mode 100644
index 0000000000000..4b2683e417420
--- /dev/null
+++ b/third_party/move/move-prover/tests/sources/functional/bug_14762.exp
@@ -0,0 +1,9 @@
+Move prover returns: exiting with model building errors
+error: invalid transfer of references
+   ┌─ tests/sources/functional/bug_14762.move:45:26
+   │
+39 │         let (found, index) = find(&s.entries, |obj| {
+   │                                   ---------- It is still being borrowed by this reference
+   ·
+45 │             option::some(vector::remove(&mut s.entries, index))
+   │                          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Invalid usage of reference as function argument. Cannot transfer a mutable reference that is being borrowed
diff --git a/third_party/move/move-prover/tests/sources/functional/bug_14762.move b/third_party/move/move-prover/tests/sources/functional/bug_14762.move
new file mode 100644
index 0000000000000..b1e1587553120
--- /dev/null
+++ b/third_party/move/move-prover/tests/sources/functional/bug_14762.move
@@ -0,0 +1,69 @@
+module 0x42::m {
+    use std::vector;
+    use std::option;
+    use std::option::Option;
+
+    struct J has copy, drop, store {
+        variant: u64,
+    }
+
+    struct T has copy, drop, store {
+        issuer: vector<u8>,
+        version: u64,
+    }
+
+    struct S has copy, drop, store {
+        entries: vector<T>,
+    }
+
+    public inline fun find<Element>(v: &vector<Element>, f: |&Element|bool): (bool, u64) {
+        let find = false;
+        let found_index = 0;
+        let i = 0;
+        let len = vector::length(v);
+        while (i < len) {
+            if (f(vector::borrow(v, i))) {
+                find = true;
+                found_index = i;
+                break
+            };
+            i = i + 1;
+        };
+        spec {
+            assert find ==> f(v[found_index]);
+        };
+        (find, found_index)
+    }
+
+    fun test(s: &mut S, issuer: vector<u8>): Option<T> {
+        let (found, index) = find(&s.entries, |obj| {
+            let set: &T = obj;
+            set.issuer == issuer
+        });
+
+        let ret = if (found) {
+            option::some(vector::remove(&mut s.entries, index))
+        } else {
+            option::none()
+        };
+
+        ret
+    }
+
+    fun test1() {
+        let t0 = T {
+            issuer: vector[1],
+            version: 1
+        };
+        let t1 = T {
+            issuer: vector[2],
+            version: 0
+        };
+        let s = S {
+            entries: vector[t0, t1]
+        };
+        let _opt_t = test(&mut s, vector[0]);
+
+    }
+
+}
diff --git a/third_party/move/move-prover/tests/sources/functional/inline-lambda.v2_exp b/third_party/move/move-prover/tests/sources/functional/inline-lambda.v2_exp
index a939ef7f0c9c6..4d220149d9a54 100644
--- a/third_party/move/move-prover/tests/sources/functional/inline-lambda.v2_exp
+++ b/third_party/move/move-prover/tests/sources/functional/inline-lambda.v2_exp
@@ -1,16 +1,4 @@
 Move prover returns: exiting with verification errors
-warning: Unused assignment to `r1`. Consider removing or prefixing with an underscore: `_r1`
-   ┌─ tests/sources/functional/inline-lambda.move:11:31
-   │
-11 │         let r1 = apply(0, |v| v >= 0);
-   │                               ^^^^^^
-
-warning: Unused assignment to `r2`. Consider removing or prefixing with an underscore: `_r2`
-   ┌─ tests/sources/functional/inline-lambda.move:16:31
-   │
-16 │         let r2 = apply(0, |v| v != a1 + a2);
-   │                               ^^^^^^^^^^^^
-
 error: unknown assertion failed
   ┌─ tests/sources/functional/inline-lambda.move:5:13
   │
diff --git a/third_party/move/move-prover/tests/sources/functional/inline_fun_simple.v2_exp b/third_party/move/move-prover/tests/sources/functional/inline_fun_simple.v2_exp
index a71d8eee327fb..00f90006edacb 100644
--- a/third_party/move/move-prover/tests/sources/functional/inline_fun_simple.v2_exp
+++ b/third_party/move/move-prover/tests/sources/functional/inline_fun_simple.v2_exp
@@ -1,28 +1,4 @@
 Move prover returns: exiting with verification errors
-warning: Unused assignment to `r1`. Consider removing or prefixing with an underscore: `_r1`
-   ┌─ tests/sources/functional/inline_fun_simple.move:10:32
-   │
-10 │         let r1 = apply(42, |v| v >= 1);
-   │                                ^^^^^^
-
-warning: Unused assignment to `r2`. Consider removing or prefixing with an underscore: `_r2`
-   ┌─ tests/sources/functional/inline_fun_simple.move:15:32
-   │
-15 │         let r2 = apply(43, |v| v <= 2);
-   │                                ^^^^^^
-
-warning: Unused assignment to `r1`. Consider removing or prefixing with an underscore: `_r1`
-   ┌─ tests/sources/functional/inline_fun_simple.move:22:32
-   │
-22 │         let r1 = apply(42, |v| v >= 1);
-   │                                ^^^^^^
-
-warning: Unused assignment to `r2`. Consider removing or prefixing with an underscore: `_r2`
-   ┌─ tests/sources/functional/inline_fun_simple.move:27:31
-   │
-27 │         let r2 = apply(3, |v| v <= 2);
-   │                               ^^^^^^
-
 error: unknown assertion failed
   ┌─ tests/sources/functional/inline_fun_simple.move:4:13
   │
diff --git a/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.v2_exp b/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.v2_exp
index 00ce62137346b..4da1a9c4977ce 100644
--- a/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.v2_exp
+++ b/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.v2_exp
@@ -42,7 +42,6 @@ error: induction case of the loop invariant does not hold
    =     at tests/sources/functional/loops_with_memory_ops.move:80: nested_loop2
    =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
    =         a = <redacted>
-   =         b = <redacted>
    =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
    =     at tests/sources/functional/loops_with_memory_ops.move:85: nested_loop2
    =         <redacted> = <redacted>
diff --git a/third_party/move/move-prover/tests/sources/functional/specs_in_fun.v2_exp b/third_party/move/move-prover/tests/sources/functional/specs_in_fun.v2_exp
index a41ce4e659842..4dc5d49a730b3 100644
--- a/third_party/move/move-prover/tests/sources/functional/specs_in_fun.v2_exp
+++ b/third_party/move/move-prover/tests/sources/functional/specs_in_fun.v2_exp
@@ -1,28 +1,4 @@
 Move prover returns: exiting with verification errors
-warning: Unused assignment to `y`. Consider removing or prefixing with an underscore: `_y`
-   ┌─ tests/sources/functional/specs_in_fun.move:18:9
-   │
-18 │         y = x + 1;
-   │         ^^^^^^^^^
-
-warning: Unused assignment to `z`. Consider removing or prefixing with an underscore: `_z`
-   ┌─ tests/sources/functional/specs_in_fun.move:33:9
-   │
-33 │         z = x + y;
-   │         ^^^^^^^^^
-
-warning: Unused assignment to `y`. Consider removing or prefixing with an underscore: `_y`
-   ┌─ tests/sources/functional/specs_in_fun.move:51:9
-   │
-51 │         y = x + 1;
-   │         ^^^^^^^^^
-
-warning: Unused assignment to `z`. Consider removing or prefixing with an underscore: `_z`
-   ┌─ tests/sources/functional/specs_in_fun.move:66:9
-   │
-66 │         z = x + y;
-   │         ^^^^^^^^^
-
 error: unknown assertion failed
    ┌─ tests/sources/functional/specs_in_fun.move:45:13
    │
diff --git a/third_party/move/move-prover/tests/sources/functional/specs_in_fun_ref.v2_exp b/third_party/move/move-prover/tests/sources/functional/specs_in_fun_ref.v2_exp
deleted file mode 100644
index a7c557355adc9..0000000000000
--- a/third_party/move/move-prover/tests/sources/functional/specs_in_fun_ref.v2_exp
+++ /dev/null
@@ -1,29 +0,0 @@
-warning: Unused assignment to `z`. Consider removing or prefixing with an underscore: `_z`
-   ┌─ tests/sources/functional/specs_in_fun_ref.move:11:9
-   │
-11 │         z = x + y;
-   │         ^^^^^^^^^
-
-warning: Unused assignment to `z`. Consider removing or prefixing with an underscore: `_z`
-   ┌─ tests/sources/functional/specs_in_fun_ref.move:44:9
-   │
-44 │         z = *x + *y;
-   │         ^^^^^^^^^^^
-
-warning: Unused assignment to `vx`. Consider removing or prefixing with an underscore: `_vx`
-   ┌─ tests/sources/functional/specs_in_fun_ref.move:45:18
-   │
-45 │         let vx = *x;
-   │                  ^^
-
-warning: Unused assignment to `vy`. Consider removing or prefixing with an underscore: `_vy`
-   ┌─ tests/sources/functional/specs_in_fun_ref.move:46:18
-   │
-46 │         let vy = *y;
-   │                  ^^
-
-warning: Unused assignment to `fx`. Consider removing or prefixing with an underscore: `_fx`
-   ┌─ tests/sources/functional/specs_in_fun_ref.move:47:18
-   │
-47 │         let fx = freeze(x);
-   │                  ^^^^^^^^^
diff --git a/third_party/move/move-prover/tests/sources/functional/verify_custom_table.v2_exp b/third_party/move/move-prover/tests/sources/functional/verify_custom_table.v2_exp
index 53156854c8c86..a859dc99038f4 100644
--- a/third_party/move/move-prover/tests/sources/functional/verify_custom_table.v2_exp
+++ b/third_party/move/move-prover/tests/sources/functional/verify_custom_table.v2_exp
@@ -1,16 +1,4 @@
 Move prover returns: exiting with verification errors
-warning: Unused assignment to `k`. Consider removing or prefixing with an underscore: `_k`
-    ┌─ tests/sources/functional/verify_custom_table.move:115:22
-    │
-115 │         let (k, v) = table::remove_return_key(&mut t, 2);
-    │                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-
-warning: Unused assignment to `v`. Consider removing or prefixing with an underscore: `_v`
-    ┌─ tests/sources/functional/verify_custom_table.move:115:22
-    │
-115 │         let (k, v) = table::remove_return_key(&mut t, 2);
-    │                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-
 error: post-condition does not hold
    ┌─ tests/sources/functional/verify_custom_table.move:76:9
    │
diff --git a/third_party/move/move-prover/tests/sources/regression/bug_828.v2_exp b/third_party/move/move-prover/tests/sources/regression/bug_828.v2_exp
deleted file mode 100644
index 1632a07cecacd..0000000000000
--- a/third_party/move/move-prover/tests/sources/regression/bug_828.v2_exp
+++ /dev/null
@@ -1,5 +0,0 @@
-warning: Unused assignment to `old_i`. Consider removing or prefixing with an underscore: `_old_i`
-  ┌─ tests/sources/regression/bug_828.move:4:21
-  │
-4 │         let old_i = i;
-  │                     ^