From 0099e4ff4dcf866c2d669c742dbfb764c2137e7a Mon Sep 17 00:00:00 2001
From: Meng Xu <mengxu@fb.com>
Date: Wed, 25 Aug 2021 10:16:45 -0700
Subject: [PATCH] [move-prover] add a test case for the asserted/assumed memory
 in usage

Closes: #9019
---
 .../bytecode/tests/usage_analysis/test.exp    | 50 +++++++++++++++++++
 .../bytecode/tests/usage_analysis/test.move   | 10 ++++
 2 files changed, 60 insertions(+)

diff --git a/language/move-prover/bytecode/tests/usage_analysis/test.exp b/language/move-prover/bytecode/tests/usage_analysis/test.exp
index 89841aefb8043..2c69cde587a71 100644
--- 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
index 4bb3e2b5c4bfc..416b4bddb4e47 100644
--- 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();
+    }
 }
 }