diff --git a/aptos-move/framework/supra-framework/doc/overview.md b/aptos-move/framework/supra-framework/doc/overview.md index 8170e10e58709..79f5b45427cf3 100644 --- a/aptos-move/framework/supra-framework/doc/overview.md +++ b/aptos-move/framework/supra-framework/doc/overview.md @@ -1,5 +1,5 @@ - + # Supra Framework diff --git a/aptos-move/framework/supra-framework/doc/supra_account.md b/aptos-move/framework/supra-framework/doc/supra_account.md index bd73caf609acb..91135b3b0b4e5 100644 --- a/aptos-move/framework/supra-framework/doc/supra_account.md +++ b/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 - + -## Function `assert_account_is_registered_for_apt` +## Function `assert_account_is_registered_for_supra` -
public fun assert_account_is_registered_for_apt(addr: address)
+
public fun assert_account_is_registered_for_supra(addr: address)
 

 
 
@@ -452,7 +452,7 @@ This would create the recipient account first and register it to receive the Coi
 Implementation
 
 
-
public fun assert_account_is_registered_for_apt(addr: address) {
+
public fun assert_account_is_registered_for_supra(addr: address) {
     assert_account_exists(addr);
     assert!(coin::is_account_registered<SupraCoin>(addr), error::not_found(EACCOUNT_NOT_REGISTERED_FOR_APT));
 }
@@ -745,7 +745,7 @@ Address of SUPRA Primary Fungible Store
 
 
 1
-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).
+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).
 Critical
 The authentication key which is passed in as an argument to create_account should satisfy all necessary conditions.
 Formally verified via CreateAccountAbortsIf.
@@ -753,7 +753,7 @@ Address of SUPRA Primary Fungible Store
 
 
 2
-After creating an Supra account, the account should become registered to receive SupraCoin.
+After creating an Aptos account, the account should become registered to receive SupraCoin.
 Critical
 The create_account function creates a new account for the particular address and registers SupraCoin.
 Formally verified via create_account.
@@ -793,7 +793,7 @@ Address of SUPRA Primary Fungible Store
 
 
 7
-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.
+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.
 Low
 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.
 Formally verified via batch_transfer_coins.
@@ -1048,12 +1048,12 @@ Limit the address of auth_key is not @vm_reserved / @supra_framework / @aptos_to
 
 
 
-
+
 
-### Function `assert_account_is_registered_for_apt`
+### Function `assert_account_is_registered_for_supra`
 
 
-
public fun assert_account_is_registered_for_apt(addr: address)
+
public fun assert_account_is_registered_for_supra(addr: address)
 

 
 
diff --git a/aptos-move/framework/supra-framework/doc/vesting.md b/aptos-move/framework/supra-framework/doc/vesting.md
index d6442335c3cbb..d472cbb7abc6e 100644
--- a/aptos-move/framework/supra-framework/doc/vesting.md
+++ b/aptos-move/framework/supra-framework/doc/vesting.md
@@ -2166,7 +2166,7 @@ Create a vesting contract with a given configurations.
         !system_addresses::is_reserved_address(withdrawal_address),
         error::invalid_argument(EINVALID_WITHDRAWAL_ADDRESS),
     );
-    assert_account_is_registered_for_apt(withdrawal_address);
+    assert_account_is_registered_for_supra(withdrawal_address);
     assert!(vector::length(shareholders) > 0, error::invalid_argument(ENO_SHAREHOLDERS));
     assert!(
         simple_map::length(&buy_ins) == vector::length(shareholders),
@@ -2907,7 +2907,7 @@ has already been terminated.
 ) acquires VestingContract {
     // Verify that the beneficiary account is set up to receive SUPRA. This is a requirement so distribute() wouldn't
     // fail and block all other accounts from receiving SUPRA if one beneficiary is not registered.
-    assert_account_is_registered_for_apt(new_beneficiary);
+    assert_account_is_registered_for_supra(new_beneficiary);
 
     let vesting_contract = borrow_global_mut<VestingContract>(contract_address);
     verify_admin(admin, vesting_contract);
@@ -3932,6 +3932,19 @@ This address should be deterministic for the same admin and vesting contract cre
 
 
 
+
+
+
+
+
schema PreconditionAbortsIf {
+    contract_addresses: vector<address>;
+    requires forall i in 0..len(contract_addresses): simple_map::spec_get(global<staking_contract::Store>(contract_addresses[i]).staking_contracts, global<VestingContract>(contract_addresses[i]).staking.operator).commission_percentage >= 0
+        && simple_map::spec_get(global<staking_contract::Store>(contract_addresses[i]).staking_contracts, global<VestingContract>(contract_addresses[i]).staking.operator).commission_percentage <= 100;
+}
+

+
+
+
 
 
 ### Function `distribute`
diff --git a/aptos-move/framework/supra-framework/doc/vesting_without_staking.md b/aptos-move/framework/supra-framework/doc/vesting_without_staking.md
index 8ae3a55e78161..673776ce36d62 100644
--- a/aptos-move/framework/supra-framework/doc/vesting_without_staking.md
+++ b/aptos-move/framework/supra-framework/doc/vesting_without_staking.md
@@ -1132,7 +1132,7 @@ Create a vesting contract with a given configurations.
 ): address acquires AdminStore {
     assert!(!system_addresses::is_reserved_address(withdrawal_address),
         error::invalid_argument(EINVALID_WITHDRAWAL_ADDRESS),);
-    assert_account_is_registered_for_apt(withdrawal_address);
+    assert_account_is_registered_for_supra(withdrawal_address);
     let shareholders_address = &simple_map::keys(&buy_ins);
     assert!(vector::length(shareholders_address) > 0,
         error::invalid_argument(ENO_SHAREHOLDERS));
@@ -1519,7 +1519,7 @@ has already been terminated.
 ) acquires VestingContract {
     // Verify that the beneficiary account is set up to receive SUPRA. This is a requirement so distribute() wouldn't
     // fail and block all other accounts from receiving SUPRA if one beneficiary is not registered.
-    assert_account_is_registered_for_apt(new_beneficiary);
+    assert_account_is_registered_for_supra(new_beneficiary);
 
     let vesting_contract = borrow_global_mut<VestingContract>(contract_address);
     verify_admin(admin, vesting_contract);