logos-co/staking
1
0
Fork 0
mirror of https://github.com/logos-co/staking.git synced 2025-02-03 06:13:43 +00:00
Code Issues Packages Projects Releases Wiki Activity

chore(StakeManager.spec): add invariant greater lock time -> more MPs

Browse Source
This commit is contained in:
r4bbit 2024-03-12 14:13:52 +01:00
parent f1c1de7993
commit 7e2f675115
1 changed files with 21 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
certora/specs/StakeManager.spec
View File

@ -144,6 +144,27 @@ rule reachability(method f)
satisfy true; satisfy true;
} }
rule stakingGreaterLockupTimeMeansGreaterMPs {
env e;
uint256 amount;
uint256 lockupTime1;
uint256 lockupTime2;
uint256 multiplierPointsAfter1;
uint256 multiplierPointsAfter2;
storage initalStorage = lastStorage;
stake(e, amount, lockupTime1);
multiplierPointsAfter1 = getAccountInitialMultiplierPoints(e.msg.sender);
stake(e, amount, lockupTime2) at initalStorage;
multiplierPointsAfter2 = getAccountInitialMultiplierPoints(e.msg.sender);
assert lockupTime1 >= lockupTime2 => to_mathint(multiplierPointsAfter1) >= to_mathint(multiplierPointsAfter2);
satisfy to_mathint(multiplierPointsAfter1) > to_mathint(multiplierPointsAfter2);
}
/** /**
@title when there is no migration - some functions must revert. @title when there is no migration - some functions must revert.
Other function should have non reverting cases Other function should have non reverting cases