Ensured that the Supra protocol configuration settings are stored in the Move state.

aptos-move/framework/supra-framework/doc/overview.md

@@ -62,6 +62,7 @@ This is the reference documentation of the Aptos framework.
 -  [`0x1::storage_gas`](storage_gas.md#0x1_storage_gas)
 -  [`0x1::supra_account`](supra_account.md#0x1_supra_account)
 -  [`0x1::supra_coin`](supra_coin.md#0x1_supra_coin)
+-  [`0x1::supra_config`](supra_config.md#0x1_supra_config)
 -  [`0x1::supra_governance`](supra_governance.md#0x1_supra_governance)
 -  [`0x1::system_addresses`](system_addresses.md#0x1_system_addresses)
 -  [`0x1::timestamp`](timestamp.md#0x1_timestamp)

aptos-move/framework/supra-framework/doc/reconfiguration_with_dkg.md

@@ -30,6 +30,7 @@ Reconfiguration with DKG helper functions.
 <b>use</b> <a href="reconfiguration.md#0x1_reconfiguration">0x1::reconfiguration</a>;
 <b>use</b> <a href="reconfiguration_state.md#0x1_reconfiguration_state">0x1::reconfiguration_state</a>;
 <b>use</b> <a href="stake.md#0x1_stake">0x1::stake</a>;
+<b>use</b> <a href="supra_config.md#0x1_supra_config">0x1::supra_config</a>;
 <b>use</b> <a href="system_addresses.md#0x1_system_addresses">0x1::system_addresses</a>;
 <b>use</b> <a href="validator_consensus_info.md#0x1_validator_consensus_info">0x1::validator_consensus_info</a>;
 <b>use</b> <a href="version.md#0x1_version">0x1::version</a>;
@@ -101,6 +102,7 @@ Run the default reconfiguration to enter the new epoch.
     <a href="dkg.md#0x1_dkg_try_clear_incomplete_session">dkg::try_clear_incomplete_session</a>(framework);
     <a href="consensus_config.md#0x1_consensus_config_on_new_epoch">consensus_config::on_new_epoch</a>(framework);
     <a href="execution_config.md#0x1_execution_config_on_new_epoch">execution_config::on_new_epoch</a>(framework);
+    <a href="supra_config.md#0x1_supra_config_on_new_epoch">supra_config::on_new_epoch</a>(framework);
     <a href="gas_schedule.md#0x1_gas_schedule_on_new_epoch">gas_schedule::on_new_epoch</a>(framework);
     std::version::on_new_epoch(framework);
     <a href="../../aptos-stdlib/../move-stdlib/doc/features.md#0x1_features_on_new_epoch">features::on_new_epoch</a>(framework);
@@ -215,6 +217,7 @@ Abort if no DKG is in progress.
     <b>include</b> <a href="config_buffer.md#0x1_config_buffer_OnNewEpochRequirement">config_buffer::OnNewEpochRequirement</a>&lt;<a href="gas_schedule.md#0x1_gas_schedule_GasScheduleV2">gas_schedule::GasScheduleV2</a>&gt;;
     <b>include</b> <a href="config_buffer.md#0x1_config_buffer_OnNewEpochRequirement">config_buffer::OnNewEpochRequirement</a>&lt;<a href="execution_config.md#0x1_execution_config_ExecutionConfig">execution_config::ExecutionConfig</a>&gt;;
     <b>include</b> <a href="config_buffer.md#0x1_config_buffer_OnNewEpochRequirement">config_buffer::OnNewEpochRequirement</a>&lt;<a href="consensus_config.md#0x1_consensus_config_ConsensusConfig">consensus_config::ConsensusConfig</a>&gt;;
+    <b>include</b> <a href="config_buffer.md#0x1_config_buffer_OnNewEpochRequirement">config_buffer::OnNewEpochRequirement</a>&lt;<a href="supra_config.md#0x1_supra_config_SupraConfig">supra_config::SupraConfig</a>&gt;;
     <b>include</b> <a href="config_buffer.md#0x1_config_buffer_OnNewEpochRequirement">config_buffer::OnNewEpochRequirement</a>&lt;<a href="jwks.md#0x1_jwks_SupportedOIDCProviders">jwks::SupportedOIDCProviders</a>&gt;;
     <b>include</b> <a href="config_buffer.md#0x1_config_buffer_OnNewEpochRequirement">config_buffer::OnNewEpochRequirement</a>&lt;<a href="randomness_config.md#0x1_randomness_config_RandomnessConfig">randomness_config::RandomnessConfig</a>&gt;;
     <b>include</b> <a href="config_buffer.md#0x1_config_buffer_OnNewEpochRequirement">config_buffer::OnNewEpochRequirement</a>&lt;<a href="randomness_config_seqnum.md#0x1_randomness_config_seqnum_RandomnessConfigSeqNum">randomness_config_seqnum::RandomnessConfigSeqNum</a>&gt;;

aptos-move/framework/supra-framework/sources/configs/config_buffer.move

@@ -20,6 +20,7 @@ module supra_framework::config_buffer {
 
     friend supra_framework::consensus_config;
     friend supra_framework::execution_config;
+    friend supra_framework::supra_config;
     friend supra_framework::gas_schedule;
     friend supra_framework::jwks;
     friend supra_framework::jwk_consensus_config;

aptos-move/framework/supra-framework/sources/configs/supra_config.move

@@ -0,0 +1,70 @@
+/// Maintains the consensus config for the blockchain. The config is stored in a
+/// Reconfiguration, and may be updated by root.
+module supra_framework::supra_config {
+    use std::error;
+    use std::vector;
+    use supra_framework::chain_status;
+    use supra_framework::config_buffer;
+
+    use supra_framework::reconfiguration;
+    use supra_framework::system_addresses;
+
+    friend supra_framework::genesis;
+    friend supra_framework::reconfiguration_with_dkg;
+
+    struct SupraConfig has drop, key, store {
+        config: vector<u8>,
+    }
+
+    /// The provided on chain config bytes are empty or invalid
+    const EINVALID_CONFIG: u64 = 1;
+
+    /// Publishes the SupraConfig config.
+    public(friend) fun initialize(supra_framework: &signer, config: vector<u8>) {
+        system_addresses::assert_supra_framework(supra_framework);
+        assert!(vector::length(&config) > 0, error::invalid_argument(EINVALID_CONFIG));
+        move_to(supra_framework, SupraConfig { config });
+    }
+
+    /// Deprecated by `set_for_next_epoch()`.
+    ///
+    /// WARNING: calling this while randomness is enabled will trigger a new epoch without randomness!
+    ///
+    /// TODO: update all the tests that reference this function, then disable this function.
+    public fun set(account: &signer, config: vector<u8>) acquires SupraConfig {
+        system_addresses::assert_supra_framework(account);
+        chain_status::assert_genesis();
+        assert!(vector::length(&config) > 0, error::invalid_argument(EINVALID_CONFIG));
+
+        let config_ref = &mut borrow_global_mut<SupraConfig>(@supra_framework).config;
+        *config_ref = config;
+
+        // Need to trigger reconfiguration so validator nodes can sync on the updated configs.
+        reconfiguration::reconfigure();
+    }
+
+    /// This can be called by on-chain governance to update on-chain configs for the next epoch.
+    /// Example usage:
+    /// ```
+    /// supra_framework::supra_config::set_for_next_epoch(&framework_signer, some_config_bytes);
+    /// supra_framework::supra_governance::reconfigure(&framework_signer);
+    /// ```
+    public fun set_for_next_epoch(account: &signer, config: vector<u8>) {
+        system_addresses::assert_supra_framework(account);
+        assert!(vector::length(&config) > 0, error::invalid_argument(EINVALID_CONFIG));
+        std::config_buffer::upsert<SupraConfig>(SupraConfig {config});
+    }
+
+    /// Only used in reconfigurations to apply the pending `SupraConfig`, if there is any.
+    public(friend) fun on_new_epoch(framework: &signer) acquires SupraConfig {
+        system_addresses::assert_supra_framework(framework);
+        if (config_buffer::does_exist<SupraConfig>()) {
+            let new_config = config_buffer::extract<SupraConfig>();
+            if (exists<SupraConfig>(@supra_framework)) {
+                *borrow_global_mut<SupraConfig>(@supra_framework) = new_config;
+            } else {
+                move_to(framework, new_config);
+            };
+        }
+    }
+}

aptos-move/framework/supra-framework/sources/configs/supra_config.spec.move

@@ -0,0 +1,83 @@
+spec supra_framework::supra_config {
+    /// <high-level-req>
+    /// No.: 1
+    /// Requirement: During genesis, the Supra framework account should be assigned the supra config resource.
+    /// Criticality: Medium
+    /// Implementation: The supra_config::initialize function calls the assert_supra_framework function to ensure
+    /// that the signer is the supra_framework and then assigns the SupraConfig resource to it.
+    /// Enforcement: Formally verified via [high-level-req-1](initialize).
+    ///
+    /// No.: 2
+    /// Requirement: Only aptos framework account is allowed to update the supra protocol configuration.
+    /// Criticality: Medium
+    /// Implementation: The supra_config::set function ensures that the signer is supra_framework.
+    /// Enforcement: Formally verified via [high-level-req-2](set).
+    ///
+    /// No.: 3
+    /// Requirement: Only a valid configuration can be used during initialization and update.
+    /// Criticality: Medium
+    /// Implementation: Both the initialize and set functions validate the config by ensuring its length to be greater
+    /// than 0.
+    /// Enforcement: Formally verified via [high-level-req-3.1](initialize) and [high-level-req-3.2](set).
+    /// </high-level-req>
+    ///
+    spec module {
+        use supra_framework::chain_status;
+        pragma verify = true;
+        pragma aborts_if_is_strict;
+        invariant [suspendable] chain_status::is_operating() ==> exists<SupraConfig>(@supra_framework);
+    }
+
+    /// Ensure caller is admin.
+    /// Aborts if StateStorageUsage already exists.
+    spec initialize(supra_framework: &signer, config: vector<u8>) {
+        use std::signer;
+        let addr = signer::address_of(supra_framework);
+        /// [high-level-req-1]
+        aborts_if !system_addresses::is_supra_framework_address(addr);
+        aborts_if exists<SupraConfig>(@supra_framework);
+        /// [high-level-req-3.1]
+        aborts_if !(len(config) > 0);
+        ensures global<SupraConfig>(addr) == SupraConfig { config };
+    }
+
+    /// Ensure the caller is admin and `SupraConfig` should exist.
+    /// When setting now time must be later than last_reconfiguration_time.
+    spec set(account: &signer, config: vector<u8>) {
+        use supra_framework::chain_status;
+        use supra_framework::timestamp;
+        use std::signer;
+        use supra_framework::stake;
+        use supra_framework::coin::CoinInfo;
+        use supra_framework::supra_coin::SupraCoin;
+        use supra_framework::transaction_fee;
+        use supra_framework::staking_config;
+
+        // TODO: set because of timeout (property proved)
+        pragma verify_duration_estimate = 600;
+        include transaction_fee::RequiresCollectedFeesPerValueLeqBlockAptosSupply;
+        include staking_config::StakingRewardsConfigRequirement;
+        let addr = signer::address_of(account);
+        /// [high-level-req-2]
+        aborts_if !system_addresses::is_supra_framework_address(addr);
+        aborts_if !exists<SupraConfig>(@supra_framework);
+        /// [high-level-req-3.2]
+        aborts_if !(len(config) > 0);
+
+        requires chain_status::is_genesis();
+        requires timestamp::spec_now_microseconds() >= reconfiguration::last_reconfiguration_time();
+        requires exists<stake::ValidatorFees>(@supra_framework);
+        requires exists<CoinInfo<SupraCoin>>(@supra_framework);
+        ensures global<SupraConfig>(@supra_framework).config == config;
+    }
+
+    spec set_for_next_epoch(account: &signer, config: vector<u8>) {
+        include config_buffer::SetForNextEpochAbortsIf;
+    }
+
+    spec on_new_epoch(framework: &signer) {
+        requires @supra_framework == std::signer::address_of(framework);
+        include config_buffer::OnNewEpochRequirement<SupraConfig>;
+        aborts_if false;
+    }
+}

aptos-move/framework/supra-framework/sources/genesis.move

@@ -20,6 +20,7 @@ module supra_framework::genesis {
     use supra_framework::coin;
     use supra_framework::consensus_config;
     use supra_framework::execution_config;
+    use supra_framework::supra_config;
     use supra_framework::create_signer::create_signer;
     use supra_framework::gas_schedule;
     use supra_framework::reconfiguration;
@@ -124,6 +125,7 @@ module supra_framework::genesis {
         initial_version: u64,
         consensus_config: vector<u8>,
         execution_config: vector<u8>,
+        supra_config: vector<u8>,
         epoch_interval_microsecs: u64,
         minimum_stake: u64,
         maximum_stake: u64,
@@ -162,6 +164,7 @@ module supra_framework::genesis {
 
         consensus_config::initialize(&supra_framework_account, consensus_config);
         execution_config::set(&supra_framework_account, execution_config);
+        supra_config::initialize(&supra_framework_account, supra_config);
         version::initialize(&supra_framework_account, initial_version);
         stake::initialize(&supra_framework_account);
         staking_config::initialize(
@@ -622,6 +625,7 @@ module supra_framework::genesis {
         initial_version: u64,
         consensus_config: vector<u8>,
         execution_config: vector<u8>,
+        supra_config: vector<u8>,
         epoch_interval_microsecs: u64,
         minimum_stake: u64,
         maximum_stake: u64,
@@ -648,6 +652,7 @@ module supra_framework::genesis {
             initial_version,
             consensus_config,
             execution_config,
+            supra_config,
             epoch_interval_microsecs,
             minimum_stake,
             maximum_stake,
@@ -684,6 +689,7 @@ module supra_framework::genesis {
             0,
             x"12",
             x"13",
+            x"14",
             1,
             0,
             1000 * ONE_APT,

aptos-move/framework/supra-framework/sources/genesis.spec.move

@@ -80,6 +80,7 @@ spec supra_framework::genesis {
         ensures exists<supra_governance::GovernanceResponsbility>(@supra_framework);
         ensures exists<consensus_config::ConsensusConfig>(@supra_framework);
         ensures exists<execution_config::ExecutionConfig>(@supra_framework);
+        ensures exists<supra_config::SupraConfig>(@supra_framework);
         ensures exists<version::Version>(@supra_framework);
         ensures exists<stake::ValidatorSet>(@supra_framework);
         ensures exists<stake::ValidatorPerformance>(@supra_framework);

aptos-move/framework/supra-framework/sources/reconfiguration.move

@@ -19,6 +19,7 @@ module supra_framework::reconfiguration {
     friend supra_framework::block;
     friend supra_framework::consensus_config;
     friend supra_framework::execution_config;
+    friend supra_framework::supra_config;
     friend supra_framework::gas_schedule;
     friend supra_framework::genesis;
     friend supra_framework::version;

aptos-move/framework/supra-framework/sources/reconfiguration_with_dkg.move

@@ -15,6 +15,7 @@ module supra_framework::reconfiguration_with_dkg {
     use supra_framework::reconfiguration;
     use supra_framework::reconfiguration_state;
     use supra_framework::stake;
+    use supra_framework::supra_config;
     use supra_framework::system_addresses;
     friend supra_framework::block;
     friend supra_framework::supra_governance;
@@ -48,6 +49,7 @@ module supra_framework::reconfiguration_with_dkg {
         dkg::try_clear_incomplete_session(framework);
         consensus_config::on_new_epoch(framework);
         execution_config::on_new_epoch(framework);
+        supra_config::on_new_epoch(framework);
         gas_schedule::on_new_epoch(framework);
         std::version::on_new_epoch(framework);
         features::on_new_epoch(framework);

aptos-move/framework/supra-framework/sources/reconfiguration_with_dkg.spec.move

@@ -41,6 +41,7 @@ spec supra_framework::reconfiguration_with_dkg {
         use supra_framework::jwks;
         use supra_framework::randomness_config;
         use supra_framework::jwk_consensus_config;
+        use supra_framework::supra_config;
         framework: signer;
         requires signer::address_of(framework) == @supra_framework;
         requires chain_status::is_operating();
@@ -53,6 +54,7 @@ spec supra_framework::reconfiguration_with_dkg {
         include config_buffer::OnNewEpochRequirement<gas_schedule::GasScheduleV2>;
         include config_buffer::OnNewEpochRequirement<execution_config::ExecutionConfig>;
         include config_buffer::OnNewEpochRequirement<consensus_config::ConsensusConfig>;
+        include config_buffer::OnNewEpochRequirement<supra_config::SupraConfig>;
         include config_buffer::OnNewEpochRequirement<jwks::SupportedOIDCProviders>;
         include config_buffer::OnNewEpochRequirement<randomness_config::RandomnessConfig>;
         include config_buffer::OnNewEpochRequirement<randomness_config_seqnum::RandomnessConfigSeqNum>;

aptos-move/vm-genesis/src/lib.rs

@@ -124,6 +124,7 @@ pub fn encode_aptos_mainnet_genesis_transaction(
     framework: &ReleaseBundle,
     chain_id: ChainId,
     genesis_config: &GenesisConfiguration,
+    supra_config_bytes: Vec<u8>,
 ) -> Transaction {
     assert!(!genesis_config.is_test, "This is mainnet!");
     validate_genesis_config(genesis_config);
@@ -149,6 +150,7 @@ pub fn encode_aptos_mainnet_genesis_transaction(
         &consensus_config,
         &execution_config,
         &gas_schedule,
+        supra_config_bytes,
     );
     initialize_features(
         &mut session,
@@ -223,6 +225,7 @@ pub fn encode_genesis_transaction(
     consensus_config: &OnChainConsensusConfig,
     execution_config: &OnChainExecutionConfig,
     gas_schedule: &GasScheduleV2,
+    supra_config_bytes: Vec<u8>,
 ) -> Transaction {
     Transaction::GenesisTransaction(WriteSetPayload::Direct(encode_genesis_change_set(
         &aptos_root_key,
@@ -238,6 +241,7 @@ pub fn encode_genesis_transaction(
         consensus_config,
         execution_config,
         gas_schedule,
+        supra_config_bytes,
     )))
 }
 
@@ -255,6 +259,7 @@ pub fn encode_genesis_change_set(
     consensus_config: &OnChainConsensusConfig,
     execution_config: &OnChainExecutionConfig,
     gas_schedule: &GasScheduleV2,
+    supra_config_bytes: Vec<u8>,
 ) -> ChangeSet {
     validate_genesis_config(genesis_config);
 
@@ -276,6 +281,7 @@ pub fn encode_genesis_change_set(
         consensus_config,
         execution_config,
         gas_schedule,
+        supra_config_bytes,
     );
     initialize_features(
         &mut session,
@@ -439,6 +445,7 @@ fn initialize(
     consensus_config: &OnChainConsensusConfig,
     execution_config: &OnChainExecutionConfig,
     gas_schedule: &GasScheduleV2,
+    supra_config_bytes: Vec<u8>,
 ) {
     let gas_schedule_blob =
         bcs::to_bytes(gas_schedule).expect("Failure serializing genesis gas schedule");
@@ -472,6 +479,7 @@ fn initialize(
             MoveValue::U64(APTOS_MAX_KNOWN_VERSION.major),
             MoveValue::vector_u8(consensus_config_bytes),
             MoveValue::vector_u8(execution_config_bytes),
+            MoveValue::vector_u8(supra_config_bytes),
             MoveValue::U64(epoch_interval_usecs),
             MoveValue::U64(genesis_config.min_stake),
             MoveValue::U64(genesis_config.max_stake),
@@ -1124,6 +1132,7 @@ pub fn generate_test_genesis(
         &OnChainConsensusConfig::default_for_genesis(),
         &OnChainExecutionConfig::default_for_genesis(),
         &default_gas_schedule(),
+        b"test".to_vec(),
     );
     (genesis, test_validators)
 }
@@ -1151,6 +1160,7 @@ pub fn generate_mainnet_genesis(
         &OnChainConsensusConfig::default_for_genesis(),
         &OnChainExecutionConfig::default_for_genesis(),
         &default_gas_schedule(),
+        b"test".to_vec(),
     );
     (genesis, test_validators)
 }
@@ -1748,6 +1758,7 @@ pub fn test_mainnet_end_to_end() {
         aptos_cached_packages::head_release_bundle(),
         ChainId::mainnet(),
         &mainnet_genesis_config(),
+        b"test".to_vec(),
     );
 
     let direct_writeset = if let Transaction::GenesisTransaction(direct_writeset) = transaction {

crates/aptos-genesis/src/lib.rs

@@ -165,6 +165,7 @@ impl GenesisInfo {
             &self.consensus_config,
             &self.execution_config,
             &self.gas_schedule,
+            b"test".to_vec(),
         )
     }
 

crates/aptos-genesis/src/mainnet.rs

@@ -154,6 +154,7 @@ impl MainnetGenesisInfo {
                 randomness_config_override: self.randomness_config_override.clone(),
                 jwk_consensus_config_override: self.jwk_consensus_config_override.clone(),
             },
+            b"test".to_vec(),
         )
     }