diff --git a/certora/specs/StakeManager.spec b/certora/specs/StakeManager.spec index 8b49a56..8832a34 100644 --- a/certora/specs/StakeManager.spec +++ b/certora/specs/StakeManager.spec @@ -85,6 +85,12 @@ invariant highEpochsAreNull(uint256 epochNumber) m -> !requiresPreviousManager(m) && !requiresNextManager(m) } +invariant accountMPIsZeroIfBalanceIsZero(address addr) + to_mathint(getAccountBalance(addr)) == 0 => to_mathint(getAccountCurrentMultiplierPoints(addr)) == 0 + filtered { + f -> f.selector != sig:migrateFrom(address,bool,StakeManager.Account).selector + } + invariant InitialMPIsNeverSmallerThanBalance(address addr) to_mathint(getAccountBonusMultiplierPoints(addr)) >= to_mathint(getAccountBalance(addr)) filtered { @@ -126,6 +132,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;