Skip to content

Commit

Permalink
[Spec] update specs of voting.move (aptos-labs#8557)
Browse files Browse the repository at this point in the history 
* init

* fix lint

* fix linter

* fix trimspace

* fix comment

* fix md
  • Loading branch information
@UIZorrot @xbtmatt
UIZorrot authored and xbtmatt committed Jul 25, 2023
1 parent 0e3be04 commit 0c167f6
Show file tree
Hide file tree
Showing 2 changed files with 70 additions and 27 deletions.
32 changes: 23 additions & 9 deletions aptos-move/framework/aptos-framework/doc/voting.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1555,11 +1555,6 @@ Return true if the voting period of the given proposal has already ended.
</code></pre>


The min_vote_threshold lower thanearly_resolution_vote_threshold.
Make sure the execution script's hash is not empty.
VotingForum<ProposalType> existed under the voting_forum_address.
The next_proposal_id in VotingForum is up to MAX_U64.
CurrentTimeMicroseconds existed under the @aptos_framework.


<pre><code><b>requires</b> <a href="chain_status.md#0x1_chain_status_is_operating">chain_status::is_operating</a>();
Expand Down Expand Up @@ -1638,9 +1633,16 @@ CurrentTimeMicroseconds existed under the @aptos_framework.

<pre><code><b>requires</b> <a href="chain_status.md#0x1_chain_status_is_operating">chain_status::is_operating</a>();
<b>include</b> <a href="voting.md#0x1_voting_AbortsIfNotContainProposalID">AbortsIfNotContainProposalID</a>&lt;ProposalType&gt;;
<b>aborts_if</b> <a href="voting.md#0x1_voting_spec_get_proposal_state">spec_get_proposal_state</a>&lt;ProposalType&gt;(voting_forum_address, proposal_id) != <a href="voting.md#0x1_voting_PROPOSAL_STATE_SUCCEEDED">PROPOSAL_STATE_SUCCEEDED</a>;
<b>let</b> voting_forum = <b>global</b>&lt;<a href="voting.md#0x1_voting_VotingForum">VotingForum</a>&lt;ProposalType&gt;&gt;(voting_forum_address);
<b>let</b> proposal = <a href="../../aptos-stdlib/doc/table.md#0x1_table_spec_get">table::spec_get</a>(voting_forum.proposals, proposal_id);
<b>let</b> early_resolution_threshold = <a href="../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_spec_borrow">option::spec_borrow</a>(proposal.early_resolution_vote_threshold);
<b>let</b> voting_period_over = <a href="timestamp.md#0x1_timestamp_now_seconds">timestamp::now_seconds</a>() &gt; proposal.expiration_secs;
<b>let</b> be_resolved_early = <a href="../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_spec_is_some">option::spec_is_some</a>(proposal.early_resolution_vote_threshold) &&
(proposal.yes_votes &gt;= early_resolution_threshold ||
proposal.no_votes &gt;= early_resolution_threshold);
<b>let</b> voting_closed = voting_period_over || be_resolved_early;
<b>aborts_if</b> voting_closed && (proposal.yes_votes &lt;= proposal.no_votes || proposal.yes_votes + proposal.no_votes &lt; proposal.min_vote_threshold);
<b>aborts_if</b> !voting_closed;
<b>aborts_if</b> proposal.is_resolved;
<b>aborts_if</b> !std::string::spec_internal_check_utf8(<a href="voting.md#0x1_voting_RESOLVABLE_TIME_METADATA_KEY">RESOLVABLE_TIME_METADATA_KEY</a>);
<b>aborts_if</b> !<a href="../../aptos-stdlib/doc/simple_map.md#0x1_simple_map_spec_contains_key">simple_map::spec_contains_key</a>(proposal.metadata, std::string::spec_utf8(<a href="voting.md#0x1_voting_RESOLVABLE_TIME_METADATA_KEY">RESOLVABLE_TIME_METADATA_KEY</a>));
Expand Down Expand Up @@ -1762,11 +1764,23 @@ CurrentTimeMicroseconds existed under the @aptos_framework.



<pre><code><b>pragma</b> opaque;
<pre><code><b>pragma</b> addition_overflow_unchecked;
<b>requires</b> <a href="chain_status.md#0x1_chain_status_is_operating">chain_status::is_operating</a>();
<b>pragma</b> addition_overflow_unchecked;
<b>include</b> <a href="voting.md#0x1_voting_AbortsIfNotContainProposalID">AbortsIfNotContainProposalID</a>&lt;ProposalType&gt;;
<b>ensures</b> [abstract] result == <a href="voting.md#0x1_voting_spec_get_proposal_state">spec_get_proposal_state</a>&lt;ProposalType&gt;(voting_forum_address, proposal_id);
<b>let</b> voting_forum = <b>global</b>&lt;<a href="voting.md#0x1_voting_VotingForum">VotingForum</a>&lt;ProposalType&gt;&gt;(voting_forum_address);
<b>let</b> proposal = <a href="../../aptos-stdlib/doc/table.md#0x1_table_spec_get">table::spec_get</a>(voting_forum.proposals, proposal_id);
<b>let</b> early_resolution_threshold = <a href="../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_spec_borrow">option::spec_borrow</a>(proposal.early_resolution_vote_threshold);
<b>let</b> voting_period_over = <a href="timestamp.md#0x1_timestamp_now_seconds">timestamp::now_seconds</a>() &gt; proposal.expiration_secs;
<b>let</b> be_resolved_early = <a href="../../aptos-stdlib/../move-stdlib/doc/option.md#0x1_option_spec_is_some">option::spec_is_some</a>(proposal.early_resolution_vote_threshold) &&
(proposal.yes_votes &gt;= early_resolution_threshold ||
proposal.no_votes &gt;= early_resolution_threshold);
<b>let</b> voting_closed = voting_period_over || be_resolved_early;
<b>ensures</b> voting_closed ==&gt; <b>if</b> (proposal.yes_votes &gt; proposal.no_votes && proposal.yes_votes + proposal.no_votes &gt;= proposal.min_vote_threshold) {
result == <a href="voting.md#0x1_voting_PROPOSAL_STATE_SUCCEEDED">PROPOSAL_STATE_SUCCEEDED</a>
} <b>else</b> {
result == <a href="voting.md#0x1_voting_PROPOSAL_STATE_FAILED">PROPOSAL_STATE_FAILED</a>
};
<b>ensures</b> !voting_closed ==&gt; result == <a href="voting.md#0x1_voting_PROPOSAL_STATE_PENDING">PROPOSAL_STATE_PENDING</a>;
</code></pre>


Expand Down
65 changes: 47 additions & 18 deletions aptos-move/framework/aptos-framework/sources/voting.spec.move
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,11 +36,11 @@ spec aptos_framework::voting {
include CreateProposalAbortsIf<ProposalType>{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<ProposalType> 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<ProposalType> 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<ProposalType: store>(
proposer: address,
voting_forum_address: address,
Expand Down Expand Up @@ -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<VotingForum<ProposalType>>(voting_forum_address);
let voting_forum = global<VotingForum<ProposalType>>(voting_forum_address);
Expand All @@ -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<ProposalType>;
// If the proposal is not resolvable, this function aborts.
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;
// 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);
Expand All @@ -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<ProposalType>;
Expand All @@ -151,7 +161,8 @@ spec aptos_framework::voting {
next_execution_hash: vector<u8>,
) {
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<ProposalType>;
Expand All @@ -165,7 +176,8 @@ spec aptos_framework::voting {

spec is_voting_closed<ProposalType: store>(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<ProposalType>;
}

Expand All @@ -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<ProposalType>;
// Any way to specify the result?
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;
// 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<ProposalType: store>(
Expand Down

0 comments on commit 0c167f6

Please sign in to comment.