Skip to content

Commit

Permalink
[Spec] Added specs for module reconfiguration & stake & storage_gas &…
Browse files Browse the repository at this point in the history 
… consensus_config & transaction_fee & transaction_validation (#5549)

* Updated specs for reconfiguration.move and stake.move and storage_gas.move

* Updated spec for consensus_config, added spec for transaction_fee & transaction_validation

* Updated aptos-framework documentation

* Updated specs for reconfiguration.move and storage_gas.move and transaction_fee.move and transaction_validation.move, Documentation updated

* Format spec.

* Updated spec documentation.

* Documentation updated.

Co-authored-by: yoyoping <[email protected]>
Co-authored-by: Junkil Park <[email protected]>
  • Loading branch information
@0xOutOfGas @yoyoping @junkil-park
3 people authored Nov 28, 2022
1 parent 59685ad commit d1ee3d6
Show file tree
Hide file tree
Showing 12 changed files with 1,385 additions and 88 deletions.
37 changes: 36 additions & 1 deletion aptos-move/framework/aptos-framework/doc/consensus_config.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ Reconfiguration, and may be updated by root.
- [Function `initialize`](#0x1_consensus_config_initialize)
- [Function `set`](#0x1_consensus_config_set)
- [Specification](#@Specification_1)
- [Function `initialize`](#@Specification_1_initialize)
- [Function `set`](#@Specification_1_set)


Expand Down Expand Up @@ -128,6 +129,34 @@ This can be called by on-chain governance to update on-chain consensus configs.
## Specification



<pre><code><b>pragma</b> verify = <b>true</b>;
<b>pragma</b> aborts_if_is_strict;
</code></pre>



<a name="@Specification_1_initialize"></a>

### Function `initialize`


<pre><code><b>public</b>(<b>friend</b>) <b>fun</b> <a href="consensus_config.md#0x1_consensus_config_initialize">initialize</a>(aptos_framework: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>, config: <a href="../../aptos-stdlib/../move-stdlib/doc/vector.md#0x1_vector">vector</a>&lt;u8&gt;)
</code></pre>


Ensure caller is admin.
Aborts if StateStorageUsage already exists.


<pre><code><b>let</b> 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>(addr);
<b>aborts_if</b> <b>exists</b>&lt;<a href="consensus_config.md#0x1_consensus_config_ConsensusConfig">ConsensusConfig</a>&gt;(@aptos_framework);
<b>aborts_if</b> !(len(config) &gt; 0);
</code></pre>



<a name="@Specification_1_set"></a>

### Function `set`
Expand All @@ -137,9 +166,15 @@ This can be called by on-chain governance to update on-chain consensus configs.
</code></pre>


Ensure the caller is admin and <code><a href="consensus_config.md#0x1_consensus_config_ConsensusConfig">ConsensusConfig</a></code> should be existed.
When setting now time must be later than last_reconfiguration_time.


<pre><code><b>requires</b> <a href="chain_status.md#0x1_chain_status_is_operating">chain_status::is_operating</a>();
<pre><code><b>let</b> 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>aborts_if</b> !<a href="system_addresses.md#0x1_system_addresses_is_aptos_framework_address">system_addresses::is_aptos_framework_address</a>(addr);
<b>aborts_if</b> !<b>exists</b>&lt;<a href="consensus_config.md#0x1_consensus_config_ConsensusConfig">ConsensusConfig</a>&gt;(@aptos_framework);
<b>aborts_if</b> !(len(config) &gt; 0);
<b>requires</b> <a href="chain_status.md#0x1_chain_status_is_operating">chain_status::is_operating</a>();
<b>requires</b> <a href="timestamp.md#0x1_timestamp_spec_now_microseconds">timestamp::spec_now_microseconds</a>() &gt;= <a href="reconfiguration.md#0x1_reconfiguration_last_reconfiguration_time">reconfiguration::last_reconfiguration_time</a>();
</code></pre>

Expand Down
134 changes: 133 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 @@ -20,7 +20,13 @@ to synchronize configuration changes for the validators.
- [Function `current_epoch`](#0x1_reconfiguration_current_epoch)
- [Function `emit_genesis_reconfiguration_event`](#0x1_reconfiguration_emit_genesis_reconfiguration_event)
- [Specification](#@Specification_1)
- [Function `initialize`](#@Specification_1_initialize)
- [Function `disable_reconfiguration`](#@Specification_1_disable_reconfiguration)
- [Function `enable_reconfiguration`](#@Specification_1_enable_reconfiguration)
- [Function `reconfigure`](#@Specification_1_reconfigure)
- [Function `last_reconfiguration_time`](#@Specification_1_last_reconfiguration_time)
- [Function `current_epoch`](#@Specification_1_current_epoch)
- [Function `emit_genesis_reconfiguration_event`](#@Specification_1_emit_genesis_reconfiguration_event)


<pre><code><b>use</b> <a href="account.md#0x1_account">0x1::account</a>;
Expand Down Expand Up @@ -462,12 +468,86 @@ reconfiguration event.



<pre><code><b>invariant</b> [suspendable] <a href="chain_status.md#0x1_chain_status_is_operating">chain_status::is_operating</a>() ==&gt; <b>exists</b>&lt;<a href="reconfiguration.md#0x1_reconfiguration_Configuration">Configuration</a>&gt;(@aptos_framework);
<pre><code><b>pragma</b> verify = <b>true</b>;
<b>pragma</b> aborts_if_is_strict;
<b>invariant</b> [suspendable] <a href="chain_status.md#0x1_chain_status_is_operating">chain_status::is_operating</a>() ==&gt; <b>exists</b>&lt;<a href="reconfiguration.md#0x1_reconfiguration_Configuration">Configuration</a>&gt;(@aptos_framework);
<b>invariant</b> [suspendable] <a href="chain_status.md#0x1_chain_status_is_operating">chain_status::is_operating</a>() ==&gt;
(<a href="timestamp.md#0x1_timestamp_spec_now_microseconds">timestamp::spec_now_microseconds</a>() &gt;= <a href="reconfiguration.md#0x1_reconfiguration_last_reconfiguration_time">last_reconfiguration_time</a>());
</code></pre>


Make sure the signer address is @aptos_framework.


<a name="0x1_reconfiguration_AbortsIfNotAptosFramework"></a>


<pre><code><b>schema</b> <a href="reconfiguration.md#0x1_reconfiguration_AbortsIfNotAptosFramework">AbortsIfNotAptosFramework</a> {
aptos_framework: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>;
<b>let</b> 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>(addr);
}
</code></pre>



<a name="@Specification_1_initialize"></a>

### Function `initialize`


<pre><code><b>public</b>(<b>friend</b>) <b>fun</b> <a href="reconfiguration.md#0x1_reconfiguration_initialize">initialize</a>(aptos_framework: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>)
</code></pre>


Address @aptos_framework must exist resource Account and Configuration.
Already exists in framework account.
Guid_creation_num should be 2 according to logic.


<pre><code><b>include</b> <a href="reconfiguration.md#0x1_reconfiguration_AbortsIfNotAptosFramework">AbortsIfNotAptosFramework</a>;
<b>let</b> addr = <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(aptos_framework);
<b>requires</b> <b>exists</b>&lt;Account&gt;(addr);
<b>aborts_if</b> !(<b>global</b>&lt;Account&gt;(addr).guid_creation_num == 2);
<b>aborts_if</b> <b>exists</b>&lt;<a href="reconfiguration.md#0x1_reconfiguration_Configuration">Configuration</a>&gt;(@aptos_framework);
</code></pre>



<a name="@Specification_1_disable_reconfiguration"></a>

### Function `disable_reconfiguration`


<pre><code><b>fun</b> <a href="reconfiguration.md#0x1_reconfiguration_disable_reconfiguration">disable_reconfiguration</a>(aptos_framework: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>)
</code></pre>




<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);
</code></pre>



<a name="@Specification_1_enable_reconfiguration"></a>

### Function `enable_reconfiguration`


<pre><code><b>fun</b> <a href="reconfiguration.md#0x1_reconfiguration_enable_reconfiguration">enable_reconfiguration</a>(aptos_framework: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>)
</code></pre>


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);
</code></pre>



<a name="@Specification_1_reconfigure"></a>

Expand All @@ -484,4 +564,56 @@ reconfiguration event.
</code></pre>



<a name="@Specification_1_last_reconfiguration_time"></a>

### Function `last_reconfiguration_time`


<pre><code><b>public</b> <b>fun</b> <a href="reconfiguration.md#0x1_reconfiguration_last_reconfiguration_time">last_reconfiguration_time</a>(): u64
</code></pre>




<pre><code><b>aborts_if</b> !<b>exists</b>&lt;<a href="reconfiguration.md#0x1_reconfiguration_Configuration">Configuration</a>&gt;(@aptos_framework);
</code></pre>



<a name="@Specification_1_current_epoch"></a>

### Function `current_epoch`


<pre><code><b>public</b> <b>fun</b> <a href="reconfiguration.md#0x1_reconfiguration_current_epoch">current_epoch</a>(): u64
</code></pre>




<pre><code><b>aborts_if</b> !<b>exists</b>&lt;<a href="reconfiguration.md#0x1_reconfiguration_Configuration">Configuration</a>&gt;(@aptos_framework);
</code></pre>



<a name="@Specification_1_emit_genesis_reconfiguration_event"></a>

### Function `emit_genesis_reconfiguration_event`


<pre><code><b>fun</b> <a href="reconfiguration.md#0x1_reconfiguration_emit_genesis_reconfiguration_event">emit_genesis_reconfiguration_event</a>()
</code></pre>


When genesis_event emit the epoch and the <code>last_reconfiguration_time</code> .
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);
</code></pre>


[move-book]: https://move-language.github.io/move/introduction.html
Loading

0 comments on commit d1ee3d6

Please sign in to comment.