diff --git a/aptos-move/e2e-move-tests/src/aggregator.rs b/aptos-move/e2e-move-tests/src/aggregator.rs index 2905422dbfc87..9589b1419a174 100644 --- a/aptos-move/e2e-move-tests/src/aggregator.rs +++ b/aptos-move/e2e-move-tests/src/aggregator.rs @@ -39,19 +39,14 @@ pub fn check( ) } -pub fn new( - harness: &mut MoveHarness, - account: &Account, - index: u64, - limit: u128, -) -> SignedTransaction { +pub fn new(harness: &mut MoveHarness, account: &Account, index: u64) -> SignedTransaction { harness.create_entry_function( account, str::parse("0x1::aggregator_test::new").unwrap(), vec![], vec![ bcs::to_bytes(&index).unwrap(), - bcs::to_bytes(&limit).unwrap(), + bcs::to_bytes(&u128::MAX).unwrap(), ], ) } diff --git a/aptos-move/e2e-move-tests/src/tests/aggregator.rs b/aptos-move/e2e-move-tests/src/tests/aggregator.rs index d22ffeda887b8..e547e5d0079a9 100644 --- a/aptos-move/e2e-move-tests/src/tests/aggregator.rs +++ b/aptos-move/e2e-move-tests/src/tests/aggregator.rs @@ -20,29 +20,52 @@ fn setup() -> (MoveHarness, Account) { initialize(common::test_dir_path("aggregator.data/pack")) } -#[test_case(BlockSplit::Whole)] -#[test_case(BlockSplit::SingleTxnPerBlock)] -fn test_aggregators_e2e(block_split: BlockSplit) { +#[test_case(BlockSplit::Whole, false)] +#[test_case(BlockSplit::Whole, true)] +#[test_case(BlockSplit::SingleTxnPerBlock, false)] +#[test_case(BlockSplit::SingleTxnPerBlock, true)] +fn test_aggregators_e2e(block_split: BlockSplit, upper_limit: bool) { let (mut h, acc) = setup(); let block_size = 200; // Create many aggregators with deterministic limit. let txns = (0..block_size) - .map(|i| (SUCCESS, new(&mut h, &acc, i, (i as u128) * 100000))) + .map(|i| (SUCCESS, new(&mut h, &acc, i))) .collect(); h.run_block_in_parts_and_check(block_split, txns); + if upper_limit { + let txns = (0..block_size) + .map(|i| { + ( + SUCCESS, + add(&mut h, &acc, i, u128::MAX - (i as u128) * 100000), + ) + }) + .collect(); + h.run_block_in_parts_and_check(block_split, txns); + } + // All transactions in block must fail, so values of aggregators are still 0. let failed_txns = (0..block_size) - .map(|i| match i % 2 { - 0 => ( - EAGGREGATOR_OVERFLOW, - materialize_and_add(&mut h, &acc, i, (i as u128) * 100000 + 1), - ), - _ => ( - EAGGREGATOR_UNDERFLOW, - materialize_and_sub(&mut h, &acc, i, (i as u128) * 100000 + 1), - ), + .filter_map(|i| { + if upper_limit { + match i % 2 { + 0 => Some(( + EAGGREGATOR_OVERFLOW, + materialize_and_add(&mut h, &acc, i, (i as u128) * 100000 + 1), + )), + _ => None, + } + } else { + match i % 2 { + 0 => None, + _ => Some(( + EAGGREGATOR_UNDERFLOW, + materialize_and_sub(&mut h, &acc, i, (i as u128) * 100000 + 1), + )), + } + } }) .collect(); h.run_block_in_parts_and_check(block_split, failed_txns); @@ -69,11 +92,16 @@ fn test_aggregators_e2e(block_split: BlockSplit) { // Finally, check values. let txns = (0..block_size) .map(|i| { + let offset = if upper_limit { + u128::MAX - (i as u128) * 100000 + } else { + 0 + }; (SUCCESS, match i % 4 { - 0 => check(&mut h, &acc, i, (i as u128) * 3000), - 1 => check(&mut h, &acc, i, (i as u128) * 2000), - 2 => check(&mut h, &acc, i, 0), - _ => check(&mut h, &acc, i, (i as u128) * 1000 + (i as u128)), + 0 => check(&mut h, &acc, i, offset + (i as u128) * 3000), + 1 => check(&mut h, &acc, i, offset + (i as u128) * 2000), + 2 => check(&mut h, &acc, i, offset), + _ => check(&mut h, &acc, i, offset + (i as u128) * 1000 + (i as u128)), }) }) .collect(); @@ -90,11 +118,39 @@ proptest! { })] #[test] - fn test_aggregator_lifetime(block_split in BlockSplit::arbitrary(15)) { + fn test_aggregator_lifetime_upper_limit(block_split in BlockSplit::arbitrary(15)) { let (mut h, acc) = setup(); + let offset = u128::MAX - 1500; let txns = vec![ - (SUCCESS, new(&mut h, &acc, 0, 1500)), + (SUCCESS, new(&mut h, &acc, 0)), + (SUCCESS, add(&mut h, &acc, 0, offset)), + (SUCCESS, add(&mut h, &acc, 0, 400)), // 400 + (SUCCESS, materialize(&mut h, &acc, 0)), + (SUCCESS, add(&mut h, &acc, 0, 500)), // 900 + (SUCCESS, check(&mut h, &acc, 0, offset + 900)), + (SUCCESS, materialize_and_add(&mut h, &acc, 0, 600)), // 1500 + (SUCCESS, materialize_and_sub(&mut h, &acc, 0, 600)), // 900 + (SUCCESS, check(&mut h, &acc, 0, offset + 900)), + (SUCCESS, sub_add(&mut h, &acc, 0, 200, 300)), // 1000 + (SUCCESS, check(&mut h, &acc, 0, offset + 1000)), + // These 2 transactions fail, and should have no side-effects. + (EAGGREGATOR_OVERFLOW, add_and_materialize(&mut h, &acc, 0, 501)), + (SUCCESS, check(&mut h, &acc, 0, offset + 1000)), + (SUCCESS, destroy(&mut h, &acc, 0)), + // Aggregator has been destroyed and we cannot add this delta. + (25863, add(&mut h, &acc, 0, 1)), + ]; + + h.run_block_in_parts_and_check(block_split, txns); + } + + #[test] + fn test_aggregator_lifetime_lower_limit(block_split in BlockSplit::arbitrary(15)) { + let (mut h, acc) = setup(); + + let txns = vec![ + (SUCCESS, new(&mut h, &acc, 0)), (SUCCESS, add(&mut h, &acc, 0, 400)), // 400 (SUCCESS, materialize(&mut h, &acc, 0)), (SUCCESS, add(&mut h, &acc, 0, 500)), // 900 @@ -104,8 +160,7 @@ proptest! { (SUCCESS, check(&mut h, &acc, 0, 900)), (SUCCESS, sub_add(&mut h, &acc, 0, 200, 300)), // 1000 (SUCCESS, check(&mut h, &acc, 0, 1000)), - // These 2 transactions fail, and should have no side-effects. - (EAGGREGATOR_OVERFLOW, add_and_materialize(&mut h, &acc, 0, 501)), + // transactions fails, and should have no side-effects. (EAGGREGATOR_UNDERFLOW, sub_and_materialize(&mut h, &acc, 0, 1001)), (SUCCESS, check(&mut h, &acc, 0, 1000)), (SUCCESS, destroy(&mut h, &acc, 0)), @@ -122,7 +177,7 @@ proptest! { let (mut h, acc) = setup(); let txns = vec![ - (SUCCESS, new(&mut h, &acc, 0, 600)), + (SUCCESS, new(&mut h, &acc, 0)), (SUCCESS, add(&mut h, &acc, 0, 400)), // Value dropped below zero - abort with EAGGREGATOR_UNDERFLOW. // We cannot catch it, because we don't materialize it. @@ -137,7 +192,8 @@ proptest! { let (mut h, acc) = setup(); let txns = vec![ - (SUCCESS, new(&mut h, &acc, 0, 600)), + (SUCCESS, new(&mut h, &acc, 0)), + // Underflow on materialized value leads to abort with EAGGREGATOR_UNDERFLOW. // We can catch it, because we materialize it. (EAGGREGATOR_UNDERFLOW, materialize_and_sub(&mut h, &acc, 0, 400)), @@ -148,11 +204,12 @@ proptest! { #[test] #[should_panic] - fn test_aggregator_overflow(block_split in BlockSplit::arbitrary(3)) { + fn test_aggregator_overflow(block_split in BlockSplit::arbitrary(4)) { let (mut h, acc) = setup(); let txns = vec![ - (SUCCESS, new(&mut h, &acc, 0, 600)), + (SUCCESS, new(&mut h, &acc, 0)), + (SUCCESS, add(&mut h, &acc, 0, u128::MAX - 600)), (SUCCESS, add(&mut h, &acc, 0, 400)), // Currently, this one will panic, instead of throwing this code. // We cannot catch it, because we don't materialize it. @@ -164,11 +221,12 @@ proptest! { #[test] - fn test_aggregator_materialize_overflow(block_split in BlockSplit::arbitrary(2)) { + fn test_aggregator_materialize_overflow(block_split in BlockSplit::arbitrary(3)) { let (mut h, acc) = setup(); let txns = vec![ - (SUCCESS, new(&mut h, &acc, 0, 399)), + (SUCCESS, new(&mut h, &acc, 0)), + (SUCCESS, add(&mut h, &acc, 0, u128::MAX - 399)), // Overflow on materialized value leads to abort with EAGGREGATOR_OVERFLOW. // We can catch it, because we materialize it. (EAGGREGATOR_OVERFLOW, materialize_and_add(&mut h, &acc, 0, 400)), diff --git a/aptos-move/framework/aptos-framework/doc/aggregator_factory.md b/aptos-move/framework/aptos-framework/doc/aggregator_factory.md index e29646e2d4b09..a19b106dd84f8 100644 --- a/aptos-move/framework/aptos-framework/doc/aggregator_factory.md +++ b/aptos-move/framework/aptos-framework/doc/aggregator_factory.md @@ -68,6 +68,15 @@ account can. ## Constants +<a id="0x1_aggregator_factory_MAX_U128"></a> + + + +<pre><code><b>const</b> <a href="aggregator_factory.md#0x1_aggregator_factory_MAX_U128">MAX_U128</a>: u128 = 340282366920938463463374607431768211455; +</code></pre> + + + <a id="0x1_aggregator_factory_EAGGREGATOR_FACTORY_NOT_FOUND"></a> Aggregator factory is not published yet. @@ -78,6 +87,16 @@ Aggregator factory is not published yet. +<a id="0x1_aggregator_factory_EAGG_V1_LIMIT_DEPRECATED"></a> + +Aggregator V1 only supports limit == MAX_U128 + + +<pre><code><b>const</b> <a href="aggregator_factory.md#0x1_aggregator_factory_EAGG_V1_LIMIT_DEPRECATED">EAGG_V1_LIMIT_DEPRECATED</a>: u64 = 2; +</code></pre> + + + <a id="0x1_aggregator_factory_initialize_aggregator_factory"></a> ## Function `initialize_aggregator_factory` @@ -124,6 +143,11 @@ Creates a new aggregator instance which overflows on exceeding a <code>limit</co <pre><code><b>public</b>(<b>friend</b>) <b>fun</b> <a href="aggregator_factory.md#0x1_aggregator_factory_create_aggregator_internal">create_aggregator_internal</a>(limit: u128): Aggregator <b>acquires</b> <a href="aggregator_factory.md#0x1_aggregator_factory_AggregatorFactory">AggregatorFactory</a> { + <b>assert</b>!( + limit == <a href="aggregator_factory.md#0x1_aggregator_factory_MAX_U128">MAX_U128</a>, + <a href="../../aptos-stdlib/../move-stdlib/doc/error.md#0x1_error_invalid_argument">error::invalid_argument</a>(<a href="aggregator_factory.md#0x1_aggregator_factory_EAGG_V1_LIMIT_DEPRECATED">EAGG_V1_LIMIT_DEPRECATED</a>) + ); + <b>assert</b>!( <b>exists</b><<a href="aggregator_factory.md#0x1_aggregator_factory_AggregatorFactory">AggregatorFactory</a>>(@aptos_framework), <a href="../../aptos-stdlib/../move-stdlib/doc/error.md#0x1_error_not_found">error::not_found</a>(<a href="aggregator_factory.md#0x1_aggregator_factory_EAGGREGATOR_FACTORY_NOT_FOUND">EAGGREGATOR_FACTORY_NOT_FOUND</a>) diff --git a/aptos-move/framework/aptos-framework/doc/coin.md b/aptos-move/framework/aptos-framework/doc/coin.md index 1754c634bec8a..ee6bc77fd7125 100644 --- a/aptos-move/framework/aptos-framework/doc/coin.md +++ b/aptos-move/framework/aptos-framework/doc/coin.md @@ -53,7 +53,6 @@ This module provides the foundation for typesafe Coins. - [Function `convert_and_take_paired_burn_ref`](#0x1_coin_convert_and_take_paired_burn_ref) - [Function `return_paired_burn_ref`](#0x1_coin_return_paired_burn_ref) - [Function `borrow_paired_burn_ref`](#0x1_coin_borrow_paired_burn_ref) -- [Function `initialize_supply_config`](#0x1_coin_initialize_supply_config) - [Function `allow_supply_upgrades`](#0x1_coin_allow_supply_upgrades) - [Function `calculate_amount_to_withdraw`](#0x1_coin_calculate_amount_to_withdraw) - [Function `maybe_convert_to_fungible_store`](#0x1_coin_maybe_convert_to_fungible_store) @@ -102,7 +101,6 @@ This module provides the foundation for typesafe Coins. - [Struct `AggregatableCoin`](#@Specification_1_AggregatableCoin) - [Function `coin_to_fungible_asset`](#@Specification_1_coin_to_fungible_asset) - [Function `fungible_asset_to_coin`](#@Specification_1_fungible_asset_to_coin) - - [Function `initialize_supply_config`](#@Specification_1_initialize_supply_config) - [Function `allow_supply_upgrades`](#@Specification_1_allow_supply_upgrades) - [Function `maybe_convert_to_fungible_store`](#@Specification_1_maybe_convert_to_fungible_store) - [Function `coin_address`](#@Specification_1_coin_address) @@ -270,7 +268,8 @@ Configuration that controls the behavior of total coin supply. If the field is set, coin creators are allowed to upgrade to parallelizable implementations. -<pre><code><b>struct</b> <a href="coin.md#0x1_coin_SupplyConfig">SupplyConfig</a> <b>has</b> key +<pre><code>#[deprecated] +<b>struct</b> <a href="coin.md#0x1_coin_SupplyConfig">SupplyConfig</a> <b>has</b> key </code></pre> @@ -1959,32 +1958,6 @@ Return the <code>BurnRef</code> with the hot potato receipt. -</details> - -<a id="0x1_coin_initialize_supply_config"></a> - -## Function `initialize_supply_config` - -Publishes supply configuration. Initially, upgrading is not allowed. - - -<pre><code><b>public</b>(<b>friend</b>) <b>fun</b> <a href="coin.md#0x1_coin_initialize_supply_config">initialize_supply_config</a>(aptos_framework: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>) -</code></pre> - - - -<details> -<summary>Implementation</summary> - - -<pre><code><b>public</b>(<b>friend</b>) <b>fun</b> <a href="coin.md#0x1_coin_initialize_supply_config">initialize_supply_config</a>(aptos_framework: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>) { - <a href="system_addresses.md#0x1_system_addresses_assert_aptos_framework">system_addresses::assert_aptos_framework</a>(aptos_framework); - <b>move_to</b>(aptos_framework, <a href="coin.md#0x1_coin_SupplyConfig">SupplyConfig</a> { allow_upgrades: <b>false</b> }); -} -</code></pre> - - - </details> <a id="0x1_coin_allow_supply_upgrades"></a> @@ -1995,7 +1968,7 @@ This should be called by on-chain governance to update the config and allow or disallow upgradability of total supply. -<pre><code><b>public</b> <b>fun</b> <a href="coin.md#0x1_coin_allow_supply_upgrades">allow_supply_upgrades</a>(aptos_framework: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>, allowed: bool) +<pre><code><b>public</b> <b>fun</b> <a href="coin.md#0x1_coin_allow_supply_upgrades">allow_supply_upgrades</a>(_aptos_framework: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>, _allowed: bool) </code></pre> @@ -2004,10 +1977,8 @@ or disallow upgradability of total supply. <summary>Implementation</summary> -<pre><code><b>public</b> <b>fun</b> <a href="coin.md#0x1_coin_allow_supply_upgrades">allow_supply_upgrades</a>(aptos_framework: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>, allowed: bool) <b>acquires</b> <a href="coin.md#0x1_coin_SupplyConfig">SupplyConfig</a> { - <a href="system_addresses.md#0x1_system_addresses_assert_aptos_framework">system_addresses::assert_aptos_framework</a>(aptos_framework); - <b>let</b> allow_upgrades = &<b>mut</b> <b>borrow_global_mut</b><<a href="coin.md#0x1_coin_SupplyConfig">SupplyConfig</a>>(@aptos_framework).allow_upgrades; - *allow_upgrades = allowed; +<pre><code><b>public</b> <b>fun</b> <a href="coin.md#0x1_coin_allow_supply_upgrades">allow_supply_upgrades</a>(_aptos_framework: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>, _allowed: bool) { + <b>abort</b> <a href="../../aptos-stdlib/../move-stdlib/doc/error.md#0x1_error_invalid_state">error::invalid_state</a>(<a href="coin.md#0x1_coin_ECOIN_SUPPLY_UPGRADE_NOT_SUPPORTED">ECOIN_SUPPLY_UPGRADE_NOT_SUPPORTED</a>) } </code></pre> @@ -2886,7 +2857,7 @@ Upgrade total supply to use a parallelizable implementation if it is available. -<pre><code><b>public</b> entry <b>fun</b> <a href="coin.md#0x1_coin_upgrade_supply">upgrade_supply</a><CoinType>(<a href="account.md#0x1_account">account</a>: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>) +<pre><code><b>public</b> entry <b>fun</b> <a href="coin.md#0x1_coin_upgrade_supply">upgrade_supply</a><CoinType>(_account: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>) </code></pre> @@ -2895,30 +2866,8 @@ available. <summary>Implementation</summary> -<pre><code><b>public</b> entry <b>fun</b> <a href="coin.md#0x1_coin_upgrade_supply">upgrade_supply</a><CoinType>(<a href="account.md#0x1_account">account</a>: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>) <b>acquires</b> <a href="coin.md#0x1_coin_CoinInfo">CoinInfo</a>, <a href="coin.md#0x1_coin_SupplyConfig">SupplyConfig</a> { - <b>let</b> account_addr = <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(<a href="account.md#0x1_account">account</a>); - - // Only <a href="coin.md#0x1_coin">coin</a> creators can upgrade total <a href="coin.md#0x1_coin_supply">supply</a>. - <b>assert</b>!( - <a href="coin.md#0x1_coin_coin_address">coin_address</a><CoinType>() == account_addr, - <a href="../../aptos-stdlib/../move-stdlib/doc/error.md#0x1_error_invalid_argument">error::invalid_argument</a>(<a href="coin.md#0x1_coin_ECOIN_INFO_ADDRESS_MISMATCH">ECOIN_INFO_ADDRESS_MISMATCH</a>), - ); - - // Can only succeed once on-chain governance agreed on the upgrade. - <b>assert</b>!( - <b>borrow_global</b><<a href="coin.md#0x1_coin_SupplyConfig">SupplyConfig</a>>(@aptos_framework).allow_upgrades, - <a href="../../aptos-stdlib/../move-stdlib/doc/error.md#0x1_error_permission_denied">error::permission_denied</a>(<a href="coin.md#0x1_coin_ECOIN_SUPPLY_UPGRADE_NOT_SUPPORTED">ECOIN_SUPPLY_UPGRADE_NOT_SUPPORTED</a>) - ); - - <b>let</b> maybe_supply = &<b>mut</b> <b>borrow_global_mut</b><<a href="coin.md#0x1_coin_CoinInfo">CoinInfo</a><CoinType>>(account_addr).<a href="coin.md#0x1_coin_supply">supply</a>; - <b>if</b> (<a href="../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_is_some">option::is_some</a>(maybe_supply)) { - <b>let</b> <a href="coin.md#0x1_coin_supply">supply</a> = <a href="../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_borrow_mut">option::borrow_mut</a>(maybe_supply); - - // If <a href="coin.md#0x1_coin_supply">supply</a> is tracked and the current implementation uses an integer - upgrade. - <b>if</b> (!<a href="optional_aggregator.md#0x1_optional_aggregator_is_parallelizable">optional_aggregator::is_parallelizable</a>(<a href="coin.md#0x1_coin_supply">supply</a>)) { - <a href="optional_aggregator.md#0x1_optional_aggregator_switch">optional_aggregator::switch</a>(<a href="coin.md#0x1_coin_supply">supply</a>); - } - } +<pre><code><b>public</b> entry <b>fun</b> <a href="coin.md#0x1_coin_upgrade_supply">upgrade_supply</a><CoinType>(_account: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>) { + <b>abort</b> <a href="../../aptos-stdlib/../move-stdlib/doc/error.md#0x1_error_invalid_state">error::invalid_state</a>(<a href="coin.md#0x1_coin_ECOIN_SUPPLY_UPGRADE_NOT_SUPPORTED">ECOIN_SUPPLY_UPGRADE_NOT_SUPPORTED</a>) } </code></pre> @@ -3682,46 +3631,19 @@ initialize, initialize_internal, initialize_with_parallelizable_supply; -<a id="@Specification_1_initialize_supply_config"></a> - -### Function `initialize_supply_config` - - -<pre><code><b>public</b>(<b>friend</b>) <b>fun</b> <a href="coin.md#0x1_coin_initialize_supply_config">initialize_supply_config</a>(aptos_framework: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>) -</code></pre> - - -Can only be initialized once. -Can only be published by reserved addresses. - - -<pre><code><b>let</b> aptos_addr = <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(aptos_framework); -<b>aborts_if</b> !<a href="system_addresses.md#0x1_system_addresses_is_aptos_framework_address">system_addresses::is_aptos_framework_address</a>(aptos_addr); -<b>aborts_if</b> <b>exists</b><<a href="coin.md#0x1_coin_SupplyConfig">SupplyConfig</a>>(aptos_addr); -<b>ensures</b> !<b>global</b><<a href="coin.md#0x1_coin_SupplyConfig">SupplyConfig</a>>(aptos_addr).allow_upgrades; -<b>ensures</b> <b>exists</b><<a href="coin.md#0x1_coin_SupplyConfig">SupplyConfig</a>>(aptos_addr); -</code></pre> - - - <a id="@Specification_1_allow_supply_upgrades"></a> ### Function `allow_supply_upgrades` -<pre><code><b>public</b> <b>fun</b> <a href="coin.md#0x1_coin_allow_supply_upgrades">allow_supply_upgrades</a>(aptos_framework: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>, allowed: bool) +<pre><code><b>public</b> <b>fun</b> <a href="coin.md#0x1_coin_allow_supply_upgrades">allow_supply_upgrades</a>(_aptos_framework: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>, _allowed: bool) </code></pre> Can only be updated by <code>@aptos_framework</code>. -<pre><code><b>modifies</b> <b>global</b><<a href="coin.md#0x1_coin_SupplyConfig">SupplyConfig</a>>(@aptos_framework); -<b>let</b> aptos_addr = <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(aptos_framework); -<b>aborts_if</b> !<a href="system_addresses.md#0x1_system_addresses_is_aptos_framework_address">system_addresses::is_aptos_framework_address</a>(aptos_addr); -<b>aborts_if</b> !<b>exists</b><<a href="coin.md#0x1_coin_SupplyConfig">SupplyConfig</a>>(aptos_addr); -<b>let</b> <b>post</b> allow_upgrades_post = <b>global</b><<a href="coin.md#0x1_coin_SupplyConfig">SupplyConfig</a>>(@aptos_framework); -<b>ensures</b> allow_upgrades_post.allow_upgrades == allowed; +<pre><code><b>aborts_if</b> <b>true</b>; </code></pre> @@ -4226,7 +4148,7 @@ The value of <code>zero_coin</code> must be 0. ### Function `upgrade_supply` -<pre><code><b>public</b> entry <b>fun</b> <a href="coin.md#0x1_coin_upgrade_supply">upgrade_supply</a><CoinType>(<a href="account.md#0x1_account">account</a>: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>) +<pre><code><b>public</b> entry <b>fun</b> <a href="coin.md#0x1_coin_upgrade_supply">upgrade_supply</a><CoinType>(_account: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>) </code></pre> @@ -4234,26 +4156,7 @@ The creator of <code>CoinType</code> must be <code>@aptos_framework</code>. <code><a href="coin.md#0x1_coin_SupplyConfig">SupplyConfig</a></code> allow upgrade. -<pre><code><b>let</b> account_addr = <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(<a href="account.md#0x1_account">account</a>); -<b>let</b> coin_address = <a href="../../aptos-stdlib/doc/type_info.md#0x1_type_info_type_of">type_info::type_of</a><CoinType>().account_address; -<b>aborts_if</b> coin_address != account_addr; -<b>aborts_if</b> !<b>exists</b><<a href="coin.md#0x1_coin_SupplyConfig">SupplyConfig</a>>(@aptos_framework); -// This enforces <a id="high-level-req-1.1" href="#high-level-req">high-level requirement 1</a>: -<b>aborts_if</b> !<b>exists</b><<a href="coin.md#0x1_coin_CoinInfo">CoinInfo</a><CoinType>>(account_addr); -<b>let</b> supply_config = <b>global</b><<a href="coin.md#0x1_coin_SupplyConfig">SupplyConfig</a>>(@aptos_framework); -<b>aborts_if</b> !supply_config.allow_upgrades; -<b>modifies</b> <b>global</b><<a href="coin.md#0x1_coin_CoinInfo">CoinInfo</a><CoinType>>(account_addr); -<b>let</b> maybe_supply = <b>global</b><<a href="coin.md#0x1_coin_CoinInfo">CoinInfo</a><CoinType>>(account_addr).<a href="coin.md#0x1_coin_supply">supply</a>; -<b>let</b> <a href="coin.md#0x1_coin_supply">supply</a> = <a href="../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_spec_borrow">option::spec_borrow</a>(maybe_supply); -<b>let</b> value = <a href="optional_aggregator.md#0x1_optional_aggregator_optional_aggregator_value">optional_aggregator::optional_aggregator_value</a>(<a href="coin.md#0x1_coin_supply">supply</a>); -<b>let</b> <b>post</b> post_maybe_supply = <b>global</b><<a href="coin.md#0x1_coin_CoinInfo">CoinInfo</a><CoinType>>(account_addr).<a href="coin.md#0x1_coin_supply">supply</a>; -<b>let</b> <b>post</b> post_supply = <a href="../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_spec_borrow">option::spec_borrow</a>(post_maybe_supply); -<b>let</b> <b>post</b> post_value = <a href="optional_aggregator.md#0x1_optional_aggregator_optional_aggregator_value">optional_aggregator::optional_aggregator_value</a>(post_supply); -<b>let</b> supply_no_parallel = <a href="../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_spec_is_some">option::spec_is_some</a>(maybe_supply) && - !<a href="optional_aggregator.md#0x1_optional_aggregator_is_parallelizable">optional_aggregator::is_parallelizable</a>(<a href="coin.md#0x1_coin_supply">supply</a>); -<b>aborts_if</b> supply_no_parallel && !<b>exists</b><<a href="aggregator_factory.md#0x1_aggregator_factory_AggregatorFactory">aggregator_factory::AggregatorFactory</a>>(@aptos_framework); -<b>ensures</b> supply_no_parallel ==> - <a href="optional_aggregator.md#0x1_optional_aggregator_is_parallelizable">optional_aggregator::is_parallelizable</a>(post_supply) && post_value == value; +<pre><code><b>aborts_if</b> <b>true</b>; </code></pre> diff --git a/aptos-move/framework/aptos-framework/doc/genesis.md b/aptos-move/framework/aptos-framework/doc/genesis.md index e767985fbd881..4df4a2f99b301 100644 --- a/aptos-move/framework/aptos-framework/doc/genesis.md +++ b/aptos-move/framework/aptos-framework/doc/genesis.md @@ -358,7 +358,6 @@ Genesis step 1: Initialize aptos framework account and core modules on chain. // Ensure we can create aggregators for supply, but not enable it for common <b>use</b> just yet. <a href="aggregator_factory.md#0x1_aggregator_factory_initialize_aggregator_factory">aggregator_factory::initialize_aggregator_factory</a>(&aptos_framework_account); - <a href="coin.md#0x1_coin_initialize_supply_config">coin::initialize_supply_config</a>(&aptos_framework_account); <a href="chain_id.md#0x1_chain_id_initialize">chain_id::initialize</a>(&aptos_framework_account, <a href="chain_id.md#0x1_chain_id">chain_id</a>); <a href="reconfiguration.md#0x1_reconfiguration_initialize">reconfiguration::initialize</a>(&aptos_framework_account); diff --git a/aptos-move/framework/aptos-framework/doc/optional_aggregator.md b/aptos-move/framework/aptos-framework/doc/optional_aggregator.md index 309ee697c2448..cdae8a1fd9bc6 100644 --- a/aptos-move/framework/aptos-framework/doc/optional_aggregator.md +++ b/aptos-move/framework/aptos-framework/doc/optional_aggregator.md @@ -18,9 +18,6 @@ aggregator (parallelizable) or via normal integers. - [Function `destroy_integer`](#0x1_optional_aggregator_destroy_integer) - [Function `new`](#0x1_optional_aggregator_new) - [Function `switch`](#0x1_optional_aggregator_switch) -- [Function `switch_and_zero_out`](#0x1_optional_aggregator_switch_and_zero_out) -- [Function `switch_to_integer_and_zero_out`](#0x1_optional_aggregator_switch_to_integer_and_zero_out) -- [Function `switch_to_aggregator_and_zero_out`](#0x1_optional_aggregator_switch_to_aggregator_and_zero_out) - [Function `destroy`](#0x1_optional_aggregator_destroy) - [Function `destroy_optional_aggregator`](#0x1_optional_aggregator_destroy_optional_aggregator) - [Function `destroy_optional_integer`](#0x1_optional_aggregator_destroy_optional_integer) @@ -40,9 +37,6 @@ aggregator (parallelizable) or via normal integers. - [Function `destroy_integer`](#@Specification_1_destroy_integer) - [Function `new`](#@Specification_1_new) - [Function `switch`](#@Specification_1_switch) - - [Function `switch_and_zero_out`](#@Specification_1_switch_and_zero_out) - - [Function `switch_to_integer_and_zero_out`](#@Specification_1_switch_to_integer_and_zero_out) - - [Function `switch_to_aggregator_and_zero_out`](#@Specification_1_switch_to_aggregator_and_zero_out) - [Function `destroy`](#@Specification_1_destroy) - [Function `destroy_optional_aggregator`](#@Specification_1_destroy_optional_aggregator) - [Function `destroy_optional_integer`](#@Specification_1_destroy_optional_integer) @@ -152,6 +146,16 @@ Aggregator feature is not supported. Raised by native code. +<a id="0x1_optional_aggregator_ESWITCH_DEPRECATED"></a> + +OptionalAggregator (Agg V1) switch not supported any more + + +<pre><code><b>const</b> <a href="optional_aggregator.md#0x1_optional_aggregator_ESWITCH_DEPRECATED">ESWITCH_DEPRECATED</a>: u64 = 3; +</code></pre> + + + <a id="0x1_optional_aggregator_new_integer"></a> ## Function `new_integer` @@ -352,98 +356,7 @@ Creates a new optional aggregator. Switches between parallelizable and non-parallelizable implementations. -<pre><code><b>public</b> <b>fun</b> <a href="optional_aggregator.md#0x1_optional_aggregator_switch">switch</a>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>: &<b>mut</b> <a href="optional_aggregator.md#0x1_optional_aggregator_OptionalAggregator">optional_aggregator::OptionalAggregator</a>) -</code></pre> - - - -<details> -<summary>Implementation</summary> - - -<pre><code><b>public</b> <b>fun</b> <a href="optional_aggregator.md#0x1_optional_aggregator_switch">switch</a>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>: &<b>mut</b> <a href="optional_aggregator.md#0x1_optional_aggregator_OptionalAggregator">OptionalAggregator</a>) { - <b>let</b> value = <a href="optional_aggregator.md#0x1_optional_aggregator_read">read</a>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>); - <a href="optional_aggregator.md#0x1_optional_aggregator_switch_and_zero_out">switch_and_zero_out</a>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>); - <a href="optional_aggregator.md#0x1_optional_aggregator_add">add</a>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>, value); -} -</code></pre> - - - -</details> - -<a id="0x1_optional_aggregator_switch_and_zero_out"></a> - -## Function `switch_and_zero_out` - -Switches between parallelizable and non-parallelizable implementations, setting -the value of the new optional aggregator to zero. - - -<pre><code><b>fun</b> <a href="optional_aggregator.md#0x1_optional_aggregator_switch_and_zero_out">switch_and_zero_out</a>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>: &<b>mut</b> <a href="optional_aggregator.md#0x1_optional_aggregator_OptionalAggregator">optional_aggregator::OptionalAggregator</a>) -</code></pre> - - - -<details> -<summary>Implementation</summary> - - -<pre><code><b>fun</b> <a href="optional_aggregator.md#0x1_optional_aggregator_switch_and_zero_out">switch_and_zero_out</a>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>: &<b>mut</b> <a href="optional_aggregator.md#0x1_optional_aggregator_OptionalAggregator">OptionalAggregator</a>) { - <b>if</b> (<a href="optional_aggregator.md#0x1_optional_aggregator_is_parallelizable">is_parallelizable</a>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>)) { - <a href="optional_aggregator.md#0x1_optional_aggregator_switch_to_integer_and_zero_out">switch_to_integer_and_zero_out</a>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>); - } <b>else</b> { - <a href="optional_aggregator.md#0x1_optional_aggregator_switch_to_aggregator_and_zero_out">switch_to_aggregator_and_zero_out</a>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>); - } -} -</code></pre> - - - -</details> - -<a id="0x1_optional_aggregator_switch_to_integer_and_zero_out"></a> - -## Function `switch_to_integer_and_zero_out` - -Switches from parallelizable to non-parallelizable implementation, zero-initializing -the value. - - -<pre><code><b>fun</b> <a href="optional_aggregator.md#0x1_optional_aggregator_switch_to_integer_and_zero_out">switch_to_integer_and_zero_out</a>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>: &<b>mut</b> <a href="optional_aggregator.md#0x1_optional_aggregator_OptionalAggregator">optional_aggregator::OptionalAggregator</a>): u128 -</code></pre> - - - -<details> -<summary>Implementation</summary> - - -<pre><code><b>fun</b> <a href="optional_aggregator.md#0x1_optional_aggregator_switch_to_integer_and_zero_out">switch_to_integer_and_zero_out</a>( - <a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>: &<b>mut</b> <a href="optional_aggregator.md#0x1_optional_aggregator_OptionalAggregator">OptionalAggregator</a> -): u128 { - <b>let</b> <a href="aggregator.md#0x1_aggregator">aggregator</a> = <a href="../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_extract">option::extract</a>(&<b>mut</b> <a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>.<a href="aggregator.md#0x1_aggregator">aggregator</a>); - <b>let</b> limit = <a href="aggregator.md#0x1_aggregator_limit">aggregator::limit</a>(&<a href="aggregator.md#0x1_aggregator">aggregator</a>); - <a href="aggregator.md#0x1_aggregator_destroy">aggregator::destroy</a>(<a href="aggregator.md#0x1_aggregator">aggregator</a>); - <b>let</b> integer = <a href="optional_aggregator.md#0x1_optional_aggregator_new_integer">new_integer</a>(limit); - <a href="../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_fill">option::fill</a>(&<b>mut</b> <a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>.integer, integer); - limit -} -</code></pre> - - - -</details> - -<a id="0x1_optional_aggregator_switch_to_aggregator_and_zero_out"></a> - -## Function `switch_to_aggregator_and_zero_out` - -Switches from non-parallelizable to parallelizable implementation, zero-initializing -the value. - - -<pre><code><b>fun</b> <a href="optional_aggregator.md#0x1_optional_aggregator_switch_to_aggregator_and_zero_out">switch_to_aggregator_and_zero_out</a>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>: &<b>mut</b> <a href="optional_aggregator.md#0x1_optional_aggregator_OptionalAggregator">optional_aggregator::OptionalAggregator</a>): u128 +<pre><code><b>public</b> <b>fun</b> <a href="optional_aggregator.md#0x1_optional_aggregator_switch">switch</a>(_optional_aggregator: &<b>mut</b> <a href="optional_aggregator.md#0x1_optional_aggregator_OptionalAggregator">optional_aggregator::OptionalAggregator</a>) </code></pre> @@ -452,15 +365,8 @@ the value. <summary>Implementation</summary> -<pre><code><b>fun</b> <a href="optional_aggregator.md#0x1_optional_aggregator_switch_to_aggregator_and_zero_out">switch_to_aggregator_and_zero_out</a>( - <a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>: &<b>mut</b> <a href="optional_aggregator.md#0x1_optional_aggregator_OptionalAggregator">OptionalAggregator</a> -): u128 { - <b>let</b> integer = <a href="../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_extract">option::extract</a>(&<b>mut</b> <a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>.integer); - <b>let</b> limit = <a href="optional_aggregator.md#0x1_optional_aggregator_limit">limit</a>(&integer); - <a href="optional_aggregator.md#0x1_optional_aggregator_destroy_integer">destroy_integer</a>(integer); - <b>let</b> <a href="aggregator.md#0x1_aggregator">aggregator</a> = <a href="aggregator_factory.md#0x1_aggregator_factory_create_aggregator_internal">aggregator_factory::create_aggregator_internal</a>(limit); - <a href="../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_fill">option::fill</a>(&<b>mut</b> <a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>.<a href="aggregator.md#0x1_aggregator">aggregator</a>, <a href="aggregator.md#0x1_aggregator">aggregator</a>); - limit +<pre><code><b>public</b> <b>fun</b> <a href="optional_aggregator.md#0x1_optional_aggregator_switch">switch</a>(_optional_aggregator: &<b>mut</b> <a href="optional_aggregator.md#0x1_optional_aggregator_OptionalAggregator">OptionalAggregator</a>) { + <b>abort</b> <a href="../../aptos-stdlib/../move-stdlib/doc/error.md#0x1_error_invalid_state">error::invalid_state</a>(<a href="optional_aggregator.md#0x1_optional_aggregator_ESWITCH_DEPRECATED">ESWITCH_DEPRECATED</a>) } </code></pre> @@ -896,89 +802,13 @@ Check for overflow. ### Function `switch` -<pre><code><b>public</b> <b>fun</b> <a href="optional_aggregator.md#0x1_optional_aggregator_switch">switch</a>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>: &<b>mut</b> <a href="optional_aggregator.md#0x1_optional_aggregator_OptionalAggregator">optional_aggregator::OptionalAggregator</a>) -</code></pre> - - - - -<pre><code><b>let</b> vec_ref = <a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>.integer.vec; -<b>aborts_if</b> <a href="optional_aggregator.md#0x1_optional_aggregator_is_parallelizable">is_parallelizable</a>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>) && len(vec_ref) != 0; -<b>aborts_if</b> !<a href="optional_aggregator.md#0x1_optional_aggregator_is_parallelizable">is_parallelizable</a>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>) && len(vec_ref) == 0; -<b>aborts_if</b> !<a href="optional_aggregator.md#0x1_optional_aggregator_is_parallelizable">is_parallelizable</a>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>) && !<b>exists</b><<a href="aggregator_factory.md#0x1_aggregator_factory_AggregatorFactory">aggregator_factory::AggregatorFactory</a>>(@aptos_framework); -<b>ensures</b> <a href="optional_aggregator.md#0x1_optional_aggregator_optional_aggregator_value">optional_aggregator_value</a>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>) == <a href="optional_aggregator.md#0x1_optional_aggregator_optional_aggregator_value">optional_aggregator_value</a>(<b>old</b>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>)); -</code></pre> - - - -<a id="@Specification_1_switch_and_zero_out"></a> - -### Function `switch_and_zero_out` - - -<pre><code><b>fun</b> <a href="optional_aggregator.md#0x1_optional_aggregator_switch_and_zero_out">switch_and_zero_out</a>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>: &<b>mut</b> <a href="optional_aggregator.md#0x1_optional_aggregator_OptionalAggregator">optional_aggregator::OptionalAggregator</a>) +<pre><code><b>public</b> <b>fun</b> <a href="optional_aggregator.md#0x1_optional_aggregator_switch">switch</a>(_optional_aggregator: &<b>mut</b> <a href="optional_aggregator.md#0x1_optional_aggregator_OptionalAggregator">optional_aggregator::OptionalAggregator</a>) </code></pre> -Option<Integer> does not exist When Option<Aggregator> exists. -Option<Integer> exists when Option<Aggregator> does not exist. -The AggregatorFactory is under the @aptos_framework when Option<Aggregator> does not exist. -<pre><code><b>let</b> vec_ref = <a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>.integer.vec; -<b>aborts_if</b> <a href="optional_aggregator.md#0x1_optional_aggregator_is_parallelizable">is_parallelizable</a>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>) && len(vec_ref) != 0; -<b>aborts_if</b> !<a href="optional_aggregator.md#0x1_optional_aggregator_is_parallelizable">is_parallelizable</a>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>) && len(vec_ref) == 0; -<b>aborts_if</b> !<a href="optional_aggregator.md#0x1_optional_aggregator_is_parallelizable">is_parallelizable</a>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>) && !<b>exists</b><<a href="aggregator_factory.md#0x1_aggregator_factory_AggregatorFactory">aggregator_factory::AggregatorFactory</a>>(@aptos_framework); -// This enforces <a id="high-level-req-3" href="#high-level-req">high-level requirement 3</a>: -<b>ensures</b> <a href="optional_aggregator.md#0x1_optional_aggregator_is_parallelizable">is_parallelizable</a>(<b>old</b>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>)) ==> !<a href="optional_aggregator.md#0x1_optional_aggregator_is_parallelizable">is_parallelizable</a>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>); -<b>ensures</b> !<a href="optional_aggregator.md#0x1_optional_aggregator_is_parallelizable">is_parallelizable</a>(<b>old</b>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>)) ==> <a href="optional_aggregator.md#0x1_optional_aggregator_is_parallelizable">is_parallelizable</a>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>); -<b>ensures</b> <a href="optional_aggregator.md#0x1_optional_aggregator_optional_aggregator_value">optional_aggregator_value</a>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>) == 0; -</code></pre> - - - -<a id="@Specification_1_switch_to_integer_and_zero_out"></a> - -### Function `switch_to_integer_and_zero_out` - - -<pre><code><b>fun</b> <a href="optional_aggregator.md#0x1_optional_aggregator_switch_to_integer_and_zero_out">switch_to_integer_and_zero_out</a>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>: &<b>mut</b> <a href="optional_aggregator.md#0x1_optional_aggregator_OptionalAggregator">optional_aggregator::OptionalAggregator</a>): u128 -</code></pre> - - -The aggregator exists and the integer dosex not exist when Switches from parallelizable to non-parallelizable implementation. - - -<pre><code><b>let</b> limit = <a href="aggregator.md#0x1_aggregator_spec_get_limit">aggregator::spec_get_limit</a>(<a href="../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_borrow">option::borrow</a>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>.<a href="aggregator.md#0x1_aggregator">aggregator</a>)); -<b>aborts_if</b> len(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>.<a href="aggregator.md#0x1_aggregator">aggregator</a>.vec) == 0; -<b>aborts_if</b> len(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>.integer.vec) != 0; -<b>ensures</b> !<a href="optional_aggregator.md#0x1_optional_aggregator_is_parallelizable">is_parallelizable</a>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>); -<b>ensures</b> <a href="../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_borrow">option::borrow</a>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>.integer).limit == limit; -<b>ensures</b> <a href="../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_borrow">option::borrow</a>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>.integer).value == 0; -</code></pre> - - - -<a id="@Specification_1_switch_to_aggregator_and_zero_out"></a> - -### Function `switch_to_aggregator_and_zero_out` - - -<pre><code><b>fun</b> <a href="optional_aggregator.md#0x1_optional_aggregator_switch_to_aggregator_and_zero_out">switch_to_aggregator_and_zero_out</a>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>: &<b>mut</b> <a href="optional_aggregator.md#0x1_optional_aggregator_OptionalAggregator">optional_aggregator::OptionalAggregator</a>): u128 -</code></pre> - - -The integer exists and the aggregator does not exist when Switches from non-parallelizable to parallelizable implementation. -The AggregatorFactory is under the @aptos_framework. - - -<pre><code><b>let</b> limit = <a href="../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_borrow">option::borrow</a>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>.integer).limit; -<b>aborts_if</b> len(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>.integer.vec) == 0; -<b>aborts_if</b> !<b>exists</b><<a href="aggregator_factory.md#0x1_aggregator_factory_AggregatorFactory">aggregator_factory::AggregatorFactory</a>>(@aptos_framework); -<b>aborts_if</b> len(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>.<a href="aggregator.md#0x1_aggregator">aggregator</a>.vec) != 0; -<b>ensures</b> <a href="optional_aggregator.md#0x1_optional_aggregator_is_parallelizable">is_parallelizable</a>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>); -<b>ensures</b> <a href="aggregator.md#0x1_aggregator_spec_get_limit">aggregator::spec_get_limit</a>(<a href="../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_borrow">option::borrow</a>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>.<a href="aggregator.md#0x1_aggregator">aggregator</a>)) == limit; -<b>ensures</b> <a href="aggregator.md#0x1_aggregator_spec_aggregator_get_val">aggregator::spec_aggregator_get_val</a>(<a href="../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_borrow">option::borrow</a>(<a href="optional_aggregator.md#0x1_optional_aggregator">optional_aggregator</a>.<a href="aggregator.md#0x1_aggregator">aggregator</a>)) == 0; +<pre><code><b>aborts_if</b> <b>true</b>; </code></pre> diff --git a/aptos-move/framework/aptos-framework/sources/aggregator/aggregator_factory.move b/aptos-move/framework/aptos-framework/sources/aggregator/aggregator_factory.move index 7ec4dad805e2a..e70397551b61e 100644 --- a/aptos-move/framework/aptos-framework/sources/aggregator/aggregator_factory.move +++ b/aptos-move/framework/aptos-framework/sources/aggregator/aggregator_factory.move @@ -16,6 +16,11 @@ module aptos_framework::aggregator_factory { /// Aggregator factory is not published yet. const EAGGREGATOR_FACTORY_NOT_FOUND: u64 = 1; + /// Aggregator V1 only supports limit == MAX_U128 + const EAGG_V1_LIMIT_DEPRECATED: u64 = 2; + + const MAX_U128: u128 = 340282366920938463463374607431768211455; + /// Creates new aggregators. Used to control the numbers of aggregators in the /// system and who can create them. At the moment, only Aptos Framework (0x1) /// account can. @@ -34,6 +39,11 @@ module aptos_framework::aggregator_factory { /// Creates a new aggregator instance which overflows on exceeding a `limit`. public(friend) fun create_aggregator_internal(limit: u128): Aggregator acquires AggregatorFactory { + assert!( + limit == MAX_U128, + error::invalid_argument(EAGG_V1_LIMIT_DEPRECATED) + ); + assert!( exists<AggregatorFactory>(@aptos_framework), error::not_found(EAGGREGATOR_FACTORY_NOT_FOUND) diff --git a/aptos-move/framework/aptos-framework/sources/aggregator/optional_aggregator.move b/aptos-move/framework/aptos-framework/sources/aggregator/optional_aggregator.move index f3a545600edbc..8fea44651a14b 100644 --- a/aptos-move/framework/aptos-framework/sources/aggregator/optional_aggregator.move +++ b/aptos-move/framework/aptos-framework/sources/aggregator/optional_aggregator.move @@ -16,6 +16,9 @@ module aptos_framework::optional_aggregator { /// Aggregator feature is not supported. Raised by native code. const EAGGREGATOR_UNDERFLOW: u64 = 2; + /// OptionalAggregator (Agg V1) switch not supported any more + const ESWITCH_DEPRECATED: u64 = 3; + /// Wrapper around integer with a custom overflow limit. Supports add, subtract and read just like `Aggregator`. struct Integer has store { value: u128, @@ -84,46 +87,8 @@ module aptos_framework::optional_aggregator { } /// Switches between parallelizable and non-parallelizable implementations. - public fun switch(optional_aggregator: &mut OptionalAggregator) { - let value = read(optional_aggregator); - switch_and_zero_out(optional_aggregator); - add(optional_aggregator, value); - } - - /// Switches between parallelizable and non-parallelizable implementations, setting - /// the value of the new optional aggregator to zero. - fun switch_and_zero_out(optional_aggregator: &mut OptionalAggregator) { - if (is_parallelizable(optional_aggregator)) { - switch_to_integer_and_zero_out(optional_aggregator); - } else { - switch_to_aggregator_and_zero_out(optional_aggregator); - } - } - - /// Switches from parallelizable to non-parallelizable implementation, zero-initializing - /// the value. - fun switch_to_integer_and_zero_out( - optional_aggregator: &mut OptionalAggregator - ): u128 { - let aggregator = option::extract(&mut optional_aggregator.aggregator); - let limit = aggregator::limit(&aggregator); - aggregator::destroy(aggregator); - let integer = new_integer(limit); - option::fill(&mut optional_aggregator.integer, integer); - limit - } - - /// Switches from non-parallelizable to parallelizable implementation, zero-initializing - /// the value. - fun switch_to_aggregator_and_zero_out( - optional_aggregator: &mut OptionalAggregator - ): u128 { - let integer = option::extract(&mut optional_aggregator.integer); - let limit = limit(&integer); - destroy_integer(integer); - let aggregator = aggregator_factory::create_aggregator_internal(limit); - option::fill(&mut optional_aggregator.aggregator, aggregator); - limit + public fun switch(_optional_aggregator: &mut OptionalAggregator) { + abort error::invalid_state(ESWITCH_DEPRECATED) } /// Destroys optional aggregator. @@ -192,7 +157,7 @@ module aptos_framework::optional_aggregator { } #[test(account = @aptos_framework)] - fun optional_aggregator_test(account: signer) { + fun optional_aggregator_test_integer(account: signer) { aggregator_factory::initialize_aggregator_factory(&account); let aggregator = new(30, false); @@ -204,9 +169,13 @@ module aptos_framework::optional_aggregator { sub(&mut aggregator, 10); assert!(read(&aggregator) == 5, 0); + } + + #[test(account = @aptos_framework)] + fun optional_aggregator_test_aggregator(account: signer) { + aggregator_factory::initialize_aggregator_factory(&account); + let aggregator = new(5, true); - // Switch to parallelizable aggregator and check the value is preserved. - switch(&mut aggregator); assert!(is_parallelizable(&aggregator), 0); assert!(read(&aggregator) == 5, 0); diff --git a/aptos-move/framework/aptos-framework/sources/aggregator/optional_aggregator.spec.move b/aptos-move/framework/aptos-framework/sources/aggregator/optional_aggregator.spec.move index bb8e29768447f..c71df72b5cabf 100644 --- a/aptos-move/framework/aptos-framework/sources/aggregator/optional_aggregator.spec.move +++ b/aptos-move/framework/aptos-framework/sources/aggregator/optional_aggregator.spec.move @@ -105,12 +105,8 @@ spec aptos_framework::optional_aggregator { (value > (option::borrow(optional_aggregator.integer).limit - option::borrow(optional_aggregator.integer).value)); } - spec switch(optional_aggregator: &mut OptionalAggregator) { - let vec_ref = optional_aggregator.integer.vec; - aborts_if is_parallelizable(optional_aggregator) && len(vec_ref) != 0; - aborts_if !is_parallelizable(optional_aggregator) && len(vec_ref) == 0; - aborts_if !is_parallelizable(optional_aggregator) && !exists<aggregator_factory::AggregatorFactory>(@aptos_framework); - ensures optional_aggregator_value(optional_aggregator) == optional_aggregator_value(old(optional_aggregator)); + spec switch(_optional_aggregator: &mut OptionalAggregator) { + aborts_if true; } spec sub_integer(integer: &mut Integer, value: u128) { @@ -126,46 +122,6 @@ spec aptos_framework::optional_aggregator { ensures optional_aggregator_value(result) <= optional_aggregator_limit(result); } - /// Option<Integer> does not exist When Option<Aggregator> exists. - /// Option<Integer> exists when Option<Aggregator> does not exist. - /// The AggregatorFactory is under the @aptos_framework when Option<Aggregator> does not exist. - spec switch_and_zero_out(optional_aggregator: &mut OptionalAggregator) { - let vec_ref = optional_aggregator.integer.vec; - aborts_if is_parallelizable(optional_aggregator) && len(vec_ref) != 0; - aborts_if !is_parallelizable(optional_aggregator) && len(vec_ref) == 0; - aborts_if !is_parallelizable(optional_aggregator) && !exists<aggregator_factory::AggregatorFactory>(@aptos_framework); - /// [high-level-req-3] - ensures is_parallelizable(old(optional_aggregator)) ==> !is_parallelizable(optional_aggregator); - ensures !is_parallelizable(old(optional_aggregator)) ==> is_parallelizable(optional_aggregator); - ensures optional_aggregator_value(optional_aggregator) == 0; - } - - /// The aggregator exists and the integer dosex not exist when Switches from parallelizable to non-parallelizable implementation. - spec switch_to_integer_and_zero_out( - optional_aggregator: &mut OptionalAggregator - ): u128 { - let limit = aggregator::spec_get_limit(option::borrow(optional_aggregator.aggregator)); - aborts_if len(optional_aggregator.aggregator.vec) == 0; - aborts_if len(optional_aggregator.integer.vec) != 0; - ensures !is_parallelizable(optional_aggregator); - ensures option::borrow(optional_aggregator.integer).limit == limit; - ensures option::borrow(optional_aggregator.integer).value == 0; - } - - /// The integer exists and the aggregator does not exist when Switches from non-parallelizable to parallelizable implementation. - /// The AggregatorFactory is under the @aptos_framework. - spec switch_to_aggregator_and_zero_out( - optional_aggregator: &mut OptionalAggregator - ): u128 { - let limit = option::borrow(optional_aggregator.integer).limit; - aborts_if len(optional_aggregator.integer.vec) == 0; - aborts_if !exists<aggregator_factory::AggregatorFactory>(@aptos_framework); - aborts_if len(optional_aggregator.aggregator.vec) != 0; - ensures is_parallelizable(optional_aggregator); - ensures aggregator::spec_get_limit(option::borrow(optional_aggregator.aggregator)) == limit; - ensures aggregator::spec_aggregator_get_val(option::borrow(optional_aggregator.aggregator)) == 0; - } - spec destroy(optional_aggregator: OptionalAggregator) { aborts_if is_parallelizable(optional_aggregator) && len(optional_aggregator.integer.vec) != 0; aborts_if !is_parallelizable(optional_aggregator) && len(optional_aggregator.integer.vec) == 0; diff --git a/aptos-move/framework/aptos-framework/sources/coin.move b/aptos-move/framework/aptos-framework/sources/coin.move index ee4382be75e4e..8823ffd27aa88 100644 --- a/aptos-move/framework/aptos-framework/sources/coin.move +++ b/aptos-move/framework/aptos-framework/sources/coin.move @@ -144,6 +144,7 @@ module aptos_framework::coin { /// Maximum possible coin supply. const MAX_U128: u128 = 340282366920938463463374607431768211455; + #[deprecated] /// Configuration that controls the behavior of total coin supply. If the field /// is set, coin creators are allowed to upgrade to parallelizable implementations. struct SupplyConfig has key { @@ -541,18 +542,10 @@ module aptos_framework::coin { // Total supply config // - /// Publishes supply configuration. Initially, upgrading is not allowed. - public(friend) fun initialize_supply_config(aptos_framework: &signer) { - system_addresses::assert_aptos_framework(aptos_framework); - move_to(aptos_framework, SupplyConfig { allow_upgrades: false }); - } - /// This should be called by on-chain governance to update the config and allow /// or disallow upgradability of total supply. - public fun allow_supply_upgrades(aptos_framework: &signer, allowed: bool) acquires SupplyConfig { - system_addresses::assert_aptos_framework(aptos_framework); - let allow_upgrades = &mut borrow_global_mut<SupplyConfig>(@aptos_framework).allow_upgrades; - *allow_upgrades = allowed; + public fun allow_supply_upgrades(_aptos_framework: &signer, _allowed: bool) { + abort error::invalid_state(ECOIN_SUPPLY_UPGRADE_NOT_SUPPORTED) } inline fun calculate_amount_to_withdraw<CoinType>( @@ -927,30 +920,8 @@ module aptos_framework::coin { /// Upgrade total supply to use a parallelizable implementation if it is /// available. - public entry fun upgrade_supply<CoinType>(account: &signer) acquires CoinInfo, SupplyConfig { - let account_addr = signer::address_of(account); - - // Only coin creators can upgrade total supply. - assert!( - coin_address<CoinType>() == account_addr, - error::invalid_argument(ECOIN_INFO_ADDRESS_MISMATCH), - ); - - // Can only succeed once on-chain governance agreed on the upgrade. - assert!( - borrow_global<SupplyConfig>(@aptos_framework).allow_upgrades, - error::permission_denied(ECOIN_SUPPLY_UPGRADE_NOT_SUPPORTED) - ); - - let maybe_supply = &mut borrow_global_mut<CoinInfo<CoinType>>(account_addr).supply; - if (option::is_some(maybe_supply)) { - let supply = option::borrow_mut(maybe_supply); - - // If supply is tracked and the current implementation uses an integer - upgrade. - if (!optional_aggregator::is_parallelizable(supply)) { - optional_aggregator::switch(supply); - } - } + public entry fun upgrade_supply<CoinType>(_account: &signer) { + abort error::invalid_state(ECOIN_SUPPLY_UPGRADE_NOT_SUPPORTED) } /// Creates a new Coin with given `CoinType` and returns minting/freezing/burning capabilities. @@ -1708,50 +1679,6 @@ module aptos_framework::coin { optional_aggregator::sub(supply, 1); } - #[test(framework = @aptos_framework)] - #[expected_failure(abort_code = 0x5000B, location = aptos_framework::coin)] - fun test_supply_upgrade_fails(framework: signer) acquires CoinInfo, SupplyConfig { - initialize_supply_config(&framework); - aggregator_factory::initialize_aggregator_factory_for_test(&framework); - initialize_with_integer(&framework); - - let maybe_supply = &mut borrow_global_mut<CoinInfo<FakeMoney>>(coin_address<FakeMoney>()).supply; - let supply = option::borrow_mut(maybe_supply); - - // Supply should be non-parallelizable. - assert!(!optional_aggregator::is_parallelizable(supply), 0); - - optional_aggregator::add(supply, 100); - optional_aggregator::sub(supply, 50); - optional_aggregator::add(supply, 950); - assert!(optional_aggregator::read(supply) == 1000, 0); - - upgrade_supply<FakeMoney>(&framework); - } - - #[test(framework = @aptos_framework)] - fun test_supply_upgrade(framework: signer) acquires CoinInfo, SupplyConfig { - initialize_supply_config(&framework); - aggregator_factory::initialize_aggregator_factory_for_test(&framework); - initialize_with_integer(&framework); - - // Ensure we have a non-parellelizable non-zero supply. - let maybe_supply = &mut borrow_global_mut<CoinInfo<FakeMoney>>(coin_address<FakeMoney>()).supply; - let supply = option::borrow_mut(maybe_supply); - assert!(!optional_aggregator::is_parallelizable(supply), 0); - optional_aggregator::add(supply, 100); - - // Upgrade. - allow_supply_upgrades(&framework, true); - upgrade_supply<FakeMoney>(&framework); - - // Check supply again. - let maybe_supply = &mut borrow_global_mut<CoinInfo<FakeMoney>>(coin_address<FakeMoney>()).supply; - let supply = option::borrow_mut(maybe_supply); - assert!(optional_aggregator::is_parallelizable(supply), 0); - assert!(optional_aggregator::read(supply) == 100, 0); - } - #[test_only] fun destroy_aggregatable_coin_for_test<CoinType>(aggregatable_coin: AggregatableCoin<CoinType>) { let AggregatableCoin { value } = aggregatable_coin; diff --git a/aptos-move/framework/aptos-framework/sources/coin.spec.move b/aptos-move/framework/aptos-framework/sources/coin.spec.move index 32bdc6645b3de..7033b42589b7f 100644 --- a/aptos-move/framework/aptos-framework/sources/coin.spec.move +++ b/aptos-move/framework/aptos-framework/sources/coin.spec.move @@ -119,24 +119,9 @@ spec aptos_framework::coin { ensures [abstract] result == type_info::type_of<CoinType>().account_address; } - /// Can only be initialized once. - /// Can only be published by reserved addresses. - spec initialize_supply_config(aptos_framework: &signer) { - let aptos_addr = signer::address_of(aptos_framework); - aborts_if !system_addresses::is_aptos_framework_address(aptos_addr); - aborts_if exists<SupplyConfig>(aptos_addr); - ensures !global<SupplyConfig>(aptos_addr).allow_upgrades; - ensures exists<SupplyConfig>(aptos_addr); - } - /// Can only be updated by `@aptos_framework`. - spec allow_supply_upgrades(aptos_framework: &signer, allowed: bool) { - modifies global<SupplyConfig>(@aptos_framework); - let aptos_addr = signer::address_of(aptos_framework); - aborts_if !system_addresses::is_aptos_framework_address(aptos_addr); - aborts_if !exists<SupplyConfig>(aptos_addr); - let post allow_upgrades_post = global<SupplyConfig>(@aptos_framework); - ensures allow_upgrades_post.allow_upgrades == allowed; + spec allow_supply_upgrades(_aptos_framework: &signer, _allowed: bool) { + aborts_if true; } spec balance<CoinType>(owner: address): u64 { @@ -394,32 +379,8 @@ spec aptos_framework::coin { /// The creator of `CoinType` must be `@aptos_framework`. /// `SupplyConfig` allow upgrade. - spec upgrade_supply<CoinType>(account: &signer) { - let account_addr = signer::address_of(account); - let coin_address = type_info::type_of<CoinType>().account_address; - aborts_if coin_address != account_addr; - aborts_if !exists<SupplyConfig>(@aptos_framework); - /// [high-level-req-1.1] - aborts_if !exists<CoinInfo<CoinType>>(account_addr); - - let supply_config = global<SupplyConfig>(@aptos_framework); - aborts_if !supply_config.allow_upgrades; - modifies global<CoinInfo<CoinType>>(account_addr); - - let maybe_supply = global<CoinInfo<CoinType>>(account_addr).supply; - let supply = option::spec_borrow(maybe_supply); - let value = optional_aggregator::optional_aggregator_value(supply); - - let post post_maybe_supply = global<CoinInfo<CoinType>>(account_addr).supply; - let post post_supply = option::spec_borrow(post_maybe_supply); - let post post_value = optional_aggregator::optional_aggregator_value(post_supply); - - let supply_no_parallel = option::spec_is_some(maybe_supply) && - !optional_aggregator::is_parallelizable(supply); - - aborts_if supply_no_parallel && !exists<aggregator_factory::AggregatorFactory>(@aptos_framework); - ensures supply_no_parallel ==> - optional_aggregator::is_parallelizable(post_supply) && post_value == value; + spec upgrade_supply<CoinType>(_account: &signer) { + aborts_if true; } spec initialize { diff --git a/aptos-move/framework/aptos-framework/sources/genesis.move b/aptos-move/framework/aptos-framework/sources/genesis.move index dde48974bc06b..207bcf74b351c 100644 --- a/aptos-move/framework/aptos-framework/sources/genesis.move +++ b/aptos-move/framework/aptos-framework/sources/genesis.move @@ -124,7 +124,6 @@ module aptos_framework::genesis { // Ensure we can create aggregators for supply, but not enable it for common use just yet. aggregator_factory::initialize_aggregator_factory(&aptos_framework_account); - coin::initialize_supply_config(&aptos_framework_account); chain_id::initialize(&aptos_framework_account, chain_id); reconfiguration::initialize(&aptos_framework_account);