Skip to content

Commit

Permalink
[Spec] Ensures of reconfiguration.move (#9383)
Browse files Browse the repository at this point in the history 
* init

* hp

* hp reconfig

* init

* fix comment

* fix comment

---------

Co-authored-by: chan-bing <[email protected]>
  • Loading branch information
@UIZorrot @chan-bing
UIZorrot and chan-bing authored Aug 11, 2023
1 parent 61b8cfd commit e450718
Show file tree
Hide file tree
Showing 2 changed files with 50 additions and 3 deletions.
19 changes: 18 additions & 1 deletion aptos-move/framework/aptos-framework/doc/reconfiguration.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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>


Expand All @@ -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>


Expand All @@ -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>


Expand All @@ -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>


Expand All @@ -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>

Expand All @@ -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>


Expand All @@ -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>


Expand All @@ -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>


Expand Down
34 changes: 32 additions & 2 deletions aptos-move/framework/aptos-framework/sources/reconfiguration.spec.move
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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` .
Expand All @@ -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);
}
}

0 comments on commit e450718

Please sign in to comment.