@@ -94,6 +94,7 @@ This module provides the foundation for typesafe Coins.
94
94
- [ Function ` register ` ] ( #0x1_coin_register )
95
95
- [ Function ` transfer ` ] ( #0x1_coin_transfer )
96
96
- [ Function ` value ` ] ( #0x1_coin_value )
97
+ - [ Function ` withdraw_from ` ] ( #0x1_coin_withdraw_from )
97
98
- [ Function ` withdraw ` ] ( #0x1_coin_withdraw )
98
99
- [ Function ` zero ` ] ( #0x1_coin_zero )
99
100
- [ Function ` destroy_freeze_cap ` ] ( #0x1_coin_destroy_freeze_cap )
@@ -3399,6 +3400,71 @@ Returns the <code>value</code> passed in <code><a href="coin.md#0x1_coin">coin</
3399
3400
3400
3401
3401
3402
3403
+ </details >
3404
+
3405
+ <a id =" 0x1_coin_withdraw_from " ></a >
3406
+
3407
+ ## Function ` withdraw_from `
3408
+
3409
+ Withdraws a specifed <code >amount</code > of coin <code >CoinType</code > from the specified <code ><a href =" account.md#0x1_account " >account</a ></code >.
3410
+ @param account The account from which to withdraw the coin.
3411
+ @param amount The amount of coin to withdraw.
3412
+
3413
+
3414
+ <pre ><code ><b >public</b >(<b >friend</b >) <b >fun</b > <a href =" coin.md#0x1_coin_withdraw_from " >withdraw_from</a >< ; CoinType> ; (account_addr: <b >address</b >, amount: u64): <a href =" coin.md#0x1_coin_Coin " >coin::Coin</a >< ; CoinType> ;
3415
+ </code ></pre >
3416
+
3417
+
3418
+
3419
+ <details >
3420
+ <summary >Implementation</summary >
3421
+
3422
+
3423
+ <pre ><code ><b >public</b >(<b >friend</b >) <b >fun</b > <a href =" coin.md#0x1_coin_withdraw_from " >withdraw_from</a >< ; CoinType> ; (
3424
+ account_addr: <b >address</b >,
3425
+ amount: u64
3426
+ ): <a href =" coin.md#0x1_coin_Coin " >Coin</a >< ; CoinType> ; <b >acquires</b > <a href =" coin.md#0x1_coin_CoinStore " >CoinStore</a >, <a href =" coin.md#0x1_coin_CoinConversionMap " >CoinConversionMap</a >, <a href =" coin.md#0x1_coin_CoinInfo " >CoinInfo</a >, <a href =" coin.md#0x1_coin_PairedCoinType " >PairedCoinType</a > {
3427
+
3428
+ <b >let</b > (coin_amount_to_withdraw, fa_amount_to_withdraw) = <a href =" coin.md#0x1_coin_calculate_amount_to_withdraw " >calculate_amount_to_withdraw</a >< ; CoinType> ; (
3429
+ account_addr,
3430
+ amount
3431
+ );
3432
+ <b >let</b > withdrawn_coin = <b >if</b > (coin_amount_to_withdraw > ; 0) {
3433
+ <b >let</b > coin_store = <b >borrow_global_mut</b >< ; <a href =" coin.md#0x1_coin_CoinStore " >CoinStore</a >< ; CoinType> ;> ; (account_addr);
3434
+ <b >assert</b >!(
3435
+ !coin_store.frozen,
3436
+ <a href =" ../../aptos-stdlib/../move-stdlib/doc/error.md#0x1_error_permission_denied " >error::permission_denied</a >(<a href =" coin.md#0x1_coin_EFROZEN " >EFROZEN</a >),
3437
+ );
3438
+ <b >if</b > (std::features::module_event_migration_enabled()) {
3439
+ <a href =" event.md#0x1_event_emit " >event::emit</a >(
3440
+ <a href =" coin.md#0x1_coin_CoinWithdraw " >CoinWithdraw</a > {
3441
+ coin_type: type_name< ; CoinType> ; (), <a href =" account.md#0x1_account " >account</a >: account_addr, amount: coin_amount_to_withdraw
3442
+ }
3443
+ );
3444
+ };
3445
+ <a href =" event.md#0x1_event_emit_event " >event::emit_event</a >< ; <a href =" coin.md#0x1_coin_WithdrawEvent " >WithdrawEvent</a >> ; (
3446
+ &<b >mut</b > coin_store.withdraw_events,
3447
+ <a href =" coin.md#0x1_coin_WithdrawEvent " >WithdrawEvent</a > { amount: coin_amount_to_withdraw },
3448
+ );
3449
+ <a href =" coin.md#0x1_coin_extract " >extract</a >(&<b >mut</b > coin_store.<a href =" coin.md#0x1_coin " >coin</a >, coin_amount_to_withdraw)
3450
+ } <b >else</b > {
3451
+ <a href =" coin.md#0x1_coin_zero " >zero</a >()
3452
+ };
3453
+ <b >if</b > (fa_amount_to_withdraw > ; 0) {
3454
+ <b >let</b > store_addr = <a href =" primary_fungible_store.md#0x1_primary_fungible_store_primary_store_address " >primary_fungible_store::primary_store_address</a >(
3455
+ account_addr,
3456
+ <a href =" ../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_destroy_some " >option::destroy_some</a >(<a href =" coin.md#0x1_coin_paired_metadata " >paired_metadata</a >< ; CoinType> ; ())
3457
+ );
3458
+ <b >let</b > fa = <a href =" fungible_asset.md#0x1_fungible_asset_withdraw_internal " >fungible_asset::withdraw_internal</a >(store_addr, fa_amount_to_withdraw);
3459
+ <a href =" coin.md#0x1_coin_merge " >merge</a >(&<b >mut</b > withdrawn_coin, <a href =" coin.md#0x1_coin_fungible_asset_to_coin " >fungible_asset_to_coin</a >< ; CoinType> ; (fa));
3460
+ };
3461
+
3462
+ withdrawn_coin
3463
+ }
3464
+ </code ></pre >
3465
+
3466
+
3467
+
3402
3468
</details >
3403
3469
3404
3470
<a id =" 0x1_coin_withdraw " ></a >
@@ -3814,64 +3880,6 @@ initialize, initialize_internal, initialize_with_parallelizable_supply;
3814
3880
3815
3881
3816
3882
3817
-
3818
- <a id =" 0x1_coin_spec_is_account_registered " ></a >
3819
-
3820
-
3821
- <pre ><code ><b >fun</b > <a href =" coin.md#0x1_coin_spec_is_account_registered " >spec_is_account_registered</a >< ; CoinType> ; (account_addr: <b >address</b >): bool {
3822
- <b >let</b > paired_metadata_opt = <a href =" coin.md#0x1_coin_spec_paired_metadata " >spec_paired_metadata</a >< ; CoinType> ; ();
3823
- <b >exists</b >< ; <a href =" coin.md#0x1_coin_CoinStore " >CoinStore</a >< ; CoinType> ;> ; (account_addr) || (<a href =" ../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_spec_is_some " >option::spec_is_some</a >(
3824
- paired_metadata_opt
3825
- ) && <a href =" primary_fungible_store.md#0x1_primary_fungible_store_spec_primary_store_exists " >primary_fungible_store::spec_primary_store_exists</a >(account_addr, <a href =" ../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_spec_borrow " >option::spec_borrow</a >(paired_metadata_opt)))
3826
- }
3827
- </code ></pre >
3828
-
3829
-
3830
-
3831
-
3832
- <a id =" 0x1_coin_CoinSubAbortsIf " ></a >
3833
-
3834
-
3835
- <pre ><code ><b >schema</b > <a href =" coin.md#0x1_coin_CoinSubAbortsIf " >CoinSubAbortsIf</a >< ; CoinType> ; {
3836
- amount: u64;
3837
- <b >let</b > addr = <a href =" ../../aptos-stdlib/doc/type_info.md#0x1_type_info_type_of " >type_info::type_of</a >< ; CoinType> ; ().account_address;
3838
- <b >let</b > maybe_supply = <b >global</b >< ; <a href =" coin.md#0x1_coin_CoinInfo " >CoinInfo</a >< ; CoinType> ;> ; (addr).<a href =" coin.md#0x1_coin_supply " >supply</a >;
3839
- <b >include</b > (<a href =" ../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_is_some " >option::is_some</a >(
3840
- maybe_supply
3841
- )) ==> ; <a href =" optional_aggregator.md#0x1_optional_aggregator_SubAbortsIf " >optional_aggregator::SubAbortsIf</a > { <a href =" optional_aggregator.md#0x1_optional_aggregator " >optional_aggregator</a >: <a href =" ../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_borrow " >option::borrow</a >(maybe_supply), value: amount };
3842
- }
3843
- </code ></pre >
3844
-
3845
-
3846
-
3847
-
3848
- <a id =" 0x1_coin_CoinAddAbortsIf " ></a >
3849
-
3850
-
3851
- <pre ><code ><b >schema</b > <a href =" coin.md#0x1_coin_CoinAddAbortsIf " >CoinAddAbortsIf</a >< ; CoinType> ; {
3852
- amount: u64;
3853
- <b >let</b > addr = <a href =" ../../aptos-stdlib/doc/type_info.md#0x1_type_info_type_of " >type_info::type_of</a >< ; CoinType> ; ().account_address;
3854
- <b >let</b > maybe_supply = <b >global</b >< ; <a href =" coin.md#0x1_coin_CoinInfo " >CoinInfo</a >< ; CoinType> ;> ; (addr).<a href =" coin.md#0x1_coin_supply " >supply</a >;
3855
- <b >include</b > (<a href =" ../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_is_some " >option::is_some</a >(
3856
- maybe_supply
3857
- )) ==> ; <a href =" optional_aggregator.md#0x1_optional_aggregator_AddAbortsIf " >optional_aggregator::AddAbortsIf</a > { <a href =" optional_aggregator.md#0x1_optional_aggregator " >optional_aggregator</a >: <a href =" ../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_borrow " >option::borrow</a >(maybe_supply), value: amount };
3858
- }
3859
- </code ></pre >
3860
-
3861
-
3862
-
3863
-
3864
- <a id =" 0x1_coin_AbortsIfNotExistCoinInfo " ></a >
3865
-
3866
-
3867
- <pre ><code ><b >schema</b > <a href =" coin.md#0x1_coin_AbortsIfNotExistCoinInfo " >AbortsIfNotExistCoinInfo</a >< ; CoinType> ; {
3868
- <b >let</b > addr = <a href =" ../../aptos-stdlib/doc/type_info.md#0x1_type_info_type_of " >type_info::type_of</a >< ; CoinType> ; ().account_address;
3869
- <b >aborts_if</b > !<b >exists</b >< ; <a href =" coin.md#0x1_coin_CoinInfo " >CoinInfo</a >< ; CoinType> ;> ; (addr);
3870
- }
3871
- </code ></pre >
3872
-
3873
-
3874
-
3875
3883
<a id =" @Specification_1_AggregatableCoin " ></a >
3876
3884
3877
3885
### Struct ` AggregatableCoin `
@@ -4095,20 +4103,6 @@ Can only be updated by <code>@aptos_framework</code>.
4095
4103
4096
4104
4097
4105
4098
-
4099
- <a id =" 0x1_coin_DepositAbortsIf " ></a >
4100
-
4101
-
4102
- <pre ><code ><b >schema</b > <a href =" coin.md#0x1_coin_DepositAbortsIf " >DepositAbortsIf</a >< ; CoinType> ; {
4103
- account_addr: <b >address</b >;
4104
- <b >let</b > coin_store = <b >global</b >< ; <a href =" coin.md#0x1_coin_CoinStore " >CoinStore</a >< ; CoinType> ;> ; (account_addr);
4105
- <b >aborts_if</b > !<b >exists</b >< ; <a href =" coin.md#0x1_coin_CoinStore " >CoinStore</a >< ; CoinType> ;> ; (account_addr);
4106
- <b >aborts_if</b > coin_store.frozen;
4107
- }
4108
- </code ></pre >
4109
-
4110
-
4111
-
4112
4106
<a id =" @Specification_1_coin_address " ></a >
4113
4107
4114
4108
### Function ` coin_address `
@@ -4215,6 +4209,64 @@ Get address by reflection.
4215
4209
4216
4210
4217
4211
4212
+
4213
+ <a id =" 0x1_coin_spec_is_account_registered " ></a >
4214
+
4215
+
4216
+ <pre ><code ><b >fun</b > <a href =" coin.md#0x1_coin_spec_is_account_registered " >spec_is_account_registered</a >< ; CoinType> ; (account_addr: <b >address</b >): bool {
4217
+ <b >let</b > paired_metadata_opt = <a href =" coin.md#0x1_coin_spec_paired_metadata " >spec_paired_metadata</a >< ; CoinType> ; ();
4218
+ <b >exists</b >< ; <a href =" coin.md#0x1_coin_CoinStore " >CoinStore</a >< ; CoinType> ;> ; (account_addr) || (<a href =" ../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_spec_is_some " >option::spec_is_some</a >(
4219
+ paired_metadata_opt
4220
+ ) && <a href =" primary_fungible_store.md#0x1_primary_fungible_store_spec_primary_store_exists " >primary_fungible_store::spec_primary_store_exists</a >(account_addr, <a href =" ../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_spec_borrow " >option::spec_borrow</a >(paired_metadata_opt)))
4221
+ }
4222
+ </code ></pre >
4223
+
4224
+
4225
+
4226
+
4227
+ <a id =" 0x1_coin_CoinSubAbortsIf " ></a >
4228
+
4229
+
4230
+ <pre ><code ><b >schema</b > <a href =" coin.md#0x1_coin_CoinSubAbortsIf " >CoinSubAbortsIf</a >< ; CoinType> ; {
4231
+ amount: u64;
4232
+ <b >let</b > addr = <a href =" ../../aptos-stdlib/doc/type_info.md#0x1_type_info_type_of " >type_info::type_of</a >< ; CoinType> ; ().account_address;
4233
+ <b >let</b > maybe_supply = <b >global</b >< ; <a href =" coin.md#0x1_coin_CoinInfo " >CoinInfo</a >< ; CoinType> ;> ; (addr).<a href =" coin.md#0x1_coin_supply " >supply</a >;
4234
+ <b >include</b > (<a href =" ../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_is_some " >option::is_some</a >(
4235
+ maybe_supply
4236
+ )) ==> ; <a href =" optional_aggregator.md#0x1_optional_aggregator_SubAbortsIf " >optional_aggregator::SubAbortsIf</a > { <a href =" optional_aggregator.md#0x1_optional_aggregator " >optional_aggregator</a >: <a href =" ../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_borrow " >option::borrow</a >(maybe_supply), value: amount };
4237
+ }
4238
+ </code ></pre >
4239
+
4240
+
4241
+
4242
+
4243
+ <a id =" 0x1_coin_CoinAddAbortsIf " ></a >
4244
+
4245
+
4246
+ <pre ><code ><b >schema</b > <a href =" coin.md#0x1_coin_CoinAddAbortsIf " >CoinAddAbortsIf</a >< ; CoinType> ; {
4247
+ amount: u64;
4248
+ <b >let</b > addr = <a href =" ../../aptos-stdlib/doc/type_info.md#0x1_type_info_type_of " >type_info::type_of</a >< ; CoinType> ; ().account_address;
4249
+ <b >let</b > maybe_supply = <b >global</b >< ; <a href =" coin.md#0x1_coin_CoinInfo " >CoinInfo</a >< ; CoinType> ;> ; (addr).<a href =" coin.md#0x1_coin_supply " >supply</a >;
4250
+ <b >include</b > (<a href =" ../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_is_some " >option::is_some</a >(
4251
+ maybe_supply
4252
+ )) ==> ; <a href =" optional_aggregator.md#0x1_optional_aggregator_AddAbortsIf " >optional_aggregator::AddAbortsIf</a > { <a href =" optional_aggregator.md#0x1_optional_aggregator " >optional_aggregator</a >: <a href =" ../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_borrow " >option::borrow</a >(maybe_supply), value: amount };
4253
+ }
4254
+ </code ></pre >
4255
+
4256
+
4257
+
4258
+
4259
+ <a id =" 0x1_coin_AbortsIfNotExistCoinInfo " ></a >
4260
+
4261
+
4262
+ <pre ><code ><b >schema</b > <a href =" coin.md#0x1_coin_AbortsIfNotExistCoinInfo " >AbortsIfNotExistCoinInfo</a >< ; CoinType> ; {
4263
+ <b >let</b > addr = <a href =" ../../aptos-stdlib/doc/type_info.md#0x1_type_info_type_of " >type_info::type_of</a >< ; CoinType> ; ().account_address;
4264
+ <b >aborts_if</b > !<b >exists</b >< ; <a href =" coin.md#0x1_coin_CoinInfo " >CoinInfo</a >< ; CoinType> ;> ; (addr);
4265
+ }
4266
+ </code ></pre >
4267
+
4268
+
4269
+
4218
4270
<a id =" @Specification_1_name " ></a >
4219
4271
4220
4272
### Function ` name `
0 commit comments