update prover tests

aptos-labs · Oct 1, 2024 · 76ad6f0 · 76ad6f0
1 parent cad200d
commit 76ad6f0
Show file tree

Hide file tree

Showing 6 changed files with 17 additions and 9 deletions.
diff --git a/aptos-move/framework/aptos-framework/doc/object.md b/aptos-move/framework/aptos-framework/doc/object.md
@@ -3319,7 +3319,12 @@ to determine the identity of the starting point of ownership.
 
 
 
-<pre><code><b>pragma</b> verify = <b>false</b>;
+<pre><code><b>pragma</b> aborts_if_is_partial;
+<b>let</b> object_address = <a href="object.md#0x1_object">object</a>.inner;
+<b>aborts_if</b> !<b>exists</b>&lt;<a href="object.md#0x1_object_ObjectCore">ObjectCore</a>&gt;(object_address);
+<b>aborts_if</b> <a href="object.md#0x1_object_owner">owner</a>(<a href="object.md#0x1_object">object</a>) != <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(owner);
+<b>aborts_if</b> <a href="object.md#0x1_object_is_burnt">is_burnt</a>(<a href="object.md#0x1_object">object</a>);
+<b>ensures</b> <b>global</b>&lt;<a href="object.md#0x1_object_ObjectCore">ObjectCore</a>&gt;(<a href="object.md#0x1_object">object</a>.inner).owner == <a href="object.md#0x1_object_BURN_ADDRESS">BURN_ADDRESS</a>;
 </code></pre>
 
 

diff --git a/aptos-move/framework/aptos-framework/sources/object.spec.move b/aptos-move/framework/aptos-framework/sources/object.spec.move
@@ -483,7 +483,12 @@ spec aptos_framework::object {
     }
 
     spec burn<T: key>(owner: &signer, object: Object<T>) {
-        pragma verify = false;
+        pragma aborts_if_is_partial;
+        let object_address = object.inner;
+        aborts_if !exists<ObjectCore>(object_address);
+        aborts_if owner(object) != signer::address_of(owner);
+        aborts_if is_burnt(object);
+        ensures global<ObjectCore>(object.inner).owner == BURN_ADDRESS;
     }
 
     spec unburn<T: key>(original_owner: &signer, object: Object<T>) {

diff --git a/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.exp b/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.exp
@@ -104,8 +104,8 @@ error: unknown assertion failed
    =     at tests/sources/functional/loops_with_memory_ops.move:80: nested_loop2
    =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
    =         b = <redacted>
-   =         a = <redacted>
    =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
+   =         a = <redacted>
    =     at tests/sources/functional/loops_with_memory_ops.move:85: nested_loop2
    =         i = <redacted>
    =     at tests/sources/functional/loops_with_memory_ops.move:86: nested_loop2

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
@@ -42,8 +42,8 @@ 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
+   =         b = <redacted>
    =     at tests/sources/functional/loops_with_memory_ops.move:85: nested_loop2
    =         <redacted> = <redacted>
    =         i = <redacted>
@@ -100,8 +100,6 @@ error: unknown assertion failed
    =     at tests/sources/functional/loops_with_memory_ops.move:75: nested_loop2
    =     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>
-   =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
    =         b = <redacted>
    =     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/trace.exp b/third_party/move/move-prover/tests/sources/functional/trace.exp
@@ -47,7 +47,7 @@ error: post-condition does not hold
    │
    = Related Global Memory:
    =         Resource name: TestTracing_R
-   =         Values:  {Address(18467): <redacted>, Default: TestTracing.R{x = 4}}
+   =         Values:  {Address(6334): <redacted>, Default: empty}
    = Related Bindings:
    =         addr = <redacted>
    =         exists<R>(addr) = <redacted>
@@ -74,7 +74,7 @@ error: global memory invariant does not hold
    │
    = Related Global Memory:
    =         Resource name: TestTracing_R
-   =         Values:  {Address(0): <redacted>, Default: TestTracing.R{x = 5}}
+   =         Values:  {Address(0): <redacted>, Default: empty}
    =     at tests/sources/functional/trace.move:29: publish_invalid
    =     at tests/sources/functional/trace.move:33: publish_invalid (spec)
    =         `let addr = signer::address_of(s);` = <redacted>

diff --git a/third_party/move/move-prover/tests/sources/functional/trace.v2_exp b/third_party/move/move-prover/tests/sources/functional/trace.v2_exp
@@ -47,7 +47,7 @@ error: post-condition does not hold
    │
    = Related Global Memory:
    =         Resource name: TestTracing_R
-   =         Values:  {Address(18467): <redacted>, Default: empty}
+   =         Values:  {Address(6334): <redacted>, Default: empty}
    = Related Bindings:
    =         addr = <redacted>
    =         exists<R>(addr) = <redacted>