From d96bc34f841841d0299b0893e41c1b4fa9ad9cb4 Mon Sep 17 00:00:00 2001 From: r4bbit <445106+0x-r4bbit@users.noreply.github.com> Date: Thu, 3 Oct 2024 00:24:12 -0300 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 Also this commit adds an invariant: add invariant that account balance == 0 => accountMP == 0 --- certora/specs/StakeManager.spec | 1 + certora/specs/StakeManagerProcessAccount.spec | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/certora/specs/StakeManager.spec b/certora/specs/StakeManager.spec index f964f85..227bb0f 100644 --- a/certora/specs/StakeManager.spec +++ b/certora/specs/StakeManager.spec @@ -115,6 +115,7 @@ rule stakingMintsMultiplierPoints1To1Ratio { requireInvariant InitialMPIsNeverSmallerThanBalance(e.msg.sender); requireInvariant CurrentMPIsNeverSmallerThanInitialMP(e.msg.sender); + requireInvariant accountMPIsZeroIfBalanceIsZero(e.msg.sender); require getAccountLockUntil(e.msg.sender) <= e.block.timestamp; 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;