diff --git a/certora/specs/StakeManager.spec b/certora/specs/StakeManager.spec index 819b13b..c1ab2b3 100644 --- a/certora/specs/StakeManager.spec +++ b/certora/specs/StakeManager.spec @@ -42,15 +42,15 @@ ghost mathint sumOfEpochRewards init_state axiom sumOfEpochRewards == 0; } -ghost mathint sumOfBalances { /* sigma account[u].balance forall u */ - init_state axiom sumOfBalances == 0; -} - ghost mathint sumOfMultipliers /* sigma account[u].multiplier forall u */ { init_state axiom sumOfMultipliers == 0; } +ghost mathint sumOfBalances /* sigma account[u].balance forall u */ { + init_state axiom sumOfBalances == 0; +} + hook Sstore epochs[KEY uint256 epochId].epochReward uint256 newValue (uint256 oldValue) STORAGE { sumOfEpochRewards = sumOfEpochRewards - oldValue + newValue; } @@ -83,7 +83,6 @@ invariant sumOfEpochRewardsIsPendingRewards() invariant highEpochsAreNull(uint256 epochNumber) epochNumber >= currentContract.currentEpoch => currentContract.epochs[epochNumber].epochReward == 0; - rule reachability(method f) { calldataarg args;