Skip to content
Aptos Docs

voting - [mainnet]

This is the general Voting module that can be used as part of a DAO Governance. Voting is designed to be used by standalone governance modules, who has full control over the voting flow and is responsible for voting power calculation and including proper capabilities when creating the proposal so resolution can go through. On-chain governance of the Aptos network also uses Voting.

The voting flow:

  1. The Voting module can be deployed at a known address (e.g. 0x1 for Aptos on-chain governance)
  2. The governance module, e.g. AptosGovernance, can be deployed later and define a GovernanceProposal resource type that can also contain other information such as Capability resource for authorization.
  3. The governance module’s owner can then register the ProposalType with Voting. This also hosts the proposal list (forum) on the calling account.
  4. A proposer, through the governance module, can call Voting::create_proposal to create a proposal. create_proposal cannot be called directly not through the governance module. A script hash of the resolution script that can later be called to execute the proposal is required.
  5. A voter, through the governance module, can call Voting::vote on a proposal. vote requires passing a &ProposalType and thus only the governance module that registers ProposalType can call vote.
  6. Once the proposal’s expiration time has passed and more than the defined threshold has voted yes on the proposal, anyone can call resolve which returns the content of the proposal (of type ProposalType) that can be used to execute.
  7. Only the resolution script with the same script hash specified in the proposal can call Voting::resolve as part of the resolution process.
use 0x1::account;
use 0x1::bcs;
use 0x1::error;
use 0x1::event;
use 0x1::features;
use 0x1::from_bcs;
use 0x1::option;
use 0x1::permissioned_signer;
use 0x1::signer;
use 0x1::simple_map;
use 0x1::string;
use 0x1::table;
use 0x1::timestamp;
use 0x1::transaction_context;
use 0x1::type_info;

Constants

Minimum vote threshold cannot be higher than early resolution threshold.

const EINVALID_MIN_VOTE_THRESHOLD: u64 = 7;

If a proposal is multi-step, we need to use resolve_proposal_v2() to resolve it. If we use resolve() to resolve a multi-step proposal, it will fail with EMULTI_STEP_PROPOSAL_CANNOT_USE_SINGLE_STEP_RESOLVE_FUNCTION.

const EMULTI_STEP_PROPOSAL_CANNOT_USE_SINGLE_STEP_RESOLVE_FUNCTION: u64 = 10;

Cannot vote if the specified multi-step proposal is in execution.

const EMULTI_STEP_PROPOSAL_IN_EXECUTION: u64 = 9;

Cannot call is_multi_step_proposal_in_execution() on single-step proposals.

const ENO_VOTE_PERMISSION: u64 = 13;

Proposal cannot be resolved more than once

const EPROPOSAL_ALREADY_RESOLVED: u64 = 3;

Proposal cannot be resolved. Either voting duration has not passed, not enough votes, or fewer yes than no votes

const EPROPOSAL_CANNOT_BE_RESOLVED: u64 = 2;

Proposal cannot contain an empty execution script hash

const EPROPOSAL_EMPTY_EXECUTION_HASH: u64 = 4;

Current script’s execution hash does not match the specified proposal’s

const EPROPOSAL_EXECUTION_HASH_NOT_MATCHING: u64 = 1;

Cannot call is_multi_step_proposal_in_execution() on single-step proposals.

const EPROPOSAL_IS_SINGLE_STEP: u64 = 12;

Proposal’s voting period has already ended.

const EPROPOSAL_VOTING_ALREADY_ENDED: u64 = 5;

Resolution of a proposal cannot happen atomically in the same transaction as the last vote.

const ERESOLUTION_CANNOT_BE_ATOMIC: u64 = 8;

If we call resolve_proposal_v2() to resolve a single-step proposal, the next_execution_hash parameter should be an empty vector.

const ESINGLE_STEP_PROPOSAL_CANNOT_HAVE_NEXT_EXECUTION_HASH: u64 = 11;

Voting forum has already been registered.

const EVOTING_FORUM_ALREADY_REGISTERED: u64 = 6;

Key used to track if the multi-step proposal is in execution / resolving in progress.

const IS_MULTI_STEP_PROPOSAL_IN_EXECUTION_KEY: vector<u8> = [73, 83, 95, 77, 85, 76, 84, 73, 95, 83, 84, 69, 80, 95, 80, 82, 79, 80, 79, 83, 65, 76, 95, 73, 78, 95, 69, 88, 69, 67, 85, 84, 73, 79, 78];

Key used to track if the proposal is multi-step

const IS_MULTI_STEP_PROPOSAL_KEY: vector<u8> = [73, 83, 95, 77, 85, 76, 84, 73, 95, 83, 84, 69, 80, 95, 80, 82, 79, 80, 79, 83, 65, 76, 95, 75, 69, 89];

Proposal has failed because either the min vote threshold is not met or majority voted no.

const PROPOSAL_STATE_FAILED: u64 = 3;

ProposalStateEnum representing proposal state.

const PROPOSAL_STATE_PENDING: u64 = 0;
const PROPOSAL_STATE_SUCCEEDED: u64 = 1;

Key used to track the resolvable time in the proposal’s metadata.

const RESOLVABLE_TIME_METADATA_KEY: vector<u8> = [82, 69, 83, 79, 76, 86, 65, 66, 76, 69, 95, 84, 73, 77, 69, 95, 77, 69, 84, 65, 68, 65, 84, 65, 95, 75, 69, 89];

Structs

Proposal

Extra metadata (e.g. description, code url) can be part of the ProposalType struct.

struct Proposal<ProposalType: store> has store
Fields
proposer: address
Required. The address of the proposer.
execution_content: option::Option<ProposalType>
Required. Should contain enough information to execute later, for example the required capability. This is stored as an option so we can return it to governance when the proposal is resolved.
metadata: simple_map::SimpleMap<string::String, vector<u8>>
Optional. Value is serialized value of an attribute. Currently, we have three attributes that are used by the voting flow. 1. RESOLVABLE_TIME_METADATA_KEY: this is uesed to record the resolvable time to ensure that resolution has to be done non-atomically. 2. IS_MULTI_STEP_PROPOSAL_KEY: this is used to track if a proposal is single-step or multi-step. 3. IS_MULTI_STEP_PROPOSAL_IN_EXECUTION_KEY: this attribute only applies to multi-step proposals. A single-step proposal will not have this field in its metadata map. The value is used to indicate if a multi-step proposal is in execution. If yes, we will disable further voting for this multi-step proposal.
creation_time_secs: u64
Timestamp when the proposal was created.
execution_hash: vector<u8>
Required. The hash for the execution script module. Only the same exact script module can resolve this proposal.
min_vote_threshold: u128
A proposal is only resolved if expiration has passed and the number of votes is above threshold.
expiration_secs: u64
early_resolution_vote_threshold: option::Option<u128>
Optional. Early resolution threshold. If specified, the proposal can be resolved early if the total number of yes or no votes passes this threshold. For example, this can be set to 50% of the total supply of the voting token, so if > 50% vote yes or no, the proposal can be resolved before expiration.
yes_votes: u128
Number of votes for each outcome. u128 since the voting power is already u64 and can add up to more than u64 can hold.
no_votes: u128
is_resolved: bool
Whether the proposal has been resolved.
resolution_time_secs: u64
Resolution timestamp if the proposal has been resolved. 0 otherwise.

VotingEvents

struct VotingEvents has store
Fields
create_proposal_events: event::EventHandle<voting::CreateProposalEvent>
register_forum_events: event::EventHandle<voting::RegisterForumEvent>
resolve_proposal_events: event::EventHandle<voting::ResolveProposal>
vote_events: event::EventHandle<voting::VoteEvent>

CreateProposal

#[event]
struct CreateProposal has drop, store
Fields
proposal_id: u64
early_resolution_vote_threshold: option::Option<u128>
execution_hash: vector<u8>
expiration_secs: u64
metadata: simple_map::SimpleMap<string::String, vector<u8>>
min_vote_threshold: u128

RegisterForum

#[event]
struct RegisterForum has drop, store
Fields
hosting_account: address
proposal_type_info: type_info::TypeInfo

Vote

#[event]
struct Vote has drop, store
Fields
proposal_id: u64
num_votes: u64

ResolveProposal

#[event]
struct ResolveProposal has drop, store
Fields
proposal_id: u64
yes_votes: u128
no_votes: u128
resolved_early: bool

CreateProposalEvent

struct CreateProposalEvent has drop, store
Fields
proposal_id: u64
early_resolution_vote_threshold: option::Option<u128>
execution_hash: vector<u8>
expiration_secs: u64
metadata: simple_map::SimpleMap<string::String, vector<u8>>
min_vote_threshold: u128

RegisterForumEvent

struct RegisterForumEvent has drop, store
Fields
hosting_account: address
proposal_type_info: type_info::TypeInfo

VoteEvent

struct VoteEvent has drop, store
Fields
proposal_id: u64
num_votes: u64

VotePermission

struct VotePermission has copy, drop, store
Fields
dummy_field: bool

Resources

VotingForum

struct VotingForum<ProposalType: store> has key
Fields
proposals: table::Table<u64, voting::Proposal<ProposalType>>
Use Table for execution optimization instead of Vector for gas cost since Vector is read entirely into memory during execution while only relevant Table entries are.
events: voting::VotingEvents
next_proposal_id: u64
Unique identifier for a proposal. This allows for 2 * 10**19 proposals.

Functions

check_vote_permission

Permissions

fun check_vote_permission(s: &signer)
Implementation 
inline fun check_vote_permission(s: &signer) {
    assert!(
        permissioned_signer::check_permission_exists(s, VotePermission {}),
        error::permission_denied(ENO_VOTE_PERMISSION),
    );
}

grant_permission

Grant permission to vote on behalf of the master signer.

public fun grant_permission(master: &signer, permissioned_signer: &signer)
Implementation 
public fun grant_permission(master: &signer, permissioned_signer: &signer) {
    permissioned_signer::authorize_unlimited(master, permissioned_signer, VotePermission {})
}

register

public fun register<ProposalType: store>(account: &signer)
Implementation 
public fun register<ProposalType: store>(account: &signer) {
    check_vote_permission(account);
    let addr = signer::address_of(account);
    assert!(!exists<VotingForum<ProposalType>>(addr), error::already_exists(EVOTING_FORUM_ALREADY_REGISTERED));


    let voting_forum = VotingForum<ProposalType> {
        next_proposal_id: 0,
        proposals: table::new<u64, Proposal<ProposalType>>(),
        events: VotingEvents {
            create_proposal_events: account::new_event_handle<CreateProposalEvent>(account),
            register_forum_events: account::new_event_handle<RegisterForumEvent>(account),
            resolve_proposal_events: account::new_event_handle<ResolveProposal>(account),
            vote_events: account::new_event_handle<VoteEvent>(account),
        }
    };


    if (std::features::module_event_migration_enabled()) {
        event::emit(
            RegisterForum {
                hosting_account: addr,
                proposal_type_info: type_info::type_of<ProposalType>(),
            },
        );
    } else {
        event::emit_event<RegisterForumEvent>(
            &mut voting_forum.events.register_forum_events,
            RegisterForumEvent {
                hosting_account: addr,
                proposal_type_info: type_info::type_of<ProposalType>(),
            },
        );
    };


    move_to(account, voting_forum);
}

create_proposal

Create a single-step proposal with the given parameters

@param voting_forum_address The forum’s address where the proposal will be stored. @param execution_content The execution content that will be given back at resolution time. This can contain data such as a capability resource used to scope the execution. @param execution_hash The hash for the execution script module. Only the same exact script module can resolve this proposal. @param min_vote_threshold The minimum number of votes needed to consider this proposal successful. @param expiration_secs The time in seconds at which the proposal expires and can potentially be resolved. @param early_resolution_vote_threshold The vote threshold for early resolution of this proposal. @param metadata A simple_map that stores information about this proposal. @return The proposal id.

public fun create_proposal<ProposalType: store>(proposer: address, voting_forum_address: address, execution_content: ProposalType, execution_hash: vector<u8>, min_vote_threshold: u128, expiration_secs: u64, early_resolution_vote_threshold: option::Option<u128>, metadata: simple_map::SimpleMap<string::String, vector<u8>>): u64
Implementation 
public fun create_proposal<ProposalType: store>(
    proposer: address,
    voting_forum_address: address,
    execution_content: ProposalType,
    execution_hash: vector<u8>,
    min_vote_threshold: u128,
    expiration_secs: u64,
    early_resolution_vote_threshold: Option<u128>,
    metadata: SimpleMap<String, vector<u8>>,
): u64 acquires VotingForum {
    create_proposal_v2(
        proposer,
        voting_forum_address,
        execution_content,
        execution_hash,
        min_vote_threshold,
        expiration_secs,
        early_resolution_vote_threshold,
        metadata,
        false
    )
}

create_proposal_v2

Create a single-step or a multi-step proposal with the given parameters

@param voting_forum_address The forum’s address where the proposal will be stored. @param execution_content The execution content that will be given back at resolution time. This can contain data such as a capability resource used to scope the execution. @param execution_hash The sha-256 hash for the execution script module. Only the same exact script module can resolve this proposal. @param min_vote_threshold The minimum number of votes needed to consider this proposal successful. @param expiration_secs The time in seconds at which the proposal expires and can potentially be resolved. @param early_resolution_vote_threshold The vote threshold for early resolution of this proposal. @param metadata A simple_map that stores information about this proposal. @param is_multi_step_proposal A bool value that indicates if the proposal is single-step or multi-step. @return The proposal id.

public fun create_proposal_v2<ProposalType: store>(proposer: address, voting_forum_address: address, execution_content: ProposalType, execution_hash: vector<u8>, min_vote_threshold: u128, expiration_secs: u64, early_resolution_vote_threshold: option::Option<u128>, metadata: simple_map::SimpleMap<string::String, vector<u8>>, is_multi_step_proposal: bool): u64
Implementation 
public fun create_proposal_v2<ProposalType: store>(
    proposer: address,
    voting_forum_address: address,
    execution_content: ProposalType,
    execution_hash: vector<u8>,
    min_vote_threshold: u128,
    expiration_secs: u64,
    early_resolution_vote_threshold: Option<u128>,
    metadata: SimpleMap<String, vector<u8>>,
    is_multi_step_proposal: bool,
): u64 acquires VotingForum {
    if (option::is_some(&early_resolution_vote_threshold)) {
        assert!(
            min_vote_threshold <= *option::borrow(&early_resolution_vote_threshold),
            error::invalid_argument(EINVALID_MIN_VOTE_THRESHOLD),
        );
    };
    // Make sure the execution script's hash is not empty.
    assert!(vector::length(&execution_hash) > 0, error::invalid_argument(EPROPOSAL_EMPTY_EXECUTION_HASH));


    let voting_forum = borrow_global_mut<VotingForum<ProposalType>>(voting_forum_address);
    let proposal_id = voting_forum.next_proposal_id;
    voting_forum.next_proposal_id = voting_forum.next_proposal_id + 1;


    // Add a flag to indicate if this proposal is single-step or multi-step.
    simple_map::add(&mut metadata, utf8(IS_MULTI_STEP_PROPOSAL_KEY), to_bytes(&is_multi_step_proposal));


    let is_multi_step_in_execution_key = utf8(IS_MULTI_STEP_PROPOSAL_IN_EXECUTION_KEY);
    if (is_multi_step_proposal) {
        // If the given proposal is a multi-step proposal, we will add a flag to indicate if this multi-step proposal is in execution.
        // This value is by default false. We turn this value to true when we start executing the multi-step proposal. This value
        // will be used to disable further voting after we started executing the multi-step proposal.
        simple_map::add(&mut metadata, is_multi_step_in_execution_key, to_bytes(&false));
        // If the proposal is a single-step proposal, we check if the metadata passed by the client has the IS_MULTI_STEP_PROPOSAL_IN_EXECUTION_KEY key.
        // If they have the key, we will remove it, because a single-step proposal that doesn't need this key.
    } else if (simple_map::contains_key(&metadata, &is_multi_step_in_execution_key)) {
        simple_map::remove(&mut metadata, &is_multi_step_in_execution_key);
    };


    table::add(&mut voting_forum.proposals, proposal_id, Proposal {
        proposer,
        creation_time_secs: timestamp::now_seconds(),
        execution_content: option::some<ProposalType>(execution_content),
        execution_hash,
        metadata,
        min_vote_threshold,
        expiration_secs,
        early_resolution_vote_threshold,
        yes_votes: 0,
        no_votes: 0,
        is_resolved: false,
        resolution_time_secs: 0,
    });


    if (std::features::module_event_migration_enabled()) {
        event::emit(
            CreateProposal {
                proposal_id,
                early_resolution_vote_threshold,
                execution_hash,
                expiration_secs,
                metadata,
                min_vote_threshold,
            },
        );
    } else {
        event::emit_event<CreateProposalEvent>(
            &mut voting_forum.events.create_proposal_events,
            CreateProposalEvent {
                proposal_id,
                early_resolution_vote_threshold,
                execution_hash,
                expiration_secs,
                metadata,
                min_vote_threshold,
            },
        );
    };
    proposal_id
}

vote

Vote on the given proposal.

@param _proof Required so only the governance module that defines ProposalType can initiate voting. This guarantees that voting eligibility and voting power are controlled by the right governance. @param voting_forum_address The address of the forum where the proposals are stored. @param proposal_id The proposal id. @param num_votes Number of votes. Voting power should be calculated by governance. @param should_pass Whether the votes are for yes or no.

public fun vote<ProposalType: store>(_proof: &ProposalType, voting_forum_address: address, proposal_id: u64, num_votes: u64, should_pass: bool)
Implementation 
public fun vote<ProposalType: store>(
    _proof: &ProposalType,
    voting_forum_address: address,
    proposal_id: u64,
    num_votes: u64,
    should_pass: bool,
) acquires VotingForum {
    let voting_forum = borrow_global_mut<VotingForum<ProposalType>>(voting_forum_address);
    let proposal = table::borrow_mut(&mut voting_forum.proposals, proposal_id);
    // Voting might still be possible after the proposal has enough yes votes to be resolved early. This would only
    // lead to possible proposal resolution failure if the resolve early threshold is not definitive (e.g. < 50% + 1
    // of the total voting token's supply). In this case, more voting might actually still be desirable.
    // Governance mechanisms built on this voting module can apply additional rules on when voting is closed as
    // appropriate.
    assert!(!is_voting_period_over(proposal), error::invalid_state(EPROPOSAL_VOTING_ALREADY_ENDED));
    assert!(!proposal.is_resolved, error::invalid_state(EPROPOSAL_ALREADY_RESOLVED));
    // Assert this proposal is single-step, or if the proposal is multi-step, it is not in execution yet.
    assert!(!simple_map::contains_key(&proposal.metadata, &utf8(IS_MULTI_STEP_PROPOSAL_IN_EXECUTION_KEY))
        || *simple_map::borrow(&proposal.metadata, &utf8(IS_MULTI_STEP_PROPOSAL_IN_EXECUTION_KEY)) == to_bytes(
        &false
    ),
        error::invalid_state(EMULTI_STEP_PROPOSAL_IN_EXECUTION));


    if (should_pass) {
        proposal.yes_votes = proposal.yes_votes + (num_votes as u128);
    } else {
        proposal.no_votes = proposal.no_votes + (num_votes as u128);
    };


    // Record the resolvable time to ensure that resolution has to be done non-atomically.
    let timestamp_secs_bytes = to_bytes(&timestamp::now_seconds());
    let key = utf8(RESOLVABLE_TIME_METADATA_KEY);
    if (simple_map::contains_key(&proposal.metadata, &key)) {
        *simple_map::borrow_mut(&mut proposal.metadata, &key) = timestamp_secs_bytes;
    } else {
        simple_map::add(&mut proposal.metadata, key, timestamp_secs_bytes);
    };


    if (std::features::module_event_migration_enabled()) {
        event::emit(Vote { proposal_id, num_votes });
    } else {
        event::emit_event<VoteEvent>(
            &mut voting_forum.events.vote_events,
            VoteEvent { proposal_id, num_votes },
        );
    };
}

is_proposal_resolvable

Common checks on if a proposal is resolvable, regardless if the proposal is single-step or multi-step.

fun is_proposal_resolvable<ProposalType: store>(voting_forum_address: address, proposal_id: u64)
Implementation 
fun is_proposal_resolvable<ProposalType: store>(
    voting_forum_address: address,
    proposal_id: u64,
) acquires VotingForum {
    let proposal_state = get_proposal_state<ProposalType>(voting_forum_address, proposal_id);
    assert!(proposal_state == PROPOSAL_STATE_SUCCEEDED, error::invalid_state(EPROPOSAL_CANNOT_BE_RESOLVED));


    let voting_forum = borrow_global_mut<VotingForum<ProposalType>>(voting_forum_address);
    let proposal = table::borrow_mut(&mut voting_forum.proposals, proposal_id);
    assert!(!proposal.is_resolved, error::invalid_state(EPROPOSAL_ALREADY_RESOLVED));


    // We need to make sure that the resolution is happening in
    // a separate transaction from the last vote to guard against any potential flashloan attacks.
    let resolvable_time = to_u64(*simple_map::borrow(&proposal.metadata, &utf8(RESOLVABLE_TIME_METADATA_KEY)));
    assert!(timestamp::now_seconds() > resolvable_time, error::invalid_state(ERESOLUTION_CANNOT_BE_ATOMIC));


    assert!(
        transaction_context::get_script_hash() == proposal.execution_hash,
        error::invalid_argument(EPROPOSAL_EXECUTION_HASH_NOT_MATCHING),
    );
}

resolve

Resolve a single-step proposal with given id. Can only be done if there are at least as many votes as min required and there are more yes votes than no. If either of these conditions is not met, this will revert.

@param voting_forum_address The address of the forum where the proposals are stored. @param proposal_id The proposal id.

public fun resolve<ProposalType: store>(voting_forum_address: address, proposal_id: u64): ProposalType
Implementation 
public fun resolve<ProposalType: store>(
    voting_forum_address: address,
    proposal_id: u64,
): ProposalType acquires VotingForum {
    is_proposal_resolvable<ProposalType>(voting_forum_address, proposal_id);


    let voting_forum = borrow_global_mut<VotingForum<ProposalType>>(voting_forum_address);
    let proposal = table::borrow_mut(&mut voting_forum.proposals, proposal_id);


    // Assert that the specified proposal is not a multi-step proposal.
    let multi_step_key = utf8(IS_MULTI_STEP_PROPOSAL_KEY);
    let has_multi_step_key = simple_map::contains_key(&proposal.metadata, &multi_step_key);
    if (has_multi_step_key) {
        let is_multi_step_proposal = from_bcs::to_bool(*simple_map::borrow(&proposal.metadata, &multi_step_key));
        assert!(
            !is_multi_step_proposal,
            error::permission_denied(EMULTI_STEP_PROPOSAL_CANNOT_USE_SINGLE_STEP_RESOLVE_FUNCTION)
        );
    };


    let resolved_early = can_be_resolved_early(proposal);
    proposal.is_resolved = true;
    proposal.resolution_time_secs = timestamp::now_seconds();


    if (std::features::module_event_migration_enabled()) {
        event::emit(
            ResolveProposal {
                proposal_id,
                yes_votes: proposal.yes_votes,
                no_votes: proposal.no_votes,
                resolved_early,
            },
        );
    } else {
        event::emit_event<ResolveProposal>(
            &mut voting_forum.events.resolve_proposal_events,
            ResolveProposal {
                proposal_id,
                yes_votes: proposal.yes_votes,
                no_votes: proposal.no_votes,
                resolved_early,
            },
        );
    };


    option::extract(&mut proposal.execution_content)
}

resolve_proposal_v2

Resolve a single-step or a multi-step proposal with the given id. Can only be done if there are at least as many votes as min required and there are more yes votes than no. If either of these conditions is not met, this will revert.

@param voting_forum_address The address of the forum where the proposals are stored. @param proposal_id The proposal id. @param next_execution_hash The next execution hash if the given proposal is multi-step.

public fun resolve_proposal_v2<ProposalType: store>(voting_forum_address: address, proposal_id: u64, next_execution_hash: vector<u8>)
Implementation 
public fun resolve_proposal_v2<ProposalType: store>(
    voting_forum_address: address,
    proposal_id: u64,
    next_execution_hash: vector<u8>,
) acquires VotingForum {
    is_proposal_resolvable<ProposalType>(voting_forum_address, proposal_id);


    let voting_forum = borrow_global_mut<VotingForum<ProposalType>>(voting_forum_address);
    let proposal = table::borrow_mut(&mut voting_forum.proposals, proposal_id);


    // Update the IS_MULTI_STEP_PROPOSAL_IN_EXECUTION_KEY key to indicate that the multi-step proposal is in execution.
    let multi_step_in_execution_key = utf8(IS_MULTI_STEP_PROPOSAL_IN_EXECUTION_KEY);
    if (simple_map::contains_key(&proposal.metadata, &multi_step_in_execution_key)) {
        let is_multi_step_proposal_in_execution_value = simple_map::borrow_mut(
            &mut proposal.metadata,
            &multi_step_in_execution_key
        );
        *is_multi_step_proposal_in_execution_value = to_bytes(&true);
    };


    let multi_step_key = utf8(IS_MULTI_STEP_PROPOSAL_KEY);
    let is_multi_step = simple_map::contains_key(&proposal.metadata, &multi_step_key) && from_bcs::to_bool(
        *simple_map::borrow(&proposal.metadata, &multi_step_key)
    );
    let next_execution_hash_is_empty = vector::length(&next_execution_hash) == 0;


    // Assert that if this proposal is single-step, the `next_execution_hash` parameter is empty.
    assert!(
        is_multi_step || next_execution_hash_is_empty,
        error::invalid_argument(ESINGLE_STEP_PROPOSAL_CANNOT_HAVE_NEXT_EXECUTION_HASH)
    );


    // If the `next_execution_hash` parameter is empty, it means that either
    // - this proposal is a single-step proposal, or
    // - this proposal is multi-step and we're currently resolving the last step in the multi-step proposal.
    // We can mark that this proposal is resolved.
    if (next_execution_hash_is_empty) {
        proposal.is_resolved = true;
        proposal.resolution_time_secs = timestamp::now_seconds();


        // Set the `IS_MULTI_STEP_PROPOSAL_IN_EXECUTION_KEY` value to false upon successful resolution of the last step of a multi-step proposal.
        if (is_multi_step) {
            let is_multi_step_proposal_in_execution_value = simple_map::borrow_mut(
                &mut proposal.metadata,
                &multi_step_in_execution_key
            );
            *is_multi_step_proposal_in_execution_value = to_bytes(&false);
        };
    } else {
        // If the current step is not the last step,
        // update the proposal's execution hash on-chain to the execution hash of the next step.
        proposal.execution_hash = next_execution_hash;
    };


    // For single-step proposals, we emit one `ResolveProposal` event per proposal.
    // For multi-step proposals, we emit one `ResolveProposal` event per step in the multi-step proposal. This means
    // that we emit multiple `ResolveProposal` events for the same multi-step proposal.
    let resolved_early = can_be_resolved_early(proposal);
    if (std::features::module_event_migration_enabled()) {
        event::emit(
            ResolveProposal {
                proposal_id,
                yes_votes: proposal.yes_votes,
                no_votes: proposal.no_votes,
                resolved_early,
            },
        );
    } else {
        event::emit_event(
            &mut voting_forum.events.resolve_proposal_events,
            ResolveProposal {
                proposal_id,
                yes_votes: proposal.yes_votes,
                no_votes: proposal.no_votes,
                resolved_early,
            },
        );
    };
}

next_proposal_id

Return the next unassigned proposal id

#[view]
public fun next_proposal_id<ProposalType: store>(voting_forum_address: address): u64
Implementation 
public fun next_proposal_id<ProposalType: store>(voting_forum_address: address, ): u64 acquires VotingForum {
    let voting_forum = borrow_global<VotingForum<ProposalType>>(voting_forum_address);
    voting_forum.next_proposal_id
}

get_proposer

#[view]
public fun get_proposer<ProposalType: store>(voting_forum_address: address, proposal_id: u64): address
Implementation 
public fun get_proposer<ProposalType: store>(
    voting_forum_address: address,
    proposal_id: u64
): address acquires VotingForum {
    let proposal = get_proposal<ProposalType>(voting_forum_address, proposal_id);
    proposal.proposer
}

is_voting_closed

#[view]
public fun is_voting_closed<ProposalType: store>(voting_forum_address: address, proposal_id: u64): bool
Implementation 
public fun is_voting_closed<ProposalType: store>(
    voting_forum_address: address,
    proposal_id: u64
): bool acquires VotingForum {
    let proposal = get_proposal<ProposalType>(voting_forum_address, proposal_id);
    can_be_resolved_early(proposal) || is_voting_period_over(proposal)
}

can_be_resolved_early

Return true if the proposal has reached early resolution threshold (if specified).

public fun can_be_resolved_early<ProposalType: store>(proposal: &voting::Proposal<ProposalType>): bool
Implementation 
public fun can_be_resolved_early<ProposalType: store>(proposal: &Proposal<ProposalType>): bool {
    if (option::is_some(&proposal.early_resolution_vote_threshold)) {
        let early_resolution_threshold = *option::borrow(&proposal.early_resolution_vote_threshold);
        if (proposal.yes_votes >= early_resolution_threshold || proposal.no_votes >= early_resolution_threshold) {
            return true
        };
    };
    false
}

get_proposal_metadata

#[view]
public fun get_proposal_metadata<ProposalType: store>(voting_forum_address: address, proposal_id: u64): simple_map::SimpleMap<string::String, vector<u8>>
Implementation 
public fun get_proposal_metadata<ProposalType: store>(
    voting_forum_address: address,
    proposal_id: u64,
): SimpleMap<String, vector<u8>> acquires VotingForum {
    let proposal = get_proposal<ProposalType>(voting_forum_address, proposal_id);
    proposal.metadata
}

get_proposal_metadata_value

#[view]
public fun get_proposal_metadata_value<ProposalType: store>(voting_forum_address: address, proposal_id: u64, metadata_key: string::String): vector<u8>
Implementation 
public fun get_proposal_metadata_value<ProposalType: store>(
    voting_forum_address: address,
    proposal_id: u64,
    metadata_key: String,
): vector<u8> acquires VotingForum {
    let proposal = get_proposal<ProposalType>(voting_forum_address, proposal_id);
    *simple_map::borrow(&proposal.metadata, &metadata_key)
}

get_proposal_state

Return the state of the proposal with given id.

@param voting_forum_address The address of the forum where the proposals are stored. @param proposal_id The proposal id. @return Proposal state as an enum value.

#[view]
public fun get_proposal_state<ProposalType: store>(voting_forum_address: address, proposal_id: u64): u64
Implementation 
public fun get_proposal_state<ProposalType: store>(
    voting_forum_address: address,
    proposal_id: u64,
): u64 acquires VotingForum {
    if (is_voting_closed<ProposalType>(voting_forum_address, proposal_id)) {
        let proposal = get_proposal<ProposalType>(voting_forum_address, proposal_id);
        let yes_votes = proposal.yes_votes;
        let no_votes = proposal.no_votes;


        if (yes_votes > no_votes && yes_votes + no_votes >= proposal.min_vote_threshold) {
            PROPOSAL_STATE_SUCCEEDED
        } else {
            PROPOSAL_STATE_FAILED
        }
    } else {
        PROPOSAL_STATE_PENDING
    }
}

get_proposal_creation_secs

Return the proposal’s creation time.

#[view]
public fun get_proposal_creation_secs<ProposalType: store>(voting_forum_address: address, proposal_id: u64): u64
Implementation 
public fun get_proposal_creation_secs<ProposalType: store>(
    voting_forum_address: address,
    proposal_id: u64,
): u64 acquires VotingForum {
    let proposal = get_proposal<ProposalType>(voting_forum_address, proposal_id);
    proposal.creation_time_secs
}

get_proposal_expiration_secs

Return the proposal’s expiration time.

#[view]
public fun get_proposal_expiration_secs<ProposalType: store>(voting_forum_address: address, proposal_id: u64): u64
Implementation 
public fun get_proposal_expiration_secs<ProposalType: store>(
    voting_forum_address: address,
    proposal_id: u64,
): u64 acquires VotingForum {
    let proposal = get_proposal<ProposalType>(voting_forum_address, proposal_id);
    proposal.expiration_secs
}

get_execution_hash

Return the proposal’s execution hash.

#[view]
public fun get_execution_hash<ProposalType: store>(voting_forum_address: address, proposal_id: u64): vector<u8>
Implementation 
public fun get_execution_hash<ProposalType: store>(
    voting_forum_address: address,
    proposal_id: u64,
): vector<u8> acquires VotingForum {
    let proposal = get_proposal<ProposalType>(voting_forum_address, proposal_id);
    proposal.execution_hash
}

get_min_vote_threshold

Return the proposal’s minimum vote threshold

#[view]
public fun get_min_vote_threshold<ProposalType: store>(voting_forum_address: address, proposal_id: u64): u128
Implementation 
public fun get_min_vote_threshold<ProposalType: store>(
    voting_forum_address: address,
    proposal_id: u64,
): u128 acquires VotingForum {
    let proposal = get_proposal<ProposalType>(voting_forum_address, proposal_id);
    proposal.min_vote_threshold
}

get_early_resolution_vote_threshold

Return the proposal’s early resolution minimum vote threshold (optionally set)

#[view]
public fun get_early_resolution_vote_threshold<ProposalType: store>(voting_forum_address: address, proposal_id: u64): option::Option<u128>
Implementation 
public fun get_early_resolution_vote_threshold<ProposalType: store>(
    voting_forum_address: address,
    proposal_id: u64,
): Option<u128> acquires VotingForum {
    let proposal = get_proposal<ProposalType>(voting_forum_address, proposal_id);
    proposal.early_resolution_vote_threshold
}

get_votes

Return the proposal’s current vote count (yes_votes, no_votes)

#[view]
public fun get_votes<ProposalType: store>(voting_forum_address: address, proposal_id: u64): (u128, u128)
Implementation 
public fun get_votes<ProposalType: store>(
    voting_forum_address: address,
    proposal_id: u64,
): (u128, u128) acquires VotingForum {
    let proposal = get_proposal<ProposalType>(voting_forum_address, proposal_id);
    (proposal.yes_votes, proposal.no_votes)
}

is_resolved

Return true if the governance proposal has already been resolved.

#[view]
public fun is_resolved<ProposalType: store>(voting_forum_address: address, proposal_id: u64): bool
Implementation 
public fun is_resolved<ProposalType: store>(
    voting_forum_address: address,
    proposal_id: u64,
): bool acquires VotingForum {
    let proposal = get_proposal<ProposalType>(voting_forum_address, proposal_id);
    proposal.is_resolved
}

get_resolution_time_secs

#[view]
public fun get_resolution_time_secs<ProposalType: store>(voting_forum_address: address, proposal_id: u64): u64
Implementation 
public fun get_resolution_time_secs<ProposalType: store>(
    voting_forum_address: address,
    proposal_id: u64,
): u64 acquires VotingForum {
    let proposal = get_proposal<ProposalType>(voting_forum_address, proposal_id);
    proposal.resolution_time_secs
}

is_multi_step_proposal_in_execution

Return true if the multi-step governance proposal is in execution.

#[view]
public fun is_multi_step_proposal_in_execution<ProposalType: store>(voting_forum_address: address, proposal_id: u64): bool
Implementation 
public fun is_multi_step_proposal_in_execution<ProposalType: store>(
    voting_forum_address: address,
    proposal_id: u64,
): bool acquires VotingForum {
    let voting_forum = borrow_global<VotingForum<ProposalType>>(voting_forum_address);
    let proposal = table::borrow(&voting_forum.proposals, proposal_id);
    let is_multi_step_in_execution_key = utf8(IS_MULTI_STEP_PROPOSAL_IN_EXECUTION_KEY);
    assert!(
        simple_map::contains_key(&proposal.metadata, &is_multi_step_in_execution_key),
        error::invalid_argument(EPROPOSAL_IS_SINGLE_STEP)
    );
    from_bcs::to_bool(*simple_map::borrow(&proposal.metadata, &is_multi_step_in_execution_key))
}

is_voting_period_over

Return true if the voting period of the given proposal has already ended.

fun is_voting_period_over<ProposalType: store>(proposal: &voting::Proposal<ProposalType>): bool
Implementation 
fun is_voting_period_over<ProposalType: store>(proposal: &Proposal<ProposalType>): bool {
    timestamp::now_seconds() > proposal.expiration_secs
}

get_proposal

fun get_proposal<ProposalType: store>(voting_forum_address: address, proposal_id: u64): &voting::Proposal<ProposalType>
Implementation 
inline fun get_proposal<ProposalType: store>(
    voting_forum_address: address,
    proposal_id: u64,
): &Proposal<ProposalType> acquires VotingForum {
    let voting_forum = borrow_global<VotingForum<ProposalType>>(voting_forum_address);
    table::borrow(&voting_forum.proposals, proposal_id)
}

Specification

High-level Requirements

No.RequirementCriticalityImplementationEnforcement
1 The proposal ID in a voting forum is unique and always increases monotonically with each new proposal created for that voting forum. High The create_proposal and create_proposal_v2 create a new proposal with a unique ID derived from the voting_forum's next_proposal_id incrementally. Formally verified via create_proposal.
2 While voting, it ensures that only the governance module that defines ProposalType may initiate voting and that the proposal under vote exists in the specified voting forum. Critical The vote function verifies the eligibility and validity of a proposal before allowing voting. It ensures that only the correct governance module initiates voting. The function checks if the proposal is currently eligible for voting by confirming it has not resolved and the voting period has not ended. Formally verified via vote.
3 After resolving a single-step proposal, the corresponding proposal is guaranteed to be marked as successfully resolved. High Upon invoking the resolve function on a proposal, it undergoes a series of checks to ensure its validity. These include verifying if the proposal exists, is a single-step proposal, and meets the criteria for resolution. If the checks pass, the proposal's is_resolved flag becomes true, indicating a successful resolution. Formally verified via resolve.
4 In the context of v2 proposal resolving, both single-step and multi-step proposals are accurately handled. It ensures that for single-step proposals, the next execution hash is empty and resolves the proposal, while for multi-step proposals, it guarantees that the next execution hash corresponds to the hash of the next step, maintaining the integrity of the proposal execution sequence. Medium The function resolve_proposal_v2 correctly handles both single-step and multi-step proposals. For single-step proposals, it ensures that the next_execution_hash parameter is empty and resolves the proposal. For multi-step proposals, it ensures that the next_execution_hash parameter contains the hash of the next step. Formally verified via resolve_proposal_v2.

Module-level Specification

pragma verify = true;
pragma aborts_if_is_partial;
schema AbortsIfPermissionedSigner {
    s: signer;
    let perm = VotePermission {};
    aborts_if !permissioned_signer::spec_check_permission_exists(s, perm);
}

register

public fun register<ProposalType: store>(account: &signer)
let addr = signer::address_of(account);
aborts_if exists<VotingForum<ProposalType>>(addr);
aborts_if !type_info::spec_is_struct<ProposalType>();
ensures exists<VotingForum<ProposalType>>(addr);

create_proposal

public fun create_proposal<ProposalType: store>(proposer: address, voting_forum_address: address, execution_content: ProposalType, execution_hash: vector<u8>, min_vote_threshold: u128, expiration_secs: u64, early_resolution_vote_threshold: option::Option<u128>, metadata: simple_map::SimpleMap<string::String, vector<u8>>): u64
requires chain_status::is_operating();
include CreateProposalAbortsIfAndEnsures<ProposalType>{is_multi_step_proposal: false};
// This enforces high-level requirement 1:
ensures result == old(global<VotingForum<ProposalType>>(voting_forum_address)).next_proposal_id;

create_proposal_v2

public fun create_proposal_v2<ProposalType: store>(proposer: address, voting_forum_address: address, execution_content: ProposalType, execution_hash: vector<u8>, min_vote_threshold: u128, expiration_secs: u64, early_resolution_vote_threshold: option::Option<u128>, metadata: simple_map::SimpleMap<string::String, vector<u8>>, is_multi_step_proposal: bool): u64
requires chain_status::is_operating();
include CreateProposalAbortsIfAndEnsures<ProposalType>;
ensures result == old(global<VotingForum<ProposalType>>(voting_forum_address)).next_proposal_id;
schema CreateProposalAbortsIfAndEnsures<ProposalType> {
    voting_forum_address: address;
    execution_hash: vector<u8>;
    min_vote_threshold: u128;
    early_resolution_vote_threshold: Option<u128>;
    metadata: SimpleMap<String, vector<u8>>;
    is_multi_step_proposal: bool;
    let voting_forum = global<VotingForum<ProposalType>>(voting_forum_address);
    let proposal_id = voting_forum.next_proposal_id;
    aborts_if !exists<VotingForum<ProposalType>>(voting_forum_address);
    aborts_if table::spec_contains(voting_forum.proposals,proposal_id);
    aborts_if len(early_resolution_vote_threshold.vec) != 0 && min_vote_threshold > early_resolution_vote_threshold.vec[0];
    aborts_if !std::string::spec_internal_check_utf8(IS_MULTI_STEP_PROPOSAL_KEY);
    aborts_if !std::string::spec_internal_check_utf8(IS_MULTI_STEP_PROPOSAL_IN_EXECUTION_KEY);
    aborts_if len(execution_hash) == 0;
    let execution_key = std::string::spec_utf8(IS_MULTI_STEP_PROPOSAL_KEY);
    aborts_if simple_map::spec_contains_key(metadata, execution_key);
    aborts_if voting_forum.next_proposal_id + 1 > MAX_U64;
    let is_multi_step_in_execution_key = std::string::spec_utf8(IS_MULTI_STEP_PROPOSAL_IN_EXECUTION_KEY);
    aborts_if is_multi_step_proposal && simple_map::spec_contains_key(metadata, is_multi_step_in_execution_key);
    let post post_voting_forum = global<VotingForum<ProposalType>>(voting_forum_address);
    let post post_metadata = table::spec_get(post_voting_forum.proposals, proposal_id).metadata;
    ensures post_voting_forum.next_proposal_id == voting_forum.next_proposal_id + 1;
    ensures table::spec_contains(post_voting_forum.proposals, proposal_id);
    ensures if (is_multi_step_proposal) {
        simple_map::spec_get(post_metadata, is_multi_step_in_execution_key) == std::bcs::serialize(false)
    } else {
        !simple_map::spec_contains_key(post_metadata, is_multi_step_in_execution_key)
    };
}

vote

public fun vote<ProposalType: store>(_proof: &ProposalType, voting_forum_address: address, proposal_id: u64, num_votes: u64, should_pass: bool)
requires chain_status::is_operating();
// This enforces high-level requirement 2:
aborts_if !exists<VotingForum<ProposalType>>(voting_forum_address);
let voting_forum = global<VotingForum<ProposalType>>(voting_forum_address);
let proposal = table::spec_get(voting_forum.proposals, proposal_id);
aborts_if !table::spec_contains(voting_forum.proposals, proposal_id);
aborts_if is_voting_period_over(proposal);
aborts_if proposal.is_resolved;
aborts_if !exists<timestamp::CurrentTimeMicroseconds>(@aptos_framework);
aborts_if !std::string::spec_internal_check_utf8(IS_MULTI_STEP_PROPOSAL_IN_EXECUTION_KEY);
let execution_key = std::string::spec_utf8(IS_MULTI_STEP_PROPOSAL_IN_EXECUTION_KEY);
aborts_if simple_map::spec_contains_key(proposal.metadata, execution_key) &&
          simple_map::spec_get(proposal.metadata, execution_key) != std::bcs::serialize(false);
aborts_if if (should_pass) { proposal.yes_votes + num_votes > MAX_U128 } else { proposal.no_votes + num_votes > MAX_U128 };
aborts_if !std::string::spec_internal_check_utf8(RESOLVABLE_TIME_METADATA_KEY);
let post post_voting_forum = global<VotingForum<ProposalType>>(voting_forum_address);
let post post_proposal = table::spec_get(post_voting_forum.proposals, proposal_id);
ensures if (should_pass) {
    post_proposal.yes_votes == proposal.yes_votes + num_votes
} else {
    post_proposal.no_votes == proposal.no_votes + num_votes
};
let timestamp_secs_bytes = std::bcs::serialize(timestamp::spec_now_seconds());
let key = std::string::spec_utf8(RESOLVABLE_TIME_METADATA_KEY);
ensures simple_map::spec_get(post_proposal.metadata, key) == timestamp_secs_bytes;

is_proposal_resolvable

fun is_proposal_resolvable<ProposalType: store>(voting_forum_address: address, proposal_id: u64)
requires chain_status::is_operating();
include IsProposalResolvableAbortsIf<ProposalType>;
schema IsProposalResolvableAbortsIf<ProposalType> {
    voting_forum_address: address;
    proposal_id: u64;
    include AbortsIfNotContainProposalID<ProposalType>;
    let voting_forum = global<VotingForum<ProposalType>>(voting_forum_address);
    let proposal = table::spec_get(voting_forum.proposals, proposal_id);
    let voting_closed = spec_is_voting_closed<ProposalType>(voting_forum_address, proposal_id);
    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));
    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;
}

resolve

public fun resolve<ProposalType: store>(voting_forum_address: address, proposal_id: u64): ProposalType
requires chain_status::is_operating();
include IsProposalResolvableAbortsIf<ProposalType>;
aborts_if !std::string::spec_internal_check_utf8(IS_MULTI_STEP_PROPOSAL_KEY);
let voting_forum = global<VotingForum<ProposalType>>(voting_forum_address);
let proposal = table::spec_get(voting_forum.proposals, proposal_id);
let multi_step_key = std::string::spec_utf8(IS_MULTI_STEP_PROPOSAL_KEY);
let has_multi_step_key = simple_map::spec_contains_key(proposal.metadata, multi_step_key);
aborts_if has_multi_step_key && !from_bcs::deserializable<bool>(simple_map::spec_get(proposal.metadata, multi_step_key));
aborts_if has_multi_step_key && from_bcs::deserialize<bool>(simple_map::spec_get(proposal.metadata, multi_step_key));
let post post_voting_forum = global<VotingForum<ProposalType>>(voting_forum_address);
let post post_proposal = table::spec_get(post_voting_forum.proposals, proposal_id);
aborts_if !exists<timestamp::CurrentTimeMicroseconds>(@aptos_framework);
// This enforces high-level requirement 3:
ensures post_proposal.is_resolved == true;
ensures post_proposal.resolution_time_secs == timestamp::spec_now_seconds();
aborts_if option::spec_is_none(proposal.execution_content);
ensures result == option::spec_borrow(proposal.execution_content);
ensures option::spec_is_none(post_proposal.execution_content);

resolve_proposal_v2

public fun resolve_proposal_v2<ProposalType: store>(voting_forum_address: address, proposal_id: u64, next_execution_hash: vector<u8>)
pragma verify_duration_estimate = 300;
requires chain_status::is_operating();
include IsProposalResolvableAbortsIf<ProposalType>;
let voting_forum = global<VotingForum<ProposalType>>(voting_forum_address);
let proposal = table::spec_get(voting_forum.proposals, proposal_id);
let post post_voting_forum = global<VotingForum<ProposalType>>(voting_forum_address);
let post post_proposal = table::spec_get(post_voting_forum.proposals, proposal_id);
let multi_step_in_execution_key = std::string::spec_utf8(IS_MULTI_STEP_PROPOSAL_IN_EXECUTION_KEY);
aborts_if !std::string::spec_internal_check_utf8(IS_MULTI_STEP_PROPOSAL_IN_EXECUTION_KEY);
aborts_if !std::string::spec_internal_check_utf8(IS_MULTI_STEP_PROPOSAL_KEY);
ensures (simple_map::spec_contains_key(proposal.metadata, multi_step_in_execution_key) && len(next_execution_hash) != 0) ==>
    simple_map::spec_get(post_proposal.metadata, multi_step_in_execution_key) == std::bcs::serialize(true);
ensures (simple_map::spec_contains_key(proposal.metadata, multi_step_in_execution_key) &&
    (len(next_execution_hash) == 0 && !is_multi_step)) ==>
    simple_map::spec_get(post_proposal.metadata, multi_step_in_execution_key) == std::bcs::serialize(true);
let multi_step_key = std::string::spec_utf8(IS_MULTI_STEP_PROPOSAL_KEY);
aborts_if simple_map::spec_contains_key(proposal.metadata, multi_step_key) &&
    !from_bcs::deserializable<bool>(simple_map::spec_get(proposal.metadata, multi_step_key));
let is_multi_step = simple_map::spec_contains_key(proposal.metadata, multi_step_key) &&
    from_bcs::deserialize(simple_map::spec_get(proposal.metadata, multi_step_key));
aborts_if !is_multi_step && len(next_execution_hash) != 0;
aborts_if len(next_execution_hash) == 0 && !exists<timestamp::CurrentTimeMicroseconds>(@aptos_framework);
aborts_if len(next_execution_hash) == 0 && is_multi_step && !simple_map::spec_contains_key(proposal.metadata, multi_step_in_execution_key);
// This enforces high-level requirement 4:
ensures len(next_execution_hash) == 0 ==> post_proposal.resolution_time_secs == timestamp::spec_now_seconds();
ensures len(next_execution_hash) == 0 ==> post_proposal.is_resolved == true;
ensures (len(next_execution_hash) == 0 && is_multi_step) ==> simple_map::spec_get(post_proposal.metadata, multi_step_in_execution_key) == std::bcs::serialize(false);
ensures len(next_execution_hash) != 0 ==> post_proposal.execution_hash == next_execution_hash;

next_proposal_id

#[view]
public fun next_proposal_id<ProposalType: store>(voting_forum_address: address): u64
aborts_if !exists<VotingForum<ProposalType>>(voting_forum_address);
ensures result == global<VotingForum<ProposalType>>(voting_forum_address).next_proposal_id;

get_proposer

#[view]
public fun get_proposer<ProposalType: store>(voting_forum_address: address, proposal_id: u64): address
include AbortsIfNotContainProposalID<ProposalType>;
let voting_forum = global<VotingForum<ProposalType>>(voting_forum_address);
let proposal = table::spec_get(voting_forum.proposals, proposal_id);
ensures result == proposal.proposer;

is_voting_closed

#[view]
public fun is_voting_closed<ProposalType: store>(voting_forum_address: address, proposal_id: u64): bool
requires chain_status::is_operating();
include AbortsIfNotContainProposalID<ProposalType>;
aborts_if !exists<timestamp::CurrentTimeMicroseconds>(@aptos_framework);
ensures result == spec_is_voting_closed<ProposalType>(voting_forum_address, proposal_id);
fun spec_is_voting_closed<ProposalType: store>(voting_forum_address: address, proposal_id: u64): bool {
   let voting_forum = global<VotingForum<ProposalType>>(voting_forum_address);
   let proposal = table::spec_get(voting_forum.proposals, proposal_id);
   spec_can_be_resolved_early<ProposalType>(proposal) || is_voting_period_over(proposal)
}

can_be_resolved_early

public fun can_be_resolved_early<ProposalType: store>(proposal: &voting::Proposal<ProposalType>): bool
aborts_if false;
ensures result == spec_can_be_resolved_early<ProposalType>(proposal);
fun spec_can_be_resolved_early<ProposalType: store>(proposal: Proposal<ProposalType>): bool {
   if (option::spec_is_some(proposal.early_resolution_vote_threshold)) {
       let early_resolution_threshold = option::spec_borrow(proposal.early_resolution_vote_threshold);
       if (proposal.yes_votes >= early_resolution_threshold || proposal.no_votes >= early_resolution_threshold) {
           true
       } else{
           false
       }
   } else {
       false
   }
}
fun spec_get_proposal_state<ProposalType>(
   voting_forum_address: address,
   proposal_id: u64,
   voting_forum: VotingForum<ProposalType>
): u64 {
   let proposal = table::spec_get(voting_forum.proposals, proposal_id);
   let voting_closed = spec_is_voting_closed<ProposalType>(voting_forum_address, proposal_id);
   let proposal_vote_cond = (proposal.yes_votes > proposal.no_votes && proposal.yes_votes + proposal.no_votes >= proposal.min_vote_threshold);
   if (voting_closed && proposal_vote_cond) {
       PROPOSAL_STATE_SUCCEEDED
   } else if (voting_closed && !proposal_vote_cond) {
       PROPOSAL_STATE_FAILED
   } else {
       PROPOSAL_STATE_PENDING
   }
}
fun spec_get_proposal_expiration_secs<ProposalType: store>(
   voting_forum_address: address,
   proposal_id: u64,
): u64 {
   let voting_forum = global<VotingForum<ProposalType>>(voting_forum_address);
   let proposal = table::spec_get(voting_forum.proposals, proposal_id);
   proposal.expiration_secs
}

get_proposal_metadata

#[view]
public fun get_proposal_metadata<ProposalType: store>(voting_forum_address: address, proposal_id: u64): simple_map::SimpleMap<string::String, vector<u8>>
include AbortsIfNotContainProposalID<ProposalType>;
let voting_forum = global<VotingForum<ProposalType>>(voting_forum_address);
let proposal = table::spec_get(voting_forum.proposals, proposal_id);
ensures result == proposal.metadata;

get_proposal_metadata_value

#[view]
public fun get_proposal_metadata_value<ProposalType: store>(voting_forum_address: address, proposal_id: u64, metadata_key: string::String): vector<u8>
include AbortsIfNotContainProposalID<ProposalType>;
let voting_forum = global<VotingForum<ProposalType>>(voting_forum_address);
let proposal = table::spec_get(voting_forum.proposals, proposal_id);
aborts_if !simple_map::spec_contains_key(proposal.metadata, metadata_key);
ensures result == simple_map::spec_get(proposal.metadata, metadata_key);

get_proposal_state

#[view]
public fun get_proposal_state<ProposalType: store>(voting_forum_address: address, proposal_id: u64): u64
pragma addition_overflow_unchecked;
requires chain_status::is_operating();
include AbortsIfNotContainProposalID<ProposalType>;
let voting_forum = global<VotingForum<ProposalType>>(voting_forum_address);
ensures result == spec_get_proposal_state(voting_forum_address, proposal_id, voting_forum);

get_proposal_creation_secs

#[view]
public fun get_proposal_creation_secs<ProposalType: store>(voting_forum_address: address, proposal_id: u64): u64
include AbortsIfNotContainProposalID<ProposalType>;
let voting_forum = global<VotingForum<ProposalType>>(voting_forum_address);
let proposal = table::spec_get(voting_forum.proposals, proposal_id);
ensures result == proposal.creation_time_secs;

get_proposal_expiration_secs

#[view]
public fun get_proposal_expiration_secs<ProposalType: store>(voting_forum_address: address, proposal_id: u64): u64
include AbortsIfNotContainProposalID<ProposalType>;
ensures result == spec_get_proposal_expiration_secs<ProposalType>(voting_forum_address, proposal_id);

get_execution_hash

#[view]
public fun get_execution_hash<ProposalType: store>(voting_forum_address: address, proposal_id: u64): vector<u8>
include AbortsIfNotContainProposalID<ProposalType>;
let voting_forum = global<VotingForum<ProposalType>>(voting_forum_address);
let proposal = table::spec_get(voting_forum.proposals, proposal_id);
ensures result == proposal.execution_hash;

get_min_vote_threshold

#[view]
public fun get_min_vote_threshold<ProposalType: store>(voting_forum_address: address, proposal_id: u64): u128
include AbortsIfNotContainProposalID<ProposalType>;
let voting_forum = global<VotingForum<ProposalType>>(voting_forum_address);
let proposal = table::spec_get(voting_forum.proposals, proposal_id);
ensures result == proposal.min_vote_threshold;

get_early_resolution_vote_threshold

#[view]
public fun get_early_resolution_vote_threshold<ProposalType: store>(voting_forum_address: address, proposal_id: u64): option::Option<u128>
include AbortsIfNotContainProposalID<ProposalType>;
let voting_forum = global<VotingForum<ProposalType>>(voting_forum_address);
let proposal = table::spec_get(voting_forum.proposals, proposal_id);
ensures result == proposal.early_resolution_vote_threshold;

get_votes

#[view]
public fun get_votes<ProposalType: store>(voting_forum_address: address, proposal_id: u64): (u128, u128)
include AbortsIfNotContainProposalID<ProposalType>;
let voting_forum = global<VotingForum<ProposalType>>(voting_forum_address);
let proposal = table::spec_get(voting_forum.proposals, proposal_id);
ensures result_1 == proposal.yes_votes;
ensures result_2 == proposal.no_votes;

is_resolved

#[view]
public fun is_resolved<ProposalType: store>(voting_forum_address: address, proposal_id: u64): bool
include AbortsIfNotContainProposalID<ProposalType>;
let voting_forum = global<VotingForum<ProposalType>>(voting_forum_address);
let proposal = table::spec_get(voting_forum.proposals, proposal_id);
ensures result == proposal.is_resolved;
schema AbortsIfNotContainProposalID<ProposalType> {
    proposal_id: u64;
    voting_forum_address: address;
    let voting_forum = global<VotingForum<ProposalType>>(voting_forum_address);
    aborts_if !table::spec_contains(voting_forum.proposals, proposal_id);
    aborts_if !exists<VotingForum<ProposalType>>(voting_forum_address);
}

get_resolution_time_secs

#[view]
public fun get_resolution_time_secs<ProposalType: store>(voting_forum_address: address, proposal_id: u64): u64
include AbortsIfNotContainProposalID<ProposalType>;
let voting_forum = global<VotingForum<ProposalType>>(voting_forum_address);
let proposal = table::spec_get(voting_forum.proposals, proposal_id);
ensures result == proposal.resolution_time_secs;

is_multi_step_proposal_in_execution

#[view]
public fun is_multi_step_proposal_in_execution<ProposalType: store>(voting_forum_address: address, proposal_id: u64): bool
include AbortsIfNotContainProposalID<ProposalType>;
let voting_forum = global<VotingForum<ProposalType>>(voting_forum_address);
let proposal = table::spec_get(voting_forum.proposals,proposal_id);
aborts_if !std::string::spec_internal_check_utf8(IS_MULTI_STEP_PROPOSAL_IN_EXECUTION_KEY);
let execution_key = std::string::spec_utf8(IS_MULTI_STEP_PROPOSAL_IN_EXECUTION_KEY);
aborts_if !simple_map::spec_contains_key(proposal.metadata,execution_key);
let is_multi_step_in_execution_key = simple_map::spec_get(proposal.metadata,execution_key);
aborts_if !from_bcs::deserializable<bool>(is_multi_step_in_execution_key);
ensures result == from_bcs::deserialize<bool>(is_multi_step_in_execution_key);

is_voting_period_over

fun is_voting_period_over<ProposalType: store>(proposal: &voting::Proposal<ProposalType>): bool
requires chain_status::is_operating();
aborts_if false;
ensures result == (timestamp::spec_now_seconds() > proposal.expiration_secs);