Add EscrowOperationsTest and update Setup

runtimeverification · Jul 4, 2024 · 01d53e9 · 01d53e9
1 parent aa191ed
commit 01d53e9
Show file tree

Hide file tree

Showing 3 changed files with 165 additions and 4 deletions.
diff --git a/test/kontrol/DualGovernanceSetUp.sol b/test/kontrol/DualGovernanceSetUp.sol
@@ -40,13 +40,21 @@ contract DualGovernanceSetUp is StorageSetup {
         // ?STORAGE1
         // ?WORD8: totalSharesLocked
         // ?WORD9: totalClaimedEthAmount
-        // ?WORD10: rageQuitExtensionDelayPeriodEnd
+        // ?WORD10: withdrawalRequestCount
+        // ?WORD11: lastWithdrawalRequestSubmitted
+        // ?WORD12: claimedWithdrawalRequests
+        // ?WORD13: rageQuitExtensionDelayPeriodEnd
+        // ?WORD14: rageQuitEthClaimTimelockStart
         _signallingEscrowStorageSetup(signallingEscrow, dualGovernance, stEth);
 
         // ?STORAGE2
-        // ?WORD11: totalSharesLocked
-        // ?WORD12: totalClaimedEthAmount
-        // ?WORD13: rageQuitExtensionDelayPeriodEnd
+        // ?WORD15: totalSharesLocked
+        // ?WORD16: totalClaimedEthAmount
+        // ?WORD17: withdrawalRequestCount
+        // ?WORD18: lastWithdrawalRequestSubmitted
+        // ?WORD19: claimedWithdrawalRequests
+        // ?WORD20: rageQuitExtensionDelayPeriodEnd
+        // ?WORD21: rageQuitEthClaimTimelockStart
         _rageQuitEscrowStorageSetup(rageQuitEscrow, dualGovernance, stEth);
 
         // ?STORAGE3

diff --git a/test/kontrol/EscrowOperations.t.sol 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/StorageSetup.sol b/test/kontrol/StorageSetup.sol
@@ -119,9 +119,26 @@ contract StorageSetup is KontrolTest {
         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));
     }