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

fix(StakeManager.spec): change `simplification()` to assume no prev manager 

`simplification()` is used to have some rules make certain assumptions
so that they can pass. We need an additional simplification, stating
that `oldManager == address(0)`.

This means `oldManager` isn't set, meaning no `migrationInitialize()`
and similar functions have a non-reverting path.
This commit is contained in:
r4bbit 2024-03-04 16:21:41 +01:00 committed by Ricardo Guilherme Schmidt
parent e9f0077488
commit 0708bdd846
1 changed files with 16 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
certora/specs/StakeManager.spec
View File

@ -33,8 +33,10 @@ function isMigrationfunction(method f) returns bool {
/* assume that migration is zero, causing the verification to take into account only
cases where it is zero. specifically no externall call to the migration contract */
function simplification() {
function simplification(env e) {
require currentContract.migration == 0;
require currentContract.oldManager() == 0;
require e.msg.sender != 0;
}
ghost mathint sumOfEpochRewards
@ -63,13 +65,17 @@ hook Sstore accounts[KEY address addr].currentMP uint256 newValue (uint256 oldVa
sumOfMultipliers = sumOfMultipliers - oldValue + newValue;
}
invariant sumOfBalancesIsStakeSupply()
sumOfBalances == to_mathint(totalSupplyBalance());
invariant sumOfBalancesIsTotalSupplyBalance()
sumOfBalances == to_mathint(totalSupplyBalance())
{ preserved with (env e) {
simplification(e);
}
}
invariant sumOfMultipliersIsMultiplierSupply()
sumOfMultipliers == to_mathint(totalSupplyMP())
{ preserved with () {
simplification();
{ preserved with (env e) {
simplification(e);
}
}
@ -81,7 +87,11 @@ invariant sumOfEpochRewardsIsPendingRewards()
}
invariant highEpochsAreNull(uint256 epochNumber)
epochNumber >= currentContract.currentEpoch => currentContract.epochs[epochNumber].epochReward == 0;
epochNumber >= currentContract.currentEpoch => currentContract.epochs[epochNumber].epochReward == 0
{ preserved with (env e) {
simplification(e);
}
}
rule reachability(method f)
{