Skip to content

Commit 1b611a5

Browse files
committed
feat(StakeManager): add Pausable capabilities
1 parent 66ce7a1 commit 1b611a5

File tree

6 files changed

+280
-163
lines changed

6 files changed

+280
-163
lines changed

status-network-contracts/.gas-report

Lines changed: 64 additions & 60 deletions
Large diffs are not rendered by default.

status-network-contracts/.gas-snapshot

Lines changed: 91 additions & 88 deletions
Original file line numberDiff line numberDiff line change
@@ -8,26 +8,26 @@ AddRewardDistributorTest:testRemoveUnknownKarmaDistributor() (gas: 41666)
88
AddRewardDistributorTest:testTotalSupply() (gas: 359391)
99
AddRewardDistributorTest:testTransfersNotAllowed() (gas: 61947)
1010
AddRewardDistributorTest:test_RevertWhen_SenderIsNotDefaultAdmin() (gas: 68406)
11-
EmergencyExitTest:test_CannotEnableEmergencyModeTwice() (gas: 93535)
12-
EmergencyExitTest:test_CannotLeaveBeforeEmergencyMode() (gas: 381899)
13-
EmergencyExitTest:test_EmergencyExitBasic() (gas: 562908)
14-
EmergencyExitTest:test_EmergencyExitMultipleUsers() (gas: 1012077)
15-
EmergencyExitTest:test_EmergencyExitToAlternateAddress() (gas: 517549)
16-
EmergencyExitTest:test_EmergencyExitWithLock() (gas: 468749)
17-
EmergencyExitTest:test_EmergencyExitWithRewards() (gas: 523071)
18-
EmergencyExitTest:test_GuardianCanEnableEmergencyMode() (gas: 61684)
11+
EmergencyExitTest:test_CannotEnableEmergencyModeTwice() (gas: 93544)
12+
EmergencyExitTest:test_CannotLeaveBeforeEmergencyMode() (gas: 384049)
13+
EmergencyExitTest:test_EmergencyExitBasic() (gas: 565128)
14+
EmergencyExitTest:test_EmergencyExitMultipleUsers() (gas: 1016514)
15+
EmergencyExitTest:test_EmergencyExitToAlternateAddress() (gas: 519702)
16+
EmergencyExitTest:test_EmergencyExitWithLock() (gas: 470902)
17+
EmergencyExitTest:test_EmergencyExitWithRewards() (gas: 525291)
18+
EmergencyExitTest:test_GuardianCanEnableEmergencyMode() (gas: 61687)
1919
EmergencyExitTest:test_OnlyOwnerOrGuardianCanEnableEmergencyMode() (gas: 43375)
20-
EmergencyExitTest:test_OwnerCanEnableEmergencyMode() (gas: 63866)
21-
FuzzTests:testFuzz_AccrueMP(uint128,uint64,uint64) (runs: 1000, μ: 601963, ~: 569241)
22-
FuzzTests:testFuzz_AccrueMP_Relock(uint128,uint64,uint64,uint64) (runs: 1000, μ: 826338, ~: 795608)
23-
FuzzTests:testFuzz_EmergencyExit(uint256,uint256) (runs: 1000, μ: 615850, ~: 615759)
24-
FuzzTests:testFuzz_Lock(uint256,uint64) (runs: 1000, μ: 1019480, ~: 1020428)
25-
FuzzTests:testFuzz_Relock(uint256,uint64,uint64) (runs: 1000, μ: 616519, ~: 592696)
26-
FuzzTests:testFuzz_Rewards(uint256,uint256,uint256,uint16,uint16) (runs: 1000, μ: 672169, ~: 674387)
27-
FuzzTests:testFuzz_Stake(uint256,uint64) (runs: 1000, μ: 396388, ~: 366370)
28-
FuzzTests:testFuzz_Unstake(uint128,uint64,uint16,uint128) (runs: 1000, μ: 776860, ~: 752260)
29-
FuzzTests:testFuzz_UpdateVault(uint128,uint64,uint64) (runs: 1000, μ: 601986, ~: 569264)
30-
IntegrationTest:testStakeFoo() (gas: 2454611)
20+
EmergencyExitTest:test_OwnerCanEnableEmergencyMode() (gas: 63869)
21+
FuzzTests:testFuzz_AccrueMP(uint128,uint64,uint64) (runs: 1000, μ: 607780, ~: 573687)
22+
FuzzTests:testFuzz_AccrueMP_Relock(uint128,uint64,uint64,uint64) (runs: 1000, μ: 830402, ~: 802234)
23+
FuzzTests:testFuzz_EmergencyExit(uint256,uint256) (runs: 1000, μ: 618065, ~: 617979)
24+
FuzzTests:testFuzz_Lock(uint256,uint64) (runs: 1000, μ: 1023817, ~: 1024840)
25+
FuzzTests:testFuzz_Relock(uint256,uint64,uint64) (runs: 1000, μ: 621022, ~: 597099)
26+
FuzzTests:testFuzz_Rewards(uint256,uint256,uint256,uint16,uint16) (runs: 1000, μ: 676428, ~: 678665)
27+
FuzzTests:testFuzz_Stake(uint256,uint64) (runs: 1000, μ: 398589, ~: 368610)
28+
FuzzTests:testFuzz_Unstake(uint128,uint64,uint16,uint128) (runs: 1000, μ: 780903, ~: 756749)
29+
FuzzTests:testFuzz_UpdateVault(uint128,uint64,uint64) (runs: 1000, μ: 607803, ~: 573710)
30+
IntegrationTest:testStakeFoo() (gas: 2474610)
3131
KarmaNFTTest:testApproveNotAllowed() (gas: 10507)
3232
KarmaNFTTest:testGetApproved() (gas: 10531)
3333
KarmaNFTTest:testIsApprovedForAll() (gas: 10705)
@@ -65,23 +65,23 @@ KarmaTiersTest:test_Revert_When_TiersNotStartingAtZero() (gas: 37667)
6565
KarmaTiersTest:test_Revert_When_UpdateTiersCalledByNonOwner() (gas: 36642)
6666
KarmaTiersTest:test_Success_When_LastTierIsUnlimited() (gas: 242295)
6767
KarmaTiersTest:test_Success_When_TiersAreContiguous() (gas: 336294)
68-
LeaveTest:test_LeaveShouldKeepFundsLockedInStakeVault() (gas: 10576618)
69-
LeaveTest:test_LeaveShouldProperlyUpdateAccounting() (gas: 10664877)
70-
LockTest:test_LockFailsWithInvalidPeriod(uint256) (runs: 1000, μ: 423703, ~: 423729)
71-
LockTest:test_LockFailsWithNoStake() (gas: 87924)
72-
LockTest:test_LockFailsWithZero() (gas: 385332)
73-
LockTest:test_LockMultipleTimesExceedMaxLock() (gas: 765795)
74-
LockTest:test_LockWithPriorLock() (gas: 698449)
75-
LockTest:test_LockWithoutPriorLock() (gas: 542550)
76-
LockTest:test_RevertWhenVaultToLockIsEmpty() (gas: 87924)
77-
MaliciousUpgradeTest:test_UpgradeStackOverflowStakeManager() (gas: 2581736)
68+
LeaveTest:test_LeaveShouldKeepFundsLockedInStakeVault() (gas: 10810421)
69+
LeaveTest:test_LeaveShouldProperlyUpdateAccounting() (gas: 10898793)
70+
LockTest:test_LockFailsWithInvalidPeriod(uint256) (runs: 1000, μ: 427982, ~: 428007)
71+
LockTest:test_LockFailsWithNoStake() (gas: 90052)
72+
LockTest:test_LockFailsWithZero() (gas: 389610)
73+
LockTest:test_LockMultipleTimesExceedMaxLock() (gas: 774351)
74+
LockTest:test_LockWithPriorLock() (gas: 704855)
75+
LockTest:test_LockWithoutPriorLock() (gas: 546828)
76+
LockTest:test_RevertWhenVaultToLockIsEmpty() (gas: 90052)
77+
MaliciousUpgradeTest:test_UpgradeStackOverflowStakeManager() (gas: 2583931)
7878
MathTest:test_CalcAbsoluteMaxTotalMP() (gas: 5240)
7979
MathTest:test_CalcAccrueMP() (gas: 8599)
80-
MathTest:test_CalcBonusMP() (gas: 30610)
80+
MathTest:test_CalcBonusMP() (gas: 30656)
8181
MathTest:test_CalcInitialMP() (gas: 5836)
8282
MathTest:test_CalcMaxAccruedMP() (gas: 4886)
83-
MathTest:test_CalcMaxTotalMP() (gas: 31372)
84-
MultipleVaultsStakeTest:test_StakeMultipleVaults() (gas: 1041639)
83+
MathTest:test_CalcMaxTotalMP() (gas: 31418)
84+
MultipleVaultsStakeTest:test_StakeMultipleVaults() (gas: 1048134)
8585
NFTMetadataGeneratorSVGTest:testGenerateMetadata() (gas: 92580)
8686
NFTMetadataGeneratorSVGTest:testSetImageStrings() (gas: 77581)
8787
NFTMetadataGeneratorSVGTest:testSetImageStringsRevert() (gas: 35891)
@@ -98,6 +98,9 @@ OverflowTest:testTotalSupply() (gas: 359391)
9898
OverflowTest:testTransfersNotAllowed() (gas: 61925)
9999
OverflowTest:test_RevertWhen_MintingCausesOverflow() (gas: 129592)
100100
OverflowTest:test_RevertWhen_SettingRewardCausesOverflow() (gas: 127920)
101+
PauseTest:test_PauseAndUnpause() (gas: 501645)
102+
PauseTest:test_RevertWhenNotAdmin() (gas: 43335)
103+
PauseTest:test_RevertWhenNotGuardian() (gas: 43380)
101104
RLNTest:test_initial_state() (gas: 45654)
102105
RLNTest:test_register_fails_when_duplicate_identity_commitment() (gas: 131740)
103106
RLNTest:test_register_fails_when_index_exceeds_set_size() (gas: 2313519)
@@ -152,30 +155,30 @@ SlashTest:test_RevertWhen_KarmaBalanceIsInvalid() (gas: 71550)
152155
SlashTest:test_RevertWhen_SenderIsNotDefaultAdminOrSlasher() (gas: 43232)
153156
SlashTest:test_Slash() (gas: 428385)
154157
SlashTest:test_SlashRemainingBalanceIfBalanceIsLow() (gas: 251800)
155-
StakeManager_RewardsTest:testRewardsBalanceOf() (gas: 2798435)
156-
StakeManager_RewardsTest:testSetRewards() (gas: 280257)
157-
StakeManager_RewardsTest:testSetRewardsAccumulatesRemainingRewards() (gas: 388372)
158-
StakeManager_RewardsTest:testSetRewardsAfterPeriodEndedNoAccumulation() (gas: 309095)
159-
StakeManager_RewardsTest:testSetRewardsWithPartialElapsedTime() (gas: 307281)
160-
StakeManager_RewardsTest:testSetRewards_RevertsBadAmount() (gas: 63845)
161-
StakeManager_RewardsTest:testSetRewards_RevertsBadDuration() (gas: 103603)
162-
StakeManager_RewardsTest:testSetRewards_RevertsNotAuthorized() (gas: 41537)
163-
StakeManager_RewardsTest:testTotalRewardsSupply() (gas: 1326087)
164-
StakeTest:test_StakeMultipleAccounts() (gas: 748595)
165-
StakeTest:test_StakeMultipleAccountsAndRewards() (gas: 803496)
166-
StakeTest:test_StakeMultipleAccountsMPIncreasesMaxMPDoesNotChange() (gas: 1406194)
167-
StakeTest:test_StakeMultipleAccountsWithMinLockUp() (gas: 674725)
168-
StakeTest:test_StakeMultipleAccountsWithRandomLockUp() (gas: 683358)
169-
StakeTest:test_StakeMultipleTimesDoesNotExceedsMaxMP() (gas: 1829113)
170-
StakeTest:test_StakeMultipleTimesWithLockIncreaseAtSameBlock() (gas: 715357)
171-
StakeTest:test_StakeMultipleTimesWithLockZeroAfterMaxLock() (gas: 1237445)
172-
StakeTest:test_StakeOneAccount() (gas: 431210)
173-
StakeTest:test_StakeOneAccountAndRewards() (gas: 486174)
174-
StakeTest:test_StakeOneAccountMPIncreasesMaxMPDoesNotChange() (gas: 865966)
175-
StakeTest:test_StakeOneAccountReachingMPLimit() (gas: 755456)
176-
StakeTest:test_StakeOneAccountWithMaxLockUp() (gas: 400384)
177-
StakeTest:test_StakeOneAccountWithMinLockUp() (gas: 400957)
178-
StakeTest:test_StakeOneAccountWithRandomLockUp() (gas: 401002)
158+
StakeManager_RewardsTest:testRewardsBalanceOf() (gas: 2808933)
159+
StakeManager_RewardsTest:testSetRewards() (gas: 282629)
160+
StakeManager_RewardsTest:testSetRewardsAccumulatesRemainingRewards() (gas: 392894)
161+
StakeManager_RewardsTest:testSetRewardsAfterPeriodEndedNoAccumulation() (gas: 313395)
162+
StakeManager_RewardsTest:testSetRewardsWithPartialElapsedTime() (gas: 311581)
163+
StakeManager_RewardsTest:testSetRewards_RevertsBadAmount() (gas: 65995)
164+
StakeManager_RewardsTest:testSetRewards_RevertsBadDuration() (gas: 105753)
165+
StakeManager_RewardsTest:testSetRewards_RevertsNotAuthorized() (gas: 43687)
166+
StakeManager_RewardsTest:testTotalRewardsSupply() (gas: 1332537)
167+
StakeTest:test_StakeMultipleAccounts() (gas: 752962)
168+
StakeTest:test_StakeMultipleAccountsAndRewards() (gas: 807930)
169+
StakeTest:test_StakeMultipleAccountsMPIncreasesMaxMPDoesNotChange() (gas: 1419295)
170+
StakeTest:test_StakeMultipleAccountsWithMinLockUp() (gas: 679115)
171+
StakeTest:test_StakeMultipleAccountsWithRandomLockUp() (gas: 687748)
172+
StakeTest:test_StakeMultipleTimesDoesNotExceedsMaxMP() (gas: 1846313)
173+
StakeTest:test_StakeMultipleTimesWithLockIncreaseAtSameBlock() (gas: 721941)
174+
StakeTest:test_StakeMultipleTimesWithLockZeroAfterMaxLock() (gas: 1250323)
175+
StakeTest:test_StakeOneAccount() (gas: 433427)
176+
StakeTest:test_StakeOneAccountAndRewards() (gas: 488458)
177+
StakeTest:test_StakeOneAccountMPIncreasesMaxMPDoesNotChange() (gas: 876917)
178+
StakeTest:test_StakeOneAccountReachingMPLimit() (gas: 762107)
179+
StakeTest:test_StakeOneAccountWithMaxLockUp() (gas: 402601)
180+
StakeTest:test_StakeOneAccountWithMinLockUp() (gas: 403197)
181+
StakeTest:test_StakeOneAccountWithRandomLockUp() (gas: 403242)
179182
StakeVaultCoverageTest:testOwner() (gas: 15412)
180183
StakeVaultCoverageTest:test_LeaveTransfersAllFunds() (gas: 215757)
181184
StakeVaultCoverageTest:test_StakeRevertsIfNotOwner() (gas: 37215)
@@ -186,42 +189,42 @@ StakeVaultCoverageTest:test_WithdrawOtherTokenTransfersToDestination() (gas: 142
186189
StakeVaultCoverageTest:test_WithdrawRevertsIfInsufficientAvailableBalance() (gas: 167250)
187190
StakeVaultCoverageTest:test_WithdrawRevertsIfInvalidDestination() (gas: 111137)
188191
StakeVaultCoverageTest:test_WithdrawTransfersGenericTokenToOwner() (gas: 139661)
189-
StakeVaultMigrationTest:testMigrateToVault() (gas: 1273180)
190-
StakeVaultMigrationTest:test_RevertWhenDestinationVaultIsNotRegistered() (gas: 268817)
191-
StakeVaultMigrationTest:test_RevertWhenMigrationVaultNotEmpty() (gas: 646944)
192+
StakeVaultMigrationTest:testMigrateToVault() (gas: 1282047)
193+
StakeVaultMigrationTest:test_RevertWhenDestinationVaultIsNotRegistered() (gas: 270967)
194+
StakeVaultMigrationTest:test_RevertWhenMigrationVaultNotEmpty() (gas: 653460)
192195
StakeVaultMigrationTest:test_RevertWhenNotOwnerOfMigrationVault() (gas: 49447)
193196
StakeVaultTest:testOwner() (gas: 15307)
194197
StakingTokenTest:testOwner() (gas: 15307)
195198
StakingTokenTest:testStakeToken() (gas: 13144)
196199
TransferOwnershipTest:testOwner() (gas: 15307)
197200
TransferOwnershipTest:test_RevertWhen_TransferOwnership() (gas: 41429)
198-
TrustedCodehashAccessTest:test_RevertWhenProxyCloneCodehashNotTrusted() (gas: 2131267)
199-
UnstakeTest:test_RevertWhen_FundsLocked() (gas: 460594)
200-
UnstakeTest:test_StakeMultipleAccounts() (gas: 748574)
201-
UnstakeTest:test_StakeMultipleAccountsAndRewards() (gas: 803540)
202-
UnstakeTest:test_StakeMultipleAccountsMPIncreasesMaxMPDoesNotChange() (gas: 1406260)
203-
UnstakeTest:test_StakeMultipleAccountsWithMinLockUp() (gas: 674791)
204-
UnstakeTest:test_StakeMultipleAccountsWithRandomLockUp() (gas: 683357)
205-
UnstakeTest:test_StakeMultipleTimesDoesNotExceedsMaxMP() (gas: 1829169)
206-
UnstakeTest:test_StakeMultipleTimesWithLockIncreaseAtSameBlock() (gas: 715312)
207-
UnstakeTest:test_StakeMultipleTimesWithLockZeroAfterMaxLock() (gas: 1237456)
208-
UnstakeTest:test_StakeOneAccount() (gas: 431232)
209-
UnstakeTest:test_StakeOneAccountAndRewards() (gas: 486173)
210-
UnstakeTest:test_StakeOneAccountMPIncreasesMaxMPDoesNotChange() (gas: 865965)
211-
UnstakeTest:test_StakeOneAccountReachingMPLimit() (gas: 755436)
212-
UnstakeTest:test_StakeOneAccountWithMaxLockUp() (gas: 400406)
213-
UnstakeTest:test_StakeOneAccountWithMinLockUp() (gas: 400957)
214-
UnstakeTest:test_StakeOneAccountWithRandomLockUp() (gas: 401002)
215-
UnstakeTest:test_UnstakeBonusMPAndAccuredMP() (gas: 774353)
216-
UnstakeTest:test_UnstakeMultipleAccounts() (gas: 1112086)
217-
UnstakeTest:test_UnstakeMultipleAccountsAndRewards() (gas: 1398136)
218-
UnstakeTest:test_UnstakeOneAccount() (gas: 801942)
219-
UnstakeTest:test_UnstakeOneAccountAndAccruedMP() (gas: 761419)
220-
UnstakeTest:test_UnstakeOneAccountAndRewards() (gas: 715667)
221-
UnstakeTest:test_UnstakeOneAccountWithLockUpAndAccruedMP() (gas: 741990)
222-
UpdateVaultTest:test_UpdateAccount() (gas: 2681687)
223-
UpgradeTest:test_RevertWhenNotOwner() (gas: 4005864)
224-
UpgradeTest:test_UpgradeStakeManager() (gas: 10494818)
201+
TrustedCodehashAccessTest:test_RevertWhenProxyCloneCodehashNotTrusted() (gas: 2135633)
202+
UnstakeTest:test_RevertWhen_FundsLocked() (gas: 464070)
203+
UnstakeTest:test_StakeMultipleAccounts() (gas: 752941)
204+
UnstakeTest:test_StakeMultipleAccountsAndRewards() (gas: 807974)
205+
UnstakeTest:test_StakeMultipleAccountsMPIncreasesMaxMPDoesNotChange() (gas: 1419361)
206+
UnstakeTest:test_StakeMultipleAccountsWithMinLockUp() (gas: 679181)
207+
UnstakeTest:test_StakeMultipleAccountsWithRandomLockUp() (gas: 687747)
208+
UnstakeTest:test_StakeMultipleTimesDoesNotExceedsMaxMP() (gas: 1846369)
209+
UnstakeTest:test_StakeMultipleTimesWithLockIncreaseAtSameBlock() (gas: 721896)
210+
UnstakeTest:test_StakeMultipleTimesWithLockZeroAfterMaxLock() (gas: 1250334)
211+
UnstakeTest:test_StakeOneAccount() (gas: 433449)
212+
UnstakeTest:test_StakeOneAccountAndRewards() (gas: 488457)
213+
UnstakeTest:test_StakeOneAccountMPIncreasesMaxMPDoesNotChange() (gas: 876916)
214+
UnstakeTest:test_StakeOneAccountReachingMPLimit() (gas: 762087)
215+
UnstakeTest:test_StakeOneAccountWithMaxLockUp() (gas: 402623)
216+
UnstakeTest:test_StakeOneAccountWithMinLockUp() (gas: 403197)
217+
UnstakeTest:test_StakeOneAccountWithRandomLockUp() (gas: 403242)
218+
UnstakeTest:test_UnstakeBonusMPAndAccuredMP() (gas: 780918)
219+
UnstakeTest:test_UnstakeMultipleAccounts() (gas: 1120866)
220+
UnstakeTest:test_UnstakeMultipleAccountsAndRewards() (gas: 1408420)
221+
UnstakeTest:test_UnstakeOneAccount() (gas: 807769)
222+
UnstakeTest:test_UnstakeOneAccountAndAccruedMP() (gas: 768093)
223+
UnstakeTest:test_UnstakeOneAccountAndRewards() (gas: 720191)
224+
UnstakeTest:test_UnstakeOneAccountWithLockUpAndAccruedMP() (gas: 748710)
225+
UpdateVaultTest:test_UpdateAccount() (gas: 2701213)
226+
UpgradeTest:test_RevertWhenNotOwner() (gas: 4126787)
227+
UpgradeTest:test_UpgradeStakeManager() (gas: 10727443)
225228
VaultRegistrationTest:test_VaultRegistration() (gas: 90314)
226-
WithdrawTest:test_RewertWhen_WithdrawingStakedFundsWithoutCallingLeaveFirst() (gas: 458520)
227-
WithdrawTest:test_WithdrawStakedTokensAfterLeave() (gas: 536637)
229+
WithdrawTest:test_RewertWhen_WithdrawingStakedFundsWithoutCallingLeaveFirst() (gas: 460737)
230+
WithdrawTest:test_WithdrawStakedTokensAfterLeave() (gas: 540077)

status-network-contracts/certora/specs/EmergencyMode.spec

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,11 @@ definition isTrustedCodehashAccessFunction(method f) returns bool = (
1515
f.selector == sig:streamer.setTrustedCodehash(bytes32, bool).selector
1616
);
1717

18+
definition isPausableFunction(method f) returns bool = (
19+
f.selector == sig:streamer.pause().selector ||
20+
f.selector == sig:streamer.unpause().selector
21+
);
22+
1823
definition isInitializerFunction(method f) returns bool = (
1924
f.selector == sig:streamer.initialize(address,address).selector
2025
);
@@ -37,9 +42,11 @@ definition noCallDuringEmergency(method f) returns bool = (
3742
|| f.selector == sig:streamer.lock(uint256, uint256).selector
3843
|| f.selector == sig:streamer.setReward(uint256, uint256).selector
3944
|| f.selector == sig:enableEmergencyMode().selector
45+
|| f.selector == sig:pause().selector
46+
|| f.selector == sig:unpause().selector
4047
);
4148

42-
rule accountCanOnlyLeaveInEmergencyMode(method f) {
49+
rule allowedActionsInEmergencyMode(method f) {
4350
env e;
4451
calldataarg args;
4552

@@ -51,6 +58,7 @@ rule accountCanOnlyLeaveInEmergencyMode(method f) {
5158
assert !isReverted => f.selector == sig:streamer.leave().selector ||
5259
f.isView ||
5360
isAccessControlFunction(f) ||
61+
isPausableFunction(f) ||
5462
isTrustedCodehashAccessFunction(f) ||
5563
isInitializerFunction(f) ||
5664
isUUPSUpgradeableFunction(f);

status-network-contracts/certora/specs/StakeManager.spec

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ methods {
1515
function emergencyModeEnabled() external returns (bool) envfree;
1616
function leave() external;
1717
function Math.mulDiv(uint256 a, uint256 b, uint256 c) internal returns uint256 => mulDivSummary(a,b,c);
18+
function paused() external returns (bool) envfree;
1819

1920
function _.migrateFromVault(IStakeVault.MigrationData) external => DISPATCHER(true);
2021
function _.lockUntil() external => DISPATCHER(true);
@@ -124,3 +125,25 @@ rule MPsOnlyDecreaseWhenUnstaking(method f) filtered { f -> f.selector != sig:up
124125

125126
assert totalMPAfter < totalMPBefore => f.selector == sig:unstake(uint256).selector || f.selector == sig:leave().selector;
126127
}
128+
129+
rule allowedActionsWhenPaused(method f) {
130+
env e;
131+
calldataarg args;
132+
133+
require paused();
134+
135+
f@withrevert(e, args);
136+
bool reverted = lastReverted;
137+
138+
assert !reverted => f.isView ||
139+
f.selector == sig:streamer.initialize(address,address).selector ||
140+
f.selector == sig:streamer.upgradeTo(address).selector ||
141+
f.selector == sig:streamer.upgradeToAndCall(address, bytes).selector ||
142+
f.selector == sig:streamer.grantRole(bytes32, address).selector ||
143+
f.selector == sig:streamer.revokeRole(bytes32, address).selector ||
144+
f.selector == sig:streamer.renounceRole(bytes32, address).selector ||
145+
f.selector == sig:streamer.setTrustedCodehash(bytes32, bool).selector ||
146+
f.selector == sig:streamer.__TrustedCodehashAccess_init(address).selector ||
147+
f.selector == sig:streamer.enableEmergencyMode().selector ||
148+
f.selector == sig:streamer.unpause().selector;
149+
}

0 commit comments

Comments
 (0)