diff --git a/aptos-move/framework/aptos-framework/doc/aptos_governance.md b/aptos-move/framework/aptos-framework/doc/aptos_governance.md index ef3a011b5ed748..c7c97bebe112cc 100644 --- a/aptos-move/framework/aptos-framework/doc/aptos_governance.md +++ b/aptos-move/framework/aptos-framework/doc/aptos_governance.md @@ -39,6 +39,7 @@ on a proposal multiple times as long as the total voting power of these votes do - [Function `get_required_proposer_stake`](#0x1_aptos_governance_get_required_proposer_stake) - [Function `has_entirely_voted`](#0x1_aptos_governance_has_entirely_voted) - [Function `get_remaining_voting_power`](#0x1_aptos_governance_get_remaining_voting_power) +- [Function `assert_proposal_expiration`](#0x1_aptos_governance_assert_proposal_expiration) - [Function `create_proposal`](#0x1_aptos_governance_create_proposal) - [Function `create_proposal_v2`](#0x1_aptos_governance_create_proposal_v2) - [Function `create_proposal_v2_impl`](#0x1_aptos_governance_create_proposal_v2_impl) @@ -74,6 +75,7 @@ on a proposal multiple times as long as the total voting power of these votes do - [Function `get_required_proposer_stake`](#@Specification_1_get_required_proposer_stake) - [Function `has_entirely_voted`](#@Specification_1_has_entirely_voted) - [Function `get_remaining_voting_power`](#@Specification_1_get_remaining_voting_power) + - [Function `assert_proposal_expiration`](#@Specification_1_assert_proposal_expiration) - [Function `create_proposal`](#@Specification_1_create_proposal) - [Function `create_proposal_v2`](#@Specification_1_create_proposal_v2) - [Function `create_proposal_v2_impl`](#@Specification_1_create_proposal_v2_impl) @@ -758,6 +760,16 @@ Partial voting feature hasn't been properly initialized. + + +The proposal has expired. + + +
const EPROPOSAL_EXPIRED: u64 = 15;
+
+
+
+
Proposal is not ready to be resolved. Waiting on time or votes
@@ -1160,6 +1172,43 @@ Note: a stake pool's voting power on a proposal could increase over time(e.g. re
+
+
+
+
+## Function `assert_proposal_expiration`
+
+
+
+public fun assert_proposal_expiration(stake_pool: address, proposal_id: u64)
+
+
+
+
+public fun assert_proposal_expiration(stake_pool: address, proposal_id: u64) {
+ assert_voting_initialization();
+ let proposal_expiration = voting::get_proposal_expiration_secs<GovernanceProposal>(
+ @aptos_framework,
+ proposal_id
+ );
+ // The voter's stake needs to be locked up at least as long as the proposal's expiration.
+ assert!(
+ proposal_expiration <= stake::get_lockup_secs(stake_pool),
+ error::invalid_argument(EINSUFFICIENT_STAKE_LOCKUP),
+ );
+ assert!(
+ timestamp::now_seconds() <= proposal_expiration,
+ error::invalid_argument(EPROPOSAL_EXPIRED),
+ );
+}
+
+
+
+
public fun assert_proposal_expiration(stake_pool: address, proposal_id: u64)
+
+
+
+
+
+include VotingInitializationAbortIfs;
+include voting::AbortsIfNotContainProposalID<GovernanceProposal>{voting_forum_address: @aptos_framework};
+let proposal_expiration = voting::spec_get_proposal_expiration_secs<GovernanceProposal>(@aptos_framework, proposal_id);
+aborts_if !stake::stake_pool_exists(stake_pool);
+aborts_if proposal_expiration > stake::spec_get_lockup_secs(stake_pool);
+aborts_if !exists<timestamp::CurrentTimeMicroseconds>(@aptos_framework);
+aborts_if timestamp::now_seconds() > proposal_expiration;
+
+
+
+
### Function `create_proposal`
diff --git a/aptos-move/framework/aptos-framework/doc/delegation_pool.md b/aptos-move/framework/aptos-framework/doc/delegation_pool.md
index 268d0618fb722f..f9c83df1ff80f6 100644
--- a/aptos-move/framework/aptos-framework/doc/delegation_pool.md
+++ b/aptos-move/framework/aptos-framework/doc/delegation_pool.md
@@ -2955,6 +2955,7 @@ Vote on a proposal with a voter's voting power. To successfully vote, the follow
if (voting_power > remaining_voting_power) {
voting_power = remaining_voting_power;
};
+ aptos_governance::assert_proposal_expiration(pool_address, proposal_id);
assert!(voting_power > 0, error::invalid_argument(ENO_VOTING_POWER));
let governance_records = borrow_global_mut<GovernanceRecords>(pool_address);
diff --git a/aptos-move/framework/aptos-framework/doc/stake.md b/aptos-move/framework/aptos-framework/doc/stake.md
index 53d815ae1ed8a3..dedfe150276419 100644
--- a/aptos-move/framework/aptos-framework/doc/stake.md
+++ b/aptos-move/framework/aptos-framework/doc/stake.md
@@ -4565,148 +4565,6 @@ Returns validator's next epoch voting power, including pending_active, active, a
-
-
-
-
-fun spec_validator_index_upper_bound(): u64 {
- len(global<ValidatorPerformance>(@aptos_framework).validators)
-}
-
-
-
-
-
-
-
-
-fun spec_has_stake_pool(a: address): bool {
- exists<StakePool>(a)
-}
-
-
-
-
-
-
-
-
-fun spec_has_validator_config(a: address): bool {
- exists<ValidatorConfig>(a)
-}
-
-
-
-
-
-
-
-
-fun spec_rewards_amount(
- stake_amount: u64,
- num_successful_proposals: u64,
- num_total_proposals: u64,
- rewards_rate: u64,
- rewards_rate_denominator: u64,
-): u64;
-
-
-
-
-
-
-
-
-fun spec_contains(validators: vector<ValidatorInfo>, addr: address): bool {
- exists i in 0..len(validators): validators[i].addr == addr
-}
-
-
-
-
-
-
-
-
-fun spec_is_current_epoch_validator(pool_address: address): bool {
- let validator_set = global<ValidatorSet>(@aptos_framework);
- !spec_contains(validator_set.pending_active, pool_address)
- && (spec_contains(validator_set.active_validators, pool_address)
- || spec_contains(validator_set.pending_inactive, pool_address))
-}
-
-
-
-
-
-
-
-
-schema ResourceRequirement {
- requires exists<AptosCoinCapabilities>(@aptos_framework);
- requires exists<ValidatorPerformance>(@aptos_framework);
- requires exists<ValidatorSet>(@aptos_framework);
- requires exists<StakingConfig>(@aptos_framework);
- requires exists<StakingRewardsConfig>(@aptos_framework) || !features::spec_periodical_reward_rate_decrease_enabled();
- requires exists<timestamp::CurrentTimeMicroseconds>(@aptos_framework);
-}
-
-
-
-
-
-
-
-
-fun spec_get_reward_rate_1(config: StakingConfig): num {
- if (features::spec_periodical_reward_rate_decrease_enabled()) {
- let epoch_rewards_rate = global<staking_config::StakingRewardsConfig>(@aptos_framework).rewards_rate;
- if (epoch_rewards_rate.value == 0) {
- 0
- } else {
- let denominator_0 = aptos_std::fixed_point64::spec_divide_u128(staking_config::MAX_REWARDS_RATE, epoch_rewards_rate);
- let denominator = if (denominator_0 > MAX_U64) {
- MAX_U64
- } else {
- denominator_0
- };
- let nominator = aptos_std::fixed_point64::spec_multiply_u128(denominator, epoch_rewards_rate);
- nominator
- }
- } else {
- config.rewards_rate
- }
-}
-
-
-
-
-
-
-
-
-fun spec_get_reward_rate_2(config: StakingConfig): num {
- if (features::spec_periodical_reward_rate_decrease_enabled()) {
- let epoch_rewards_rate = global<staking_config::StakingRewardsConfig>(@aptos_framework).rewards_rate;
- if (epoch_rewards_rate.value == 0) {
- 1
- } else {
- let denominator_0 = aptos_std::fixed_point64::spec_divide_u128(staking_config::MAX_REWARDS_RATE, epoch_rewards_rate);
- let denominator = if (denominator_0 > MAX_U64) {
- MAX_U64
- } else {
- denominator_0
- };
- denominator
- }
- } else {
- config.rewards_rate_denominator
- }
-}
-
-
-
-
### Resource `ValidatorSet`
@@ -5492,158 +5350,6 @@ Returns validator's next epoch voting power, including pending_active, active, a
-
-
-
-
-schema AddStakeWithCapAbortsIfAndEnsures {
- owner_cap: OwnerCapability;
- amount: u64;
- let pool_address = owner_cap.pool_address;
- aborts_if !exists<StakePool>(pool_address);
- let config = global<staking_config::StakingConfig>(@aptos_framework);
- let validator_set = global<ValidatorSet>(@aptos_framework);
- let voting_power_increase_limit = config.voting_power_increase_limit;
- let post post_validator_set = global<ValidatorSet>(@aptos_framework);
- let update_voting_power_increase = amount != 0 && (spec_contains(validator_set.active_validators, pool_address)
- || spec_contains(validator_set.pending_active, pool_address));
- aborts_if update_voting_power_increase && validator_set.total_joining_power + amount > MAX_U128;
- ensures update_voting_power_increase ==> post_validator_set.total_joining_power == validator_set.total_joining_power + amount;
- aborts_if update_voting_power_increase && validator_set.total_voting_power > 0
- && validator_set.total_voting_power * voting_power_increase_limit > MAX_U128;
- aborts_if update_voting_power_increase && validator_set.total_voting_power > 0
- && validator_set.total_joining_power + amount > validator_set.total_voting_power * voting_power_increase_limit / 100;
- let stake_pool = global<StakePool>(pool_address);
- let post post_stake_pool = global<StakePool>(pool_address);
- let value_pending_active = stake_pool.pending_active.value;
- let value_active = stake_pool.active.value;
- ensures amount != 0 && spec_is_current_epoch_validator(pool_address) ==> post_stake_pool.pending_active.value == value_pending_active + amount;
- ensures amount != 0 && !spec_is_current_epoch_validator(pool_address) ==> post_stake_pool.active.value == value_active + amount;
- let maximum_stake = config.maximum_stake;
- let value_pending_inactive = stake_pool.pending_inactive.value;
- let next_epoch_voting_power = value_pending_active + value_active + value_pending_inactive;
- let voting_power = next_epoch_voting_power + amount;
- aborts_if amount != 0 && voting_power > MAX_U64;
- aborts_if amount != 0 && voting_power > maximum_stake;
-}
-
-
-
-
-
-
-
-
-schema AddStakeAbortsIfAndEnsures {
- owner: signer;
- amount: u64;
- let owner_address = signer::address_of(owner);
- aborts_if !exists<OwnerCapability>(owner_address);
- let owner_cap = global<OwnerCapability>(owner_address);
- include AddStakeWithCapAbortsIfAndEnsures { owner_cap };
-}
-
-
-
-
-
-
-
-
-fun spec_is_allowed(account: address): bool {
- if (!exists<AllowedValidators>(@aptos_framework)) {
- true
- } else {
- let allowed = global<AllowedValidators>(@aptos_framework);
- contains(allowed.accounts, account)
- }
-}
-
-
-
-
-
-
-
-
-fun spec_find_validator(v: vector<ValidatorInfo>, addr: address): Option<u64>;
-
-
-
-
-
-
-
-
-fun spec_validators_are_initialized(validators: vector<ValidatorInfo>): bool {
- forall i in 0..len(validators):
- spec_has_stake_pool(validators[i].addr) &&
- spec_has_validator_config(validators[i].addr)
-}
-
-
-
-
-
-
-
-
-fun spec_validators_are_initialized_addrs(addrs: vector<address>): bool {
- forall i in 0..len(addrs):
- spec_has_stake_pool(addrs[i]) &&
- spec_has_validator_config(addrs[i])
-}
-
-
-
-
-
-
-
-
-fun spec_validator_indices_are_valid(validators: vector<ValidatorInfo>): bool {
- spec_validator_indices_are_valid_addr(validators, spec_validator_index_upper_bound()) &&
- spec_validator_indices_are_valid_config(validators, spec_validator_index_upper_bound())
-}
-
-
-
-
-
-
-
-
-fun spec_validator_indices_are_valid_addr(validators: vector<ValidatorInfo>, upper_bound: u64): bool {
- forall i in 0..len(validators):
- global<ValidatorConfig>(validators[i].addr).validator_index < upper_bound
-}
-
-
-
-
-
-
-
-
-fun spec_validator_indices_are_valid_config(validators: vector<ValidatorInfo>, upper_bound: u64): bool {
- forall i in 0..len(validators):
- validators[i].config.validator_index < upper_bound
-}
-
-
-
-
-
-
-
-
-fun spec_validator_indices_active_pending_inactive(validator_set: ValidatorSet): bool {
- len(validator_set.pending_inactive) + len(validator_set.active_validators) == spec_validator_index_upper_bound()
-}
-
-
-
-
### Function `update_stake_pool`
@@ -5755,6 +5461,17 @@ Returns validator's next epoch voting power, including pending_active, active, a
+
+
+
+
+fun spec_get_lockup_secs(pool_address: address): u64 {
+ global<StakePool>(pool_address).locked_until_secs
+}
+
+
+
+
### Function `calculate_rewards_amount`
diff --git a/aptos-move/framework/aptos-framework/sources/aptos_governance.move b/aptos-move/framework/aptos-framework/sources/aptos_governance.move
index fb1469bc7e6841..f5de768d05864d 100644
--- a/aptos-move/framework/aptos-framework/sources/aptos_governance.move
+++ b/aptos-move/framework/aptos-framework/sources/aptos_governance.move
@@ -62,6 +62,8 @@ module aptos_framework::aptos_governance {
const EPARTIAL_VOTING_NOT_INITIALIZED: u64 = 13;
/// The proposal in the argument is not a partial voting proposal.
const ENOT_PARTIAL_VOTING_PROPOSAL: u64 = 14;
+ /// The proposal has expired.
+ const EPROPOSAL_EXPIRED: u64 = 15;
/// This matches the same enum const in voting. We have to duplicate it as Move doesn't have support for enums yet.
const PROPOSAL_STATE_SUCCEEDED: u64 = 1;
@@ -331,6 +333,23 @@ module aptos_framework::aptos_governance {
get_voting_power(stake_pool) - used_voting_power
}
+ public fun assert_proposal_expiration(stake_pool: address, proposal_id: u64) {
+ assert_voting_initialization();
+ let proposal_expiration = voting::get_proposal_expiration_secs