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
parent 44e1eec7b5
commit c5d44380e7
No known key found for this signature in database
GPG Key ID: E95F1E9447DC91A9
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 /* 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 */ 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.migration == 0;
require currentContract.oldManager() == 0;
require e.msg.sender != 0;
} }
ghost mathint sumOfEpochRewards ghost mathint sumOfEpochRewards
@ -63,13 +65,17 @@ hook Sstore accounts[KEY address addr].currentMP uint256 newValue (uint256 oldVa
sumOfMultipliers = sumOfMultipliers - oldValue + newValue; sumOfMultipliers = sumOfMultipliers - oldValue + newValue;
} }
invariant sumOfBalancesIsStakeSupply() invariant sumOfBalancesIsTotalSupplyBalance()
sumOfBalances == to_mathint(totalSupplyBalance()); sumOfBalances == to_mathint(totalSupplyBalance())
{ preserved with (env e) {
simplification(e);
}
}
invariant sumOfMultipliersIsMultiplierSupply() invariant sumOfMultipliersIsMultiplierSupply()
sumOfMultipliers == to_mathint(totalSupplyMP()) sumOfMultipliers == to_mathint(totalSupplyMP())
{ preserved with () { { preserved with (env e) {
simplification(); simplification(e);
} }
} }
@ -81,7 +87,11 @@ invariant sumOfEpochRewardsIsPendingRewards()
} }
invariant highEpochsAreNull(uint256 epochNumber) 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) rule reachability(method f)
{ {