Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Spec] update specs of voting.move #8557

Merged
merged 13 commits into from
Jun 15, 2023
Merged

[Spec] update specs of voting.move #8557

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
c8cf835
init
UIZorrot Jun 7, 2023
82a1988
Merge branch 'aptos-labs:main' into spec_update_voting
UIZorrot Jun 7, 2023
aa33321
fix lint
UIZorrot Jun 8, 2023
9021fe3
Merge branch 'spec_update_voting' of https://github.com/movebit/aptos…
UIZorrot Jun 8, 2023
39fb211
fix linter
UIZorrot Jun 12, 2023
5e0ab04
fix trimspace
UIZorrot Jun 12, 2023
fbbb2c2
fix comment
UIZorrot Jun 12, 2023
de1522a
Merge branch 'main' into spec_update_voting
UIZorrot Jun 13, 2023
bd1e457
Merge branch 'main' into spec_update_voting
UIZorrot Jun 14, 2023
9adcf37
Merge branch 'spec_update_voting' of https://github.com/movebit/aptos…
UIZorrot Jun 15, 2023
fab91cd
Merge branch 'main' into spec_update_voting
UIZorrot Jun 15, 2023
d2c4c68
Merge branch 'spec_update_voting' of https://github.com/movebit/aptos…
UIZorrot Jun 15, 2023
5c7f814
fix md
UIZorrot Jun 15, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
32 changes: 23 additions & 9 deletions aptos-move/framework/aptos-framework/doc/voting.md
View file
Open in desktop
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
Open in desktop
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