[move-prover] Implement opaque spec var updates.

This completes the implementation of the `update` condition to also work if used in opaque functions.

Closes: aptos-labs#9180

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

@@ -691,9 +691,12 @@ impl<'a> Instrumenter<'a> {
                 self.builder.emit_with(move |id| Prop(id, Assume, exp));
             }
 
-            // Emit `let update` assignments.
+            // Emit `let post` assignments.
             self.emit_lets(&callee_spec, true);
 
+            // Emit spec var updates.
+            self.emit_updates(&callee_spec);
+
             // Emit post conditions as assumptions.
             for (_, cond) in std::mem::take(&mut callee_spec.post) {
                 self.emit_traces(&callee_spec, &cond);
@@ -957,11 +960,19 @@ impl<'a> Instrumenter<'a> {
 
         // Emit specification variable updates. They are generated for both verified and inlined
         // function variants, as the evolution of state updates is always the same.
-        self.emit_updates(spec);
+        let lets_emitted = if !spec.updates.is_empty() {
+            self.emit_lets(spec, true);
+            self.emit_updates(spec);
+            true
+        } else {
+            false
+        };
 
         if self.is_verified() {
-            // Emit `let` bindings.
-            self.emit_lets(spec, true);
+            // Emit `let` bindings if not already emitted.
+            if !lets_emitted {
+                self.emit_lets(spec, true);
+            }
 
             // Emit the negation of all aborts conditions.
             for (loc, abort_cond, _) in &spec.aborts {
@@ -1149,6 +1160,9 @@ fn check_opaque_modifies_completeness(
         if env.is_wellknown_event_handle_type(&Type::Struct(mem.module_id, mem.id, vec![])) {
             continue;
         }
+        if env.get_struct_qid(mem.to_qualified_id()).is_ghost_memory() {
+            continue;
+        }
         let found = target.get_modify_ids().iter().any(|id| mem == id);
         if !found {
             let loc = fun_env.get_spec_loc();

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

@@ -20,51 +20,79 @@ error: post-condition does not hold
    =     at tests/sources/functional/global_vars.move:41
 
 error: precondition does not hold at this call
-   ┌─ tests/sources/functional/global_vars.move:66:9
-   │
-66 │         requires access_verified;
-   │         ^^^^^^^^^^^^^^^^^^^^^^^^^
-   │
-   =     at tests/sources/functional/global_vars.move:74: do_privileged_invalid
-   =         _s = <redacted>
-   =     at tests/sources/functional/global_vars.move:66
+    ┌─ tests/sources/functional/global_vars.move:101:9
+    │
+101 │         requires access_verified;
+    │         ^^^^^^^^^^^^^^^^^^^^^^^^^
+    │
+    =     at tests/sources/functional/global_vars.move:109: do_privileged_invalid
+    =         _s = <redacted>
+    =     at tests/sources/functional/global_vars.move:101
 
 error: post-condition does not hold
-    ┌─ tests/sources/functional/global_vars.move:102:9
+    ┌─ tests/sources/functional/global_vars.move:137:9
     │
-102 │         ensures type_has_property<u64>;
+137 │         ensures type_has_property<u64>;
     │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
     │
-    =     at tests/sources/functional/global_vars.move:98: expect_property_of_u64_invalid
-    =     at tests/sources/functional/global_vars.move:99: expect_property_of_u64_invalid
-    =     at tests/sources/functional/global_vars.move:86: give_property_to
-    =     at tests/sources/functional/global_vars.move:88
-    =     at tests/sources/functional/global_vars.move:100: expect_property_of_u64_invalid
-    =     at tests/sources/functional/global_vars.move:102
+    =     at tests/sources/functional/global_vars.move:133: expect_property_of_u64_invalid
+    =     at tests/sources/functional/global_vars.move:134: expect_property_of_u64_invalid
+    =     at tests/sources/functional/global_vars.move:121: give_property_to
+    =     at tests/sources/functional/global_vars.move:123
+    =     at tests/sources/functional/global_vars.move:135: expect_property_of_u64_invalid
+    =     at tests/sources/functional/global_vars.move:137
 
 error: global memory invariant does not hold
-    ┌─ tests/sources/functional/global_vars.move:114:5
+    ┌─ tests/sources/functional/global_vars.move:174:5
     │
-114 │     invariant global<R>(@0).v <= limit;
+174 │     invariant global<R>(@0).v <= limit;
     │     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
     │
-    =     at tests/sources/functional/global_vars.move:136: limit_change_invalid
+    =     at tests/sources/functional/global_vars.move:196: limit_change_invalid
     =         s = <redacted>
-    =     at tests/sources/functional/global_vars.move:137: limit_change_invalid
-    =     at tests/sources/functional/global_vars.move:116: publish
+    =     at tests/sources/functional/global_vars.move:197: limit_change_invalid
+    =     at tests/sources/functional/global_vars.move:176: publish
     =         s = <redacted>
-    =     at tests/sources/functional/global_vars.move:117: publish
-    =     at tests/sources/functional/global_vars.move:118: publish
-    =     at tests/sources/functional/global_vars.move:138: limit_change_invalid
-    =     at tests/sources/functional/global_vars.move:140
-    =     at tests/sources/functional/global_vars.move:114
+    =     at tests/sources/functional/global_vars.move:177: publish
+    =     at tests/sources/functional/global_vars.move:178: publish
+    =     at tests/sources/functional/global_vars.move:198: limit_change_invalid
+    =     at tests/sources/functional/global_vars.move:200
+    =     at tests/sources/functional/global_vars.move:174
+
+error: post-condition does not hold
+   ┌─ tests/sources/functional/global_vars.move:76:9
+   │
+76 │         ensures sum_of_T == 2;
+   │         ^^^^^^^^^^^^^^^^^^^^^^
+   │
+   =     at tests/sources/functional/global_vars.move:72: opaque_call_add_sub_invalid
+   =     at tests/sources/functional/global_vars.move:73: opaque_call_add_sub_invalid
+   =     at tests/sources/functional/global_vars.move:53
+   =     at tests/sources/functional/global_vars.move:73: opaque_call_add_sub_invalid
+   =     at tests/sources/functional/global_vars.move:62
+   =     at tests/sources/functional/global_vars.move:73: opaque_call_add_sub_invalid
+   =     at tests/sources/functional/global_vars.move:53
+   =     at tests/sources/functional/global_vars.move:74: opaque_call_add_sub_invalid
+   =     at tests/sources/functional/global_vars.move:76
+
+error: post-condition does not hold
+    ┌─ tests/sources/functional/global_vars.move:161:9
+    │
+161 │         ensures type_has_property<u64>;
+    │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+    │
+    =     at tests/sources/functional/global_vars.move:157: opaque_expect_property_of_u64_invalid
+    =     at tests/sources/functional/global_vars.move:158: opaque_expect_property_of_u64_invalid
+    =     at tests/sources/functional/global_vars.move:147
+    =     at tests/sources/functional/global_vars.move:159: opaque_expect_property_of_u64_invalid
+    =     at tests/sources/functional/global_vars.move:161
 
 error: global memory invariant does not hold
-    ┌─ tests/sources/functional/global_vars.move:114:5
+    ┌─ tests/sources/functional/global_vars.move:174:5
     │
-114 │     invariant global<R>(@0).v <= limit;
+174 │     invariant global<R>(@0).v <= limit;
     │     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
     │
-    =     at tests/sources/functional/global_vars.move:128: update_invalid
-    =     at tests/sources/functional/global_vars.move:129: update_invalid
-    =     at tests/sources/functional/global_vars.move:114
+    =     at tests/sources/functional/global_vars.move:188: update_invalid
+    =     at tests/sources/functional/global_vars.move:189: update_invalid
+    =     at tests/sources/functional/global_vars.move:174

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

@@ -1,5 +1,5 @@
+// separate_baseline: no_opaque
 module 0x42::TestGlobalVars {
-
     use Std::Signer;
 
     // ================================================================================
@@ -41,6 +41,41 @@ module 0x42::TestGlobalVars {
         ensures sum_of_T == 2;
     }
 
+    // ================================================================================
+    // Counting (opaque)
+
+    fun opaque_add() acquires T {
+        borrow_global_mut<T>(@0).i = borrow_global_mut<T>(@0).i + 1
+    }
+    spec opaque_add {
+        pragma opaque;
+        modifies global<T>(@0);
+        update sum_of_T = sum_of_T + 1;
+    }
+
+    fun opaque_sub() acquires T {
+        borrow_global_mut<T>(@0).i = borrow_global_mut<T>(@0).i - 1
+    }
+    spec opaque_sub {
+        pragma opaque;
+        modifies global<T>(@0);
+        update sum_of_T = sum_of_T - 1;
+    }
+
+    fun opaque_call_add_sub() acquires T {
+        opaque_add(); opaque_add(); opaque_sub();
+    }
+    spec opaque_call_add_sub {
+        ensures sum_of_T == 1;
+    }
+
+    fun opaque_call_add_sub_invalid() acquires T {
+        opaque_add(); opaque_sub(); opaque_add();
+    }
+    spec opaque_call_add_sub_invalid {
+        ensures sum_of_T == 2;
+    }
+
     // ================================================================================
     // Access Control
 
@@ -102,6 +137,31 @@ module 0x42::TestGlobalVars {
         ensures type_has_property<u64>;
     }
 
+    // ================================================================================
+    // Generic spec vars (opaque)
+
+    fun opaque_give_property_to<X>() {
+    }
+    spec opaque_give_property_to {
+        pragma opaque;
+        update type_has_property<X> = true;
+    }
+
+    fun opaque_expect_property_of_bool() {
+        opaque_give_property_to<bool>();
+    }
+    spec opaque_expect_property_of_bool {
+        ensures type_has_property<bool>;
+    }
+
+    fun opaque_expect_property_of_u64_invalid() {
+        opaque_give_property_to<bool>();
+    }
+    spec opaque_expect_property_of_u64_invalid {
+        ensures type_has_property<u64>;
+    }
+
+
     // ================================================================================
     // Invariants and spec vars
 
@@ -139,7 +199,4 @@ module 0x42::TestGlobalVars {
     spec limit_change_invalid {
         update limit = 1;
     }
-
-    // ================================================================================
-    // TODO: implement and test opaque
 }

language/move-prover/tests/sources/functional/global_vars.no_opaque_exp

@@ -0,0 +1,103 @@
+Move prover returns: exiting with boogie verification errors
+error: post-condition does not hold
+   ┌─ tests/sources/functional/global_vars.move:41:9
+   │
+41 │         ensures sum_of_T == 2;
+   │         ^^^^^^^^^^^^^^^^^^^^^^
+   │
+   =     at tests/sources/functional/global_vars.move:37: call_add_sub_invalid
+   =     at tests/sources/functional/global_vars.move:38: call_add_sub_invalid
+   =     at tests/sources/functional/global_vars.move:17: add
+   =     at tests/sources/functional/global_vars.move:18: add
+   =     at tests/sources/functional/global_vars.move:20
+   =     at tests/sources/functional/global_vars.move:24: sub
+   =     at tests/sources/functional/global_vars.move:25: sub
+   =     at tests/sources/functional/global_vars.move:27
+   =     at tests/sources/functional/global_vars.move:17: add
+   =     at tests/sources/functional/global_vars.move:18: add
+   =     at tests/sources/functional/global_vars.move:20
+   =     at tests/sources/functional/global_vars.move:39: call_add_sub_invalid
+   =     at tests/sources/functional/global_vars.move:41
+
+error: precondition does not hold at this call
+    ┌─ tests/sources/functional/global_vars.move:101:9
+    │
+101 │         requires access_verified;
+    │         ^^^^^^^^^^^^^^^^^^^^^^^^^
+    │
+    =     at tests/sources/functional/global_vars.move:109: do_privileged_invalid
+    =         _s = <redacted>
+    =     at tests/sources/functional/global_vars.move:101
+
+error: post-condition does not hold
+    ┌─ tests/sources/functional/global_vars.move:137:9
+    │
+137 │         ensures type_has_property<u64>;
+    │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+    │
+    =     at tests/sources/functional/global_vars.move:133: expect_property_of_u64_invalid
+    =     at tests/sources/functional/global_vars.move:134: expect_property_of_u64_invalid
+    =     at tests/sources/functional/global_vars.move:121: give_property_to
+    =     at tests/sources/functional/global_vars.move:123
+    =     at tests/sources/functional/global_vars.move:135: expect_property_of_u64_invalid
+    =     at tests/sources/functional/global_vars.move:137
+
+error: global memory invariant does not hold
+    ┌─ tests/sources/functional/global_vars.move:174:5
+    │
+174 │     invariant global<R>(@0).v <= limit;
+    │     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+    │
+    =     at tests/sources/functional/global_vars.move:196: limit_change_invalid
+    =         s = <redacted>
+    =     at tests/sources/functional/global_vars.move:197: limit_change_invalid
+    =     at tests/sources/functional/global_vars.move:176: publish
+    =         s = <redacted>
+    =     at tests/sources/functional/global_vars.move:177: publish
+    =     at tests/sources/functional/global_vars.move:178: publish
+    =     at tests/sources/functional/global_vars.move:198: limit_change_invalid
+    =     at tests/sources/functional/global_vars.move:200
+    =     at tests/sources/functional/global_vars.move:174
+
+error: post-condition does not hold
+   ┌─ tests/sources/functional/global_vars.move:76:9
+   │
+76 │         ensures sum_of_T == 2;
+   │         ^^^^^^^^^^^^^^^^^^^^^^
+   │
+   =     at tests/sources/functional/global_vars.move:72: opaque_call_add_sub_invalid
+   =     at tests/sources/functional/global_vars.move:73: opaque_call_add_sub_invalid
+   =     at tests/sources/functional/global_vars.move:48: opaque_add
+   =     at tests/sources/functional/global_vars.move:49: opaque_add
+   =     at tests/sources/functional/global_vars.move:53
+   =     at tests/sources/functional/global_vars.move:57: opaque_sub
+   =     at tests/sources/functional/global_vars.move:58: opaque_sub
+   =     at tests/sources/functional/global_vars.move:62
+   =     at tests/sources/functional/global_vars.move:48: opaque_add
+   =     at tests/sources/functional/global_vars.move:49: opaque_add
+   =     at tests/sources/functional/global_vars.move:53
+   =     at tests/sources/functional/global_vars.move:74: opaque_call_add_sub_invalid
+   =     at tests/sources/functional/global_vars.move:76
+
+error: post-condition does not hold
+    ┌─ tests/sources/functional/global_vars.move:161:9
+    │
+161 │         ensures type_has_property<u64>;
+    │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+    │
+    =     at tests/sources/functional/global_vars.move:157: opaque_expect_property_of_u64_invalid
+    =     at tests/sources/functional/global_vars.move:158: opaque_expect_property_of_u64_invalid
+    =     at tests/sources/functional/global_vars.move:144: opaque_give_property_to
+    =     at tests/sources/functional/global_vars.move:147
+    =     at tests/sources/functional/global_vars.move:159: opaque_expect_property_of_u64_invalid
+    =     at tests/sources/functional/global_vars.move:161
+
+error: global memory invariant does not hold
+    ┌─ tests/sources/functional/global_vars.move:174:5
+    │
+174 │     invariant global<R>(@0).v <= limit;
+    │     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+    │
+    =     at tests/sources/functional/global_vars.move:188: update_invalid
+    =     at tests/sources/functional/global_vars.move:189: update_invalid
+    =     at tests/sources/functional/global_vars.move:174