From 5bdbc19835225cb06f4c438c3291cf5f637afa1f Mon Sep 17 00:00:00 2001 From: Teng Zhang Date: Tue, 13 Jun 2023 16:05:56 -0700 Subject: [PATCH] fix aptos account spec block (#8640) GitOrigin-RevId: 015bc88e7091c423ac454a886d0706b8c61ec77d --- aptos-framework/doc/aptos_account.md | 28 ++++++------------- aptos-framework/sources/aptos_account.move | 23 ++++----------- .../sources/aptos_account.spec.move | 5 +++- 3 files changed, 18 insertions(+), 38 deletions(-) diff --git a/aptos-framework/doc/aptos_account.md b/aptos-framework/doc/aptos_account.md index 6ee25c867..80fc8816f 100644 --- a/aptos-framework/doc/aptos_account.md +++ b/aptos-framework/doc/aptos_account.md @@ -273,12 +273,6 @@ 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),
@@ -314,12 +308,6 @@ This would create the recipient account first and register it to receive the Coi
 
 
 
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));
 }
 

@@ -346,14 +334,13 @@ This would create the recipient account first and register it to receive the Coi
 
 
 
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!(
@@ -741,7 +728,10 @@ Limit the address of auth_key is not @vm_reserved / @aptos_framework / @aptos_to
 
schema RegistCoinAbortsIf<CoinType> {
     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);
 }
 

 
diff --git a/aptos-framework/sources/aptos_account.move b/aptos-framework/sources/aptos_account.move
index 9eeb66bda..c58395714 100644
--- a/aptos-framework/sources/aptos_account.move
+++ b/aptos-framework/sources/aptos_account.move
@@ -75,12 +75,6 @@ module aptos_framework::aptos_account {
     /// Batch version of transfer_coins.
     public entry fun batch_transfer_coins(
         from: &signer, recipients: vector
, amounts: vector) 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() != type_info::type_of();
-        };
         let recipients_len = vector::length(&recipients);
         assert!(
             recipients_len == vector::length(&amounts),
@@ -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(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() != type_info::type_of();
-        };
         deposit_coins(to, coin::withdraw(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(to: address, coins: Coin) 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() != type_info::type_of();
-        };
         if (!account::exists_at(to)) {
             create_account(to);
+            spec {
+                assert coin::is_account_registered(to);
+                assume aptos_std::type_info::type_of() == aptos_std::type_info::type_of() ==>
+                    coin::is_account_registered(to);
+            };
         };
         if (!coin::is_account_registered(to)) {
             assert!(
diff --git a/aptos-framework/sources/aptos_account.spec.move b/aptos-framework/sources/aptos_account.spec.move
index d1a4e18ce..661bd0414 100644
--- a/aptos-framework/sources/aptos_account.spec.move
+++ b/aptos-framework/sources/aptos_account.spec.move
@@ -206,6 +206,9 @@ spec aptos_framework::aptos_account {
         use aptos_std::type_info;
         to: address;
         aborts_if !coin::is_account_registered(to) && !type_info::spec_is_struct();
-        aborts_if !coin::is_account_registered(to) && !can_receive_direct_coin_transfers(to);
+        aborts_if exists(to)
+            && !coin::is_account_registered(to) && !can_receive_direct_coin_transfers(to);
+        aborts_if type_info::type_of() != type_info::type_of()
+            && !coin::is_account_registered(to) && !can_receive_direct_coin_transfers(to);
     }
 }