Skip to content

Commit

Permalink
Spec aptos account (#8364)
Browse files Browse the repository at this point in the history 
* init

* run lint

* delete verfiy and add schema

* pass linter test

* fix lint

* merge aptos main

* run lint

* [python] return int balance of coins

* [python] async sleep for async calls

* [python] use aptos_account::transfer instead of coin::transfer

* [python] expose payload generators for token client

* [python] support inserting sequence numbers in transaction helpers

* [python] add a transaction management layer

This provides a framework for managing as many transactions from a
single account at once
* The AccountSequenceNumber allocates up to 100 outstanding sequence numbers to maximize the number of concurrent transactions in the happy path.
* The transaction manager provides async workers that push a transaction from submission through to validating completion
Together they provide the basic harness for scaling transaction
submission on the Aptos blockchain from a single account.

* [python] Add testing coverage

* [python] cleaning up with feedback

* [docs] update transaction management

* [python] add a modest reliablity layer to transaction management

this handles all the failures associated with network congestion,
meaning this is ready to ship for now... need more testing on other
failure cases.... such as intermittent network connectivity, lost
connections, bad upstreams.

* [python] remove unnecessary python dependencies

* [Execution Benchmark] Calibrate Threshold (#8591)

* clean AptosVmImpl::new() up a bit

* [Helm] Add charts for kube-state-metrics and prometheus-node-exporter (#8576)

* Add a zip functions to iterate over 2 vectors concurrently (#8584)

* [TF] Add health check for waypoint service in GCP testnet-addons

Also, add a default for "gke_maintenance_policy" in the
aptos-node-testnet module.

* [Storage][Sharding][Pruner] Restructure ledger pruner. (#8443)

* use assume to replace require Cointype != Aptos

* fix linter

---------

Co-authored-by: David Wolinsky <isaac.wolinsky@gmail.com>
Co-authored-by: danielx <66756900+danielxiangzl@users.noreply.github.com>
Co-authored-by: aldenhu <msmouse@gmail.com>
Co-authored-by: Stelian Ionescu <stelian@aptoslabs.com>
Co-authored-by: Kevin <105028215+movekevin@users.noreply.github.com>
Co-authored-by: Guoteng Rao <3603304+grao1991@users.noreply.github.com>
GitOrigin-RevId: b5f5f522ce76ecbd04f51fda34fb34ec676412a7
  • Loading branch information
@UIZorrot @davidiw
@danielxiangzl @msmouse @sionescu @movekevin @grao1991
7 people authored and aptos-bot committed Oct 23, 2024
1 parent 872361e commit 7cec839
Show file tree
Hide file tree
Showing 3 changed files with 319 additions and 17 deletions.
163 changes: 156 additions & 7 deletions aptos-framework/doc/aptos_account.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -273,6 +273,12 @@ Batch version of transfer_coins.

<pre><code><b>public</b> entry <b>fun</b> <a href="aptos_account.md#0x1_aptos_account_batch_transfer_coins">batch_transfer_coins</a>&lt;CoinType&gt;(
from: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>, recipients: <a href="../../aptos-stdlib/../move-stdlib/doc/vector.md#0x1_vector">vector</a>&lt;<b>address</b>&gt;, amounts: <a href="../../aptos-stdlib/../move-stdlib/doc/vector.md#0x1_vector">vector</a>&lt;u64&gt;) <b>acquires</b> <a href="aptos_account.md#0x1_aptos_account_DirectTransferConfig">DirectTransferConfig</a> {
<b>spec</b> {
// Cointype should not be aptoscoin, otherwise it will automaticly create an <a href="account.md#0x1_account">account</a>.
// Meanwhile, aptoscoin <b>has</b> already been proved in normal tranfer
<b>use</b> aptos_std::type_info;
<b>assume</b> <a href="../../aptos-stdlib/doc/type_info.md#0x1_type_info_type_of">type_info::type_of</a>&lt;CoinType&gt;() != <a href="../../aptos-stdlib/doc/type_info.md#0x1_type_info_type_of">type_info::type_of</a>&lt;AptosCoin&gt;();
};
<b>let</b> recipients_len = <a href="../../aptos-stdlib/../move-stdlib/doc/vector.md#0x1_vector_length">vector::length</a>(&recipients);
<b>assert</b>!(
recipients_len == <a href="../../aptos-stdlib/../move-stdlib/doc/vector.md#0x1_vector_length">vector::length</a>(&amounts),
Expand Down Expand Up @@ -308,6 +314,12 @@ This would create the recipient account first and register it to receive the Coi


<pre><code><b>public</b> entry <b>fun</b> <a href="aptos_account.md#0x1_aptos_account_transfer_coins">transfer_coins</a>&lt;CoinType&gt;(from: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>, <b>to</b>: <b>address</b>, amount: u64) <b>acquires</b> <a href="aptos_account.md#0x1_aptos_account_DirectTransferConfig">DirectTransferConfig</a> {
<b>spec</b> {
// Cointype should not be aptoscoin, otherwise it will automaticly create an <a href="account.md#0x1_account">account</a>.
// Meanwhile, aptoscoin <b>has</b> already been proved in normal tranfer
<b>use</b> aptos_std::type_info;
<b>assume</b> <a href="../../aptos-stdlib/doc/type_info.md#0x1_type_info_type_of">type_info::type_of</a>&lt;CoinType&gt;() != <a href="../../aptos-stdlib/doc/type_info.md#0x1_type_info_type_of">type_info::type_of</a>&lt;AptosCoin&gt;();
};
<a href="aptos_account.md#0x1_aptos_account_deposit_coins">deposit_coins</a>(<b>to</b>, <a href="coin.md#0x1_coin_withdraw">coin::withdraw</a>&lt;CoinType&gt;(from, amount));
}
</code></pre>
Expand All @@ -334,6 +346,12 @@ This would create the recipient account first and register it to receive the Coi


<pre><code><b>public</b> <b>fun</b> <a href="aptos_account.md#0x1_aptos_account_deposit_coins">deposit_coins</a>&lt;CoinType&gt;(<b>to</b>: <b>address</b>, coins: Coin&lt;CoinType&gt;) <b>acquires</b> <a href="aptos_account.md#0x1_aptos_account_DirectTransferConfig">DirectTransferConfig</a> {
<b>spec</b> {
// Cointype should not be aptoscoin, otherwise it will automaticly create an <a href="account.md#0x1_account">account</a>.
// Meanwhile, aptoscoin <b>has</b> already been proved in normal tranfer
<b>use</b> aptos_std::type_info;
<b>assume</b> <a href="../../aptos-stdlib/doc/type_info.md#0x1_type_info_type_of">type_info::type_of</a>&lt;CoinType&gt;() != <a href="../../aptos-stdlib/doc/type_info.md#0x1_type_info_type_of">type_info::type_of</a>&lt;AptosCoin&gt;();
};
<b>if</b> (!<a href="account.md#0x1_account_exists_at">account::exists_at</a>(<b>to</b>)) {
<a href="aptos_account.md#0x1_aptos_account_create_account">create_account</a>(<b>to</b>);
};
Expand Down Expand Up @@ -482,8 +500,7 @@ By default, this returns true if an account has not explicitly set whether the c



<pre><code><b>pragma</b> verify = <b>true</b>;
<b>pragma</b> aborts_if_is_strict;
<pre><code><b>pragma</b> aborts_if_is_strict;
</code></pre>


Expand Down Expand Up @@ -548,7 +565,34 @@ Limit the address of auth_key is not @vm_reserved / @aptos_framework / @aptos_to



<pre><code><b>pragma</b> verify=<b>false</b>;
<pre><code><b>pragma</b> verify = <b>false</b>;
<b>let</b> account_addr_source = <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(source);
<b>let</b> coin_store_source = <b>global</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;AptosCoin&gt;&gt;(account_addr_source);
<b>let</b> balance_source = coin_store_source.<a href="coin.md#0x1_coin">coin</a>.value;
<b>requires</b> <b>forall</b> i in 0..len(recipients):
recipients[i] != account_addr_source;
<b>requires</b> <b>exists</b> i in 0..len(recipients):
amounts[i] &gt; 0;
<b>aborts_if</b> len(recipients) != len(amounts);
<b>aborts_if</b> <b>exists</b> i in 0..len(recipients):
!<a href="account.md#0x1_account_exists_at">account::exists_at</a>(recipients[i]) && <a href="aptos_account.md#0x1_aptos_account_length_judgment">length_judgment</a>(recipients[i]);
<b>aborts_if</b> <b>exists</b> i in 0..len(recipients):
!<a href="account.md#0x1_account_exists_at">account::exists_at</a>(recipients[i]) && (recipients[i] == @vm_reserved || recipients[i] == @aptos_framework || recipients[i] == @aptos_token);
<b>ensures</b> <b>forall</b> i in 0..len(recipients):
(!<a href="account.md#0x1_account_exists_at">account::exists_at</a>(recipients[i]) ==&gt; !<a href="aptos_account.md#0x1_aptos_account_length_judgment">length_judgment</a>(recipients[i])) &&
(!<a href="account.md#0x1_account_exists_at">account::exists_at</a>(recipients[i]) ==&gt; (recipients[i] != @vm_reserved && recipients[i] != @aptos_framework && recipients[i] != @aptos_token));
<b>aborts_if</b> <b>exists</b> i in 0..len(recipients):
!<b>exists</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;AptosCoin&gt;&gt;(account_addr_source);
<b>aborts_if</b> <b>exists</b> i in 0..len(recipients):
coin_store_source.frozen;
<b>aborts_if</b> <b>exists</b> i in 0..len(recipients):
<b>global</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;AptosCoin&gt;&gt;(account_addr_source).<a href="coin.md#0x1_coin">coin</a>.value &lt; amounts[i];
<b>aborts_if</b> <b>exists</b> i in 0..len(recipients):
<b>exists</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;AptosCoin&gt;&gt;(recipients[i]) && <b>global</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;AptosCoin&gt;&gt;(recipients[i]).frozen;
<b>aborts_if</b> <b>exists</b> i in 0..len(recipients):
<a href="account.md#0x1_account_exists_at">account::exists_at</a>(recipients[i]) && !<b>exists</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;AptosCoin&gt;&gt;(recipients[i]) && <b>global</b>&lt;<a href="account.md#0x1_account_Account">account::Account</a>&gt;(recipients[i]).guid_creation_num + 2 &gt;= <a href="account.md#0x1_account_MAX_GUID_CREATION_NUM">account::MAX_GUID_CREATION_NUM</a>;
<b>aborts_if</b> <b>exists</b> i in 0..len(recipients):
<a href="account.md#0x1_account_exists_at">account::exists_at</a>(recipients[i]) && !<b>exists</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;AptosCoin&gt;&gt;(recipients[i]) && <b>global</b>&lt;<a href="account.md#0x1_account_Account">account::Account</a>&gt;(recipients[i]).guid_creation_num + 2 &gt; MAX_U64;
</code></pre>


Expand All @@ -564,7 +608,13 @@ Limit the address of auth_key is not @vm_reserved / @aptos_framework / @aptos_to



<pre><code><b>pragma</b> verify = <b>false</b>;
<pre><code><b>let</b> account_addr_source = <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(source);
<b>let</b> coin_store_to = <b>global</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;AptosCoin&gt;&gt;(<b>to</b>);
<b>requires</b> account_addr_source != <b>to</b>;
<b>include</b> <a href="aptos_account.md#0x1_aptos_account_CreateAccountTransferAbortsIf">CreateAccountTransferAbortsIf</a>;
<b>include</b> <a href="aptos_account.md#0x1_aptos_account_GuidAbortsIf">GuidAbortsIf</a>&lt;AptosCoin&gt;;
<b>include</b> <a href="aptos_account.md#0x1_aptos_account_WithdrawAbortsIf">WithdrawAbortsIf</a>&lt;AptosCoin&gt;{from: source};
<b>aborts_if</b> <b>exists</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;AptosCoin&gt;&gt;(<b>to</b>) && <b>global</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;AptosCoin&gt;&gt;(<b>to</b>).frozen;
</code></pre>


Expand All @@ -580,7 +630,38 @@ Limit the address of auth_key is not @vm_reserved / @aptos_framework / @aptos_to



<pre><code><b>pragma</b> verify=<b>false</b>;
<pre><code><b>pragma</b> verify = <b>false</b>;
<b>let</b> account_addr_source = <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(from);
<b>let</b> coin_store_source = <b>global</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;CoinType&gt;&gt;(account_addr_source);
<b>let</b> balance_source = coin_store_source.<a href="coin.md#0x1_coin">coin</a>.value;
<b>requires</b> <b>forall</b> i in 0..len(recipients):
recipients[i] != account_addr_source;
<b>requires</b> <b>exists</b> i in 0..len(recipients):
amounts[i] &gt; 0;
<b>aborts_if</b> len(recipients) != len(amounts);
<b>aborts_if</b> <b>exists</b> i in 0..len(recipients):
!<a href="account.md#0x1_account_exists_at">account::exists_at</a>(recipients[i]) && <a href="aptos_account.md#0x1_aptos_account_length_judgment">length_judgment</a>(recipients[i]);
<b>aborts_if</b> <b>exists</b> i in 0..len(recipients):
!<a href="account.md#0x1_account_exists_at">account::exists_at</a>(recipients[i]) && (recipients[i] == @vm_reserved || recipients[i] == @aptos_framework || recipients[i] == @aptos_token);
<b>ensures</b> <b>forall</b> i in 0..len(recipients):
(!<a href="account.md#0x1_account_exists_at">account::exists_at</a>(recipients[i]) ==&gt; !<a href="aptos_account.md#0x1_aptos_account_length_judgment">length_judgment</a>(recipients[i])) &&
(!<a href="account.md#0x1_account_exists_at">account::exists_at</a>(recipients[i]) ==&gt; (recipients[i] != @vm_reserved && recipients[i] != @aptos_framework && recipients[i] != @aptos_token));
<b>aborts_if</b> <b>exists</b> i in 0..len(recipients):
!<b>exists</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;CoinType&gt;&gt;(account_addr_source);
<b>aborts_if</b> <b>exists</b> i in 0..len(recipients):
coin_store_source.frozen;
<b>aborts_if</b> <b>exists</b> i in 0..len(recipients):
<b>global</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;CoinType&gt;&gt;(account_addr_source).<a href="coin.md#0x1_coin">coin</a>.value &lt; amounts[i];
<b>aborts_if</b> <b>exists</b> i in 0..len(recipients):
<b>exists</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;CoinType&gt;&gt;(recipients[i]) && <b>global</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;CoinType&gt;&gt;(recipients[i]).frozen;
<b>aborts_if</b> <b>exists</b> i in 0..len(recipients):
<a href="account.md#0x1_account_exists_at">account::exists_at</a>(recipients[i]) && !<b>exists</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;CoinType&gt;&gt;(recipients[i]) && <b>global</b>&lt;<a href="account.md#0x1_account_Account">account::Account</a>&gt;(recipients[i]).guid_creation_num + 2 &gt;= <a href="account.md#0x1_account_MAX_GUID_CREATION_NUM">account::MAX_GUID_CREATION_NUM</a>;
<b>aborts_if</b> <b>exists</b> i in 0..len(recipients):
<a href="account.md#0x1_account_exists_at">account::exists_at</a>(recipients[i]) && !<b>exists</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;CoinType&gt;&gt;(recipients[i]) && <b>global</b>&lt;<a href="account.md#0x1_account_Account">account::Account</a>&gt;(recipients[i]).guid_creation_num + 2 &gt; MAX_U64;
<b>aborts_if</b> <b>exists</b> i in 0..len(recipients):
!<a href="coin.md#0x1_coin_is_account_registered">coin::is_account_registered</a>&lt;CoinType&gt;(recipients[i]) && !<a href="../../aptos-stdlib/doc/type_info.md#0x1_type_info_spec_is_struct">type_info::spec_is_struct</a>&lt;CoinType&gt;();
<b>aborts_if</b> <b>exists</b> i in 0..len(recipients):
!<a href="coin.md#0x1_coin_is_account_registered">coin::is_account_registered</a>&lt;CoinType&gt;(recipients[i]) && !<a href="aptos_account.md#0x1_aptos_account_can_receive_direct_coin_transfers">can_receive_direct_coin_transfers</a>(recipients[i]);
</code></pre>


Expand All @@ -596,7 +677,72 @@ Limit the address of auth_key is not @vm_reserved / @aptos_framework / @aptos_to



<pre><code><b>pragma</b> verify=<b>false</b>;
<pre><code><b>let</b> account_addr_source = <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(from);
<b>let</b> coin_store_to = <b>global</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;CoinType&gt;&gt;(<b>to</b>);
<b>requires</b> account_addr_source != <b>to</b>;
<b>include</b> <a href="aptos_account.md#0x1_aptos_account_CreateAccountTransferAbortsIf">CreateAccountTransferAbortsIf</a>;
<b>include</b> <a href="aptos_account.md#0x1_aptos_account_WithdrawAbortsIf">WithdrawAbortsIf</a>&lt;CoinType&gt;;
<b>include</b> <a href="aptos_account.md#0x1_aptos_account_GuidAbortsIf">GuidAbortsIf</a>&lt;CoinType&gt;;
<b>include</b> <a href="aptos_account.md#0x1_aptos_account_RegistCoinAbortsIf">RegistCoinAbortsIf</a>&lt;CoinType&gt;;
<b>aborts_if</b> <b>exists</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;CoinType&gt;&gt;(<b>to</b>) && <b>global</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;CoinType&gt;&gt;(<b>to</b>).frozen;
</code></pre>




<a name="0x1_aptos_account_CreateAccountTransferAbortsIf"></a>


<pre><code><b>schema</b> <a href="aptos_account.md#0x1_aptos_account_CreateAccountTransferAbortsIf">CreateAccountTransferAbortsIf</a> {
<b>to</b>: <b>address</b>;
<b>aborts_if</b> !<a href="account.md#0x1_account_exists_at">account::exists_at</a>(<b>to</b>) && <a href="aptos_account.md#0x1_aptos_account_length_judgment">length_judgment</a>(<b>to</b>);
<b>aborts_if</b> !<a href="account.md#0x1_account_exists_at">account::exists_at</a>(<b>to</b>) && (<b>to</b> == @vm_reserved || <b>to</b> == @aptos_framework || <b>to</b> == @aptos_token);
}
</code></pre>




<a name="0x1_aptos_account_WithdrawAbortsIf"></a>


<pre><code><b>schema</b> <a href="aptos_account.md#0x1_aptos_account_WithdrawAbortsIf">WithdrawAbortsIf</a>&lt;CoinType&gt; {
from: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>;
amount: u64;
<b>let</b> account_addr_source = <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(from);
<b>let</b> coin_store_source = <b>global</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;CoinType&gt;&gt;(account_addr_source);
<b>let</b> balance_source = coin_store_source.<a href="coin.md#0x1_coin">coin</a>.value;
<b>aborts_if</b> !<b>exists</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;CoinType&gt;&gt;(account_addr_source);
<b>aborts_if</b> coin_store_source.frozen;
<b>aborts_if</b> balance_source &lt; amount;
}
</code></pre>




<a name="0x1_aptos_account_GuidAbortsIf"></a>


<pre><code><b>schema</b> <a href="aptos_account.md#0x1_aptos_account_GuidAbortsIf">GuidAbortsIf</a>&lt;CoinType&gt; {
<b>to</b>: <b>address</b>;
<b>let</b> acc = <b>global</b>&lt;<a href="account.md#0x1_account_Account">account::Account</a>&gt;(<b>to</b>);
<b>aborts_if</b> <a href="account.md#0x1_account_exists_at">account::exists_at</a>(<b>to</b>) && !<b>exists</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;CoinType&gt;&gt;(<b>to</b>) && acc.guid_creation_num + 2 &gt;= <a href="account.md#0x1_account_MAX_GUID_CREATION_NUM">account::MAX_GUID_CREATION_NUM</a>;
<b>aborts_if</b> <a href="account.md#0x1_account_exists_at">account::exists_at</a>(<b>to</b>) && !<b>exists</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;CoinType&gt;&gt;(<b>to</b>) && acc.guid_creation_num + 2 &gt; MAX_U64;
}
</code></pre>




<a name="0x1_aptos_account_RegistCoinAbortsIf"></a>


<pre><code><b>schema</b> <a href="aptos_account.md#0x1_aptos_account_RegistCoinAbortsIf">RegistCoinAbortsIf</a>&lt;CoinType&gt; {
<b>to</b>: <b>address</b>;
<b>aborts_if</b> !<a href="coin.md#0x1_coin_is_account_registered">coin::is_account_registered</a>&lt;CoinType&gt;(<b>to</b>) && !<a href="../../aptos-stdlib/doc/type_info.md#0x1_type_info_spec_is_struct">type_info::spec_is_struct</a>&lt;CoinType&gt;();
<b>aborts_if</b> !<a href="coin.md#0x1_coin_is_account_registered">coin::is_account_registered</a>&lt;CoinType&gt;(<b>to</b>) && !<a href="aptos_account.md#0x1_aptos_account_can_receive_direct_coin_transfers">can_receive_direct_coin_transfers</a>(<b>to</b>);
}
</code></pre>


Expand All @@ -612,7 +758,10 @@ Limit the address of auth_key is not @vm_reserved / @aptos_framework / @aptos_to



<pre><code><b>pragma</b> verify=<b>false</b>;
<pre><code><b>include</b> <a href="aptos_account.md#0x1_aptos_account_CreateAccountTransferAbortsIf">CreateAccountTransferAbortsIf</a>;
<b>include</b> <a href="aptos_account.md#0x1_aptos_account_GuidAbortsIf">GuidAbortsIf</a>&lt;CoinType&gt;;
<b>include</b> <a href="aptos_account.md#0x1_aptos_account_RegistCoinAbortsIf">RegistCoinAbortsIf</a>&lt;CoinType&gt;;
<b>aborts_if</b> <b>exists</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;CoinType&gt;&gt;(<b>to</b>) && <b>global</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;CoinType&gt;&gt;(<b>to</b>).frozen;
</code></pre>


Expand Down
18 changes: 18 additions & 0 deletions aptos-framework/sources/aptos_account.move
View file
Original file line number Diff line number Diff line change
Expand Up @@ -75,6 +75,12 @@ module aptos_framework::aptos_account {
/// Batch version of transfer_coins.
public entry fun batch_transfer_coins<CoinType>(
from: &signer, recipients: vector<address>, amounts: vector<u64>) acquires DirectTransferConfig {
spec {
// Cointype should not be aptoscoin, otherwise it will automaticly create an account.
// Meanwhile, aptoscoin has already been proved in normal tranfer
use aptos_std::type_info;
assume type_info::type_of<CoinType>() != type_info::type_of<AptosCoin>();
};
let recipients_len = vector::length(&recipients);
assert!(
recipients_len == vector::length(&amounts),
Expand All @@ -90,12 +96,24 @@ module aptos_framework::aptos_account {
/// Convenient function to transfer a custom CoinType to a recipient account that might not exist.
/// This would create the recipient account first and register it to receive the CoinType, before transferring.
public entry fun transfer_coins<CoinType>(from: &signer, to: address, amount: u64) acquires DirectTransferConfig {
spec {
// Cointype should not be aptoscoin, otherwise it will automaticly create an account.
// Meanwhile, aptoscoin has already been proved in normal tranfer
use aptos_std::type_info;
assume type_info::type_of<CoinType>() != type_info::type_of<AptosCoin>();
};
deposit_coins(to, coin::withdraw<CoinType>(from, amount));
}

/// Convenient function to deposit a custom CoinType into a recipient account that might not exist.
/// This would create the recipient account first and register it to receive the CoinType, before transferring.
public fun deposit_coins<CoinType>(to: address, coins: Coin<CoinType>) acquires DirectTransferConfig {
spec {
// Cointype should not be aptoscoin, otherwise it will automaticly create an account.
// Meanwhile, aptoscoin has already been proved in normal tranfer
use aptos_std::type_info;
assume type_info::type_of<CoinType>() != type_info::type_of<AptosCoin>();
};
if (!account::exists_at(to)) {
create_account(to);
};
Expand Down
Loading

0 comments on commit 7cec839

Please sign in to comment.