logos-co
/
staking
mirror of https://github.com/logos-co/staking.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

chore: add cerora rules for `totalSupplyBalance` ghost rule

This commit is contained in:
Nurit Dor 2024-01-24 12:16:01 +01:00 committed by Ricardo Guilherme Schmidt
parent 5cdd54a884
commit e1bd0f31f8
1 changed files with 4 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
certora/specs/StakeManager.spec
View File

@ -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;