Skip to content

Commit

Permalink
[Spec] Added specs for module block & aptos_account & state_storage (a…
Browse files Browse the repository at this point in the history 
…ptos-labs#5478)

* add account.move,coin.move spec

* remove coin.spec.move aborts_if_is_strict

* update specs for account.move and coin.move

* update account.move,coin.move spec

* add account.move,coin.move spec comments

* Merge aptos:main

* Generate account.move.coin.move spec doc

* Trim coin.move spec trailing whitespace

* add spec for aptos_account & block & state_storage

* Generate aptos_account & block & state_storage spec

* Changed schema naming style for block and aptos_account to camelcase

* Remove the aborts if false of get_state_storage_usage_only_at_epoch_beginning() and modify the inappropriate ensures of update_epoch_interval_microsecs()

Co-authored-by: tiutiutiu <[email protected]>
Co-authored-by: 英雄造时势 <[email protected]>
  • Loading branch information
@0xOutOfGas @qpb8023 @yoyoping
3 people authored Nov 15, 2022
1 parent b91aa24 commit e89e898
Show file tree
Hide file tree
Showing 6 changed files with 490 additions and 4 deletions.
116 changes: 116 additions & 0 deletions aptos-move/framework/aptos-framework/doc/aptos_account.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,11 @@
- [Function `transfer`](#0x1_aptos_account_transfer)
- [Function `assert_account_exists`](#0x1_aptos_account_assert_account_exists)
- [Function `assert_account_is_registered_for_apt`](#0x1_aptos_account_assert_account_is_registered_for_apt)
- [Specification](#@Specification_1)
- [Function `create_account`](#@Specification_1_create_account)
- [Function `transfer`](#@Specification_1_transfer)
- [Function `assert_account_exists`](#@Specification_1_assert_account_exists)
- [Function `assert_account_is_registered_for_apt`](#@Specification_1_assert_account_is_registered_for_apt)


<pre><code><b>use</b> <a href="account.md#0x1_account">0x1::account</a>;
Expand Down Expand Up @@ -147,5 +152,116 @@ Basic account creation methods.

</details>

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

## Specification



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



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

### Function `create_account`


<pre><code><b>public</b> entry <b>fun</b> <a href="aptos_account.md#0x1_aptos_account_create_account">create_account</a>(auth_key: <b>address</b>)
</code></pre>


Check if the bytes of the auth_key is 32.
The Account does not exist under the auth_key before creating the account.
Limit the address of auth_key is not @vm_reserved / @aptos_framework / @aptos_toke.


<pre><code><b>include</b> <a href="aptos_account.md#0x1_aptos_account_Create_account">Create_account</a>;
<b>ensures</b> <b>exists</b>&lt;<a href="account.md#0x1_account_Account">account::Account</a>&gt;(auth_key);
<b>ensures</b> <b>exists</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;AptosCoin&gt;&gt;(auth_key);
</code></pre>




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


<pre><code><b>schema</b> <a href="aptos_account.md#0x1_aptos_account_Create_account">Create_account</a> {
auth_key: <b>address</b>;
<b>aborts_if</b> <b>exists</b>&lt;<a href="account.md#0x1_account_Account">account::Account</a>&gt;(auth_key);
<b>aborts_if</b> <a href="aptos_account.md#0x1_aptos_account_length_judgment">length_judgment</a>(auth_key);
<b>aborts_if</b> auth_key == @vm_reserved || auth_key == @aptos_framework || auth_key == @aptos_token;
<b>aborts_if</b> <b>exists</b>&lt;<a href="coin.md#0x1_coin_CoinStore">coin::CoinStore</a>&lt;AptosCoin&gt;&gt;(auth_key);
}
</code></pre>




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


<pre><code><b>fun</b> <a href="aptos_account.md#0x1_aptos_account_length_judgment">length_judgment</a>(auth_key: <b>address</b>): bool {
<b>use</b> std::bcs;

<b>let</b> authentication_key = <a href="../../aptos-stdlib/../move-stdlib/doc/bcs.md#0x1_bcs_to_bytes">bcs::to_bytes</a>(auth_key);
len(authentication_key) != 32
}
</code></pre>



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

### Function `transfer`


<pre><code><b>public</b> entry <b>fun</b> <a href="aptos_account.md#0x1_aptos_account_transfer">transfer</a>(source: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>, <b>to</b>: <b>address</b>, amount: u64)
</code></pre>




<pre><code><b>pragma</b> verify = <b>false</b>;
</code></pre>



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

### Function `assert_account_exists`


<pre><code><b>public</b> <b>fun</b> <a href="aptos_account.md#0x1_aptos_account_assert_account_exists">assert_account_exists</a>(addr: <b>address</b>)
</code></pre>




<pre><code><b>aborts_if</b> !<a href="account.md#0x1_account_exists_at">account::exists_at</a>(addr);
</code></pre>



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

### Function `assert_account_is_registered_for_apt`


<pre><code><b>public</b> <b>fun</b> <a href="aptos_account.md#0x1_aptos_account_assert_account_is_registered_for_apt">assert_account_is_registered_for_apt</a>(addr: <b>address</b>)
</code></pre>


Check if the address existed.
Check if the AptosCoin under the address existed.


<pre><code><b>aborts_if</b> !<a href="account.md#0x1_account_exists_at">account::exists_at</a>(addr);
<b>aborts_if</b> !<a href="coin.md#0x1_coin_is_account_registered">coin::is_account_registered</a>&lt;AptosCoin&gt;(addr);
</code></pre>


[move-book]: https://move-language.github.io/move/introduction.html
164 changes: 164 additions & 0 deletions aptos-move/framework/aptos-framework/doc/block.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,9 +19,14 @@ This module defines a struct storing the metadata of the block and new block eve
- [Function `emit_genesis_block_event`](#0x1_block_emit_genesis_block_event)
- [Function `emit_writeset_block_event`](#0x1_block_emit_writeset_block_event)
- [Specification](#@Specification_1)
- [Function `initialize`](#@Specification_1_initialize)
- [Function `update_epoch_interval_microsecs`](#@Specification_1_update_epoch_interval_microsecs)
- [Function `get_epoch_interval_secs`](#@Specification_1_get_epoch_interval_secs)
- [Function `block_prologue`](#@Specification_1_block_prologue)
- [Function `get_current_block_height`](#@Specification_1_get_current_block_height)
- [Function `emit_new_block_event`](#@Specification_1_emit_new_block_event)
- [Function `emit_genesis_block_event`](#@Specification_1_emit_genesis_block_event)
- [Function `emit_writeset_block_event`](#@Specification_1_emit_writeset_block_event)


<pre><code><b>use</b> <a href="account.md#0x1_account">0x1::account</a>;
Expand Down Expand Up @@ -551,6 +556,113 @@ new block event for WriteSetPayload.



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

### Function `initialize`


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


The caller is aptos_framework.
The new_epoch_interval must be greater than 0.
The BlockResource is not under the caller before initializing.
The Account is not under the caller until the BlockResource is created for the caller.
Make sure The BlockResource under the caller existed after initializing.
The number of new events created does not exceed MAX_U64.


<pre><code><b>include</b> <a href="block.md#0x1_block_Initialize">Initialize</a>;
<b>include</b> <a href="block.md#0x1_block_New_event_handle">New_event_handle</a>;
</code></pre>




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


<pre><code><b>schema</b> <a href="block.md#0x1_block_Initialize">Initialize</a> {
aptos_framework: <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>;
epoch_interval_microsecs: u64;
<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> addr != @aptos_framework;
<b>aborts_if</b> epoch_interval_microsecs &lt;= 0;
<b>aborts_if</b> <b>exists</b>&lt;<a href="block.md#0x1_block_BlockResource">BlockResource</a>&gt;(addr);
<b>ensures</b> <b>exists</b>&lt;<a href="block.md#0x1_block_BlockResource">BlockResource</a>&gt;(addr);
}
</code></pre>




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


<pre><code><b>schema</b> <a href="block.md#0x1_block_New_event_handle">New_event_handle</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>let</b> <a href="account.md#0x1_account">account</a> = <b>global</b>&lt;<a href="account.md#0x1_account_Account">account::Account</a>&gt;(addr);
<b>aborts_if</b> !<b>exists</b>&lt;<a href="account.md#0x1_account_Account">account::Account</a>&gt;(addr);
<b>aborts_if</b> <a href="account.md#0x1_account">account</a>.guid_creation_num + 2 &gt; <a href="block.md#0x1_block_MAX_U64">MAX_U64</a>;
}
</code></pre>



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

### Function `update_epoch_interval_microsecs`


<pre><code><b>public</b> <b>fun</b> <a href="block.md#0x1_block_update_epoch_interval_microsecs">update_epoch_interval_microsecs</a>(aptos_framework: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>, new_epoch_interval: u64)
</code></pre>


The caller is @aptos_framework.
The new_epoch_interval must be greater than 0.
The BlockResource existed under the @aptos_framework.


<pre><code><b>include</b> <a href="block.md#0x1_block_Update_epoch_interval_microsecs">Update_epoch_interval_microsecs</a>;
</code></pre>




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


<pre><code><b>schema</b> <a href="block.md#0x1_block_Update_epoch_interval_microsecs">Update_epoch_interval_microsecs</a> {
aptos_framework: <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>;
new_epoch_interval: u64;
<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> addr != @aptos_framework;
<b>aborts_if</b> new_epoch_interval &lt;= 0;
<b>aborts_if</b> !<b>exists</b>&lt;<a href="block.md#0x1_block_BlockResource">BlockResource</a>&gt;(addr);
<b>ensures</b> <b>exists</b>&lt;<a href="block.md#0x1_block_BlockResource">BlockResource</a>&gt;(addr);
}
</code></pre>



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

### Function `get_epoch_interval_secs`


<pre><code><b>public</b> <b>fun</b> <a href="block.md#0x1_block_get_epoch_interval_secs">get_epoch_interval_secs</a>(): u64
</code></pre>




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



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

### Function `block_prologue`
Expand All @@ -573,6 +685,22 @@ new block event for WriteSetPayload.



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

### Function `get_current_block_height`


<pre><code><b>public</b> <b>fun</b> <a href="block.md#0x1_block_get_current_block_height">get_current_block_height</a>(): u64
</code></pre>




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



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

### Function `emit_new_block_event`
Expand Down Expand Up @@ -615,4 +743,40 @@ new block event for WriteSetPayload.
</code></pre>



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

### Function `emit_writeset_block_event`


<pre><code><b>public</b> <b>fun</b> <a href="block.md#0x1_block_emit_writeset_block_event">emit_writeset_block_event</a>(vm_signer: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>, fake_block_hash: <b>address</b>)
</code></pre>


The caller is @vm_reserved.
The BlockResource existed under the @aptos_framework.
The Configuration existed under the @aptos_framework.
The CurrentTimeMicroseconds existed under the @aptos_framework.


<pre><code><b>include</b> <a href="block.md#0x1_block_Emit_writeset_block_event">Emit_writeset_block_event</a>;
</code></pre>




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


<pre><code><b>schema</b> <a href="block.md#0x1_block_Emit_writeset_block_event">Emit_writeset_block_event</a> {
vm_signer: <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>(vm_signer);
<b>aborts_if</b> addr != @vm_reserved;
<b>aborts_if</b> !<b>exists</b>&lt;<a href="block.md#0x1_block_BlockResource">BlockResource</a>&gt;(@aptos_framework);
<b>aborts_if</b> !<b>exists</b>&lt;<a href="reconfiguration.md#0x1_reconfiguration_Configuration">reconfiguration::Configuration</a>&gt;(@aptos_framework);
<b>aborts_if</b> !<b>exists</b>&lt;<a href="timestamp.md#0x1_timestamp_CurrentTimeMicroseconds">timestamp::CurrentTimeMicroseconds</a>&gt;(@aptos_framework);
}
</code></pre>


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

0 comments on commit e89e898

Please sign in to comment.