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

fix: StakeManager migration fixes and certora rules

This commit is contained in:
Ricardo Guilherme Schmidt 2024-01-24 16:07:23 +01:00 committed by r4bbit
parent a906cdebe2
commit f433dcd628
No known key found for this signature in database
GPG Key ID: E95F1E9447DC91A9
9 changed files with 364 additions and 77 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

46
.gas-snapshot
View File

@ -1,26 +1,32 @@
CreateVaultTest:testDeployment() (gas: 9774)
CreateVaultTest:test_createVault() (gas: 650970)
ExecuteAccountTest:testDeployment() (gas: 26421)
ExecuteAccountTest:test_RevertWhen_InvalidLimitEpoch() (gas: 992511)
LeaveTest:testDeployment() (gas: 26193)
LeaveTest:test_RevertWhen_NoPendingMigration() (gas: 678007)
LeaveTest:test_RevertWhen_SenderIsNotVault() (gas: 10540)
LockTest:testDeployment() (gas: 26421)
LockTest:test_RevertWhen_DecreasingLockTime() (gas: 995651)
LockTest:test_RevertWhen_InvalidLockupPeriod() (gas: 815891)
CreateVaultTest:test_createVault() (gas: 678842)
ExecuteAccountTest:testDeployment() (gas: 26378)
ExecuteAccountTest:test_RevertWhen_InvalidLimitEpoch() (gas: 1021726)
LeaveTest:testDeployment() (gas: 26150)
LeaveTest:test_RevertWhen_NoPendingMigration() (gas: 711549)
LeaveTest:test_RevertWhen_SenderIsNotVault() (gas: 10726)
LockTest:testDeployment() (gas: 26378)
LockTest:test_RevertWhen_DecreasingLockTime() (gas: 1025162)
LockTest:test_RevertWhen_InvalidLockupPeriod() (gas: 846956)
LockTest:test_RevertWhen_SenderIsNotVault() (gas: 10652)
MigrateTest:testDeployment() (gas: 26193)
MigrateTest:test_RevertWhen_NoPendingMigration() (gas: 677868)
MigrateTest:test_RevertWhen_SenderIsNotVault() (gas: 10629)
MigrateTest:testDeployment() (gas: 26150)
MigrateTest:test_RevertWhen_NoPendingMigration() (gas: 706961)
MigrateTest:test_RevertWhen_SenderIsNotVault() (gas: 10726)
SetStakeManagerTest:testDeployment() (gas: 9774)
SetStakeManagerTest:test_RevertWhen_InvalidStakeManagerAddress() (gas: 20481)
SetStakeManagerTest:test_SetStakeManager() (gas: 19869)
StakeManagerTest:testDeployment() (gas: 26193)
StakeTest:testDeployment() (gas: 26421)
StakeTest:test_RevertWhen_InvalidLockupPeriod() (gas: 827181)
StakeTest:test_RevertWhen_SenderIsNotVault() (gas: 10672)
StakedTokenTest:testStakeToken() (gas: 7638)
UnstakeTest:testDeployment() (gas: 26376)
UnstakeTest:test_RevertWhen_FundsLocked() (gas: 991901)
UnstakeTest:test_RevertWhen_SenderIsNotVault() (gas: 10609)
StakeManagerTest:testDeployment() (gas: 26150)
StakeTest:testDeployment() (gas: 26378)
StakeTest:test_RevertWhen_InvalidLockupPeriod() (gas: 860420)
StakeTest:test_RevertWhen_SenderIsNotVault() (gas: 10650)
StakeTest:test_RevertWhen_StakeTokenTransferFails() (gas: 175040)
StakeTest:test_StakeWithoutLockUpTimeMintsMultiplierPoints() (gas: 935199)
StakedTokenTest:testStakeToken() (gas: 7616)
UnstakeTest:testDeployment() (gas: 26400)
UnstakeTest:test_RevertWhen_FundsLocked() (gas: 1021273)
UnstakeTest:test_RevertWhen_SenderIsNotVault() (gas: 10631)
UnstakeTest:test_UnstakeShouldReturnFunds() (gas: 933613)
UserFlowsTest:testDeployment() (gas: 26378)
UserFlowsTest:test_StakeWithLockUpTimeLocksStake() (gas: 1001435)
UserFlowsTest:test_StakedSupplyShouldIncreaseAndDecreaseAgain() (gas: 1797181)
VaultFactoryTest:testDeployment() (gas: 9774)

20
certora/confs/StakeManagerStartMigration.conf Normal file
View File

@ -0,0 +1,20 @@
{
"files":
[ "contracts/StakeManager.sol",
"certora/harness/StakeManagerNew.sol",
"certora/helpers/ERC20A.sol"
],
"link" : [
"StakeManager:stakedToken=ERC20A"
],
"msg": "Verifying StakeManager.sol",
"rule_sanity": "basic",
"verify": "StakeManager:certora/specs/StakeManagerStartMigration.spec",
"optimistic_loop": true,
"loop_iter": "3",
"packages": [
"@openzeppelin=lib/openzeppelin-contracts"
]
}

9
certora/harness/StakeManagerNew.sol Normal file
View File

@ -0,0 +1,9 @@
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.19;
import {StakeManager} from "../../contracts/StakeManager.sol";
contract StakeManagerNew is StakeManager {
constructor(address token, address oldManager) StakeManager(token, oldManager) {}
}

64
certora/specs/StakeManager.spec
View File

@ -5,7 +5,10 @@ methods {
function stakeSupply() external returns (uint256) envfree;
function multiplierSupply() external returns (uint256) envfree;
function oldManager() external returns (address) envfree;
function _.migrate(address, StakeManager.Account) external => NONDET;
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(uint256, uint256, uint256, uint256, uint256, address) envfree;
}
@ -24,9 +27,9 @@ function getAccountBalance(address addr) returns uint256 {
}
function isMigrationfunction(method f) returns bool {
return f.selector == sig:leave().selector ||
f.selector == sig:migrate(address,StakeManager.Account).selector ||
f.selector == sig:migrate().selector;
return
f.selector == sig:migrateFrom(address,bool,StakeManager.Account).selector ||
f.selector == sig:migrateTo(bool).selector;
}
/* assume that migration is zero, causing the verification to take into account only
@ -37,6 +40,11 @@ function simplification(env e) {
require currentContract.migration == 0;
}
ghost mathint sumOfEpochRewards
{
init_state axiom sumOfEpochRewards == 0;
}
ghost mathint sumOfBalances { /* sigma account[u].balance forall u */
init_state axiom sumOfBalances == 0;
}
@ -46,6 +54,10 @@ ghost mathint sumOfMultipliers /* sigma account[u].multiplier forall u */
init_state axiom sumOfMultipliers == 0;
}
hook Sstore epochs[KEY uint256 epochId].epochReward uint256 newValue (uint256 oldValue) STORAGE {
sumOfEpochRewards = sumOfEpochRewards - oldValue + newValue;
}
hook Sstore accounts[KEY address addr].balance uint256 newValue (uint256 oldValue) STORAGE {
sumOfBalances = sumOfBalances - oldValue + newValue;
}
@ -64,6 +76,17 @@ invariant sumOfMultipliersIsMultiplierSupply()
}
}
invariant sumOfEpochRewardsIsPendingRewards()
sumOfEpochRewards == to_mathint(currentContract.pendingReward)
{ preserved {
requireInvariant highEpochsAreNull(currentContract.currentEpoch);
}
}
invariant highEpochsAreNull(uint256 epochNumber)
epochNumber >= currentContract.currentEpoch => currentContract.epochs[epochNumber].epochReward == 0;
rule reachability(method f)
{
calldataarg args;
@ -138,3 +161,36 @@ rule whoChangeERC20Balance( method f ) filtered { f -> f.contract != staked }
f(e,args);
assert before == staked.balanceOf(user);
}
rule epochOnlyIncreases {
method f;
env e;
calldataarg args;
uint256 epochBefore = currentContract.currentEpoch;
f(e, args);
assert currentContract.currentEpoch >= epochBefore;
}
//TODO codehash / isVault
/*
ghost mapping(address => bytes32) codehash;
hook EXTCODEHASH(address a) bytes32 hash {
require hash == codehash[a];
}
rule checksCodeHash(method f) filtered {
f -> requiresVault(f)
} {
env e;
bool isWhitelisted = isVault(codehash[e.msg.sender]);
f(e);
assert isWhitelisted;
}
*/

130
certora/specs/StakeManagerStartMigration.spec Normal file
View File

@ -0,0 +1,130 @@
using ERC20A as staked;
using StakeManagerNew as newStakeManager;
methods {
function staked.balanceOf(address) external returns (uint256) envfree;
function stakeSupply() external returns (uint256) envfree;
function multiplierSupply() external returns (uint256) envfree;
function oldManager() external returns (address) envfree;
function accounts(address) external returns(uint256, uint256, uint256, uint256, uint256, address) envfree;
function _.migrationInitialize(uint256,uint256,uint256,uint256) external => DISPATCHER(true);
function StakeManagerNew.stakeSupply() external returns (uint256) envfree;
//function _.stakeSupply() external => DISPATCHER(true);
}
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 ||
f.selector == sig:lock(uint256).selector ||
f.selector == sig:executeEpoch().selector ||
f.selector == sig:startMigration(address).selector
);
definition blockedWhenNotMigrating(method f) returns bool = (
f.selector == sig:migrateTo(bool).selector ||
f.selector == sig:transferNonPending().selector
);
rule rejectWhenMigrating(method f) filtered {
f -> blockedWhenMigrating(f)
} {
calldataarg args;
env e;
require currentContract.migration != 0;
f@withrevert(e, args);
assert lastReverted;
}
rule allowWhenMigrating(method f) filtered {
f -> !blockedWhenMigrating(f)
} {
calldataarg args;
env e;
require currentContract.migration != 0;
f@withrevert(e, args);
satisfy !lastReverted;
}
rule rejectWhenNotMigrating(method f) filtered {
f -> blockedWhenNotMigrating(f)
} {
calldataarg args;
env e;
require currentContract.migration == 0;
f@withrevert(e, args);
assert lastReverted;
}
rule allowWhenNotMigrating(method f) filtered {
f -> !blockedWhenNotMigrating(f)
} {
calldataarg args;
env e;
require currentContract.migration == 0;
f@withrevert(e, args);
satisfy !lastReverted;
}
rule startMigrationCorrect {
env e;
address newContract = newStakeManager;
startMigration(e, newContract);
assert currentContract.migration == newContract;
assert newStakeManager.stakeSupply() == currentContract.stakeSupply();
}
rule migrationLockedIn {
method f;
env e;
calldataarg args;
require currentContract.migration != 0;
f(e, args);
assert currentContract.migration != 0;
}
rule epochStaysSameOnMigration {
method f;
env e;
calldataarg args;
uint256 epochBefore = currentContract.currentEpoch;
require currentContract.migration != 0;
f(e, args);
assert currentContract.currentEpoch == epochBefore;
}

152
contracts/StakeManager.sol
View File

@ -57,6 +57,27 @@ contract StakeManager is Ownable {
_;
}
modifier noMigration() {
if (address(migration) != address(0)) {
revert StakeManager__PendingMigration();
}
_;
}
modifier onlyMigration() {
if (address(migration) == address(0)) {
revert StakeManager__NoPendingMigration();
}
_;
}
modifier onlyOldManager() {
if (msg.sender != address(oldManager)) {
revert StakeManager__SenderIsNotPreviousStakeManager();
}
_;
}
constructor(address _stakedToken, address _oldManager) {
epochs[0].startTime = block.timestamp;
oldManager = StakeManager(_oldManager);
@ -70,7 +91,7 @@ contract StakeManager is Ownable {
*
* @dev Reverts when `_time` is not in range of [MIN_LOCKUP_PERIOD, MAX_LOCKUP_PERIOD]
*/
function stake(uint256 _amount, uint256 _time) external onlyVault {
function stake(uint256 _amount, uint256 _time) external onlyVault noMigration {
if (_time > 0 && (_time < MIN_LOCKUP_PERIOD || _time > MAX_LOCKUP_PERIOD)) {
revert StakeManager__InvalidLockupPeriod();
}
@ -86,7 +107,7 @@ contract StakeManager is Ownable {
* Decreases balance of msg.sender;
* @param _amount Amount of balance to be decreased
*/
function unstake(uint256 _amount) external onlyVault {
function unstake(uint256 _amount) external onlyVault noMigration {
Account storage account = accounts[msg.sender];
if (account.lockUntil > block.timestamp) {
revert StakeManager__FundsLocked();
@ -106,7 +127,7 @@ contract StakeManager is Ownable {
* @dev Reverts when `_time` is bigger than `MAX_LOCKUP_PERIOD`
* @dev Reverts when `_time + block.timestamp` is smaller than current lock time.
*/
function lock(uint256 _time) external onlyVault {
function lock(uint256 _time) external onlyVault noMigration {
if (_time > MAX_LOCKUP_PERIOD) {
revert StakeManager__InvalidLockupPeriod();
}
@ -118,23 +139,10 @@ contract StakeManager is Ownable {
mintIntialMultiplier(account, _time, account.balance, 0);
}
/**
* @notice leave without processing account
*/
function leave() external onlyVault {
if (address(migration) == address(0)) {
revert StakeManager__NoPendingMigration();
}
Account memory account = accounts[msg.sender];
delete accounts[msg.sender];
multiplierSupply -= account.multiplier;
stakeSupply -= account.balance;
}
/**
* @notice Release rewards for current epoch and increase epoch.
*/
function executeEpoch() external {
function executeEpoch() external noMigration {
processEpoch();
}
@ -154,21 +162,59 @@ contract StakeManager is Ownable {
function setVault(bytes32 _codehash) external onlyOwner {
isVault[_codehash] = true;
}
/**
* @notice starts migration to new StakeManager
* @param _migration new StakeManager
*/
function startMigration(StakeManager _migration) external onlyOwner noMigration {
processEpoch();
migration = _migration;
stakedToken.transfer(address(migration), epochReward());
migration.migrationInitialize(currentEpoch, multiplierSupply, stakeSupply, epochs[currentEpoch].startTime);
}
/**
* @dev Callable automatically from old StakeManager.startMigration(address)
* @notice Initilizes migration process
* @param _currentEpoch epoch of old manager
* @param _multiplierSupply MP supply on old manager
* @param _stakeSupply stake supply on old manager
* @param _epochStartTime epoch start time of old manager
*/
function migrationInitialize(
uint256 _currentEpoch,
uint256 _multiplierSupply,
uint256 _stakeSupply,
uint256 _epochStartTime
)
external
onlyOldManager
{
currentEpoch = _currentEpoch;
multiplierSupply = _multiplierSupply;
stakeSupply = _stakeSupply;
epochs[currentEpoch].startTime = _epochStartTime;
}
/**
* @notice Transfer current epoch funds for migrated manager
*/
function transferNonPending() external onlyMigration {
stakedToken.transfer(address(migration), epochReward());
}
/**
* @notice Migrate account to new manager.
* @param _acceptMigration true if wants to migrate, false if wants to leave
*/
function migrate() external onlyVault returns (StakeManager newManager) {
if (address(migration) == address(0)) {
revert StakeManager__NoPendingMigration();
}
Account storage account = accounts[msg.sender];
stakedToken.approve(address(migration), account.balance);
migration.migrate(msg.sender, account);
multiplierSupply -= accounts[msg.sender].multiplier;
function migrateTo(bool _acceptMigration) external onlyVault onlyMigration returns (StakeManager newManager) {
processAccount(accounts[msg.sender], currentEpoch);
Account memory account = accounts[msg.sender];
multiplierSupply -= account.multiplier;
stakeSupply -= account.balance;
delete accounts[msg.sender];
migration.migrateFrom(msg.sender, _acceptMigration, account);
return migration;
}
@ -177,13 +223,24 @@ contract StakeManager is Ownable {
* @notice Migrate account from old manager
* @param _vault Account address
* @param _account Account data
* @param _acceptMigration If account should be stored or its MP/balance supply reduced
*/
function migrate(address _vault, Account memory _account) external {
if (msg.sender != address(oldManager)) {
revert StakeManager__SenderIsNotPreviousStakeManager();
function migrateFrom(address _vault, bool _acceptMigration, Account memory _account) external onlyOldManager {
if (_acceptMigration) {
accounts[_vault] = _account;
} else {
multiplierSupply -= _account.multiplier;
stakeSupply -= _account.balance;
}
stakedToken.transferFrom(address(oldManager), address(this), _account.balance);
accounts[_vault] = _account;
}
/**
* @dev Only callable from old manager.
* @notice Increase total MP from old manager
* @param _increasedMP amount MP increased on account after migration initialized
*/
function increaseMPFromMigration(uint256 _increasedMP) external onlyOldManager {
multiplierSupply += _increasedMP;
}
function calcMaxMultiplierIncrease(
@ -207,7 +264,7 @@ contract StakeManager is Ownable {
}
function processEpoch() private {
if (block.timestamp >= epochEnd()) {
if (block.timestamp >= epochEnd() && address(migration) == address(0)) {
//finalize current epoch
epochs[currentEpoch].epochReward = epochReward();
epochs[currentEpoch].totalSupply = totalSupply();
@ -220,38 +277,43 @@ contract StakeManager is Ownable {
function processAccount(Account storage account, uint256 _limitEpoch) private {
processEpoch();
if (address(migration) != address(0)) {
revert StakeManager__PendingMigration();
}
if (_limitEpoch > currentEpoch) {
revert StakeManager__InvalidLimitEpoch();
}
uint256 userReward;
uint256 userEpoch = account.epoch;
for (Epoch memory iEpoch = epochs[userEpoch]; userEpoch < _limitEpoch; userEpoch++) {
for (Epoch storage iEpoch = epochs[userEpoch]; userEpoch < _limitEpoch; userEpoch++) {
//mint multipliers to that epoch
mintMultiplier(account, iEpoch.startTime + EPOCH_SIZE);
mintMultiplier(account, iEpoch.startTime + EPOCH_SIZE, iEpoch);
uint256 userSupply = account.balance + account.multiplier;
uint256 userShare = userSupply / iEpoch.totalSupply; //TODO: might lose precision, multiply by 100 and
// divide back later?
userReward += userShare * iEpoch.epochReward;
uint256 userShare = (userSupply / iEpoch.totalSupply) * 100;
uint256 userEpochReward = (userShare * iEpoch.epochReward) / 100;
userReward += userEpochReward;
iEpoch.epochReward -= userEpochReward;
iEpoch.totalSupply -= userSupply;
}
account.epoch = userEpoch;
if (userReward > 0) {
pendingReward -= userReward;
stakedToken.transfer(account.rewardAddress, userReward);
}
mintMultiplier(account, block.timestamp);
if (userEpoch == currentEpoch && address(migration) == address(0)) {
mintMultiplier(account, block.timestamp, epochs[currentEpoch]);
}
}
function mintMultiplier(Account storage account, uint256 processTime) private {
function mintMultiplier(Account storage account, uint256 processTime, Epoch storage epoch) private {
uint256 deltaTime = processTime - account.lastMint;
account.lastMint = processTime;
uint256 increasedMultiplier = calcMaxMultiplierIncrease(
account.balance * (MP_APY / YEAR * deltaTime), account.multiplier, account.lockUntil, account.balance
account.balance * ((MP_APY / YEAR) * deltaTime), account.multiplier, account.lockUntil, account.balance
);
account.multiplier += increasedMultiplier;
multiplierSupply += increasedMultiplier;
epoch.totalSupply += increasedMultiplier;
if (address(migration) != address(0)) {
migration.increaseMPFromMigration(increasedMultiplier);
}
}
function mintIntialMultiplier(

6
contracts/StakeVault.sol
View File

@ -53,15 +53,15 @@ contract StakeVault is Ownable {
}
function leave() external onlyOwner {
stakeManager.leave();
stakeManager.migrateTo(false);
STAKED_TOKEN.transferFrom(address(this), msg.sender, STAKED_TOKEN.balanceOf(address(this)));
}
/**
* @notice Opt-in migration to a new StakeManager contract.
*/
function updateManager() external onlyOwner {
StakeManager migrated = stakeManager.migrate();
function acceptMigration() external onlyOwner {
StakeManager migrated = stakeManager.migrateTo(true);
if (address(migrated) == address(0)) revert StakeVault__MigrationNotAvailable();
stakeManager = migrated;
}

5
package.json
View File

@ -20,11 +20,12 @@
"scripts": {
"clean": "rm -rf cache out",
"lint": "pnpm lint:sol && pnpm prettier:check",
"verify": "pnpm verify:stake_vault && pnpm verify:stake_manager",
"verify": "pnpm verify:stake_vault && pnpm verify:stake_manager && pnpm verify:stake_manager_start_migration",
"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",
"verify:stake_vault": "certoraRun certora/confs/StakeVault.conf",
"verify:stake_manager": "certoraRun certora/confs/StakeManager.conf"
"verify:stake_manager": "certoraRun certora/confs/StakeManager.conf",
"verify:stake_manager_start_migration": "certoraRun certora/confs/StakeManagerStartMigration.conf"
}
}

9
test/StakeManager.t.sol
View File

@ -194,13 +194,16 @@ contract LeaveTest is StakeManagerTest {
function test_RevertWhen_SenderIsNotVault() public {
vm.expectRevert(StakeManager.StakeManager__SenderIsNotVault.selector);
stakeManager.leave();
stakeManager.migrateTo(false);
}
function test_RevertWhen_NoPendingMigration() public {
StakeVault userVault = _createTestVault(testUser);
vm.prank(testUser);
vm.expectRevert(StakeManager.StakeManager__NoPendingMigration.selector);
userVault.acceptMigration();
vm.prank(testUser);
vm.expectRevert(StakeManager.StakeManager__NoPendingMigration.selector);
userVault.leave();
}
}
@ -212,14 +215,14 @@ contract MigrateTest is StakeManagerTest {
function test_RevertWhen_SenderIsNotVault() public {
vm.expectRevert(StakeManager.StakeManager__SenderIsNotVault.selector);
stakeManager.migrate();
stakeManager.migrateTo(true);
}
function test_RevertWhen_NoPendingMigration() public {
StakeVault userVault = _createTestVault(testUser);
vm.prank(testUser);
vm.expectRevert(StakeManager.StakeManager__NoPendingMigration.selector);
userVault.updateManager();
userVault.acceptMigration();
}
}