verifier fixes

aptos-labs · May 29, 2024 · c6b9ae5 · c6b9ae5
1 parent 04873c5
commit c6b9ae5
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 1 deletion.
diff --git a/aptos-move/framework/aptos-framework/doc/stake.md b/aptos-move/framework/aptos-framework/doc/stake.md
@@ -4911,7 +4911,8 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
 
-<pre><code><b>include</b> <a href="stake.md#0x1_stake_ResourceRequirement">ResourceRequirement</a>;
+<pre><code><b>pragma</b> verify_duration_estimate = 120;
+<b>include</b> <a href="stake.md#0x1_stake_ResourceRequirement">ResourceRequirement</a>;
 <b>let</b> addr = <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(owner);
 <b>ensures</b> <b>global</b>&lt;<a href="stake.md#0x1_stake_ValidatorConfig">ValidatorConfig</a>&gt;(addr) == <a href="stake.md#0x1_stake_ValidatorConfig">ValidatorConfig</a> {
     consensus_pubkey: <a href="../../aptos-stdlib/../move-stdlib/doc/vector.md#0x1_vector_empty">vector::empty</a>(),

diff --git a/aptos-move/framework/aptos-framework/sources/stake.spec.move b/aptos-move/framework/aptos-framework/sources/stake.spec.move
@@ -705,6 +705,9 @@ spec aptos_framework::stake {
         operator: address,
         voter: address,
     ) {
+        // TODO: These function failed in github CI
+        pragma verify_duration_estimate = 120;
+
         include ResourceRequirement;
         let addr = signer::address_of(owner);
         ensures global<ValidatorConfig>(addr) == ValidatorConfig {