From ab2d0991d932b241f4f531f1e3c5e47c71a049fd Mon Sep 17 00:00:00 2001 From: Zorrot Chen Date: Fri, 16 Jun 2023 06:54:29 +0800 Subject: [PATCH] [Spec] update specs of voting.move (#8557) * init * fix lint * fix linter * fix trimspace * fix comment * fix md --- .../framework/aptos-framework/doc/voting.md | 32 ++++++--- .../aptos-framework/sources/voting.spec.move | 65 ++++++++++++++----- 2 files changed, 70 insertions(+), 27 deletions(-) diff --git a/aptos-move/framework/aptos-framework/doc/voting.md b/aptos-move/framework/aptos-framework/doc/voting.md index 45d08706a1f345..ef1e50db8fae75 100644 --- a/aptos-move/framework/aptos-framework/doc/voting.md +++ b/aptos-move/framework/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-move/framework/aptos-framework/sources/voting.spec.move b/aptos-move/framework/aptos-framework/sources/voting.spec.move
index fd3625d61540ef..0f523f8b083add 100644
--- a/aptos-move/framework/aptos-framework/sources/voting.spec.move
+++ b/aptos-move/framework/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(