chore(cerotra/spec): fix rules

This commit is contained in:
Ricardo Guilherme Schmidt 2024-11-13 16:46:30 -03:00
parent 94858a4eb3
commit 377f01903f
6 changed files with 32 additions and 43 deletions

View File

@ -6,7 +6,7 @@
"certora/helpers/ERC20A.sol" "certora/helpers/ERC20A.sol"
], ],
"link" : [ "link" : [
"StakeVault:STAKED_TOKEN=ERC20A", "StakeVault:STAKING_TOKEN=ERC20A",
"StakeManager:REWARD_TOKEN=ERC20A", "StakeManager:REWARD_TOKEN=ERC20A",
"StakeManager:expiredStakeStorage=ExpiredStakeStorageA", "StakeManager:expiredStakeStorage=ExpiredStakeStorageA",
"StakeVault:stakeManager=StakeManager" "StakeVault:stakeManager=StakeManager"

View File

@ -5,13 +5,13 @@ methods {
} }
invariant MPcantBeGreaterThanMaxMP(address addr) invariant MPcantBeGreaterThanMaxMP(address addr)
to_mathint(getAccountCurrentMultiplierPoints(addr)) <= (getAccountBalance(addr) * 8) + getAccountBonusMultiplierPoints(addr) to_mathint(getAccountCurrentMultiplierPoints(addr)) <= to_mathint(getAccountMaxMultiplierPoints(addr))
filtered { filtered {
f -> f.selector != sig:migrateFrom(address,bool,StakeManager.Account).selector f -> f.selector != sig:migrateFrom(address,bool,StakeManager.Account).selector
} }
{ preserved { { preserved {
requireInvariant InitialMPIsNeverSmallerThanBalance(addr); requireInvariant MaxMPIsNeverSmallerThanBalance(addr);
requireInvariant CurrentMPIsNeverSmallerThanInitialMP(addr); requireInvariant CurrentMPIsNeverSmallerThanBalance(addr);
} }
} }

View File

@ -78,7 +78,7 @@ invariant sumOfMultipliersIsMultiplierSupply()
} }
{ preserved with (env e){ { preserved with (env e){
requireInvariant accountMPIsZeroIfBalanceIsZero(e.msg.sender); requireInvariant accountMPIsZeroIfBalanceIsZero(e.msg.sender);
requireInvariant accountBonusMPIsZeroIfBalanceIsZero(e.msg.sender); requireInvariant accountMaxMPIsZeroIfBalanceIsZero(e.msg.sender);
} }
} }
@ -95,20 +95,8 @@ invariant highEpochsAreNull(uint256 epochNumber)
m -> !requiresPreviousManager(m) && !requiresNextManager(m) m -> !requiresPreviousManager(m) && !requiresNextManager(m)
} }
invariant accountBonusMPIsZeroIfBalanceIsZero(address addr) invariant accountMaxMPIsZeroIfBalanceIsZero(address addr)
to_mathint(getAccountBalance(addr)) == 0 => to_mathint(getAccountBonusMultiplierPoints(addr)) == 0 to_mathint(getAccountBalance(addr)) == 0 => to_mathint(getAccountMaxMultiplierPoints(addr)) == 0
filtered {
f -> f.selector != sig:migrateFrom(address,bool,StakeManager.Account).selector
}
invariant accountMPIsZeroIfBalanceIsZero(address addr)
to_mathint(getAccountBalance(addr)) == 0 => to_mathint(getAccountCurrentMultiplierPoints(addr)) == 0
filtered {
f -> f.selector != sig:migrateFrom(address,bool,StakeManager.Account).selector
}
invariant InitialMPIsNeverSmallerThanBalance(address addr)
to_mathint(getAccountBonusMultiplierPoints(addr)) >= to_mathint(getAccountBalance(addr))
filtered { filtered {
f -> f.selector != sig:migrateFrom(address,bool,StakeManager.Account).selector f -> f.selector != sig:migrateFrom(address,bool,StakeManager.Account).selector
} }
@ -135,18 +123,18 @@ rule stakingMintsMultiplierPoints1To1Ratio {
uint256 multiplierPointsBefore; uint256 multiplierPointsBefore;
uint256 multiplierPointsAfter; uint256 multiplierPointsAfter;
requireInvariant InitialMPIsNeverSmallerThanBalance(e.msg.sender); requireInvariant MaxMPIsNeverSmallerThanBalance(e.msg.sender);
requireInvariant CurrentMPIsNeverSmallerThanInitialMP(e.msg.sender); requireInvariant CurrentMPIsNeverSmallerThanBalance(e.msg.sender);
requireInvariant accountMPIsZeroIfBalanceIsZero(e.msg.sender); requireInvariant accountMPIsZeroIfBalanceIsZero(e.msg.sender);
require getAccountLockUntil(e.msg.sender) <= e.block.timestamp; require getAccountLockUntil(e.msg.sender) <= e.block.timestamp;
multiplierPointsBefore = getAccountBonusMultiplierPoints(e.msg.sender); multiplierPointsBefore = getAccountMaxMultiplierPoints(e.msg.sender);
stake(e, amount, lockupTime); stake(e, amount, lockupTime);
multiplierPointsAfter = getAccountBonusMultiplierPoints(e.msg.sender); multiplierPointsAfter = getAccountMaxMultiplierPoints(e.msg.sender);
//
assert lockupTime == 0 => to_mathint(multiplierPointsAfter) == multiplierPointsBefore + amount; assert lockupTime == 0 => to_mathint(multiplierPointsAfter) == amount * 5;
assert to_mathint(multiplierPointsAfter) >= multiplierPointsBefore + amount; assert to_mathint(multiplierPointsAfter) == to_mathint(amount + ((amount * 100) * ((4 * 31556925) + lockupTime)) / (31556925 * 100));
} }
rule stakingGreaterLockupTimeMeansGreaterMPs { rule stakingGreaterLockupTimeMeansGreaterMPs {
@ -155,19 +143,19 @@ rule stakingGreaterLockupTimeMeansGreaterMPs {
uint256 amount; uint256 amount;
uint256 lockupTime1; uint256 lockupTime1;
uint256 lockupTime2; uint256 lockupTime2;
uint256 multiplierPointsAfter1; uint256 maxMPAfter1;
uint256 multiplierPointsAfter2; uint256 maxMPAfter2;
storage initalStorage = lastStorage; storage initalStorage = lastStorage;
stake(e, amount, lockupTime1); stake(e, amount, lockupTime1);
multiplierPointsAfter1 = getAccountBonusMultiplierPoints(e.msg.sender); maxMPAfter1 = getAccountMaxMultiplierPoints(e.msg.sender);
stake(e, amount, lockupTime2) at initalStorage; stake(e, amount, lockupTime2) at initalStorage;
multiplierPointsAfter2 = getAccountBonusMultiplierPoints(e.msg.sender); maxMPAfter2 = getAccountMaxMultiplierPoints(e.msg.sender);
assert lockupTime1 >= lockupTime2 => to_mathint(multiplierPointsAfter1) >= to_mathint(multiplierPointsAfter2); assert lockupTime1 >= lockupTime2 => to_mathint(maxMPAfter1) >= to_mathint(maxMPAfter2);
satisfy to_mathint(multiplierPointsAfter1) > to_mathint(multiplierPointsAfter2); satisfy to_mathint(maxMPAfter1) > to_mathint(maxMPAfter2);
} }
/** /**

View File

@ -6,7 +6,7 @@ methods {
function staked.balanceOf(address) external returns (uint256) envfree; function staked.balanceOf(address) external returns (uint256) envfree;
function totalStaked() external returns (uint256) envfree; function totalStaked() external returns (uint256) envfree;
function totalMP() external returns (uint256) envfree; function totalMP() external returns (uint256) envfree;
function totalMPPerEpoch() external returns (uint256) envfree; function totalMPRate() external returns (uint256) envfree;
function accounts(address) external returns(address, uint256, uint256, uint256, uint256, uint256, uint256, uint256) envfree; function accounts(address) external returns(address, uint256, uint256, uint256, uint256, uint256, uint256, uint256) envfree;
function _processAccount(StakeManager.Account storage account, uint256 _limitEpoch) internal with(env e) => markAccountProccessed(e.msg.sender, _limitEpoch); function _processAccount(StakeManager.Account storage account, uint256 _limitEpoch) internal with(env e) => markAccountProccessed(e.msg.sender, _limitEpoch);

View File

@ -19,11 +19,11 @@ function getAccountBalance(address addr) returns uint256 {
return balance; return balance;
} }
function getAccountBonusMultiplierPoints(address addr) returns uint256 { function getAccountMaxMultiplierPoints(address addr) returns uint256 {
uint256 bonusMP; uint256 maxMP;
_, _, bonusMP, _, _, _, _, _ = _stakeManager.accounts(addr); _, _, maxMP, _, _, _, _, _ = _stakeManager.accounts(addr);
return bonusMP; return maxMP;
} }
function getAccountCurrentMultiplierPoints(address addr) returns uint256 { function getAccountCurrentMultiplierPoints(address addr) returns uint256 {
@ -40,14 +40,15 @@ function getAccountLockUntil(address addr) returns uint256 {
return lockUntil; return lockUntil;
} }
invariant InitialMPIsNeverSmallerThanBalance(address addr)
to_mathint(getAccountBonusMultiplierPoints(addr)) >= to_mathint(getAccountBalance(addr)) invariant MaxMPIsNeverSmallerThanBalance(address addr)
to_mathint(getAccountMaxMultiplierPoints(addr)) >= to_mathint(getAccountBalance(addr))
filtered { filtered {
f -> f.selector != sig:_stakeManager.migrateFrom(address,bool,StakeManager.Account).selector f -> f.selector != sig:_stakeManager.migrateFrom(address,bool,StakeManager.Account).selector
} }
invariant CurrentMPIsNeverSmallerThanInitialMP(address addr) invariant CurrentMPIsNeverSmallerThanBalance(address addr)
to_mathint(getAccountCurrentMultiplierPoints(addr)) >= to_mathint(getAccountBonusMultiplierPoints(addr)) to_mathint(getAccountCurrentMultiplierPoints(addr)) >= to_mathint(getAccountBalance(addr))
filtered { filtered {
f -> f.selector != sig:_stakeManager.migrateFrom(address,bool,StakeManager.Account).selector f -> f.selector != sig:_stakeManager.migrateFrom(address,bool,StakeManager.Account).selector
} }

View File

@ -381,7 +381,7 @@ contract StakeManager is StakeMath, EpochMath, TrustedCodehashAccess, IStakeMana
uint256 _totalMP, uint256 _totalMP,
uint256 _totalStaked, uint256 _totalStaked,
uint256 _startTime, uint256 _startTime,
uint256 _totalMPPerEpoch, uint256 _totalMPRate,
uint256 _potentialMP, uint256 _potentialMP,
uint256 _currentEpochExpiredMP uint256 _currentEpochExpiredMP
) )
@ -398,7 +398,7 @@ contract StakeManager is StakeMath, EpochMath, TrustedCodehashAccess, IStakeMana
currentEpoch = _currentEpoch; currentEpoch = _currentEpoch;
totalMP = _totalMP; totalMP = _totalMP;
totalStaked = _totalStaked; totalStaked = _totalStaked;
totalMPRate = _totalMPPerEpoch; totalMPRate = _totalMPRate;
potentialMP = _potentialMP; potentialMP = _potentialMP;
currentEpochTotalExpiredMP = _currentEpochExpiredMP; currentEpochTotalExpiredMP = _currentEpochExpiredMP;
} }