Rename assert_account_is_registered_for_apt to assert_account_is_re…

…gistered_for_supra

aptos-move/framework/supra-framework/doc/overview.md

@@ -1,5 +1,5 @@
 
-<a id="@Aptos_Framework_0"></a>
+<a id="@Supra_Framework_0"></a>
 
 # Supra Framework
 

aptos-move/framework/supra-framework/doc/supra_account.md

@@ -16,7 +16,7 @@
 -  [Function `transfer_coins`](#0x1_supra_account_transfer_coins)
 -  [Function `deposit_coins`](#0x1_supra_account_deposit_coins)
 -  [Function `assert_account_exists`](#0x1_supra_account_assert_account_exists)
--  [Function `assert_account_is_registered_for_apt`](#0x1_supra_account_assert_account_is_registered_for_apt)
+-  [Function `assert_account_is_registered_for_supra`](#0x1_supra_account_assert_account_is_registered_for_supra)
 -  [Function `set_allow_direct_coin_transfers`](#0x1_supra_account_set_allow_direct_coin_transfers)
 -  [Function `can_receive_direct_coin_transfers`](#0x1_supra_account_can_receive_direct_coin_transfers)
 -  [Function `register_supra`](#0x1_supra_account_register_supra)
@@ -35,7 +35,7 @@
     -  [Function `transfer_coins`](#@Specification_1_transfer_coins)
     -  [Function `deposit_coins`](#@Specification_1_deposit_coins)
     -  [Function `assert_account_exists`](#@Specification_1_assert_account_exists)
-    -  [Function `assert_account_is_registered_for_apt`](#@Specification_1_assert_account_is_registered_for_apt)
+    -  [Function `assert_account_is_registered_for_supra`](#@Specification_1_assert_account_is_registered_for_supra)
     -  [Function `set_allow_direct_coin_transfers`](#@Specification_1_set_allow_direct_coin_transfers)
     -  [Function `can_receive_direct_coin_transfers`](#@Specification_1_can_receive_direct_coin_transfers)
     -  [Function `register_supra`](#@Specification_1_register_supra)
@@ -437,13 +437,13 @@ This would create the recipient account first and register it to receive the Coi
 
 </details>
 
-<a id="0x1_supra_account_assert_account_is_registered_for_apt"></a>
+<a id="0x1_supra_account_assert_account_is_registered_for_supra"></a>
 
-## Function `assert_account_is_registered_for_apt`
+## Function `assert_account_is_registered_for_supra`
 
 
 
-<pre><code><b>public</b> <b>fun</b> <a href="supra_account.md#0x1_supra_account_assert_account_is_registered_for_apt">assert_account_is_registered_for_apt</a>(addr: <b>address</b>)
+<pre><code><b>public</b> <b>fun</b> <a href="supra_account.md#0x1_supra_account_assert_account_is_registered_for_supra">assert_account_is_registered_for_supra</a>(addr: <b>address</b>)
 </code></pre>
 
 
@@ -452,7 +452,7 @@ This would create the recipient account first and register it to receive the Coi
 <summary>Implementation</summary>
 
 
-<pre><code><b>public</b> <b>fun</b> <a href="supra_account.md#0x1_supra_account_assert_account_is_registered_for_apt">assert_account_is_registered_for_apt</a>(addr: <b>address</b>) {
+<pre><code><b>public</b> <b>fun</b> <a href="supra_account.md#0x1_supra_account_assert_account_is_registered_for_supra">assert_account_is_registered_for_supra</a>(addr: <b>address</b>) {
     <a href="supra_account.md#0x1_supra_account_assert_account_exists">assert_account_exists</a>(addr);
     <b>assert</b>!(<a href="coin.md#0x1_coin_is_account_registered">coin::is_account_registered</a>&lt;SupraCoin&gt;(addr), <a href="../../aptos-stdlib/../move-stdlib/doc/error.md#0x1_error_not_found">error::not_found</a>(<a href="supra_account.md#0x1_supra_account_EACCOUNT_NOT_REGISTERED_FOR_APT">EACCOUNT_NOT_REGISTERED_FOR_APT</a>));
 }
@@ -745,15 +745,15 @@ Address of SUPRA Primary Fungible Store
 
 <tr>
 <td>1</td>
-<td>During the creation of an Supra account the following rules should hold: (1) the authentication key should be 32 bytes in length, (2) an Supra account should not already exist for that authentication key, and (3) the address of the authentication key should not be equal to a reserved address (0x0, 0x1, or 0x3).</td>
+<td>During the creation of an Aptos account the following rules should hold: (1) the authentication key should be 32 bytes in length, (2) an Aptos account should not already exist for that authentication key, and (3) the address of the authentication key should not be equal to a reserved address (0x0, 0x1, or 0x3).</td>
 <td>Critical</td>
 <td>The authentication key which is passed in as an argument to create_account should satisfy all necessary conditions.</td>
 <td>Formally verified via <a href="#high-level-req-1">CreateAccountAbortsIf</a>.</td>
 </tr>
 
 <tr>
 <td>2</td>
-<td>After creating an Supra account, the account should become registered to receive SupraCoin.</td>
+<td>After creating an Aptos account, the account should become registered to receive SupraCoin.</td>
 <td>Critical</td>
 <td>The create_account function creates a new account for the particular address and registers SupraCoin.</td>
 <td>Formally verified via <a href="#high-level-req-2">create_account</a>.</td>
@@ -793,7 +793,7 @@ Address of SUPRA Primary Fungible Store
 
 <tr>
 <td>7</td>
-<td>When performing a batch transfer of Supra Coin and/or a batch transfer of a custom coin type, it should ensure that the vector containing destination addresses and the vector containing the corresponding amounts are equal in length.</td>
+<td>When performing a batch transfer of Aptos Coin and/or a batch transfer of a custom coin type, it should ensure that the vector containing destination addresses and the vector containing the corresponding amounts are equal in length.</td>
 <td>Low</td>
 <td>The batch_transfer and batch_transfer_coins functions verify that the length of the recipient addresses vector matches the length of the amount vector through an assertion.</td>
 <td>Formally verified via <a href="#high-level-req-7">batch_transfer_coins</a>.</td>
@@ -1048,12 +1048,12 @@ Limit the address of auth_key is not @vm_reserved / @supra_framework / @aptos_to
 
 
 
-<a id="@Specification_1_assert_account_is_registered_for_apt"></a>
+<a id="@Specification_1_assert_account_is_registered_for_supra"></a>
 
-### Function `assert_account_is_registered_for_apt`
+### Function `assert_account_is_registered_for_supra`
 
 
-<pre><code><b>public</b> <b>fun</b> <a href="supra_account.md#0x1_supra_account_assert_account_is_registered_for_apt">assert_account_is_registered_for_apt</a>(addr: <b>address</b>)
+<pre><code><b>public</b> <b>fun</b> <a href="supra_account.md#0x1_supra_account_assert_account_is_registered_for_supra">assert_account_is_registered_for_supra</a>(addr: <b>address</b>)
 </code></pre>
 
 

aptos-move/framework/supra-framework/doc/vesting.md

@@ -2166,7 +2166,7 @@ Create a vesting contract with a given configurations.
         !<a href="system_addresses.md#0x1_system_addresses_is_reserved_address">system_addresses::is_reserved_address</a>(withdrawal_address),
         <a href="../../aptos-stdlib/../move-stdlib/doc/error.md#0x1_error_invalid_argument">error::invalid_argument</a>(<a href="vesting.md#0x1_vesting_EINVALID_WITHDRAWAL_ADDRESS">EINVALID_WITHDRAWAL_ADDRESS</a>),
     );
-    assert_account_is_registered_for_apt(withdrawal_address);
+    assert_account_is_registered_for_supra(withdrawal_address);
     <b>assert</b>!(<a href="../../aptos-stdlib/../move-stdlib/doc/vector.md#0x1_vector_length">vector::length</a>(shareholders) &gt; 0, <a href="../../aptos-stdlib/../move-stdlib/doc/error.md#0x1_error_invalid_argument">error::invalid_argument</a>(<a href="vesting.md#0x1_vesting_ENO_SHAREHOLDERS">ENO_SHAREHOLDERS</a>));
     <b>assert</b>!(
         <a href="../../aptos-stdlib/doc/simple_map.md#0x1_simple_map_length">simple_map::length</a>(&buy_ins) == <a href="../../aptos-stdlib/../move-stdlib/doc/vector.md#0x1_vector_length">vector::length</a>(shareholders),
@@ -2907,7 +2907,7 @@ has already been terminated.
 ) <b>acquires</b> <a href="vesting.md#0x1_vesting_VestingContract">VestingContract</a> {
     // Verify that the beneficiary <a href="account.md#0x1_account">account</a> is set up <b>to</b> receive SUPRA. This is a requirement so <a href="vesting.md#0x1_vesting_distribute">distribute</a>() wouldn't
     // fail and <a href="block.md#0x1_block">block</a> all other accounts from receiving SUPRA <b>if</b> one beneficiary is not registered.
-    assert_account_is_registered_for_apt(new_beneficiary);
+    assert_account_is_registered_for_supra(new_beneficiary);
 
     <b>let</b> vesting_contract = <b>borrow_global_mut</b>&lt;<a href="vesting.md#0x1_vesting_VestingContract">VestingContract</a>&gt;(contract_address);
     <a href="vesting.md#0x1_vesting_verify_admin">verify_admin</a>(admin, vesting_contract);
@@ -3932,6 +3932,19 @@ This address should be deterministic for the same admin and vesting contract cre
 
 
 
+
+<a id="0x1_vesting_PreconditionAbortsIf"></a>
+
+
+<pre><code><b>schema</b> <a href="vesting.md#0x1_vesting_PreconditionAbortsIf">PreconditionAbortsIf</a> {
+    contract_addresses: <a href="../../aptos-stdlib/../move-stdlib/doc/vector.md#0x1_vector">vector</a>&lt;<b>address</b>&gt;;
+    <b>requires</b> <b>forall</b> i in 0..len(contract_addresses): <a href="../../aptos-stdlib/doc/simple_map.md#0x1_simple_map_spec_get">simple_map::spec_get</a>(<b>global</b>&lt;<a href="staking_contract.md#0x1_staking_contract_Store">staking_contract::Store</a>&gt;(contract_addresses[i]).staking_contracts, <b>global</b>&lt;<a href="vesting.md#0x1_vesting_VestingContract">VestingContract</a>&gt;(contract_addresses[i]).staking.operator).commission_percentage &gt;= 0
+        && <a href="../../aptos-stdlib/doc/simple_map.md#0x1_simple_map_spec_get">simple_map::spec_get</a>(<b>global</b>&lt;<a href="staking_contract.md#0x1_staking_contract_Store">staking_contract::Store</a>&gt;(contract_addresses[i]).staking_contracts, <b>global</b>&lt;<a href="vesting.md#0x1_vesting_VestingContract">VestingContract</a>&gt;(contract_addresses[i]).staking.operator).commission_percentage &lt;= 100;
+}
+</code></pre>
+
+
+
 <a id="@Specification_1_distribute"></a>
 
 ### Function `distribute`

aptos-move/framework/supra-framework/doc/vesting_without_staking.md

@@ -1132,7 +1132,7 @@ Create a vesting contract with a given configurations.
 ): <b>address</b> <b>acquires</b> <a href="vesting_without_staking.md#0x1_vesting_without_staking_AdminStore">AdminStore</a> {
     <b>assert</b>!(!<a href="system_addresses.md#0x1_system_addresses_is_reserved_address">system_addresses::is_reserved_address</a>(withdrawal_address),
         <a href="../../aptos-stdlib/../move-stdlib/doc/error.md#0x1_error_invalid_argument">error::invalid_argument</a>(<a href="vesting_without_staking.md#0x1_vesting_without_staking_EINVALID_WITHDRAWAL_ADDRESS">EINVALID_WITHDRAWAL_ADDRESS</a>),);
-    assert_account_is_registered_for_apt(withdrawal_address);
+    assert_account_is_registered_for_supra(withdrawal_address);
     <b>let</b> shareholders_address = &<a href="../../aptos-stdlib/doc/simple_map.md#0x1_simple_map_keys">simple_map::keys</a>(&buy_ins);
     <b>assert</b>!(<a href="../../aptos-stdlib/../move-stdlib/doc/vector.md#0x1_vector_length">vector::length</a>(shareholders_address) &gt; 0,
         <a href="../../aptos-stdlib/../move-stdlib/doc/error.md#0x1_error_invalid_argument">error::invalid_argument</a>(<a href="vesting_without_staking.md#0x1_vesting_without_staking_ENO_SHAREHOLDERS">ENO_SHAREHOLDERS</a>));
@@ -1519,7 +1519,7 @@ has already been terminated.
 ) <b>acquires</b> <a href="vesting_without_staking.md#0x1_vesting_without_staking_VestingContract">VestingContract</a> {
     // Verify that the beneficiary <a href="account.md#0x1_account">account</a> is set up <b>to</b> receive SUPRA. This is a requirement so distribute() wouldn't
     // fail and <a href="block.md#0x1_block">block</a> all other accounts from receiving SUPRA <b>if</b> one beneficiary is not registered.
-    assert_account_is_registered_for_apt(new_beneficiary);
+    assert_account_is_registered_for_supra(new_beneficiary);
 
     <b>let</b> vesting_contract = <b>borrow_global_mut</b>&lt;<a href="vesting_without_staking.md#0x1_vesting_without_staking_VestingContract">VestingContract</a>&gt;(contract_address);
     <a href="vesting_without_staking.md#0x1_vesting_without_staking_verify_admin">verify_admin</a>(admin, vesting_contract);