high-level spec for resource account (aptos-labs#9033)

Author: rahxephon89

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

@@ -418,6 +418,7 @@ the SignerCapability.
 <b>include</b> <a href="aptos_account.md#0x1_aptos_account_GuidAbortsIf">aptos_account::GuidAbortsIf</a>&lt;AptosCoin&gt;{<b>to</b>: resource_addr};
 <b>include</b> <a href="resource_account.md#0x1_resource_account_RotateAccountAuthenticationKeyAndStoreCapabilityAbortsIfWithoutAccountLimit">RotateAccountAuthenticationKeyAndStoreCapabilityAbortsIfWithoutAccountLimit</a>;
 <b>aborts_if</b> <a href="coin.md#0x1_coin_is_account_registered">coin::is_account_registered</a>&lt;AptosCoin&gt;(resource_addr) && coin_store_resource.frozen;
+<b>ensures</b> <b>exists</b>&lt;aptos_framework::coin::CoinStore&lt;AptosCoin&gt;&gt;(resource_addr);
 </code></pre>
 
 
@@ -455,6 +456,9 @@ the SignerCapability.
 
 <pre><code><b>let</b> resource_addr = <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(resource);
 <b>include</b> <a href="resource_account.md#0x1_resource_account_RotateAccountAuthenticationKeyAndStoreCapabilityAbortsIf">RotateAccountAuthenticationKeyAndStoreCapabilityAbortsIf</a>;
+<b>ensures</b> <b>exists</b>&lt;<a href="resource_account.md#0x1_resource_account_Container">Container</a>&gt;(<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(origin));
+<b>ensures</b> <a href="../../aptos-stdlib/../move-stdlib/doc/vector.md#0x1_vector_length">vector::length</a>(optional_auth_key) != 0 ==&gt;
+    <b>global</b>&lt;aptos_framework::account::Account&gt;(resource_addr).authentication_key == optional_auth_key;
 </code></pre>
 
 
@@ -516,9 +520,11 @@ the SignerCapability.
 
 <pre><code><b>aborts_if</b> !<b>exists</b>&lt;<a href="resource_account.md#0x1_resource_account_Container">Container</a>&gt;(source_addr);
 <b>let</b> resource_addr = <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(resource);
-<b>let</b> container = <b>borrow_global_mut</b>&lt;<a href="resource_account.md#0x1_resource_account_Container">Container</a>&gt;(source_addr);
+<b>let</b> container = <b>global</b>&lt;<a href="resource_account.md#0x1_resource_account_Container">Container</a>&gt;(source_addr);
 <b>aborts_if</b> !<a href="../../aptos-stdlib/doc/simple_map.md#0x1_simple_map_spec_contains_key">simple_map::spec_contains_key</a>(container.store, resource_addr);
 <b>aborts_if</b> !<b>exists</b>&lt;<a href="account.md#0x1_account_Account">account::Account</a>&gt;(resource_addr);
+<b>ensures</b> <a href="../../aptos-stdlib/doc/simple_map.md#0x1_simple_map_spec_contains_key">simple_map::spec_contains_key</a>(<b>old</b>(<b>global</b>&lt;<a href="resource_account.md#0x1_resource_account_Container">Container</a>&gt;(source_addr)).store, resource_addr) &&
+<a href="../../aptos-stdlib/doc/simple_map.md#0x1_simple_map_spec_len">simple_map::spec_len</a>(<b>old</b>(<b>global</b>&lt;<a href="resource_account.md#0x1_resource_account_Container">Container</a>&gt;(source_addr)).store) == 1 ==&gt; !<b>exists</b>&lt;<a href="resource_account.md#0x1_resource_account_Container">Container</a>&gt;(source_addr);
 </code></pre>
 
 

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

@@ -31,6 +31,7 @@ spec aptos_framework::resource_account {
 
         //coin property
         aborts_if coin::is_account_registered<AptosCoin>(resource_addr) && coin_store_resource.frozen;
+        ensures exists<aptos_framework::coin::CoinStore<AptosCoin>>(resource_addr);
     }
 
     spec create_resource_account_and_publish_package(
@@ -55,6 +56,9 @@ spec aptos_framework::resource_account {
     ) {
         let resource_addr = signer::address_of(resource);
         include RotateAccountAuthenticationKeyAndStoreCapabilityAbortsIf;
+        ensures exists<Container>(signer::address_of(origin));
+        ensures vector::length(optional_auth_key) != 0 ==>
+            global<aptos_framework::account::Account>(resource_addr).authentication_key == optional_auth_key;
     }
 
     spec schema RotateAccountAuthenticationKeyAndStoreCapabilityAbortsIf {
@@ -101,8 +105,10 @@ spec aptos_framework::resource_account {
         aborts_if !exists<Container>(source_addr);
         let resource_addr = signer::address_of(resource);
 
-        let container = borrow_global_mut<Container>(source_addr);
+        let container = global<Container>(source_addr);
         aborts_if !simple_map::spec_contains_key(container.store, resource_addr);
         aborts_if !exists<account::Account>(resource_addr);
+        ensures simple_map::spec_contains_key(old(global<Container>(source_addr)).store, resource_addr) &&
+        simple_map::spec_len(old(global<Container>(source_addr)).store) == 1 ==> !exists<Container>(source_addr);
     }
 }