mirror of https://github.com/logos-co/staking.git
refactor(certora): introduce shared.spec to reuse helper functions
We have a couple of helper functions redefined in multiple spec files. This commit introduces a `shared.spec` that provides such functions. The file is then imported in other spec files, so we can make use of the functions there. Closes #87
This commit is contained in:
parent
3e5361f9be
commit
40c5be49bc
|
@ -1,4 +1,7 @@
|
|||
import "./shared.spec";
|
||||
|
||||
using ERC20A as staked;
|
||||
|
||||
methods {
|
||||
function staked.balanceOf(address) external returns (uint256) envfree;
|
||||
function totalSupplyBalance() external returns (uint256) envfree;
|
||||
|
@ -17,34 +20,6 @@ function mulDivSummary(uint256 a, uint256 b, uint256 c) returns uint256 {
|
|||
return require_uint256(a*b/c);
|
||||
}
|
||||
|
||||
function getAccountBalance(address addr) returns uint256 {
|
||||
uint256 balance;
|
||||
_, balance, _, _, _, _, _, _ = accounts(addr);
|
||||
|
||||
return balance;
|
||||
}
|
||||
|
||||
function getAccountBonusMultiplierPoints(address addr) returns uint256 {
|
||||
uint256 bonusMP;
|
||||
_, _, bonusMP, _, _, _, _, _ = accounts(addr);
|
||||
|
||||
return bonusMP;
|
||||
}
|
||||
|
||||
function getAccountCurrentMultiplierPoints(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 isMigrationfunction(method f) returns bool {
|
||||
return
|
||||
f.selector == sig:migrateTo(bool).selector ||
|
||||
|
@ -59,17 +34,6 @@ function simplification(env e) {
|
|||
require e.msg.sender != 0;
|
||||
}
|
||||
|
||||
definition requiresPreviousManager(method f) returns bool = (
|
||||
f.selector == sig:migrationInitialize(uint256,uint256,uint256,uint256,uint256,uint256,uint256).selector ||
|
||||
f.selector == sig:migrateFrom(address,bool,StakeManager.Account).selector ||
|
||||
f.selector == sig:increaseTotalMP(uint256).selector
|
||||
);
|
||||
|
||||
definition requiresNextManager(method f) returns bool = (
|
||||
f.selector == sig:migrateTo(bool).selector ||
|
||||
f.selector == sig:transferNonPending().selector
|
||||
);
|
||||
|
||||
ghost mathint sumOfEpochRewards
|
||||
{
|
||||
init_state axiom sumOfEpochRewards == 0;
|
||||
|
|
|
@ -1,4 +1,7 @@
|
|||
import "./shared.spec";
|
||||
|
||||
using ERC20A as staked;
|
||||
|
||||
methods {
|
||||
function staked.balanceOf(address) external returns (uint256) envfree;
|
||||
function totalSupplyBalance() external returns (uint256) envfree;
|
||||
|
@ -20,28 +23,10 @@ function markAccountProccessed(address account, uint256 _limitEpoch) {
|
|||
accountProcessed[account] = to_mathint(_limitEpoch);
|
||||
}
|
||||
|
||||
function getAccountLockUntil(address addr) returns uint256 {
|
||||
uint256 lockUntil;
|
||||
_, _, _, _, _, lockUntil, _, _ = accounts(addr);
|
||||
|
||||
return lockUntil;
|
||||
}
|
||||
|
||||
hook Sstore accounts[KEY address addr].balance uint256 newValue (uint256 oldValue) {
|
||||
balanceChangedInEpoch[addr] = accountProcessed[addr];
|
||||
}
|
||||
|
||||
definition requiresPreviousManager(method f) returns bool = (
|
||||
f.selector == sig:migrationInitialize(uint256,uint256,uint256,uint256,uint256,uint256,uint256).selector ||
|
||||
f.selector == sig:migrateFrom(address,bool,StakeManager.Account).selector ||
|
||||
f.selector == sig:increaseTotalMP(uint256).selector
|
||||
);
|
||||
|
||||
definition requiresNextManager(method f) returns bool = (
|
||||
f.selector == sig:migrateTo(bool).selector ||
|
||||
f.selector == sig:transferNonPending().selector
|
||||
);
|
||||
|
||||
/*
|
||||
If a balance of an account has changed, the account should have been processed up to the `currentEpoch`.
|
||||
This is filtering out most of migration related functions, as those will be vacuous.
|
||||
|
|
|
@ -1,3 +1,5 @@
|
|||
import "./shared.spec";
|
||||
|
||||
using ERC20A as staked;
|
||||
using StakeManagerNew as newStakeManager;
|
||||
|
||||
|
@ -12,21 +14,6 @@ methods {
|
|||
function StakeManagerNew.totalSupplyBalance() external returns (uint256) envfree;
|
||||
}
|
||||
|
||||
|
||||
function getAccountMultiplierPoints(address addr) returns uint256 {
|
||||
uint256 multiplierPoints;
|
||||
_, _, _, multiplierPoints, _, _, _, _ = accounts(addr);
|
||||
|
||||
return multiplierPoints;
|
||||
}
|
||||
|
||||
function getAccountBalance(address addr) returns uint256 {
|
||||
uint256 balance;
|
||||
_, balance, _, _, _, _, _, _ = accounts(addr);
|
||||
|
||||
return balance;
|
||||
}
|
||||
|
||||
definition blockedWhenMigrating(method f) returns bool = (
|
||||
f.selector == sig:stake(uint256, uint256).selector ||
|
||||
f.selector == sig:unstake(uint256).selector ||
|
||||
|
|
|
@ -1,3 +1,5 @@
|
|||
import "./shared.spec";
|
||||
|
||||
using ERC20A as staked;
|
||||
using StakeManager as stakeManager;
|
||||
|
||||
|
@ -17,13 +19,6 @@ function mulDivSummary(uint256 a, uint256 b, uint256 c) returns uint256 {
|
|||
return require_uint256(a*b/c);
|
||||
}
|
||||
|
||||
function getAccountBalance(address addr) returns uint256 {
|
||||
uint256 balance;
|
||||
_, balance, _, _, _, _, _, _ = stakeManager.accounts(addr);
|
||||
|
||||
return balance;
|
||||
}
|
||||
|
||||
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 ||
|
||||
|
|
|
@ -0,0 +1,42 @@
|
|||
using StakeManager as _stakeManager;
|
||||
|
||||
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.migrateTo(bool).selector ||
|
||||
f.selector == sig:_stakeManager.transferNonPending().selector
|
||||
);
|
||||
|
||||
function getAccountBalance(address addr) returns uint256 {
|
||||
uint256 balance;
|
||||
_, balance, _, _, _, _, _, _ = _stakeManager.accounts(addr);
|
||||
|
||||
return balance;
|
||||
}
|
||||
|
||||
function getAccountBonusMultiplierPoints(address addr) returns uint256 {
|
||||
uint256 bonusMP;
|
||||
_, _, bonusMP, _, _, _, _, _ = _stakeManager.accounts(addr);
|
||||
|
||||
return bonusMP;
|
||||
}
|
||||
|
||||
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;
|
||||
}
|
||||
|
||||
|
Loading…
Reference in New Issue