forked from lidofinance/dual-governance
-
Notifications
You must be signed in to change notification settings - Fork 2
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Refactor DualGovernanceSetUp into 3 contracts for more fine-grained f…
…unctionality reuse. * KontrolTest has basic helper functions, such as _establish and _storeUInt256, etc. * StorageSetup has the ...StorageSetup functions, refactored to receive the relevant contracts as parameters. * DualGovernanceSetUp has the storage variables for tests of the DualGovernance contract and the setUp function initializing them.
- Loading branch information
Showing
3 changed files
with
200 additions
and
154 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,37 @@ | ||
| pragma solidity 0.8.23; | ||
|
|
||
| import "forge-std/Vm.sol"; | ||
| import "forge-std/Test.sol"; | ||
| import "kontrol-cheatcodes/KontrolCheats.sol"; | ||
|
|
||
| contract KontrolTest is Test, KontrolCheats { | ||
| // Note: there are lemmas dependent on `ethUpperBound` | ||
| uint256 constant ethMaxWidth = 96; | ||
| uint256 constant ethUpperBound = 2 ** ethMaxWidth; | ||
| uint256 constant timeUpperBound = 2 ** 40; | ||
|
|
||
| enum Mode { | ||
| Assume, | ||
| Assert | ||
| } | ||
|
|
||
| function _establish(Mode mode, bool condition) internal pure { | ||
| if (mode == Mode.Assume) { | ||
| vm.assume(condition); | ||
| } else { | ||
| assert(condition); | ||
| } | ||
| } | ||
|
|
||
| function _storeBytes32(address contractAddress, uint256 slot, bytes32 value) internal { | ||
| vm.store(contractAddress, bytes32(slot), value); | ||
| } | ||
|
|
||
| function _storeUInt256(address contractAddress, uint256 slot, uint256 value) internal { | ||
| vm.store(contractAddress, bytes32(slot), bytes32(value)); | ||
| } | ||
|
|
||
| function _storeAddress(address contractAddress, uint256 slot, address value) internal { | ||
| vm.store(contractAddress, bytes32(slot), bytes32(uint256(uint160(value)))); | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,131 @@ | ||
| pragma solidity 0.8.23; | ||
|
|
||
| import "contracts/model/DualGovernanceModel.sol"; | ||
| import "contracts/model/EmergencyProtectedTimelockModel.sol"; | ||
| import "contracts/model/EscrowModel.sol"; | ||
| import "contracts/model/StETHModel.sol"; | ||
|
|
||
| import "test/kontrol/KontrolTest.sol"; | ||
|
|
||
| contract StorageSetup is KontrolTest { | ||
| function _stEthStorageSetup(StETHModel _stEth, EscrowModel _escrow) internal { | ||
| kevm.symbolicStorage(address(_stEth)); | ||
| // Slot 0 | ||
| uint256 totalPooledEther = kevm.freshUInt(32); | ||
| vm.assume(0 < totalPooledEther); | ||
| vm.assume(totalPooledEther < ethUpperBound); | ||
| _stEth.setTotalPooledEther(totalPooledEther); | ||
| // Slot 1 | ||
| uint256 totalShares = kevm.freshUInt(32); | ||
| vm.assume(0 < totalShares); | ||
| vm.assume(totalShares < ethUpperBound); | ||
| _stEth.setTotalShares(totalShares); | ||
| // Slot 2 | ||
| uint256 shares = kevm.freshUInt(32); | ||
| vm.assume(shares < totalShares); | ||
| _stEth.setShares(address(_escrow), shares); | ||
| } | ||
|
|
||
| function _dualGovernanceStorageSetup( | ||
| DualGovernanceModel _dualGovernance, | ||
| EmergencyProtectedTimelockModel _timelock, | ||
| StETHModel _stEth, | ||
| EscrowModel _signallingEscrow, | ||
| EscrowModel _rageQuitEscrow | ||
| ) internal { | ||
| kevm.symbolicStorage(address(_dualGovernance)); | ||
| // Slot 0 | ||
| _storeAddress(address(_dualGovernance), 0, address(_timelock)); | ||
| // Slot 1 | ||
| _storeAddress(address(_dualGovernance), 1, address(_signallingEscrow)); | ||
| // Slot 2 | ||
| _storeAddress(address(_dualGovernance), 2, address(_rageQuitEscrow)); | ||
| // Slot 3 | ||
| _storeAddress(address(_dualGovernance), 3, address(_stEth)); | ||
| // Slot 6 | ||
| uint256 lastStateChangeTime = kevm.freshUInt(32); | ||
| vm.assume(lastStateChangeTime <= block.timestamp); | ||
| vm.assume(lastStateChangeTime < timeUpperBound); | ||
| _storeUInt256(address(_dualGovernance), 6, lastStateChangeTime); | ||
| // Slot 7 | ||
| uint256 lastSubStateActivationTime = kevm.freshUInt(32); | ||
| vm.assume(lastSubStateActivationTime <= block.timestamp); | ||
| vm.assume(lastSubStateActivationTime < timeUpperBound); | ||
| _storeUInt256(address(_dualGovernance), 7, lastSubStateActivationTime); | ||
| // Slot 8 | ||
| uint256 lastStateReactivationTime = kevm.freshUInt(32); | ||
| vm.assume(lastStateReactivationTime <= block.timestamp); | ||
| vm.assume(lastStateReactivationTime < timeUpperBound); | ||
| _storeUInt256(address(_dualGovernance), 8, lastStateReactivationTime); | ||
| // Slot 9 | ||
| uint256 lastVetoSignallingTime = kevm.freshUInt(32); | ||
| vm.assume(lastVetoSignallingTime <= block.timestamp); | ||
| vm.assume(lastVetoSignallingTime < timeUpperBound); | ||
| _storeUInt256(address(_dualGovernance), 9, lastVetoSignallingTime); | ||
| // Slot 10 | ||
| uint256 rageQuitSequenceNumber = kevm.freshUInt(32); | ||
| vm.assume(rageQuitSequenceNumber < type(uint256).max); | ||
| _storeUInt256(address(_dualGovernance), 10, rageQuitSequenceNumber); | ||
| // Slot 11 | ||
| uint256 state = kevm.freshUInt(32); | ||
| vm.assume(state <= 4); | ||
| _storeUInt256(address(_dualGovernance), 11, state); | ||
| } | ||
|
|
||
| function _signallingEscrowStorageSetup( | ||
| EscrowModel _signallingEscrow, | ||
| DualGovernanceModel _dualGovernance, | ||
| StETHModel _stEth | ||
| ) internal { | ||
| _escrowStorageSetup( | ||
| _signallingEscrow, | ||
| _dualGovernance, | ||
| _stEth, | ||
| 0 // SignallingEscrow | ||
| ); | ||
|
|
||
| vm.assume(_signallingEscrow.rageQuitExtensionDelayPeriodEnd() == 0); | ||
| } | ||
|
|
||
| function _rageQuitEscrowStorageSetup( | ||
| EscrowModel _rageQuitEscrow, | ||
| DualGovernanceModel _dualGovernance, | ||
| StETHModel _stEth | ||
| ) internal { | ||
| _escrowStorageSetup( | ||
| _rageQuitEscrow, | ||
| _dualGovernance, | ||
| _stEth, | ||
| 1 // RageQuitEscrow | ||
| ); | ||
| } | ||
|
|
||
| function _escrowStorageSetup( | ||
| EscrowModel _escrow, | ||
| DualGovernanceModel _dualGovernance, | ||
| StETHModel _stEth, | ||
| uint8 _currentState | ||
| ) internal { | ||
| kevm.symbolicStorage(address(_escrow)); | ||
| // Slot 0: currentState, dualGovernance | ||
| bytes memory slot_0_abi_encoding = abi.encodePacked(uint88(0), address(_dualGovernance), _currentState); | ||
| bytes32 slot_0_for_storage; | ||
| assembly { | ||
| slot_0_for_storage := mload(add(slot_0_abi_encoding, 0x20)) | ||
| } | ||
| _storeBytes32(address(_escrow), 0, slot_0_for_storage); | ||
| // Slot 1 | ||
| _storeAddress(address(_escrow), 1, address(_stEth)); | ||
| // Slot 3 | ||
| uint256 totalStakedShares = kevm.freshUInt(32); | ||
| vm.assume(totalStakedShares < ethUpperBound); | ||
| _storeUInt256(address(_escrow), 3, totalStakedShares); | ||
| // Slot 5 | ||
| uint256 totalClaimedEthAmount = kevm.freshUInt(32); | ||
| vm.assume(totalClaimedEthAmount <= totalStakedShares); | ||
| _storeUInt256(address(_escrow), 5, totalClaimedEthAmount); | ||
| // Slot 11 | ||
| uint256 rageQUitExtensionDelayPeriodEnd = kevm.freshUInt(32); | ||
| _storeUInt256(address(_escrow), 11, rageQUitExtensionDelayPeriodEnd); | ||
| } | ||
| } |