[move-prover] add a test case for the asserted/assumed memory in usage

Closes: aptos-labs#9019
GS- · Aug 25, 2021 · 0099e4f · 0099e4f
1 parent 4f3e5f2
commit 0099e4f
Show file tree

Hide file tree

Showing 2 changed files with 60 additions and 0 deletions.
diff --git a/language/move-prover/bytecode/tests/usage_analysis/test.exp b/language/move-prover/bytecode/tests/usage_analysis/test.exp
@@ -15,6 +15,21 @@ public fun Test::update<#0>($t0|x: #0) {
 }
 
 
+[variant baseline]
+public fun Test::assert_assume_memory() {
+  0: assume exists<Test::A<bool, u64>>(1)
+  1: assert exists<Test::A<u64, bool>>(1)
+  2: return ()
+}
+
+
+[variant baseline]
+public fun Test::call_assert_assume_memory() {
+  0: Test::assert_assume_memory()
+  1: return ()
+}
+
+
 [variant baseline]
 public fun Test::publish<#0>($t0|signer: &signer, $t1|x: Test::A<#0, u8>) {
      var $t2: &signer
@@ -76,6 +91,21 @@ public fun Test::update<#0>($t0|x: #0) {
 }
 
 
+[variant baseline]
+public fun Test::assert_assume_memory() {
+  0: assume exists<Test::A<bool, u64>>(1)
+  1: assert exists<Test::A<u64, bool>>(1)
+  2: return ()
+}
+
+
+[variant baseline]
+public fun Test::call_assert_assume_memory() {
+  0: Test::assert_assume_memory()
+  1: return ()
+}
+
+
 [variant baseline]
 public fun Test::publish<#0>($t0|signer: &signer, $t1|x: Test::A<#0, u8>) {
      var $t2: &signer
@@ -135,6 +165,26 @@ function Test::update [baseline] {
   asserted = {}
   directly asserted = {}
 }
+function Test::assert_assume_memory [baseline] {
+  accessed = {}
+  directly accessed = {}
+  modified = {}
+  directly modified = {}
+  assumed = {Test::A<bool, u64>}
+  directly assumed = {Test::A<bool, u64>}
+  asserted = {Test::A<u64, bool>}
+  directly asserted = {Test::A<u64, bool>}
+}
+function Test::call_assert_assume_memory [baseline] {
+  accessed = {}
+  directly accessed = {}
+  modified = {}
+  directly modified = {}
+  assumed = {Test::A<bool, u64>}
+  directly assumed = {}
+  asserted = {Test::A<u64, bool>}
+  directly asserted = {}
+}
 function Test::publish [baseline] {
   accessed = {Test::A<#0, u8>}
   directly accessed = {Test::A<#0, u8>}

diff --git a/language/move-prover/bytecode/tests/usage_analysis/test.move b/language/move-prover/bytecode/tests/usage_analysis/test.move
@@ -25,5 +25,15 @@ module Test {
     public fun publish<T: store>(signer: &signer, x: A<T, u8>) {
         move_to<A<T, u8>>(signer, x)
     }
+
+    public fun assert_assume_memory() {
+        spec {
+            assume exists<A<bool, u64>>(@0x1);
+            assert exists<A<u64, bool>>(@0x1);
+        };
+    }
+    public fun call_assert_assume_memory() {
+        assert_assume_memory();
+    }
 }
 }