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

chore(StakeManager.spec): add rule to ensure MP 1to1 ratio

This commit is contained in:
r4bbit 2024-03-12 16:08:28 +01:00
parent 7e2f675115
commit 1632e08f83
No known key found for this signature in database
GPG Key ID: E95F1E9447DC91A9
1 changed files with 28 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
certora/specs/StakeManager.spec
View File

@ -37,6 +37,13 @@ function getAccountCurrentMultiplierPoints(address addr) returns uint256 {
return currentMP; return currentMP;
} }
function getAccountLockUntil(address addr) returns uint256 {
uint256 lockUntil;
_, _, _, _, _, lockUntil, _ = accounts(addr);
return lockUntil;
}
function isMigrationfunction(method f) returns bool { function isMigrationfunction(method f) returns bool {
return return
f.selector == sig:migrateTo(bool).selector || f.selector == sig:migrateTo(bool).selector ||
@ -144,6 +151,27 @@ rule reachability(method f)
satisfy true; satisfy true;
} }
rule stakingMintsMultiplierPoints1To1Ratio {
env e;
uint256 amount;
uint256 lockupTime;
uint256 multiplierPointsBefore;
uint256 multiplierPointsAfter;
requireInvariant InitialMPIsNeverSmallerThanBalance(e.msg.sender);
requireInvariant CurrentMPIsNeverSmallerThanInitialMP(e.msg.sender);
require getAccountLockUntil(e.msg.sender) <= e.block.timestamp;
multiplierPointsBefore = getAccountInitialMultiplierPoints(e.msg.sender);
stake(e, amount, lockupTime);
multiplierPointsAfter = getAccountInitialMultiplierPoints(e.msg.sender);
assert lockupTime == 0 => to_mathint(multiplierPointsAfter) == multiplierPointsBefore + amount;
assert to_mathint(multiplierPointsAfter) >= multiplierPointsBefore + amount;
}
rule stakingGreaterLockupTimeMeansGreaterMPs { rule stakingGreaterLockupTimeMeansGreaterMPs {
env e; env e;