diff --git a/aptos-framework/doc/voting.md b/aptos-framework/doc/voting.md index 45d08706a..ef1e50db8 100644 --- a/aptos-framework/doc/voting.md +++ b/aptos-framework/doc/voting.md @@ -1555,11 +1555,6 @@ Return true if the voting period of the given proposal has already ended. -The min_vote_threshold lower thanearly_resolution_vote_threshold. -Make sure the execution script's hash is not empty. -VotingForum existed under the voting_forum_address. -The next_proposal_id in VotingForum is up to MAX_U64. -CurrentTimeMicroseconds existed under the @aptos_framework.
requires chain_status::is_operating();
@@ -1638,9 +1633,16 @@ CurrentTimeMicroseconds existed under the @aptos_framework.
 
 
requires chain_status::is_operating();
 include AbortsIfNotContainProposalID<ProposalType>;
-aborts_if spec_get_proposal_state<ProposalType>(voting_forum_address, proposal_id) != PROPOSAL_STATE_SUCCEEDED;
 let voting_forum =  global<VotingForum<ProposalType>>(voting_forum_address);
 let proposal = table::spec_get(voting_forum.proposals, proposal_id);
+let early_resolution_threshold = option::spec_borrow(proposal.early_resolution_vote_threshold);
+let voting_period_over = timestamp::now_seconds() > proposal.expiration_secs;
+let be_resolved_early = option::spec_is_some(proposal.early_resolution_vote_threshold) &&
+                            (proposal.yes_votes >= early_resolution_threshold ||
+                             proposal.no_votes >= early_resolution_threshold);
+let voting_closed = voting_period_over || be_resolved_early;
+aborts_if voting_closed && (proposal.yes_votes <= proposal.no_votes || proposal.yes_votes + proposal.no_votes < proposal.min_vote_threshold);
+aborts_if !voting_closed;
 aborts_if proposal.is_resolved;
 aborts_if !std::string::spec_internal_check_utf8(RESOLVABLE_TIME_METADATA_KEY);
 aborts_if !simple_map::spec_contains_key(proposal.metadata, std::string::spec_utf8(RESOLVABLE_TIME_METADATA_KEY));
@@ -1762,11 +1764,23 @@ CurrentTimeMicroseconds existed under the @aptos_framework.
 
 
 
-
pragma opaque;
+
pragma addition_overflow_unchecked;
 requires chain_status::is_operating();
-pragma addition_overflow_unchecked;
 include AbortsIfNotContainProposalID<ProposalType>;
-ensures [abstract] result == spec_get_proposal_state<ProposalType>(voting_forum_address, proposal_id);
+let voting_forum = global<VotingForum<ProposalType>>(voting_forum_address);
+let proposal = table::spec_get(voting_forum.proposals, proposal_id);
+let early_resolution_threshold = option::spec_borrow(proposal.early_resolution_vote_threshold);
+let voting_period_over = timestamp::now_seconds() > proposal.expiration_secs;
+let be_resolved_early = option::spec_is_some(proposal.early_resolution_vote_threshold) &&
+                            (proposal.yes_votes >= early_resolution_threshold ||
+                             proposal.no_votes >= early_resolution_threshold);
+let voting_closed = voting_period_over || be_resolved_early;
+ensures voting_closed ==> if (proposal.yes_votes > proposal.no_votes && proposal.yes_votes + proposal.no_votes >= proposal.min_vote_threshold) {
+    result == PROPOSAL_STATE_SUCCEEDED
+} else {
+    result == PROPOSAL_STATE_FAILED
+};
+ensures !voting_closed ==> result == PROPOSAL_STATE_PENDING;
 
diff --git a/aptos-framework/sources/voting.spec.move b/aptos-framework/sources/voting.spec.move index fd3625d61..0f523f8b0 100644 --- a/aptos-framework/sources/voting.spec.move +++ b/aptos-framework/sources/voting.spec.move @@ -36,11 +36,11 @@ spec aptos_framework::voting { include CreateProposalAbortsIf{is_multi_step_proposal: false}; } - /// The min_vote_threshold lower thanearly_resolution_vote_threshold. - /// Make sure the execution script's hash is not empty. - /// VotingForum existed under the voting_forum_address. - /// The next_proposal_id in VotingForum is up to MAX_U64. - /// CurrentTimeMicroseconds existed under the @aptos_framework. + // The min_vote_threshold lower thanearly_resolution_vote_threshold. + // Make sure the execution script's hash is not empty. + // VotingForum existed under the voting_forum_address. + // The next_proposal_id in VotingForum is up to MAX_U64. + // CurrentTimeMicroseconds existed under the @aptos_framework. spec create_proposal_v2( proposer: address, voting_forum_address: address, @@ -90,7 +90,8 @@ spec aptos_framework::voting { should_pass: bool, ) { use aptos_framework::chain_status; - requires chain_status::is_operating(); // Ensures existence of Timestamp + // Ensures existence of Timestamp + requires chain_status::is_operating(); aborts_if !exists>(voting_forum_address); let voting_forum = global>(voting_forum_address); @@ -116,14 +117,22 @@ spec aptos_framework::voting { ) { use aptos_framework::chain_status; - - requires chain_status::is_operating(); // Ensures existence of Timestamp + // Ensures existence of Timestamp + requires chain_status::is_operating(); include AbortsIfNotContainProposalID; - // If the proposal is not resolvable, this function aborts. - aborts_if spec_get_proposal_state(voting_forum_address, proposal_id) != PROPOSAL_STATE_SUCCEEDED; let voting_forum = global>(voting_forum_address); let proposal = table::spec_get(voting_forum.proposals, proposal_id); + let early_resolution_threshold = option::spec_borrow(proposal.early_resolution_vote_threshold); + let voting_period_over = timestamp::now_seconds() > proposal.expiration_secs; + let be_resolved_early = option::spec_is_some(proposal.early_resolution_vote_threshold) && + (proposal.yes_votes >= early_resolution_threshold || + proposal.no_votes >= early_resolution_threshold); + let voting_closed = voting_period_over || be_resolved_early; + // Avoid Overflow + aborts_if voting_closed && (proposal.yes_votes <= proposal.no_votes || proposal.yes_votes + proposal.no_votes < proposal.min_vote_threshold); + // Resolvable_time Properties + aborts_if !voting_closed; aborts_if proposal.is_resolved; aborts_if !std::string::spec_internal_check_utf8(RESOLVABLE_TIME_METADATA_KEY); @@ -138,7 +147,8 @@ spec aptos_framework::voting { proposal_id: u64, ): ProposalType { use aptos_framework::chain_status; - requires chain_status::is_operating(); // Ensures existence of Timestamp + // Ensures existence of Timestamp + requires chain_status::is_operating(); pragma aborts_if_is_partial; include AbortsIfNotContainProposalID; @@ -151,7 +161,8 @@ spec aptos_framework::voting { next_execution_hash: vector, ) { use aptos_framework::chain_status; - requires chain_status::is_operating(); // Ensures existence of Timestamp + // Ensures existence of Timestamp + requires chain_status::is_operating(); pragma aborts_if_is_partial; include AbortsIfNotContainProposalID; @@ -165,7 +176,8 @@ spec aptos_framework::voting { spec is_voting_closed(voting_forum_address: address, proposal_id: u64): bool { use aptos_framework::chain_status; - requires chain_status::is_operating(); // Ensures existence of Timestamp + // Ensures existence of Timestamp + requires chain_status::is_operating(); include AbortsIfNotContainProposalID; } @@ -184,14 +196,31 @@ spec aptos_framework::voting { ): u64 { use aptos_framework::chain_status; - pragma opaque; - requires chain_status::is_operating(); // Ensures existence of Timestamp - // Addition of yes_votes and no_votes might overflow. + pragma addition_overflow_unchecked; + // Ensures existence of Timestamp + requires chain_status::is_operating(); include AbortsIfNotContainProposalID; - // Any way to specify the result? - ensures [abstract] result == spec_get_proposal_state(voting_forum_address, proposal_id); + + let voting_forum = global>(voting_forum_address); + let proposal = table::spec_get(voting_forum.proposals, proposal_id); + let early_resolution_threshold = option::spec_borrow(proposal.early_resolution_vote_threshold); + let voting_period_over = timestamp::now_seconds() > proposal.expiration_secs; + let be_resolved_early = option::spec_is_some(proposal.early_resolution_vote_threshold) && + (proposal.yes_votes >= early_resolution_threshold || + proposal.no_votes >= early_resolution_threshold); + let voting_closed = voting_period_over || be_resolved_early; + // Voting Succeeded or Failed + ensures voting_closed ==> if (proposal.yes_votes > proposal.no_votes && proposal.yes_votes + proposal.no_votes >= proposal.min_vote_threshold) { + result == PROPOSAL_STATE_SUCCEEDED + } else { + result == PROPOSAL_STATE_FAILED + }; + + // Voting is Pending + ensures !voting_closed ==> result == PROPOSAL_STATE_PENDING; + } spec get_proposal_creation_secs(