modify signer prelude

aptos-move/framework/aptos-framework/doc/object.md

@@ -3471,7 +3471,8 @@ to determine the identity of the starting point of ownership.
 
 
 
-<pre><code><b>aborts_if</b> !<a href="permissioned_signer.md#0x1_permissioned_signer_spec_is_permissioned_signer">permissioned_signer::spec_is_permissioned_signer</a>(<a href="permissioned_signer.md#0x1_permissioned_signer">permissioned_signer</a>);
+<pre><code><b>pragma</b> aborts_if_is_partial;
+<b>aborts_if</b> !<a href="permissioned_signer.md#0x1_permissioned_signer_spec_is_permissioned_signer">permissioned_signer::spec_is_permissioned_signer</a>(<a href="permissioned_signer.md#0x1_permissioned_signer">permissioned_signer</a>);
 <b>aborts_if</b> <a href="permissioned_signer.md#0x1_permissioned_signer_spec_is_permissioned_signer">permissioned_signer::spec_is_permissioned_signer</a>(master);
 <b>aborts_if</b> <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(master) != <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(<a href="permissioned_signer.md#0x1_permissioned_signer">permissioned_signer</a>);
 </code></pre>

aptos-move/framework/aptos-framework/doc/permissioned_signer.md

@@ -1223,7 +1223,11 @@ signer::address_of(master) == signer::address_of(signer_from_permissioned(create
 
 
 
-<pre><code><b>pragma</b> verify = <b>false</b>;
+<pre><code><b>pragma</b> aborts_if_is_partial;
+<b>aborts_if</b> !<a href="permissioned_signer.md#0x1_permissioned_signer_spec_is_permissioned_signer">spec_is_permissioned_signer</a>(permissioned);
+<b>aborts_if</b> <a href="permissioned_signer.md#0x1_permissioned_signer_spec_is_permissioned_signer">spec_is_permissioned_signer</a>(master);
+<b>aborts_if</b> <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(permissioned) != <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(master);
+<b>ensures</b> <b>exists</b>&lt;<a href="permissioned_signer.md#0x1_permissioned_signer_PermStorage">PermStorage</a>&gt;(<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(<a href="permissioned_signer.md#0x1_permissioned_signer_spec_permission_signer">spec_permission_signer</a>(permissioned)));
 </code></pre>
 
 

aptos-move/framework/aptos-framework/sources/object.spec.move

@@ -50,6 +50,7 @@ spec aptos_framework::object {
     }
 
     spec grant_permission {
+        pragma aborts_if_is_partial;
         aborts_if !permissioned_signer::spec_is_permissioned_signer(permissioned_signer);
         aborts_if permissioned_signer::spec_is_permissioned_signer(master);
         aborts_if signer::address_of(master) != signer::address_of(permissioned_signer);

aptos-move/framework/aptos-framework/sources/permissioned_signer.spec.move

@@ -82,28 +82,22 @@ spec aptos_framework::permissioned_signer {
     capacity: u256,
     perm: PermKey
     ) {
-        pragma verify = false;
-        // TODO: cannot verify this because the native implementation of signer
-        // in boogie is defined as a wrapper of an address so that,
-        // if signer::address_of(permissioned) == signer::address_of(master)
-        // then permissioned == master.
-
-        // use aptos_std::type_info;
-        // use std::bcs;
-        // aborts_if !spec_is_permissioned_signer(permissioned);
-        // aborts_if spec_is_permissioned_signer(master);
-        // let permission_signer_addr = signer::address_of(permissioned);
-        // let master_addr = signer::address_of(master);
-        // aborts_if permission_signer_addr != master_addr;
-        // ensures exists<PermStorage>(permission_signer_addr);
+
+        use aptos_std::type_info;
+        use std::bcs;
+        pragma aborts_if_is_partial;
+        aborts_if !spec_is_permissioned_signer(permissioned);
+        aborts_if spec_is_permissioned_signer(master);
+        aborts_if signer::address_of(permissioned) != signer::address_of(master);
+        ensures exists<PermStorage>(signer::address_of(spec_permission_signer(permissioned)));
         // let perms = global<PermStorage>(permission_signer_addr).perms;
         // let post post_perms = global<PermStorage>(permission_signer_addr).perms;
         // let key = Any {
         //     type_name: type_info::type_name<SmartTable<Any, u256>>(),
         //     data: bcs::serialize(perm)
         // };
-        // // ensures smart_table::spec_contains(perms, key) ==>
-        // //     smart_table::spec_get(post_perms, key) == old(smart_table::spec_get(perms, key)) + capacity;
+        // ensures smart_table::spec_contains(perms, key) ==>
+        //     smart_table::spec_get(post_perms, key) == old(smart_table::spec_get(perms, key)) + capacity;
         // ensures !smart_table::spec_contains(perms, key) ==>
         //     smart_table::spec_get(post_perms, key) == capacity;
     }

third_party/move/move-prover/boogie-backend/src/prelude/prelude.bpl

@@ -1090,13 +1090,25 @@ procedure {:inline 1} $1_Account_create_signer(
 // Native Signer
 
 datatype $signer {
-    $signer($addr: int)
+    $signer($addr: int),
+    $permissioned_signer($addr: int, $permission_addr: int)
 }
+
 function {:inline} $IsValid'signer'(s: $signer): bool {
-    $IsValid'address'(s->$addr)
+    if s is $signer then
+        $IsValid'address'(s->$addr)
+    else
+        $IsValid'address'(s->$addr) &&
+        $IsValid'address'(s->$permission_addr)
 }
+
 function {:inline} $IsEqual'signer'(s1: $signer, s2: $signer): bool {
-    s1 == s2
+    if s1 is $signer && s2 is $signer then
+        s1 == s2
+    else if s1 is $permissioned_signer && s2 is $permissioned_signer then
+        s1 == s2
+    else
+        false
 }
 
 procedure {:inline 1} $1_signer_borrow_address(signer: $signer) returns (res: int) {