Skip to content

Commit 03bc655

Browse files
3esmit0x-r4bbit
3esmit
authored and
0x-r4bbit
committed
fix: StakeManager migration fixes and certora rules
1 parent 14248a2 commit 03bc655

File tree

9 files changed

+408
-73
lines changed

9 files changed

+408
-73
lines changed

‎.gas-snapshot

Lines changed: 26 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,26 +1,32 @@
11
CreateVaultTest:testDeployment() (gas: 9774)
2-
CreateVaultTest:test_createVault() (gas: 650970)
3-
ExecuteAccountTest:testDeployment() (gas: 26421)
4-
ExecuteAccountTest:test_RevertWhen_InvalidLimitEpoch() (gas: 992511)
5-
LeaveTest:testDeployment() (gas: 26193)
6-
LeaveTest:test_RevertWhen_NoPendingMigration() (gas: 678007)
7-
LeaveTest:test_RevertWhen_SenderIsNotVault() (gas: 10540)
8-
LockTest:testDeployment() (gas: 26421)
9-
LockTest:test_RevertWhen_DecreasingLockTime() (gas: 995651)
10-
LockTest:test_RevertWhen_InvalidLockupPeriod() (gas: 815891)
2+
CreateVaultTest:test_createVault() (gas: 678842)
3+
ExecuteAccountTest:testDeployment() (gas: 26378)
4+
ExecuteAccountTest:test_RevertWhen_InvalidLimitEpoch() (gas: 1021726)
5+
LeaveTest:testDeployment() (gas: 26150)
6+
LeaveTest:test_RevertWhen_NoPendingMigration() (gas: 711549)
7+
LeaveTest:test_RevertWhen_SenderIsNotVault() (gas: 10726)
8+
LockTest:testDeployment() (gas: 26378)
9+
LockTest:test_RevertWhen_DecreasingLockTime() (gas: 1025162)
10+
LockTest:test_RevertWhen_InvalidLockupPeriod() (gas: 846956)
1111
LockTest:test_RevertWhen_SenderIsNotVault() (gas: 10652)
12-
MigrateTest:testDeployment() (gas: 26193)
13-
MigrateTest:test_RevertWhen_NoPendingMigration() (gas: 677868)
14-
MigrateTest:test_RevertWhen_SenderIsNotVault() (gas: 10629)
12+
MigrateTest:testDeployment() (gas: 26150)
13+
MigrateTest:test_RevertWhen_NoPendingMigration() (gas: 706961)
14+
MigrateTest:test_RevertWhen_SenderIsNotVault() (gas: 10726)
1515
SetStakeManagerTest:testDeployment() (gas: 9774)
1616
SetStakeManagerTest:test_RevertWhen_InvalidStakeManagerAddress() (gas: 20481)
1717
SetStakeManagerTest:test_SetStakeManager() (gas: 19869)
18-
StakeManagerTest:testDeployment() (gas: 26193)
19-
StakeTest:testDeployment() (gas: 26421)
20-
StakeTest:test_RevertWhen_InvalidLockupPeriod() (gas: 827181)
21-
StakeTest:test_RevertWhen_SenderIsNotVault() (gas: 10672)
22-
StakedTokenTest:testStakeToken() (gas: 7638)
23-
UnstakeTest:testDeployment() (gas: 26376)
24-
UnstakeTest:test_RevertWhen_FundsLocked() (gas: 991901)
25-
UnstakeTest:test_RevertWhen_SenderIsNotVault() (gas: 10609)
18+
StakeManagerTest:testDeployment() (gas: 26150)
19+
StakeTest:testDeployment() (gas: 26378)
20+
StakeTest:test_RevertWhen_InvalidLockupPeriod() (gas: 860420)
21+
StakeTest:test_RevertWhen_SenderIsNotVault() (gas: 10650)
22+
StakeTest:test_RevertWhen_StakeTokenTransferFails() (gas: 175040)
23+
StakeTest:test_StakeWithoutLockUpTimeMintsMultiplierPoints() (gas: 935199)
24+
StakedTokenTest:testStakeToken() (gas: 7616)
25+
UnstakeTest:testDeployment() (gas: 26400)
26+
UnstakeTest:test_RevertWhen_FundsLocked() (gas: 1021273)
27+
UnstakeTest:test_RevertWhen_SenderIsNotVault() (gas: 10631)
28+
UnstakeTest:test_UnstakeShouldReturnFunds() (gas: 933613)
29+
UserFlowsTest:testDeployment() (gas: 26378)
30+
UserFlowsTest:test_StakeWithLockUpTimeLocksStake() (gas: 1001435)
31+
UserFlowsTest:test_StakedSupplyShouldIncreaseAndDecreaseAgain() (gas: 1797181)
2632
VaultFactoryTest:testDeployment() (gas: 9774)

‎certora/confs/StakeManagerStartMigration.conf

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
{
2+
"files":
3+
[ "contracts/StakeManager.sol",
4+
"certora/harness/StakeManagerNew.sol",
5+
"certora/helpers/ERC20A.sol"
6+
],
7+
"link" : [
8+
"StakeManager:stakedToken=ERC20A"
9+
],
10+
"msg": "Verifying StakeManager.sol",
11+
"rule_sanity": "basic",
12+
"verify": "StakeManager:certora/specs/StakeManagerStartMigration.spec",
13+
"optimistic_loop": true,
14+
"loop_iter": "3",
15+
"packages": [
16+
"@openzeppelin=lib/openzeppelin-contracts"
17+
]
18+
}
19+
20+

‎certora/harness/StakeManagerNew.sol

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
// SPDX-License-Identifier: MIT
2+
3+
pragma solidity ^0.8.19;
4+
5+
import {StakeManager} from "../../contracts/StakeManager.sol";
6+
7+
contract StakeManagerNew is StakeManager {
8+
constructor(address token, address oldManager) StakeManager(token, oldManager) {}
9+
}

‎certora/specs/StakeManager.spec

Lines changed: 104 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,34 @@
11
using ERC20A as staked;
22
methods {
33
function staked.balanceOf(address) external returns (uint256) envfree;
4+
function stakeSupply() external returns (uint256) envfree;
5+
function multiplierSupply() external returns (uint256) envfree;
6+
function oldManager() external returns (address) envfree;
7+
function _.migrateFrom(address, bool, StakeManager.Account) external => NONDET;
8+
function _.increaseMPFromMigration(uint256) external => NONDET;
9+
function _.migrationInitialize(uint256,uint256,uint256,uint256) external => NONDET;
10+
11+
function accounts(address) external returns(uint256, uint256, uint256, uint256, uint256, address) envfree;
12+
}
13+
14+
function getAccountMultiplierPoints(address addr) returns uint256 {
15+
uint256 multiplierPoints;
16+
_, _, multiplierPoints, _, _, _ = accounts(addr);
17+
18+
return multiplierPoints;
19+
}
20+
21+
function getAccountBalance(address addr) returns uint256 {
22+
uint256 balance;
23+
_, balance, _, _, _, _ = accounts(addr);
24+
25+
return balance;
426
}
527

628
function isMigrationfunction(method f) returns bool {
7-
return f.selector == sig:leave().selector ||
8-
f.selector == sig:migrate(address,StakeManager.Account).selector ||
9-
f.selector == sig:migrate().selector;
29+
return
30+
f.selector == sig:migrateFrom(address,bool,StakeManager.Account).selector ||
31+
f.selector == sig:migrateTo(bool).selector;
1032
}
1133

1234
/* assume that migration is zero, causing the verification to take into account only
@@ -15,6 +37,52 @@ function simplification() {
1537
require currentContract.migration == 0;
1638
}
1739

40+
ghost mathint sumOfEpochRewards
41+
{
42+
init_state axiom sumOfEpochRewards == 0;
43+
}
44+
45+
ghost mathint sumOfBalances { /* sigma account[u].balance forall u */
46+
init_state axiom sumOfBalances == 0;
47+
}
48+
49+
ghost mathint sumOfMultipliers /* sigma account[u].multiplier forall u */
50+
{
51+
init_state axiom sumOfMultipliers == 0;
52+
}
53+
54+
hook Sstore epochs[KEY uint256 epochId].epochReward uint256 newValue (uint256 oldValue) STORAGE {
55+
sumOfEpochRewards = sumOfEpochRewards - oldValue + newValue;
56+
}
57+
58+
hook Sstore accounts[KEY address addr].balance uint256 newValue (uint256 oldValue) STORAGE {
59+
sumOfBalances = sumOfBalances - oldValue + newValue;
60+
}
61+
62+
hook Sstore accounts[KEY address addr].multiplier uint256 newValue (uint256 oldValue) STORAGE {
63+
sumOfMultipliers = sumOfMultipliers - oldValue + newValue;
64+
}
65+
66+
invariant sumOfBalancesIsStakeSupply()
67+
sumOfBalances == to_mathint(stakeSupply());
68+
69+
invariant sumOfMultipliersIsMultiplierSupply()
70+
sumOfMultipliers == to_mathint(multiplierSupply())
71+
{ preserved with (env e) {
72+
simplification(e);
73+
}
74+
}
75+
76+
invariant sumOfEpochRewardsIsPendingRewards()
77+
sumOfEpochRewards == to_mathint(currentContract.pendingReward)
78+
{ preserved {
79+
requireInvariant highEpochsAreNull(currentContract.currentEpoch);
80+
}
81+
}
82+
83+
invariant highEpochsAreNull(uint256 epochNumber)
84+
epochNumber >= currentContract.currentEpoch => currentContract.epochs[epochNumber].epochReward == 0;
85+
1886

1987
rule reachability(method f)
2088
{
@@ -48,3 +116,36 @@ rule whoChangeERC20Balance( method f ) filtered { f -> f.contract != staked }
48116
f(e,args);
49117
assert before == staked.balanceOf(user);
50118
}
119+
120+
rule epochOnlyIncreases {
121+
method f;
122+
env e;
123+
calldataarg args;
124+
125+
uint256 epochBefore = currentContract.currentEpoch;
126+
127+
f(e, args);
128+
129+
assert currentContract.currentEpoch >= epochBefore;
130+
}
131+
132+
133+
//TODO codehash / isVault
134+
/*
135+
ghost mapping(address => bytes32) codehash;
136+
137+
hook EXTCODEHASH(address a) bytes32 hash {
138+
require hash == codehash[a];
139+
}
140+
141+
rule checksCodeHash(method f) filtered {
142+
f -> requiresVault(f)
143+
} {
144+
env e;
145+
146+
bool isWhitelisted = isVault(codehash[e.msg.sender]);
147+
f(e);
148+
149+
assert isWhitelisted;
150+
}
151+
*/

‎certora/specs/StakeManagerStartMigration.spec

Lines changed: 130 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,130 @@
1+
using ERC20A as staked;
2+
using StakeManagerNew as newStakeManager;
3+
4+
methods {
5+
function staked.balanceOf(address) external returns (uint256) envfree;
6+
function stakeSupply() external returns (uint256) envfree;
7+
function multiplierSupply() external returns (uint256) envfree;
8+
function oldManager() external returns (address) envfree;
9+
function accounts(address) external returns(uint256, uint256, uint256, uint256, uint256, address) envfree;
10+
11+
function _.migrationInitialize(uint256,uint256,uint256,uint256) external => DISPATCHER(true);
12+
function StakeManagerNew.stakeSupply() external returns (uint256) envfree;
13+
//function _.stakeSupply() external => DISPATCHER(true);
14+
}
15+
16+
17+
function getAccountMultiplierPoints(address addr) returns uint256 {
18+
uint256 multiplierPoints;
19+
_, _, multiplierPoints, _, _, _ = accounts(addr);
20+
21+
return multiplierPoints;
22+
}
23+
24+
function getAccountBalance(address addr) returns uint256 {
25+
uint256 balance;
26+
_, balance, _, _, _, _ = accounts(addr);
27+
28+
return balance;
29+
}
30+
31+
definition blockedWhenMigrating(method f) returns bool = (
32+
f.selector == sig:stake(uint256, uint256).selector ||
33+
f.selector == sig:unstake(uint256).selector ||
34+
f.selector == sig:lock(uint256).selector ||
35+
f.selector == sig:executeEpoch().selector ||
36+
f.selector == sig:startMigration(address).selector
37+
);
38+
39+
definition blockedWhenNotMigrating(method f) returns bool = (
40+
f.selector == sig:migrateTo(bool).selector ||
41+
f.selector == sig:transferNonPending().selector
42+
);
43+
44+
rule rejectWhenMigrating(method f) filtered {
45+
f -> blockedWhenMigrating(f)
46+
} {
47+
calldataarg args;
48+
env e;
49+
50+
require currentContract.migration != 0;
51+
52+
f@withrevert(e, args);
53+
54+
assert lastReverted;
55+
}
56+
57+
rule allowWhenMigrating(method f) filtered {
58+
f -> !blockedWhenMigrating(f)
59+
} {
60+
calldataarg args;
61+
env e;
62+
63+
require currentContract.migration != 0;
64+
65+
f@withrevert(e, args);
66+
67+
satisfy !lastReverted;
68+
}
69+
70+
71+
rule rejectWhenNotMigrating(method f) filtered {
72+
f -> blockedWhenNotMigrating(f)
73+
} {
74+
calldataarg args;
75+
env e;
76+
77+
require currentContract.migration == 0;
78+
79+
f@withrevert(e, args);
80+
81+
assert lastReverted;
82+
}
83+
84+
rule allowWhenNotMigrating(method f) filtered {
85+
f -> !blockedWhenNotMigrating(f)
86+
} {
87+
calldataarg args;
88+
env e;
89+
90+
require currentContract.migration == 0;
91+
92+
f@withrevert(e, args);
93+
94+
satisfy !lastReverted;
95+
}
96+
97+
rule startMigrationCorrect {
98+
env e;
99+
address newContract = newStakeManager;
100+
101+
startMigration(e, newContract);
102+
103+
assert currentContract.migration == newContract;
104+
assert newStakeManager.stakeSupply() == currentContract.stakeSupply();
105+
}
106+
107+
rule migrationLockedIn {
108+
method f;
109+
env e;
110+
calldataarg args;
111+
112+
require currentContract.migration != 0;
113+
114+
f(e, args);
115+
116+
assert currentContract.migration != 0;
117+
}
118+
119+
rule epochStaysSameOnMigration {
120+
method f;
121+
env e;
122+
calldataarg args;
123+
124+
uint256 epochBefore = currentContract.currentEpoch;
125+
require currentContract.migration != 0;
126+
127+
f(e, args);
128+
129+
assert currentContract.currentEpoch == epochBefore;
130+
}

0 commit comments

Comments
 (0)