diff --git a/.github/workflows/lido-ci.yml b/.github/workflows/lido-ci.yml index 2b4f13ad..9cd28a03 100644 --- a/.github/workflows/lido-ci.yml +++ b/.github/workflows/lido-ci.yml @@ -1,9 +1,11 @@ --- name: "Test Proofs" on: + workflow_dispatch: push: branches: - develop + - rvdevelop jobs: test: runs-on: ubuntu-latest @@ -23,7 +25,7 @@ -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", 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..273a975f 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 @@ -62,7 +63,7 @@ contract DualGovernance { * Proposals can be submitted when in the Normal state or during Veto Signalling; however they cannot be executed in Veto Signalling. */ function submitProposal(ExecutorCall[] calldata calls) external returns (uint256 proposalId) { - activateNextState(); + // activateNextState(); require(proposers[msg.sender], "Caller is not authorized to submit proposals."); require(calls.length != 0, "Empty calls."); @@ -79,7 +80,7 @@ contract DualGovernance { * Scheduling is allowed in Normal and Veto Cooldown states to prepare proposals for decision-making. */ function scheduleProposal(uint256 proposalId) external { - activateNextState(); + // activateNextState(); require( currentState == State.Normal || currentState == State.VetoCooldown, @@ -98,7 +99,7 @@ contract DualGovernance { // Cancel all non-executed proposals. function cancelAllPendingProposals() external { - activateNextState(); + // activateNextState(); require(admin_proposers[msg.sender], "Caller is not admin proposers."); require( @@ -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..e85f6fd8 --- /dev/null +++ b/contracts/model/StETHModel.sol @@ -0,0 +1,159 @@ +pragma solidity 0.8.23; + +contract StETHModel { + 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/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/test/kontrol/DualGovernanceSetUp.sol b/test/kontrol/DualGovernanceSetUp.sol new file mode 100644 index 00000000..2ce33f1f --- /dev/null +++ b/test/kontrol/DualGovernanceSetUp.sol @@ -0,0 +1,63 @@ +pragma solidity 0.8.23; + +import "contracts/model/DualGovernanceModel.sol"; +import "contracts/model/EmergencyProtectedTimelockModel.sol"; +import "contracts/model/EscrowModel.sol"; +import "contracts/model/StETHModel.sol"; + +import "test/kontrol/StorageSetup.sol"; + +contract DualGovernanceSetUp is StorageSetup { + DualGovernanceModel dualGovernance; + EmergencyProtectedTimelockModel timelock; + StETHModel stEth; + EscrowModel signallingEscrow; + EscrowModel rageQuitEscrow; + + function setUp() public { + stEth = new StETHModel(); + uint256 emergencyProtectionTimelock = 0; // Regular deployment mode + dualGovernance = new DualGovernanceModel(address(stEth), emergencyProtectionTimelock); + timelock = dualGovernance.emergencyProtectedTimelock(); + signallingEscrow = dualGovernance.signallingEscrow(); + rageQuitEscrow = new EscrowModel(address(dualGovernance), address(stEth)); + + // ?STORAGE + // ?WORD: totalPooledEther + // ?WORD0: totalShares + // ?WORD1: shares[signallingEscrow] + _stEthStorageSetup(stEth, signallingEscrow); + + // ?STORAGE0 + // ?WORD2: lastStateChangeTime + // ?WORD3: lastSubStateActivationTime + // ?WORD4: lastStateReactivationTime + // ?WORD5: lastVetoSignallingTime + // ?WORD6: rageQuitSequenceNumber + // ?WORD7: currentState + _dualGovernanceStorageSetup(dualGovernance, timelock, stEth, signallingEscrow, rageQuitEscrow); + + // ?STORAGE1 + // ?WORD8: totalSharesLocked + // ?WORD9: totalClaimedEthAmount + // ?WORD10: withdrawalRequestCount + // ?WORD11: lastWithdrawalRequestSubmitted + // ?WORD12: claimedWithdrawalRequests + // ?WORD13: rageQuitExtensionDelayPeriodEnd + // ?WORD14: rageQuitEthClaimTimelockStart + _signallingEscrowStorageSetup(signallingEscrow, dualGovernance, stEth); + + // ?STORAGE2 + // ?WORD15: totalSharesLocked + // ?WORD16: totalClaimedEthAmount + // ?WORD17: withdrawalRequestCount + // ?WORD18: lastWithdrawalRequestSubmitted + // ?WORD19: claimedWithdrawalRequests + // ?WORD20: rageQuitExtensionDelayPeriodEnd + // ?WORD21: rageQuitEthClaimTimelockStart + _rageQuitEscrowStorageSetup(rageQuitEscrow, dualGovernance, stEth); + + // ?STORAGE3 + kevm.symbolicStorage(address(timelock)); + } +} diff --git a/test/kontrol/EscrowAccounting.t.sol b/test/kontrol/EscrowAccounting.t.sol new file mode 100644 index 00000000..7bb0f5ca --- /dev/null +++ b/test/kontrol/EscrowAccounting.t.sol @@ -0,0 +1,226 @@ +pragma solidity 0.8.23; + +import "contracts/model/DualGovernanceModel.sol"; +import "contracts/model/EmergencyProtectedTimelockModel.sol"; +import "contracts/model/EscrowModel.sol"; +import "contracts/model/StETHModel.sol"; + +import "test/kontrol/StorageSetup.sol"; + +contract EscrowAccountingTest is StorageSetup { + StETHModel stEth; + EscrowModel escrow; + + function _setUpInitialState() public { + stEth = new StETHModel(); + address dualGovernanceAddress = address(uint160(uint256(keccak256("dualGovernance")))); // arbitrary DG address + escrow = new EscrowModel(dualGovernanceAddress, address(stEth)); + + // ?STORAGE + // ?WORD: totalPooledEther + // ?WORD0: totalShares + // ?WORD1: shares[escrow] + _stEthStorageSetup(stEth, escrow); + } + + function _setUpGenericState() public { + stEth = new StETHModel(); + escrow = new EscrowModel(address(0), address(0)); + + // ?STORAGE + // ?WORD: totalPooledEther + // ?WORD0: totalShares + // ?WORD1: shares[escrow] + _stEthStorageSetup(stEth, escrow); + + address dualGovernanceAddress = address(uint160(kevm.freshUInt(20))); // ?WORD2 + uint8 currentState = uint8(kevm.freshUInt(1)); // ?WORD3 + vm.assume(currentState < 2); + + // ?STORAGE0 + // ?WORD4: totalSharesLocked + // ?WORD5: totalClaimedEthAmount + // ?WORD6: rageQuitExtensionDelayPeriodEnd + _escrowStorageSetup(escrow, DualGovernanceModel(dualGovernanceAddress), stEth, currentState); + } + + function testRageQuitSupport() public { + _setUpGenericState(); + + uint256 totalSharesLocked = escrow.totalSharesLocked(); + uint256 totalFundsLocked = stEth.getPooledEthByShares(totalSharesLocked); + uint256 expectedRageQuitSupport = totalFundsLocked * 1e18 / stEth.totalSupply(); + + assert(escrow.getRageQuitSupport() == expectedRageQuitSupport); + } + + function _escrowInvariants(Mode mode) internal view { + _establish(mode, escrow.totalSharesLocked() <= stEth.sharesOf(address(escrow))); + uint256 totalPooledEther = stEth.getPooledEthByShares(escrow.totalSharesLocked()); + _establish(mode, totalPooledEther <= stEth.balanceOf(address(escrow))); + _establish(mode, escrow.totalWithdrawalRequestAmount() <= totalPooledEther); + _establish(mode, escrow.totalClaimedEthAmount() <= escrow.totalWithdrawalRequestAmount()); + _establish(mode, escrow.totalWithdrawnPostRageQuit() <= escrow.totalClaimedEthAmount()); + } + + function _signallingEscrowInvariants(Mode mode) internal view { + if (escrow.currentState() == EscrowModel.State.SignallingEscrow) { + _establish(mode, escrow.totalWithdrawalRequestAmount() == 0); + _establish(mode, escrow.totalClaimedEthAmount() == 0); + _establish(mode, escrow.totalWithdrawnPostRageQuit() == 0); + } + } + + function _escrowUserInvariants(Mode mode, address user) internal view { + _establish(mode, escrow.shares(user) <= escrow.totalSharesLocked()); + } + + function testEscrowInvariantsHoldInitially() public { + _setUpInitialState(); + + // Placeholder address to avoid complications with keccak of symbolic addresses + address sender = address(uint160(uint256(keccak256("sender")))); + _escrowInvariants(Mode.Assert); + _signallingEscrowInvariants(Mode.Assert); + _escrowUserInvariants(Mode.Assert, sender); + } + + struct AccountingRecord { + EscrowModel.State escrowState; + uint256 allowance; + uint256 userBalance; + uint256 escrowBalance; + uint256 userShares; + uint256 escrowShares; + uint256 userSharesLocked; + uint256 totalSharesLocked; + uint256 totalEth; + uint256 userLastLockedTime; + } + + function _saveAccountingRecord(address user) internal view returns (AccountingRecord memory ar) { + ar.escrowState = escrow.currentState(); + 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.shares(user); + ar.totalSharesLocked = escrow.totalSharesLocked(); + ar.totalEth = stEth.getPooledEthByShares(ar.totalSharesLocked); + ar.userLastLockedTime = escrow.lastLockedTimes(user); + } + + function _assumeFreshAddress(address account) internal { + 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 _assumeNoOverflow(uint256 augend, uint256 addend) internal { + unchecked { + vm.assume(augend < augend + addend); + } + } + + function testLockStEth(uint256 amount) 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(stEth.balanceOf(sender) < ethUpperBound); + + AccountingRecord memory pre = _saveAccountingRecord(sender); + vm.assume(pre.escrowState == EscrowModel.State.SignallingEscrow); + 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); + + _escrowInvariants(Mode.Assume); + _signallingEscrowInvariants(Mode.Assume); + _escrowUserInvariants(Mode.Assume, sender); + + vm.startPrank(sender); + escrow.lock(amount); + vm.stopPrank(); + + _escrowInvariants(Mode.Assert); + _signallingEscrowInvariants(Mode.Assert); + _escrowUserInvariants(Mode.Assert, sender); + + AccountingRecord memory post = _saveAccountingRecord(sender); + assert(post.escrowState == EscrowModel.State.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 == block.timestamp); + + // 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 < errorTerm || pre.escrowBalance + amount - errorTerm <= post.escrowBalance); + assert(pre.totalEth + amount < errorTerm || pre.totalEth + amount - errorTerm <= post.totalEth); + } + + function testUnlockStEth() 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(escrow.lastLockedTimes(sender) < timeUpperBound); + + AccountingRecord memory pre = _saveAccountingRecord(sender); + vm.assume(pre.escrowState == EscrowModel.State.SignallingEscrow); + vm.assume(pre.userSharesLocked <= pre.totalSharesLocked); + vm.assume(block.timestamp >= pre.userLastLockedTime + escrow.SIGNALLING_ESCROW_MIN_LOCK_TIME()); + + _escrowInvariants(Mode.Assume); + _signallingEscrowInvariants(Mode.Assume); + _escrowUserInvariants(Mode.Assume, sender); + + vm.startPrank(sender); + escrow.unlock(); + vm.stopPrank(); + + _escrowInvariants(Mode.Assert); + _signallingEscrowInvariants(Mode.Assert); + _escrowUserInvariants(Mode.Assert, sender); + + AccountingRecord memory post = _saveAccountingRecord(sender); + assert(post.escrowState == EscrowModel.State.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); + assert(pre.escrowBalance - amount <= post.escrowBalance); + assert(pre.totalEth - amount <= post.totalEth); + assert(post.userBalance <= post.userBalance + amount); + + uint256 errorTerm = stEth.getPooledEthByShares(1) + 1; + assert(post.escrowBalance <= pre.escrowBalance - amount + errorTerm); + assert(post.totalEth <= pre.totalEth - amount + errorTerm); + assert(pre.userBalance + amount < errorTerm || pre.userBalance + amount - errorTerm <= post.userBalance); + } +} diff --git a/test/kontrol/EscrowOperations.t.sol b/test/kontrol/EscrowOperations.t.sol new file mode 100644 index 00000000..df21d84e --- /dev/null +++ b/test/kontrol/EscrowOperations.t.sol @@ -0,0 +1,136 @@ +pragma solidity 0.8.23; + +import "test/kontrol/EscrowAccounting.t.sol"; + +contract EscrowOperationsTest is EscrowAccountingTest { + /** + * 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(escrow.lastLockedTimes(sender) < timeUpperBound); + + AccountingRecord memory pre = _saveAccountingRecord(sender); + vm.assume(pre.escrowState == EscrowModel.State.SignallingEscrow); + vm.assume(pre.userSharesLocked <= pre.totalSharesLocked); + + uint256 lockPeriod = pre.userLastLockedTime + escrow.SIGNALLING_ESCROW_MIN_LOCK_TIME(); + + if (block.timestamp < lockPeriod) { + vm.prank(sender); + vm.expectRevert("Lock period not expired."); + escrow.unlock(); + } + } + + /** + * 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 = _saveAccountingRecord(sender); + 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); + + _escrowInvariants(Mode.Assume); + _signallingEscrowInvariants(Mode.Assume); + _escrowUserInvariants(Mode.Assume, sender); + + if (pre.escrowState == EscrowModel.State.RageQuitEscrow) { + vm.prank(sender); + vm.expectRevert("Cannot lock in current state."); + escrow.lock(amount); + + vm.prank(sender); + vm.expectRevert("Cannot unlock in current state."); + escrow.unlock(); + } else { + vm.prank(sender); + escrow.lock(amount); + + AccountingRecord memory afterLock = _saveAccountingRecord(sender); + vm.assume(afterLock.userShares < ethUpperBound); + vm.assume(afterLock.userLastLockedTime < timeUpperBound); + vm.assume(afterLock.userSharesLocked <= afterLock.totalSharesLocked); + vm.assume(block.timestamp >= afterLock.userLastLockedTime + escrow.SIGNALLING_ESCROW_MIN_LOCK_TIME()); + + vm.prank(sender); + escrow.unlock(); + + _escrowInvariants(Mode.Assert); + _signallingEscrowInvariants(Mode.Assert); + _escrowUserInvariants(Mode.Assert, sender); + + AccountingRecord memory post = _saveAccountingRecord(sender); + assert(post.escrowState == EscrowModel.State.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. + */ + 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 = _saveAccountingRecord(sender); + vm.assume(pre.escrowState == EscrowModel.State.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); + + _escrowInvariants(Mode.Assume); + _escrowUserInvariants(Mode.Assume, sender); + + vm.assume(escrow.lastWithdrawalRequestSubmitted()); + vm.assume(escrow.claimedWithdrawalRequests() == escrow.withdrawalRequestCount()); + 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(); + + _escrowInvariants(Mode.Assert); + _escrowUserInvariants(Mode.Assert, sender); + + AccountingRecord memory post = _saveAccountingRecord(sender); + assert(post.userSharesLocked == 0); + } + } +} diff --git a/test/kontrol/KontrolTest.sol b/test/kontrol/KontrolTest.sol new file mode 100644 index 00000000..07786f09 --- /dev/null +++ b/test/kontrol/KontrolTest.sol @@ -0,0 +1,37 @@ +pragma solidity 0.8.23; + +import "forge-std/Vm.sol"; +import "forge-std/Test.sol"; +import "kontrol-cheatcodes/KontrolCheats.sol"; + +contract KontrolTest is Test, KontrolCheats { + // Note: there are lemmas dependent on `ethUpperBound` + uint256 constant ethMaxWidth = 96; + uint256 constant ethUpperBound = 2 ** ethMaxWidth; + uint256 constant timeUpperBound = 2 ** 40; + + enum Mode { + Assume, + Assert + } + + function _establish(Mode mode, bool condition) internal pure { + if (mode == Mode.Assume) { + vm.assume(condition); + } else { + assert(condition); + } + } + + function _storeBytes32(address contractAddress, uint256 slot, bytes32 value) internal { + vm.store(contractAddress, bytes32(slot), value); + } + + function _storeUInt256(address contractAddress, uint256 slot, uint256 value) internal { + vm.store(contractAddress, bytes32(slot), bytes32(value)); + } + + function _storeAddress(address contractAddress, uint256 slot, address value) internal { + vm.store(contractAddress, bytes32(slot), bytes32(uint256(uint160(value)))); + } +} diff --git a/test/kontrol/ProposalOperations.t.sol b/test/kontrol/ProposalOperations.t.sol new file mode 100644 index 00000000..ab4bdc8f --- /dev/null +++ b/test/kontrol/ProposalOperations.t.sol @@ -0,0 +1,308 @@ +pragma solidity 0.8.23; + +import "test/kontrol/DualGovernanceSetUp.sol"; + +contract ProposalOperationsTest is DualGovernanceSetUp { + // ?STORAGE3 + // ?WORD21: nextProposalId + // ?WROD22: emergencyModeActive + function _timelockSetup() internal { + // Slot 6: nextProposalId + uint256 nextProposalId = kevm.freshUInt(32); + vm.assume(nextProposalId < type(uint256).max); + _storeUInt256(address(timelock), 6, nextProposalId); + // Slot 7: emergencyModeActive + uint8 emergencyModeActive = uint8(kevm.freshUInt(1)); + vm.assume(emergencyModeActive < 2); + _storeUInt256(address(timelock), 7, uint256(emergencyModeActive)); + } + + // Set up the storage for a proposal. + // ?WORD23: numCalls + // ?WORD24: submissionTime + // ?WORD25: schedulingTime + // ?WORD26: status + function _proposalStorageSetup(uint256 proposalId) internal { + // Slot 5 + // Proposal: id + uint256 slot = uint256(keccak256(abi.encodePacked(proposalId, uint256(5)))); + vm.assume(slot <= type(uint256).max - 5); + _storeUInt256(address(timelock), slot, proposalId); + // Proposal: proposer + address proposer = address(uint160(uint256(keccak256("proposer")))); + vm.assume(dualGovernance.proposers(proposer)); + _storeAddress(address(timelock), slot + 1, proposer); + // Proposal: ExecutorCall + uint256 numCalls = kevm.freshUInt(32); + vm.assume(numCalls > 0); + uint256 callsSlot = uint256(keccak256(abi.encodePacked(slot + 2))); + _storeUInt256(address(timelock), callsSlot, numCalls); + // Proposal: submissionTime + uint256 submissionTime = kevm.freshUInt(32); + vm.assume(submissionTime < timeUpperBound); + _storeUInt256(address(timelock), slot + 3, submissionTime); + // Proposal: schedulingTime + uint256 schedulingTime = kevm.freshUInt(32); + vm.assume(schedulingTime < timeUpperBound); + _storeUInt256(address(timelock), slot + 4, schedulingTime); + // Proposal: status + uint256 statusIndex = kevm.freshUInt(32); + vm.assume(statusIndex < 4); + ProposalStatus status = ProposalStatus(statusIndex); + _storeUInt256(address(timelock), slot + 5, uint256(status)); + } + + struct ProposalRecord { + DualGovernanceModel.State state; + ProposalStatus status; + uint256 submissionTime; + uint256 schedulingTime; + uint256 lastVetoSignallingTime; + } + + // Record a proposal's details with the current governance state. + function _recordProposal(uint256 proposalId) internal view returns (ProposalRecord memory pr) { + (,, uint256 submissionTime, uint256 schedulingTime, ProposalStatus status) = timelock.proposals(proposalId); + pr.state = dualGovernance.currentState(); + pr.status = status; + pr.submissionTime = submissionTime; + pr.schedulingTime = schedulingTime; + pr.lastVetoSignallingTime = dualGovernance.lastVetoSignallingTime(); + } + + // Validate that a pending proposal meets the criteria. + function _validPendingProposal(Mode mode, ProposalRecord memory pr) internal view { + _establish(mode, pr.status == ProposalStatus.Pending); + _establish(mode, pr.submissionTime <= block.timestamp); + _establish(mode, pr.schedulingTime == 0); + } + + // Validate that a scheduled proposal meets the criteria. + function _validScheduledProposal(Mode mode, ProposalRecord memory pr) internal view { + _establish(mode, pr.status == ProposalStatus.Scheduled); + _establish(mode, pr.submissionTime <= block.timestamp); + _establish(mode, block.timestamp >= pr.submissionTime + timelock.PROPOSAL_EXECUTION_MIN_TIMELOCK()); + _establish(mode, pr.schedulingTime <= block.timestamp); + _establish(mode, pr.schedulingTime >= pr.submissionTime); + } + + function _validExecutedProposal(Mode mode, ProposalRecord memory pr) internal view { + _establish(mode, pr.status == ProposalStatus.Executed); + _establish(mode, pr.submissionTime <= block.timestamp); + _establish(mode, block.timestamp >= pr.submissionTime + timelock.PROPOSAL_EXECUTION_MIN_TIMELOCK()); + _establish(mode, pr.schedulingTime <= block.timestamp); + _establish(mode, pr.schedulingTime >= pr.submissionTime); + } + + function _validCanceledProposal(Mode mode, ProposalRecord memory pr) internal view { + _establish(mode, pr.status == ProposalStatus.Canceled); + _establish(mode, pr.submissionTime <= block.timestamp); + } + + // Function to handle common assumptions. + function _commonAssumptions() internal { + vm.assume(block.timestamp < timeUpperBound); + vm.assume(timelock.governance() == address(dualGovernance)); + uint256 emergencyProtectionTimelock = kevm.freshUInt(32); + vm.assume(emergencyProtectionTimelock < timeUpperBound); + vm.assume(timelock.emergencyProtectionTimelock() == emergencyProtectionTimelock); + } + + /** + * Test that proposals cannot be submitted in the VetoSignallingDeactivation and VetoCooldown states. + */ + function testCannotProposeInInvalidState() external { + _timelockSetup(); + vm.assume(block.timestamp < timeUpperBound); + uint256 nextProposalId = timelock.nextProposalId(); + + address proposer = address(uint160(uint256(keccak256("proposer")))); + vm.assume(dualGovernance.proposers(proposer)); + DualGovernanceModel.State state = dualGovernance.currentState(); + + vm.assume( + state == DualGovernanceModel.State.VetoSignallingDeactivation + || state == DualGovernanceModel.State.VetoCooldown + ); + vm.prank(proposer); + vm.expectRevert("Cannot submit in current state."); + dualGovernance.submitProposal(new ExecutorCall[](1)); + + assert(timelock.nextProposalId() == nextProposalId); + } + + /** + * Test that a proposal cannot be scheduled for execution if the Dual Governance state is not Normal or VetoCooldown. + */ + function testCannotScheduleInInvalidStates(uint256 proposalId) external { + _proposalStorageSetup(proposalId); + _commonAssumptions(); + + vm.assume(proposalId < timelock.nextProposalId()); + ProposalRecord memory pre = _recordProposal(proposalId); + _validPendingProposal(Mode.Assume, pre); + + vm.assume(pre.state != DualGovernanceModel.State.Normal); + vm.assume(pre.state != DualGovernanceModel.State.VetoCooldown); + vm.expectRevert("Proposals can only be scheduled in Normal or Veto Cooldown states."); + 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 { + _proposalStorageSetup(proposalId); + _commonAssumptions(); + + vm.assume(proposalId < timelock.nextProposalId()); + ProposalRecord memory pre = _recordProposal(proposalId); + _validPendingProposal(Mode.Assume, pre); + vm.assume(pre.state == DualGovernanceModel.State.VetoCooldown); + + vm.assume(pre.submissionTime >= pre.lastVetoSignallingTime); + vm.expectRevert("Proposal submitted after the last time Veto Signalling state was entered."); + 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) public { + _timelockSetup(); + _proposalStorageSetup(proposalId); + _commonAssumptions(); + + vm.assume(proposalId < timelock.nextProposalId()); + ProposalRecord memory pre = _recordProposal(proposalId); + vm.assume(pre.submissionTime <= block.timestamp); + vm.assume(pre.state == DualGovernanceModel.State.Normal || pre.state == DualGovernanceModel.State.VetoCooldown); + + if (pre.state == DualGovernanceModel.State.VetoCooldown) { + vm.assume(pre.submissionTime < pre.lastVetoSignallingTime); + } + + vm.assume(pre.status == ProposalStatus.Canceled || pre.status == ProposalStatus.Executed); + + vm.expectRevert("Proposal must be in Pending status."); + dualGovernance.scheduleProposal(proposalId); + + ProposalRecord memory post = _recordProposal(proposalId); + assert(post.status != ProposalStatus.Scheduled); + } + + /** + * Test that a proposal cannot be scheduled for execution before ProposalExecutionMinTimelock has passed since its submission. + */ + function testCannotScheduleBeforeMinTimelock(uint256 proposalId) external { + _timelockSetup(); + _proposalStorageSetup(proposalId); + _commonAssumptions(); + + vm.assume(proposalId < timelock.nextProposalId()); + ProposalRecord memory pre = _recordProposal(proposalId); + _validPendingProposal(Mode.Assume, pre); + + uint256 schedulingMinDelay = pre.submissionTime + timelock.PROPOSAL_EXECUTION_MIN_TIMELOCK(); + + vm.assume(pre.state == DualGovernanceModel.State.Normal || pre.state == DualGovernanceModel.State.VetoCooldown); + + if (pre.state == DualGovernanceModel.State.VetoCooldown) { + vm.assume(pre.submissionTime < pre.lastVetoSignallingTime); + } + + vm.assume(block.timestamp < schedulingMinDelay); + vm.expectRevert("Required time since submission has not yet elapsed."); + dualGovernance.scheduleProposal(proposalId); + + ProposalRecord memory post = _recordProposal(proposalId); + _validPendingProposal(Mode.Assert, post); + } + + function testSchedulingSuccess(uint256 proposalId) external { + _timelockSetup(); + _proposalStorageSetup(proposalId); + _commonAssumptions(); + + vm.assume(proposalId < timelock.nextProposalId()); + ProposalRecord memory pre = _recordProposal(proposalId); + _validPendingProposal(Mode.Assume, pre); + + uint256 schedulingMinDelay = pre.submissionTime + timelock.PROPOSAL_EXECUTION_MIN_TIMELOCK(); + vm.assume(pre.state == DualGovernanceModel.State.Normal || pre.state == DualGovernanceModel.State.VetoCooldown); + + if (pre.state == DualGovernanceModel.State.VetoCooldown) { + vm.assume(pre.submissionTime < pre.lastVetoSignallingTime); + } + + vm.assume(block.timestamp >= schedulingMinDelay); + dualGovernance.scheduleProposal(proposalId); + + ProposalRecord memory post = _recordProposal(proposalId); + _validScheduledProposal(Mode.Assert, post); + + assert(post.state == pre.state); + assert(post.submissionTime == pre.submissionTime); + assert(post.schedulingTime == block.timestamp); + } + + /** + * Test that a proposal cannot be executed until the emergency protection timelock has passed since it was scheduled. + */ + function testCannotExecuteBeforeEmergencyProtectionTimelock(uint256 proposalId) external { + _timelockSetup(); + _proposalStorageSetup(proposalId); + _commonAssumptions(); + + vm.assume(proposalId < timelock.nextProposalId()); + ProposalRecord memory pre = _recordProposal(proposalId); + _validScheduledProposal(Mode.Assume, pre); + + uint256 executionMinDelay = pre.schedulingTime + timelock.emergencyProtectionTimelock(); + vm.assume(!timelock.emergencyModeActive()); + + vm.assume(block.timestamp < executionMinDelay); + vm.expectRevert("Scheduled time plus delay must pass before execution."); + timelock.execute(proposalId); + + ProposalRecord memory post = _recordProposal(proposalId); + _validScheduledProposal(Mode.Assert, post); + } + + /** + * Test that only admin proposers can cancel proposals. + */ + function testOnlyAdminProposersCanCancelProposals() external { + _timelockSetup(); + + uint256 numProposals = timelock.nextProposalId(); + vm.assume(numProposals > 0); + for (uint256 proposalId = 0; proposalId < numProposals; proposalId++) { + _proposalStorageSetup(proposalId); + } + _commonAssumptions(); + + address adminProposer = address(uint160(uint256(keccak256("adminProposer")))); + vm.assume(dualGovernance.admin_proposers(adminProposer)); + address proposer = address(uint160(uint256(keccak256("proposer")))); + vm.assume(!dualGovernance.admin_proposers(proposer)); + + DualGovernanceModel.State state = dualGovernance.currentState(); + vm.assume(state != DualGovernanceModel.State.Normal); + vm.assume(state != DualGovernanceModel.State.VetoCooldown); + vm.assume(state != DualGovernanceModel.State.RageQuit); + + // Cancel as a non-admin proposer + vm.prank(proposer); + vm.expectRevert("Caller is not admin proposers."); + dualGovernance.cancelAllPendingProposals(); + + // Cancel as an admin proposer + vm.prank(adminProposer); + dualGovernance.cancelAllPendingProposals(); + } +} diff --git a/test/kontrol/StorageSetup.sol b/test/kontrol/StorageSetup.sol new file mode 100644 index 00000000..ef58ba19 --- /dev/null +++ b/test/kontrol/StorageSetup.sol @@ -0,0 +1,145 @@ +pragma solidity 0.8.23; + +import "contracts/model/DualGovernanceModel.sol"; +import "contracts/model/EmergencyProtectedTimelockModel.sol"; +import "contracts/model/EscrowModel.sol"; +import "contracts/model/StETHModel.sol"; + +import "test/kontrol/KontrolTest.sol"; + +contract StorageSetup is KontrolTest { + function _stEthStorageSetup(StETHModel _stEth, EscrowModel _escrow) internal { + kevm.symbolicStorage(address(_stEth)); + // Slot 0 + uint256 totalPooledEther = kevm.freshUInt(32); + vm.assume(0 < totalPooledEther); + vm.assume(totalPooledEther < ethUpperBound); + _stEth.setTotalPooledEther(totalPooledEther); + // Slot 1 + uint256 totalShares = kevm.freshUInt(32); + vm.assume(0 < totalShares); + vm.assume(totalShares < ethUpperBound); + _stEth.setTotalShares(totalShares); + // Slot 2 + uint256 shares = kevm.freshUInt(32); + vm.assume(shares < totalShares); + _stEth.setShares(address(_escrow), shares); + } + + function _dualGovernanceStorageSetup( + DualGovernanceModel _dualGovernance, + EmergencyProtectedTimelockModel _timelock, + StETHModel _stEth, + EscrowModel _signallingEscrow, + EscrowModel _rageQuitEscrow + ) internal { + kevm.symbolicStorage(address(_dualGovernance)); + // Slot 0 + _storeAddress(address(_dualGovernance), 0, address(_timelock)); + // Slot 1 + _storeAddress(address(_dualGovernance), 1, address(_signallingEscrow)); + // Slot 2 + _storeAddress(address(_dualGovernance), 2, address(_rageQuitEscrow)); + // Slot 3 + _storeAddress(address(_dualGovernance), 3, address(_stEth)); + // Slot 6 + uint256 lastStateChangeTime = kevm.freshUInt(32); + vm.assume(lastStateChangeTime <= block.timestamp); + vm.assume(lastStateChangeTime < timeUpperBound); + _storeUInt256(address(_dualGovernance), 6, lastStateChangeTime); + // Slot 7 + uint256 lastSubStateActivationTime = kevm.freshUInt(32); + vm.assume(lastSubStateActivationTime <= block.timestamp); + vm.assume(lastSubStateActivationTime < timeUpperBound); + _storeUInt256(address(_dualGovernance), 7, lastSubStateActivationTime); + // Slot 8 + uint256 lastStateReactivationTime = kevm.freshUInt(32); + vm.assume(lastStateReactivationTime <= block.timestamp); + vm.assume(lastStateReactivationTime < timeUpperBound); + _storeUInt256(address(_dualGovernance), 8, lastStateReactivationTime); + // Slot 9 + uint256 lastVetoSignallingTime = kevm.freshUInt(32); + vm.assume(lastVetoSignallingTime <= block.timestamp); + vm.assume(lastVetoSignallingTime < timeUpperBound); + _storeUInt256(address(_dualGovernance), 9, lastVetoSignallingTime); + // Slot 10 + uint256 rageQuitSequenceNumber = kevm.freshUInt(32); + vm.assume(rageQuitSequenceNumber < type(uint256).max); + _storeUInt256(address(_dualGovernance), 10, rageQuitSequenceNumber); + // Slot 11 + uint256 currentState = kevm.freshUInt(32); + vm.assume(currentState <= 4); + _storeUInt256(address(_dualGovernance), 11, currentState); + } + + function _signallingEscrowStorageSetup( + EscrowModel _signallingEscrow, + DualGovernanceModel _dualGovernance, + StETHModel _stEth + ) internal { + _escrowStorageSetup( + _signallingEscrow, + _dualGovernance, + _stEth, + 0 // SignallingEscrow + ); + + vm.assume(_signallingEscrow.rageQuitExtensionDelayPeriodEnd() == 0); + } + + function _rageQuitEscrowStorageSetup( + EscrowModel _rageQuitEscrow, + DualGovernanceModel _dualGovernance, + StETHModel _stEth + ) internal { + _escrowStorageSetup( + _rageQuitEscrow, + _dualGovernance, + _stEth, + 1 // RageQuitEscrow + ); + } + + function _escrowStorageSetup( + EscrowModel _escrow, + DualGovernanceModel _dualGovernance, + StETHModel _stEth, + uint8 _currentState + ) internal { + kevm.symbolicStorage(address(_escrow)); + // Slot 0: dualGovernance + _storeAddress(address(_escrow), 0, address(_dualGovernance)); + // Slot 1: stEth + _storeAddress(address(_escrow), 1, address(_stEth)); + // Slot 3: totalSharesLocked + uint256 totalSharesLocked = kevm.freshUInt(32); + vm.assume(totalSharesLocked < ethUpperBound); + _storeUInt256(address(_escrow), 3, totalSharesLocked); + // Slot 4: totalClaimedEthAmount + uint256 totalClaimedEthAmount = kevm.freshUInt(32); + vm.assume(totalClaimedEthAmount <= totalSharesLocked); + _storeUInt256(address(_escrow), 4, totalClaimedEthAmount); + // Slot 6: withdrawalRequestCount + uint256 withdrawalRequestCount = kevm.freshUInt(32); + vm.assume(withdrawalRequestCount < type(uint256).max); + _storeUInt256(address(_escrow), 6, withdrawalRequestCount); + // Slot 7: lastWithdrawalRequestSubmitted + uint256 lastWithdrawalRequestSubmitted = kevm.freshUInt(32); + vm.assume(lastWithdrawalRequestSubmitted < 2); + _storeUInt256(address(_escrow), 7, lastWithdrawalRequestSubmitted); + // Slot 8: claimedWithdrawalRequests + uint256 claimedWithdrawalRequests = kevm.freshUInt(32); + vm.assume(claimedWithdrawalRequests < type(uint256).max); + _storeUInt256(address(_escrow), 8, claimedWithdrawalRequests); + // Slot 13: rageQuitExtensionDelayPeriodEnd + uint256 rageQuitExtensionDelayPeriodEnd = kevm.freshUInt(32); + _storeUInt256(address(_escrow), 13, rageQuitExtensionDelayPeriodEnd); + // Slot 15: rageQuitEthClaimTimelockStart + uint256 rageQuitEthClaimTimelockStart = kevm.freshUInt(32); + vm.assume(rageQuitEthClaimTimelockStart <= block.timestamp); + vm.assume(rageQuitEthClaimTimelockStart < timeUpperBound); + _storeUInt256(address(_escrow), 15, rageQuitEthClaimTimelockStart); + // Slot 16: currentState + _storeUInt256(address(_escrow), 16, uint256(_currentState)); + } +} diff --git a/test/kontrol/VetoSignalling.t.sol b/test/kontrol/VetoSignalling.t.sol index 0db58bd3..59493d28 100644 --- a/test/kontrol/VetoSignalling.t.sol +++ b/test/kontrol/VetoSignalling.t.sol @@ -1,170 +1,13 @@ 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"; - -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. @@ -172,13 +15,13 @@ contract VetoSignallingTest is Test, KontrolCheats { 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(dualGovernance.currentState() == DualGovernanceModel.State.Normal); dualGovernance.activateNextState(); - assert(dualGovernance.currentState() == DualGovernance.State.VetoSignalling); + assert(dualGovernance.currentState() == DualGovernanceModel.State.VetoSignalling); } struct StateRecord { - DualGovernance.State state; + DualGovernanceModel.State state; uint256 timestamp; uint256 rageQuitSupport; uint256 maxRageQuitSupport; @@ -192,8 +35,8 @@ contract VetoSignallingTest is Test, KontrolCheats { */ function _vetoSignallingInvariants(Mode mode, StateRecord memory sr) internal view { require( - sr.state != DualGovernance.State.Normal && sr.state != DualGovernance.State.VetoCooldown - && sr.state != DualGovernance.State.RageQuit, + sr.state != DualGovernanceModel.State.Normal && sr.state != DualGovernanceModel.State.VetoCooldown + && sr.state != DualGovernanceModel.State.RageQuit, "Invariants only apply to the Veto Signalling states." ); @@ -235,14 +78,14 @@ contract VetoSignallingTest is Test, KontrolCheats { // Note: creates three branches in symbolic execution if (sr.timestamp <= sr.activationTime + dynamicTimelock) { - _establish(mode, sr.state == DualGovernance.State.VetoSignalling); + _establish(mode, sr.state == DualGovernanceModel.State.VetoSignalling); } else if ( sr.timestamp <= Math.max(sr.reactivationTime, sr.activationTime) + dualGovernance.VETO_SIGNALLING_MIN_ACTIVE_DURATION() ) { - _establish(mode, sr.state == DualGovernance.State.VetoSignalling); + _establish(mode, sr.state == DualGovernanceModel.State.VetoSignalling); } else { - _establish(mode, sr.state == DualGovernance.State.VetoSignallingDeactivation); + _establish(mode, sr.state == DualGovernanceModel.State.VetoSignallingDeactivation); } } @@ -259,7 +102,7 @@ contract VetoSignallingTest is Test, KontrolCheats { function _vetoSignallingMaxDelayInvariant(Mode mode, StateRecord memory sr) internal view { // Note: creates two branches in symbolic execution if (_maxDeactivationDelayPassed(sr)) { - _establish(mode, sr.state == DualGovernance.State.VetoSignallingDeactivation); + _establish(mode, sr.state == DualGovernanceModel.State.VetoSignallingDeactivation); } } @@ -316,15 +159,15 @@ 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.currentState() != DualGovernanceModel.State.VetoSignalling); + vm.assume(dualGovernance.currentState() != DualGovernanceModel.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 (sr.state == DualGovernanceModel.State.VetoSignalling) { _vetoSignallingInvariants(Mode.Assert, sr); } } @@ -348,9 +191,9 @@ contract VetoSignallingTest is Test, KontrolCheats { StateRecord memory previous = _recordPreviousState(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 != DualGovernanceModel.State.Normal); + vm.assume(previous.state != DualGovernanceModel.State.VetoCooldown); + vm.assume(previous.state != DualGovernanceModel.State.RageQuit); _vetoSignallingInvariants(Mode.Assume, previous); dualGovernance.activateNextState(); @@ -358,8 +201,8 @@ contract VetoSignallingTest is Test, KontrolCheats { StateRecord memory current = _recordCurrentState(maxRageQuitSupport); if ( - current.state != DualGovernance.State.Normal && current.state != DualGovernance.State.VetoCooldown - && current.state != DualGovernance.State.RageQuit + current.state != DualGovernanceModel.State.Normal && current.state != DualGovernanceModel.State.VetoCooldown + && current.state != DualGovernanceModel.State.RageQuit ) { _vetoSignallingInvariants(Mode.Assert, current); } @@ -386,13 +229,13 @@ contract VetoSignallingTest is Test, KontrolCheats { vm.assume(signallingEscrow.getRageQuitSupport() <= previous.maxRageQuitSupport); vm.assume( - previous.state == DualGovernance.State.VetoSignalling - || previous.state == DualGovernance.State.VetoSignallingDeactivation + previous.state == DualGovernanceModel.State.VetoSignalling + || previous.state == DualGovernanceModel.State.VetoSignallingDeactivation ); _vetoSignallingInvariants(Mode.Assume, previous); - assert(previous.state == DualGovernance.State.VetoSignallingDeactivation); + assert(previous.state == DualGovernanceModel.State.VetoSignallingDeactivation); dualGovernance.activateNextState(); @@ -404,9 +247,9 @@ contract VetoSignallingTest is Test, KontrolCheats { // 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); + assert(current.state == DualGovernanceModel.State.VetoCooldown); } else { - assert(current.state == DualGovernance.State.VetoSignallingDeactivation); + assert(current.state == DualGovernanceModel.State.VetoSignallingDeactivation); } } } diff --git a/test/kontrol/lido-lemmas.k b/test/kontrol/lido-lemmas.k index 65da0a19..e494613b 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 + imports EVM imports FOUNDRY imports INT-SYMBOLIC imports MAP-SYMBOLIC @@ -64,6 +66,10 @@ module LIDO-LEMMAS requires #rangeUInt(256, A) andBool #rangeUInt(256, (-1) *Int B) [concrete(B), simplification, comm] + rule chop (0 -Int A) ==Int B => A ==Int (pow256 -Int B) modInt pow256 + requires #rangeUInt(256, A) andBool #rangeUInt(256, B) + [concrete(B), simplification, comm] + // *Int rule A *Int B ==Int 0 => A ==Int 0 orBool B ==Int 0 [simplification] @@ -78,6 +84,7 @@ module LIDO-LEMMAS // 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 ( 0 ==Int 0 /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 + { #range ( B, 0, lengthBytes(B1) ) #Equals B1 } #And + { #range ( B, lengthBytes(B1), lengthBytes(B) -Int lengthBytes(B1) ) #Equals B2 } + requires lengthBytes(B1) <=Int lengthBytes(B) + [simplification(60), concrete(B, B1)] + + rule { B1:Bytes +Bytes B2:Bytes #Equals B } => + { #range ( B, 0, lengthBytes(B1) ) #Equals B1 } #And + { #range ( B, lengthBytes(B1), lengthBytes(B) -Int lengthBytes(B1) ) #Equals B2 } + requires lengthBytes(B1) <=Int lengthBytes(B) + [simplification(60), concrete(B, B1)] + + rule { B:Bytes #Equals #buf( N, X:Int ) +Bytes B2:Bytes } => + { X #Equals #asWord ( #range ( B, 0, N ) ) } #And + { #range ( B, N, lengthBytes(B) -Int N ) #Equals B2 } + requires N <=Int lengthBytes(B) + [simplification(60), concrete(B, N)] + + rule { #buf( N, X:Int ) +Bytes B2:Bytes #Equals B } => + { X #Equals #asWord ( #range ( B, 0, N ) ) } #And + { #range ( B, N, lengthBytes(B) -Int N ) #Equals B2 } + requires N <=Int lengthBytes(B) + [simplification(60), concrete(B, N)] + // // Specific simplifications // @@ -212,6 +246,34 @@ module LIDO-LEMMAS requires #asWord ( BUF1 ) ==Int 0 [simplification, concrete(BUF1)] + // + // Rules + // + + // 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] + endmodule module LIDO-LEMMAS-SPEC diff --git a/test/kontrol/scripts/run-kontrol.sh b/test/kontrol/scripts/run-kontrol.sh index cd055976..a3c21760 100755 --- a/test/kontrol/scripts/run-kontrol.sh +++ b/test/kontrol/scripts/run-kontrol.sh @@ -28,10 +28,12 @@ kontrol_prove() { notif "Kontrol Prove" # shellcheck disable=SC2086 run kontrol prove \ + --verbose \ --max-depth $max_depth \ --max-iterations $max_iterations \ --smt-timeout $smt_timeout \ --workers $workers \ + --max-frontier-parallel $max_frontier_parallel \ $reinit \ $bug_report \ $break_on_calls \ @@ -98,7 +100,24 @@ regen= test_list=() if [ "$SCRIPT_TESTS" == true ]; then # Here go the list of tests to execute with the `script` option - test_list=( "VetoSignallingTest.testTransitionNormalToVetoSignalling" ) + test_list=( + "VetoSignallingTest.testTransitionNormalToVetoSignalling" + "VetoSignallingTest.testVetoSignallingInvariantsHoldInitially" + "EscrowAccountingTest.testRageQuitSupport" + "EscrowAccountingTest.testEscrowInvariantsHoldInitially" + "EscrowAccountingTest.testLockStEth" + "EscrowAccountingTest.testUnlockStEth" + "EscrowOperationsTest.testCannotUnlockBeforeMinLockTime" + "EscrowOperationsTest.testCannotLockUnlockInRageQuitEscrowState" + "EscrowOperationsTest.testCannotWithdrawBeforeEthClaimTimelockElapsed" + "ProposalOperationsTest.testCannotProposeInInvalidState" + "ProposalOperationsTest.testCannotScheduleInInvalidStates" + "ProposalOperationsTest.testCannotScheduleSubmissionAfterLastVetoSignalling" + "ProposalOperationsTest.testCanceledOrExecutedActionsCannotBeRescheduled" + "ProposalOperationsTest.testCannotScheduleBeforeMinTimelock" + "ProposalOperationsTest.testSchedulingSuccess" + "ProposalOperationsTest.testCannotExecuteBeforeEmergencyProtectionTimelock" + ) elif [ "$CUSTOM_TESTS" != 0 ]; then test_list=( "${@:${CUSTOM_TESTS}}" ) fi @@ -115,7 +134,7 @@ done ######################### max_depth=10000 max_iterations=10000 -smt_timeout=100000 +smt_timeout=1000 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 @@ -124,6 +143,7 @@ if [ "$CUSTOM_TESTS" == 0 ] && [ "$SCRIPT_TESTS" == false ]; then else workers=$((${#test_list[@]}>max_workers ? max_workers : ${#test_list[@]})) fi +max_frontier_parallel=6 reinit=--reinit reinit= break_on_calls=--no-break-on-calls diff --git a/test/kontrol/scripts/versions.json b/test/kontrol/scripts/versions.json index 38350d43..9368fc76 100644 --- a/test/kontrol/scripts/versions.json +++ b/test/kontrol/scripts/versions.json @@ -1,4 +1,4 @@ { - "kontrol": "0.1.242", + "kontrol": "0.1.314", "kontrol-cheatcodes": "master" }