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 6 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
60 changes: 57 additions & 3 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 @@ -1637,7 +1637,35 @@ 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>pragma</b> aborts_if_is_strict = <b>false</b>;
<b>include</b> <a href="voting.md#0x1_voting_AbortsIfNotContainProposalID">AbortsIfNotContainProposalID</a>&lt;ProposalType&gt;;
<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;
</code></pre>


Failed


<pre><code><b>aborts_if</b> voting_closed && (proposal.yes_votes &lt;= proposal.no_votes || proposal.yes_votes + proposal.no_votes &lt; proposal.min_vote_threshold);
</code></pre>


Pending


<pre><code><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>));
<b>aborts_if</b> !<a href="../../aptos-stdlib/doc/from_bcs.md#0x1_from_bcs_deserializable">from_bcs::deserializable</a>&lt;u64&gt;(<a href="../../aptos-stdlib/doc/simple_map.md#0x1_simple_map_spec_get">simple_map::spec_get</a>(proposal.metadata, std::string::spec_utf8(<a href="voting.md#0x1_voting_RESOLVABLE_TIME_METADATA_KEY">RESOLVABLE_TIME_METADATA_KEY</a>)));
<b>aborts_if</b> <a href="timestamp.md#0x1_timestamp_spec_now_seconds">timestamp::spec_now_seconds</a>() &lt;= <a href="../../aptos-stdlib/doc/from_bcs.md#0x1_from_bcs_deserialize">from_bcs::deserialize</a>&lt;u64&gt;(<a href="../../aptos-stdlib/doc/simple_map.md#0x1_simple_map_spec_get">simple_map::spec_get</a>(proposal.metadata, std::string::spec_utf8(<a href="voting.md#0x1_voting_RESOLVABLE_TIME_METADATA_KEY">RESOLVABLE_TIME_METADATA_KEY</a>)));
<b>aborts_if</b> <a href="transaction_context.md#0x1_transaction_context_spec_get_script_hash">transaction_context::spec_get_script_hash</a>() != proposal.execution_hash;
</code></pre>


Expand Down Expand Up @@ -1741,9 +1769,35 @@ 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>pragma</b> addition_overflow_unchecked;
<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>include</b> <a href="voting.md#0x1_voting_AbortsIfNotContainProposalID">AbortsIfNotContainProposalID</a>&lt;ProposalType&gt;;
<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;
</code></pre>


Succeeded or Failed


<pre><code><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>
};
</code></pre>


Pending


<pre><code><b>ensures</b> !voting_closed ==&gt; result == <a href="voting.md#0x1_voting_PROPOSAL_STATE_PENDING">PROPOSAL_STATE_PENDING</a>;
</code></pre>


Expand Down
49 changes: 41 additions & 8 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 @@ -115,13 +115,27 @@ spec aptos_framework::voting {
proposal_id: u64,
) {
use aptos_framework::chain_status;

requires chain_status::is_operating(); // Ensures existence of Timestamp
include AbortsIfNotContainProposalID<ProposalType>;

// If the proposal is not resolvable, this function aborts.

// TODO: Find a way to specify when it will abort. The opaque with spec fun doesn't work.
pragma aborts_if_is_strict = false;
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;
/// Failed
rahxephon89 marked this conversation as resolved.
Show resolved Hide resolved
aborts_if voting_closed && (proposal.yes_votes <= proposal.no_votes || proposal.yes_votes + proposal.no_votes < proposal.min_vote_threshold);
/// Pending
rahxephon89 marked this conversation as resolved.
Show resolved Hide resolved
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));
aborts_if !from_bcs::deserializable<u64>(simple_map::spec_get(proposal.metadata, std::string::spec_utf8(RESOLVABLE_TIME_METADATA_KEY)));
aborts_if timestamp::spec_now_seconds() <= from_bcs::deserialize<u64>(simple_map::spec_get(proposal.metadata, std::string::spec_utf8(RESOLVABLE_TIME_METADATA_KEY)));
aborts_if transaction_context::spec_get_script_hash() != proposal.execution_hash;
}

spec resolve<ProposalType: store>(
Expand Down Expand Up @@ -169,11 +183,29 @@ spec aptos_framework::voting {
proposal_id: u64,
): u64 {
use aptos_framework::chain_status;
requires chain_status::is_operating(); // Ensures existence of Timestamp
// Addition of yes_votes and no_votes might overflow.
pragma addition_overflow_unchecked;

requires chain_status::is_operating(); // Ensures existence of Timestamp

include AbortsIfNotContainProposalID<ProposalType>;
// Any way to specify the result?

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;
/// Succeeded or Failed
rahxephon89 marked this conversation as resolved.
Show resolved Hide resolved
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
};

/// Pending
rahxephon89 marked this conversation as resolved.
Show resolved Hide resolved
ensures !voting_closed ==> result == PROPOSAL_STATE_PENDING;
}

spec get_proposal_creation_secs<ProposalType: store>(
Expand Down Expand Up @@ -255,4 +287,5 @@ spec aptos_framework::voting {
requires chain_status::is_operating();
aborts_if false;
}

}