diff --git a/certora/specs/StakeManager.spec b/certora/specs/StakeManager.spec index 4d05215..00d765f 100644 --- a/certora/specs/StakeManager.spec +++ b/certora/specs/StakeManager.spec @@ -75,6 +75,11 @@ invariant sumOfMultipliersIsMultiplierSupply() filtered { m -> !requiresPreviousManager(m) && !requiresNextManager(m) } + { preserved with (env e){ + requireInvariant accountMPIsZeroIfBalanceIsZero(e.msg.sender); + requireInvariant accountBonusMPIsZeroIfBalanceIsZero(e.msg.sender); + } + } invariant sumOfEpochRewardsIsPendingRewards() sumOfEpochRewards == to_mathint(currentContract.pendingReward) @@ -89,6 +94,12 @@ invariant highEpochsAreNull(uint256 epochNumber) m -> !requiresPreviousManager(m) && !requiresNextManager(m) } +invariant accountBonusMPIsZeroIfBalanceIsZero(address addr) + to_mathint(getAccountBalance(addr)) == 0 => to_mathint(getAccountBonusMultiplierPoints(addr)) == 0 + filtered { + f -> f.selector != sig:migrateFrom(address,bool,StakeManager.Account).selector + } + invariant accountMPIsZeroIfBalanceIsZero(address addr) to_mathint(getAccountBalance(addr)) == 0 => to_mathint(getAccountCurrentMultiplierPoints(addr)) == 0 filtered {