mirror of https://github.com/logos-co/staking.git
refactor(certora): Reorganize files, add proper descriptions, fix conf files and add summaries
This commit is contained in:
Ricardo Guilherme Schmidt
parent
ff94f5e46c
commit
cb81a7609c
|
|
@ -6,9 +6,9 @@
|
|||
],
|
||||
"link": [
|
||||
"StakeManager:REWARD_TOKEN=ERC20A",
|
||||
"StakeManager:expiredStakeStorage=ExpiredStakeStorageA"
|
||||
"StakeManager:EXPIRED_STAKE_STORAGE=ExpiredStakeStorageA"
|
||||
],
|
||||
"msg": "Verifying StakeManager.sol maxMP rule",
|
||||
"msg": "StakeManager:MaxMP",
|
||||
"rule_sanity": "basic",
|
||||
"verify": "StakeManager:certora/specs/MaxMPRule.spec",
|
||||
"optimistic_loop": true,
|
||||
|
|
|
|||
|
|
@ -6,9 +6,9 @@
|
|||
],
|
||||
"link": [
|
||||
"StakeManager:REWARD_TOKEN=ERC20A",
|
||||
"StakeManager:expiredStakeStorage=ExpiredStakeStorageA"
|
||||
"StakeManager:EXPIRED_STAKE_STORAGE=ExpiredStakeStorageA"
|
||||
],
|
||||
"msg": "Verifying StakeManager.sol",
|
||||
"msg": "StakeManager",
|
||||
"rule_sanity": "basic",
|
||||
"verify": "StakeManager:certora/specs/StakeManager.spec",
|
||||
"optimistic_loop": true,
|
||||
|
|
|
|||
|
|
@ -6,9 +6,9 @@
|
|||
],
|
||||
"link": [
|
||||
"StakeManager:REWARD_TOKEN=ERC20A",
|
||||
"StakeManager:expiredStakeStorage=ExpiredStakeStorageA"
|
||||
"StakeManager:EXPIRED_STAKE_STORAGE=ExpiredStakeStorageA"
|
||||
],
|
||||
"msg": "Verifying StakeManager ProcessAccount",
|
||||
"msg": "StakeManager:ProcessAccount",
|
||||
"rule_sanity": "basic",
|
||||
"verify": "StakeManager:certora/specs/StakeManagerProcessAccount.spec",
|
||||
"optimistic_loop": true,
|
||||
|
|
|
|||
|
|
@ -1,15 +1,15 @@
|
|||
{
|
||||
"files": [
|
||||
"contracts/StakeManager.sol",
|
||||
"certora/harness/StakeManagerNew.sol",
|
||||
"contracts/StakeManagerUpdated.sol",
|
||||
"certora/helpers/ExpiredStakeStorageA.sol",
|
||||
"certora/helpers/ERC20A.sol"
|
||||
],
|
||||
"link": [
|
||||
"StakeManager:REWARD_TOKEN=ERC20A",
|
||||
"StakeManager:expiredStakeStorage=ExpiredStakeStorageA"
|
||||
"StakeManager:EXPIRED_STAKE_STORAGE=ExpiredStakeStorageA"
|
||||
],
|
||||
"msg": "Verifying StakeManager.sol",
|
||||
"msg": "StakeManager:Migration",
|
||||
"rule_sanity": "basic",
|
||||
"verify": "StakeManager:certora/specs/StakeManagerStartMigration.spec",
|
||||
"optimistic_loop": true,
|
||||
|
|
|
|||
|
|
@ -8,10 +8,10 @@
|
|||
"link": [
|
||||
"StakeVault:STAKING_TOKEN=ERC20A",
|
||||
"StakeManager:REWARD_TOKEN=ERC20A",
|
||||
"StakeManager:expiredStakeStorage=ExpiredStakeStorageA",
|
||||
"StakeManager:EXPIRED_STAKE_STORAGE=ExpiredStakeStorageA",
|
||||
"StakeVault:stakeManager=StakeManager"
|
||||
],
|
||||
"msg": "Verifying StakeVault.sol",
|
||||
"msg": "StakeVault",
|
||||
"rule_sanity": "basic",
|
||||
"verify": "StakeVault:certora/specs/StakeVault.spec",
|
||||
"optimistic_loop": true,
|
||||
|
|
|
|||
|
|
@ -0,0 +1,29 @@
|
|||
import "./definition/DefinitionEpoch.spec";
|
||||
|
||||
methods {
|
||||
function EpochMath._calculateMPPrediction(uint256 _balance, uint256 _accountEpoch, uint256 _deltaTime) internal returns (uint256, uint256, uint256, uint256) => calculateMPPredictionSummary(_balance, _accountEpoch, _deltaTime);
|
||||
function EpochMath._calculateNewStartTime(uint256 _balance, uint256 _totalMP,uint256 _maxMP, uint256 _processTime) internal returns (uint256) => calculateNewStartTime( _balance, _totalMP, _maxMP, _processTime);
|
||||
}
|
||||
|
||||
function calculateMPPredictionSummary(uint256 _balance, uint256 _accountEpoch, uint256 _deltaTime) returns (uint256, uint256, uint256, uint256) {
|
||||
require _balance >= A_MIN();
|
||||
uint256 mpRate = require_uint256(accrueMP(_balance, T_RATE()));
|
||||
uint256 mpFractional = require_uint256(mpRate - accrueMP(_balance, _deltaTime));
|
||||
|
||||
mathint mpTarget = maxAccrueMP(_balance) + mpFractional;
|
||||
mathint deltaEpochTarget1 = mpTarget / mpRate;
|
||||
|
||||
uint256 epochTarget1 = require_uint256(_accountEpoch + deltaEpochTarget1);
|
||||
uint256 mpRemainder;
|
||||
if (mpTarget % mpRate > 0) {
|
||||
mpRemainder = require_uint256((mpRate * (deltaEpochTarget1 + 1)) - mpTarget);
|
||||
} else {
|
||||
mpRemainder = 0;
|
||||
}
|
||||
return (mpRate, mpFractional, epochTarget1, mpRemainder);
|
||||
}
|
||||
|
||||
|
||||
function calculateNewStartTime(uint256 _balance, uint256 _totalMP,uint256 _maxMP, uint256 _processTime) returns uint256 {
|
||||
return require_uint256(_processTime - timeToAccrueMP(_balance, retrieveAccruedMP(_balance, _totalMP, _maxMP)));
|
||||
}
|
||||
|
|
@ -0,0 +1,136 @@
|
|||
import "./definition/DefinitionEpoch.spec";
|
||||
|
||||
methods {
|
||||
function potentialMP() external returns (uint256) envfree;
|
||||
function START_TIME() external returns (uint256) envfree;
|
||||
function currentEpoch() external returns (uint256) envfree;
|
||||
function accounts(address) external returns(address, uint256, uint256, uint256, uint256, uint256, uint256, uint256) envfree;
|
||||
function totalStaked() external returns (uint256) envfree;
|
||||
function totalMP() external returns (uint256) envfree;
|
||||
function getEpochStartTime(uint256) external returns (uint256) envfree;
|
||||
function totalMPRate() external returns (uint256) envfree;
|
||||
function getEpoch(uint) external returns (uint256) envfree;
|
||||
function MIN_LOCKUP_PERIOD() external returns (uint256) envfree;
|
||||
function MAX_LOCKUP_PERIOD() external returns (uint256) envfree;
|
||||
function YEAR() external returns (uint256) envfree;
|
||||
function MAX_MULTIPLIER() external returns (uint256) envfree;
|
||||
function MP_APY() external returns (uint256) envfree;
|
||||
function MP_MPY() external returns (uint256) envfree;
|
||||
function MP_MPY_ABSOLUTE() external returns (uint256) envfree;
|
||||
function ACCURE_RATE() external returns (uint256) envfree;
|
||||
function MIN_BALANCE() external returns (uint256) envfree;
|
||||
}
|
||||
|
||||
definition requiresNextManager(method f) returns bool = (
|
||||
f.selector == sig:acceptUpdate().selector ||
|
||||
f.selector == sig:leave().selector ||
|
||||
f.selector == sig:transferNonPending().selector
|
||||
);
|
||||
|
||||
|
||||
function requireValidSystem(uint256 _processTime, uint256 _globalStartTime, uint256 _globalEpoch, uint256 _maxEpochsToProcess) {
|
||||
require _globalStartTime > 0;
|
||||
require _processTime >= START_TIME();
|
||||
mathint newEpoch = epoch(_processTime, _globalStartTime);
|
||||
require _globalEpoch <= newEpoch;
|
||||
require newEpoch - _globalEpoch <= _maxEpochsToProcess;
|
||||
}
|
||||
|
||||
function simplifyEpochProcessing(uint256 _processTime, uint256 _globalStartTime, uint256 _globalEpoch) {
|
||||
require _processTime == _globalStartTime;
|
||||
require _globalEpoch == 0;
|
||||
}
|
||||
|
||||
function requireValidAccount(uint256 _processTime, uint256 _globalStartTime, uint256 _globalEpoch, address _addr, uint256 _maxEpochsToProcess) {
|
||||
address rewardAddress;
|
||||
uint256 balance;
|
||||
uint256 maxMP;
|
||||
uint256 totalMP;
|
||||
uint256 lastMint;
|
||||
uint256 lockUntil;
|
||||
uint256 accountEpoch;
|
||||
uint256 accountStartTime;
|
||||
rewardAddress, balance, maxMP, totalMP, lastMint, lockUntil, accountEpoch, accountStartTime = accounts(_addr);
|
||||
|
||||
if(balance > 0){
|
||||
require balance >= MIN_BALANCE();
|
||||
require lastMint >= _globalStartTime;
|
||||
require lastMint <= _processTime;
|
||||
require lastMint < epochStart(accountEpoch+1, _globalStartTime);
|
||||
require accountStartTime >= _globalStartTime;
|
||||
require accountStartTime <= lastMint;
|
||||
require lockUntil >= accountStartTime;
|
||||
require accountEpoch <= _globalEpoch;
|
||||
require accountEpoch >= _globalEpoch - _maxEpochsToProcess;
|
||||
mathint lockTime = lockUntil - accountStartTime;
|
||||
require maxMP > maxTotalMP(balance, lockTime);
|
||||
require totalMP <= maxMP;
|
||||
} else {
|
||||
require accountStartTime == 0;
|
||||
require lastMint == 0;
|
||||
require rewardAddress == 0;
|
||||
require maxMP == 0;
|
||||
require totalMP == 0;
|
||||
require lockUntil == 0;
|
||||
require accountEpoch == 0;
|
||||
}
|
||||
}
|
||||
|
||||
function requireValidState(env e, uint256 _maxEpochsToProcess) {
|
||||
uint256 processTime = e.block.timestamp;
|
||||
address addr = e.msg.sender;
|
||||
uint256 globalEpoch = currentEpoch();
|
||||
uint256 globalStartTime = START_TIME();
|
||||
requireValidSystem(processTime, globalStartTime, globalEpoch, _maxEpochsToProcess);
|
||||
requireValidAccount(processTime, globalStartTime, globalEpoch, addr, _maxEpochsToProcess);
|
||||
}
|
||||
/**
|
||||
struct Account {
|
||||
address rewardAddress;
|
||||
uint256 balance;
|
||||
uint256 maxMP;
|
||||
uint256 totalMP;
|
||||
uint256 lastMint;
|
||||
uint256 lockUntil;
|
||||
uint256 accountEpoch;
|
||||
uint256 _globalStartTime;
|
||||
}
|
||||
**/
|
||||
|
||||
|
||||
function getAccountBalance(address _addr) returns uint256 {
|
||||
uint256 balance;
|
||||
_, balance, _, _, _, _, _, _ = accounts(_addr);
|
||||
return balance;
|
||||
}
|
||||
|
||||
|
||||
function getAccountLastMint(address _addr) returns uint256 {
|
||||
uint256 lastMint;
|
||||
_, _, _, _, lastMint, _, _, _ = accounts(_addr);
|
||||
return lastMint;
|
||||
}
|
||||
|
||||
function getAccountMaxMPs(address _addr) returns uint256 {
|
||||
uint256 maxMP;
|
||||
_, _, maxMP, _, _, _, _, _ = accounts(_addr);
|
||||
return maxMP;
|
||||
}
|
||||
|
||||
function getAccountTotalMPs(address _addr) returns uint256 {
|
||||
uint256 totalMP;
|
||||
_, _, _, totalMP, _, _, _, _ = accounts(_addr);
|
||||
return totalMP;
|
||||
}
|
||||
|
||||
function getAccountLockUntil(address _addr) returns uint256 {
|
||||
uint256 lockUntil;
|
||||
_, _, _, _, _, lockUntil, _, _ = accounts(_addr);
|
||||
return lockUntil;
|
||||
}
|
||||
|
||||
function getAccountEpoch(address _addr) returns uint256 {
|
||||
uint256 accountEpoch;
|
||||
_, _, _, _, _, _, accountEpoch, _ = accounts(_addr);
|
||||
return accountEpoch;
|
||||
}
|
||||
|
|
@ -1,42 +1,27 @@
|
|||
import "./shared.spec";
|
||||
import "./math/OpenZeppelinMath.spec";
|
||||
import "./EpochMath.spec";
|
||||
import "./IStakeManager.spec";
|
||||
import "./MultiplierPointsMathSummarized.spec";
|
||||
|
||||
methods {
|
||||
function startTime() external returns (uint256) envfree;
|
||||
function currentEpoch() external returns (uint256) envfree;
|
||||
|
||||
invariant MaxMPIsNeverSmallerThanBalance(address addr)
|
||||
to_mathint(getAccountMaxMPs(addr)) >= to_mathint(getAccountBalance(addr))
|
||||
{ preserved with (env e) {
|
||||
requireValidState(e, 2);
|
||||
}
|
||||
}
|
||||
|
||||
function simplifyEpochProcessing(env e){
|
||||
require e.block.timestamp == _stakeManager.startTime();
|
||||
require _stakeManager.currentEpoch() == 0;
|
||||
}
|
||||
|
||||
/* TODO: very usage of CONSTANT with Math.mulDiv or simplify mulDiv somehow, and replace simplifyEpochProcessing with reduceEpochProcessing
|
||||
|
||||
function reduceEpochProcessing(env e, uint256 maxEpochs) {
|
||||
require e.block.timestamp >= _stakeManager.startTime();
|
||||
uint256 currentEpoch = _stakeManager.currentEpoch();
|
||||
uint256 newEpoch = _stakeManager.newEpoch(e);
|
||||
require currentEpoch <= newEpoch;
|
||||
require currentEpoch - newEpoch <= maxEpochs;
|
||||
}
|
||||
|
||||
function reduceAccountProcessing(env e, address addr, uint256 maxEpochs) {
|
||||
uint256 currentEpoch = _stakeManager.currentEpoch();
|
||||
uint256 accountEpoch = getAccountEpoch(addr);
|
||||
require accountEpoch <= currentEpoch;
|
||||
require accountEpoch >= currentEpoch - maxEpochs;
|
||||
}
|
||||
*/
|
||||
invariant CurrentMPIsNeverSmallerThanBalance(address addr)
|
||||
to_mathint(getAccountTotalMPs(addr)) >= to_mathint(getAccountBalance(addr))
|
||||
{ preserved with (env e) {
|
||||
requireValidState(e, 2);
|
||||
}
|
||||
}
|
||||
|
||||
invariant MPcantBeGreaterThanMaxMP(address addr)
|
||||
to_mathint(getAccountCurrentMultiplierPoints(addr)) <= to_mathint(getAccountMaxMultiplierPoints(addr))
|
||||
filtered {
|
||||
f -> f.selector != sig:migrateFrom(address,bool,StakeManager.Account).selector
|
||||
}
|
||||
to_mathint(getAccountTotalMPs(addr)) <= to_mathint(getAccountMaxMPs(addr))
|
||||
{ preserved with (env e) {
|
||||
simplifyEpochProcessing(e);
|
||||
/*reduceEpochProcessing(e, 3);
|
||||
reduceAccountProcessing(e, addr, 3);*/
|
||||
requireValidState(e, 2);
|
||||
requireInvariant MaxMPIsNeverSmallerThanBalance(addr);
|
||||
requireInvariant CurrentMPIsNeverSmallerThanBalance(addr);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -0,0 +1,64 @@
|
|||
import "./definition/DefinitionMultiplierPointsMath.spec";
|
||||
|
||||
methods {
|
||||
function MultiplierPointMath._accrueMP(uint256 _balance, uint256 _deltaTime) internal returns (uint256) => accrueMPSummary(_balance, _deltaTime) ;
|
||||
function MultiplierPointMath._bonusMP(uint256 _balance, uint256 _lockedSeconds) internal returns (uint256) => bonusMPSummary(_balance, _lockedSeconds);
|
||||
function MultiplierPointMath._initialMP(uint256 _balance) internal returns (uint256) => initialMPSummary(_balance);
|
||||
function MultiplierPointMath._reduceMP(uint256 _balance, uint256 _mp, uint256 _reducedAmount) internal returns (uint256) => reduceMPSummary(_balance, _mp, _reducedAmount);
|
||||
function MultiplierPointMath._maxAccrueMP(uint256 _balance) internal returns (uint256) => maxAccrueMPSummary(_balance);
|
||||
function MultiplierPointMath._maxTotalMP(uint256 _balance, uint256 _lockTime) internal returns (uint256) => maxTotalMPSummary(_balance, _lockTime) ;
|
||||
function MultiplierPointMath._maxAbsoluteMP(uint256 _balance) internal returns (uint256) => maxAbsoluteMPSummary(_balance);
|
||||
function MultiplierPointMath._lockTimeAvailable(uint256 _balance, uint256 _mpMax) internal returns (uint256) => lockTimeAvailableSummary(_balance, _mpMax);
|
||||
function MultiplierPointMath._timeToAccrueMP(uint256 _balance, uint256 _mp) internal returns (uint256) => timeToAccrueMPSummary(_balance, _mp);
|
||||
function MultiplierPointMath._retrieveBonusMP(uint256 _balance, uint256 _maxMP) internal returns (uint256) => retrieveBonusMPSummary(_balance, _maxMP);
|
||||
function MultiplierPointMath._retrieveAccruedMP(uint256 _balance, uint256 _totalMP, uint256 _maxMP) internal returns (uint256) => retrieveAccruedMPSummary(_balance, _totalMP, _maxMP);
|
||||
}
|
||||
|
||||
function accrueMPSummary(uint256 _balance, uint256 _deltaTime) returns uint256 {
|
||||
return require_uint256(accrueMP(_balance, _deltaTime));
|
||||
}
|
||||
|
||||
function bonusMPSummary(uint256 _balance, uint256 _lockedSeconds) returns uint256 {
|
||||
return require_uint256(bonusMP(_balance, _lockedSeconds));
|
||||
}
|
||||
|
||||
function initialMPSummary(uint256 _balance) returns uint256 {
|
||||
return _balance;
|
||||
}
|
||||
|
||||
function reduceMPSummary(
|
||||
uint256 _balance,
|
||||
uint256 _mp,
|
||||
uint256 _reducedAmount
|
||||
) returns uint256 {
|
||||
return require_uint256(reduceMP(_balance,_mp,_reducedAmount));
|
||||
}
|
||||
|
||||
function maxAccrueMPSummary(uint256 _balance) returns uint256 {
|
||||
return require_uint256(maxAccrueMP(_balance));
|
||||
}
|
||||
|
||||
function maxTotalMPSummary(uint256 _balance, uint256 _lockTime) returns uint256 {
|
||||
return require_uint256(maxTotalMP(_balance, _lockTime));
|
||||
}
|
||||
|
||||
function maxAbsoluteMPSummary(uint256 _balance) returns uint256 {
|
||||
return require_uint256(maxAbsoluteMP(_balance));
|
||||
}
|
||||
|
||||
function lockTimeAvailableSummary(
|
||||
uint256 _balance,
|
||||
uint256 _mpMax
|
||||
) returns uint256 {
|
||||
return require_uint256(lockTimeAvailable(_balance, _mpMax));
|
||||
}
|
||||
|
||||
function timeToAccrueMPSummary(uint256 _balance, uint256 _mp) returns uint256 {
|
||||
return require_uint256(timeToAccrueMP(_balance, _mp));
|
||||
}
|
||||
function retrieveBonusMPSummary(uint256 _balance, uint256 _maxMP) returns uint256 {
|
||||
return require_uint256(retrieveBonusMP(_balance, _maxMP));
|
||||
}
|
||||
function retrieveAccruedMPSummary(uint256 _balance, uint256 _totalMP, uint256 _maxMP) returns uint256 {
|
||||
return require_uint256(retrieveAccruedMP(_balance, _totalMP, _maxMP));
|
||||
}
|
||||
|
|
@ -1,15 +1,15 @@
|
|||
import "./shared.spec";
|
||||
import "./definition/DefinitionMath.spec";
|
||||
import "./definition/DefinitionMultiplierPointsMath.spec";
|
||||
import "./math/OpenZeppelinMath.spec";
|
||||
import "./IStakeManager.spec";
|
||||
|
||||
using ERC20A as staked;
|
||||
using StakeManager as _stakeManager;
|
||||
|
||||
methods {
|
||||
function staked.balanceOf(address) external returns (uint256) envfree;
|
||||
function totalStaked() external returns (uint256) envfree;
|
||||
function totalMP() external returns (uint256) envfree;
|
||||
function previousManager() external returns (address) envfree;
|
||||
function _.migrateFrom(address, bool, StakeManager.Account) external => NONDET;
|
||||
function _.increaseTotalMP(uint256) external => NONDET;
|
||||
function _.migrationInitialize(uint256,uint256,uint256,uint256,uint256,uint256,uint256) external => NONDET;
|
||||
function _._ external => DISPATCH [] default NONDET;
|
||||
}
|
||||
|
||||
|
|
@ -24,7 +24,6 @@ function isMigrationfunction(method f) returns bool {
|
|||
cases where it is zero. specifically no externall call to the migration contract */
|
||||
function simplification(env e) {
|
||||
require currentContract.migration == 0;
|
||||
require currentContract.previousManager() == 0;
|
||||
require e.msg.sender != 0;
|
||||
}
|
||||
|
||||
|
|
@ -58,16 +57,22 @@ hook Sload uint256 newValue accounts[KEY address addr].totalMP {
|
|||
require sumOfMultipliers >= to_mathint(newValue);
|
||||
}
|
||||
|
||||
invariant MaxMPIsNeverSmallerThanBalance(address addr)
|
||||
to_mathint(getAccountMaxMPs(addr)) >= to_mathint(getAccountBalance(addr));
|
||||
|
||||
invariant CurrentMPIsNeverSmallerThanBalance(address addr)
|
||||
to_mathint(getAccountTotalMPs(addr)) >= to_mathint(getAccountBalance(addr));
|
||||
|
||||
invariant sumOfBalancesIsTotalSupplyBalance()
|
||||
sumOfBalances == to_mathint(totalStaked())
|
||||
filtered {
|
||||
m -> !requiresPreviousManager(m) && !requiresNextManager(m)
|
||||
m -> !requiresNextManager(m)
|
||||
}
|
||||
|
||||
invariant sumOfMultipliersIsMultiplierSupply()
|
||||
sumOfMultipliers == to_mathint(totalMP())
|
||||
filtered {
|
||||
m -> !requiresPreviousManager(m) && !requiresNextManager(m)
|
||||
m -> !requiresNextManager(m)
|
||||
}
|
||||
{ preserved with (env e){
|
||||
requireInvariant accountMPIsZeroIfBalanceIsZero(e.msg.sender);
|
||||
|
|
@ -85,20 +90,14 @@ invariant sumOfEpochRewardsIsPendingRewards()
|
|||
invariant highEpochsAreNull(uint256 epochNumber)
|
||||
epochNumber >= currentContract.currentEpoch => currentContract.epochs[epochNumber].epochReward == 0
|
||||
filtered {
|
||||
m -> !requiresPreviousManager(m) && !requiresNextManager(m)
|
||||
m -> !requiresNextManager(m)
|
||||
}
|
||||
|
||||
invariant accountMaxMPIsZeroIfBalanceIsZero(address addr)
|
||||
to_mathint(getAccountBalance(addr)) == 0 => to_mathint(getAccountMaxMultiplierPoints(addr)) == 0
|
||||
filtered {
|
||||
f -> f.selector != sig:migrateFrom(address,bool,StakeManager.Account).selector
|
||||
}
|
||||
to_mathint(getAccountBalance(addr)) == 0 => to_mathint(getAccountMaxMPs(addr)) == 0;
|
||||
|
||||
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
|
||||
}
|
||||
to_mathint(getAccountBalance(addr)) == 0 => to_mathint(getAccountTotalMPs(addr)) == 0;
|
||||
|
||||
rule reachability(method f)
|
||||
{
|
||||
|
|
@ -122,12 +121,12 @@ rule stakingMintsMultiplierPoints1To1Ratio {
|
|||
|
||||
require getAccountLockUntil(e.msg.sender) <= e.block.timestamp;
|
||||
|
||||
multiplierPointsBefore = getAccountMaxMultiplierPoints(e.msg.sender);
|
||||
multiplierPointsBefore = getAccountMaxMPs(e.msg.sender);
|
||||
stake(e, amount, lockupTime);
|
||||
multiplierPointsAfter = getAccountMaxMultiplierPoints(e.msg.sender);
|
||||
//
|
||||
multiplierPointsAfter = getAccountMaxMPs(e.msg.sender);
|
||||
|
||||
assert lockupTime == 0 => to_mathint(multiplierPointsAfter) == amount * 5;
|
||||
assert to_mathint(multiplierPointsAfter) == to_mathint(amount + ((amount * 100) * ((4 * 31556925) + lockupTime)) / (31556925 * 100));
|
||||
assert to_mathint(multiplierPointsAfter) == maxTotalMP(amount, lockupTime);
|
||||
}
|
||||
|
||||
rule stakingGreaterLockupTimeMeansGreaterMPs {
|
||||
|
|
@ -142,10 +141,10 @@ rule stakingGreaterLockupTimeMeansGreaterMPs {
|
|||
storage initalStorage = lastStorage;
|
||||
|
||||
stake(e, amount, lockupTime1);
|
||||
maxMPAfter1 = getAccountMaxMultiplierPoints(e.msg.sender);
|
||||
maxMPAfter1 = getAccountMaxMPs(e.msg.sender);
|
||||
|
||||
stake(e, amount, lockupTime2) at initalStorage;
|
||||
maxMPAfter2 = getAccountMaxMultiplierPoints(e.msg.sender);
|
||||
maxMPAfter2 = getAccountMaxMPs(e.msg.sender);
|
||||
|
||||
assert lockupTime1 >= lockupTime2 => to_mathint(maxMPAfter1) >= to_mathint(maxMPAfter2);
|
||||
satisfy to_mathint(maxMPAfter1) > to_mathint(maxMPAfter2);
|
||||
|
|
|
|||
|
|
@ -1,16 +1,10 @@
|
|||
import "./shared.spec";
|
||||
import "./IStakeManager.spec";
|
||||
|
||||
using ERC20A as staked;
|
||||
|
||||
methods {
|
||||
function staked.balanceOf(address) external returns (uint256) envfree;
|
||||
function totalStaked() external returns (uint256) envfree;
|
||||
function totalMP() external returns (uint256) envfree;
|
||||
function totalMPRate() external returns (uint256) envfree;
|
||||
|
||||
function _processAccount(StakeManager.Account storage account, uint256 _limitEpoch) internal with(env e) => markAccountProccessed(e.msg.sender, _limitEpoch);
|
||||
function _.migrationInitialize(uint256,uint256,uint256,uint256,uint256,uint256,uint256) external => NONDET;
|
||||
function potentialMP() external returns (uint256) envfree;
|
||||
function _processAccount(IStakeManager.Account storage account, uint256 _limitEpoch) internal with(env e) => markAccountProccessed(e.msg.sender, _limitEpoch);
|
||||
}
|
||||
|
||||
// keeps track of the last epoch an account was processed
|
||||
|
|
@ -35,7 +29,7 @@ hook Sstore accounts[KEY address addr].balance uint256 newValue (uint256 oldValu
|
|||
https://prover.certora.com/output/40726/055d52bc67154e3fbea330fd7d68d36d/?anonymousKey=73030555b4cefe429d4eed6718b9a7e5be3a22c8
|
||||
*/
|
||||
rule checkAccountProcessedBeforeStoring(method f) filtered {
|
||||
f -> !requiresPreviousManager(f) && !requiresNextManager(f) && f.selector != sig:stake(uint256,uint256).selector
|
||||
f -> !requiresNextManager(f) && f.selector != sig:stake(uint256,uint256).selector && f.selector != sig:startMigration(address).selector
|
||||
} {
|
||||
address account;
|
||||
|
||||
|
|
|
|||
|
|
@ -1,27 +1,49 @@
|
|||
import "./shared.spec";
|
||||
import "./IStakeManager.spec";
|
||||
|
||||
using ERC20A as staked;
|
||||
using StakeManagerNew as newStakeManager;
|
||||
using StakeManagerUpdated as newStakeManager;
|
||||
|
||||
methods {
|
||||
function staked.balanceOf(address) external returns (uint256) envfree;
|
||||
function totalStaked() external returns (uint256) envfree;
|
||||
function totalMP() external returns (uint256) envfree;
|
||||
function previousManager() external returns (address) envfree;
|
||||
function newStakeManager.PREVIOUS_MANAGER() external returns (address) envfree;
|
||||
|
||||
function _.migrationInitialize(uint256,uint256,uint256,uint256,uint256,uint256,uint256) external => DISPATCHER(true);
|
||||
function StakeManagerNew.totalStaked() external returns (uint256) envfree;
|
||||
function newStakeManager.totalStaked() external returns (uint256) envfree;
|
||||
}
|
||||
|
||||
|
||||
invariant MaxMPIsNeverSmallerThanBalance(address addr)
|
||||
to_mathint(getAccountMaxMPs(addr)) >= to_mathint(getAccountBalance(addr))
|
||||
filtered {
|
||||
f -> f.selector != sig:StakeManagerUpdated.migrateFrom(address,bool,IStakeManager.Account).selector
|
||||
}
|
||||
|
||||
invariant CurrentMPIsNeverSmallerThanBalance(address addr)
|
||||
to_mathint(getAccountTotalMPs(addr)) >= to_mathint(getAccountBalance(addr))
|
||||
filtered {
|
||||
f -> f.selector != sig:StakeManagerUpdated.migrateFrom(address,bool,IStakeManager.Account).selector
|
||||
}
|
||||
|
||||
|
||||
|
||||
definition requiresPreviousManager(method f) returns bool = (
|
||||
f.selector == sig:StakeManagerUpdated.migrationInitialize(uint256,uint256,uint256,uint256,uint256,uint256,uint256).selector ||
|
||||
f.selector == sig:StakeManagerUpdated.migrateFrom(address,bool,IStakeManager.Account).selector ||
|
||||
f.selector == sig:StakeManagerUpdated.increaseTotalMP(uint256).selector
|
||||
);
|
||||
|
||||
|
||||
definition blockedWhenMigrating(method f) returns bool = (
|
||||
f.selector == sig:stake(uint256, uint256).selector ||
|
||||
f.selector == sig:unstake(uint256).selector ||
|
||||
f.selector == sig:lock(uint256).selector ||
|
||||
f.selector == sig:executeEpoch().selector ||
|
||||
f.selector == sig:executeEpoch(uint256).selector ||
|
||||
f.selector == sig:startMigration(address).selector ||
|
||||
f.selector == sig:migrationInitialize(uint256,uint256,uint256,uint256,uint256,uint256,uint256).selector
|
||||
);
|
||||
f.selector == sig:stake(uint256, uint256).selector ||
|
||||
f.selector == sig:unstake(uint256).selector ||
|
||||
f.selector == sig:lock(uint256).selector ||
|
||||
f.selector == sig:executeEpoch().selector ||
|
||||
f.selector == sig:executeEpoch(uint256).selector ||
|
||||
f.selector == sig:startMigration(address).selector ||
|
||||
f.selector == sig:StakeManagerUpdated.migrationInitialize(uint256,uint256,uint256,uint256,uint256,uint256,uint256).selector
|
||||
);
|
||||
|
||||
definition blockedWhenNotMigrating(method f) returns bool = (
|
||||
f.selector == sig:acceptUpdate().selector ||
|
||||
|
|
|
|||
|
|
@ -0,0 +1,95 @@
|
|||
import "./definition/DefinitionMath.spec";
|
||||
import "./definition/DefinitionEpoch.spec";
|
||||
import "./definition/DefinitionMultiplierPointsMath.spec";
|
||||
import "./math/OpenZeppelinMath.spec";
|
||||
import "./EpochMath.spec";
|
||||
import "./IStakeManager.spec";
|
||||
|
||||
rule check_stake(
|
||||
uint256 _increasedAmount,
|
||||
uint256 _increasedLockSeconds
|
||||
)
|
||||
{
|
||||
env e;
|
||||
uint256 processTime = e.block.timestamp;
|
||||
address addr = e.msg.sender;
|
||||
uint256 globalEpoch = currentEpoch();
|
||||
uint256 globalStartTime = START_TIME();
|
||||
|
||||
requireValidSystem(processTime, globalStartTime, globalEpoch, 2);
|
||||
requireValidAccount(processTime, globalStartTime, globalEpoch, addr, 2);
|
||||
|
||||
address initial_rewardAddress;
|
||||
uint256 initial_balance;
|
||||
uint256 initial_maxMP;
|
||||
uint256 initial_totalMP;
|
||||
uint256 initial_lastMint;
|
||||
uint256 initial_lockUntil;
|
||||
uint256 initial_accountEpoch;
|
||||
uint256 initial_accountStartTime;
|
||||
|
||||
initial_rewardAddress, initial_balance, initial_maxMP, initial_totalMP, initial_lastMint, initial_lockUntil, initial_accountEpoch, initial_accountStartTime = accounts(addr);
|
||||
|
||||
|
||||
mathint calc_balance = initial_balance + _increasedAmount;
|
||||
mathint calc_lockUntil = max(initial_lockUntil, processTime) + _increasedLockSeconds;
|
||||
mathint dt_lock = calc_lockUntil - processTime;
|
||||
mathint calc_accountEpoch = newEpoch(e);
|
||||
|
||||
require calc_balance >= A_MIN();
|
||||
require dt_lock == 0 || dt_lock >= T_MIN();
|
||||
require dt_lock <= T_MAX();
|
||||
|
||||
|
||||
|
||||
mathint delta_bonusMP_initial_balance = bonusMP(initial_balance, _increasedLockSeconds);
|
||||
mathint delta_bonusMP_increasedAmount = bonusMP(_increasedAmount, dt_lock);
|
||||
|
||||
mathint delta_bonusMP = delta_bonusMP_initial_balance + delta_bonusMP_increasedAmount;
|
||||
mathint delta_accountEpoch = calc_accountEpoch - initial_accountEpoch;
|
||||
|
||||
mathint calc_lastMint;
|
||||
if(initial_lastMint == 0){
|
||||
calc_lastMint = processTime;
|
||||
} else if (delta_accountEpoch == 0) {
|
||||
calc_lastMint = initial_lastMint;
|
||||
} else {
|
||||
calc_lastMint = epochStart(calc_accountEpoch, globalStartTime);
|
||||
}
|
||||
|
||||
mathint delta_totalMP = initialMP(_increasedAmount) + delta_bonusMP;
|
||||
mathint currentEpochAccrued = initial_accountEpoch < calc_accountEpoch ? accrueMP(initial_balance, epochStart(initial_accountEpoch+1, globalStartTime) - initial_lastMint) : 0;
|
||||
mathint calc_accruedMP = initial_accountEpoch < calc_accountEpoch ? min(currentEpochAccrued + (accrueMP(initial_balance, T_RATE()) * (delta_accountEpoch-1)), initial_maxMP - initial_totalMP) : 0;
|
||||
mathint calc_maxMP = initial_maxMP + delta_totalMP + accrueMP(_increasedAmount, MAX_MULTIPLIER() * YEAR());
|
||||
mathint calc_totalMP = initial_totalMP + delta_totalMP + calc_accruedMP;
|
||||
|
||||
mathint calc_accountStartTime ;
|
||||
if(initial_accountStartTime == 0) {
|
||||
calc_accountStartTime = processTime;
|
||||
} else if (_increasedAmount > 0) {
|
||||
calc_accountStartTime = processTime - timeToAccrueMP(calc_balance, retrieveAccruedMP(calc_balance, calc_totalMP, calc_maxMP));
|
||||
} else {
|
||||
calc_accountStartTime = initial_accountStartTime;
|
||||
}
|
||||
|
||||
stake(e, _increasedAmount, _increasedLockSeconds);
|
||||
|
||||
address final_rewardAddress;
|
||||
uint256 final_balance;
|
||||
uint256 final_maxMP;
|
||||
uint256 final_totalMP;
|
||||
uint256 final_lastMint;
|
||||
uint256 final_lockUntil;
|
||||
uint256 final_accountEpoch;
|
||||
uint256 final_accountStartTime;
|
||||
final_rewardAddress, final_balance, final_maxMP, final_totalMP, final_lastMint, final_lockUntil, final_accountEpoch, final_accountStartTime = accounts(addr);
|
||||
|
||||
//assert(final_rewardAddress == calc_rewardAddress);
|
||||
assert(to_mathint(final_balance) == calc_balance);
|
||||
assert(to_mathint(final_maxMP) == calc_maxMP);
|
||||
assert(to_mathint(final_totalMP) == calc_totalMP);
|
||||
assert(to_mathint(final_lastMint) == calc_lastMint);
|
||||
assert(to_mathint(final_lockUntil) == calc_lockUntil);
|
||||
assert(to_mathint(final_accountEpoch) == calc_accountEpoch);
|
||||
assert(to_mathint(final_accountStartTime) == calc_accountStartTime);
|
||||
}
|
||||
|
|
@ -1,5 +1,3 @@
|
|||
import "./shared.spec";
|
||||
|
||||
using ERC20A as staked;
|
||||
using StakeManager as stakeManager;
|
||||
|
||||
|
|
@ -7,23 +5,22 @@ methods {
|
|||
function ERC20A.balanceOf(address) external returns (uint256) envfree;
|
||||
function ERC20A.allowance(address, address) external returns(uint256) envfree;
|
||||
function ERC20A.totalSupply() external returns(uint256) envfree;
|
||||
function _.migrateFrom(address, bool, StakeManager.Account) external => DISPATCHER(true);
|
||||
function _.increaseTotalMP(uint256) external => DISPATCHER(true);
|
||||
function StakeManager.accounts(address) external returns(address, uint256, uint256, uint256, uint256, uint256, uint256, uint256) envfree;
|
||||
|
||||
function _.owner() external => DISPATCHER(true);
|
||||
}
|
||||
|
||||
definition isMigrationFunction(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 ||
|
||||
f.selector == sig:stakeManager.startMigration(address).selector
|
||||
);
|
||||
function getAccountBalance(address _addr) returns uint256 {
|
||||
uint256 balance;
|
||||
_, balance, _, _, _, _, _, _ = stakeManager.accounts(_addr);
|
||||
return balance;
|
||||
}
|
||||
|
||||
// check that the ERC20.balanceOf(vault) is >= to StakeManager.accounts[a].balance
|
||||
invariant accountBalanceVsERC20Balance()
|
||||
staked.balanceOf(currentContract) >= getAccountBalance(currentContract)
|
||||
filtered {
|
||||
m -> m.selector != sig:leave().selector && !isMigrationFunction(m)
|
||||
m -> m.selector != sig:leave().selector
|
||||
}
|
||||
{ preserved with (env e) {
|
||||
// the sender can't be the vault otherwise it can transfer tokens
|
||||
|
|
@ -48,9 +45,7 @@ invariant accountBalanceVsERC20Balance()
|
|||
}
|
||||
|
||||
preserved stake(uint256 amount, uint256 duration) with (env e) {
|
||||
|
||||
require e.msg.sender != currentContract;
|
||||
|
||||
require staked.balanceOf(currentContract) + staked.balanceOf(e.msg.sender) + staked.balanceOf(stakeManager) <= to_mathint(staked.totalSupply());
|
||||
}
|
||||
}
|
||||
|
|
@ -62,7 +57,7 @@ function simplification() {
|
|||
require stakeManager.migration == 0;
|
||||
}
|
||||
|
||||
rule reachability(method f) filtered { f -> !isMigrationFunction(f) }
|
||||
rule reachability(method f)
|
||||
{
|
||||
calldataarg args;
|
||||
env e;
|
||||
|
|
|
|||
|
|
@ -0,0 +1,6 @@
|
|||
import "./DefinitionMultiplierPointsMath.spec";
|
||||
|
||||
definition epoch(mathint _timestamp, mathint startTime) returns mathint = (_timestamp - startTime) / T_RATE();
|
||||
definition epochStart(mathint _epochNum, mathint startTime) returns mathint = startTime + (T_RATE() * _epochNum);
|
||||
|
||||
|
||||
|
|
@ -0,0 +1,17 @@
|
|||
definition abs(mathint x) returns mathint =
|
||||
x >= 0 ? x : 0 - x;
|
||||
|
||||
definition min(mathint x, mathint y) returns mathint =
|
||||
x > y ? y : x;
|
||||
|
||||
definition max(mathint x, mathint y) returns mathint =
|
||||
x > y ? x : y;
|
||||
|
||||
definition average(mathint a, mathint b) returns mathint =
|
||||
(a + b) / 2;
|
||||
|
||||
definition mulDiv(mathint x, mathint y, mathint denominator) returns mathint =
|
||||
(x * y) / denominator;
|
||||
|
||||
definition ceilMulDiv(mathint x, mathint y, mathint denominator) returns mathint =
|
||||
mulDiv(x, y, denominator) + ((x * y) % denominator > 0 ? 1 : 0);
|
||||
|
|
@ -0,0 +1,29 @@
|
|||
import "./DefinitionTime.spec";
|
||||
definition M_MAX() returns mathint = 4;
|
||||
definition APY() returns mathint = 100;
|
||||
definition MPY() returns mathint = M_MAX() * APY();
|
||||
definition MPY_ABS() returns mathint = 100 + (2 * (M_MAX() * APY()));
|
||||
definition T_RATE() returns mathint = 1 * T_WEEK();
|
||||
definition A_MIN() returns mathint = (((T_YEAR() * 100) - 1) / (APY() * T_RATE())) + 1;
|
||||
definition T_MIN() returns mathint = 90 * T_DAY();
|
||||
definition T_MAX() returns mathint = M_MAX() * T_YEAR();
|
||||
|
||||
|
||||
definition accrueMP(mathint _balance, mathint _deltaTime) returns mathint = (_balance * _deltaTime * APY()) / (T_YEAR() * 100);
|
||||
definition bonusMP(mathint _balance, mathint _lockedSeconds) returns mathint = accrueMP(_balance, _lockedSeconds);
|
||||
definition initialMP(mathint _balance) returns mathint = _balance;
|
||||
definition reduceMP(mathint _balance, mathint _mp, mathint _reducedAmount) returns mathint = (_mp * _balance) / _reducedAmount;
|
||||
|
||||
definition maxTotalMP(mathint _balance, mathint _lockTime) returns mathint = _balance + ((_balance * APY()) * ((M_MAX() * T_YEAR()) + _lockTime) / (T_YEAR() * 100));
|
||||
definition maxAccrueMP(mathint _balance) returns mathint = (_balance * MPY()) / 100;
|
||||
definition maxAbsoluteMP(mathint _balance) returns mathint = (_balance * MPY_ABS()) / 100;
|
||||
definition retrieveBonusMP(mathint _balance, mathint _maxMP) returns mathint = _maxMP - (_balance + maxAccrueMP(_balance));
|
||||
definition retrieveAccruedMP(mathint _balance, mathint _totalMP, mathint _maxMP) returns mathint = _totalMP - maxAccrueMP(_balance) - _maxMP;
|
||||
definition timeToAccrueMP(mathint _balance, mathint _targetMP) returns mathint = (_targetMP * 100 * T_YEAR()) / (_balance * APY());
|
||||
definition estimateLockTime(mathint _balance, mathint _maxMP) returns mathint = (((_maxMP-_balance) * 100 * T_YEAR())+1) / ((_balance * APY())-1);
|
||||
definition lockTimeAvailable(mathint _balance, mathint _maxMP) returns mathint = ((maxAbsoluteMP(_balance) - _maxMP) * T_YEAR()) / _balance;
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
|
@ -0,0 +1,5 @@
|
|||
definition T_MINUTE() returns mathint = 60;
|
||||
definition T_HOUR() returns mathint = 60 * T_MINUTE();
|
||||
definition T_DAY() returns mathint = 24 * T_HOUR();
|
||||
definition T_WEEK() returns mathint = 7 * T_DAY();
|
||||
definition T_YEAR() returns mathint = 365 * T_DAY() + 5 * T_HOUR() + 48 * T_MINUTE() + 45;
|
||||
|
|
@ -0,0 +1,44 @@
|
|||
// Summary for OpenZeppelin's Math.
|
||||
methods
|
||||
{
|
||||
function Math.max(uint256 a, uint256 b) internal returns (uint256) => maxSummary(a, b);
|
||||
function Math.min(uint256 a, uint256 b) internal returns (uint256) => minSummary(a, b);
|
||||
function Math.average(uint256 a, uint256 b) internal returns (uint256) => averageSummary(a, b);
|
||||
function Math.ceilDiv(uint256 a, uint256 b) internal returns (uint256) => ceilDivSummary(a, b);
|
||||
function Math.mulDiv(uint256 x, uint256 y, uint256 denominator) internal returns (uint256) => mulDivSummary(x, y, denominator);
|
||||
function Math.mulDiv(uint256 x, uint256 y, uint256 denominator, Math.Rounding rounding) internal returns (uint256) => mulDivSummaryRounding(x, y, denominator, rounding);
|
||||
}
|
||||
|
||||
function maxSummary(uint256 a, uint256 b) returns uint256
|
||||
{
|
||||
return a > b ? a : b;
|
||||
}
|
||||
|
||||
function minSummary(uint256 a, uint256 b) returns uint256
|
||||
{
|
||||
return a < b ? a : b;
|
||||
}
|
||||
|
||||
function averageSummary(uint256 a, uint256 b) returns uint256
|
||||
{
|
||||
return require_uint256((a + b) / 2);
|
||||
}
|
||||
|
||||
function ceilDivSummary(uint256 numerator, uint256 denominator) returns uint256 {
|
||||
require denominator > 0;
|
||||
return require_uint256((numerator + denominator - 1) / denominator);
|
||||
}
|
||||
|
||||
function mulDivSummary(uint256 x, uint256 y, uint256 denominator) returns uint256 {
|
||||
require denominator > 0;
|
||||
return require_uint256((x * y) / denominator);
|
||||
}
|
||||
|
||||
function mulDivSummaryRounding(uint256 x, uint256 y, uint256 denominator, Math.Rounding rounding) returns uint256 {
|
||||
require denominator > 0;
|
||||
if (rounding == Math.Rounding.Up) {
|
||||
return require_uint256(((x * y) + denominator - 1) / denominator);
|
||||
} else {
|
||||
return require_uint256((x * y) / denominator);
|
||||
}
|
||||
}
|
||||
|
|
@ -1,70 +0,0 @@
|
|||
using StakeManager as _stakeManager;
|
||||
|
||||
methods {
|
||||
function StakeManager.accounts(address) external returns(address, uint256, uint256, uint256, uint256, uint256, uint256, uint256) envfree;
|
||||
function Math.mulDiv(uint256 a, uint256 b, uint256 c) internal returns uint256 => mulDivSummary(a, b, c);
|
||||
}
|
||||
|
||||
function mulDivSummary(uint256 a, uint256 b, uint256 c) returns uint256 {
|
||||
require c != 0;
|
||||
return require_uint256(a*b/c);
|
||||
}
|
||||
|
||||
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.acceptUpdate().selector ||
|
||||
f.selector == sig:_stakeManager.leave().selector ||
|
||||
f.selector == sig:_stakeManager.transferNonPending().selector
|
||||
);
|
||||
|
||||
function getAccountBalance(address addr) returns uint256 {
|
||||
uint256 balance;
|
||||
_, balance, _, _, _, _, _, _ = _stakeManager.accounts(addr);
|
||||
|
||||
return balance;
|
||||
}
|
||||
|
||||
function getAccountMaxMultiplierPoints(address addr) returns uint256 {
|
||||
uint256 maxMP;
|
||||
_, _, maxMP, _, _, _, _, _ = _stakeManager.accounts(addr);
|
||||
|
||||
return maxMP;
|
||||
}
|
||||
|
||||
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;
|
||||
}
|
||||
|
||||
function getAccountEpoch(address addr) returns uint256 {
|
||||
uint256 epoch;
|
||||
_, _, _, _, _, _, epoch, _ = _stakeManager.accounts(addr);
|
||||
return epoch;
|
||||
}
|
||||
|
||||
invariant MaxMPIsNeverSmallerThanBalance(address addr)
|
||||
to_mathint(getAccountMaxMultiplierPoints(addr)) >= to_mathint(getAccountBalance(addr))
|
||||
filtered {
|
||||
f -> f.selector != sig:_stakeManager.migrateFrom(address,bool,StakeManager.Account).selector
|
||||
}
|
||||
|
||||
invariant CurrentMPIsNeverSmallerThanBalance(address addr)
|
||||
to_mathint(getAccountCurrentMultiplierPoints(addr)) >= to_mathint(getAccountBalance(addr))
|
||||
filtered {
|
||||
f -> f.selector != sig:_stakeManager.migrateFrom(address,bool,StakeManager.Account).selector
|
||||
}
|
||||
|
||||
|
|
@ -0,0 +1,12 @@
|
|||
// erc20 methods
|
||||
methods {
|
||||
function _.name() external => DISPATCHER(true);
|
||||
function _.symbol() external => DISPATCHER(true);
|
||||
function _.decimals() external => DISPATCHER(true);
|
||||
function _.totalSupply() external => DISPATCHER(true);
|
||||
function _.balanceOf(address) external => DISPATCHER(true);
|
||||
function _.allowance(address,address) external => DISPATCHER(true);
|
||||
function _.approve(address,uint256) external => DISPATCHER(true);
|
||||
function _.transfer(address,uint256) external => DISPATCHER(true);
|
||||
function _.transferFrom(address,address,uint256) external => DISPATCHER(true);
|
||||
}
|
||||
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
|
|
@ -29,7 +29,7 @@
|
|||
"scripts": {
|
||||
"clean": "rm -rf cache out",
|
||||
"lint": "pnpm lint:sol && pnpm prettier:check",
|
||||
"verify": "pnpm verify:stake_vault && pnpm verify:stake_manager && pnpm verify:stake_manager_start_migration && pnpm verify:stake_manager_process",
|
||||
"verify": "pnpm verify:stake_vault && pnpm verify:stake_manager && pnpm verify:stake_manager_start_migration && pnpm verify:stake_manager_process && pnpm verify:max_mp_rule",
|
||||
"lint:sol": "forge fmt --check && pnpm solhint {script,src,test,certora}/**/*.sol",
|
||||
"prettier:check": "prettier --check **/*.{json,md,yml} --ignore-path=.prettierignore",
|
||||
"prettier:write": "prettier --write **/*.{json,md,yml} --ignore-path=.prettierignore",
|
||||
|
|
|
|||
Loading…
Reference in New Issue