[move-prover] data invariant assume and assertion for &mut params

For functions with `&mut` params `s: S`, the data invariant for `S` will
be assumed at function entry (via `Wellformedness` - this is already
done) and re-checked on any write-back to this reference --- this is
newly added in this commit.

This PR is the opposite of PR move-language#783 which does the opposite, i.e., drop
the assumption at the function entry. PR move-language#783 is proposed following the
following guideline:

> Data invariants are only checked when the `&mut` borrow ends. During
> the lifetime of the `&mut` reference, the invariant can be temporarily
> violated and hence, assuming data invariants there can lead to
> inconsistency issues.

In theory, both PR's fix are better than the current practice (which
is essentially assuming without assertion).

However, as the test result in PR move-language#783 shows, the `Options.move` in
`stdlib` heavily relies on the entrypoint assumption that a `&mut
Option` has either 0 or 1 entry in its vector. Therefore, in this
commit, we tighten the conditions where we assert data invariant.

In summary, after this PR, data invariants will be checked:

- on write-backs to local root, arised from `let r = &mut s` where `s`
  is a local variable
- on write-backs to global root, arised from `let r =
  borrow_global_mut<S>(addr)`
- on write-backs to `&mut` parameter.

```move
struct S {
    f: u8
}
spec S {
    invariant f != 0;
}

fun foo(s: &mut S) {
    // spec: assume s.f != 0;

    let r = &mut s.f;
    r = 0;

    // spec: write-back[s.f](r);
    // spec: assert s.f != 0;
}
```

language/documentation/examples/diem-framework/move-packages/experimental/sources/Vote.move

@@ -329,6 +329,7 @@ module ExperimentalFramework::Vote {
         let removed_ballots = vector::empty();
         while ({
             spec {
+                invariant unique_ballots(ballots);
                 invariant no_expired_ballots(ballots, DiemTimestamp::spec_now_seconds(), i);
                 invariant vector_subset(ballots, old(ballot_data).ballots);
                 invariant i <= len(ballots);

language/move-prover/bytecode/src/memory_instrumentation.rs

@@ -273,28 +273,25 @@ impl<'a> Instrumenter<'a> {
 
                 // issue a chain of write-back actions
                 for action in chain {
-                    // decide if we need a pack-ref (i.e., data structure invariant checking)
-                    if matches!(
-                        action.dst,
-                        BorrowNode::LocalRoot(..) | BorrowNode::GlobalRoot(..)
-                    ) {
-                        // On write-back to a root, "pack" the reference i.e. validate all its invariants.
-                        let ty = &self
-                            .builder
-                            .get_target()
-                            .get_local_type(action.src)
-                            .to_owned();
-                        if self.is_pack_ref_ty(ty) {
-                            self.builder.emit_with(|id| {
-                                Bytecode::Call(
-                                    id,
-                                    vec![],
-                                    Operation::PackRefDeep,
-                                    vec![action.src],
-                                    None,
-                                )
-                            });
+                    // decide if we need a pre-writeback pack-ref (i.e., data structure invariant checking)
+                    let pre_writeback_check_opt = match &action.dst {
+                        BorrowNode::LocalRoot(..) | BorrowNode::GlobalRoot(..) => {
+                            // On write-back to a root, "pack" the reference i.e. validate all its invariants.
+                            let target = self.builder.get_target();
+                            let ty = target.get_local_type(action.src);
+                            if self.is_pack_ref_ty(ty) {
+                                Some(action.src)
+                            } else {
+                                None
+                            }
                         }
+                        BorrowNode::Reference(..) => None,
+                        BorrowNode::ReturnPlaceholder(..) => unreachable!("invalid placeholder"),
+                    };
+                    if let Some(idx) = pre_writeback_check_opt {
+                        self.builder.emit_with(|id| {
+                            Bytecode::Call(id, vec![], Operation::PackRefDeep, vec![idx], None)
+                        });
                     }
 
                     // emit the write-back
@@ -308,6 +305,37 @@ impl<'a> Instrumenter<'a> {
                         )
                     });
 
+                    // decide if we need a post-writeback pack-ref (i.e., data structure invariant checking)
+                    let post_writeback_check_opt = match &action.dst {
+                        BorrowNode::Reference(idx) => {
+                            // NOTE: we have an entry-point assumption where a &mut parameter must
+                            // have its data invariants hold. As a result, when we write-back the
+                            // references, we should assert that the data invariant still hold.
+                            //
+                            // This, however, does not apply to &mut references we obtained in the
+                            // function body, i.e., by borrow local or borrow global. These cases
+                            // are handled by the `pre_writeback_check_opt` above.
+                            if *idx < param_count {
+                                let target = self.builder.get_target();
+                                let ty = target.get_local_type(*idx);
+                                if self.is_pack_ref_ty(ty) {
+                                    Some(*idx)
+                                } else {
+                                    None
+                                }
+                            } else {
+                                None
+                            }
+                        }
+                        BorrowNode::LocalRoot(..) | BorrowNode::GlobalRoot(..) => None,
+                        BorrowNode::ReturnPlaceholder(..) => unreachable!("invalid placeholder"),
+                    };
+                    if let Some(idx) = post_writeback_check_opt {
+                        self.builder.emit_with(|id| {
+                            Bytecode::Call(id, vec![], Operation::PackRefDeep, vec![idx], None)
+                        });
+                    }
+
                     // add a trace for written back value if it's a user variable.
                     match action.dst {
                         BorrowNode::LocalRoot(temp) | BorrowNode::Reference(temp) => {

language/move-prover/tests/sources/functional/data_invariant_for_mut_ref_arg.exp

@@ -0,0 +1,24 @@
+Move prover returns: exiting with verification errors
+error: data invariant does not hold
+  ┌─ tests/sources/functional/data_invariant_for_mut_ref_arg.move:8:9
+  │
+8 │         invariant len(v) == 0;
+  │         ^^^^^^^^^^^^^^^^^^^^^^
+  │
+  =     at tests/sources/functional/data_invariant_for_mut_ref_arg.move:15: push_1
+  =         s = <redacted>
+  =     at tests/sources/functional/data_invariant_for_mut_ref_arg.move:17: push_1
+  =     at tests/sources/functional/data_invariant_for_mut_ref_arg.move:19: push_1
+  =     at tests/sources/functional/data_invariant_for_mut_ref_arg.move:8
+
+error: data invariant does not hold
+  ┌─ tests/sources/functional/data_invariant_for_mut_ref_arg.move:8:9
+  │
+8 │         invariant len(v) == 0;
+  │         ^^^^^^^^^^^^^^^^^^^^^^
+  │
+  =     at tests/sources/functional/data_invariant_for_mut_ref_arg.move:22: push_2
+  =         s = <redacted>
+  =     at tests/sources/functional/data_invariant_for_mut_ref_arg.move:24: push_2
+  =     at tests/sources/functional/data_invariant_for_mut_ref_arg.move:26: push_2
+  =     at tests/sources/functional/data_invariant_for_mut_ref_arg.move:8

language/move-prover/tests/sources/functional/data_invariant_for_mut_ref_arg.move

@@ -0,0 +1,30 @@
+module 0x42::struct_invariant_mut_ref_param {
+    use std::vector;
+
+    struct S {
+        v: vector<u64>,
+    }
+    spec S {
+        invariant len(v) == 0;
+    }
+
+    public fun empty(): S {
+        S { v: vector::empty<u64>() }
+    }
+
+    public fun push_1(s: &mut S) {
+        spec {
+            assert len(s.v) == 0;
+        };
+        vector::push_back(&mut s.v, 1);
+    }
+
+    public fun push_2(s: &mut S) {
+        spec {
+            assert len(s.v) == 0;
+        };
+        vector::push_back(&mut s.v, 2);
+        let t = freeze(s);
+        let _ = vector::length(&t.v);
+    }
+}

language/move-prover/tests/sources/functional/mut_ref.exp

@@ -36,6 +36,8 @@ error: data invariant does not hold
   =     at tests/sources/functional/mut_ref.move:91: return_ref_different_path_vec2
   =         result = <redacted>
   =         x = <redacted>
+  =         x = <redacted>
+  =         x = <redacted>
   =     at tests/sources/functional/mut_ref.move:92: return_ref_different_path_vec2
   =         r = <redacted>
   =     at tests/sources/functional/mut_ref.move:122: call_return_ref_different_path_vec2_incorrect