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): use filtered invariants for vacuous rules 

This refactors the spec to no longer rely on the `simplification()`
but instead filter out the vacuous rules from the get go.

Using the `simplification()` previously was needed so that the prover
will ignore cases that revert by design. This made some invariants
vacuous.

Having vacuous rules or invariants is still considered a failure, so to
make get prover happy, we're using filtered invariants instead which
renders the `simplification` obsolete.
This commit is contained in:
r4bbit 2024-03-05 09:52:40 +01:00 committed by Ricardo Guilherme Schmidt
parent da007451a4
commit 544cc42f34
1 changed files with 21 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

34
certora/specs/StakeManager.spec
View File

@ -39,6 +39,17 @@ function simplification(env e) {
require e.msg.sender != 0;
}
definition requiresPreviousManager(method f) returns bool = (
f.selector == sig:migrationInitialize(uint256,uint256,uint256,uint256).selector ||
f.selector == sig:migrateFrom(address,bool,StakeManager.Account).selector ||
f.selector == sig:increaseMPFromMigration(uint256).selector
);
definition requiresNextManager(method f) returns bool = (
f.selector == sig:migrateTo(bool).selector ||
f.selector == sig:transferNonPending().selector
);
ghost mathint sumOfEpochRewards
{
init_state axiom sumOfEpochRewards == 0;
@ -66,18 +77,16 @@ hook Sstore accounts[KEY address addr].currentMP uint256 newValue (uint256 oldVa
}
invariant sumOfBalancesIsTotalSupplyBalance()
sumOfBalances == to_mathint(totalSupplyBalance())
{ preserved with (env e) {
simplification(e);
}
}
sumOfBalances == to_mathint(totalSupplyBalance())
filtered {
m -> !requiresPreviousManager(m) && !requiresNextManager(m)
}
invariant sumOfMultipliersIsMultiplierSupply()
sumOfMultipliers == to_mathint(totalSupplyMP())
{ preserved with (env e) {
simplification(e);
}
}
sumOfMultipliers == to_mathint(totalSupplyMP())
filtered {
m -> !requiresPreviousManager(m) && !requiresNextManager(m)
}
invariant sumOfEpochRewardsIsPendingRewards()
sumOfEpochRewards == to_mathint(currentContract.pendingReward)
@ -88,9 +97,8 @@ invariant sumOfEpochRewardsIsPendingRewards()
invariant highEpochsAreNull(uint256 epochNumber)
epochNumber >= currentContract.currentEpoch => currentContract.epochs[epochNumber].epochReward == 0
{ preserved with (env e) {
simplification(e);
}
filtered {
m -> !requiresPreviousManager(m) && !requiresNextManager(m)
}
rule reachability(method f)