mirror of
https://github.com/vacp2p/staking-reward-streamer.git
synced 2026-01-09 13:08:03 -05:00
8bebfbc9d2
- BREAKING CHANGE: Updated stake and lock functions in StakeManager to accept an additional parameter for current lock until timestamp. - BREAKING CHANGE: Modified StakeVault to handle the new locking mechanism and removed the old updateLockUntil function. - Adjusted related tests to reflect changes in function signatures and expected behaviors. - Ensured that funds locked checks are properly referenced in tests and contracts.
74 lines
2.6 KiB
Ruby
74 lines
2.6 KiB
Ruby
using StakeManager as streamer;
|
|
using ERC20A as staked;
|
|
|
|
methods {
|
|
function emergencyModeEnabled() external returns (bool) envfree;
|
|
}
|
|
|
|
definition isOwnableFunction(method f) returns bool = (
|
|
f.selector == sig:streamer.renounceOwnership().selector ||
|
|
f.selector == sig:streamer.transferOwnership(address).selector ||
|
|
f.selector == sig:streamer.setReward(uint256, uint256).selector
|
|
);
|
|
|
|
definition isTrustedCodehashAccessFunction(method f) returns bool = (
|
|
f.selector == sig:streamer.setTrustedCodehash(bytes32, bool).selector
|
|
);
|
|
|
|
definition isInitializerFunction(method f) returns bool = (
|
|
f.selector == sig:streamer.initialize(address,address).selector
|
|
);
|
|
|
|
definition isUUPSUpgradeableFunction(method f) returns bool = (
|
|
f.selector == sig:streamer.upgradeTo(address).selector ||
|
|
f.selector == sig:streamer.upgradeToAndCall(address, bytes).selector ||
|
|
f.selector == sig:streamer.__TrustedCodehashAccess_init(address).selector
|
|
);
|
|
|
|
definition noCallDuringEmergency(method f) returns bool = (
|
|
f.selector == sig:streamer.updateGlobalState().selector
|
|
|| f.selector == sig:streamer.setRewardsSupplier(address).selector
|
|
|| f.selector == sig:streamer.registerVault().selector
|
|
|| f.selector == sig:streamer.migrateToVault(address).selector
|
|
|| f.selector == sig:streamer.updateAccount(address).selector
|
|
|| f.selector == sig:streamer.updateVault(address).selector
|
|
|| f.selector == sig:streamer.unstake(uint256).selector
|
|
|| f.selector == sig:streamer.stake(uint256, uint256, uint256).selector
|
|
|| f.selector == sig:streamer.lock(uint256, uint256).selector
|
|
|| f.selector == sig:enableEmergencyMode().selector
|
|
);
|
|
|
|
rule accountCanOnlyLeaveInEmergencyMode(method f) {
|
|
env e;
|
|
calldataarg args;
|
|
|
|
require emergencyModeEnabled() == true;
|
|
|
|
f@withrevert(e, args);
|
|
bool isReverted = lastReverted;
|
|
|
|
assert !isReverted => f.selector == sig:streamer.leave().selector ||
|
|
f.isView ||
|
|
isOwnableFunction(f) ||
|
|
isTrustedCodehashAccessFunction(f) ||
|
|
isInitializerFunction(f) ||
|
|
isUUPSUpgradeableFunction(f);
|
|
}
|
|
|
|
rule cantBeCalledInEmergency(method f)
|
|
{
|
|
env e;
|
|
calldataarg args;
|
|
|
|
bool inEmergencyMode = emergencyModeEnabled();
|
|
|
|
f@withrevert(e, args);
|
|
bool isReverted = lastReverted;
|
|
|
|
assert inEmergencyMode && noCallDuringEmergency(f) => isReverted;
|
|
|
|
satisfy !noCallDuringEmergency(f) => !isReverted && inEmergencyMode;
|
|
}
|
|
|
|
|