staking/certora/specs/shared.spec
r4bbit 40c5be49bc refactor(certora): introduce shared.spec to reuse helper functions
We have a couple of helper functions redefined in multiple spec files.
This commit introduces a `shared.spec` that provides such functions.

The file is then imported in other spec files, so we can make use of the
functions there.

Closes #87
2024-09-19 14:35:08 +02:00

43 lines
1.2 KiB
Python

using StakeManager as _stakeManager;
definition requiresPreviousManager(method f) returns bool = (
f.selector == sig:_stakeManager.migrationInitialize(uint256,uint256,uint256,uint256,uint256,uint256,uint256).selector ||
f.selector == sig:_stakeManager.migrateFrom(address,bool,StakeManager.Account).selector ||
f.selector == sig:_stakeManager.increaseTotalMP(uint256).selector
);
definition requiresNextManager(method f) returns bool = (
f.selector == sig:_stakeManager.migrateTo(bool).selector ||
f.selector == sig:_stakeManager.transferNonPending().selector
);
function getAccountBalance(address addr) returns uint256 {
uint256 balance;
_, balance, _, _, _, _, _, _ = _stakeManager.accounts(addr);
return balance;
}
function getAccountBonusMultiplierPoints(address addr) returns uint256 {
uint256 bonusMP;
_, _, bonusMP, _, _, _, _, _ = _stakeManager.accounts(addr);
return bonusMP;
}
function getAccountCurrentMultiplierPoints(address addr) returns uint256 {
uint256 totalMP;
_, _, _, totalMP, _, _, _, _ = _stakeManager.accounts(addr);
return totalMP;
}
function getAccountLockUntil(address addr) returns uint256 {
uint256 lockUntil;
_, _, _, _, _, lockUntil, _, _ = _stakeManager.accounts(addr);
return lockUntil;
}