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 MPCantBeGreaterThanMaxMP invariant 

This commit introduces an invariant that ensures the generated
multiplier points can never be greater than the max boost multiplier
points.

See discussion in #80

Closes #80
This commit is contained in:
r4bbit 2024-03-11 12:38:54 +01:00
parent 4f590049d4
commit 8afa4f3ac9
No known key found for this signature in database
GPG Key ID: E95F1E9447DC91A9
1 changed files with 29 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

35
certora/specs/StakeManager.spec
View File

@ -7,15 +7,13 @@ methods {
function _.migrateFrom(address, bool, StakeManager.Account) external => NONDET;
function _.increaseMPFromMigration(uint256) external => NONDET;
function _.migrationInitialize(uint256,uint256,uint256,uint256) external => NONDET;
function accounts(address) external returns(address, uint256, uint256, uint256, uint256, uint256, uint256) envfree;
function Math.mulDiv(uint256 a, uint256 b, uint256 c) internal returns uint256 => mulDivSummary(a,b,c);
}
function getAccountMultiplierPoints(address addr) returns uint256 {
uint256 multiplierPoints;
_, _, _, multiplierPoints, _, _, _ = accounts(addr);
return multiplierPoints;
function mulDivSummary(uint256 a, uint256 b, uint256 c) returns uint256 {
require c != 0;
return require_uint256(a*b/c);
}
function getAccountBalance(address addr) returns uint256 {
@ -25,6 +23,20 @@ function getAccountBalance(address addr) returns uint256 {
return balance;
}
function getAccountInitialMultiplierPoints(address addr) returns uint256 {
uint256 initialMP;
_, _, initialMP, _, _, _, _ = accounts(addr);
return initialMP;
}
function getAccountCurrentMultiplierPoints(address addr) returns uint256 {
uint256 currentMP;
_, _, _, currentMP, _, _, _ = accounts(addr);
return currentMP;
}
function isMigrationfunction(method f) returns bool {
return
f.selector == sig:migrateTo(bool).selector ||
@ -101,6 +113,17 @@ invariant highEpochsAreNull(uint256 epochNumber)
m -> !requiresPreviousManager(m) && !requiresNextManager(m)
}
invariant MPcantBeGreaterThanMaxMP(address addr)
to_mathint(getAccountCurrentMultiplierPoints(addr)) <= (getAccountBalance(addr) * 8) + getAccountInitialMultiplierPoints(addr)
filtered {
f -> f.selector != sig:migrateFrom(address,bool,StakeManager.Account).selector
}
{ preserved {
require getAccountInitialMultiplierPoints(addr) >= getAccountBalance(addr);
require getAccountCurrentMultiplierPoints(addr) >= getAccountInitialMultiplierPoints(addr);
}
}
rule reachability(method f)
{
calldataarg args;