[Spec] Ensures for staking_contract (#9701)

* hp6-8 cannot be verfied * hp6-8 cannot be verified * hp6-8 cannot be verified * init * fix comment * 1 * fix comment * fix timeout * fix timeout --------- Co-authored-by: chan-bing <[email protected]> Co-authored-by: chan-bing <[email protected]>
aptos-labs · Oct 19, 2023 · 7805954 · 7805954
1 parent 16bdb31
commit 7805954
Show file tree

Hide file tree

Showing 5 changed files with 206 additions and 293 deletions.
diff --git a/aptos-move/framework/aptos-framework/doc/aptos_governance.md b/aptos-move/framework/aptos-framework/doc/aptos_governance.md
@@ -2366,6 +2366,7 @@ Address @aptos_framework must exist ApprovedExecutionHashes and GovernancePropos
 
 
 <pre><code><b>requires</b> <a href="chain_status.md#0x1_chain_status_is_operating">chain_status::is_operating</a>();
+<b>pragma</b> verify_duration_estimate = 120;
 <b>include</b> <a href="aptos_governance.md#0x1_aptos_governance_VotingIsProposalResolvableAbortsif">VotingIsProposalResolvableAbortsif</a>;
 <b>let</b> voting_forum = <b>global</b>&lt;<a href="voting.md#0x1_voting_VotingForum">voting::VotingForum</a>&lt;GovernanceProposal&gt;&gt;(@aptos_framework);
 <b>let</b> proposal = <a href="../../aptos-stdlib/doc/table.md#0x1_table_spec_get">table::spec_get</a>(voting_forum.proposals, proposal_id);