Skip to content

Commit

Permalink
fix aptos account spec block (aptos-labs#8640)
Browse files Browse the repository at this point in the history
  • Loading branch information
@rahxephon89 @xbtmatt
rahxephon89 authored and xbtmatt committed Jul 25, 2023
1 parent 336bdf4 commit 05ec3e4
Show file tree
Hide file tree
Showing 3 changed files with 18 additions and 38 deletions.
28 changes: 9 additions & 19 deletions aptos-move/framework/aptos-framework/doc/aptos_account.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -273,12 +273,6 @@ 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 @@ -314,12 +308,6 @@ 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 @@ -346,14 +334,13 @@ 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>);
<b>spec</b> {
<b>assert</b> <a href="coin.md#0x1_coin_is_account_registered">coin::is_account_registered</a>&lt;AptosCoin&gt;(<b>to</b>);
<b>assume</b> aptos_std::type_info::type_of&lt;CoinType&gt;() == aptos_std::type_info::type_of&lt;AptosCoin&gt;() ==&gt;
<a href="coin.md#0x1_coin_is_account_registered">coin::is_account_registered</a>&lt;CoinType&gt;(<b>to</b>);
};
};
<b>if</b> (!<a href="coin.md#0x1_coin_is_account_registered">coin::is_account_registered</a>&lt;CoinType&gt;(<b>to</b>)) {
<b>assert</b>!(
Expand Down Expand Up @@ -741,7 +728,10 @@ Limit the address of auth_key is not @vm_reserved / @aptos_framework / @aptos_to
<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>);
<b>aborts_if</b> <b>exists</b>&lt;aptos_framework::account::Account&gt;(<b>to</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>);
<b>aborts_if</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="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 Down
23 changes: 5 additions & 18 deletions aptos-move/framework/aptos-framework/sources/aptos_account.move
View file
Original file line number Diff line number Diff line change
Expand Up @@ -75,12 +75,6 @@ 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 @@ -96,26 +90,19 @@ 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);
spec {
assert coin::is_account_registered<AptosCoin>(to);
assume aptos_std::type_info::type_of<CoinType>() == aptos_std::type_info::type_of<AptosCoin>() ==>
coin::is_account_registered<CoinType>(to);
};
};
if (!coin::is_account_registered<CoinType>(to)) {
assert!(
Expand Down
5 changes: 4 additions & 1 deletion aptos-move/framework/aptos-framework/sources/aptos_account.spec.move
View file
Original file line number Diff line number Diff line change
Expand Up @@ -206,6 +206,9 @@ spec aptos_framework::aptos_account {
use aptos_std::type_info;
to: address;
aborts_if !coin::is_account_registered<CoinType>(to) && !type_info::spec_is_struct<CoinType>();
aborts_if !coin::is_account_registered<CoinType>(to) && !can_receive_direct_coin_transfers(to);
aborts_if exists<aptos_framework::account::Account>(to)
&& !coin::is_account_registered<CoinType>(to) && !can_receive_direct_coin_transfers(to);
aborts_if type_info::type_of<CoinType>() != type_info::type_of<AptosCoin>()
&& !coin::is_account_registered<CoinType>(to) && !can_receive_direct_coin_transfers(to);
}
}

0 comments on commit 05ec3e4

Please sign in to comment.