Skip to content

Commit

Permalink
fix spec
Browse files Browse the repository at this point in the history
  • Loading branch information
@rahxephon89 @runtian-zhou
rahxephon89 authored and runtian-zhou committed Nov 19, 2024
1 parent bac9db2 commit 1d39406
Show file tree
Hide file tree
Showing 8 changed files with 143 additions and 63 deletions.
53 changes: 2 additions & 51 deletions aptos-move/framework/aptos-framework/doc/aptos_governance.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,6 @@ on a proposal multiple times as long as the total voting power of these votes do
- [Function `get_signer`](#0x1_aptos_governance_get_signer)
- [Function `create_proposal_metadata`](#0x1_aptos_governance_create_proposal_metadata)
- [Function `assert_voting_initialization`](#0x1_aptos_governance_assert_voting_initialization)
- [Function `initialize_for_verification`](#0x1_aptos_governance_initialize_for_verification)
- [Specification](#@Specification_1)
- [High-level Requirements](#high-level-req)
- [Module-level Specification](#module-level-spec)
Expand Down Expand Up @@ -96,7 +95,6 @@ on a proposal multiple times as long as the total voting power of these votes do
- [Function `get_signer`](#@Specification_1_get_signer)
- [Function `create_proposal_metadata`](#@Specification_1_create_proposal_metadata)
- [Function `assert_voting_initialization`](#@Specification_1_assert_voting_initialization)
- [Function `initialize_for_verification`](#@Specification_1_initialize_for_verification)


<pre><code><b>use</b> <a href="account.md#0x1_account">0x1::account</a>;
Expand Down Expand Up @@ -1891,7 +1889,7 @@ Only called in testnet where the core resources account exists and has been gran
<pre><code><b>public</b> <b>fun</b> <a href="aptos_governance.md#0x1_aptos_governance_get_signer_testnet_only">get_signer_testnet_only</a>(
core_resources: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>, signer_address: <b>address</b>): <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a> <b>acquires</b> <a href="aptos_governance.md#0x1_aptos_governance_GovernanceResponsbility">GovernanceResponsbility</a> {
<a href="system_addresses.md#0x1_system_addresses_assert_core_resource">system_addresses::assert_core_resource</a>(core_resources);
// Core resources <a href="account.md#0x1_account">account</a> only <b>has</b> mint capability in tests/testnets.
// Core resources <a href="account.md#0x1_account">account</a> only <b>has</b> mint <a href="../../aptos-stdlib/doc/capability.md#0x1_capability">capability</a> in tests/testnets.
<b>assert</b>!(<a href="aptos_coin.md#0x1_aptos_coin_has_mint_capability">aptos_coin::has_mint_capability</a>(core_resources), <a href="../../aptos-stdlib/../move-stdlib/doc/error.md#0x1_error_unauthenticated">error::unauthenticated</a>(<a href="aptos_governance.md#0x1_aptos_governance_EUNAUTHORIZED">EUNAUTHORIZED</a>));
<a href="aptos_governance.md#0x1_aptos_governance_get_signer">get_signer</a>(signer_address)
}
Expand Down Expand Up @@ -2020,36 +2018,6 @@ Return a signer for making changes to 0x1 as part of on-chain governance proposa



</details>

<a id="0x1_aptos_governance_initialize_for_verification"></a>

## Function `initialize_for_verification`



<pre><code>#[verify_only]
<b>public</b> <b>fun</b> <a href="aptos_governance.md#0x1_aptos_governance_initialize_for_verification">initialize_for_verification</a>(aptos_framework: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>, min_voting_threshold: u128, required_proposer_stake: u64, voting_duration_secs: u64)
</code></pre>



<details>
<summary>Implementation</summary>


<pre><code><b>public</b> <b>fun</b> <a href="aptos_governance.md#0x1_aptos_governance_initialize_for_verification">initialize_for_verification</a>(
aptos_framework: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>,
min_voting_threshold: u128,
required_proposer_stake: u64,
voting_duration_secs: u64,
) {
<a href="aptos_governance.md#0x1_aptos_governance_initialize">initialize</a>(aptos_framework, min_voting_threshold, required_proposer_stake, voting_duration_secs);
}
</code></pre>



</details>

<a id="@Specification_1"></a>
Expand Down Expand Up @@ -2156,6 +2124,7 @@ Limit addition overflow.

<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>let</b> register_account = <b>global</b>&lt;<a href="account.md#0x1_account_Account">account::Account</a>&gt;(addr);
<b>aborts_if</b> <a href="permissioned_signer.md#0x1_permissioned_signer_spec_is_permissioned_signer">permissioned_signer::spec_is_permissioned_signer</a>(aptos_framework);
<b>aborts_if</b> <b>exists</b>&lt;<a href="voting.md#0x1_voting_VotingForum">voting::VotingForum</a>&lt;GovernanceProposal&gt;&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> register_account.guid_creation_num + 7 &gt; <a href="aptos_governance.md#0x1_aptos_governance_MAX_U64">MAX_U64</a>;
Expand Down Expand Up @@ -3243,22 +3212,4 @@ pool_address must exist in StakePool.
</code></pre>



<a id="@Specification_1_initialize_for_verification"></a>

### Function `initialize_for_verification`


<pre><code>#[verify_only]
<b>public</b> <b>fun</b> <a href="aptos_governance.md#0x1_aptos_governance_initialize_for_verification">initialize_for_verification</a>(aptos_framework: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>, min_voting_threshold: u128, required_proposer_stake: u64, voting_duration_secs: u64)
</code></pre>


verify_only


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


[move-book]: https://aptos.dev/move/book/SUMMARY
2 changes: 1 addition & 1 deletion aptos-move/framework/aptos-framework/doc/delegation_pool.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2989,7 +2989,7 @@ The existing voter will be replaced. The function is permissionless.

<b>let</b> <a href="delegation_pool.md#0x1_delegation_pool">delegation_pool</a> = <b>borrow_global</b>&lt;<a href="delegation_pool.md#0x1_delegation_pool_DelegationPool">DelegationPool</a>&gt;(pool_address);
<b>let</b> stake_pool_signer = <a href="delegation_pool.md#0x1_delegation_pool_retrieve_stake_pool_owner">retrieve_stake_pool_owner</a>(<a href="delegation_pool.md#0x1_delegation_pool">delegation_pool</a>);
// delegated_voter is managed by the <a href="stake.md#0x1_stake">stake</a> pool itself, which <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a> capability is managed by <a href="delegation_pool.md#0x1_delegation_pool_DelegationPool">DelegationPool</a>.
// delegated_voter is managed by the <a href="stake.md#0x1_stake">stake</a> pool itself, which <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a> <a href="../../aptos-stdlib/doc/capability.md#0x1_capability">capability</a> is managed by <a href="delegation_pool.md#0x1_delegation_pool_DelegationPool">DelegationPool</a>.
// So <a href="voting.md#0x1_voting">voting</a> power of this <a href="stake.md#0x1_stake">stake</a> pool can only be used through this <b>module</b>.
<a href="stake.md#0x1_stake_set_delegated_voter">stake::set_delegated_voter</a>(&stake_pool_signer, <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(&stake_pool_signer));

Expand Down
56 changes: 54 additions & 2 deletions aptos-move/framework/aptos-framework/doc/staking_proxy.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@
- [Specification](#@Specification_1)
- [High-level Requirements](#high-level-req)
- [Module-level Specification](#module-level-spec)
- [Function `grant_permission`](#@Specification_1_grant_permission)
- [Function `set_operator`](#@Specification_1_set_operator)
- [Function `set_voter`](#@Specification_1_set_voter)
- [Function `set_vesting_contract_operator`](#@Specification_1_set_vesting_contract_operator)
Expand Down Expand Up @@ -436,6 +437,25 @@ Grant permission to mutate staking on behalf of the master signer.



<a id="@Specification_1_grant_permission"></a>

### Function `grant_permission`


<pre><code><b>public</b> <b>fun</b> <a href="staking_proxy.md#0x1_staking_proxy_grant_permission">grant_permission</a>(master: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>, <a href="permissioned_signer.md#0x1_permissioned_signer">permissioned_signer</a>: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>)
</code></pre>




<pre><code><b>pragma</b> aborts_if_is_partial;
<b>aborts_if</b> !<a href="permissioned_signer.md#0x1_permissioned_signer_spec_is_permissioned_signer">permissioned_signer::spec_is_permissioned_signer</a>(<a href="permissioned_signer.md#0x1_permissioned_signer">permissioned_signer</a>);
<b>aborts_if</b> <a href="permissioned_signer.md#0x1_permissioned_signer_spec_is_permissioned_signer">permissioned_signer::spec_is_permissioned_signer</a>(master);
<b>aborts_if</b> <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(master) != <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(<a href="permissioned_signer.md#0x1_permissioned_signer">permissioned_signer</a>);
</code></pre>



<a id="@Specification_1_set_operator"></a>

### Function `set_operator`
Expand Down Expand Up @@ -559,6 +579,12 @@ One of them are not exists


<pre><code><b>include</b> <a href="staking_proxy.md#0x1_staking_proxy_SetStakePoolOperator">SetStakePoolOperator</a>;
<b>include</b> <a href="staking_proxy.md#0x1_staking_proxy_AbortsIfSignerPermissionStakeProxy">AbortsIfSignerPermissionStakeProxy</a> {
s: owner
};
<b>include</b> <b>exists</b>&lt;<a href="stake.md#0x1_stake_StakePool">stake::StakePool</a>&gt;(<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(owner)) ==&gt; <a href="stake.md#0x1_stake_AbortsIfSignerPermissionStake">stake::AbortsIfSignerPermissionStake</a> {
s:owner
};
</code></pre>


Expand All @@ -570,7 +596,9 @@ One of them are not exists
<pre><code><b>schema</b> <a href="staking_proxy.md#0x1_staking_proxy_SetStakePoolOperator">SetStakePoolOperator</a> {
owner: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>;
new_operator: <b>address</b>;
<b>aborts_if</b> <a href="permissioned_signer.md#0x1_permissioned_signer_spec_is_permissioned_signer">permissioned_signer::spec_is_permissioned_signer</a>(owner);
<b>include</b> <a href="staking_proxy.md#0x1_staking_proxy_AbortsIfSignerPermissionStakeProxy">AbortsIfSignerPermissionStakeProxy</a> {
s: owner
};
<b>let</b> owner_address = <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(owner);
<b>let</b> ownership_cap = <b>borrow_global</b>&lt;<a href="stake.md#0x1_stake_OwnerCapability">stake::OwnerCapability</a>&gt;(owner_address);
<b>let</b> pool_address = ownership_cap.pool_address;
Expand Down Expand Up @@ -609,6 +637,9 @@ One of them are not exists


<pre><code><b>include</b> <a href="staking_proxy.md#0x1_staking_proxy_SetStakingContractVoter">SetStakingContractVoter</a>;
<b>include</b> <a href="staking_proxy.md#0x1_staking_proxy_AbortsIfSignerPermissionStakeProxy">AbortsIfSignerPermissionStakeProxy</a> {
s: owner
};
</code></pre>


Expand Down Expand Up @@ -651,6 +682,12 @@ Then abort if the resource is not exist


<pre><code><b>include</b> <a href="staking_proxy.md#0x1_staking_proxy_SetStakePoolVoterAbortsIf">SetStakePoolVoterAbortsIf</a>;
<b>include</b> <a href="staking_proxy.md#0x1_staking_proxy_AbortsIfSignerPermissionStakeProxy">AbortsIfSignerPermissionStakeProxy</a> {
s: owner
};
<b>include</b> <b>exists</b>&lt;<a href="stake.md#0x1_stake_StakePool">stake::StakePool</a>&gt;(<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(owner)) ==&gt; <a href="stake.md#0x1_stake_AbortsIfSignerPermissionStake">stake::AbortsIfSignerPermissionStake</a> {
s:owner
};
</code></pre>


Expand All @@ -662,7 +699,9 @@ Then abort if the resource is not exist
<pre><code><b>schema</b> <a href="staking_proxy.md#0x1_staking_proxy_SetStakePoolVoterAbortsIf">SetStakePoolVoterAbortsIf</a> {
owner: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>;
new_voter: <b>address</b>;
<b>aborts_if</b> <a href="permissioned_signer.md#0x1_permissioned_signer_spec_is_permissioned_signer">permissioned_signer::spec_is_permissioned_signer</a>(owner);
<b>include</b> <a href="staking_proxy.md#0x1_staking_proxy_AbortsIfSignerPermissionStakeProxy">AbortsIfSignerPermissionStakeProxy</a> {
s: owner
};
<b>let</b> owner_address = <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(owner);
<b>let</b> ownership_cap = <b>global</b>&lt;<a href="stake.md#0x1_stake_OwnerCapability">stake::OwnerCapability</a>&gt;(owner_address);
<b>let</b> pool_address = ownership_cap.pool_address;
Expand All @@ -672,4 +711,17 @@ Then abort if the resource is not exist
</code></pre>




<a id="0x1_staking_proxy_AbortsIfSignerPermissionStakeProxy"></a>


<pre><code><b>schema</b> <a href="staking_proxy.md#0x1_staking_proxy_AbortsIfSignerPermissionStakeProxy">AbortsIfSignerPermissionStakeProxy</a> {
s: <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>;
<b>let</b> perm = <a href="staking_proxy.md#0x1_staking_proxy_StakeProxyPermission">StakeProxyPermission</a> {};
<b>aborts_if</b> !<a href="permissioned_signer.md#0x1_permissioned_signer_spec_check_permission_exists">permissioned_signer::spec_check_permission_exists</a>(s, perm);
}
</code></pre>


[move-book]: https://aptos.dev/move/book/SUMMARY
1 change: 1 addition & 0 deletions aptos-move/framework/aptos-framework/sources/aptos_governance.spec.move
View file
Original file line number Diff line number Diff line change
Expand Up @@ -63,6 +63,7 @@ spec aptos_framework::aptos_governance {
let addr = signer::address_of(aptos_framework);
let register_account = global<account::Account>(addr);

aborts_if permissioned_signer::spec_is_permissioned_signer(aptos_framework);
aborts_if exists<voting::VotingForum<GovernanceProposal>>(addr);
aborts_if !exists<account::Account>(addr);
aborts_if register_account.guid_creation_num + 7 > MAX_U64;
Expand Down
53 changes: 46 additions & 7 deletions aptos-move/framework/aptos-framework/sources/stake.spec.move
View file
Original file line number Diff line number Diff line change
Expand Up @@ -125,6 +125,9 @@ spec aptos_framework::stake {
network_addresses: vector<u8>,
fullnode_addresses: vector<u8>,
){
include AbortsIfSignerPermissionStake {
s: account
};
let pubkey_from_pop = bls12381::spec_public_key_from_bytes_with_pop(
consensus_pubkey,
proof_of_possession_from_bytes(proof_of_possession)
Expand Down Expand Up @@ -170,6 +173,9 @@ spec aptos_framework::stake {
// This function casue timeout (property proved)
pragma verify_duration_estimate = 60;
pragma disable_invariants_in_body;
include AbortsIfSignerPermissionStake {
s: operator
};
aborts_if !staking_config::get_allow_validator_set_change(staking_config::get());
aborts_if !exists<StakePool>(pool_address);
aborts_if !exists<ValidatorConfig>(pool_address);
Expand Down Expand Up @@ -223,6 +229,9 @@ spec aptos_framework::stake {
{
// TODO(fa_migration)
pragma verify = false;
include AbortsIfSignerPermissionStake {
s: owner
};
aborts_if reconfiguration_state::spec_is_in_progress();
let addr = signer::address_of(owner);
let ownership_cap = global<OwnerCapability>(addr);
Expand Down Expand Up @@ -262,6 +271,9 @@ spec aptos_framework::stake {
) {
pragma disable_invariants_in_body;
requires chain_status::is_operating();
include AbortsIfSignerPermissionStake {
s: operator
};
aborts_if reconfiguration_state::spec_is_in_progress();
let config = staking_config::get();
aborts_if !staking_config::get_allow_validator_set_change(config);
Expand Down Expand Up @@ -297,13 +309,19 @@ spec aptos_framework::stake {
spec extract_owner_cap(owner: &signer): OwnerCapability {
// TODO: set because of timeout (property proved)
pragma verify_duration_estimate = 300;
include AbortsIfSignerPermissionStake {
s: owner
};
let owner_address = signer::address_of(owner);
aborts_if !exists<OwnerCapability>(owner_address);
ensures !exists<OwnerCapability>(owner_address);
}

spec deposit_owner_cap(owner: &signer, owner_cap: OwnerCapability) {
aborts_if permissioned_signer::spec_is_permissioned_signer(owner);
include AbortsIfSignerPermissionStake {
s: owner
};
// aborts_if permissioned_signer::spec_is_permissioned_signer(owner);
let owner_address = signer::address_of(owner);
aborts_if exists<OwnerCapability>(owner_address);
ensures exists<OwnerCapability>(owner_address);
Expand Down Expand Up @@ -352,7 +370,10 @@ spec aptos_framework::stake {
new_network_addresses: vector<u8>,
new_fullnode_addresses: vector<u8>,
) {
aborts_if permissioned_signer::spec_is_permissioned_signer(operator);
include AbortsIfSignerPermissionStake {
s: operator
};
// aborts_if permissioned_signer::spec_is_permissioned_signer(operator);
let pre_stake_pool = global<StakePool>(pool_address);
let post validator_info = global<ValidatorConfig>(pool_address);
modifies global<ValidatorConfig>(pool_address);
Expand Down Expand Up @@ -399,7 +420,10 @@ spec aptos_framework::stake {
new_consensus_pubkey: vector<u8>,
proof_of_possession: vector<u8>,
) {
aborts_if permissioned_signer::spec_is_permissioned_signer(operator);
include AbortsIfSignerPermissionStake {
s: operator
};
// aborts_if permissioned_signer::spec_is_permissioned_signer(operator);
let pre_stake_pool = global<StakePool>(pool_address);
let post validator_info = global<ValidatorConfig>(pool_address);
aborts_if reconfiguration_state::spec_is_in_progress();
Expand Down Expand Up @@ -505,6 +529,13 @@ spec aptos_framework::stake {
};
}

spec schema AbortsIfSignerPermissionStake {
use aptos_framework::permissioned_signer;
s: signer;
let perm = StakePermission {};
aborts_if !permissioned_signer::spec_check_permission_exists(s, perm);
}

spec schema UpdateStakePoolAbortsIf {
use aptos_std::type_info;

Expand Down Expand Up @@ -593,6 +624,7 @@ spec aptos_framework::stake {
pragma opaque;
// TODO: set because of timeout (property proved)
pragma verify_duration_estimate = 300;
pragma verify = false;
requires rewards_rate <= MAX_REWARDS_RATE;
requires rewards_rate_denominator > 0;
requires rewards_rate <= rewards_rate_denominator;
Expand Down Expand Up @@ -670,18 +702,21 @@ spec aptos_framework::stake {

spec add_stake_with_cap {
pragma disable_invariants_in_body;
pragma verify_duration_estimate = 300;
pragma verify = false;
include ResourceRequirement;
let amount = coins.value;
aborts_if reconfiguration_state::spec_is_in_progress();
include AddStakeWithCapAbortsIfAndEnsures { amount };
}

spec add_stake {
// TODO: These function passed locally however failed in github CI
pragma verify_duration_estimate = 120;
// TODO: fix
pragma verify = false;
// TODO(fa_migration)
pragma aborts_if_is_partial;
include AbortsIfSignerPermissionStake {
s: owner
};
aborts_if reconfiguration_state::spec_is_in_progress();
include ResourceRequirement;
include AddStakeAbortsIfAndEnsures;
Expand All @@ -695,7 +730,11 @@ spec aptos_framework::stake {
) {
// TODO: These function failed in github CI
pragma verify_duration_estimate = 120;

pragma verify = false;
pragma aborts_if_is_partial;
include AbortsIfSignerPermissionStake {
s: owner
};
include ResourceRequirement;
let addr = signer::address_of(owner);
ensures global<ValidatorConfig>(addr) == ValidatorConfig {
Expand Down
Loading

0 comments on commit 1d39406

Please sign in to comment.