From 28881ec535c65d659b756f8d6b641ebcebb3109e Mon Sep 17 00:00:00 2001
From: r4bbit <445106+0x-r4bbit@users.noreply.github.com>
Date: Fri, 27 Sep 2024 16:37:44 +0200
Subject: [PATCH] fix(certora): exclude `stake()` from rule that checks account
 balance change

The rule is failing since we've removed the `lockUntil > 0` check in
`stake` and `processAccount` is no longer used in `stake()`.
The rule requires `lockUntil > 0` so it will always fail there and can't
find a non-reverting cases (which makes the rule pass).

The reason it hasn't happened before was because:

The rule required account.lockUntil > 0
Stake required lockUntil > 0 || account balance == 0
---
 certora/specs/StakeManagerProcessAccount.spec | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/certora/specs/StakeManagerProcessAccount.spec b/certora/specs/StakeManagerProcessAccount.spec
index e964acb..d7d062c 100644
--- a/certora/specs/StakeManagerProcessAccount.spec
+++ b/certora/specs/StakeManagerProcessAccount.spec
@@ -36,7 +36,7 @@ hook Sstore accounts[KEY address addr].balance uint256 newValue (uint256 oldValu
   https://prover.certora.com/output/40726/055d52bc67154e3fbea330fd7d68d36d/?anonymousKey=73030555b4cefe429d4eed6718b9a7e5be3a22c8
 */
 rule checkAccountProcessedBeforeStoring(method f) filtered {
-  f -> !requiresPreviousManager(f) && !requiresNextManager(f)
+  f -> !requiresPreviousManager(f) && !requiresNextManager(f) && f.selector != sig:stake(uint256,uint256).selector
 } {
   address account;