[Spec] Ensures of reconfiguration.move

aptos-move/framework/aptos-framework/doc/reconfiguration.md

@@ -530,6 +530,15 @@ Guid_creation_num should be 2 according to logic.
 <b>aborts_if</b> <b>exists</b>&lt;<a href="reconfiguration.md#0x1_reconfiguration_Configuration">Configuration</a>&gt;(@aptos_framework);
 <b>ensures</b> <b>exists</b>&lt;<a href="reconfiguration.md#0x1_reconfiguration_Configuration">Configuration</a>&gt;(@aptos_framework);
 <b>ensures</b> config.epoch == 0 && config.last_reconfiguration_time == 0;
+<b>ensures</b> config.events == <a href="event.md#0x1_event_EventHandle">event::EventHandle</a>&lt;<a href="reconfiguration.md#0x1_reconfiguration_NewEpochEvent">NewEpochEvent</a>&gt; {
+    counter: 0,
+    <a href="guid.md#0x1_guid">guid</a>: <a href="guid.md#0x1_guid_GUID">guid::GUID</a> {
+        id: <a href="guid.md#0x1_guid_ID">guid::ID</a> {
+            creation_num: 2,
+            addr: @aptos_framework
+        }
+    }
+};
 </code></pre>
 
 
@@ -547,6 +556,7 @@ Guid_creation_num should be 2 according to logic.
 
 <pre><code><b>include</b> <a href="reconfiguration.md#0x1_reconfiguration_AbortsIfNotAptosFramework">AbortsIfNotAptosFramework</a>;
 <b>aborts_if</b> <b>exists</b>&lt;<a href="reconfiguration.md#0x1_reconfiguration_DisableReconfiguration">DisableReconfiguration</a>&gt;(@aptos_framework);
+<b>ensures</b> <b>exists</b>&lt;<a href="reconfiguration.md#0x1_reconfiguration_DisableReconfiguration">DisableReconfiguration</a>&gt;(@aptos_framework);
 </code></pre>
 
 
@@ -565,6 +575,7 @@ Make sure the caller is admin and check the resource DisableReconfiguration.
 
 <pre><code><b>include</b> <a href="reconfiguration.md#0x1_reconfiguration_AbortsIfNotAptosFramework">AbortsIfNotAptosFramework</a>;
 <b>aborts_if</b> !<b>exists</b>&lt;<a href="reconfiguration.md#0x1_reconfiguration_DisableReconfiguration">DisableReconfiguration</a>&gt;(@aptos_framework);
+<b>ensures</b> !<b>exists</b>&lt;<a href="reconfiguration.md#0x1_reconfiguration_DisableReconfiguration">DisableReconfiguration</a>&gt;(@aptos_framework);
 </code></pre>
 
 
@@ -581,6 +592,7 @@ Make sure the caller is admin and check the resource DisableReconfiguration.
 
 
 <pre><code><b>aborts_if</b> <b>false</b>;
+<b>ensures</b> result == !<b>exists</b>&lt;<a href="reconfiguration.md#0x1_reconfiguration_DisableReconfiguration">DisableReconfiguration</a>&gt;(@aptos_framework);
 </code></pre>
 
 
@@ -598,13 +610,15 @@ Make sure the caller is admin and check the resource DisableReconfiguration.
 
 <pre><code><b>pragma</b> verify_duration_estimate = 120;
 <b>requires</b> <b>exists</b>&lt;<a href="stake.md#0x1_stake_ValidatorFees">stake::ValidatorFees</a>&gt;(@aptos_framework);
-<b>include</b> <a href="transaction_fee.md#0x1_transaction_fee_RequiresCollectedFeesPerValueLeqBlockAptosSupply">transaction_fee::RequiresCollectedFeesPerValueLeqBlockAptosSupply</a>;
+<b>requires</b> <b>exists</b>&lt;CoinInfo&lt;AptosCoin&gt;&gt;(@aptos_framework);
 <b>include</b> <a href="../../aptos-stdlib/../move-stdlib/doc/features.md#0x1_features_spec_periodical_reward_rate_decrease_enabled">features::spec_periodical_reward_rate_decrease_enabled</a>() ==&gt; <a href="staking_config.md#0x1_staking_config_StakingRewardsConfigEnabledRequirement">staking_config::StakingRewardsConfigEnabledRequirement</a>;
 <b>include</b> <a href="../../aptos-stdlib/../move-stdlib/doc/features.md#0x1_features_spec_collect_and_distribute_gas_fees_enabled">features::spec_collect_and_distribute_gas_fees_enabled</a>() ==&gt; <a href="aptos_coin.md#0x1_aptos_coin_ExistsAptosCoin">aptos_coin::ExistsAptosCoin</a>;
+<b>include</b> <a href="transaction_fee.md#0x1_transaction_fee_RequiresCollectedFeesPerValueLeqBlockAptosSupply">transaction_fee::RequiresCollectedFeesPerValueLeqBlockAptosSupply</a>;
 <b>aborts_if</b> <b>false</b>;
 <b>let</b> success = !(<a href="chain_status.md#0x1_chain_status_is_genesis">chain_status::is_genesis</a>() || <a href="timestamp.md#0x1_timestamp_spec_now_microseconds">timestamp::spec_now_microseconds</a>() == 0 || !<a href="reconfiguration.md#0x1_reconfiguration_reconfiguration_enabled">reconfiguration_enabled</a>())
     && <a href="timestamp.md#0x1_timestamp_spec_now_microseconds">timestamp::spec_now_microseconds</a>() != <b>global</b>&lt;<a href="reconfiguration.md#0x1_reconfiguration_Configuration">Configuration</a>&gt;(@aptos_framework).last_reconfiguration_time;
 <b>ensures</b> success ==&gt; <b>global</b>&lt;<a href="reconfiguration.md#0x1_reconfiguration_Configuration">Configuration</a>&gt;(@aptos_framework).epoch == <b>old</b>(<b>global</b>&lt;<a href="reconfiguration.md#0x1_reconfiguration_Configuration">Configuration</a>&gt;(@aptos_framework).epoch) + 1;
+<b>ensures</b> success ==&gt; <b>global</b>&lt;<a href="reconfiguration.md#0x1_reconfiguration_Configuration">Configuration</a>&gt;(@aptos_framework).last_reconfiguration_time == <a href="timestamp.md#0x1_timestamp_spec_now_microseconds">timestamp::spec_now_microseconds</a>();
 <b>ensures</b> !success ==&gt; <b>global</b>&lt;<a href="reconfiguration.md#0x1_reconfiguration_Configuration">Configuration</a>&gt;(@aptos_framework).epoch == <b>old</b>(<b>global</b>&lt;<a href="reconfiguration.md#0x1_reconfiguration_Configuration">Configuration</a>&gt;(@aptos_framework).epoch);
 </code></pre>
 
@@ -622,6 +636,7 @@ Make sure the caller is admin and check the resource DisableReconfiguration.
 
 
 <pre><code><b>aborts_if</b> !<b>exists</b>&lt;<a href="reconfiguration.md#0x1_reconfiguration_Configuration">Configuration</a>&gt;(@aptos_framework);
+<b>ensures</b> result == <b>global</b>&lt;<a href="reconfiguration.md#0x1_reconfiguration_Configuration">Configuration</a>&gt;(@aptos_framework).last_reconfiguration_time;
 </code></pre>
 
 
@@ -638,6 +653,7 @@ Make sure the caller is admin and check the resource DisableReconfiguration.
 
 
 <pre><code><b>aborts_if</b> !<b>exists</b>&lt;<a href="reconfiguration.md#0x1_reconfiguration_Configuration">Configuration</a>&gt;(@aptos_framework);
+<b>ensures</b> result == <b>global</b>&lt;<a href="reconfiguration.md#0x1_reconfiguration_Configuration">Configuration</a>&gt;(@aptos_framework).epoch;
 </code></pre>
 
 
@@ -658,6 +674,7 @@ Should equal to 0
 <pre><code><b>aborts_if</b> !<b>exists</b>&lt;<a href="reconfiguration.md#0x1_reconfiguration_Configuration">Configuration</a>&gt;(@aptos_framework);
 <b>let</b> config_ref = <b>global</b>&lt;<a href="reconfiguration.md#0x1_reconfiguration_Configuration">Configuration</a>&gt;(@aptos_framework);
 <b>aborts_if</b> !(config_ref.epoch == 0 && config_ref.last_reconfiguration_time == 0);
+<b>ensures</b> <b>global</b>&lt;<a href="reconfiguration.md#0x1_reconfiguration_Configuration">Configuration</a>&gt;(@aptos_framework).epoch == 1;
 </code></pre>
 
 

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

@@ -23,31 +23,45 @@ spec aptos_framework::reconfiguration {
     spec initialize(aptos_framework: &signer) {
         use std::signer;
         use aptos_framework::account::{Account};
+        use aptos_framework::guid;
 
         include AbortsIfNotAptosFramework;
         let addr = signer::address_of(aptos_framework);
         let post config = global<Configuration>(@aptos_framework);
         requires exists<Account>(addr);
         aborts_if !(global<Account>(addr).guid_creation_num == 2);
         aborts_if exists<Configuration>(@aptos_framework);
+        // property 1: During the module's initialization, it guarantees that the Configuration resource will move under the Aptos framework account with initial values.
         ensures exists<Configuration>(@aptos_framework);
         ensures config.epoch == 0 && config.last_reconfiguration_time == 0;
+        ensures config.events == event::EventHandle<NewEpochEvent> {
+            counter: 0,
+            guid: guid::GUID {
+                id: guid::ID {
+                    creation_num: 2,
+                    addr: @aptos_framework
+                }
+            }
+        };
     }
 
     spec current_epoch(): u64 {
         aborts_if !exists<Configuration>(@aptos_framework);
+        ensures result == global<Configuration>(@aptos_framework).epoch;
     }
 
     spec disable_reconfiguration(aptos_framework: &signer) {
         include AbortsIfNotAptosFramework;
         aborts_if exists<DisableReconfiguration>(@aptos_framework);
+        ensures exists<DisableReconfiguration>(@aptos_framework);
     }
 
     /// Make sure the caller is admin and check the resource DisableReconfiguration.
     spec enable_reconfiguration(aptos_framework: &signer) {
         use aptos_framework::reconfiguration::{DisableReconfiguration};
         include AbortsIfNotAptosFramework;
         aborts_if !exists<DisableReconfiguration>(@aptos_framework);
+        ensures !exists<DisableReconfiguration>(@aptos_framework);
     }
 
     /// When genesis_event emit the epoch and the `last_reconfiguration_time` .
@@ -58,33 +72,49 @@ spec aptos_framework::reconfiguration {
         aborts_if !exists<Configuration>(@aptos_framework);
         let config_ref = global<Configuration>(@aptos_framework);
         aborts_if !(config_ref.epoch == 0 && config_ref.last_reconfiguration_time == 0);
+        ensures global<Configuration>(@aptos_framework).epoch == 1;
     }
 
     spec last_reconfiguration_time {
         aborts_if !exists<Configuration>(@aptos_framework);
+        ensures result == global<Configuration>(@aptos_framework).last_reconfiguration_time;
     }
 
     spec reconfigure {
         use aptos_framework::aptos_coin;
+        use aptos_framework::coin::CoinInfo;
+        use aptos_framework::aptos_coin::AptosCoin;
         use aptos_framework::transaction_fee;
         use aptos_framework::staking_config;
 
         pragma verify_duration_estimate = 120; // TODO: set because of timeout (property proved)
 
         requires exists<stake::ValidatorFees>(@aptos_framework);
+        requires exists<CoinInfo<AptosCoin>>(@aptos_framework);
 
-        include transaction_fee::RequiresCollectedFeesPerValueLeqBlockAptosSupply;
         include features::spec_periodical_reward_rate_decrease_enabled() ==> staking_config::StakingRewardsConfigEnabledRequirement;
         include features::spec_collect_and_distribute_gas_fees_enabled() ==> aptos_coin::ExistsAptosCoin;
-
+        include transaction_fee::RequiresCollectedFeesPerValueLeqBlockAptosSupply;
         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.
         let success = !(chain_status::is_genesis() || timestamp::spec_now_microseconds() == 0 || !reconfiguration_enabled())
             && timestamp::spec_now_microseconds() != global<Configuration>(@aptos_framework).last_reconfiguration_time;
+        // The property below is not proved within 500s and still cause an timeout
+        // property 3: Synchronization of NewEpochEvent counter with configuration epoch.
         ensures success ==> global<Configuration>(@aptos_framework).epoch == old(global<Configuration>(@aptos_framework).epoch) + 1;
+        ensures success ==> global<Configuration>(@aptos_framework).last_reconfiguration_time == timestamp::spec_now_microseconds();
+        // We remove the ensures of event increment due to inconsisency
+        // TODO: property 4: Only performs reconfiguration if genesis has started and reconfiguration is enabled.
+        // Also, the last reconfiguration must not be the current time, returning early without further actions otherwise.
+        // property 5: Consecutive reconfigurations without the passage of time are not permitted.
         ensures !success ==> global<Configuration>(@aptos_framework).epoch == old(global<Configuration>(@aptos_framework).epoch);
     }
 
     spec reconfiguration_enabled {
+        // property 2: The reconfiguration status may be determined at any time without causing an abort, indicating whether or not the system allows reconfiguration.
         aborts_if false;
+        ensures result == !exists<DisableReconfiguration>(@aptos_framework);
     }
 }