[compiler-v2 native] Change framework name

vm/framework/starcoin-framework/sources/block.spec.move

@@ -147,7 +147,7 @@ spec starcoin_framework::block {
         requires (proposer != @vm_reserved) ==> (timestamp::spec_now_microseconds() < timestamp);
         requires exists<stake::ValidatorFees>(@starcoin_framework);
         requires exists<CoinInfo<StarcoinCoin>>(@starcoin_framework);
-        include transaction_fee::RequiresCollectedFeesPerValueLeqBlockAptosSupply;
+        include transaction_fee::RequiresCollectedFeesPerValueLeqBlockStarcoinSupply;
         include staking_config::StakingRewardsConfigRequirement;
     }
 

vm/framework/starcoin-framework/sources/code.spec.move

@@ -73,9 +73,9 @@ spec starcoin_framework::code {
     }
 
     spec initialize(starcoin_framework: &signer, package_owner: &signer, metadata: PackageMetadata) {
-        let aptos_addr = signer::address_of(starcoin_framework);
+        let starcoin_addr = signer::address_of(starcoin_framework);
         let owner_addr = signer::address_of(package_owner);
-        aborts_if !system_addresses::is_starcoin_framework_address(aptos_addr);
+        aborts_if !system_addresses::is_starcoin_framework_address(starcoin_addr);
 
         ensures exists<PackageRegistry>(owner_addr);
     }

vm/framework/starcoin-framework/sources/configs/consensus_config.spec.move

@@ -55,7 +55,7 @@ spec starcoin_framework::consensus_config {
 
         // TODO: set because of timeout (property proved)
         pragma verify_duration_estimate = 600;
-        include transaction_fee::RequiresCollectedFeesPerValueLeqBlockAptosSupply;
+        include transaction_fee::RequiresCollectedFeesPerValueLeqBlockStarcoinSupply;
         include staking_config::StakingRewardsConfigRequirement;
         let addr = signer::address_of(account);
         /// [high-level-req-2]

vm/framework/starcoin-framework/sources/configs/execution_config.spec.move

@@ -19,7 +19,7 @@ spec starcoin_framework::execution_config {
         // TODO: set because of timeout (property proved)
         pragma verify_duration_estimate = 600;
         let addr = signer::address_of(account);
-        include transaction_fee::RequiresCollectedFeesPerValueLeqBlockAptosSupply;
+        include transaction_fee::RequiresCollectedFeesPerValueLeqBlockStarcoinSupply;
         requires chain_status::is_genesis();
         requires exists<stake::ValidatorFees>(@starcoin_framework);
         requires exists<staking_config::StakingRewardsConfig>(@starcoin_framework);

vm/framework/starcoin-framework/sources/configs/gas_schedule.spec.move

@@ -61,7 +61,7 @@ spec starcoin_framework::gas_schedule {
         requires exists<stake::ValidatorFees>(@starcoin_framework);
         requires exists<CoinInfo<StarcoinCoin>>(@starcoin_framework);
         requires chain_status::is_genesis();
-        include transaction_fee::RequiresCollectedFeesPerValueLeqBlockAptosSupply;
+        include transaction_fee::RequiresCollectedFeesPerValueLeqBlockStarcoinSupply;
         include staking_config::StakingRewardsConfigRequirement;
 
         /// [high-level-req-2]
@@ -88,7 +88,7 @@ spec starcoin_framework::gas_schedule {
         requires exists<stake::ValidatorFees>(@starcoin_framework);
         requires exists<CoinInfo<StarcoinCoin>>(@starcoin_framework);
         include system_addresses::AbortsIfNotAptosFramework{ account: starcoin_framework };
-        include transaction_fee::RequiresCollectedFeesPerValueLeqBlockAptosSupply;
+        include transaction_fee::RequiresCollectedFeesPerValueLeqBlockStarcoinSupply;
         include staking_config::StakingRewardsConfigRequirement;
         aborts_if !exists<StorageGasConfig>(@starcoin_framework);
         ensures global<StorageGasConfig>(@starcoin_framework) == config;

vm/framework/starcoin-framework/sources/configs/version.spec.move

@@ -35,7 +35,7 @@ spec starcoin_framework::version {
 
         // TODO: set because of timeout (property proved)
         pragma verify_duration_estimate = 120;
-        include transaction_fee::RequiresCollectedFeesPerValueLeqBlockAptosSupply;
+        include transaction_fee::RequiresCollectedFeesPerValueLeqBlockStarcoinSupply;
         include staking_config::StakingRewardsConfigRequirement;
         requires chain_status::is_genesis();
         requires timestamp::spec_now_microseconds() >= reconfiguration::last_reconfiguration_time();

vm/framework/starcoin-framework/sources/genesis.move

@@ -143,9 +143,9 @@ module starcoin_framework::genesis {
         // Give stake module MintCapability<StarcoinCoin> so it can mint rewards.
         stake::store_aptos_coin_mint_cap(starcoin_framework, mint_cap);
         // Give transaction_fee module BurnCapability<StarcoinCoin> so it can burn gas.
-        transaction_fee::store_aptos_coin_burn_cap(starcoin_framework, burn_cap);
+        transaction_fee::store_coin_burn_cap(starcoin_framework, burn_cap);
         // Give transaction_fee module MintCapability<StarcoinCoin> so it can mint refunds.
-        transaction_fee::store_aptos_coin_mint_cap(starcoin_framework, mint_cap);
+        transaction_fee::store_coin_mint_cap(starcoin_framework, mint_cap);
     }
 
     /// Only called for testnets and e2e tests.
@@ -161,9 +161,9 @@ module starcoin_framework::genesis {
         // Give stake module MintCapability<StarcoinCoin> so it can mint rewards.
         stake::store_aptos_coin_mint_cap(starcoin_framework, mint_cap);
         // Give transaction_fee module BurnCapability<StarcoinCoin> so it can burn gas.
-        transaction_fee::store_aptos_coin_burn_cap(starcoin_framework, burn_cap);
+        transaction_fee::store_coin_burn_cap(starcoin_framework, burn_cap);
         // Give transaction_fee module MintCapability<StarcoinCoin> so it can mint refunds.
-        transaction_fee::store_aptos_coin_mint_cap(starcoin_framework, mint_cap);
+        transaction_fee::store_coin_mint_cap(starcoin_framework, mint_cap);
 
         let core_resources = account::create_account(@core_resources);
         account::rotate_authentication_key_internal(&core_resources, core_resources_auth_key);

vm/framework/starcoin-framework/sources/genesis.spec.move

@@ -104,8 +104,8 @@ spec starcoin_framework::genesis {
         /// [high-level-req-3]
         requires !exists<stake::AptosCoinCapabilities>(@starcoin_framework);
         ensures exists<stake::AptosCoinCapabilities>(@starcoin_framework);
-        requires exists<transaction_fee::AptosCoinCapabilities>(@starcoin_framework);
-        ensures exists<transaction_fee::AptosCoinCapabilities>(@starcoin_framework);
+        requires exists<transaction_fee::CoinCapabilities>(@starcoin_framework);
+        ensures exists<transaction_fee::CoinCapabilities>(@starcoin_framework);
     }
 
     spec create_initialize_validators_with_commission {
@@ -160,7 +160,7 @@ spec starcoin_framework::genesis {
         requires exists<stake::ValidatorFees>(@starcoin_framework);
         requires exists<coin::CoinInfo<StarcoinCoin>>(@starcoin_framework);
         include CompareTimeRequires;
-        include transaction_fee::RequiresCollectedFeesPerValueLeqBlockAptosSupply;
+        include transaction_fee::RequiresCollectedFeesPerValueLeqBlockStarcoinSupply;
     }
 
     spec schema CompareTimeRequires {

vm/framework/starcoin-framework/sources/reconfiguration.spec.move

@@ -53,7 +53,7 @@ spec starcoin_framework::reconfiguration {
     }
 
     /// Make sure the signer address is @starcoin_framework.
-    spec schema AbortsIfNotAptosFramework {
+    spec schema AbortsIfNotStarcoinFramework {
         starcoin_framework: &signer;
 
         let addr = signer::address_of(starcoin_framework);
@@ -68,7 +68,7 @@ spec starcoin_framework::reconfiguration {
         use starcoin_framework::account::{Account};
         use starcoin_framework::guid;
 
-        include AbortsIfNotAptosFramework;
+        include AbortsIfNotStarcoinFramework;
         let addr = signer::address_of(starcoin_framework);
         let post config = global<Configuration>(@starcoin_framework);
         requires exists<Account>(addr);
@@ -96,15 +96,15 @@ spec starcoin_framework::reconfiguration {
     }
 
     spec disable_reconfiguration(starcoin_framework: &signer) {
-        include AbortsIfNotAptosFramework;
+        include AbortsIfNotStarcoinFramework;
         aborts_if exists<DisableReconfiguration>(@starcoin_framework);
         ensures exists<DisableReconfiguration>(@starcoin_framework);
     }
 
     /// Make sure the caller is admin and check the resource DisableReconfiguration.
     spec enable_reconfiguration(starcoin_framework: &signer) {
         use starcoin_framework::reconfiguration::{DisableReconfiguration};
-        include AbortsIfNotAptosFramework;
+        include AbortsIfNotStarcoinFramework;
         aborts_if !exists<DisableReconfiguration>(@starcoin_framework);
         ensures !exists<DisableReconfiguration>(@starcoin_framework);
     }
@@ -139,7 +139,7 @@ spec starcoin_framework::reconfiguration {
             && timestamp::spec_now_microseconds() != global<Configuration>(@starcoin_framework).last_reconfiguration_time;
         include features::spec_periodical_reward_rate_decrease_enabled() ==> staking_config::StakingRewardsConfigEnabledRequirement;
         include success ==> starcoin_coin::ExistsAptosCoin;
-        include transaction_fee::RequiresCollectedFeesPerValueLeqBlockAptosSupply;
+        include transaction_fee::RequiresCollectedFeesPerValueLeqBlockStarcoinSupply;
         aborts_if false;
         // The ensure conditions of the reconfigure function are not fully written, because there is a new cycle in it,
         // but its existing ensure conditions satisfy hp.

vm/framework/starcoin-framework/sources/reconfiguration_with_dkg.spec.move

@@ -47,7 +47,7 @@ spec starcoin_framework::reconfiguration_with_dkg {
         requires exists<CoinInfo<StarcoinCoin>>(@starcoin_framework);
         include staking_config::StakingRewardsConfigRequirement;
         requires exists<stake::ValidatorFees>(@starcoin_framework);
-        include transaction_fee::RequiresCollectedFeesPerValueLeqBlockAptosSupply;
+        include transaction_fee::RequiresCollectedFeesPerValueLeqBlockStarcoinSupply;
         requires exists<features::Features>(@std);
         include config_buffer::OnNewEpochRequirement<version::Version>;
         include config_buffer::OnNewEpochRequirement<gas_schedule::GasScheduleV2>;

vm/framework/starcoin-framework/sources/starcoin_governance.spec.move

@@ -146,7 +146,7 @@ spec starcoin_framework::starcoin_governance {
             framework: starcoin_framework
         };
         include stake::GetReconfigStartTimeRequirement;
-        include transaction_fee::RequiresCollectedFeesPerValueLeqBlockAptosSupply;
+        include transaction_fee::RequiresCollectedFeesPerValueLeqBlockStarcoinSupply;
         requires chain_status::is_operating();
         requires exists<stake::ValidatorFees>(@starcoin_framework);
         requires exists<CoinInfo<StarcoinCoin>>(@starcoin_framework);
@@ -586,7 +586,7 @@ spec starcoin_framework::starcoin_governance {
         };
         include stake::GetReconfigStartTimeRequirement;
 
-        include transaction_fee::RequiresCollectedFeesPerValueLeqBlockAptosSupply;
+        include transaction_fee::RequiresCollectedFeesPerValueLeqBlockStarcoinSupply;
         requires chain_status::is_operating();
         requires exists<stake::ValidatorFees>(@starcoin_framework);
         requires exists<CoinInfo<StarcoinCoin>>(@starcoin_framework);

vm/framework/starcoin-framework/sources/transaction_fee.move

@@ -30,17 +30,17 @@ module starcoin_framework::transaction_fee {
     const EFA_GAS_CHARGING_NOT_ENABLED: u64 = 5;
 
     /// Stores burn capability to burn the gas fees.
-    struct AptosCoinCapabilities has key {
+    struct CoinCapabilities has key {
         burn_cap: BurnCapability<StarcoinCoin>,
     }
 
     /// Stores burn capability to burn the gas fees.
-    struct AptosFABurnCapabilities has key {
+    struct FABurnCapabilities has key {
         burn_ref: BurnRef,
     }
 
     /// Stores mint capability to mint the refunds.
-    struct AptosCoinMintCapability has key {
+    struct CoinMintCapability has key {
         mint_cap: MintCapability<StarcoinCoin>,
     }
 
@@ -115,7 +115,7 @@ module starcoin_framework::transaction_fee {
     public fun upgrade_burn_percentage(
         starcoin_framework: &signer,
         new_burn_percentage: u8
-    ) acquires AptosCoinCapabilities, CollectedFeesPerBlock {
+    ) acquires CoinCapabilities, CollectedFeesPerBlock {
         system_addresses::assert_starcoin_framework(starcoin_framework);
         assert!(new_burn_percentage <= 100, error::out_of_range(EINVALID_BURN_PERCENTAGE));
 
@@ -141,7 +141,7 @@ module starcoin_framework::transaction_fee {
     }
 
     /// Burns a specified fraction of the coin.
-    fun burn_coin_fraction(coin: &mut Coin<StarcoinCoin>, burn_percentage: u8) acquires AptosCoinCapabilities {
+    fun burn_coin_fraction(coin: &mut Coin<StarcoinCoin>, burn_percentage: u8) acquires CoinCapabilities {
         assert!(burn_percentage <= 100, error::out_of_range(EINVALID_BURN_PERCENTAGE));
 
         let collected_amount = coin::value(coin);
@@ -154,15 +154,15 @@ module starcoin_framework::transaction_fee {
             let coin_to_burn = coin::extract(coin, amount_to_burn);
             coin::burn(
                 coin_to_burn,
-                &borrow_global<AptosCoinCapabilities>(@starcoin_framework).burn_cap,
+                &borrow_global<CoinCapabilities>(@starcoin_framework).burn_cap,
             );
         }
     }
 
     /// Calculates the fee which should be distributed to the block proposer at the
     /// end of an epoch, and records it in the system. This function can only be called
     /// at the beginning of the block or during reconfiguration.
-    public(friend) fun process_collected_fees() acquires AptosCoinCapabilities, CollectedFeesPerBlock {
+    public(friend) fun process_collected_fees() acquires CoinCapabilities, CollectedFeesPerBlock {
         if (!is_fees_collection_enabled()) {
             return
         };
@@ -208,12 +208,12 @@ module starcoin_framework::transaction_fee {
     }
 
     /// Burn transaction fees in epilogue.
-    public(friend) fun burn_fee(account: address, fee: u64) acquires AptosFABurnCapabilities, AptosCoinCapabilities {
-        if (exists<AptosFABurnCapabilities>(@starcoin_framework)) {
-            let burn_ref = &borrow_global<AptosFABurnCapabilities>(@starcoin_framework).burn_ref;
+    public(friend) fun burn_fee(account: address, fee: u64) acquires FABurnCapabilities, CoinCapabilities {
+        if (exists<FABurnCapabilities>(@starcoin_framework)) {
+            let burn_ref = &borrow_global<FABurnCapabilities>(@starcoin_framework).burn_ref;
             starcoin_account::burn_from_fungible_store(burn_ref, account, fee);
         } else {
-            let burn_cap = &borrow_global<AptosCoinCapabilities>(@starcoin_framework).burn_cap;
+            let burn_cap = &borrow_global<CoinCapabilities>(@starcoin_framework).burn_cap;
             if (features::operations_default_to_fa_apt_store_enabled()) {
                 let (burn_ref, burn_receipt) = coin::get_paired_burn_ref(burn_cap);
                 starcoin_account::burn_from_fungible_store(&burn_ref, account, fee);
@@ -229,8 +229,8 @@ module starcoin_framework::transaction_fee {
     }
 
     /// Mint refund in epilogue.
-    public(friend) fun mint_and_refund(account: address, refund: u64) acquires AptosCoinMintCapability {
-        let mint_cap = &borrow_global<AptosCoinMintCapability>(@starcoin_framework).mint_cap;
+    public(friend) fun mint_and_refund(account: address, refund: u64) acquires CoinMintCapability {
+        let mint_cap = &borrow_global<CoinMintCapability>(@starcoin_framework).mint_cap;
         let refund_coin = coin::mint(refund, mint_cap);
         coin::force_deposit(account, refund_coin);
     }
@@ -247,31 +247,31 @@ module starcoin_framework::transaction_fee {
     }
 
     /// Only called during genesis.
-    public(friend) fun store_aptos_coin_burn_cap(starcoin_framework: &signer, burn_cap: BurnCapability<StarcoinCoin>) {
+    public(friend) fun store_coin_burn_cap(starcoin_framework: &signer, burn_cap: BurnCapability<StarcoinCoin>) {
         system_addresses::assert_starcoin_framework(starcoin_framework);
 
         if (features::operations_default_to_fa_apt_store_enabled()) {
             let burn_ref = coin::convert_and_take_paired_burn_ref(burn_cap);
-            move_to(starcoin_framework, AptosFABurnCapabilities { burn_ref });
+            move_to(starcoin_framework, FABurnCapabilities { burn_ref });
         } else {
-            move_to(starcoin_framework, AptosCoinCapabilities { burn_cap })
+            move_to(starcoin_framework, CoinCapabilities { burn_cap })
         }
     }
 
-    public entry fun convert_to_aptos_fa_burn_ref(starcoin_framework: &signer) acquires AptosCoinCapabilities {
+    public entry fun convert_to_starcoin_fa_burn_ref(starcoin_framework: &signer) acquires CoinCapabilities {
         assert!(features::operations_default_to_fa_apt_store_enabled(), EFA_GAS_CHARGING_NOT_ENABLED);
         system_addresses::assert_starcoin_framework(starcoin_framework);
-        let AptosCoinCapabilities {
+        let CoinCapabilities {
             burn_cap,
-        } = move_from<AptosCoinCapabilities>(signer::address_of(starcoin_framework));
+        } = move_from<CoinCapabilities>(signer::address_of(starcoin_framework));
         let burn_ref = coin::convert_and_take_paired_burn_ref(burn_cap);
-        move_to(starcoin_framework, AptosFABurnCapabilities { burn_ref });
+        move_to(starcoin_framework, FABurnCapabilities { burn_ref });
     }
 
     /// Only called during genesis.
-    public(friend) fun store_aptos_coin_mint_cap(starcoin_framework: &signer, mint_cap: MintCapability<StarcoinCoin>) {
+    public(friend) fun store_coin_mint_cap(starcoin_framework: &signer, mint_cap: MintCapability<StarcoinCoin>) {
         system_addresses::assert_starcoin_framework(starcoin_framework);
-        move_to(starcoin_framework, AptosCoinMintCapability { mint_cap })
+        move_to(starcoin_framework, CoinMintCapability { mint_cap })
     }
 
     #[deprecated]
@@ -305,10 +305,10 @@ module starcoin_framework::transaction_fee {
     }
 
     #[test(starcoin_framework = @starcoin_framework)]
-    fun test_burn_fraction_calculation(starcoin_framework: signer) acquires AptosCoinCapabilities {
+    fun test_burn_fraction_calculation(starcoin_framework: signer) acquires CoinCapabilities {
         use starcoin_framework::starcoin_coin;
         let (burn_cap, mint_cap) = starcoin_coin::initialize_for_test(&starcoin_framework);
-        store_aptos_coin_burn_cap(&starcoin_framework, burn_cap);
+        store_coin_burn_cap(&starcoin_framework, burn_cap);
 
         let c1 = coin::mint<StarcoinCoin>(100, &mint_cap);
         assert!(*option::borrow(&coin::supply<StarcoinCoin>()) == 100, 0);
@@ -348,14 +348,14 @@ module starcoin_framework::transaction_fee {
         alice: signer,
         bob: signer,
         carol: signer,
-    ) acquires AptosCoinCapabilities, CollectedFeesPerBlock {
+    ) acquires CoinCapabilities, CollectedFeesPerBlock {
         use std::signer;
         use starcoin_framework::starcoin_account;
         use starcoin_framework::starcoin_coin;
 
         // Initialization.
         let (burn_cap, mint_cap) = starcoin_coin::initialize_for_test(&starcoin_framework);
-        store_aptos_coin_burn_cap(&starcoin_framework, burn_cap);
+        store_coin_burn_cap(&starcoin_framework, burn_cap);
         initialize_fee_collection_and_distribution(&starcoin_framework, 10);
 
         // Create dummy accounts.