diff --git a/.github/workflows/lido-ci.yml b/.github/workflows/lido-ci.yml index 2b4f13ad..6177e939 100644 --- a/.github/workflows/lido-ci.yml +++ b/.github/workflows/lido-ci.yml @@ -1,9 +1,12 @@ --- name: "Test Proofs" on: + workflow_dispatch: push: branches: - develop + - rvdevelop + - tests-on-client-code jobs: test: runs-on: ubuntu-latest @@ -23,10 +26,9 @@ -H "Authorization: Bearer ${{ secrets.RV_COMPUTE_TOKEN }}" \ https://api.github.com/repos/runtimeverification/_kaas_lidofinance_dual-governance/actions/workflows/lido-ci.yml/dispatches \ -d '{ - "ref": "develop", + "ref": "master", "inputs": { "branch_name": "'"${{ github.event.pull_request.head.sha || github.sha }}"'", - "extra_args": "script", "statuses_sha": "'$sha'", "org": "${{ github.repository_owner }}", "repository": "${{ github.event.repository.name }}", diff --git a/contracts/interfaces/IStETH.sol b/contracts/interfaces/IStETH.sol index 764dc145..864fb3ed 100644 --- a/contracts/interfaces/IStETH.sol +++ b/contracts/interfaces/IStETH.sol @@ -9,10 +9,11 @@ interface IStETH is IERC20 { function getPooledEthByShares(uint256 sharesAmount) external view returns (uint256); - function transferShares(address to, uint256 amount) external; + function transferShares(address to, uint256 amount) external returns (uint256); function transferSharesFrom( address _sender, address _recipient, uint256 _sharesAmount ) external returns (uint256); + function sharesOf(address _account) external view returns (uint256); } diff --git a/contracts/libraries/DualGovernanceState.sol b/contracts/libraries/DualGovernanceState.sol index 5b030899..96085b57 100644 --- a/contracts/libraries/DualGovernanceState.sol +++ b/contracts/libraries/DualGovernanceState.sol @@ -2,6 +2,7 @@ pragma solidity 0.8.23; import {Clones} from "@openzeppelin/contracts/proxy/Clones.sol"; +import {Math} from "@openzeppelin/contracts/utils/math/Math.sol"; import {IEscrow} from "../interfaces/IEscrow.sol"; import {ISealable} from "../interfaces/ISealable.sol"; @@ -297,14 +298,14 @@ library DualGovernanceState { DualGovernanceConfig memory config, uint256 rageQuitSupport ) private pure returns (bool) { - return rageQuitSupport > config.firstSealRageQuitSupport; + return rageQuitSupport >= config.firstSealRageQuitSupport; } function _isSecondSealRageQuitSupportCrossed( DualGovernanceConfig memory config, uint256 rageQuitSupport ) private pure returns (bool) { - return rageQuitSupport > config.secondSealRageQuitSupport; + return rageQuitSupport >= config.secondSealRageQuitSupport; } function _isDynamicTimelockMaxDurationPassed( @@ -327,7 +328,17 @@ library DualGovernanceState { Store storage self, DualGovernanceConfig memory config ) private view returns (bool) { - return Timestamps.now() > config.vetoSignallingMinActiveDuration.addTo(self.vetoSignallingReactivationTime); + return Timestamps.now() + > config.vetoSignallingMinActiveDuration.addTo( + Timestamp.wrap( + uint40( + Math.max( + Timestamp.unwrap(self.vetoSignallingActivationTime), + Timestamp.unwrap(self.vetoSignallingReactivationTime) + ) + ) + ) + ); } function _isVetoSignallingDeactivationMaxDurationPassed( @@ -381,15 +392,15 @@ library DualGovernanceState { return Durations.ZERO; } - if (rageQuitSupport >= secondSealRageQuitSupport) { - return dynamicTimelockMaxDuration; + if (rageQuitSupport < secondSealRageQuitSupport) { + return dynamicTimelockMinDuration + + Durations.from( + (rageQuitSupport - firstSealRageQuitSupport) + * (dynamicTimelockMaxDuration - dynamicTimelockMinDuration).toSeconds() + / (secondSealRageQuitSupport - firstSealRageQuitSupport) + ); } - duration_ = dynamicTimelockMinDuration - + Durations.from( - (rageQuitSupport - firstSealRageQuitSupport) - * (dynamicTimelockMaxDuration - dynamicTimelockMinDuration).toSeconds() - / (secondSealRageQuitSupport - firstSealRageQuitSupport) - ); + return dynamicTimelockMaxDuration; } } diff --git a/contracts/libraries/WithdrawalBatchesQueue.sol b/contracts/libraries/WithdrawalBatchesQueue.sol index 6c096be8..1aa2d6b8 100644 --- a/contracts/libraries/WithdrawalBatchesQueue.sol +++ b/contracts/libraries/WithdrawalBatchesQueue.sol @@ -7,17 +7,6 @@ import {SafeCast} from "@openzeppelin/contracts/utils/math/SafeCast.sol"; import {ArrayUtils} from "../utils/arrays.sol"; import {SequentialBatch, SequentialBatches} from "../types/SequentialBatches.sol"; -enum Status { - // The default status of the WithdrawalsBatchesQueue. In the closed state the only action allowed - // to be called is open(), which transfers it into Opened state. - Empty, - // In the Opened state WithdrawalsBatchesQueue allows to add batches into the queue - Opened, - // When the WithdrawalsBatchesQueue enters Filled queue - it's not allowed to add batches and - // only allowed to mark batches claimed - Closed -} - struct QueueIndex { uint32 batchIndex; uint16 valueIndex; @@ -26,6 +15,17 @@ struct QueueIndex { library WithdrawalsBatchesQueue { using SafeCast for uint256; + enum Status { + // The default status of the WithdrawalsBatchesQueue. In the closed state the only action allowed + // to be called is open(), which transfers it into Opened state. + Empty, + // In the Opened state WithdrawalsBatchesQueue allows to add batches into the queue + Opened, + // When the WithdrawalsBatchesQueue enters Filled queue - it's not allowed to add batches and + // only allowed to mark batches claimed + Closed + } + struct State { Status status; QueueIndex lastClaimedUnstETHIdIndex; diff --git a/contracts/model/DualGovernance.sol b/contracts/model/DualGovernanceModel.sol similarity index 87% rename from contracts/model/DualGovernance.sol rename to contracts/model/DualGovernanceModel.sol index c5a192f0..56abc5fc 100644 --- a/contracts/model/DualGovernance.sol +++ b/contracts/model/DualGovernanceModel.sol @@ -3,8 +3,8 @@ pragma solidity ^0.8.0; import "@openzeppelin/contracts/utils/math/Math.sol"; -import "./EmergencyProtectedTimelock.sol"; -import "./Escrow.sol"; +import "./EmergencyProtectedTimelockModel.sol"; +import "./EscrowModel.sol"; /** * @title Dual Governance Mechanism @@ -13,7 +13,7 @@ import "./Escrow.sol"; */ // DualGovernance contract to handle proposal submissions and lifecycle management. -contract DualGovernance { +contract DualGovernanceModel { enum State { Normal, VetoSignalling, @@ -22,13 +22,12 @@ contract DualGovernance { RageQuit } - EmergencyProtectedTimelock public emergencyProtectedTimelock; - Escrow public signallingEscrow; - Escrow public rageQuitEscrow; + EmergencyProtectedTimelockModel public emergencyProtectedTimelock; + EscrowModel public signallingEscrow; + EscrowModel public rageQuitEscrow; address public fakeETH; // State Variables - State public currentState; mapping(address => bool) public proposers; mapping(address => bool) public admin_proposers; uint256 public lastStateChangeTime; @@ -37,6 +36,8 @@ contract DualGovernance { uint256 public lastVetoSignallingTime; uint256 public rageQuitSequenceNumber; + State public currentState; + // Constants uint256 public constant FIRST_SEAL_RAGE_QUIT_SUPPORT = 10 ** 16; // Threshold required for transition from Normal to Veto Signalling state (1%). uint256 public constant SECOND_SEAL_RAGE_QUIT_SUPPORT = 10 ** 17; // Transition to Rage Quit occurs if t - t^S_{act} > DynamicTimelockMaxDuration and R > SecondSealRageQuitSupport (10%). @@ -52,8 +53,8 @@ contract DualGovernance { currentState = State.Normal; lastStateChangeTime = block.timestamp; fakeETH = _fakeETH; - emergencyProtectedTimelock = new EmergencyProtectedTimelock(address(this), emergencyProtectionTimelock); - signallingEscrow = new Escrow(address(this), _fakeETH); + emergencyProtectedTimelock = new EmergencyProtectedTimelockModel(address(this), emergencyProtectionTimelock); + signallingEscrow = new EscrowModel(address(this), _fakeETH); } // Operations @@ -86,7 +87,7 @@ contract DualGovernance { "Proposals can only be scheduled in Normal or Veto Cooldown states." ); if (currentState == State.VetoCooldown) { - (,,, uint256 submissionTime,) = emergencyProtectedTimelock.proposals(proposalId); + (,, uint256 submissionTime,,) = emergencyProtectedTimelock.proposals(proposalId); require( submissionTime < lastVetoSignallingTime, "Proposal submitted after the last time Veto Signalling state was entered." @@ -117,7 +118,7 @@ contract DualGovernance { function calculateDynamicTimelock(uint256 rageQuitSupport) public pure returns (uint256) { if (rageQuitSupport <= FIRST_SEAL_RAGE_QUIT_SUPPORT) { return 0; - } else if (rageQuitSupport < SECOND_SEAL_RAGE_QUIT_SUPPORT) { + } else if (rageQuitSupport <= SECOND_SEAL_RAGE_QUIT_SUPPORT) { return linearInterpolation(rageQuitSupport); } else { return DYNAMIC_TIMELOCK_MAX_DURATION; @@ -132,6 +133,13 @@ contract DualGovernance { function linearInterpolation(uint256 rageQuitSupport) private pure returns (uint256) { uint256 L_min = DYNAMIC_TIMELOCK_MIN_DURATION; uint256 L_max = DYNAMIC_TIMELOCK_MAX_DURATION; + // Assumption: No underflow + require(FIRST_SEAL_RAGE_QUIT_SUPPORT <= rageQuitSupport); + // Assumption: No overflow + require( + ((rageQuitSupport - FIRST_SEAL_RAGE_QUIT_SUPPORT) * (L_max - L_min)) / (L_max - L_min) + == (rageQuitSupport - FIRST_SEAL_RAGE_QUIT_SUPPORT) + ); return L_min + ((rageQuitSupport - FIRST_SEAL_RAGE_QUIT_SUPPORT) * (L_max - L_min)) / (SECOND_SEAL_RAGE_QUIT_SUPPORT - FIRST_SEAL_RAGE_QUIT_SUPPORT); @@ -149,7 +157,7 @@ contract DualGovernance { signallingEscrow.startRageQuit(); rageQuitSequenceNumber++; rageQuitEscrow = signallingEscrow; - signallingEscrow = new Escrow(address(this), fakeETH); + signallingEscrow = new EscrowModel(address(this), fakeETH); } lastStateChangeTime = block.timestamp; @@ -180,6 +188,11 @@ contract DualGovernance { // State Transitions function activateNextState() public { + // Assumption: various time stamps are in the past + require(lastStateChangeTime <= block.timestamp); + require(lastSubStateActivationTime <= block.timestamp); + require(lastStateReactivationTime <= block.timestamp); + uint256 rageQuitSupport = signallingEscrow.getRageQuitSupport(); State previousState; @@ -224,12 +237,14 @@ contract DualGovernance { // Check the conditions for transitioning to RageQuit or Veto Deactivation based on the time elapsed and support level. if ( - block.timestamp - lastStateChangeTime > DYNAMIC_TIMELOCK_MAX_DURATION + block.timestamp != lastStateChangeTime + && block.timestamp - lastStateChangeTime > DYNAMIC_TIMELOCK_MAX_DURATION && rageQuitSupport > SECOND_SEAL_RAGE_QUIT_SUPPORT ) { transitionState(State.RageQuit); } else if ( - block.timestamp - lastStateChangeTime > calculateDynamicTimelock(rageQuitSupport) + block.timestamp != lastStateChangeTime + && block.timestamp - lastStateChangeTime > calculateDynamicTimelock(rageQuitSupport) && block.timestamp - Math.max(lastStateChangeTime, lastStateReactivationTime) > VETO_SIGNALLING_MIN_ACTIVE_DURATION ) { @@ -247,7 +262,8 @@ contract DualGovernance { uint256 elapsed = block.timestamp - lastSubStateActivationTime; // Check the conditions for transitioning to VetoCooldown or back to VetoSignalling if ( - block.timestamp - lastStateChangeTime <= calculateDynamicTimelock(rageQuitSupport) + block.timestamp == lastStateChangeTime + || block.timestamp - lastStateChangeTime <= calculateDynamicTimelock(rageQuitSupport) || rageQuitSupport > SECOND_SEAL_RAGE_QUIT_SUPPORT ) { exitSubState(State.VetoSignalling); @@ -264,7 +280,7 @@ contract DualGovernance { require(currentState == State.VetoCooldown, "Must be in Veto Cooldown state."); // Ensure the Veto Cooldown has lasted for at least the minimum duration. - if (block.timestamp - lastStateChangeTime > VETO_COOLDOWN_DURATION) { + if (block.timestamp != lastStateChangeTime && block.timestamp - lastStateChangeTime > VETO_COOLDOWN_DURATION) { // Depending on the level of rage quit support, transition to Normal or Veto Signalling. if (rageQuitSupport <= FIRST_SEAL_RAGE_QUIT_SUPPORT) { transitionState(State.Normal); @@ -279,7 +295,7 @@ contract DualGovernance { * Checks if withdrawal process is complete, cooldown period expired. * Transitions to VetoCooldown if support has decreased below the threshold; otherwise, transitions to VetoSignalling. */ - function fromRageQuit(uint256 rageQuitSupport) private { + function fromRageQuit(uint256 rageQuitSupport) public { require(currentState == State.RageQuit, "Must be in Rage Quit state."); // Check if the withdrawal process is completed and if the RageQuitExtensionDelay has elapsed diff --git a/contracts/model/EmergencyProtectedTimelock.sol b/contracts/model/EmergencyProtectedTimelockModel.sol similarity index 95% rename from contracts/model/EmergencyProtectedTimelock.sol rename to contracts/model/EmergencyProtectedTimelockModel.sol index f63bd6c9..bb6ac72a 100644 --- a/contracts/model/EmergencyProtectedTimelock.sol +++ b/contracts/model/EmergencyProtectedTimelockModel.sol @@ -26,7 +26,7 @@ struct Proposal { // This contract manages the timelocking of proposals with emergency intervention capabilities. // It provides controls for entering and managing emergency states as well as executing proposals under normal and emergency conditions. -contract EmergencyProtectedTimelock { +contract EmergencyProtectedTimelockModel { // Addresses associated with governance roles and permissions. address public governance; address public emergencyGovernance; @@ -124,11 +124,13 @@ contract EmergencyProtectedTimelock { function cancelAllNonExecutedProposals() public { require(msg.sender == governance, "Caller is not authorized to cancel proposal."); - // Loop through all the proposals stored in the contract. - for (uint256 i = 0; i < nextProposalId; i++) { - // Ensure that only proposals in 'Submitted' or 'Scheduled' status are canceled. - if (proposals[i].status != ProposalStatus.Executed) { - proposals[i].status = ProposalStatus.Canceled; + if (nextProposalId > 0) { + // Loop through all the proposals stored in the contract. + for (uint256 i = 0; i < nextProposalId; i++) { + // Ensure that only proposals in 'Submitted' or 'Scheduled' status are canceled. + if (proposals[i].status != ProposalStatus.Executed) { + proposals[i].status = ProposalStatus.Canceled; + } } } } diff --git a/contracts/model/EscrowModel.sol b/contracts/model/EscrowModel.sol new file mode 100644 index 00000000..f1fa5c06 --- /dev/null +++ b/contracts/model/EscrowModel.sol @@ -0,0 +1,203 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.0; + +import "contracts/model/StETHModel.sol"; + +/** + * Simplified abstract model of the Escrow contract. Includes the following simplifications: + * + * - To make calculations simpler and focus on the core logic, this model uses only + * stETH (and not wstETH and unstETH) to signal support. + * + * - The model does not interact with the WithdrawalQueue, instead only simulates it by + * keeping track of withdrawal requests internally. + * + * - Replaces requestNextWithdrawalBatch and claimNextWithdrawalBatch with simpler non-batch + * requestNextWithdrawal and claimNextWithdrawal functions that process a single request. + */ +contract EscrowModel { + enum State { + SignallingEscrow, + RageQuitEscrow + } + + enum WithdrawalRequestStatus { + Requested, + Finalized, + Claimed + } + + address public dualGovernance; + StETHModel public stEth; + mapping(address => uint256) public shares; + uint256 public totalSharesLocked; + uint256 public totalClaimedEthAmount; + uint256 public totalWithdrawalRequestAmount; + uint256 public withdrawalRequestCount; + bool public lastWithdrawalRequestSubmitted; // Flag indicating the last withdrawal request submitted + uint256 public claimedWithdrawalRequests; + uint256 public totalWithdrawnPostRageQuit; + mapping(address => uint256) public lastLockedTimes; // Track the last time tokens were locked by each user + mapping(uint256 => WithdrawalRequestStatus) public withdrawalRequestStatus; + mapping(uint256 => uint256) public withdrawalRequestAmount; + uint256 public rageQuitExtensionDelayPeriodEnd; + uint256 public rageQuitSequenceNumber; + uint256 public rageQuitEthClaimTimelockStart; + + State public currentState; + + // Constants + uint256 public constant RAGE_QUIT_EXTENSION_DELAY = 7 days; + uint256 public constant RAGE_QUIT_ETH_CLAIM_MIN_TIMELOCK = 60 days; + uint256 public constant RAGE_QUIT_ETH_CLAIM_TIMELOCK_GROWTH_START_SEQ_NUMBER = 2; + uint256 public constant RAGE_QUIT_ETH_CLAIM_TIMELOCK_GROWTH_COEFFS_0 = 0; + uint256 public constant RAGE_QUIT_ETH_CLAIM_TIMELOCK_GROWTH_COEFFS_1 = 1; // Placeholder value + uint256 public constant RAGE_QUIT_ETH_CLAIM_TIMELOCK_GROWTH_COEFFS_2 = 2; // Placeholder value + uint256 public constant SIGNALLING_ESCROW_MIN_LOCK_TIME = 5 hours; // Minimum time that funds must be locked before they can be unlocked + + uint256 public constant MIN_WITHDRAWAL_AMOUNT = 100; + uint256 public constant MAX_WITHDRAWAL_AMOUNT = 1000 * 1e18; + + constructor(address _dualGovernance, address _stEth) { + currentState = State.SignallingEscrow; + dualGovernance = _dualGovernance; + stEth = StETHModel(_stEth); + } + + // Locks a specified amount of tokens. + function lock(uint256 amount) external { + require(currentState == State.SignallingEscrow, "Cannot lock in current state."); + require(amount > 0, "Amount must be greater than zero."); + require(stEth.allowance(msg.sender, address(this)) >= amount, "Need allowance to transfer tokens."); + require(stEth.balanceOf(msg.sender) >= amount, "Not enough balance."); + + stEth.transferFrom(msg.sender, address(this), amount); + uint256 sharesAmount = stEth.getSharesByPooledEth(amount); + shares[msg.sender] += sharesAmount; + totalSharesLocked += sharesAmount; + lastLockedTimes[msg.sender] = block.timestamp; + } + + // Unlocks all of the user's tokens. + function unlock() external { + require(currentState == State.SignallingEscrow, "Cannot unlock in current state."); + require( + block.timestamp >= lastLockedTimes[msg.sender] + SIGNALLING_ESCROW_MIN_LOCK_TIME, "Lock period not expired." + ); + + uint256 sharesAmount = shares[msg.sender]; + + stEth.transferShares(msg.sender, sharesAmount); + shares[msg.sender] = 0; + totalSharesLocked -= sharesAmount; + } + + // Returns total rage quit support as a percentage of the total supply. + function getRageQuitSupport() external view returns (uint256) { + uint256 totalPooledEth = stEth.getPooledEthByShares(totalSharesLocked); + // Assumption: No overflow + unchecked { + require((totalPooledEth * 10 ** 18) / 10 ** 18 == totalPooledEth); + } + return (totalPooledEth * 10 ** 18) / stEth.totalSupply(); + } + + // Transitions the escrow to the RageQuitEscrow state and initiates withdrawal processes. + function startRageQuit() external { + require(msg.sender == dualGovernance, "Only DualGovernance can start rage quit."); + require(currentState == State.SignallingEscrow, "Already in RageQuit or invalid state."); + currentState = State.RageQuitEscrow; + } + + function min(uint256 a, uint256 b) internal pure returns (uint256) { + return a < b ? a : b; + } + + // Initiates a withdrawal request. + function requestNextWithdrawal() external { + require(currentState == State.RageQuitEscrow, "Withdrawal only allowed in RageQuit state."); + uint256 remainingLockedEth = stEth.getPooledEthByShares(totalSharesLocked) - totalWithdrawalRequestAmount; + require(remainingLockedEth >= MIN_WITHDRAWAL_AMOUNT, "Withdrawal requests already concluded."); + + uint256 amount = min(remainingLockedEth, MAX_WITHDRAWAL_AMOUNT); + + withdrawalRequestStatus[withdrawalRequestCount] = WithdrawalRequestStatus.Requested; + withdrawalRequestAmount[withdrawalRequestCount] = amount; + withdrawalRequestCount++; + + totalWithdrawalRequestAmount += amount; + + if (remainingLockedEth - amount < MIN_WITHDRAWAL_AMOUNT) { + lastWithdrawalRequestSubmitted = true; + } + } + + // Claims the ETH associated with a finalized withdrawal request. + function claimNextWithdrawal(uint256 requestId) external { + require(currentState == State.RageQuitEscrow, "Withdrawal only allowed in RageQuit state."); + require( + withdrawalRequestStatus[requestId] == WithdrawalRequestStatus.Finalized, + "Withdrawal request must be finalized and not claimed." + ); + + withdrawalRequestStatus[requestId] = WithdrawalRequestStatus.Claimed; + totalClaimedEthAmount += withdrawalRequestAmount[requestId]; + claimedWithdrawalRequests++; + + if (lastWithdrawalRequestSubmitted && claimedWithdrawalRequests == withdrawalRequestCount) { + rageQuitExtensionDelayPeriodEnd = block.timestamp + RAGE_QUIT_EXTENSION_DELAY; + } + } + + // Check if the RageQuitExtensionDelay has passed since all withdrawals were finalized. + function isRageQuitFinalized() public view returns (bool) { + return currentState == State.RageQuitEscrow && lastWithdrawalRequestSubmitted + && claimedWithdrawalRequests == withdrawalRequestCount && rageQuitExtensionDelayPeriodEnd < block.timestamp; + } + + // Called by the governance to initiate ETH claim timelock. + function startEthClaimTimelock(uint256 _rageQuitSequenceNumber) external { + require(msg.sender == dualGovernance, "Only DualGovernance can start ETH claim timelock."); + + rageQuitSequenceNumber = _rageQuitSequenceNumber; + rageQuitEthClaimTimelockStart = block.timestamp; + } + + // Timelock between exit from Rage Quit state and when stakers are allowed to withdraw funds. + // Quadratic on the rage quit sequence number. + function rageQuitEthClaimTimelock() public view returns (uint256) { + uint256 ethClaimTimelock = RAGE_QUIT_ETH_CLAIM_MIN_TIMELOCK; + + if (rageQuitSequenceNumber >= RAGE_QUIT_ETH_CLAIM_TIMELOCK_GROWTH_START_SEQ_NUMBER) { + uint256 c0 = RAGE_QUIT_ETH_CLAIM_TIMELOCK_GROWTH_COEFFS_0; + uint256 c1 = RAGE_QUIT_ETH_CLAIM_TIMELOCK_GROWTH_COEFFS_1; + uint256 c2 = RAGE_QUIT_ETH_CLAIM_TIMELOCK_GROWTH_COEFFS_2; + + uint256 x = rageQuitSequenceNumber - RAGE_QUIT_ETH_CLAIM_TIMELOCK_GROWTH_START_SEQ_NUMBER; + + ethClaimTimelock += c0 + c1 * x + c2 * (x ** 2); + } + + return ethClaimTimelock; + } + + // Withdraws all locked funds after the RageQuit delay has passed. + function withdraw() public { + require(currentState == State.RageQuitEscrow, "Withdrawal only allowed in RageQuit state."); + require(isRageQuitFinalized(), "Rage quit process not yet finalized."); + require( + rageQuitEthClaimTimelockStart + rageQuitEthClaimTimelock() < block.timestamp, + "Rage quit ETH claim timelock has not elapsed." + ); + uint256 stakedShares = shares[msg.sender]; + require(stakedShares > 0, "No funds to withdraw."); + uint256 totalEth = address(this).balance; // Total ETH held by contract + uint256 amount = stEth.getPooledEthByShares(stakedShares); + require(totalEth >= amount, "Not enough balance."); + + shares[msg.sender] = 0; + + // Transfer ETH equivalent + payable(msg.sender).transfer(amount); + } +} diff --git a/contracts/model/Escrow.sol b/contracts/model/EscrowNonRebasable.sol similarity index 100% rename from contracts/model/Escrow.sol rename to contracts/model/EscrowNonRebasable.sol diff --git a/contracts/model/StETHModel.sol b/contracts/model/StETHModel.sol new file mode 100644 index 00000000..03e287b9 --- /dev/null +++ b/contracts/model/StETHModel.sol @@ -0,0 +1,161 @@ +pragma solidity 0.8.23; + +import "contracts/interfaces/IStETH.sol"; + +contract StETHModel is IStETH { + uint256 private totalPooledEther; + uint256 private totalShares; + mapping(address => uint256) private shares; + mapping(address => mapping(address => uint256)) private allowances; + + uint256 internal constant INFINITE_ALLOWANCE = type(uint256).max; + + function setTotalPooledEther(uint256 _value) external { + // Assumption: totalPooledEther is not zero + require(_value != 0); + totalPooledEther = _value; + } + + function setTotalShares(uint256 _value) external { + // Assumption: totalShares is not zero + require(_value != 0); + totalShares = _value; + } + + function setShares(address _account, uint256 _value) external { + shares[_account] = _value; + } + + function setAllowances(address _owner, address _spender, uint256 _amount) external { + allowances[_owner][_spender] = _amount; + } + + function totalSupply() external view returns (uint256) { + // Assumption: totalPooledEther is not zero + require(totalPooledEther != 0); + return totalPooledEther; + } + + function getTotalPooledEther() external view returns (uint256) { + // Assumption: totalPooledEther is not zero + require(totalPooledEther != 0); + return totalPooledEther; + } + + function balanceOf(address _account) external view returns (uint256) { + return getPooledEthByShares(shares[_account]); + } + + function transfer(address _recipient, uint256 _amount) external returns (bool) { + _transfer(msg.sender, _recipient, _amount); + return true; + } + + function allowance(address _owner, address _spender) external view returns (uint256) { + return allowances[_owner][_spender]; + } + + function approve(address _spender, uint256 _amount) external returns (bool) { + _approve(msg.sender, _spender, _amount); + return true; + } + + function transferFrom(address _sender, address _recipient, uint256 _amount) external returns (bool) { + _spendAllowance(_sender, msg.sender, _amount); + _transfer(_sender, _recipient, _amount); + return true; + } + + function increaseAllowance(address _spender, uint256 _addedValue) external returns (bool) { + _approve(msg.sender, _spender, allowances[msg.sender][_spender] + _addedValue); + return true; + } + + function decreaseAllowance(address _spender, uint256 _subtractedValue) external returns (bool) { + uint256 currentAllowance = allowances[msg.sender][_spender]; + require(currentAllowance >= _subtractedValue, "ALLOWANCE_BELOW_ZERO"); + _approve(msg.sender, _spender, currentAllowance - _subtractedValue); + return true; + } + + function getTotalShares() external view returns (uint256) { + // Assumption: totalShares is not zero + require(totalShares != 0); + return totalShares; + } + + function sharesOf(address _account) external view returns (uint256) { + return shares[_account]; + } + + function getSharesByPooledEth(uint256 _ethAmount) public view returns (uint256) { + // Assumption: totalPooledEther and totalShares are not zero + require(totalPooledEther != 0); + require(totalShares != 0); + // Assumption: no overflow + unchecked { + require((_ethAmount * totalShares) / totalShares == _ethAmount); + } + return _ethAmount * totalShares / totalPooledEther; + } + + function getPooledEthByShares(uint256 _sharesAmount) public view returns (uint256) { + // Assumption: totalPooledEther and totalShares are not zero + require(totalPooledEther != 0); + require(totalShares != 0); + // Assumption: no overflow + unchecked { + require((_sharesAmount * totalPooledEther) / totalPooledEther == _sharesAmount); + } + return _sharesAmount * totalPooledEther / totalShares; + } + + function transferShares(address _recipient, uint256 _sharesAmount) external returns (uint256) { + _transferShares(msg.sender, _recipient, _sharesAmount); + uint256 tokensAmount = getPooledEthByShares(_sharesAmount); + return tokensAmount; + } + + function transferSharesFrom( + address _sender, + address _recipient, + uint256 _sharesAmount + ) external returns (uint256) { + uint256 tokensAmount = getPooledEthByShares(_sharesAmount); + _spendAllowance(_sender, msg.sender, tokensAmount); + _transferShares(_sender, _recipient, _sharesAmount); + return tokensAmount; + } + + function _transfer(address _sender, address _recipient, uint256 _amount) internal { + uint256 _sharesToTransfer = getSharesByPooledEth(_amount); + _transferShares(_sender, _recipient, _sharesToTransfer); + } + + function _approve(address _owner, address _spender, uint256 _amount) internal { + require(_owner != address(0), "APPROVE_FROM_ZERO_ADDR"); + require(_spender != address(0), "APPROVE_TO_ZERO_ADDR"); + + allowances[_owner][_spender] = _amount; + } + + function _spendAllowance(address _owner, address _spender, uint256 _amount) internal { + uint256 currentAllowance = allowances[_owner][_spender]; + if (currentAllowance != INFINITE_ALLOWANCE) { + require(currentAllowance >= _amount, "ALLOWANCE_EXCEEDED"); + _approve(_owner, _spender, currentAllowance - _amount); + } + } + + function _transferShares(address _sender, address _recipient, uint256 _sharesAmount) internal { + require(_sender != address(0), "TRANSFER_FROM_ZERO_ADDR"); + require(_recipient != address(0), "TRANSFER_TO_ZERO_ADDR"); + require(_recipient != address(this), "TRANSFER_TO_STETH_CONTRACT"); + + uint256 currentSenderShares = shares[_sender]; + require(_sharesAmount <= currentSenderShares, "BALANCE_EXCEEDED"); + + shares[_sender] = currentSenderShares - _sharesAmount; + shares[_recipient] = shares[_recipient] + _sharesAmount; + } +} diff --git a/contracts/model/WithdrawalQueueModel.sol b/contracts/model/WithdrawalQueueModel.sol new file mode 100644 index 00000000..4ca9591a --- /dev/null +++ b/contracts/model/WithdrawalQueueModel.sol @@ -0,0 +1,12 @@ +pragma solidity 0.8.23; + +contract WithdrawalQueueModel { + uint256 public constant MIN_STETH_WITHDRAWAL_AMOUNT = 100; + uint256 public constant MAX_STETH_WITHDRAWAL_AMOUNT = 1000 * 1e18; + + uint256 _lastFinalizedRequestId; + + function getLastFinalizedRequestId() external view returns (uint256) { + return _lastFinalizedRequestId; + } +} diff --git a/contracts/model/WstETHAdapted.sol b/contracts/model/WstETHAdapted.sol new file mode 100644 index 00000000..e5c59c6f --- /dev/null +++ b/contracts/model/WstETHAdapted.sol @@ -0,0 +1,119 @@ +// SPDX-FileCopyrightText: 2021 Lido + +// SPDX-License-Identifier: GPL-3.0 + +pragma solidity 0.8.23; + +import "@openzeppelin/contracts/token/ERC20/extensions/ERC20Permit.sol"; +import "contracts/interfaces/IStETH.sol"; + +/** + * @title StETH token wrapper with static balances. + * @dev It's an ERC20 token that represents the account's share of the total + * supply of stETH tokens. WstETH token's balance only changes on transfers, + * unlike StETH that is also changed when oracles report staking rewards and + * penalties. It's a "power user" token for DeFi protocols which don't + * support rebasable tokens. + * + * The contract is also a trustless wrapper that accepts stETH tokens and mints + * wstETH in return. Then the user unwraps, the contract burns user's wstETH + * and sends user locked stETH in return. + * + * The contract provides the staking shortcut: user can send ETH with regular + * transfer and get wstETH in return. The contract will send ETH to Lido submit + * method, staking it and wrapping the received stETH. + * + */ +contract WstETHAdapted is ERC20Permit { + IStETH public stETH; + + /** + * @param _stETH address of the StETH token to wrap + */ + constructor(IStETH _stETH) + public + ERC20Permit("Wrapped liquid staked Ether 2.0") + ERC20("Wrapped liquid staked Ether 2.0", "wstETH") + { + stETH = _stETH; + } + + /** + * @notice Exchanges stETH to wstETH + * @param _stETHAmount amount of stETH to wrap in exchange for wstETH + * @dev Requirements: + * - `_stETHAmount` must be non-zero + * - msg.sender must approve at least `_stETHAmount` stETH to this + * contract. + * - msg.sender must have at least `_stETHAmount` of stETH. + * User should first approve _stETHAmount to the WstETH contract + * @return Amount of wstETH user receives after wrap + */ + function wrap(uint256 _stETHAmount) external returns (uint256) { + require(_stETHAmount > 0, "wstETH: can't wrap zero stETH"); + uint256 wstETHAmount = stETH.getSharesByPooledEth(_stETHAmount); + _mint(msg.sender, wstETHAmount); + stETH.transferFrom(msg.sender, address(this), _stETHAmount); + return wstETHAmount; + } + + /** + * @notice Exchanges wstETH to stETH + * @param _wstETHAmount amount of wstETH to uwrap in exchange for stETH + * @dev Requirements: + * - `_wstETHAmount` must be non-zero + * - msg.sender must have at least `_wstETHAmount` wstETH. + * @return Amount of stETH user receives after unwrap + */ + function unwrap(uint256 _wstETHAmount) external returns (uint256) { + require(_wstETHAmount > 0, "wstETH: zero amount unwrap not allowed"); + uint256 stETHAmount = stETH.getPooledEthByShares(_wstETHAmount); + _burn(msg.sender, _wstETHAmount); + stETH.transfer(msg.sender, stETHAmount); + return stETHAmount; + } + + /** + * @notice Shortcut to stake ETH and auto-wrap returned stETH + */ + /* + receive() external payable { + uint256 shares = stETH.submit{value: msg.value}(address(0)); + _mint(msg.sender, shares); + } + */ + + /** + * @notice Get amount of wstETH for a given amount of stETH + * @param _stETHAmount amount of stETH + * @return Amount of wstETH for a given stETH amount + */ + function getWstETHByStETH(uint256 _stETHAmount) external view returns (uint256) { + return stETH.getSharesByPooledEth(_stETHAmount); + } + + /** + * @notice Get amount of stETH for a given amount of wstETH + * @param _wstETHAmount amount of wstETH + * @return Amount of stETH for a given wstETH amount + */ + function getStETHByWstETH(uint256 _wstETHAmount) external view returns (uint256) { + return stETH.getPooledEthByShares(_wstETHAmount); + } + + /** + * @notice Get amount of stETH for a one wstETH + * @return Amount of stETH for 1 wstETH + */ + function stEthPerToken() external view returns (uint256) { + return stETH.getPooledEthByShares(1 ether); + } + + /** + * @notice Get amount of wstETH for a one stETH + * @return Amount of wstETH for a 1 stETH + */ + function tokensPerStEth() external view returns (uint256) { + return stETH.getSharesByPooledEth(1 ether); + } +} diff --git a/foundry.toml b/foundry.toml index 196e3fca..35ca19b5 100644 --- a/foundry.toml +++ b/foundry.toml @@ -6,6 +6,7 @@ test = 'test' cache_path = 'cache_forge' solc-version = "0.8.23" no-match-path = 'test/kontrol/*' +extra_output = ['storageLayout', 'abi'] [profile.kprove] src = 'test/kontrol' diff --git a/kontrol.toml b/kontrol.toml new file mode 100644 index 00000000..dc1f47a0 --- /dev/null +++ b/kontrol.toml @@ -0,0 +1,62 @@ +[build.default] +foundry-project-root = '.' +regen = true +rekompile = true +verbose = true +debug = false +require = 'test/kontrol/lido-lemmas.k' +module-import = 'VetoSignallingTest:LIDO-LEMMAS' +auxiliary-lemmas = true + +[prove.default] +foundry-project-root = '.' +verbose = false +debug = false +max-depth = 100000 +max-iterations = 10000 +reinit = false +cse = false +workers = 1 +max-frontier-parallel = 6 +maintenance-rate = 24 +assume-defined = true +no-log-rewrites = true +kore-rpc-command = 'kore-rpc-booster --no-post-exec-simplify' +failure-information = true +counterexample-information = true +minimize-proofs = false +fail-fast = true +smt-timeout = 64000 +smt-retry-limit = 0 +break-every-step = false +break-on-jumpi = false +break-on-calls = false +break-on-storage = false +break-on-basic-blocks = false +break-on-cheatcodes = false +auto_abstract = true +run-constructor = false +match-test = [ + "RageQuitTest.testRageQuitDuration", + "VetoCooldownTest.testVetoCooldownDuration", + "VetoSignallingTest.testTransitionNormalToVetoSignalling", + "VetoSignallingTest.testVetoSignallingInvariantsHoldInitially", + "VetoSignallingTest.testVetoSignallingInvariantsArePreserved", + "VetoSignallingTest.testDeactivationNotCancelled", + "EscrowAccountingTest.testRageQuitSupport", + "EscrowAccountingTest.testEscrowInvariantsHoldInitially", + "EscrowLockUnlockTest.testLockStEth", + #"EscrowAccountingTest.testUnlockStEth", + #"EscrowOperationsTest.testCannotUnlockBeforeMinLockTime", + #"EscrowOperationsTest.testCannotLockUnlockInRageQuitEscrowState", + #"EscrowOperationsTest.testCannotWithdrawBeforeEthClaimTimelockElapsed", + "ProposalOperationsTest.testOnlyAdminProposersCanCancelProposals", + "ProposalOperationsTest.testCannotProposeInInvalidState", + #"ActivateNextStateTest.testEscrowStateTransition" + ] +# bug-report = disabled by default + +[show.default] +foundry-project-root = '.' +verbose = false +debug = false \ No newline at end of file diff --git a/lib/kontrol-cheatcodes b/lib/kontrol-cheatcodes index 0048278e..a5dd4b0b 160000 --- a/lib/kontrol-cheatcodes +++ b/lib/kontrol-cheatcodes @@ -1 +1 @@ -Subproject commit 0048278ebdfb04f452a448bf1fe19a06205efae3 +Subproject commit a5dd4b0b0f055fc628248d920cac5c9bcad6da4b diff --git a/test/kontrol/ActivateNextState.t.sol b/test/kontrol/ActivateNextState.t.sol new file mode 100644 index 00000000..855aa4e0 --- /dev/null +++ b/test/kontrol/ActivateNextState.t.sol @@ -0,0 +1,155 @@ +pragma solidity 0.8.23; + +import {State} from "contracts/libraries/DualGovernanceState.sol"; + +import "test/kontrol/DualGovernanceSetUp.sol"; + +contract ActivateNextStateMock is StorageSetup { + StorageSetup public immutable STORAGE_SETUP; + address public immutable USER; + + constructor(address storageSetup, address user) { + STORAGE_SETUP = StorageSetup(storageSetup); + USER = user; + } + + function activateNextState() external { + DualGovernance dualGovernance = DualGovernance(address(this)); + Escrow signallingEscrow = Escrow(payable(dualGovernance.getVetoSignallingEscrow())); + Escrow rageQuitEscrow = Escrow(payable(dualGovernance.getRageQuitEscrow())); + + STORAGE_SETUP.dualGovernanceStorageInvariants(Mode.Assert, dualGovernance); + STORAGE_SETUP.escrowStorageInvariants(Mode.Assert, signallingEscrow); + STORAGE_SETUP.signallingEscrowStorageInvariants(Mode.Assert, signallingEscrow); + STORAGE_SETUP.escrowStorageInvariants(Mode.Assert, rageQuitEscrow); + STORAGE_SETUP.rageQuitEscrowStorageInvariants(Mode.Assert, rageQuitEscrow); + + AccountingRecord memory pre = STORAGE_SETUP.saveAccountingRecord(USER, signallingEscrow); + + State initialState = dualGovernance.getCurrentState(); + uint256 rageQuitSupport = signallingEscrow.getRageQuitSupport(); + Timestamp vetoSignallingActivationTime = Timestamp.wrap(_getVetoSignallingActivationTime(dualGovernance)); + IConfiguration config = dualGovernance.CONFIG(); + + IEscrow newSignallingEscrow; + IEscrow newRageQuitEscrow; + + bool transitionToRageQuit = ( + initialState == State.VetoSignalling || initialState == State.VetoSignallingDeactivation + ) && rageQuitSupport > config.SECOND_SEAL_RAGE_QUIT_SUPPORT() + && Timestamps.now() > config.DYNAMIC_TIMELOCK_MAX_DURATION().addTo(vetoSignallingActivationTime); + + if (transitionToRageQuit) { + address escrowMasterCopy = signallingEscrow.MASTER_COPY(); + newSignallingEscrow = IEscrow(Clones.clone(escrowMasterCopy)); + newRageQuitEscrow = signallingEscrow; + } else { + newSignallingEscrow = signallingEscrow; + newRageQuitEscrow = rageQuitEscrow; + } + + STORAGE_SETUP.dualGovernanceInitializeStorage(dualGovernance, newSignallingEscrow, newRageQuitEscrow); + + if (transitionToRageQuit) { + vm.assume(dualGovernance.getCurrentState() == State.RageQuit); + } + + STORAGE_SETUP.signallingEscrowInitializeStorage(newSignallingEscrow, dualGovernance); + STORAGE_SETUP.rageQuitEscrowInitializeStorage(newRageQuitEscrow, dualGovernance); + vm.assume(_getLastAssetsLockTimestamp(signallingEscrow, USER) < timeUpperBound); + + { + uint128 senderLockedShares = uint128(kevm.freshUInt(16)); + vm.assume(senderLockedShares < ethUpperBound); + uint128 senderUnlockedShares = uint128(kevm.freshUInt(16)); + bytes memory slotAbi = abi.encodePacked(uint128(senderUnlockedShares), uint128(senderLockedShares)); + bytes32 slot; + assembly { + slot := mload(add(slotAbi, 0x20)) + } + _storeBytes32( + address(signallingEscrow), + 93842437974268059396725027201531251382101332839645030345425397622830526343272, + slot + ); + } + + AccountingRecord memory post = STORAGE_SETUP.saveAccountingRecord(USER, signallingEscrow); + + STORAGE_SETUP.establishEqualAccountingRecords(Mode.Assume, pre, post); + } +} + +contract ActivateNextStateTest is DualGovernanceSetUp { + function testActivateNextStateTermination() external { + dualGovernance.activateNextState(); + } + + function testActivateNextStateCorrectEscrows() external { + State preState = dualGovernance.getCurrentState(); + + dualGovernance.activateNextState(); + + State postState = dualGovernance.getCurrentState(); + + Escrow newSignallingEscrow = Escrow(payable(dualGovernance.getVetoSignallingEscrow())); + Escrow newRageQuitEscrow = Escrow(payable(dualGovernance.getRageQuitEscrow())); + + if (postState == State.RageQuit && preState != State.RageQuit) { + this.infoAssert(address(newSignallingEscrow) != address(signallingEscrow), "NRQ: NS != OS"); + this.infoAssert(address(newSignallingEscrow) != address(rageQuitEscrow), "NRQ: NS != OR"); + this.infoAssert(address(newRageQuitEscrow) == address(signallingEscrow), "NRQ: NR == OS"); + } else { + this.infoAssert(address(newSignallingEscrow) == address(signallingEscrow), "RQ: NS == OS"); + this.infoAssert(address(newRageQuitEscrow) == address(rageQuitEscrow), "RQ: NR == OR"); + } + } + + function testActivateNextStateInvariants() external { + dualGovernance.activateNextState(); + + Escrow newSignallingEscrow = Escrow(payable(dualGovernance.getVetoSignallingEscrow())); + Escrow newRageQuitEscrow = Escrow(payable(dualGovernance.getRageQuitEscrow())); + + this.dualGovernanceStorageInvariants(Mode.Assert, dualGovernance); + this.escrowStorageInvariants(Mode.Assert, newSignallingEscrow); + this.signallingEscrowStorageInvariants(Mode.Assert, newSignallingEscrow); + this.escrowStorageInvariants(Mode.Assert, newRageQuitEscrow); + this.rageQuitEscrowStorageInvariants(Mode.Assert, newRageQuitEscrow); + } + + function testEscrowStateTransition() public { + State initialState = dualGovernance.getCurrentState(); + + uint256 rageQuitSupport = signallingEscrow.getRageQuitSupport(); + (,, Timestamp vetoSignallingActivationTime,) = dualGovernance.getVetoSignallingState(); + address sender = address(uint160(uint256(keccak256("sender")))); + AccountingRecord memory pre = this.saveAccountingRecord(sender, signallingEscrow); + + dualGovernance.activateNextState(); + + if ( + (initialState == State.VetoSignalling || initialState == State.VetoSignallingDeactivation) + && rageQuitSupport > config.SECOND_SEAL_RAGE_QUIT_SUPPORT() + && Timestamps.now() > config.DYNAMIC_TIMELOCK_MAX_DURATION().addTo(vetoSignallingActivationTime) + ) { + IEscrow newSignallingEscrow = IEscrow(dualGovernance.getVetoSignallingEscrow()); + + assert(dualGovernance.getRageQuitEscrow() == address(signallingEscrow)); + assert(EscrowState(_getCurrentState(signallingEscrow)) == EscrowState.RageQuitEscrow); + this.dualGovernanceStorageInvariants(Mode.Assert, dualGovernance); + this.signallingEscrowStorageInvariants(Mode.Assert, newSignallingEscrow); + this.rageQuitEscrowStorageInvariants(Mode.Assert, signallingEscrow); + } else { + assert(dualGovernance.getVetoSignallingEscrow() == address(signallingEscrow)); + assert(dualGovernance.getRageQuitEscrow() == address(rageQuitEscrow)); + assert(EscrowState(_getCurrentState(signallingEscrow)) == EscrowState.SignallingEscrow); + this.dualGovernanceStorageInvariants(Mode.Assert, dualGovernance); + this.signallingEscrowStorageInvariants(Mode.Assert, signallingEscrow); + this.rageQuitEscrowStorageInvariants(Mode.Assert, rageQuitEscrow); + } + + AccountingRecord memory post = this.saveAccountingRecord(sender, signallingEscrow); + this.establishEqualAccountingRecords(Mode.Assert, pre, post); + } +} diff --git a/test/kontrol/DualGovernanceSetUp.sol b/test/kontrol/DualGovernanceSetUp.sol new file mode 100644 index 00000000..ffce4863 --- /dev/null +++ b/test/kontrol/DualGovernanceSetUp.sol @@ -0,0 +1,92 @@ +pragma solidity 0.8.23; + +import {Clones} from "@openzeppelin/contracts/proxy/Clones.sol"; + +import "contracts/Configuration.sol"; +import "contracts/DualGovernance.sol"; +import "contracts/EmergencyProtectedTimelock.sol"; +import "contracts/Escrow.sol"; +import "contracts/model/StETHModel.sol"; +import "contracts/model/WstETHAdapted.sol"; +import "contracts/model/WithdrawalQueueModel.sol"; + +import "test/kontrol/StorageSetup.sol"; + +contract DualGovernanceSetUp is StorageSetup { + using DualGovernanceState for DualGovernanceState.Store; + + Configuration config; + DualGovernance dualGovernance; + EmergencyProtectedTimelock timelock; + StETHModel stEth; + WstETHAdapted wstEth; + WithdrawalQueueModel withdrawalQueue; + Escrow escrowMasterCopy; + Escrow signallingEscrow; + Escrow rageQuitEscrow; + + function setUp() public { + vm.chainId(1); // Set block.chainid so it's not symbolic + vm.assume(block.timestamp < timeUpperBound); + + stEth = new StETHModel(); + wstEth = new WstETHAdapted(IStETH(stEth)); + withdrawalQueue = new WithdrawalQueueModel(); + + // Placeholder addresses + address adminExecutor = address(uint160(uint256(keccak256("adminExecutor")))); + address emergencyGovernance = address(uint160(uint256(keccak256("emergencyGovernance")))); + address adminProposer = address(uint160(uint256(keccak256("adminProposer")))); + + config = new Configuration(adminExecutor, emergencyGovernance, new address[](0)); + timelock = new EmergencyProtectedTimelock(address(config)); + escrowMasterCopy = new Escrow(address(stEth), address(wstEth), address(withdrawalQueue), address(config)); + dualGovernance = + new DualGovernance(address(config), address(timelock), address(escrowMasterCopy), adminProposer); + signallingEscrow = Escrow(payable(dualGovernance.getVetoSignallingEscrow())); + rageQuitEscrow = Escrow(payable(Clones.clone(address(escrowMasterCopy)))); + + // ?STORAGE + // ?WORD: totalPooledEther + // ?WORD0: totalShares + // ?WORD1: shares[signallingEscrow] + this.stEthStorageSetup(stEth, signallingEscrow); + + // ?STORAGE0 + // ?WORD2: currentState + // ?WORD3: enteredAt + // ?WORD4: vetoSignallingActivationTime + // ?WORD5: vetoSignallingReactivationTime + // ?WORD6: lastAdoptableStaateExitedAt + // ?WORD7: rageQuitRound + this.dualGovernanceInitializeStorage(dualGovernance, signallingEscrow, rageQuitEscrow); + + // ?STORAGE1 + // ?WORD8: lockedShares + // ?WORD9: claimedETH + // ?WORD10: unfinalizedShares + // ?WORD11: finalizedETH + // ?WORD12: batchesQueue + // ?WORD13: rageQuitExtensionDelay + // ?WORD14: rageQuitWithdrawalsTimelock + // ?WORD15: rageQuitTimelockStartedAt + this.signallingEscrowInitializeStorage(signallingEscrow, dualGovernance); + + // ?STORAGE2 + // ?WORD16: lockedShares + // ?WORD17: claimedETH + // ?WORD18: unfinalizedShares + // ?WORD19: finalizedETH + // ?WORD20: batchesQueue + // ?WORD21: rageQuitExtensionDelay + // ?WORD22: rageQuitWithdrawalsTimelock + // ?WORD23: rageQuitTimelockStartedAt + this.rageQuitEscrowInitializeStorage(rageQuitEscrow, dualGovernance); + + // ?STORAGE3 + kevm.symbolicStorage(address(timelock)); + + // ?STORAGE4 + kevm.symbolicStorage(address(withdrawalQueue)); + } +} diff --git a/test/kontrol/EscrowAccounting.t.sol b/test/kontrol/EscrowAccounting.t.sol new file mode 100644 index 00000000..d6611e16 --- /dev/null +++ b/test/kontrol/EscrowAccounting.t.sol @@ -0,0 +1,161 @@ +pragma solidity 0.8.23; + +import "@openzeppelin/contracts/proxy/Clones.sol"; + +import "contracts/Configuration.sol"; +import "contracts/DualGovernance.sol"; +import "contracts/EmergencyProtectedTimelock.sol"; +import "contracts/Escrow.sol"; + +import {addTo, Duration, Durations} from "contracts/types/Duration.sol"; +import {Timestamp, Timestamps} from "contracts/types/Timestamp.sol"; + +import "contracts/model/StETHModel.sol"; +import "contracts/model/WithdrawalQueueModel.sol"; +import "contracts/model/WstETHAdapted.sol"; + +import {EscrowInvariants} from "test/kontrol/EscrowInvariants.sol"; + +contract EscrowAccountingTest is EscrowInvariants { + Configuration config; + StETHModel stEth; + WstETHAdapted wstEth; + WithdrawalQueueModel withdrawalQueue; + Escrow escrow; + + function _setUpInitialState() public { + vm.chainId(1); // Set block.chainid so it's not symbolic + + stEth = new StETHModel(); + wstEth = new WstETHAdapted(IStETH(stEth)); + withdrawalQueue = new WithdrawalQueueModel(); + + // Placeholder addresses + address adminExecutor = address(uint160(uint256(keccak256("adminExecutor")))); + address emergencyGovernance = address(uint160(uint256(keccak256("emergencyGovernance")))); + address dualGovernanceAddress = address(uint160(uint256(keccak256("dualGovernance")))); + + config = new Configuration(adminExecutor, emergencyGovernance, new address[](0)); + + Escrow escrowMasterCopy = new Escrow(address(stEth), address(wstEth), address(withdrawalQueue), address(config)); + escrow = Escrow(payable(Clones.clone(address(escrowMasterCopy)))); + escrow.initialize(dualGovernanceAddress); + + // ?STORAGE + // ?WORD: totalPooledEther + // ?WORD0: totalShares + // ?WORD1: shares[escrow] + this.stEthStorageSetup(stEth, escrow); + } + + function _setUpGenericState() public { + _setUpInitialState(); + + address dualGovernanceAddress = address(uint160(kevm.freshUInt(20))); // ?WORD2 + uint8 currentState = uint8(kevm.freshUInt(1)); // ?WORD3 + vm.assume(currentState < 3); + + // ?STORAGE0 + // ?WORD4: lockedShares + // ?WORD5: claimedETH + // ?WORD6: unfinalizedShares + // ?WORD7: finalizedETH + // ?WORD8: batchesQueue + // ?WORD9: rageQuitExtensionDelay + // ?WORD10: rageQuitWithdrawalsTimelock + // ?WORD11: rageQuitTimelockStartedAt + this.escrowStorageSetup(escrow, DualGovernance(dualGovernanceAddress), EscrowState(currentState)); + } + + function testRageQuitSupport() public { + _setUpGenericState(); + + uint256 totalSharesLocked = escrow.getLockedAssetsTotals().stETHLockedShares; + uint256 unfinalizedShares = totalSharesLocked + escrow.getLockedAssetsTotals().unstETHUnfinalizedShares; + uint256 totalFundsLocked = stEth.getPooledEthByShares(unfinalizedShares); + uint256 finalizedETH = escrow.getLockedAssetsTotals().unstETHFinalizedETH; + uint256 expectedRageQuitSupport = + (totalFundsLocked + finalizedETH) * 1e18 / (stEth.totalSupply() + finalizedETH); + + assert(escrow.getRageQuitSupport() == expectedRageQuitSupport); + } + + function testEscrowInvariantsHoldInitially() public { + _setUpInitialState(); + + // Placeholder address to avoid complications with keccak of symbolic addresses + address sender = address(uint160(uint256(keccak256("sender")))); + this.escrowInvariants(Mode.Assert, escrow); + this.signallingEscrowInvariants(Mode.Assert, escrow); + this.escrowUserInvariants(Mode.Assert, escrow, sender); + } + + function testRequestWithdrawals(uint256 stEthAmount) public { + _setUpGenericState(); + + // Placeholder address to avoid complications with keccak of symbolic addresses + address sender = address(uint160(uint256(keccak256("sender")))); + vm.assume(stEth.sharesOf(sender) < ethUpperBound); + + AccountingRecord memory pre = this.saveAccountingRecord(sender, escrow); + + this.escrowInvariants(Mode.Assume, escrow); + this.escrowUserInvariants(Mode.Assume, escrow, sender); + + // Only request one withdrawal for simplicity + uint256[] memory stEthAmounts = new uint256[](1); + stEthAmounts[0] = stEthAmount; + + vm.startPrank(sender); + escrow.requestWithdrawals(stEthAmounts); + vm.stopPrank(); + + this.escrowInvariants(Mode.Assert, escrow); + this.escrowUserInvariants(Mode.Assert, escrow, sender); + + AccountingRecord memory post = this.saveAccountingRecord(sender, escrow); + assert(post.userSharesLocked == pre.userSharesLocked - stEthAmount); + assert(post.totalSharesLocked == pre.totalSharesLocked - stEthAmount); + assert(post.userLastLockedTime == Timestamps.now()); + assert(post.userUnstEthLockedShares == pre.userUnstEthLockedShares + stEthAmount); + assert(post.unfinalizedShares == pre.unfinalizedShares + stEthAmount); + } + + function testRequestNextWithdrawalsBatch(uint256 maxBatchSize) public { + _setUpGenericState(); + + vm.assume(EscrowState(_getCurrentState(escrow)) == EscrowState.RageQuitEscrow); + vm.assume(maxBatchSize >= config.MIN_WITHDRAWALS_BATCH_SIZE()); + vm.assume(maxBatchSize <= config.MAX_WITHDRAWALS_BATCH_SIZE()); + + this.escrowInvariants(Mode.Assume, escrow); + + escrow.requestNextWithdrawalsBatch(maxBatchSize); + + this.escrowInvariants(Mode.Assert, escrow); + } + + function testClaimNextWithdrawalsBatch() public { + _setUpGenericState(); + + // Placeholder address to avoid complications with keccak of symbolic addresses + address sender = address(uint160(uint256(keccak256("sender")))); + vm.assume(stEth.sharesOf(sender) < ethUpperBound); + + vm.assume(EscrowState(_getCurrentState(escrow)) == EscrowState.RageQuitEscrow); + vm.assume(_getRageQuitTimelockStartedAt(escrow) == 0); + + this.escrowInvariants(Mode.Assume, escrow); + this.escrowUserInvariants(Mode.Assume, escrow, sender); + + // Only claim one unstETH for simplicity + uint256 maxUnstETHIdsCount = 1; + + vm.startPrank(sender); + escrow.claimNextWithdrawalsBatch(maxUnstETHIdsCount); + vm.stopPrank(); + + this.escrowInvariants(Mode.Assert, escrow); + this.escrowUserInvariants(Mode.Assert, escrow, sender); + } +} diff --git a/test/kontrol/EscrowInvariants.sol b/test/kontrol/EscrowInvariants.sol new file mode 100644 index 00000000..3fa77fe1 --- /dev/null +++ b/test/kontrol/EscrowInvariants.sol @@ -0,0 +1,52 @@ +pragma solidity 0.8.23; + +import "contracts/Configuration.sol"; +import "contracts/DualGovernance.sol"; +import "contracts/EmergencyProtectedTimelock.sol"; +import "contracts/Escrow.sol"; + +import {addTo, Duration, Durations} from "contracts/types/Duration.sol"; +import {Timestamp, Timestamps} from "contracts/types/Timestamp.sol"; + +import "contracts/model/StETHModel.sol"; +import "contracts/model/WithdrawalQueueModel.sol"; +import "contracts/model/WstETHAdapted.sol"; + +import {StorageSetup} from "test/kontrol/StorageSetup.sol"; + +contract EscrowInvariants is StorageSetup { + function escrowInvariants(Mode mode, Escrow escrow) external view { + IStETH stEth = escrow.ST_ETH(); + LockedAssetsTotals memory totals = escrow.getLockedAssetsTotals(); + _establish(mode, totals.stETHLockedShares <= stEth.sharesOf(address(escrow))); + // TODO: Adapt to updated code + //_establish(mode, totals.sharesFinalized <= totals.stETHLockedShares); + uint256 totalPooledEther = stEth.getPooledEthByShares(totals.stETHLockedShares); + _establish(mode, totalPooledEther <= stEth.balanceOf(address(escrow))); + // TODO: Adapt to updated code + //_establish(mode, totals.amountFinalized == stEth.getPooledEthByShares(totals.sharesFinalized)); + //_establish(mode, totals.amountFinalized <= totalPooledEther); + //_establish(mode, totals.amountClaimed <= totals.amountFinalized); + EscrowState currentState = EscrowState(_getCurrentState(escrow)); + _establish(mode, 0 < uint8(currentState)); + _establish(mode, uint8(currentState) < 3); + } + + function signallingEscrowInvariants(Mode mode, Escrow escrow) external view { + // TODO: Adapt to updated code + /* + if (_getCurrentState(escrow) == EscrowState.SignallingEscrow) { + LockedAssetsTotals memory totals = escrow.getLockedAssetsTotals(); + _establish(mode, totals.sharesFinalized == 0); + _establish(mode, totals.amountFinalized == 0); + _establish(mode, totals.amountClaimed == 0); + } + */ + } + + function escrowUserInvariants(Mode mode, Escrow escrow, address user) external view { + _establish( + mode, escrow.getVetoerState(user).stETHLockedShares <= escrow.getLockedAssetsTotals().stETHLockedShares + ); + } +} diff --git a/test/kontrol/EscrowLockUnlock.t.sol b/test/kontrol/EscrowLockUnlock.t.sol new file mode 100644 index 00000000..da97341b --- /dev/null +++ b/test/kontrol/EscrowLockUnlock.t.sol @@ -0,0 +1,257 @@ +pragma solidity 0.8.23; + +import {Clones} from "@openzeppelin/contracts/proxy/Clones.sol"; + +import "contracts/Configuration.sol"; +import "contracts/DualGovernance.sol"; +import "contracts/EmergencyProtectedTimelock.sol"; +import "contracts/Escrow.sol"; + +import {addTo, Duration, Durations} from "contracts/types/Duration.sol"; +import {Timestamp, Timestamps} from "contracts/types/Timestamp.sol"; + +import "contracts/model/StETHModel.sol"; +import "contracts/model/WithdrawalQueueModel.sol"; +import "contracts/model/WstETHAdapted.sol"; + +import {StorageSetup} from "test/kontrol/StorageSetup.sol"; +import {DualGovernanceSetUp} from "test/kontrol/DualGovernanceSetUp.sol"; +import {EscrowInvariants} from "test/kontrol/EscrowInvariants.sol"; +import {ActivateNextStateMock} from "test/kontrol/ActivateNextState.t.sol"; + +contract EscrowLockUnlockTest is EscrowInvariants, DualGovernanceSetUp { + function _assumeFreshAddress(address account) internal { + IEscrow escrow = signallingEscrow; + vm.assume(account != address(0)); + vm.assume(account != address(this)); + vm.assume(account != address(vm)); + vm.assume(account != address(kevm)); + vm.assume(account != address(stEth)); + vm.assume(account != address(escrow)); // Important assumption: could potentially violate invariants if violated + + // Keccak injectivity + vm.assume( + keccak256(abi.encodePacked(account, uint256(2))) != keccak256(abi.encodePacked(address(escrow), uint256(2))) + ); + } + + function testLockStEth(uint256 amount) public { + // Placeholder address to avoid complications with keccak of symbolic addresses + address sender = address(uint160(uint256(keccak256("sender")))); + + uint256 senderShares = kevm.freshUInt(32); + vm.assume(senderShares < ethUpperBound); + stEth.setShares(sender, senderShares); + vm.assume(stEth.balanceOf(sender) < ethUpperBound); + + uint256 senderAllowance = kevm.freshUInt(32); + // This assumption means that senderAllowance != INFINITE_ALLOWANCE, + // which doubles the execution effort without any added vaue + vm.assume(senderAllowance < ethUpperBound); + // Hardcoded for "sender" + _storeUInt256( + address(stEth), + 74992941968319547325319283905569341819227548318746972755481050864341498730161, + senderAllowance + ); + + uint128 senderLockedShares = uint128(kevm.freshUInt(16)); + uint128 senderUnlockedShares = uint128(kevm.freshUInt(16)); + bytes memory slotAbi = abi.encodePacked(uint128(senderUnlockedShares), uint128(senderLockedShares)); + bytes32 slot; + assembly { + slot := mload(add(slotAbi, 0x20)) + } + _storeBytes32( + address(signallingEscrow), + 93842437974268059396725027201531251382101332839645030345425397622830526343272, + slot + ); + + uint256 senderLastAssetsLockTimestamp = kevm.freshUInt(32); + vm.assume(senderLastAssetsLockTimestamp < timeUpperBound); + _storeUInt256( + address(signallingEscrow), + 93842437974268059396725027201531251382101332839645030345425397622830526343273, + senderLastAssetsLockTimestamp + ); + + vm.assume(0 < amount); + vm.assume(amount <= stEth.balanceOf(sender)); + vm.assume(amount <= senderAllowance); + + AccountingRecord memory pre = this.saveAccountingRecord(sender, signallingEscrow); + + uint256 amountInShares = stEth.getSharesByPooledEth(amount); + _assumeNoOverflow(pre.userSharesLocked, amountInShares); + _assumeNoOverflow(pre.totalSharesLocked, amountInShares); + + this.escrowInvariants(Mode.Assume, signallingEscrow); + this.signallingEscrowInvariants(Mode.Assume, signallingEscrow); + this.escrowUserInvariants(Mode.Assume, signallingEscrow, sender); + + vm.startPrank(sender); + signallingEscrow.lockStETH(amount); + vm.stopPrank(); + + this.escrowInvariants(Mode.Assert, signallingEscrow); + this.signallingEscrowInvariants(Mode.Assert, signallingEscrow); + this.escrowUserInvariants(Mode.Assert, signallingEscrow, sender); + + AccountingRecord memory post = this.saveAccountingRecord(sender, signallingEscrow); + assert(post.userShares == pre.userShares - amountInShares); + assert(post.escrowShares == pre.escrowShares + amountInShares); + assert(post.userSharesLocked == pre.userSharesLocked + amountInShares); + assert(post.totalSharesLocked == pre.totalSharesLocked + amountInShares); + assert(post.userLastLockedTime == Timestamps.now()); + + // Accounts for rounding errors in the conversion to and from shares + assert(pre.userBalance - amount <= post.userBalance); + assert(post.escrowBalance <= pre.escrowBalance + amount); + assert(post.totalEth <= pre.totalEth + amount); + + uint256 errorTerm = stEth.getPooledEthByShares(1) + 1; + assert(post.userBalance <= pre.userBalance - amount + errorTerm); + assert(pre.escrowBalance + amount <= post.escrowBalance + errorTerm); + assert(pre.totalEth + amount <= post.totalEth + errorTerm); + } + + // Isolating individual branches of testUnlockStEth + + function testUnlockStEth_1() public { + State initialState = dualGovernance.getCurrentState(); + + vm.assume(initialState != State.VetoSignalling); + vm.assume(initialState != State.VetoSignallingDeactivation); + + testUnlockStEth(); + } + + function testUnlockStEth_2() public { + State initialState = dualGovernance.getCurrentState(); + uint256 rageQuitSupport = signallingEscrow.getRageQuitSupport(); + + vm.assume(initialState != State.Normal); + vm.assume(initialState != State.VetoCooldown); + vm.assume(initialState != State.RageQuit); + vm.assume(rageQuitSupport <= config.SECOND_SEAL_RAGE_QUIT_SUPPORT()); + + testUnlockStEth(); + } + + function testUnlockStEth_3() public { + State initialState = dualGovernance.getCurrentState(); + uint256 rageQuitSupport = signallingEscrow.getRageQuitSupport(); + Timestamp vetoSignallingActivationTime = Timestamp.wrap(_getVetoSignallingActivationTime(dualGovernance)); + + vm.assume(initialState != State.Normal); + vm.assume(initialState != State.VetoCooldown); + vm.assume(initialState != State.RageQuit); + vm.assume(rageQuitSupport > config.SECOND_SEAL_RAGE_QUIT_SUPPORT()); + vm.assume(Timestamps.now() <= config.DYNAMIC_TIMELOCK_MAX_DURATION().addTo(vetoSignallingActivationTime)); + + testUnlockStEth(); + } + + // + function testUnlockStEth() public { + // Placeholder address to avoid complications with keccak of symbolic addresses + address sender = address(uint160(uint256(keccak256("sender")))); + uint256 senderShares = kevm.freshUInt(32); + vm.assume(senderShares < ethUpperBound); + stEth.setShares(sender, senderShares); + vm.assume(stEth.balanceOf(sender) < ethUpperBound); + + uint256 senderAllowance = kevm.freshUInt(32); + // This assumption means that senderAllowance != INFINITE_ALLOWANCE, + // which doubles the execution effort without any added vaue + vm.assume(senderAllowance < ethUpperBound); + // Hardcoded for "sender" + _storeUInt256( + address(stEth), + 74992941968319547325319283905569341819227548318746972755481050864341498730161, + senderAllowance + ); + + uint128 senderLockedShares = uint128(kevm.freshUInt(16)); + vm.assume(senderLockedShares < ethUpperBound); + uint128 senderUnlockedShares = uint128(kevm.freshUInt(16)); + bytes memory slotAbi = abi.encodePacked(uint128(senderUnlockedShares), uint128(senderLockedShares)); + bytes32 slot; + assembly { + slot := mload(add(slotAbi, 0x20)) + } + _storeBytes32( + address(signallingEscrow), + 93842437974268059396725027201531251382101332839645030345425397622830526343272, + slot + ); + + uint256 senderLastAssetsLockTimestamp = kevm.freshUInt(32); + vm.assume(senderLastAssetsLockTimestamp < timeUpperBound); + _storeUInt256( + address(signallingEscrow), + 93842437974268059396725027201531251382101332839645030345425397622830526343273, + senderLastAssetsLockTimestamp + ); + + AccountingRecord memory pre = this.saveAccountingRecord(sender, signallingEscrow); + vm.assume(0 < pre.userSharesLocked); + vm.assume(pre.userSharesLocked <= pre.totalSharesLocked); + vm.assume(Timestamps.now() > addTo(config.SIGNALLING_ESCROW_MIN_LOCK_TIME(), pre.userLastLockedTime)); + + this.escrowInvariants(Mode.Assume, signallingEscrow); + this.signallingEscrowInvariants(Mode.Assume, signallingEscrow); + this.escrowUserInvariants(Mode.Assume, signallingEscrow, sender); + + bool transitionToRageQuit; + + { + State initialState = dualGovernance.getCurrentState(); + uint256 rageQuitSupport = signallingEscrow.getRageQuitSupport(); + Timestamp vetoSignallingActivationTime = Timestamp.wrap(_getVetoSignallingActivationTime(dualGovernance)); + + transitionToRageQuit = ( + initialState == State.VetoSignalling || initialState == State.VetoSignallingDeactivation + ) && rageQuitSupport > config.SECOND_SEAL_RAGE_QUIT_SUPPORT() + && Timestamps.now() > config.DYNAMIC_TIMELOCK_MAX_DURATION().addTo(vetoSignallingActivationTime); + } + + vm.assume(!transitionToRageQuit); + + ActivateNextStateMock mock = new ActivateNextStateMock(address(this), sender); + kevm.mockFunction( + address(dualGovernance), address(mock), abi.encodeWithSelector(mock.activateNextState.selector) + ); + + vm.startPrank(sender); + signallingEscrow.unlockStETH(); + vm.stopPrank(); + + this.escrowInvariants(Mode.Assert, signallingEscrow); + this.signallingEscrowInvariants(Mode.Assert, signallingEscrow); + this.escrowUserInvariants(Mode.Assert, signallingEscrow, sender); + + AccountingRecord memory post = this.saveAccountingRecord(sender, signallingEscrow); + assert(post.userShares == pre.userShares + pre.userSharesLocked); + assert(post.userSharesLocked == 0); + assert(post.totalSharesLocked == pre.totalSharesLocked - pre.userSharesLocked); + assert(post.userLastLockedTime == pre.userLastLockedTime); + + // Accounts for rounding errors in the conversion to and from shares + uint256 amount = stEth.getPooledEthByShares(pre.userSharesLocked); + + // Rewritten to avoid branching + //assert(pre.escrowBalance - amount < 1 || pre.escrowBalance - amount - 1 <= post.escrowBalance); + assert(pre.escrowBalance - amount <= post.escrowBalance + 1); + assert(post.escrowBalance <= pre.escrowBalance - amount); + + // Rewritten to avoid branching + //assert(pre.totalEth - amount < 1 || pre.totalEth - amount - 1 <= post.totalEth); + assert(pre.totalEth - amount <= post.totalEth + 1); + assert(post.totalEth <= pre.totalEth - amount); + + assert(pre.userBalance + amount <= post.userBalance); + assert(post.userBalance <= pre.userBalance + amount + 1); + } +} diff --git a/test/kontrol/EscrowOperations.t.sol b/test/kontrol/EscrowOperations.t.sol new file mode 100644 index 00000000..406791d8 --- /dev/null +++ b/test/kontrol/EscrowOperations.t.sol @@ -0,0 +1,163 @@ +pragma solidity 0.8.23; + +import {Duration, Durations} from "contracts/types/Duration.sol"; +import {Timestamp, Timestamps} from "contracts/types/Timestamp.sol"; + +import "test/kontrol/EscrowAccounting.t.sol"; + +contract EscrowOperationsTest is EscrowAccountingTest { + function _tryLockStETH(uint256 amount) internal returns (bool) { + try escrow.lockStETH(amount) { + return true; + } catch { + return false; + } + } + + function _tryUnlockStETH() internal returns (bool) { + try escrow.unlockStETH() { + return true; + } catch { + return false; + } + } + + /** + * Test that a staker cannot unlock funds from the escrow until SignallingEscrowMinLockTime has passed since the last time that user has locked tokens. + */ + function testCannotUnlockBeforeMinLockTime() external { + _setUpGenericState(); + + // Placeholder address to avoid complications with keccak of symbolic addresses + address sender = address(uint160(uint256(keccak256("sender")))); + vm.assume(stEth.sharesOf(sender) < ethUpperBound); + vm.assume(_getLastAssetsLockTimestamp(escrow, sender) < timeUpperBound); + + AccountingRecord memory pre = this.saveAccountingRecord(sender, escrow); + vm.assume(pre.escrowState == EscrowState.SignallingEscrow); + vm.assume(pre.userSharesLocked <= pre.totalSharesLocked); + + Timestamp lockPeriod = addTo(config.SIGNALLING_ESCROW_MIN_LOCK_TIME(), pre.userLastLockedTime); + + if (Timestamps.now() < lockPeriod) { + vm.prank(sender); + vm.expectRevert(abi.encodeWithSelector(AssetsAccounting.AssetsUnlockDelayNotPassed.selector, lockPeriod)); + escrow.unlockStETH(); + } + } + + /** + * Test that funds cannot be locked and unlocked if the escrow is in the RageQuitEscrow state. + */ + function testCannotLockUnlockInRageQuitEscrowState(uint256 amount) external { + _setUpGenericState(); + + // Placeholder address to avoid complications with keccak of symbolic addresses + address sender = address(uint160(uint256(keccak256("sender")))); + vm.assume(stEth.sharesOf(sender) < ethUpperBound); + vm.assume(stEth.balanceOf(sender) < ethUpperBound); + + AccountingRecord memory pre = this.saveAccountingRecord(sender, escrow); + vm.assume(0 < amount); + vm.assume(amount <= pre.userBalance); + vm.assume(amount <= pre.allowance); + + uint256 amountInShares = stEth.getSharesByPooledEth(amount); + _assumeNoOverflow(pre.userSharesLocked, amountInShares); + _assumeNoOverflow(pre.totalSharesLocked, amountInShares); + + this.escrowInvariants(Mode.Assume, escrow); + this.signallingEscrowInvariants(Mode.Assume, escrow); + this.escrowUserInvariants(Mode.Assume, escrow, sender); + + if (pre.escrowState == EscrowState.RageQuitEscrow) { + vm.startPrank(sender); + //vm.expectRevert("Cannot lock in current state."); + bool lockSuccess = _tryLockStETH(amount); + assertTrue(lockSuccess, "Cannot lock in current state."); + vm.stopPrank; + + vm.startPrank(sender); + //vm.expectRevert("Cannot unlock in current state."); + bool unlockSuccess = _tryUnlockStETH(); + assertTrue(unlockSuccess, "Cannot unlock in current state."); + vm.stopPrank; + } else { + vm.prank(sender); + escrow.lockStETH(amount); + + AccountingRecord memory afterLock = this.saveAccountingRecord(sender, escrow); + vm.assume(afterLock.userShares < ethUpperBound); + //vm.assume(afterLock.userLastLockedTime < timeUpperBound); + vm.assume(afterLock.userSharesLocked <= afterLock.totalSharesLocked); + vm.assume(Timestamps.now() >= addTo(config.SIGNALLING_ESCROW_MIN_LOCK_TIME(), afterLock.userLastLockedTime)); + + vm.prank(sender); + escrow.unlockStETH(); + + this.escrowInvariants(Mode.Assert, escrow); + this.signallingEscrowInvariants(Mode.Assert, escrow); + this.escrowUserInvariants(Mode.Assert, escrow, sender); + + AccountingRecord memory post = this.saveAccountingRecord(sender, escrow); + assert(post.escrowState == EscrowState.SignallingEscrow); + assert(post.userShares == pre.userShares); + assert(post.escrowShares == pre.escrowShares); + assert(post.userSharesLocked == 0); + assert(post.totalSharesLocked == pre.totalSharesLocked); + assert(post.userLastLockedTime == afterLock.userLastLockedTime); + } + } + + /** + * Test that a user cannot withdraw funds from the escrow until the RageQuitEthClaimTimelock has elapsed after the RageQuitExtensionDelay period. + */ + // TODO: Uncomment this test and adapt it to the client code + /* + function testCannotWithdrawBeforeEthClaimTimelockElapsed() external { + _setUpGenericState(); + + // Placeholder address to avoid complications with keccak of symbolic addresses + address sender = address(uint160(uint256(keccak256("sender")))); + vm.assume(stEth.sharesOf(sender) < ethUpperBound); + vm.assume(stEth.balanceOf(sender) < ethUpperBound); + + AccountingRecord memory pre = this.saveAccountingRecord(sender, escrow); + vm.assume(pre.escrowState == EscrowState.RageQuitEscrow); + vm.assume(pre.userSharesLocked > 0); + vm.assume(pre.userSharesLocked <= pre.totalSharesLocked); + uint256 userEth = stEth.getPooledEthByShares(pre.userSharesLocked); + vm.assume(userEth <= pre.totalEth); + vm.assume(userEth <= address(escrow).balance); + + this.escrowInvariants(Mode.Assume, escrow); + this.escrowUserInvariants(Mode.Assume, escrow, sender); + + vm.assume(escrow.lastWithdrawalRequestSubmitted()); + vm.assume(escrow.claimedWithdrawalRequests() == escrow.withdrawalRequestCount()); + vm.assume(escrow.getIsWithdrawalsClaimed()); + vm.assume(escrow.rageQuitExtensionDelayPeriodEnd() < block.timestamp); + // Assumption for simplicity + vm.assume(escrow.rageQuitSequenceNumber() < 2); + + uint256 timelockStart = escrow.rageQuitEthClaimTimelockStart(); + uint256 ethClaimTimelock = escrow.rageQuitEthClaimTimelock(); + vm.assume(timelockStart + ethClaimTimelock < timeUpperBound); + + if (block.timestamp <= timelockStart + ethClaimTimelock) { + vm.prank(sender); + vm.expectRevert("Rage quit ETH claim timelock has not elapsed."); + escrow.withdraw(); + } else { + vm.prank(sender); + escrow.withdraw(); + + this.escrowInvariants(Mode.Assert); + this.escrowUserInvariants(Mode.Assert, sender); + + AccountingRecord memory post = this.saveAccountingRecord(sender, escrow); + assert(post.userSharesLocked == 0); + } + } + */ +} diff --git a/test/kontrol/KontrolTest.sol b/test/kontrol/KontrolTest.sol new file mode 100644 index 00000000..1cb57cba --- /dev/null +++ b/test/kontrol/KontrolTest.sol @@ -0,0 +1,63 @@ +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; + // Note: 2 ** 35 takes us to year 3058 + uint256 constant timeUpperBound = 2 ** 35; + + function infoAssert(bool condition, string memory message) external { + if (!condition) { + revert(message); + } + } + + enum Mode { + Assume, + Try, + Assert + } + + function _establish(Mode mode, bool condition) internal pure returns (bool) { + if (mode == Mode.Assume) { + vm.assume(condition); + return true; + } else if (mode == Mode.Try) { + return condition; + } else { + assert(condition); + return true; + } + } + + function _loadUInt256(address contractAddress, uint256 slot) internal view returns (uint256) { + return uint256(vm.load(contractAddress, bytes32(slot))); + } + + function _loadAddress(address contractAddress, uint256 slot) internal view returns (address) { + return address(uint160(uint256(vm.load(contractAddress, bytes32(slot))))); + } + + 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)))); + } + + function _assumeNoOverflow(uint256 augend, uint256 addend) internal { + unchecked { + vm.assume(augend < augend + addend); + } + } +} diff --git a/test/kontrol/ProposalOperations.t.sol b/test/kontrol/ProposalOperations.t.sol new file mode 100644 index 00000000..224ff84a --- /dev/null +++ b/test/kontrol/ProposalOperations.t.sol @@ -0,0 +1,259 @@ +pragma solidity 0.8.23; + +import {Clones} from "@openzeppelin/contracts/proxy/Clones.sol"; + +import "contracts/Configuration.sol"; +import "contracts/DualGovernance.sol"; +import "contracts/EmergencyProtectedTimelock.sol"; +import "contracts/Escrow.sol"; + +import {Status, Proposal} from "contracts/libraries/Proposals.sol"; +import {State} from "contracts/libraries/DualGovernanceState.sol"; +import {addTo, Duration, Durations} from "contracts/types/Duration.sol"; +import {Timestamp, Timestamps} from "contracts/types/Timestamp.sol"; + +import {ProposalOperationsSetup} from "test/kontrol/ProposalOperationsSetup.sol"; + +contract ProposalOperationsTest is ProposalOperationsSetup { + function _proposalOperationsInitializeStorage( + DualGovernance _dualGovernance, + EmergencyProtectedTimelock _timelock, + uint256 _proposalId + ) public { + _timelockStorageSetup(_dualGovernance, _timelock); + _proposalIdAssumeBound(_proposalId); + _proposalStorageSetup(_timelock, _proposalId); + _storeExecutorCalls(_timelock, _proposalId); + } + + struct ProposalRecord { + State state; + uint256 id; + uint256 lastCancelledProposalId; + Timestamp submittedAt; + Timestamp scheduledAt; + Timestamp executedAt; + Timestamp vetoSignallingActivationTime; + } + + // Record a proposal's details with the current governance state. + function _recordProposal(uint256 proposalId) internal returns (ProposalRecord memory pr) { + uint256 baseSlot = _getProposalsSlot(proposalId); + pr.id = proposalId; + pr.state = dualGovernance.getCurrentState(); + pr.lastCancelledProposalId = _getLastCancelledProposalId(timelock); + pr.submittedAt = Timestamp.wrap(_getSubmittedAt(timelock, baseSlot)); + pr.scheduledAt = Timestamp.wrap(_getScheduledAt(timelock, baseSlot)); + pr.executedAt = Timestamp.wrap(_getExecutedAt(timelock, baseSlot)); + pr.vetoSignallingActivationTime = Timestamp.wrap(_getVetoSignallingActivationTime(dualGovernance)); + } + + // Validate that a pending proposal meets the criteria. + function _validPendingProposal(Mode mode, ProposalRecord memory pr) internal pure { + _establish(mode, pr.lastCancelledProposalId < pr.id); + _establish(mode, pr.submittedAt != Timestamp.wrap(0)); + _establish(mode, pr.scheduledAt == Timestamp.wrap(0)); + _establish(mode, pr.executedAt == Timestamp.wrap(0)); + } + + // Validate that a scheduled proposal meets the criteria. + function _validScheduledProposal(Mode mode, ProposalRecord memory pr) internal { + _establish(mode, pr.lastCancelledProposalId < pr.id); + _establish(mode, pr.submittedAt != Timestamp.wrap(0)); + _establish(mode, pr.scheduledAt != Timestamp.wrap(0)); + _establish(mode, pr.executedAt == Timestamp.wrap(0)); + _establish(mode, config.AFTER_SUBMIT_DELAY().addTo(pr.submittedAt) <= Timestamps.now()); + } + + function _validExecutedProposal(Mode mode, ProposalRecord memory pr) internal { + _establish(mode, pr.lastCancelledProposalId < pr.id); + _establish(mode, pr.submittedAt != Timestamp.wrap(0)); + _establish(mode, pr.scheduledAt != Timestamp.wrap(0)); + _establish(mode, pr.executedAt != Timestamp.wrap(0)); + _establish(mode, config.AFTER_SUBMIT_DELAY().addTo(pr.submittedAt) <= Timestamps.now()); + _establish(mode, config.AFTER_SCHEDULE_DELAY().addTo(pr.scheduledAt) <= Timestamps.now()); + } + + function _validCanceledProposal(Mode mode, ProposalRecord memory pr) internal pure { + _establish(mode, pr.id <= pr.lastCancelledProposalId); + _establish(mode, pr.submittedAt != Timestamp.wrap(0)); + _establish(mode, pr.executedAt == Timestamp.wrap(0)); + } + + function _isExecuted(ProposalRecord memory pr) internal pure returns (bool) { + return pr.executedAt != Timestamp.wrap(0); + } + + function _isCancelled(ProposalRecord memory pr) internal pure returns (bool) { + return pr.lastCancelledProposalId >= pr.id; + } + + function testCannotProposeInInvalidState() external { + _initializeAuxDualGovernance(); + + _timelockStorageSetup(dualGovernance, timelock); + uint256 newProposalIndex = timelock.getProposalsCount(); + + address proposer = address(uint160(uint256(keccak256("proposer")))); + uint8 proposerIndexOneBased = uint8(kevm.freshUInt(1)); + vm.assume(proposerIndexOneBased != 0); + uint160 executor = uint160(kevm.freshUInt(20)); + bytes memory slotAbi = abi.encodePacked(uint88(0), uint160(executor), uint8(proposerIndexOneBased)); + bytes32 slot; + assembly { + slot := mload(add(slotAbi, 0x20)) + } + _storeBytes32( + address(dualGovernance), 28324487748957058971331294301258181510018269374235438230632061138814754629752, slot + ); + + auxDualGovernance.activateNextState(); + State nextState = auxDualGovernance.getCurrentState(); + vm.assume(nextState != State.Normal); + vm.assume(nextState != State.VetoSignalling); + vm.assume(nextState != State.RageQuit); + + vm.prank(proposer); + vm.expectRevert(DualGovernanceState.ProposalsCreationSuspended.selector); + dualGovernance.submitProposal(new ExecutorCall[](1)); + + assert(timelock.getProposalsCount() == newProposalIndex); + } + + /** + * Test that a proposal cannot be scheduled for execution if the Dual Governance state is not Normal or VetoCooldown. + */ + function testCannotScheduleInInvalidStates(uint256 proposalId) external { + _timelockStorageSetup(dualGovernance, timelock); + _proposalIdAssumeBound(proposalId); + _proposalStorageSetup(timelock, proposalId); + + ProposalRecord memory pre = _recordProposal(proposalId); + _validPendingProposal(Mode.Assume, pre); + vm.assume(timelock.canSchedule(proposalId)); + vm.assume(!dualGovernance.isSchedulingEnabled()); + + vm.expectRevert(DualGovernanceState.ProposalsAdoptionSuspended.selector); + dualGovernance.scheduleProposal(proposalId); + + ProposalRecord memory post = _recordProposal(proposalId); + _validPendingProposal(Mode.Assert, post); + } + + /** + * Test that a proposal cannot be scheduled for execution if it was submitted after the last time the VetoSignalling state was entered. + */ + function testCannotScheduleSubmissionAfterLastVetoSignalling(uint256 proposalId) external { + _timelockStorageSetup(dualGovernance, timelock); + _proposalIdAssumeBound(proposalId); + _proposalStorageSetup(timelock, proposalId); + + ProposalRecord memory pre = _recordProposal(proposalId); + _validPendingProposal(Mode.Assume, pre); + vm.assume(timelock.canSchedule(proposalId)); + vm.assume(pre.state == State.VetoCooldown); + vm.assume(pre.submittedAt > pre.vetoSignallingActivationTime); + + vm.expectRevert(DualGovernanceState.ProposalsAdoptionSuspended.selector); + dualGovernance.scheduleProposal(proposalId); + + ProposalRecord memory post = _recordProposal(proposalId); + _validPendingProposal(Mode.Assert, post); + } + + // Test that actions that are canceled or executed cannot be rescheduled + function testCanceledOrExecutedActionsCannotBeRescheduled(uint256 proposalId) external { + _proposalOperationsInitializeStorage(dualGovernance, timelock, proposalId); + + ProposalRecord memory pre = _recordProposal(proposalId); + vm.assume(pre.submittedAt != Timestamp.wrap(0)); + vm.assume(dualGovernance.isSchedulingEnabled()); + if (pre.state == State.VetoCooldown) { + vm.assume(pre.submittedAt <= pre.vetoSignallingActivationTime); + } + + // Check if the proposal has been executed + if (pre.executedAt != Timestamp.wrap(0)) { + _validExecutedProposal(Mode.Assume, pre); + + vm.expectRevert(abi.encodeWithSelector(Proposals.ProposalNotSubmitted.selector, proposalId)); + dualGovernance.scheduleProposal(proposalId); + + ProposalRecord memory post = _recordProposal(proposalId); + _validExecutedProposal(Mode.Assert, post); + } else if (pre.lastCancelledProposalId >= proposalId) { + // Check if the proposal has been cancelled + _validCanceledProposal(Mode.Assume, pre); + + vm.expectRevert(abi.encodeWithSelector(Proposals.ProposalNotSubmitted.selector, proposalId)); + dualGovernance.scheduleProposal(proposalId); + + ProposalRecord memory post = _recordProposal(proposalId); + _validCanceledProposal(Mode.Assert, post); + } + } + + /** + * Test that a proposal cannot be scheduled for execution before ProposalExecutionMinTimelock has passed since its submission. + */ + function testCannotScheduleBeforeMinTimelock(uint256 proposalId) external { + _proposalOperationsInitializeStorage(dualGovernance, timelock, proposalId); + + ProposalRecord memory pre = _recordProposal(proposalId); + _validPendingProposal(Mode.Assume, pre); + + vm.assume(dualGovernance.isSchedulingEnabled()); + if (pre.state == State.VetoCooldown) { + vm.assume(pre.submittedAt <= pre.vetoSignallingActivationTime); + } + vm.assume(Timestamps.now() < addTo(config.AFTER_SUBMIT_DELAY(), pre.submittedAt)); + + vm.expectRevert(abi.encodeWithSelector(Proposals.AfterSubmitDelayNotPassed.selector, proposalId)); + dualGovernance.scheduleProposal(proposalId); + + ProposalRecord memory post = _recordProposal(proposalId); + _validPendingProposal(Mode.Assert, post); + } + + /** + * Test that a proposal cannot be executed until the emergency protection timelock has passed since it was scheduled. + */ + function testCannotExecuteBeforeEmergencyProtectionTimelock(uint256 proposalId) external { + _proposalOperationsInitializeStorage(dualGovernance, timelock, proposalId); + + ProposalRecord memory pre = _recordProposal(proposalId); + _validScheduledProposal(Mode.Assume, pre); + vm.assume(_getEmergencyModeEndsAfter(timelock) == 0); + vm.assume(Timestamps.now() < addTo(config.AFTER_SCHEDULE_DELAY(), pre.scheduledAt)); + + vm.expectRevert(abi.encodeWithSelector(Proposals.AfterScheduleDelayNotPassed.selector, proposalId)); + timelock.execute(proposalId); + + ProposalRecord memory post = _recordProposal(proposalId); + _validScheduledProposal(Mode.Assert, post); + } + + /** + * Test that only admin proposers can cancel proposals. + */ + function testOnlyAdminProposersCanCancelProposals() external { + _timelockStorageSetup(dualGovernance, timelock); + + // Cancel as a non-admin proposer + address proposer = address(uint160(uint256(keccak256("proposer")))); + vm.assume(dualGovernance.isProposer(proposer)); + vm.assume(dualGovernance.getProposer(proposer).executor != config.ADMIN_EXECUTOR()); + + vm.prank(proposer); + vm.expectRevert(abi.encodeWithSelector(Proposers.NotAdminProposer.selector, proposer)); + dualGovernance.cancelAllPendingProposals(); + + // Cancel as an admin proposer + address adminProposer = address(uint160(uint256(keccak256("adminProposer")))); + vm.assume(dualGovernance.isProposer(adminProposer)); + vm.assume(dualGovernance.getProposer(adminProposer).executor == config.ADMIN_EXECUTOR()); + + vm.prank(adminProposer); + dualGovernance.cancelAllPendingProposals(); + } +} diff --git a/test/kontrol/ProposalOperationsSetup.sol b/test/kontrol/ProposalOperationsSetup.sol new file mode 100644 index 00000000..60518e60 --- /dev/null +++ b/test/kontrol/ProposalOperationsSetup.sol @@ -0,0 +1,204 @@ +pragma solidity 0.8.23; + +import {Clones} from "@openzeppelin/contracts/proxy/Clones.sol"; + +import "contracts/Configuration.sol"; +import "contracts/DualGovernance.sol"; +import "contracts/EmergencyProtectedTimelock.sol"; +import "contracts/Escrow.sol"; + +import {Status, Proposal} from "contracts/libraries/Proposals.sol"; +import {State} from "contracts/libraries/DualGovernanceState.sol"; +import {addTo, Duration, Durations} from "contracts/types/Duration.sol"; +import {Timestamp, Timestamps} from "contracts/types/Timestamp.sol"; + +import {DualGovernanceSetUp} from "test/kontrol/DualGovernanceSetUp.sol"; + +contract ProposalOperationsSetup is DualGovernanceSetUp { + DualGovernance auxDualGovernance; + EmergencyProtectedTimelock auxTimelock; + Escrow auxSignallingEscrow; + Escrow auxRageQuitEscrow; + + function _initializeAuxDualGovernance() public { + address adminProposer = address(uint160(uint256(keccak256("adminProposer")))); + auxTimelock = new EmergencyProtectedTimelock(address(config)); + kevm.symbolicStorage(address(auxTimelock)); + + auxDualGovernance = + new DualGovernance(address(config), address(timelock), address(escrowMasterCopy), adminProposer); + kevm.copyStorage(address(dualGovernance), address(auxDualGovernance)); + + auxSignallingEscrow = Escrow(payable(Clones.clone(dualGovernance.getVetoSignallingEscrow()))); + auxRageQuitEscrow = Escrow(payable(Clones.clone(dualGovernance.getRageQuitEscrow()))); + kevm.copyStorage(dualGovernance.getVetoSignallingEscrow(), address(auxSignallingEscrow)); + kevm.copyStorage(dualGovernance.getRageQuitEscrow(), address(auxRageQuitEscrow)); + + uint256 signallingEscrowSlot = _loadUInt256(address(auxDualGovernance), 5); + uint256 rageQuitEscrowSlot = _loadUInt256(address(auxDualGovernance), 6); + + uint256 signallingEscrowMask = type(uint256).max ^ ((2 ** 160 - 1) << 88); + uint256 rageQuitEscrowMask = type(uint256).max ^ ((2 ** 160 - 1) << 80); + + signallingEscrowSlot = + (uint256(uint160(address(auxSignallingEscrow))) * (2 ** 88)) | (signallingEscrowMask & signallingEscrowSlot); + rageQuitEscrowSlot = + (uint256(uint160(address(auxRageQuitEscrow))) * (2 ** 80)) | (rageQuitEscrowMask & rageQuitEscrowSlot); + + _storeUInt256(address(auxDualGovernance), 5, signallingEscrowSlot); + _storeUInt256(address(auxDualGovernance), 6, rageQuitEscrowSlot); + + uint256 dualGovernanceMask = type(uint256).max ^ ((2 ** 160 - 1) << 8); + + uint256 dualGovernanceSlotSE = _loadUInt256(address(auxSignallingEscrow), 0); + uint256 dualGovernanceSlotRE = _loadUInt256(address(auxRageQuitEscrow), 0); + + dualGovernanceSlotSE = + (uint256(uint160(address(auxDualGovernance))) * (2 ** 8)) | (dualGovernanceMask & dualGovernanceSlotSE); + dualGovernanceSlotRE = + (uint256(uint160(address(auxDualGovernance))) * (2 ** 8)) | (dualGovernanceMask & dualGovernanceSlotRE); + + _storeUInt256(address(auxSignallingEscrow), 0, dualGovernanceSlotSE); + _storeUInt256(address(auxRageQuitEscrow), 0, dualGovernanceSlotRE); + } + + // ?STORAGE3 + // ?WORD21: lastCancelledProposalId + // ?WORD22: proposalsLength + // ?WORD23: protectedTill + // ?WORD24: emergencyModeEndsAfter + function _timelockStorageSetup(DualGovernance _dualGovernance, EmergencyProtectedTimelock _timelock) public { + // Slot 0 + _storeAddress(address(_timelock), 0, address(_dualGovernance)); + // Slot 1 + uint256 lastCancelledProposalId = kevm.freshUInt(32); + vm.assume(lastCancelledProposalId < type(uint256).max); + _storeUInt256(address(timelock), 1, lastCancelledProposalId); + // Slot 2 + uint256 proposalsLength = kevm.freshUInt(32); + vm.assume(proposalsLength < type(uint64).max); + vm.assume(lastCancelledProposalId <= proposalsLength); + _storeUInt256(address(_timelock), 2, proposalsLength); + // Slot 3 + { + address activationCommittee = address(uint160(uint256(keccak256("activationCommittee")))); + uint40 protectedTill = uint40(kevm.freshUInt(5)); + vm.assume(protectedTill < timeUpperBound); + vm.assume(protectedTill <= block.timestamp); + bytes memory slot3Abi = abi.encodePacked(uint56(0), uint40(protectedTill), uint160(activationCommittee)); + bytes32 slot3; + assembly { + slot3 := mload(add(slot3Abi, 0x20)) + } + _storeBytes32(address(_timelock), 3, slot3); + } + // Slot 4 + uint40 emergencyModeEndsAfter = uint40(kevm.freshUInt(5)); + vm.assume(emergencyModeEndsAfter < timeUpperBound); + vm.assume(emergencyModeEndsAfter <= block.timestamp); + _storeUInt256(address(_timelock), 4, emergencyModeEndsAfter); + } + + // Set up the storage for a proposal. + // ?WORD25: submittedAt + // ?WORD26: scheduledAt + // ?WORD27: executedAt + // ?WORD28: numCalls + function _proposalStorageSetup(EmergencyProtectedTimelock _timelock, uint256 _proposalId) public { + uint256 baseSlot = _getProposalsSlot(_proposalId); + // slot 1 + { + address executor = address(uint160(uint256(keccak256("executor")))); + uint40 submittedAt = uint40(kevm.freshUInt(5)); + vm.assume(submittedAt < timeUpperBound); + vm.assume(submittedAt <= block.timestamp); + uint40 scheduledAt = uint40(kevm.freshUInt(5)); + vm.assume(scheduledAt < timeUpperBound); + vm.assume(scheduledAt <= block.timestamp); + bytes memory slot1Abi = + abi.encodePacked(uint16(0), uint40(scheduledAt), uint40(submittedAt), uint160(executor)); + bytes32 slot1; + assembly { + slot1 := mload(add(slot1Abi, 0x20)) + } + _storeBytes32(address(_timelock), baseSlot, slot1); + } + // slot 2 + { + uint40 executedAt = uint40(kevm.freshUInt(5)); + vm.assume(executedAt < timeUpperBound); + vm.assume(executedAt <= block.timestamp); + _storeUInt256(address(_timelock), baseSlot + 1, executedAt); + } + // slot 3 + { + uint256 numCalls = kevm.freshUInt(32); + vm.assume(numCalls < type(uint256).max); + vm.assume(numCalls > 0); + _storeUInt256(address(_timelock), baseSlot + 2, numCalls); + } + } + + function _storeExecutorCalls(EmergencyProtectedTimelock _timelock, uint256 _proposalId) public { + uint256 baseSlot = _getProposalsSlot(_proposalId); + uint256 numCalls = _getCallsCount(_timelock, _proposalId); + uint256 callsSlot = uint256(keccak256(abi.encodePacked(baseSlot + 2))); + + for (uint256 j = 0; j < numCalls; j++) { + uint256 callSlot = callsSlot + j * 3; + vm.assume(callSlot < type(uint256).max); + address target = address(uint160(uint256(keccak256(abi.encodePacked(j, "target"))))); + _storeAddress(address(_timelock), callSlot, target); + uint96 value = uint96(kevm.freshUInt(12)); + vm.assume(value != 0); + _storeUInt256(address(_timelock), callSlot + 1, uint256(value)); + bytes memory payload = abi.encodePacked(j, "payload"); + _storeBytes32(address(_timelock), callSlot + 2, keccak256(payload)); + } + } + + function _proposalIdAssumeBound(uint256 _proposalId) internal view { + vm.assume(_proposalId > 0); + vm.assume(_proposalId < _getProposalsCount(timelock)); + uint256 slot2 = uint256(keccak256(abi.encodePacked(uint256(2)))); + vm.assume((_proposalId - 1) <= ((type(uint256).max - 3 - slot2) / 3)); + } + + function _getProposalsSlot(uint256 _proposalId) internal returns (uint256 baseSlot) { + uint256 startSlot = uint256(keccak256(abi.encodePacked(uint256(2)))); + uint256 offset = 3 * (_proposalId - 1); + baseSlot = startSlot + offset; + } + + function _getProtectedTill(EmergencyProtectedTimelock _timelock) internal view returns (uint40) { + return uint40(_loadUInt256(address(_timelock), 3) >> 160); + } + + function _getLastCancelledProposalId(EmergencyProtectedTimelock _timelock) internal view returns (uint256) { + return _loadUInt256(address(_timelock), 1); + } + + function _getProposalsCount(EmergencyProtectedTimelock _timelock) internal view returns (uint256) { + return _loadUInt256(address(_timelock), 2); + } + + function _getEmergencyModeEndsAfter(EmergencyProtectedTimelock _timelock) internal view returns (uint40) { + return uint40(_loadUInt256(address(_timelock), 4)); + } + + function _getSubmittedAt(EmergencyProtectedTimelock _timelock, uint256 baseSlot) internal view returns (uint40) { + return uint40(_loadUInt256(address(_timelock), baseSlot) >> 160); + } + + function _getScheduledAt(EmergencyProtectedTimelock _timelock, uint256 baseSlot) internal view returns (uint40) { + return uint40(_loadUInt256(address(_timelock), baseSlot) >> 200); + } + + function _getExecutedAt(EmergencyProtectedTimelock _timelock, uint256 baseSlot) internal view returns (uint40) { + return uint40(_loadUInt256(address(_timelock), baseSlot + 1)); + } + + function _getCallsCount(EmergencyProtectedTimelock _timelock, uint256 baseSlot) internal view returns (uint256) { + return _loadUInt256(address(_timelock), baseSlot + 2); + } +} diff --git a/test/kontrol/RageQuit.t.sol b/test/kontrol/RageQuit.t.sol new file mode 100644 index 00000000..58d7e3b2 --- /dev/null +++ b/test/kontrol/RageQuit.t.sol @@ -0,0 +1,21 @@ +pragma solidity 0.8.23; + +import "forge-std/Vm.sol"; +import "kontrol-cheatcodes/KontrolCheats.sol"; + +import "test/kontrol/DualGovernanceSetUp.sol"; + +contract RageQuitTest is DualGovernanceSetUp { + function testRageQuitDuration() external { + vm.assume(dualGovernance.getCurrentState() == State.RageQuit); + + dualGovernance.activateNextState(); + + uint40 rageQuitTimelockStartedAt = _getRageQuitTimelockStartedAt(rageQuitEscrow); + uint32 rageQuitExtensionDelay = _getRageQuitExtensionDelay(rageQuitEscrow); + + if (block.timestamp <= rageQuitTimelockStartedAt + rageQuitExtensionDelay) { + assert(dualGovernance.getCurrentState() == State.RageQuit); + } + } +} diff --git a/test/kontrol/StorageSetup.sol b/test/kontrol/StorageSetup.sol new file mode 100644 index 00000000..6ff8f2e2 --- /dev/null +++ b/test/kontrol/StorageSetup.sol @@ -0,0 +1,426 @@ +pragma solidity 0.8.23; + +import "contracts/DualGovernance.sol"; +import "contracts/EmergencyProtectedTimelock.sol"; +import "contracts/Escrow.sol"; + +import {Timestamp} from "contracts/types/Timestamp.sol"; +import "contracts/libraries/WithdrawalBatchesQueue.sol"; + +import "contracts/model/StETHModel.sol"; +import "contracts/model/WstETHAdapted.sol"; + +import "test/kontrol/KontrolTest.sol"; + +contract StorageSetup is KontrolTest { + function stEthStorageSetup(StETHModel _stEth, IEscrow _escrow) external { + 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); + vm.assume(shares < ethUpperBound); + _stEth.setShares(address(_escrow), shares); + } + + function stEthStorageInvariants(Mode mode, StETHModel _stEth, IEscrow _escrow) external { + uint256 totalPooledEther = _stEth.getTotalPooledEther(); + uint256 totalShares = _stEth.getTotalShares(); + uint256 escrowShares = _stEth.sharesOf(address(_escrow)); + + _establish(mode, 0 < _stEth.getTotalPooledEther()); + _establish(mode, 0 < _stEth.getTotalShares()); + _establish(mode, escrowShares < totalShares); + } + + function stEthAssumeBounds(StETHModel _stEth, IEscrow _escrow) external { + uint256 totalPooledEther = _stEth.getTotalPooledEther(); + uint256 totalShares = _stEth.getTotalShares(); + uint256 escrowShares = _stEth.sharesOf(address(_escrow)); + + vm.assume(totalPooledEther < ethUpperBound); + vm.assume(totalShares < ethUpperBound); + vm.assume(escrowShares < ethUpperBound); + } + + function _wstEthStorageSetup(WstETHAdapted _wstEth, IStETH _stEth) internal { + kevm.symbolicStorage(address(_wstEth)); + } + + function _getCurrentState(DualGovernance _dualGovernance) internal view returns (uint8) { + return uint8(_loadUInt256(address(_dualGovernance), 5)); + } + + function _getEnteredAt(DualGovernance _dualGovernance) internal view returns (uint40) { + return uint40(_loadUInt256(address(_dualGovernance), 5) >> 8); + } + + function _getVetoSignallingActivationTime(DualGovernance _dualGovernance) internal view returns (uint40) { + return uint40(_loadUInt256(address(_dualGovernance), 5) >> 48); + } + + function _getVetoSignallingReactivationTime(DualGovernance _dualGovernance) internal view returns (uint40) { + return uint40(_loadUInt256(address(_dualGovernance), 6)); + } + + function _getLastAdoptableStateExitedAt(DualGovernance _dualGovernance) internal view returns (uint40) { + return uint40(_loadUInt256(address(_dualGovernance), 6) >> 40); + } + + function _getRageQuitRound(DualGovernance _dualGovernance) internal view returns (uint8) { + return uint8(_loadUInt256(address(_dualGovernance), 6) >> 240); + } + + function dualGovernanceStorageSetup( + DualGovernance _dualGovernance, + IEscrow _signallingEscrow, + IEscrow _rageQuitEscrow + ) external { + kevm.symbolicStorage(address(_dualGovernance)); + // Slot 5 + 0 = 5 + uint8 currentState = uint8(kevm.freshUInt(1)); + vm.assume(currentState <= 4); + uint40 enteredAt = uint40(kevm.freshUInt(5)); + vm.assume(enteredAt <= block.timestamp); + vm.assume(enteredAt < timeUpperBound); + uint40 vetoSignallingActivationTime = uint40(kevm.freshUInt(5)); + vm.assume(vetoSignallingActivationTime <= block.timestamp); + vm.assume(vetoSignallingActivationTime < timeUpperBound); + bytes memory slot5Abi = abi.encodePacked( + uint8(0), + uint160(address(_signallingEscrow)), + uint40(vetoSignallingActivationTime), + uint40(enteredAt), + uint8(currentState) + ); + bytes32 slot5; + assembly { + slot5 := mload(add(slot5Abi, 0x20)) + } + _storeBytes32(address(_dualGovernance), 5, slot5); + // Slot 5 + 1 = 6 + uint40 vetoSignallingReactivationTime = uint40(kevm.freshUInt(5)); + vm.assume(vetoSignallingReactivationTime <= block.timestamp); + vm.assume(vetoSignallingReactivationTime < timeUpperBound); + uint40 lastAdoptableStateExitedAt = uint40(kevm.freshUInt(5)); + vm.assume(lastAdoptableStateExitedAt <= block.timestamp); + vm.assume(lastAdoptableStateExitedAt < timeUpperBound); + uint8 rageQuitRound = uint8(kevm.freshUInt(1)); + vm.assume(rageQuitRound < type(uint8).max); + bytes memory slot6Abi = abi.encodePacked( + uint8(0), + uint8(rageQuitRound), + uint160(address(_rageQuitEscrow)), + uint40(lastAdoptableStateExitedAt), + uint40(vetoSignallingReactivationTime) + ); + bytes32 slot6; + assembly { + slot6 := mload(add(slot6Abi, 0x20)) + } + _storeBytes32(address(_dualGovernance), 6, slot6); + } + + function dualGovernanceStorageInvariants(Mode mode, DualGovernance _dualGovernance) external { + uint8 currentState = _getCurrentState(_dualGovernance); + uint40 enteredAt = _getEnteredAt(_dualGovernance); + uint40 vetoSignallingActivationTime = _getVetoSignallingActivationTime(_dualGovernance); + uint40 vetoSignallingReactivationTime = _getVetoSignallingReactivationTime(_dualGovernance); + uint40 lastAdoptableStateExitedAt = _getLastAdoptableStateExitedAt(_dualGovernance); + uint8 rageQuitRound = _getRageQuitRound(_dualGovernance); + + _establish(mode, currentState <= 4); + _establish(mode, enteredAt <= block.timestamp); + _establish(mode, vetoSignallingActivationTime <= block.timestamp); + _establish(mode, vetoSignallingReactivationTime <= block.timestamp); + _establish(mode, lastAdoptableStateExitedAt <= block.timestamp); + } + + function dualGovernanceAssumeBounds(DualGovernance _dualGovernance) external { + uint40 enteredAt = _getEnteredAt(_dualGovernance); + uint40 vetoSignallingActivationTime = _getVetoSignallingActivationTime(_dualGovernance); + uint40 vetoSignallingReactivationTime = _getVetoSignallingReactivationTime(_dualGovernance); + uint40 lastAdoptableStateExitedAt = _getLastAdoptableStateExitedAt(_dualGovernance); + uint8 rageQuitRound = _getRageQuitRound(_dualGovernance); + + vm.assume(enteredAt < timeUpperBound); + vm.assume(vetoSignallingActivationTime < timeUpperBound); + vm.assume(vetoSignallingReactivationTime < timeUpperBound); + vm.assume(lastAdoptableStateExitedAt < timeUpperBound); + vm.assume(rageQuitRound < type(uint8).max); + } + + function dualGovernanceInitializeStorage( + DualGovernance _dualGovernance, + IEscrow _signallingEscrow, + IEscrow _rageQuitEscrow + ) external { + this.dualGovernanceStorageSetup(_dualGovernance, _signallingEscrow, _rageQuitEscrow); + this.dualGovernanceStorageInvariants(Mode.Assume, _dualGovernance); + this.dualGovernanceAssumeBounds(_dualGovernance); + } + + function _getCurrentState(IEscrow _escrow) internal view returns (uint8) { + return uint8(_loadUInt256(address(_escrow), 0)); + } + + function _getStEthLockedShares(IEscrow _escrow) internal view returns (uint128) { + return uint128(_loadUInt256(address(_escrow), 1)); + } + + function _getClaimedEth(IEscrow _escrow) internal view returns (uint128) { + return uint128(_loadUInt256(address(_escrow), 1) >> 128); + } + + function _getUnfinalizedShares(IEscrow _escrow) internal view returns (uint128) { + return uint128(_loadUInt256(address(_escrow), 2)); + } + + function _getFinalizedEth(IEscrow _escrow) internal view returns (uint128) { + return uint128(_loadUInt256(address(_escrow), 2) >> 128); + } + + function _getLastAssetsLockTimestamp(IEscrow _escrow, address _vetoer) internal view returns (uint256) { + uint256 assetsSlot = 3; + uint256 vetoerAddressPadded = uint256(uint160(_vetoer)); + bytes32 vetoerAssetsSlot = keccak256(abi.encodePacked(vetoerAddressPadded, assetsSlot)); + uint256 lastAssetsLockTimestampSlot = uint256(vetoerAssetsSlot) + 1; + return _loadUInt256(address(_escrow), lastAssetsLockTimestampSlot); + } + + function _getBatchesQueueStatus(IEscrow _escrow) internal view returns (uint8) { + return uint8(_loadUInt256(address(_escrow), 5)); + } + + function _getRageQuitExtensionDelay(IEscrow _escrow) internal view returns (uint32) { + return uint32(_loadUInt256(address(_escrow), 9)); + } + + function _getRageQuitWithdrawalsTimelock(IEscrow _escrow) internal view returns (uint32) { + return uint32(_loadUInt256(address(_escrow), 9) >> 32); + } + + function _getRageQuitTimelockStartedAt(IEscrow _escrow) internal view returns (uint40) { + return uint40(_loadUInt256(address(_escrow), 9) >> 64); + } + + struct AccountingRecord { + EscrowState escrowState; + uint256 allowance; + uint256 userBalance; + uint256 escrowBalance; + uint256 userShares; + uint256 escrowShares; + uint256 userSharesLocked; + uint256 totalSharesLocked; + uint256 totalEth; + uint256 userUnstEthLockedShares; + uint256 unfinalizedShares; + Timestamp userLastLockedTime; + } + + struct EscrowRecord { + EscrowState escrowState; + AccountingRecord accounting; + } + + function saveEscrowRecord(address user, Escrow escrow) external view returns (EscrowRecord memory er) { + AccountingRecord memory accountingRecord = this.saveAccountingRecord(user, escrow); + er.escrowState = EscrowState(_getCurrentState(escrow)); + er.accounting = accountingRecord; + } + + function saveAccountingRecord(address user, Escrow escrow) external view returns (AccountingRecord memory ar) { + IStETH stEth = escrow.ST_ETH(); + ar.allowance = stEth.allowance(user, address(escrow)); + ar.userBalance = stEth.balanceOf(user); + ar.escrowBalance = stEth.balanceOf(address(escrow)); + ar.userShares = stEth.sharesOf(user); + ar.escrowShares = stEth.sharesOf(address(escrow)); + ar.userSharesLocked = escrow.getVetoerState(user).stETHLockedShares; + ar.totalSharesLocked = escrow.getLockedAssetsTotals().stETHLockedShares; + ar.totalEth = stEth.getPooledEthByShares(ar.totalSharesLocked); + ar.userUnstEthLockedShares = escrow.getVetoerState(user).unstETHLockedShares; + ar.unfinalizedShares = escrow.getLockedAssetsTotals().unstETHUnfinalizedShares; + uint256 lastAssetsLockTimestamp = _getLastAssetsLockTimestamp(escrow, user); + require(lastAssetsLockTimestamp < timeUpperBound, "lastAssetsLockTimestamp >= timeUpperBound"); + ar.userLastLockedTime = Timestamp.wrap(uint40(lastAssetsLockTimestamp)); + } + + function establishEqualAccountingRecords( + Mode mode, + AccountingRecord memory ar1, + AccountingRecord memory ar2 + ) external view { + _establish(mode, ar1.allowance == ar2.allowance); + _establish(mode, ar1.userBalance == ar2.userBalance); + _establish(mode, ar1.escrowBalance == ar2.escrowBalance); + _establish(mode, ar1.userShares == ar2.userShares); + _establish(mode, ar1.escrowShares == ar2.escrowShares); + _establish(mode, ar1.userSharesLocked == ar2.userSharesLocked); + _establish(mode, ar1.totalSharesLocked == ar2.totalSharesLocked); + _establish(mode, ar1.totalEth == ar2.totalEth); + _establish(mode, ar1.userUnstEthLockedShares == ar2.userUnstEthLockedShares); + _establish(mode, ar1.unfinalizedShares == ar2.unfinalizedShares); + _establish(mode, ar1.userLastLockedTime == ar2.userLastLockedTime); + } + + function escrowStorageSetup(IEscrow _escrow, DualGovernance _dualGovernance, EscrowState _currentState) external { + kevm.symbolicStorage(address(_escrow)); + // Slot 0 + { + bytes memory slot0Abi = abi.encodePacked(uint88(0), uint160(address(_dualGovernance)), uint8(_currentState)); + bytes32 slot0; + assembly { + slot0 := mload(add(slot0Abi, 0x20)) + } + _storeBytes32(address(_escrow), 0, slot0); + } + // Slot 1 + 0 + 0 = 1 + { + uint128 lockedShares = uint128(kevm.freshUInt(16)); + vm.assume(lockedShares < ethUpperBound); + uint128 claimedEth = uint128(kevm.freshUInt(16)); + vm.assume(claimedEth < ethUpperBound); + bytes memory slot1Abi = abi.encodePacked(uint128(claimedEth), uint128(lockedShares)); + bytes32 slot1; + assembly { + slot1 := mload(add(slot1Abi, 0x20)) + } + _storeBytes32(address(_escrow), 1, slot1); + } + // Slot 1 + 1 + 0 = 2 + { + uint128 unfinalizedShares = uint128(kevm.freshUInt(16)); + vm.assume(unfinalizedShares < ethUpperBound); + uint128 finalizedEth = uint128(kevm.freshUInt(16)); + vm.assume(finalizedEth < ethUpperBound); + bytes memory slot2Abi = abi.encodePacked(uint128(finalizedEth), uint128(unfinalizedShares)); + bytes32 slot2; + assembly { + slot2 := mload(add(slot2Abi, 0x20)) + } + _storeBytes32(address(_escrow), 2, slot2); + } + // Slot 5 + // FIXME: This branching is done to avoid the fresh existential generation bug + if (_currentState == EscrowState.RageQuitEscrow) { + uint8 batchesQueueStatus = uint8(kevm.freshUInt(1)); + vm.assume(batchesQueueStatus < 3); + _storeUInt256(address(_escrow), 5, batchesQueueStatus); + } else { + _storeUInt256(address(_escrow), 5, 0); + } + // Slot 8 + if (_currentState == EscrowState.RageQuitEscrow) { + uint256 batchesQueueLength = uint256(kevm.freshUInt(32)); + vm.assume(batchesQueueLength < 2 ** 64); + _storeUInt256(address(_escrow), 8, batchesQueueLength); + } else { + _storeUInt256(address(_escrow), 8, 0); + } + // Slot 9 + // FIXME: This branching is done to avoid the fresh existential generation bug + if (_currentState == EscrowState.RageQuitEscrow) { + uint32 rageQuitExtensionDelay = uint32(kevm.freshUInt(4)); + vm.assume(rageQuitExtensionDelay <= block.timestamp); + vm.assume(rageQuitExtensionDelay < timeUpperBound); + uint32 rageQuitWithdrawalsTimelock = uint32(kevm.freshUInt(4)); + vm.assume(rageQuitWithdrawalsTimelock <= block.timestamp); + vm.assume(rageQuitWithdrawalsTimelock < timeUpperBound); + uint40 rageQuitTimelockStartedAt = uint40(kevm.freshUInt(5)); + vm.assume(rageQuitTimelockStartedAt <= block.timestamp); + vm.assume(rageQuitTimelockStartedAt < timeUpperBound); + bytes memory slot9Abi = abi.encodePacked( + uint152(0), + uint40(rageQuitTimelockStartedAt), + uint32(rageQuitWithdrawalsTimelock), + uint32(rageQuitExtensionDelay) + ); + bytes32 slot9; + assembly { + slot9 := mload(add(slot9Abi, 0x20)) + } + _storeBytes32(address(_escrow), 9, slot9); + } else { + _storeUInt256(address(_escrow), 9, 0); + } + } + + function escrowStorageInvariants(Mode mode, IEscrow _escrow) external { + uint8 batchesQueueStatus = _getBatchesQueueStatus(_escrow); + uint32 rageQuitExtensionDelay = _getRageQuitExtensionDelay(_escrow); + uint32 rageQuitWithdrawalsTimelock = _getRageQuitWithdrawalsTimelock(_escrow); + uint40 rageQuitTimelockStartedAt = _getRageQuitTimelockStartedAt(_escrow); + + _establish(mode, batchesQueueStatus < 3); + _establish(mode, rageQuitExtensionDelay <= block.timestamp); + _establish(mode, rageQuitWithdrawalsTimelock <= block.timestamp); + _establish(mode, rageQuitTimelockStartedAt <= block.timestamp); + } + + function escrowAssumeBounds(IEscrow _escrow) external { + uint128 lockedShares = _getStEthLockedShares(_escrow); + uint128 claimedEth = _getClaimedEth(_escrow); + uint128 unfinalizedShares = _getUnfinalizedShares(_escrow); + uint128 finalizedEth = _getFinalizedEth(_escrow); + uint32 rageQuitExtensionDelay = _getRageQuitExtensionDelay(_escrow); + uint32 rageQuitWithdrawalsTimelock = _getRageQuitWithdrawalsTimelock(_escrow); + uint40 rageQuitTimelockStartedAt = _getRageQuitTimelockStartedAt(_escrow); + + vm.assume(lockedShares < ethUpperBound); + vm.assume(claimedEth < ethUpperBound); + vm.assume(unfinalizedShares < ethUpperBound); + vm.assume(finalizedEth < ethUpperBound); + vm.assume(rageQuitExtensionDelay < timeUpperBound); + vm.assume(rageQuitWithdrawalsTimelock < timeUpperBound); + vm.assume(rageQuitTimelockStartedAt < timeUpperBound); + } + + function escrowInitializeStorage( + IEscrow _escrow, + DualGovernance _dualGovernance, + EscrowState _currentState + ) external { + this.escrowStorageSetup(_escrow, _dualGovernance, _currentState); + this.escrowStorageInvariants(Mode.Assume, _escrow); + this.escrowAssumeBounds(_escrow); + } + + function signallingEscrowStorageInvariants(Mode mode, IEscrow _signallingEscrow) external { + uint32 rageQuitExtensionDelay = _getRageQuitExtensionDelay(_signallingEscrow); + uint32 rageQuitWithdrawalsTimelock = _getRageQuitWithdrawalsTimelock(_signallingEscrow); + uint40 rageQuitTimelockStartedAt = _getRageQuitTimelockStartedAt(_signallingEscrow); + uint8 batchesQueueStatus = _getBatchesQueueStatus(_signallingEscrow); + + _establish(mode, rageQuitExtensionDelay == 0); + _establish(mode, rageQuitWithdrawalsTimelock == 0); + _establish(mode, rageQuitTimelockStartedAt == 0); + _establish(mode, batchesQueueStatus == uint8(WithdrawalsBatchesQueue.Status.Empty)); + } + + function signallingEscrowInitializeStorage(IEscrow _signallingEscrow, DualGovernance _dualGovernance) external { + this.escrowInitializeStorage(_signallingEscrow, _dualGovernance, EscrowState.SignallingEscrow); + this.signallingEscrowStorageInvariants(Mode.Assume, _signallingEscrow); + } + + function rageQuitEscrowStorageInvariants(Mode mode, IEscrow _rageQuitEscrow) external { + uint8 batchesQueueStatus = _getBatchesQueueStatus(_rageQuitEscrow); + + _establish(mode, batchesQueueStatus != uint8(WithdrawalsBatchesQueue.Status.Empty)); + } + + function rageQuitEscrowInitializeStorage(IEscrow _rageQuitEscrow, DualGovernance _dualGovernance) external { + this.escrowInitializeStorage(_rageQuitEscrow, _dualGovernance, EscrowState.RageQuitEscrow); + this.rageQuitEscrowStorageInvariants(Mode.Assume, _rageQuitEscrow); + } +} diff --git a/test/kontrol/VetoCooldown.t.sol b/test/kontrol/VetoCooldown.t.sol new file mode 100644 index 00000000..c4c029bf --- /dev/null +++ b/test/kontrol/VetoCooldown.t.sol @@ -0,0 +1,23 @@ +pragma solidity 0.8.23; + +import "forge-std/Vm.sol"; +import "kontrol-cheatcodes/KontrolCheats.sol"; + +import {addTo, Duration, Durations} from "contracts/types/Duration.sol"; +import {Timestamp, Timestamps} from "contracts/types/Timestamp.sol"; + +import "test/kontrol/DualGovernanceSetUp.sol"; + +contract VetoCooldownTest is DualGovernanceSetUp { + function testVetoCooldownDuration() external { + vm.assume(dualGovernance.getCurrentState() == State.VetoCooldown); + Timestamp timeEnteredAt = Timestamp.wrap(_getEnteredAt(dualGovernance)); + Timestamp maxCooldownDuration = addTo(config.VETO_COOLDOWN_DURATION(), timeEnteredAt); + + dualGovernance.activateNextState(); + + bool stillInVetoCooldown = (dualGovernance.getCurrentState() == State.VetoCooldown); + bool durationHasElapsed = (Timestamps.now() > maxCooldownDuration); + assert(stillInVetoCooldown != durationHasElapsed); + } +} diff --git a/test/kontrol/VetoSignalling.t.sol b/test/kontrol/VetoSignalling.t.sol index 0db58bd3..89535a8c 100644 --- a/test/kontrol/VetoSignalling.t.sol +++ b/test/kontrol/VetoSignalling.t.sol @@ -1,216 +1,64 @@ pragma solidity 0.8.23; import "forge-std/Vm.sol"; -import "forge-std/Test.sol"; import "kontrol-cheatcodes/KontrolCheats.sol"; -import "@openzeppelin/contracts/token/ERC20/ERC20.sol"; import "@openzeppelin/contracts/utils/math/Math.sol"; -import "contracts/model/DualGovernance.sol"; -import "contracts/model/EmergencyProtectedTimelock.sol"; -import "contracts/model/Escrow.sol"; +import {State} from "contracts/libraries/DualGovernanceState.sol"; +import {addTo, Duration, Durations} from "contracts/types/Duration.sol"; +import {Timestamp, Timestamps} from "contracts/types/Timestamp.sol"; -contract FakeETH is ERC20("fakeETH", "fETH") {} - -contract VetoSignallingTest is Test, KontrolCheats { - DualGovernance dualGovernance; - EmergencyProtectedTimelock timelock; - ERC20 fakeETH; - Escrow signallingEscrow; - Escrow rageQuitEscrow; - - uint256 constant CURRENT_STATE_SLOT = 3; - uint256 constant CURRENT_STATE_OFFSET = 160; - - // 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 view { - if (mode == Mode.Assume) { - vm.assume(condition); - } else { - assert(condition); - } - } - - function setUp() public { - fakeETH = new FakeETH(); - uint256 emergencyProtectionTimelock = 0; // Regular deployment mode - dualGovernance = new DualGovernance(address(fakeETH), emergencyProtectionTimelock); - timelock = dualGovernance.emergencyProtectedTimelock(); - signallingEscrow = dualGovernance.signallingEscrow(); - rageQuitEscrow = new Escrow(address(dualGovernance), address(fakeETH)); - - _fakeETHStorageSetup(); - _dualGovernanceStorageSetup(); - _signallingEscrowStorageSetup(); - _rageQuitEscrowStorageSetup(); - kevm.symbolicStorage(address(timelock)); // ?STORAGE3 - } - - function _fakeETHStorageSetup() internal { - kevm.symbolicStorage(address(fakeETH)); // ?STORAGE - // Slot 2 - uint256 totalSupply = kevm.freshUInt(32); // ?WORD - vm.assume(0 < totalSupply); - _storeUInt256(address(fakeETH), 2, totalSupply); - } - - function _dualGovernanceStorageSetup() internal { - kevm.symbolicStorage(address(dualGovernance)); // ?STORAGE0 - // 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 - uint8 state = uint8(kevm.freshUInt(1)); // ?WORD0 - vm.assume(state <= 4); - bytes memory slot_3_abi_encoding = abi.encodePacked(uint88(0), state, address(fakeETH)); - bytes32 slot_3_for_storage; - assembly { - slot_3_for_storage := mload(add(slot_3_abi_encoding, 0x20)) - } - _storeBytes32(address(dualGovernance), 3, slot_3_for_storage); - // Slot 6 - uint256 lastStateChangeTime = kevm.freshUInt(32); // ?WORD1 - vm.assume(lastStateChangeTime <= block.timestamp); - _storeUInt256(address(dualGovernance), 6, lastStateChangeTime); - // Slot 7 - uint256 lastSubStateActivationTime = kevm.freshUInt(32); // ?WORD2 - vm.assume(lastSubStateActivationTime <= block.timestamp); - _storeUInt256(address(dualGovernance), 7, lastSubStateActivationTime); - // Slot 8 - uint256 lastStateReactivationTime = kevm.freshUInt(32); // ?WORD3 - vm.assume(lastStateReactivationTime <= block.timestamp); - _storeUInt256(address(dualGovernance), 8, lastStateReactivationTime); - // Slot 9 - uint256 lastVetoSignallingTime = kevm.freshUInt(32); // ?WORD4 - vm.assume(lastVetoSignallingTime <= block.timestamp); - _storeUInt256(address(dualGovernance), 9, lastVetoSignallingTime); - // Slot 10 - uint256 rageQuitSequenceNumber = kevm.freshUInt(32); // ?WORD5 - vm.assume(rageQuitSequenceNumber < type(uint256).max); - _storeUInt256(address(dualGovernance), 10, rageQuitSequenceNumber); - } - - function _signallingEscrowStorageSetup() internal { - kevm.symbolicStorage(address(signallingEscrow)); // ?STORAGE1 - // Slot 0: currentState == 0 (SignallingEscrow), dualGovernance - uint8 currentState = 0; - 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(signallingEscrow), 0, slot_0_for_storage); - // Slot 1 - _storeAddress(address(signallingEscrow), 1, address(fakeETH)); - // Slot 3 - uint256 totalStaked = kevm.freshUInt(32); // ?WORD6 - vm.assume(totalStaked < ethUpperBound); - _storeUInt256(address(signallingEscrow), 3, totalStaked); - // Slot 5 - uint256 totalClaimedEthAmount = kevm.freshUInt(32); // ?WORD7 - vm.assume(totalClaimedEthAmount <= totalStaked); - _storeUInt256(address(signallingEscrow), 5, totalClaimedEthAmount); - // Slot 11 - uint256 rageQuitExtensionDelayPeriodEnd = 0; // since SignallingEscrow - _storeUInt256(address(signallingEscrow), 11, rageQuitExtensionDelayPeriodEnd); - } - - function _rageQuitEscrowStorageSetup() internal { - kevm.symbolicStorage(address(rageQuitEscrow)); // ?STORAGE2 - // Slot 0: currentState == 1 (RageQuitEscrow), dualGovernance - uint8 currentState = 1; - 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(rageQuitEscrow), 0, slot_0_for_storage); - // Slot 1 - _storeAddress(address(rageQuitEscrow), 1, address(fakeETH)); - // Slot 3 - uint256 totalStaked = kevm.freshUInt(32); // ?WORD8 - vm.assume(totalStaked < ethUpperBound); - _storeUInt256(address(rageQuitEscrow), 3, totalStaked); - // Slot 5 - uint256 totalClaimedEthAmount = kevm.freshUInt(32); // ?WORD9 - vm.assume(totalClaimedEthAmount <= totalStaked); - _storeUInt256(address(rageQuitEscrow), 5, totalClaimedEthAmount); - // Slot 11 - uint256 rageQuitExtensionDelayPeriodEnd = kevm.freshUInt(32); // ?WORD10 - _storeUInt256(address(rageQuitEscrow), 11, rageQuitExtensionDelayPeriodEnd); - } - - 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)))); - } +import "test/kontrol/DualGovernanceSetUp.sol"; +contract VetoSignallingTest is DualGovernanceSetUp { /** * Test that the Normal state transitions to VetoSignalling if the total * veto power in the signalling escrow exceeds the first seal threshold. */ function testTransitionNormalToVetoSignalling() external { uint256 rageQuitSupport = signallingEscrow.getRageQuitSupport(); - vm.assume(rageQuitSupport > dualGovernance.FIRST_SEAL_RAGE_QUIT_SUPPORT()); - vm.assume(dualGovernance.currentState() == DualGovernance.State.Normal); + vm.assume(rageQuitSupport >= config.FIRST_SEAL_RAGE_QUIT_SUPPORT()); + vm.assume(dualGovernance.getCurrentState() == State.Normal); dualGovernance.activateNextState(); - assert(dualGovernance.currentState() == DualGovernance.State.VetoSignalling); + assert(dualGovernance.getCurrentState() == State.VetoSignalling); } struct StateRecord { - DualGovernance.State state; - uint256 timestamp; + State state; + Timestamp timestamp; uint256 rageQuitSupport; uint256 maxRageQuitSupport; - uint256 activationTime; - uint256 reactivationTime; + Timestamp activationTime; + Timestamp reactivationTime; } /** * Invariants that should hold while in the Veto Signalling state * (including Deactivation sub-state) */ - function _vetoSignallingInvariants(Mode mode, StateRecord memory sr) internal view { + function _vetoSignallingInvariants(Mode mode, StateRecord memory sr) internal view returns (bool) { require( - sr.state != DualGovernance.State.Normal && sr.state != DualGovernance.State.VetoCooldown - && sr.state != DualGovernance.State.RageQuit, + sr.state != State.Normal && sr.state != State.VetoCooldown && sr.state != State.RageQuit, "Invariants only apply to the Veto Signalling states." ); - _vetoSignallingTimesInvariant(mode, sr); - _vetoSignallingRageQuitInvariant(mode, sr); - _vetoSignallingDeactivationInvariant(mode, sr); - _vetoSignallingMaxDelayInvariant(mode, sr); + return ( + _vetoSignallingTimesInvariant(mode, sr) && _vetoSignallingRageQuitInvariant(mode, sr) + && _vetoSignallingDeactivationInvariant(mode, sr) && _vetoSignallingMaxDelayInvariant(mode, sr) + ); } /** * Veto Signalling Invariant: At any given point t up to the present time, * the Veto Signalling activation and reactivation times must be before t. */ - function _vetoSignallingTimesInvariant(Mode mode, StateRecord memory sr) internal view { - _establish(mode, sr.timestamp <= block.timestamp); - _establish(mode, sr.activationTime <= sr.timestamp); - _establish(mode, sr.reactivationTime <= sr.timestamp); + function _vetoSignallingTimesInvariant(Mode mode, StateRecord memory sr) internal view returns (bool) { + return ( + _establish(mode, sr.timestamp <= Timestamps.now()) && _establish(mode, sr.activationTime <= sr.timestamp) + && _establish(mode, sr.reactivationTime <= sr.timestamp) + && _establish(mode, sr.reactivationTime <= addTo(config.DYNAMIC_TIMELOCK_MAX_DURATION(), sr.activationTime)) + ); } /** @@ -219,9 +67,35 @@ contract VetoSignallingTest is Test, KontrolCheats { * and the maximum rage quit support must be greater than the first seal * threshold. */ - function _vetoSignallingRageQuitInvariant(Mode mode, StateRecord memory sr) internal view { - _establish(mode, sr.rageQuitSupport <= sr.maxRageQuitSupport); - _establish(mode, dualGovernance.FIRST_SEAL_RAGE_QUIT_SUPPORT() < sr.maxRageQuitSupport); + function _vetoSignallingRageQuitInvariant(Mode mode, StateRecord memory sr) internal view returns (bool) { + return ( + _establish(mode, sr.rageQuitSupport <= sr.maxRageQuitSupport) + && _establish(mode, config.FIRST_SEAL_RAGE_QUIT_SUPPORT() <= sr.maxRageQuitSupport) + ); + } + + function _calculateDynamicTimelock(Configuration _config, uint256 rageQuitSupport) public view returns (Duration) { + if (rageQuitSupport < _config.FIRST_SEAL_RAGE_QUIT_SUPPORT()) { + return Durations.ZERO; + } else if (rageQuitSupport < _config.SECOND_SEAL_RAGE_QUIT_SUPPORT()) { + return _linearInterpolation(_config, rageQuitSupport); + } else { + return _config.DYNAMIC_TIMELOCK_MAX_DURATION(); + } + } + + function _linearInterpolation(Configuration _config, uint256 rageQuitSupport) private view returns (Duration) { + uint32 L_min = Duration.unwrap(_config.DYNAMIC_TIMELOCK_MIN_DURATION()); + uint32 L_max = Duration.unwrap(_config.DYNAMIC_TIMELOCK_MAX_DURATION()); + uint256 interpolation = L_min + + ((rageQuitSupport - _config.FIRST_SEAL_RAGE_QUIT_SUPPORT()) * (L_max - L_min)) + / (_config.SECOND_SEAL_RAGE_QUIT_SUPPORT() - _config.FIRST_SEAL_RAGE_QUIT_SUPPORT()); + assert(interpolation <= type(uint32).max); + return Duration.wrap(uint32(interpolation)); + } + + function _maxTimestamp(Timestamp t1, Timestamp t2) internal pure returns (Timestamp) { + return Timestamp.wrap(uint40(Math.max(Timestamp.unwrap(t1), Timestamp.unwrap(t2)))); } /** @@ -230,20 +104,22 @@ contract VetoSignallingTest is Test, KontrolCheats { * the Deactivation sub-state was last exited have passed, the protocol is * in the Deactivation sub-state. Otherwise, it is in the parent state. */ - function _vetoSignallingDeactivationInvariant(Mode mode, StateRecord memory sr) internal view { - uint256 dynamicTimelock = dualGovernance.calculateDynamicTimelock(sr.rageQuitSupport); + function _vetoSignallingDeactivationInvariant(Mode mode, StateRecord memory sr) internal view returns (bool) { + Duration dynamicTimelock = _calculateDynamicTimelock(config, sr.rageQuitSupport); // Note: creates three branches in symbolic execution - if (sr.timestamp <= sr.activationTime + dynamicTimelock) { - _establish(mode, sr.state == DualGovernance.State.VetoSignalling); - } else if ( + if (sr.timestamp <= addTo(dynamicTimelock, sr.activationTime)) { + return _establish(mode, sr.state == State.VetoSignalling); + } + if ( sr.timestamp - <= Math.max(sr.reactivationTime, sr.activationTime) + dualGovernance.VETO_SIGNALLING_MIN_ACTIVE_DURATION() + <= addTo( + config.VETO_SIGNALLING_MIN_ACTIVE_DURATION(), _maxTimestamp(sr.activationTime, sr.reactivationTime) + ) ) { - _establish(mode, sr.state == DualGovernance.State.VetoSignalling); - } else { - _establish(mode, sr.state == DualGovernance.State.VetoSignallingDeactivation); + return _establish(mode, sr.state == State.VetoSignalling); } + return _establish(mode, sr.state == State.VetoSignallingDeactivation); } /** @@ -256,41 +132,42 @@ contract VetoSignallingTest is Test, KontrolCheats { * - D is the minimum active duration before the Deactivation sub-state can * be re-entered. */ - function _vetoSignallingMaxDelayInvariant(Mode mode, StateRecord memory sr) internal view { + function _vetoSignallingMaxDelayInvariant(Mode mode, StateRecord memory sr) internal view returns (bool) { // Note: creates two branches in symbolic execution if (_maxDeactivationDelayPassed(sr)) { - _establish(mode, sr.state == DualGovernance.State.VetoSignallingDeactivation); + return _establish(mode, sr.state == State.VetoSignallingDeactivation); } + return true; } function _maxDeactivationDelayPassed(StateRecord memory sr) internal view returns (bool) { - uint256 maxDeactivationDelay = dualGovernance.calculateDynamicTimelock(sr.maxRageQuitSupport) - + dualGovernance.VETO_SIGNALLING_MIN_ACTIVE_DURATION(); + Duration maxDeactivationDelay = + _calculateDynamicTimelock(config, sr.maxRageQuitSupport) + config.VETO_SIGNALLING_MIN_ACTIVE_DURATION(); - return sr.activationTime + maxDeactivationDelay < sr.timestamp; + return addTo(maxDeactivationDelay, sr.activationTime) < sr.timestamp; } function _recordPreviousState( - uint256 lastInteractionTimestamp, + Timestamp lastInteractionTimestamp, uint256 previousRageQuitSupport, uint256 maxRageQuitSupport ) internal view returns (StateRecord memory sr) { - sr.state = dualGovernance.currentState(); + sr.state = dualGovernance.getCurrentState(); sr.timestamp = lastInteractionTimestamp; sr.rageQuitSupport = previousRageQuitSupport; sr.maxRageQuitSupport = maxRageQuitSupport; - sr.activationTime = dualGovernance.lastStateChangeTime(); - sr.reactivationTime = dualGovernance.lastStateReactivationTime(); + sr.activationTime = Timestamp.wrap(_getVetoSignallingActivationTime(dualGovernance)); + sr.reactivationTime = Timestamp.wrap(_getVetoSignallingReactivationTime(dualGovernance)); } function _recordCurrentState(uint256 previousMaxRageQuitSupport) internal view returns (StateRecord memory sr) { - sr.state = dualGovernance.currentState(); - sr.timestamp = block.timestamp; + sr.state = dualGovernance.getCurrentState(); + sr.timestamp = Timestamps.now(); sr.rageQuitSupport = signallingEscrow.getRageQuitSupport(); sr.maxRageQuitSupport = previousMaxRageQuitSupport < sr.rageQuitSupport ? sr.rageQuitSupport : previousMaxRageQuitSupport; - sr.activationTime = dualGovernance.lastStateChangeTime(); - sr.reactivationTime = dualGovernance.lastStateReactivationTime(); + sr.activationTime = Timestamp.wrap(_getVetoSignallingActivationTime(dualGovernance)); + sr.reactivationTime = Timestamp.wrap(_getVetoSignallingReactivationTime(dualGovernance)); } /** @@ -316,15 +193,14 @@ contract VetoSignallingTest is Test, KontrolCheats { function testVetoSignallingInvariantsHoldInitially() external { vm.assume(block.timestamp < timeUpperBound); - vm.assume(dualGovernance.currentState() != DualGovernance.State.VetoSignalling); - vm.assume(dualGovernance.currentState() != DualGovernance.State.VetoSignallingDeactivation); + vm.assume(dualGovernance.getCurrentState() != State.VetoSignalling); + vm.assume(dualGovernance.getCurrentState() != State.VetoSignallingDeactivation); dualGovernance.activateNextState(); - StateRecord memory sr = _recordCurrentState(0); - // Consider only the case where we have transitioned to Veto Signalling - if (sr.state == DualGovernance.State.VetoSignalling) { + if (dualGovernance.getCurrentState() == State.VetoSignalling) { + StateRecord memory sr = _recordCurrentState(0); _vetoSignallingInvariants(Mode.Assert, sr); } } @@ -345,24 +221,62 @@ contract VetoSignallingTest is Test, KontrolCheats { vm.assume(previousRageQuitSupport < ethUpperBound); vm.assume(maxRageQuitSupport < ethUpperBound); - StateRecord memory previous = - _recordPreviousState(lastInteractionTimestamp, previousRageQuitSupport, maxRageQuitSupport); + StateRecord memory previous = _recordPreviousState( + Timestamp.wrap(uint40(lastInteractionTimestamp)), previousRageQuitSupport, maxRageQuitSupport + ); - vm.assume(previous.state != DualGovernance.State.Normal); - vm.assume(previous.state != DualGovernance.State.VetoCooldown); - vm.assume(previous.state != DualGovernance.State.RageQuit); + vm.assume(previous.state != State.Normal); + vm.assume(previous.state != State.VetoCooldown); + vm.assume(previous.state != State.RageQuit); - _vetoSignallingInvariants(Mode.Assume, previous); - dualGovernance.activateNextState(); + // Assume the first two invariants, which are non-branching + _vetoSignallingTimesInvariant(Mode.Assume, previous); + _vetoSignallingRageQuitInvariant(Mode.Assume, previous); - StateRecord memory current = _recordCurrentState(maxRageQuitSupport); + dualGovernance.activateNextState(); - if ( - current.state != DualGovernance.State.Normal && current.state != DualGovernance.State.VetoCooldown - && current.state != DualGovernance.State.RageQuit - ) { - _vetoSignallingInvariants(Mode.Assert, current); + State currentState = dualGovernance.getCurrentState(); + + if (currentState != State.Normal && currentState != State.VetoCooldown && currentState != State.RageQuit) { + bool assumedDeactivationInvariant = false; + bool assumedMaxDelayInvariant = false; + + StateRecord memory current = _recordCurrentState(maxRageQuitSupport); + + // First two invariants can be established immediately + _vetoSignallingTimesInvariant(Mode.Assert, current); + _vetoSignallingRageQuitInvariant(Mode.Assert, current); + + // Try establishing third invariant + if (!_vetoSignallingDeactivationInvariant(Mode.Try, current)) { + // Assume third invariant + assumedDeactivationInvariant = true; + _vetoSignallingDeactivationInvariant(Mode.Assume, previous); + // Assume fourth invariant only if initial state is VetoSignalling, + // because fourth invariant can only cut VetoSignalling initial states + if (previous.state == State.VetoSignalling) { + assumedMaxDelayInvariant = true; + _vetoSignallingMaxDelayInvariant(Mode.Assume, previous); + } + // Establish third invariant + _vetoSignallingDeactivationInvariant(Mode.Assert, current); + if (!_vetoSignallingMaxDelayInvariant(Mode.Try, current)) { + // Assume fourth invariant if not already assumed + if (!assumedMaxDelayInvariant) { + _vetoSignallingMaxDelayInvariant(Mode.Assume, previous); + } + // If we still fail, it means that we have not assumed the third invariant, + // which has to eliminate all of the remaining branches + if (!_vetoSignallingMaxDelayInvariant(Mode.Try, current)) { + assert(!assumedDeactivationInvariant); + _vetoSignallingDeactivationInvariant(Mode.Assume, previous); + assert(false); + } + } + } + return; } + vm.assume(currentState == State.VetoSignalling || currentState == State.VetoSignallingDeactivation); } /** @@ -377,36 +291,38 @@ contract VetoSignallingTest is Test, KontrolCheats { uint256 maxRageQuitSupport ) external { vm.assume(block.timestamp < timeUpperBound); + vm.assume(lastInteractionTimestamp < timeUpperBound); + vm.assume(signallingEscrow.getRageQuitSupport() <= maxRageQuitSupport); + vm.assume(maxRageQuitSupport < config.SECOND_SEAL_RAGE_QUIT_SUPPORT()); - StateRecord memory previous = - _recordPreviousState(lastInteractionTimestamp, previousRageQuitSupport, maxRageQuitSupport); + StateRecord memory previous = _recordPreviousState( + Timestamp.wrap(uint40(lastInteractionTimestamp)), previousRageQuitSupport, maxRageQuitSupport + ); - vm.assume(previous.maxRageQuitSupport <= dualGovernance.SECOND_SEAL_RAGE_QUIT_SUPPORT()); - vm.assume(_maxDeactivationDelayPassed(previous)); - vm.assume(signallingEscrow.getRageQuitSupport() <= previous.maxRageQuitSupport); + Timestamp deactivationStartTime = Timestamp.wrap(_getEnteredAt(dualGovernance)); + Timestamp deactivationEndTime = addTo(config.VETO_SIGNALLING_DEACTIVATION_MAX_DURATION(), deactivationStartTime); - vm.assume( - previous.state == DualGovernance.State.VetoSignalling - || previous.state == DualGovernance.State.VetoSignallingDeactivation - ); + vm.assume(previous.state != State.Normal); + vm.assume(previous.state != State.VetoCooldown); + vm.assume(previous.state != State.RageQuit); - _vetoSignallingInvariants(Mode.Assume, previous); + _vetoSignallingTimesInvariant(Mode.Assume, previous); + _vetoSignallingRageQuitInvariant(Mode.Assume, previous); + vm.assume(_maxDeactivationDelayPassed(previous)); + _vetoSignallingMaxDelayInvariant(Mode.Assume, previous); - assert(previous.state == DualGovernance.State.VetoSignallingDeactivation); + assert(previous.state == State.VetoSignallingDeactivation); dualGovernance.activateNextState(); - StateRecord memory current = _recordCurrentState(maxRageQuitSupport); - - uint256 deactivationStartTime = dualGovernance.lastSubStateActivationTime(); - uint256 deactivationEndTime = deactivationStartTime + dualGovernance.VETO_SIGNALLING_DEACTIVATION_MAX_DURATION(); + State currentState = dualGovernance.getCurrentState(); // The protocol is either in the Deactivation sub-state, or, if the // maximum deactivation duration has passed, in the Veto Cooldown state - if (deactivationEndTime < block.timestamp) { - assert(current.state == DualGovernance.State.VetoCooldown); + if (deactivationEndTime < Timestamps.now()) { + assert(currentState == State.VetoCooldown); } else { - assert(current.state == DualGovernance.State.VetoSignallingDeactivation); + assert(currentState == State.VetoSignallingDeactivation); } } } diff --git a/test/kontrol/lido-lemmas.k b/test/kontrol/lido-lemmas.k index 65da0a19..a8bda5d8 100644 --- a/test/kontrol/lido-lemmas.k +++ b/test/kontrol/lido-lemmas.k @@ -1,6 +1,8 @@ +requires "evm.md" requires "foundry.md" -module LIDO-LEMMAS +module LIDO-LEMMAS [symbolic] + imports EVM imports FOUNDRY imports INT-SYMBOLIC imports MAP-SYMBOLIC @@ -9,6 +11,7 @@ module LIDO-LEMMAS syntax StepSort ::= Int | Bool | Bytes + | Map | Set // ------------------------- @@ -17,200 +20,75 @@ module LIDO-LEMMAS // -------------------------------------- rule runLemma(T) => doneLemma(T) ... - syntax Int ::= "ethMaxWidth" [macro] - syntax Int ::= "ethUpperBound" [macro] - // -------------------------------------- - rule ethMaxWidth => 96 - rule ethUpperBound => 2 ^Int ethMaxWidth - // ---------------------------------------- - - // /Int to byte representation - rule X /Int pow160 => #asWord ( #range ( #buf ( 32 , X ) , 0 , 12 ) ) - requires #rangeUInt(256, X) - [simplification, preserves-definedness] + rule C <=Int A *Int B => C /Int A <=Int B + requires 0 <=Int C andBool 0 - #asWord ( #range(#buf(32, X), 0, 11) +Bytes #buf(1, 0) +Bytes #range(#buf(32, X), 12, 20) ) - requires #rangeUInt(256, X) - [simplification] - - // |Int distributivity over #asWord and +Bytes, v1 - rule A |Int #asWord ( BA1 +Bytes BA2 ) => - #asWord ( BA1 +Bytes #buf ( lengthBytes(BA2), A |Int #asWord ( BA2 ) ) ) - requires 0 <=Int A andBool A - #asWord ( - #buf ( lengthBytes(BA1), (A >>Int (8 *Int lengthBytes(BA2))) |Int #asWord ( BA1 ) ) - +Bytes - #buf ( lengthBytes(BA2), (A modInt (2 ^Int (8 *Int lengthBytes(BA2)))) |Int #asWord ( BA2 ) ) - ) - requires #rangeUInt(256, A) - [simplification, concrete(A, BA1)] - - // |Int and #asWord - rule #range ( #buf ( A, X |Int Y) , 0, B ) => - #buf ( B, X >>Int (8 *Int (A -Int B)) ) - requires B <=Int A - andBool 0 <=Int X andBool X A ==Int (-1) *Int B - requires #rangeUInt(256, A) andBool #rangeUInt(256, (-1) *Int B) - [concrete(B), simplification, comm] - - // *Int - rule A *Int B ==Int 0 => A ==Int 0 orBool B ==Int 0 [simplification] - - // /Int - rule 0 /Int B => 0 requires B =/=Int 0 [simplification, preserves-definedness] - rule A /Int B ==Int 0 => A ==Int 0 requires B =/=Int 0 [simplification, preserves-definedness] - - // /Word - rule _ /Word W1 => 0 requires W1 ==Int 0 [simplification] - rule W0 /Word W1 => W0 /Int W1 requires W1 =/=Int 0 [simplification, preserves-definedness] - - // Further arithmetic - rule ( X *Int Y ) /Int Y => X requires Y =/=Int 0 [simplification, preserves-definedness] - rule ( X ==Int ( X *Int Y ) /Word Y ) orBool Y ==Int 0 => true [simplification, preserves-definedness] - - rule A <=Int B /Int C => A *Int C <=Int B requires 0 (A +Int 1) *Int C <=Int B requires 0 Int B /Int C => A *Int C >Int B requires 0 =Int B /Int C => (A +Int 1) *Int C >Int B requires 0 =Int A => A *Int C <=Int B requires 0 Int A => (A +Int 1) *Int C <=Int B requires 0 A *Int C >Int B requires 0 (A +Int 1) *Int C >Int B requires 0 #asWord ( #range(BA, lengthBytes(BA) -Int (log2Int(X +Int 1) /Int 8), log2Int(X +Int 1) /Int 8) ) - requires #rangeUInt(256, X) - andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1) - andBool log2Int (X +Int 1) modInt 8 ==Int 0 - andBool (log2Int (X +Int 1)) /Int 8 <=Int lengthBytes(BA) andBool lengthBytes(BA) <=Int 32 - [simplification, concrete(X), preserves-definedness] - - // &Int distributivity - rule X &Int ( Y |Int Z ) => ( X &Int Y ) |Int ( X &Int Z ) [simplification, concrete(X)] - rule X &Int ( Y &Int Z ) => ( X &Int Y ) &Int ( X &Int Z ) [simplification, concrete(X)] - - // KEVM simplification - rule #asWord(WS) >>Int M => #asWord(#range(WS, 0, lengthBytes(WS) -Int (M /Int 8) )) - requires 0 <=Int M andBool M modInt 8 ==Int 0 - [simplification, preserves-definedness] + rule A ==Int B => false + requires 0 <=Int A andBool B true [simplification, comm] + rule 0 <=Int A -Int B => B <=Int A + [simplification, symbolic(A, B)] - rule b"" ==K #buf(X, _) +Bytes _ => false requires 0 false requires 0 false requires 0 false requires 0 ( ( ( A /Int 10 ) *Int B ) +Int ( ( D /Int 10 ) -Int 1 ) ) /Int ( D /Int 10 ) + requires 0 <=Int A andBool 0 B:Bytes [simplification] - rule [concat-neutral-right]: B:Bytes +Bytes b"" => B:Bytes [simplification] + rule [asWord-lt-concat-left]: + #asWord ( BA1 +Bytes BA2 ) #asWord ( BA1 ) B1 +Bytes (B2 [ S -Int lengthBytes(B1) := B ]) - requires lengthBytes(B1) <=Int S - [simplification(40)] - rule [memUpdate-concat-in-left]: (B1 +Bytes B2) [ S := B ] => (B1 [S := B]) +Bytes B2 - requires 0 <=Int S andBool S +Int lengthBytes(B) <=Int lengthBytes(B1) - [simplification(45)] + // rule [create-valid-enhanced]: + // CREATE VALUE MEMSTART MEMWIDTH + // => #accessAccounts #newAddr(ACCT, NONCE) + // ~> #checkCreate ACCT VALUE + // ~> #create ACCT #newAddr(ACCT, NONCE) VALUE #range(LM, MEMSTART, MEMWIDTH) + // ~> #codeDeposit #newAddr(ACCT, NONCE) + // ... + // + // ACCT + // LM + // + // + // ACCT + // NONCE + // ... + // + // ACCOUNTS_REST + // + // SCHED + // requires #hasValidInitCode(MEMWIDTH, SCHED) + // ensures notBool ( #newAddr(ACCT, NONCE) ==Int ACCT ) + // andBool notBool ( #newAddr(ACCT, NONCE) in_keys ( ACCOUNTS_REST:AccountCellMap ) ) + // [priority(30), preserves-definedness] // - // Specific simplifications + // Syntactics // - rule X &Int #asWord ( BA ) ==Int Y:Int => true - requires 0 <=Int X andBool X false - requires 0 <=Int X andBool X true - requires 0 <=Int X andBool X false - requires 0 <=Int X andBool X true - requires 0 <=Int X andBool X false - requires 0 <=Int X andBool X 0 - requires 0 <=Int X andBool 0 <=Int Y andBool 0 <=Int Z - andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1) - andBool Y ==Int 2 ^Int log2Int(Y) - andBool log2Int(X +Int 1) <=Int log2Int(Y) - [simplification, concrete(X, Y), preserves-definedness] - - rule X &Int ( Y *Int Z ) => 0 - requires 0 <=Int X andBool 0 <=Int Y andBool 0 <=Int Z - andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1) - andBool Z ==Int 2 ^Int log2Int(Z) - andBool log2Int(X +Int 1) <=Int log2Int(Z) - [simplification, concrete(X, Z), preserves-definedness] - - rule chop ( X *Int Y ) => X *Int Y - requires 0 <=Int X andBool X X *Int Y { true #Equals X *Int Y true [simplification, smt-lemma] + // rule A <=Int B => true requires C <=Int B andBool A <=Int C [simplification, concrete(A, C), syntactic(1)] + // rule A <=Int B => true requires C true requires A <=Int C andBool C <=Int B [simplification, concrete(B, C), syntactic(1)] + // rule A <=Int B => true requires A true requires A true requires A <=Int C andBool C >Int N => X /Int (2 ^Int N) [simplification, concrete(N)] + // rule A true requires C true requires C <=Int B andBool A #asWord ( BUF2 ) - requires #asWord ( BUF1 ) ==Int 0 - [simplification, concrete(BUF1)] + // rule A <=Int B => A true requires B runLemma ( + STORAGE0:Map + [ 5 <- #asWord ( b"\x00E\xc9,,\xd0\xdf{-p^\xf1,\xffw\xcb\x0b\xc5W\xed\"" +Bytes #buf ( 5 , WORD4:Int ) +Bytes #buf ( 5 , WORD3:Int ) +Bytes b"\x00" ) ] + [ 6 <- #asWord ( #buf ( 1 , WORD7:Int ) +Bytes b"\xa4\xadOh\xd0\xb9\x1c\xfd\x19h|\x88\x1eP\xf3\xa0\x02B\x82\x8c" +Bytes #buf ( 5 , WORD6:Int ) +Bytes #buf ( 5 , WORD5:Int ) ) ] + [ 5 <- #asWord ( b"\x00E\xc9,,\xd0\xdf{-p^\xf1,\xffw\xcb\x0b\xc5W\xed\"" +Bytes #buf ( 5 , WORD4:Int ) +Bytes #buf ( 5 , TIMESTAMP_CELL:Int ) +Bytes b"\x01" ) ] + [ 6 <- ( ( TIMESTAMP_CELL:Int *Int pow40 ) |Int ( 115792089237316195423570985008687907853269984665640562830531764394383466561535 &Int #asWord ( #buf ( 1 , WORD7:Int ) +Bytes b"\xa4\xadOh\xd0\xb9\x1c\xfd\x19h|\x88\x1eP\xf3\xa0\x02B\x82\x8c" +Bytes #buf ( 5 , WORD6:Int ) +Bytes #buf ( 5 , WORD5:Int ) ) ) ) ] + [ 5 <- #asWord ( b"\x00E\xc9,,\xd0\xdf{-p^\xf1,\xffw\xcb\x0b\xc5W\xed\"" +Bytes #buf ( 5 , TIMESTAMP_CELL:Int ) +Bytes #buf ( 5 , TIMESTAMP_CELL:Int ) +Bytes b"\x01" ) ] + ) => doneLemma ( + STORAGE0:Map + [ 6 <- #asWord ( #buf ( 1 , WORD7:Int ) +Bytes b"\xa4\xadOh\xd0\xb9\x1c\xfd\x19h|\x88\x1eP\xf3\xa0\x02B\x82\x8c" +Bytes #buf ( 5 , TIMESTAMP_CELL:Int ) +Bytes #buf ( 5 , WORD5:Int ) ) ] + [ 5 <- #asWord ( b"\x00E\xc9,,\xd0\xdf{-p^\xf1,\xffw\xcb\x0b\xc5W\xed\"" +Bytes #buf ( 5 , TIMESTAMP_CELL:Int ) +Bytes #buf ( 5 , TIMESTAMP_CELL:Int ) +Bytes b"\x01" ) ] + ) ... + requires 0 <=Int TIMESTAMP_CELL andBool TIMESTAMP_CELL runLemma( + ( maxUInt8 &Int ( ( TIMESTAMP_CELL:Int *Int pow48 ) |Int ( 115792089237316195423570985008687907853269984665640254554447762944319381569535 &Int ( ( TIMESTAMP_CELL:Int *Int 256 ) |Int ( 115792089237316195423570985008687907853269984665640564039457583726438152929535 &Int ( 1 |Int #asWord ( b"\x00E\xc9,,\xd0\xdf{-p^\xf1,\xffw\xcb\x0b\xc5W\xed\"" +Bytes #buf ( 5 , _WORD4:Int ) +Bytes #buf ( 5 , _WORD3:Int ) +Bytes b"\x00" ) ) ) ) ) ) ) + ) => doneLemma( + 1 + ) ... + requires 0 <=Int TIMESTAMP_CELL andBool TIMESTAMP_CELL runLemma ( + ( ( maxUInt40 &Int ( ( 115341543235797707419527244145998463631733976271937281205136574426583511597055 &Int #asWord ( #buf ( 2 , WORD7:Int ) +Bytes b"\xa4\xadOh\xd0\xb9\x1c\xfd\x19h|\x88\x1eP\xf3\xa0\x02B\x82\x8c" +Bytes #buf ( 5 , TIMESTAMP_CELL:Int ) +Bytes #buf ( 5 , WORD5:Int ) ) ) /Int pow40 ) ) ) + ) => doneLemma ( + TIMESTAMP_CELL + ) ... + requires 0 <=Int TIMESTAMP_CELL andBool TIMESTAMP_CELL runLemma ( + ( maxUInt40 &Int ( ( TIMESTAMP_CELL:Int |Int ( 115792089237316195423570985008687907853269984665640564039457584006813618012160 &Int #asWord ( #buf ( 1 , WORD7:Int ) +Bytes b"\xa4\xadOh\xd0\xb9\x1c\xfd\x19h|\x88\x1eP\xf3\xa0\x02B\x82\x8c" +Bytes #buf ( 5 , WORD6:Int ) +Bytes #buf ( 5 , WORD5:Int ) ) ) ) /Int pow40 ) ) <=Int TIMESTAMP_CELL:Int + ) => doneLemma ( + true + ) ... + requires 0 <=Int TIMESTAMP_CELL andBool TIMESTAMP_CELL runLemma ( + #asWord ( #range ( #buf ( 10 , ( ( ( TIMESTAMP_CELL:Int *Int pow48 ) /Int 256 ) |Int TIMESTAMP_CELL:Int ) ) , 5 , 5 ) ) <=Int TIMESTAMP_CELL:Int + ) => doneLemma ( + true + ) ... + requires 0 <=Int TIMESTAMP_CELL andBool TIMESTAMP_CELL runLemma ( + #asWord ( #range ( #buf ( 6 , TIMESTAMP_CELL:Int *Int 256 ) , 5 , 1 ) ) + ) => doneLemma ( + false + ) ... + requires 0 <=Int TIMESTAMP_CELL andBool TIMESTAMP_CELL runLemma ( + #asWord ( #range ( #buf ( 26 , 960911443338137442927181681227604902095826437272264907948032 |Int WORD4:Int ) , 21 , 5 ) ) <=Int TIMESTAMP_CELL:Int + ) => doneLemma ( + WORD4 <=Int TIMESTAMP_CELL + ) ... + requires 0 <=Int WORD4 andBool WORD4 runLemma ( + #asWord ( #range ( #buf ( 25 , ( ( ( WORD7:Int +Int 1 ) *Int pow200 ) |Int #asWord ( #buf ( 25 , ( 438052756531465687819472504520361015472122898704787692322816 |Int WORD6:Int ) ) ) ) ) , 20 , 5 ) ) <=Int TIMESTAMP_CELL:Int + ) => doneLemma ( + WORD6 <=Int TIMESTAMP_CELL + ) ... + requires 0 <=Int WORD6 andBool WORD6 runLemma ( + #asWord ( #buf ( 20 , 770621190285571058874329108704665103402425909248 |Int ( ( WORD7:Int +Int 1 ) *Int pow160 ) ) ) + ) => doneLemma ( + 770621190285571058874329108704665103402425909248 + ) ... + requires 0 <=Int WORD7 andBool WORD7 runLemma ( + ( 481644099385675654177479669474857658256926169505224677670350078624137216 |Int ( 115790322390251417039241401711187164934754157181743689629425282016341011726335 &Int #asWord ( #buf ( 2 , WORD7:Int ) +Bytes b"\xa4\xadOh\xd0\xb9\x1c\xfd\x19h|\x88\x1eP\xf3\xa0\x02B\x82\x8c" +Bytes #buf ( 5 , WORD6:Int ) +Bytes #buf ( 5 , WORD5:Int ) ) ) ) + ) => doneLemma ( + #asWord ( #buf ( 2 , WORD7:Int ) +Bytes b"E\xc9,,\xd0\xdf{-p^\xf1,\xffw\xcb\x0b\xc5W\xed\"" +Bytes #buf ( 5 , WORD6:Int ) +Bytes #buf ( 5 , WORD5:Int ) ) + ) ... + requires 0 <=Int WORD5 andBool WORD5 /packages/contracts-bedrock +# Set Run Directory /, This is where the foundtry.toml file generally is located. WORKSPACE_DIR=$( cd "$SCRIPT_HOME/../../.." >/dev/null 2>&1 && pwd ) pushd "$WORKSPACE_DIR" > /dev/null || exit @@ -170,11 +170,9 @@ copy_to_docker() { } clean_docker(){ - trap if [ "$LOCAL" = false ]; then notif "Cleaning Docker Container" - docker stop "$CONTAINER_NAME" > /dev/null 2>&1 || true - docker rm "$CONTAINER_NAME" > /dev/null 2>&1 || true + docker stop "$CONTAINER_NAME" > /dev/null 2>&1 sleep 2 # Give time for system to clean up container else notif "Not Running in Container. Done." diff --git a/test/kontrol/scripts/run-kontrol.sh b/test/kontrol/scripts/run-kontrol.sh index cd055976..6195e7d5 100755 --- a/test/kontrol/scripts/run-kontrol.sh +++ b/test/kontrol/scripts/run-kontrol.sh @@ -13,32 +13,18 @@ parse_args "$@" ############# # Functions # ############# +GHCRTS='' kontrol_build() { notif "Kontrol Build" # shellcheck disable=SC2086 - run kontrol build \ - --verbose \ - --require $lemmas \ - --module-import $module \ - $rekompile + run kontrol build return $? } kontrol_prove() { notif "Kontrol Prove" # shellcheck disable=SC2086 - run kontrol prove \ - --max-depth $max_depth \ - --max-iterations $max_iterations \ - --smt-timeout $smt_timeout \ - --workers $workers \ - $reinit \ - $bug_report \ - $break_on_calls \ - $break_every_step \ - $auto_abstract \ - $tests \ - $use_booster + run kontrol prove return $? } @@ -48,8 +34,8 @@ get_log_results(){ LOG_PATH="$SCRIPT_HOME/logs" RESULTS_LOG="$LOG_PATH/$RESULTS_FILE" - if [ ! -d "$LOG_PATH" ]; then - mkdir "$LOG_PATH" + if [ ! -d $LOG_PATH ]; then + mkdir $LOG_PATH fi notif "Generating Results Log: $LOG_PATH" @@ -59,7 +45,7 @@ get_log_results(){ mv results.tar.gz "$RESULTS_LOG" else docker cp "$CONTAINER_NAME:/home/user/workspace/results.tar.gz" "$RESULTS_LOG" - tar -xzvf "$RESULTS_LOG" + tar -xzvf "$RESULTS_LOG" > /dev/null 2>&1 fi if [ -f "$RESULTS_LOG" ]; then cp "$RESULTS_LOG" "$LOG_PATH/kontrol-results_latest.tar.gz" @@ -76,73 +62,12 @@ get_log_results(){ fi } -######################### -# kontrol build options # -######################### -# NOTE: This script has a recurring pattern of setting and unsetting variables, -# such as `rekompile`. Such a pattern is intended for easy use while locally -# developing and executing the proofs via this script. Comment/uncomment the -# empty assignment to activate/deactivate the corresponding flag -lemmas=test/kontrol/lido-lemmas.k -base_module=LIDO-LEMMAS -module=VetoSignallingTest:$base_module -rekompile=--rekompile -rekompile= -regen=--regen -# shellcheck disable=SC2034 -regen= - -################################# -# Tests to symbolically execute # -################################# -test_list=() -if [ "$SCRIPT_TESTS" == true ]; then - # Here go the list of tests to execute with the `script` option - test_list=( "VetoSignallingTest.testTransitionNormalToVetoSignalling" ) -elif [ "$CUSTOM_TESTS" != 0 ]; then - test_list=( "${@:${CUSTOM_TESTS}}" ) -fi -tests="" -# If test_list is empty, tests will be empty as well -# This will make kontrol execute any `test`, `prove` or `check` prefixed-function -# under the foundry-defined `test` directory -for test_name in "${test_list[@]}"; do - tests+="--match-test $test_name " -done - -######################### -# kontrol prove options # -######################### -max_depth=10000 -max_iterations=10000 -smt_timeout=100000 -max_workers=16 # Should be at most (M - 8) / 8 in a machine with M GB of RAM -# workers is the minimum between max_workers and the length of test_list -# unless no test arguments are provided, in which case we default to max_workers -if [ "$CUSTOM_TESTS" == 0 ] && [ "$SCRIPT_TESTS" == false ]; then - workers=${max_workers} -else - workers=$((${#test_list[@]}>max_workers ? max_workers : ${#test_list[@]})) -fi -reinit=--reinit -reinit= -break_on_calls=--no-break-on-calls -break_on_calls= -break_every_step=--no-break-every-step -break_every_step= -auto_abstract=--auto-abstract-gas -auto_abstract= -bug_report=--bug-report -bug_report= -use_booster=--no-use-booster -use_booster= - ############# # RUN TESTS # ############# # Set up the trap to run the function on failure -trap on_failure ERR INT +trap on_failure ERR INT TERM trap clean_docker EXIT conditionally_start_docker diff --git a/test/kontrol/scripts/versions.json b/test/kontrol/scripts/versions.json index 38350d43..ad0f2712 100644 --- a/test/kontrol/scripts/versions.json +++ b/test/kontrol/scripts/versions.json @@ -1,4 +1,4 @@ { - "kontrol": "0.1.242", + "kontrol": "1.0.35", "kontrol-cheatcodes": "master" }