From ed2cb4e58cb698c875495b47250c6dc9e3dfb1a4 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Mon, 22 Jul 2024 23:54:58 +0200 Subject: [PATCH 01/12] further externals --- test/kontrol/ActivateNextState.t.sol | 46 +++--- test/kontrol/DualGovernanceSetUp.sol | 8 +- test/kontrol/EscrowAccounting.t.sol | 8 +- test/kontrol/EscrowLockUnlock.t.sol | 8 +- test/kontrol/EscrowOperations.t.sol | 8 +- test/kontrol/StorageSetup.sol | 62 +++---- test/kontrol/lido-lemmas.k | 237 ++++++++++++++++----------- 7 files changed, 211 insertions(+), 166 deletions(-) diff --git a/test/kontrol/ActivateNextState.t.sol b/test/kontrol/ActivateNextState.t.sol index 36ad1b66..a67572d2 100644 --- a/test/kontrol/ActivateNextState.t.sol +++ b/test/kontrol/ActivateNextState.t.sol @@ -11,13 +11,13 @@ contract ActivateNextStateMock is StorageSetup { Escrow signallingEscrow = Escrow(payable(dualGovernance.getVetoSignallingEscrow())); Escrow rageQuitEscrow = Escrow(payable(dualGovernance.getRageQuitEscrow())); address sender = address(uint160(uint256(keccak256("sender")))); - AccountingRecord memory pre = _saveAccountingRecord(sender, signallingEscrow); + AccountingRecord memory pre = this.saveAccountingRecord(sender, signallingEscrow); - _dualGovernanceStorageInvariants(Mode.Assert, dualGovernance); - _escrowStorageInvariants(Mode.Assert, signallingEscrow); - _signallingEscrowStorageInvariants(Mode.Assert, signallingEscrow); - _escrowStorageInvariants(Mode.Assert, rageQuitEscrow); - _rageQuitEscrowStorageInvariants(Mode.Assert, rageQuitEscrow); + this.dualGovernanceStorageInvariants(Mode.Assert, dualGovernance); + this.escrowStorageInvariants(Mode.Assert, signallingEscrow); + this.signallingEscrowStorageInvariants(Mode.Assert, signallingEscrow); + this.escrowStorageInvariants(Mode.Assert, rageQuitEscrow); + this.rageQuitEscrowStorageInvariants(Mode.Assert, rageQuitEscrow); State initialState = dualGovernance.getCurrentState(); uint256 rageQuitSupport = signallingEscrow.getRageQuitSupport(); @@ -31,17 +31,17 @@ contract ActivateNextStateMock is StorageSetup { address escrowMasterCopy = signallingEscrow.MASTER_COPY(); IEscrow newSignallingEscrow = IEscrow(Clones.clone(escrowMasterCopy)); - _dualGovernanceInitializeStorage(dualGovernance, newSignallingEscrow, signallingEscrow); - _signallingEscrowInitializeStorage(newSignallingEscrow, dualGovernance); - _rageQuitEscrowInitializeStorage(signallingEscrow, dualGovernance); + this.dualGovernanceInitializeStorage(dualGovernance, newSignallingEscrow, signallingEscrow); + this.signallingEscrowInitializeStorage(newSignallingEscrow, dualGovernance); + this.rageQuitEscrowInitializeStorage(signallingEscrow, dualGovernance); } else { - _dualGovernanceInitializeStorage(dualGovernance, signallingEscrow, rageQuitEscrow); - _signallingEscrowInitializeStorage(signallingEscrow, dualGovernance); - _rageQuitEscrowInitializeStorage(rageQuitEscrow, dualGovernance); + this.dualGovernanceInitializeStorage(dualGovernance, signallingEscrow, rageQuitEscrow); + this.signallingEscrowInitializeStorage(signallingEscrow, dualGovernance); + this.rageQuitEscrowInitializeStorage(rageQuitEscrow, dualGovernance); } - AccountingRecord memory post = _saveAccountingRecord(sender, signallingEscrow); - _establishEqualAccountingRecords(Mode.Assume, pre, post); + AccountingRecord memory post = this.saveAccountingRecord(sender, signallingEscrow); + this.establishEqualAccountingRecords(Mode.Assume, pre, post); } } @@ -51,7 +51,7 @@ contract ActivateNextStateTest is DualGovernanceSetUp { uint256 rageQuitSupport = signallingEscrow.getRageQuitSupport(); (,, Timestamp vetoSignallingActivationTime,) = dualGovernance.getVetoSignallingState(); address sender = address(uint160(uint256(keccak256("sender")))); - AccountingRecord memory pre = _saveAccountingRecord(sender, signallingEscrow); + AccountingRecord memory pre = this.saveAccountingRecord(sender, signallingEscrow); dualGovernance.activateNextState(); @@ -64,19 +64,19 @@ contract ActivateNextStateTest is DualGovernanceSetUp { assert(dualGovernance.getRageQuitEscrow() == address(signallingEscrow)); assert(EscrowState(_getCurrentState(signallingEscrow)) == EscrowState.RageQuitEscrow); - _dualGovernanceStorageInvariants(Mode.Assert, dualGovernance); - _signallingEscrowStorageInvariants(Mode.Assert, newSignallingEscrow); - _rageQuitEscrowStorageInvariants(Mode.Assert, signallingEscrow); + 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); - _dualGovernanceStorageInvariants(Mode.Assert, dualGovernance); - _signallingEscrowStorageInvariants(Mode.Assert, signallingEscrow); - _rageQuitEscrowStorageInvariants(Mode.Assert, rageQuitEscrow); + this.dualGovernanceStorageInvariants(Mode.Assert, dualGovernance); + this.signallingEscrowStorageInvariants(Mode.Assert, signallingEscrow); + this.rageQuitEscrowStorageInvariants(Mode.Assert, rageQuitEscrow); } - AccountingRecord memory post = _saveAccountingRecord(sender, signallingEscrow); - _establishEqualAccountingRecords(Mode.Assert, pre, post); + 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 index 8e37b69a..268cf541 100644 --- a/test/kontrol/DualGovernanceSetUp.sol +++ b/test/kontrol/DualGovernanceSetUp.sol @@ -49,7 +49,7 @@ contract DualGovernanceSetUp is StorageSetup { // ?WORD: totalPooledEther // ?WORD0: totalShares // ?WORD1: shares[signallingEscrow] - _stEthStorageSetup(stEth, signallingEscrow); + this.stEthStorageSetup(stEth, signallingEscrow); // ?STORAGE0 // ?WORD2: currentState @@ -58,7 +58,7 @@ contract DualGovernanceSetUp is StorageSetup { // ?WORD5: vetoSignallingReactivationTime // ?WORD6: lastAdoptableStaateExitedAt // ?WORD7: rageQuitRound - _dualGovernanceInitializeStorage(dualGovernance, signallingEscrow, rageQuitEscrow); + this.dualGovernanceInitializeStorage(dualGovernance, signallingEscrow, rageQuitEscrow); // ?STORAGE1 // ?WORD8: lockedShares @@ -69,7 +69,7 @@ contract DualGovernanceSetUp is StorageSetup { // ?WORD13: rageQuitExtensionDelay // ?WORD14: rageQuitWithdrawalsTimelock // ?WORD15: rageQuitTimelockStartedAt - _signallingEscrowInitializeStorage(signallingEscrow, dualGovernance); + this.signallingEscrowInitializeStorage(signallingEscrow, dualGovernance); // ?STORAGE2 // ?WORD16: lockedShares @@ -80,7 +80,7 @@ contract DualGovernanceSetUp is StorageSetup { // ?WORD21: rageQuitExtensionDelay // ?WORD22: rageQuitWithdrawalsTimelock // ?WORD23: rageQuitTimelockStartedAt - _rageQuitEscrowInitializeStorage(rageQuitEscrow, dualGovernance); + this.rageQuitEscrowInitializeStorage(rageQuitEscrow, dualGovernance); // ?STORAGE3 kevm.symbolicStorage(address(timelock)); diff --git a/test/kontrol/EscrowAccounting.t.sol b/test/kontrol/EscrowAccounting.t.sol index cbe616ee..89aba3ce 100644 --- a/test/kontrol/EscrowAccounting.t.sol +++ b/test/kontrol/EscrowAccounting.t.sol @@ -42,7 +42,7 @@ contract EscrowAccountingTest is EscrowInvariants { // ?WORD: totalPooledEther // ?WORD0: totalShares // ?WORD1: shares[escrow] - _stEthStorageSetup(stEth, escrow); + this.stEthStorageSetup(stEth, escrow); } function _setUpGenericState() public { @@ -61,7 +61,7 @@ contract EscrowAccountingTest is EscrowInvariants { // ?WORD9: rageQuitExtensionDelay // ?WORD10: rageQuitWithdrawalsTimelock // ?WORD11: rageQuitTimelockStartedAt - _escrowStorageSetup(escrow, DualGovernance(dualGovernanceAddress), EscrowState(currentState)); + this.escrowStorageSetup(escrow, DualGovernance(dualGovernanceAddress), EscrowState(currentState)); } function testRageQuitSupport() public { @@ -91,7 +91,7 @@ contract EscrowAccountingTest is EscrowInvariants { address sender = address(uint160(uint256(keccak256("sender")))); vm.assume(stEth.sharesOf(sender) < ethUpperBound); - AccountingRecord memory pre = _saveAccountingRecord(sender, escrow); + AccountingRecord memory pre = this.saveAccountingRecord(sender, escrow); _escrowInvariants(Mode.Assume, escrow); _escrowUserInvariants(Mode.Assume, escrow, sender); @@ -107,7 +107,7 @@ contract EscrowAccountingTest is EscrowInvariants { _escrowInvariants(Mode.Assert, escrow); _escrowUserInvariants(Mode.Assert, escrow, sender); - AccountingRecord memory post = _saveAccountingRecord(sender, escrow); + AccountingRecord memory post = this.saveAccountingRecord(sender, escrow); assert(post.userSharesLocked == pre.userSharesLocked - stEthAmount); assert(post.totalSharesLocked == pre.totalSharesLocked - stEthAmount); assert(post.userLastLockedTime == Timestamps.now()); diff --git a/test/kontrol/EscrowLockUnlock.t.sol b/test/kontrol/EscrowLockUnlock.t.sol index f23dc367..bb1a120c 100644 --- a/test/kontrol/EscrowLockUnlock.t.sol +++ b/test/kontrol/EscrowLockUnlock.t.sol @@ -42,7 +42,7 @@ contract EscrowLockUnlockTest is EscrowInvariants, DualGovernanceSetUp { vm.assume(stEth.balanceOf(sender) < ethUpperBound); vm.assume(_getLastAssetsLockTimestamp(signallingEscrow, sender) < timeUpperBound); - AccountingRecord memory pre = _saveAccountingRecord(sender, signallingEscrow); + AccountingRecord memory pre = this.saveAccountingRecord(sender, signallingEscrow); vm.assume(0 < amount); vm.assume(amount <= pre.userBalance); vm.assume(amount <= pre.allowance); @@ -68,7 +68,7 @@ contract EscrowLockUnlockTest is EscrowInvariants, DualGovernanceSetUp { _signallingEscrowInvariants(Mode.Assert, signallingEscrow); _escrowUserInvariants(Mode.Assert, signallingEscrow, sender); - AccountingRecord memory post = _saveAccountingRecord(sender, signallingEscrow); + AccountingRecord memory post = this.saveAccountingRecord(sender, signallingEscrow); assert(post.escrowState == EscrowState.SignallingEscrow); assert(post.userShares == pre.userShares - amountInShares); assert(post.escrowShares == pre.escrowShares + amountInShares); @@ -93,7 +93,7 @@ contract EscrowLockUnlockTest is EscrowInvariants, DualGovernanceSetUp { vm.assume(stEth.sharesOf(sender) < ethUpperBound); vm.assume(_getLastAssetsLockTimestamp(signallingEscrow, sender) < timeUpperBound); - AccountingRecord memory pre = _saveAccountingRecord(sender, signallingEscrow); + AccountingRecord memory pre = this.saveAccountingRecord(sender, signallingEscrow); vm.assume(pre.userSharesLocked <= pre.totalSharesLocked); vm.assume(Timestamps.now() >= addTo(config.SIGNALLING_ESCROW_MIN_LOCK_TIME(), pre.userLastLockedTime)); @@ -109,7 +109,7 @@ contract EscrowLockUnlockTest is EscrowInvariants, DualGovernanceSetUp { _signallingEscrowInvariants(Mode.Assert, signallingEscrow); _escrowUserInvariants(Mode.Assert, signallingEscrow, sender); - AccountingRecord memory post = _saveAccountingRecord(sender, signallingEscrow); + AccountingRecord memory post = this.saveAccountingRecord(sender, signallingEscrow); assert(post.escrowState == EscrowState.SignallingEscrow); assert(post.userShares == pre.userShares + pre.userSharesLocked); assert(post.userSharesLocked == 0); diff --git a/test/kontrol/EscrowOperations.t.sol b/test/kontrol/EscrowOperations.t.sol index bba11e9f..bd70badf 100644 --- a/test/kontrol/EscrowOperations.t.sol +++ b/test/kontrol/EscrowOperations.t.sol @@ -17,7 +17,7 @@ contract EscrowOperationsTest is EscrowAccountingTest { vm.assume(stEth.sharesOf(sender) < ethUpperBound); vm.assume(_getLastAssetsLockTimestamp(escrow, sender) < timeUpperBound); - AccountingRecord memory pre = _saveAccountingRecord(sender, escrow); + AccountingRecord memory pre = this.saveAccountingRecord(sender, escrow); vm.assume(pre.escrowState == EscrowState.SignallingEscrow); vm.assume(pre.userSharesLocked <= pre.totalSharesLocked); @@ -41,7 +41,7 @@ contract EscrowOperationsTest is EscrowAccountingTest { vm.assume(stEth.sharesOf(sender) < ethUpperBound); vm.assume(stEth.balanceOf(sender) < ethUpperBound); - AccountingRecord memory pre = _saveAccountingRecord(sender, escrow); + AccountingRecord memory pre = this.saveAccountingRecord(sender, escrow); vm.assume(0 < amount); vm.assume(amount <= pre.userBalance); vm.assume(amount <= pre.allowance); @@ -66,7 +66,7 @@ contract EscrowOperationsTest is EscrowAccountingTest { vm.prank(sender); escrow.lockStETH(amount); - AccountingRecord memory afterLock = _saveAccountingRecord(sender, escrow); + AccountingRecord memory afterLock = this.saveAccountingRecord(sender, escrow); vm.assume(afterLock.userShares < ethUpperBound); //vm.assume(afterLock.userLastLockedTime < timeUpperBound); vm.assume(afterLock.userSharesLocked <= afterLock.totalSharesLocked); @@ -79,7 +79,7 @@ contract EscrowOperationsTest is EscrowAccountingTest { _signallingEscrowInvariants(Mode.Assert, escrow); _escrowUserInvariants(Mode.Assert, escrow, sender); - AccountingRecord memory post = _saveAccountingRecord(sender, escrow); + AccountingRecord memory post = this.saveAccountingRecord(sender, escrow); assert(post.escrowState == EscrowState.SignallingEscrow); assert(post.userShares == pre.userShares); assert(post.escrowShares == pre.escrowShares); diff --git a/test/kontrol/StorageSetup.sol b/test/kontrol/StorageSetup.sol index 45644605..997e2d71 100644 --- a/test/kontrol/StorageSetup.sol +++ b/test/kontrol/StorageSetup.sol @@ -13,7 +13,7 @@ import "contracts/model/WstETHAdapted.sol"; import "test/kontrol/KontrolTest.sol"; contract StorageSetup is KontrolTest { - function _stEthStorageSetup(StETHModel _stEth, IEscrow _escrow) internal { + function stEthStorageSetup(StETHModel _stEth, IEscrow _escrow) external { kevm.symbolicStorage(address(_stEth)); // Slot 0 uint256 totalPooledEther = kevm.freshUInt(32); @@ -59,11 +59,11 @@ contract StorageSetup is KontrolTest { return uint8(_loadUInt256(address(_dualGovernance), 6) >> 240); } - function _dualGovernanceStorageSetup( + function dualGovernanceStorageSetup( DualGovernance _dualGovernance, IEscrow _signallingEscrow, IEscrow _rageQuitEscrow - ) internal { + ) external { kevm.symbolicStorage(address(_dualGovernance)); // Slot 5 + 0 = 5 uint8 currentState = uint8(kevm.freshUInt(1)); @@ -99,7 +99,7 @@ contract StorageSetup is KontrolTest { _storeBytes32(address(_dualGovernance), 6, slot6); } - function _dualGovernanceStorageInvariants(Mode mode, DualGovernance _dualGovernance) internal { + function dualGovernanceStorageInvariants(Mode mode, DualGovernance _dualGovernance) external { uint8 currentState = _getCurrentState(_dualGovernance); uint40 enteredAt = _getEnteredAt(_dualGovernance); uint40 vetoSignallingActivationTime = _getVetoSignallingActivationTime(_dualGovernance); @@ -114,7 +114,7 @@ contract StorageSetup is KontrolTest { _establish(mode, lastAdoptableStateExitedAt <= block.timestamp); } - function _dualGovernanceAssumeBounds(DualGovernance _dualGovernance) internal { + function dualGovernanceAssumeBounds(DualGovernance _dualGovernance) external { uint40 enteredAt = _getEnteredAt(_dualGovernance); uint40 vetoSignallingActivationTime = _getVetoSignallingActivationTime(_dualGovernance); uint40 vetoSignallingReactivationTime = _getVetoSignallingReactivationTime(_dualGovernance); @@ -128,14 +128,14 @@ contract StorageSetup is KontrolTest { vm.assume(rageQuitRound < type(uint8).max); } - function _dualGovernanceInitializeStorage( + function dualGovernanceInitializeStorage( DualGovernance _dualGovernance, IEscrow _signallingEscrow, IEscrow _rageQuitEscrow - ) internal { - _dualGovernanceStorageSetup(_dualGovernance, _signallingEscrow, _rageQuitEscrow); - _dualGovernanceStorageInvariants(Mode.Assume, _dualGovernance); - _dualGovernanceAssumeBounds(_dualGovernance); + ) external { + this.dualGovernanceStorageSetup(_dualGovernance, _signallingEscrow, _rageQuitEscrow); + this.dualGovernanceStorageInvariants(Mode.Assume, _dualGovernance); + this.dualGovernanceAssumeBounds(_dualGovernance); } function _getCurrentState(IEscrow _escrow) internal view returns (uint8) { @@ -202,13 +202,13 @@ contract StorageSetup is KontrolTest { AccountingRecord accounting; } - function _saveEscrowRecord(address user, Escrow escrow) internal view returns (EscrowRecord memory er) { - AccountingRecord memory accountingRecord = _saveAccountingRecord(user, escrow); + 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) internal view returns (AccountingRecord memory ar) { + 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); @@ -225,11 +225,11 @@ contract StorageSetup is KontrolTest { ar.userLastLockedTime = Timestamp.wrap(uint40(lastAssetsLockTimestamp)); } - function _establishEqualAccountingRecords( + function establishEqualAccountingRecords( Mode mode, AccountingRecord memory ar1, AccountingRecord memory ar2 - ) internal view { + ) external view { _establish(mode, ar1.allowance == ar2.allowance); _establish(mode, ar1.userBalance == ar2.userBalance); _establish(mode, ar1.escrowBalance == ar2.escrowBalance); @@ -243,7 +243,7 @@ contract StorageSetup is KontrolTest { _establish(mode, ar1.userLastLockedTime == ar2.userLastLockedTime); } - function _escrowStorageSetup(IEscrow _escrow, DualGovernance _dualGovernance, EscrowState _currentState) internal { + function escrowStorageSetup(IEscrow _escrow, DualGovernance _dualGovernance, EscrowState _currentState) external { kevm.symbolicStorage(address(_escrow)); // Slot 0 { @@ -300,7 +300,7 @@ contract StorageSetup is KontrolTest { } } - function _escrowStorageInvariants(Mode mode, IEscrow _escrow) internal { + function escrowStorageInvariants(Mode mode, IEscrow _escrow) external { uint8 batchesQueueStatus = _getBatchesQueueStatus(_escrow); uint32 rageQuitExtensionDelay = _getRageQuitExtensionDelay(_escrow); uint32 rageQuitWithdrawalsTimelock = _getRageQuitWithdrawalsTimelock(_escrow); @@ -312,7 +312,7 @@ contract StorageSetup is KontrolTest { _establish(mode, rageQuitTimelockStartedAt <= block.timestamp); } - function _escrowAssumeBounds(IEscrow _escrow) internal { + function escrowAssumeBounds(IEscrow _escrow) external { uint128 lockedShares = _getStEthLockedShares(_escrow); uint128 claimedEth = _getClaimedEth(_escrow); uint128 unfinalizedShares = _getUnfinalizedShares(_escrow); @@ -330,17 +330,17 @@ contract StorageSetup is KontrolTest { vm.assume(rageQuitTimelockStartedAt < timeUpperBound); } - function _escrowInitializeStorage( + function escrowInitializeStorage( IEscrow _escrow, DualGovernance _dualGovernance, EscrowState _currentState - ) internal { - _escrowStorageSetup(_escrow, _dualGovernance, _currentState); - _escrowStorageInvariants(Mode.Assume, _escrow); - _escrowAssumeBounds(_escrow); + ) external { + this.escrowStorageSetup(_escrow, _dualGovernance, _currentState); + this.escrowStorageInvariants(Mode.Assume, _escrow); + this.escrowAssumeBounds(_escrow); } - function _signallingEscrowStorageInvariants(Mode mode, IEscrow _signallingEscrow) internal { + function signallingEscrowStorageInvariants(Mode mode, IEscrow _signallingEscrow) external { uint32 rageQuitExtensionDelay = _getRageQuitExtensionDelay(_signallingEscrow); uint32 rageQuitWithdrawalsTimelock = _getRageQuitWithdrawalsTimelock(_signallingEscrow); uint40 rageQuitTimelockStartedAt = _getRageQuitTimelockStartedAt(_signallingEscrow); @@ -352,19 +352,19 @@ contract StorageSetup is KontrolTest { _establish(mode, batchesQueueStatus == uint8(WithdrawalsBatchesQueue.Status.Empty)); } - function _signallingEscrowInitializeStorage(IEscrow _signallingEscrow, DualGovernance _dualGovernance) internal { - _escrowInitializeStorage(_signallingEscrow, _dualGovernance, EscrowState.SignallingEscrow); - _signallingEscrowStorageInvariants(Mode.Assume, _signallingEscrow); + function signallingEscrowInitializeStorage(IEscrow _signallingEscrow, DualGovernance _dualGovernance) external { + this.escrowInitializeStorage(_signallingEscrow, _dualGovernance, EscrowState.SignallingEscrow); + this.signallingEscrowStorageInvariants(Mode.Assume, _signallingEscrow); } - function _rageQuitEscrowStorageInvariants(Mode mode, IEscrow _rageQuitEscrow) internal { + function rageQuitEscrowStorageInvariants(Mode mode, IEscrow _rageQuitEscrow) external { uint8 batchesQueueStatus = _getBatchesQueueStatus(_rageQuitEscrow); _establish(mode, batchesQueueStatus != uint8(WithdrawalsBatchesQueue.Status.Empty)); } - function _rageQuitEscrowInitializeStorage(IEscrow _rageQuitEscrow, DualGovernance _dualGovernance) internal { - _escrowInitializeStorage(_rageQuitEscrow, _dualGovernance, EscrowState.RageQuitEscrow); - _rageQuitEscrowStorageInvariants(Mode.Assume, _rageQuitEscrow); + function rageQuitEscrowInitializeStorage(IEscrow _rageQuitEscrow, DualGovernance _dualGovernance) external { + this.escrowInitializeStorage(_rageQuitEscrow, _dualGovernance, EscrowState.RageQuitEscrow); + this.rageQuitEscrowStorageInvariants(Mode.Assume, _rageQuitEscrow); } } diff --git a/test/kontrol/lido-lemmas.k b/test/kontrol/lido-lemmas.k index 3022d13d..4c2a0249 100644 --- a/test/kontrol/lido-lemmas.k +++ b/test/kontrol/lido-lemmas.k @@ -27,38 +27,15 @@ module LIDO-LEMMAS rule ethUpperBound => 2 ^Int ethMaxWidth // ---------------------------------------- - // |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 + // chop and +Int + rule [chop-plus]: chop (A +Int B) ==Int 0 => A ==Int (-1) *Int B 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 + // chop and -Int + rule [chop-zero-minus]: 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] + [concrete(B), simplification, comm, preserves-definedness] // *Int rule A *Int B ==Int 0 => A ==Int 0 orBool B ==Int 0 [simplification] @@ -73,7 +50,9 @@ module LIDO-LEMMAS // Further arithmetic rule ( X *Int Y ) /Int Y => X requires Y =/=Int 0 [simplification, preserves-definedness] + rule ( X *Int Y ) /Int X => Y requires X =/=Int 0 [simplification, preserves-definedness] rule ( X ==Int ( X *Int Y ) /Word Y ) orBool Y ==Int 0 => true [simplification, preserves-definedness] + rule ( X ==Int ( Y *Int X ) /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 ( 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)] + // #asWord + rule #asWord ( B1 +Bytes B2 ) => #asWord ( B2 ) + requires #asWord ( B1 ) ==Int 0 + [simplification, concrete(B1)] + + rule #asWord( BA ) >>Int N => #asWord( #range ( BA, 0, lengthBytes( BA ) -Int ( N /Int 8 ) ) ) + requires 0 <=Int N andBool N modInt 8 ==Int 0 + [simplification, concrete(N), preserves-definedness] - // 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] + // >>Int + rule [shift-to-div]: X >>Int N => X /Int (2 ^Int N) [simplification(60), concrete(N)] + + // bool2Word + rule [bool2Word-lt-true]: bool2Word(_:Bool) true requires 1 notBool B [simplification] // // .Bytes @@ -228,43 +214,130 @@ module LIDO-LEMMAS requires #rangeUInt(256, X) andBool 0 true [simplification, smt-lemma] + // + // Overflows and ranges + // + rule X <=Int A +Int B => true requires X <=Int 0 andBool 0 <=Int A andBool 0 <=Int B [concrete(X), simplification, preserves-definedness] + rule X <=Int A *Int B => true requires X <=Int 0 andBool 0 <=Int A andBool 0 <=Int B [concrete(X), simplification, preserves-definedness] + rule X <=Int A /Int B => true requires X <=Int 0 andBool 0 <=Int A andBool 0 >Int N => X /Int (2 ^Int N) [simplification, concrete(N)] + rule X true requires X <=Int 0 andBool 0 true requires X <=Int 0 andBool 0 <=Int A andBool 0 true requires X <=Int 0 andBool 0 true requires X <=Int 0 andBool 0 #asWord ( BUF2 ) - requires #asWord ( BUF1 ) ==Int 0 - [simplification, concrete(BUF1)] + rule [chop-no-overflow-add-l]: X:Int <=Int chop ( X +Int Y:Int ) => X +Int Y X +Int Y X *Int Y X *Int Y X /Int Y - #asWord ( ( #buf ( 32 -Int lengthBytes ( SLOT ), 0 ) +Bytes SLOT ) [ 32 -Int ( log2Int ( ( maxUInt256 xorInt ( ( MASK_SLOT /Int SHIFT ) *Int SHIFT ) ) +Int 1 ) /Int 8 ) := - #buf ( ( log2Int ( ( maxUInt256 xorInt ( ( MASK_SLOT /Int SHIFT ) *Int SHIFT ) ) +Int 1 ) -Int log2Int ( SHIFT ) ) /Int 8, VALUE:Int ) ] ) - requires // Appropriate bounds for SHIFT, MASK_SLOT, and SLOT - #rangeUInt(256, SHIFT) andBool #rangeUInt(256, MASK_SLOT) andBool lengthBytes(SLOT) <=Int 32 - // Shift is a power of two + + // Auxiliaries + + syntax Int ::= #getFirstOneBit(Int) [function, total] + syntax Int ::= #getFirstZeroBit(Int) [function, total] + + rule #getFirstOneBit(X:Int) => log2Int ( X &Int ( ( maxUInt256 xorInt X ) +Int 1 ) ) requires #rangeUInt(256, X) [concrete(X), simplification] + rule #getFirstOneBit(X:Int) => -1 requires notBool #rangeUInt(256, X) [concrete(X), simplification] + + rule #getFirstZeroBit(X:Int) => #getFirstOneBit ( maxUInt256 xorInt X ) requires #rangeUInt(256, X) [concrete(X), simplification] + rule #getFirstZeroBit(X:Int) => -1 requires notBool #rangeUInt(256, X) [concrete(X), simplification] + + syntax Int ::= #getMaskShiftBits(Int) [function, total] + syntax Int ::= #getMaskShiftBytes(Int) [function, total] + + rule #getMaskShiftBits(X:Int) => #getFirstZeroBit(X) [concrete(X), simplification] + + rule #getMaskShiftBytes(X:Int) => #getFirstZeroBit(X) /Int 8 requires #getMaskShiftBits(X) modInt 8 ==Int 0 [concrete(X), simplification, preserves-definedness] + rule #getMaskShiftBytes(X:Int) => -1 requires notBool ( #getMaskShiftBits(X) modInt 8 ==Int 0 ) [concrete(X), simplification, preserves-definedness] + + syntax Int ::= #getMaskWidthBits(Int) [function, total] + syntax Int ::= #getMaskWidthBytes(Int) [function, total] + + rule #getMaskWidthBits(X:Int) => #getFirstOneBit(X >>Int #getMaskShiftBits(X:Int)) requires #rangeUInt(256, X) [concrete(X), simplification] + rule #getMaskWidthBits(X:Int) => -1 requires notBool #rangeUInt(256, X) [concrete(X), simplification] + + rule #getMaskWidthBytes(X:Int) => #getMaskWidthBits(X) /Int 8 requires #getMaskWidthBits(X) modInt 8 ==Int 0 [concrete(X), simplification, preserves-definedness] + rule #getMaskWidthBytes(X:Int) => -1 requires notBool ( #getMaskWidthBits(X) modInt 8 ==Int 0 ) [concrete(X), simplification, preserves-definedness] + + syntax Bool ::= #isMask(Int) [function, total] + + rule #isMask(X:Int) => maxUInt256 ==Int X |Int ( 2 ^Int ( #getMaskShiftBits(X) +Int #getMaskWidthBits(X) ) -Int 1 ) + requires 0 <=Int #getMaskShiftBytes(X) andBool 0 <=Int #getMaskWidthBytes(X) + [concrete(X), simplification, preserves-definedness] + + rule #isMask(X:Int) => false + requires notBool ( 0 <=Int #getMaskShiftBytes(X) andBool 0 <=Int #getMaskWidthBytes(X) ) + [concrete(X), simplification, preserves-definedness] + + // Actual masking lemmas + + // |Int and +Bytes, into right + rule A |Int #asWord ( B1 +Bytes B2 ) => + #asWord ( B1 +Bytes #buf ( lengthBytes(B2), A |Int #asWord ( B2 ) ) ) + requires 0 <=Int A andBool A + #asWord ( ( #buf ( 32 -Int lengthBytes ( SLOT ), 0 ) +Bytes SLOT ) + [ 32 -Int ( #getMaskShiftBytes(MASK) +Int #getMaskWidthBytes(MASK) ) := + #buf ( #getMaskWidthBytes(MASK), VALUE:Int ) ] ) + requires #rangeUInt(256, SHIFT) andBool #rangeUInt(256, MASK) andBool lengthBytes(SLOT) <=Int 32 + andBool #isMask(MASK) andBool SHIFT ==Int 2 ^Int log2Int(SHIFT) - // MASK_SLOT preserves all bits below the starting point at log2Int ( SHIFT ) - andBool ( ( SHIFT -Int 1 ) &Int MASK_SLOT ) +Int 1 ==Int SHIFT - // MASK_SLOT preserves all bits starting from a certain point, - // which is identified by log2Int ( ( maxUInt256 xorInt ( ( MASK_SLOT /Int SHIFT ) *Int SHIFT ) ) +Int 1 ), - // and all bits between that point and the starting point are zero - andBool ( maxUInt256 xorInt ( ( MASK_SLOT /Int SHIFT ) *Int SHIFT ) ) +Int 1 ==Int - 2 ^Int log2Int ( ( maxUInt256 xorInt ( ( MASK_SLOT /Int SHIFT ) *Int SHIFT ) ) +Int 1 ) - // The start and endpoints are multiples of 8 - andBool log2Int ( SHIFT ) modInt 8 ==Int 0 - andBool log2Int ( ( maxUInt256 xorInt ( ( MASK_SLOT /Int SHIFT ) *Int SHIFT ) ) +Int 1 ) modInt 8 ==Int 0 - // VALUE is not wider than the gap - andBool 0 <=Int VALUE andBool VALUE + #asWord ( ( #buf ( 32 -Int lengthBytes ( SLOT ), 0 ) +Bytes SLOT ) + [ 32 -Int ( #getMaskShiftBytes(MASK) +Int #getMaskWidthBytes(MASK) ) := + #buf ( #getMaskWidthBytes(MASK), VALUE >>Int #getMaskShiftBits(MASK) ) ] ) + requires #rangeUInt(256, MASK) andBool lengthBytes(SLOT) <=Int 32 + andBool #isMask(MASK) + andBool 0 <=Int ( VALUE >>Int #getMaskShiftBits(MASK) ) + andBool ( VALUE >>Int #getMaskShiftBits(MASK) ) M:Map [ K2 <- V2 ] [ K1 <- V3 ] [simplification] + // + // keccak assumptions: these assumptions are not sound in principle, but are + // required for verification - they should ideally be collected at the end of execution + // + + rule 0 <=Int keccak( _ ) => true [simplification, smt-lemma] + rule keccak( _ ) true [simplification, smt-lemma] + + // keccak does not equal a concrete value + rule [keccak-eq-conc-false]: keccak(_A) ==Int _B => false [symbolic(_A), concrete(_B), simplification(30), comm] + rule [keccak-neq-conc-true]: keccak(_A) =/=Int _B => true [symbolic(_A), concrete(_B), simplification(30), comm] + rule [keccak-eq-conc-false-ml-lr]: { keccak(A) #Equals B } => { true #Equals keccak(A) ==Int B } [symbolic(A), concrete(B), simplification] + rule [keccak-eq-conc-false-ml-rl]: { B #Equals keccak(A) } => { true #Equals keccak(A) ==Int B } [symbolic(A), concrete(B), simplification] + + // keccak is injective + rule [keccak-inj]: keccak(A) ==Int keccak(B) => A ==K B [simplification] + rule [keccak-inj-ml]: { keccak(A) #Equals keccak(B) } => { true #Equals A ==K B } [simplification] + + // chop of negative keccak + rule chop (0 -Int keccak(BA)) => pow256 -Int keccak(BA) + [simplification] + + // keccak cannot equal a number outside of its range + rule { X #Equals keccak (_) } => #Bottom + requires X =Int pow256 + [concrete(X), simplification] + + // // Rules // @@ -318,43 +391,6 @@ module LIDO-LEMMAS-SPEC andBool WORD11:Int runLemma ( - #rangeUInt(256, maxUInt40) andBool #rangeUInt(256, 256) - andBool #rangeUInt(256, 115792089237316195423570985008687907853269984665640564039457583726438152929535) - andBool lengthBytes(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") ==Int 32 - andBool maxUInt40 +Int 1 ==Int 2 ^Int log2Int(maxUInt40 +Int 1) - andBool 256 ==Int 2 ^Int log2Int(256) - andBool maxUInt40 &Int ( 115792089237316195423570985008687907853269984665640564039457583726438152929535 /Int 256 ) ==Int 0 - andBool log2Int ( ( ( 115792089237316195423570985008687907853269984665640564039457583726438152929535 /Int 256 ) /Int ( maxUInt40 +Int 1 ) ) +Int 1 ) ==Int - 256 -Int log2Int (256) -Int log2Int (maxUInt40 +Int 1) - andBool 0 <=Int VALUE andBool VALUE doneLemma ( - true - ) ... - requires 0 runLemma ( - #rangeUInt(256, pow40) andBool #rangeUInt(256, 115792089237316195423570985008687907853269984665640562830531764394383466561535) andBool lengthBytes( #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 X - // Shift is a power of two - andBool pow40 ==Int 2 ^Int log2Int(pow40) - andBool ( ( pow40 -Int 1 ) &Int 115792089237316195423570985008687907853269984665640562830531764394383466561535 ) +Int 1 ==Int pow40 - andBool ( maxUInt256 xorInt ( ( 115792089237316195423570985008687907853269984665640562830531764394383466561535 /Int pow40 ) *Int pow40 ) ) +Int 1 ==Int - 2 ^Int log2Int ( ( maxUInt256 xorInt ( ( 115792089237316195423570985008687907853269984665640562830531764394383466561535 /Int pow40 ) *Int pow40 ) ) +Int 1 ) - andBool 0 <=Int TIMESTAMP_CELL andBool TIMESTAMP_CELL doneLemma ( - true - ) ... - - claim [master-masking-01]: - runLemma ( - ( ( maxUInt40 &Int TIMESTAMP_CELL:Int ) *Int 256 ) |Int ( 115792089237316195423570985008687907853269984665640564039457583726438152929535 &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"\x01" ) ) - ) => doneLemma ( - #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" ) - ) ... - requires 0 <=Int TIMESTAMP_CELL andBool TIMESTAMP_CELL runLemma ( STORAGE0:Map @@ -369,4 +405,13 @@ module LIDO-LEMMAS-SPEC [ 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 Date: Tue, 23 Jul 2024 10:01:41 +0200 Subject: [PATCH 02/12] further external calls --- test/kontrol/EscrowAccounting.t.sol | 26 +++++++++++++------------- test/kontrol/EscrowInvariants.sol | 6 +++--- test/kontrol/EscrowLockUnlock.t.sol | 24 ++++++++++++------------ test/kontrol/EscrowOperations.t.sol | 20 ++++++++++---------- test/kontrol/StorageSetup.sol | 2 +- 5 files changed, 39 insertions(+), 39 deletions(-) diff --git a/test/kontrol/EscrowAccounting.t.sol b/test/kontrol/EscrowAccounting.t.sol index 89aba3ce..ab6762ab 100644 --- a/test/kontrol/EscrowAccounting.t.sol +++ b/test/kontrol/EscrowAccounting.t.sol @@ -79,9 +79,9 @@ contract EscrowAccountingTest is EscrowInvariants { // Placeholder address to avoid complications with keccak of symbolic addresses address sender = address(uint160(uint256(keccak256("sender")))); - _escrowInvariants(Mode.Assert, escrow); - _signallingEscrowInvariants(Mode.Assert, escrow); - _escrowUserInvariants(Mode.Assert, escrow, sender); + this.escrowInvariants(Mode.Assert, escrow); + this.signallingEscrowInvariants(Mode.Assert, escrow); + this.escrowUserInvariants(Mode.Assert, escrow, sender); } function testRequestWithdrawals(uint256 stEthAmount) public { @@ -93,8 +93,8 @@ contract EscrowAccountingTest is EscrowInvariants { AccountingRecord memory pre = this.saveAccountingRecord(sender, escrow); - _escrowInvariants(Mode.Assume, escrow); - _escrowUserInvariants(Mode.Assume, escrow, sender); + this.escrowInvariants(Mode.Assume, escrow); + this.escrowUserInvariants(Mode.Assume, escrow, sender); // Only request one withdrawal for simplicity uint256[] memory stEthAmounts = new uint256[](1); @@ -104,8 +104,8 @@ contract EscrowAccountingTest is EscrowInvariants { escrow.requestWithdrawals(stEthAmounts); vm.stopPrank(); - _escrowInvariants(Mode.Assert, escrow); - _escrowUserInvariants(Mode.Assert, escrow, sender); + this.escrowInvariants(Mode.Assert, escrow); + this.escrowUserInvariants(Mode.Assert, escrow, sender); AccountingRecord memory post = this.saveAccountingRecord(sender, escrow); assert(post.userSharesLocked == pre.userSharesLocked - stEthAmount); @@ -120,11 +120,11 @@ contract EscrowAccountingTest is EscrowInvariants { vm.assume(EscrowState(_getCurrentState(escrow)) == EscrowState.RageQuitEscrow); - _escrowInvariants(Mode.Assume, escrow); + this.escrowInvariants(Mode.Assume, escrow); escrow.requestNextWithdrawalsBatch(maxBatchSize); - _escrowInvariants(Mode.Assert, escrow); + this.escrowInvariants(Mode.Assert, escrow); } function testClaimNextWithdrawalsBatch() public { @@ -136,8 +136,8 @@ contract EscrowAccountingTest is EscrowInvariants { vm.assume(EscrowState(_getCurrentState(escrow)) == EscrowState.RageQuitEscrow); - _escrowInvariants(Mode.Assume, escrow); - _escrowUserInvariants(Mode.Assume, escrow, sender); + this.escrowInvariants(Mode.Assume, escrow); + this.escrowUserInvariants(Mode.Assume, escrow, sender); // Only claim one unstETH for simplicity uint256 maxUnstETHIdsCount = 1; @@ -146,7 +146,7 @@ contract EscrowAccountingTest is EscrowInvariants { escrow.claimNextWithdrawalsBatch(maxUnstETHIdsCount); vm.stopPrank(); - _escrowInvariants(Mode.Assert, escrow); - _escrowUserInvariants(Mode.Assert, escrow, sender); + this.escrowInvariants(Mode.Assert, escrow); + this.escrowUserInvariants(Mode.Assert, escrow, sender); } } diff --git a/test/kontrol/EscrowInvariants.sol b/test/kontrol/EscrowInvariants.sol index ca4b8603..3fa77fe1 100644 --- a/test/kontrol/EscrowInvariants.sol +++ b/test/kontrol/EscrowInvariants.sol @@ -15,7 +15,7 @@ import "contracts/model/WstETHAdapted.sol"; import {StorageSetup} from "test/kontrol/StorageSetup.sol"; contract EscrowInvariants is StorageSetup { - function _escrowInvariants(Mode mode, Escrow escrow) internal view { + 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))); @@ -32,7 +32,7 @@ contract EscrowInvariants is StorageSetup { _establish(mode, uint8(currentState) < 3); } - function _signallingEscrowInvariants(Mode mode, Escrow escrow) internal view { + function signallingEscrowInvariants(Mode mode, Escrow escrow) external view { // TODO: Adapt to updated code /* if (_getCurrentState(escrow) == EscrowState.SignallingEscrow) { @@ -44,7 +44,7 @@ contract EscrowInvariants is StorageSetup { */ } - function _escrowUserInvariants(Mode mode, Escrow escrow, address user) internal view { + 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 index bb1a120c..957f5c8d 100644 --- a/test/kontrol/EscrowLockUnlock.t.sol +++ b/test/kontrol/EscrowLockUnlock.t.sol @@ -51,9 +51,9 @@ contract EscrowLockUnlockTest is EscrowInvariants, DualGovernanceSetUp { _assumeNoOverflow(pre.userSharesLocked, amountInShares); _assumeNoOverflow(pre.totalSharesLocked, amountInShares); - _escrowInvariants(Mode.Assume, signallingEscrow); - _signallingEscrowInvariants(Mode.Assume, signallingEscrow); - _escrowUserInvariants(Mode.Assume, signallingEscrow, sender); + this.escrowInvariants(Mode.Assume, signallingEscrow); + this.signallingEscrowInvariants(Mode.Assume, signallingEscrow); + this.escrowUserInvariants(Mode.Assume, signallingEscrow, sender); ActivateNextStateMock mock = new ActivateNextStateMock(); kevm.mockFunction( @@ -64,9 +64,9 @@ contract EscrowLockUnlockTest is EscrowInvariants, DualGovernanceSetUp { signallingEscrow.lockStETH(amount); vm.stopPrank(); - _escrowInvariants(Mode.Assert, signallingEscrow); - _signallingEscrowInvariants(Mode.Assert, signallingEscrow); - _escrowUserInvariants(Mode.Assert, signallingEscrow, sender); + 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.escrowState == EscrowState.SignallingEscrow); @@ -97,17 +97,17 @@ contract EscrowLockUnlockTest is EscrowInvariants, DualGovernanceSetUp { vm.assume(pre.userSharesLocked <= pre.totalSharesLocked); vm.assume(Timestamps.now() >= addTo(config.SIGNALLING_ESCROW_MIN_LOCK_TIME(), pre.userLastLockedTime)); - _escrowInvariants(Mode.Assume, signallingEscrow); - _signallingEscrowInvariants(Mode.Assume, signallingEscrow); - _escrowUserInvariants(Mode.Assume, signallingEscrow, sender); + this.escrowInvariants(Mode.Assume, signallingEscrow); + this.signallingEscrowInvariants(Mode.Assume, signallingEscrow); + this.escrowUserInvariants(Mode.Assume, signallingEscrow, sender); vm.startPrank(sender); signallingEscrow.unlockStETH(); vm.stopPrank(); - _escrowInvariants(Mode.Assert, signallingEscrow); - _signallingEscrowInvariants(Mode.Assert, signallingEscrow); - _escrowUserInvariants(Mode.Assert, signallingEscrow, sender); + 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.escrowState == EscrowState.SignallingEscrow); diff --git a/test/kontrol/EscrowOperations.t.sol b/test/kontrol/EscrowOperations.t.sol index bd70badf..c38f167b 100644 --- a/test/kontrol/EscrowOperations.t.sol +++ b/test/kontrol/EscrowOperations.t.sol @@ -50,9 +50,9 @@ contract EscrowOperationsTest is EscrowAccountingTest { _assumeNoOverflow(pre.userSharesLocked, amountInShares); _assumeNoOverflow(pre.totalSharesLocked, amountInShares); - _escrowInvariants(Mode.Assume, escrow); - _signallingEscrowInvariants(Mode.Assume, escrow); - _escrowUserInvariants(Mode.Assume, escrow, sender); + this.escrowInvariants(Mode.Assume, escrow); + this.signallingEscrowInvariants(Mode.Assume, escrow); + this.escrowUserInvariants(Mode.Assume, escrow, sender); if (pre.escrowState == EscrowState.RageQuitEscrow) { vm.prank(sender); @@ -75,9 +75,9 @@ contract EscrowOperationsTest is EscrowAccountingTest { vm.prank(sender); escrow.unlockStETH(); - _escrowInvariants(Mode.Assert, escrow); - _signallingEscrowInvariants(Mode.Assert, escrow); - _escrowUserInvariants(Mode.Assert, escrow, sender); + 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); @@ -110,8 +110,8 @@ contract EscrowOperationsTest is EscrowAccountingTest { vm.assume(userEth <= pre.totalEth); vm.assume(userEth <= address(escrow).balance); - _escrowInvariants(Mode.Assume, escrow); - _escrowUserInvariants(Mode.Assume, escrow, sender); + this.escrowInvariants(Mode.Assume, escrow); + this.escrowUserInvariants(Mode.Assume, escrow, sender); vm.assume(escrow.lastWithdrawalRequestSubmitted()); vm.assume(escrow.claimedWithdrawalRequests() == escrow.withdrawalRequestCount()); @@ -132,8 +132,8 @@ contract EscrowOperationsTest is EscrowAccountingTest { vm.prank(sender); escrow.withdraw(); - _escrowInvariants(Mode.Assert); - _escrowUserInvariants(Mode.Assert, sender); + this.escrowInvariants(Mode.Assert); + this.escrowUserInvariants(Mode.Assert, sender); AccountingRecord memory post = _saveAccountingRecord(sender, escrow); assert(post.userSharesLocked == 0); diff --git a/test/kontrol/StorageSetup.sol b/test/kontrol/StorageSetup.sol index 997e2d71..96351e14 100644 --- a/test/kontrol/StorageSetup.sol +++ b/test/kontrol/StorageSetup.sol @@ -221,7 +221,7 @@ contract StorageSetup is KontrolTest { ar.userUnstEthLockedShares = escrow.getVetoerState(user).unstETHLockedShares; ar.unfinalizedShares = escrow.getLockedAssetsTotals().unstETHUnfinalizedShares; uint256 lastAssetsLockTimestamp = _getLastAssetsLockTimestamp(escrow, user); - require(lastAssetsLockTimestamp < timeUpperBound); + require(lastAssetsLockTimestamp < timeUpperBound, "lastAssetsLockTimestamp >= timeUpperBound"); ar.userLastLockedTime = Timestamp.wrap(uint40(lastAssetsLockTimestamp)); } From acad7bbbaa2d131b6ce51f532b94de679c9cb1c6 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Tue, 23 Jul 2024 20:01:03 +0200 Subject: [PATCH 03/12] removing mock --- test/kontrol/DualGovernanceSetUp.sol | 1 + test/kontrol/EscrowLockUnlock.t.sol | 50 +++++++++++++++++++++++----- test/kontrol/lido-lemmas.k | 2 +- 3 files changed, 43 insertions(+), 10 deletions(-) diff --git a/test/kontrol/DualGovernanceSetUp.sol b/test/kontrol/DualGovernanceSetUp.sol index 268cf541..f3de8939 100644 --- a/test/kontrol/DualGovernanceSetUp.sol +++ b/test/kontrol/DualGovernanceSetUp.sol @@ -42,6 +42,7 @@ contract DualGovernanceSetUp is StorageSetup { Escrow 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)))); diff --git a/test/kontrol/EscrowLockUnlock.t.sol b/test/kontrol/EscrowLockUnlock.t.sol index 957f5c8d..291083f9 100644 --- a/test/kontrol/EscrowLockUnlock.t.sol +++ b/test/kontrol/EscrowLockUnlock.t.sol @@ -38,14 +38,46 @@ contract EscrowLockUnlockTest is EscrowInvariants, DualGovernanceSetUp { function testLockStEth(uint256 amount) public { // Placeholder address to avoid complications with keccak of symbolic addresses address sender = address(uint160(uint256(keccak256("sender")))); - vm.assume(stEth.sharesOf(sender) < ethUpperBound); + + uint256 senderShares = kevm.freshUInt(32); + vm.assume(senderShares < ethUpperBound); + stEth.setShares(sender, senderShares); vm.assume(stEth.balanceOf(sender) < ethUpperBound); - vm.assume(_getLastAssetsLockTimestamp(signallingEscrow, sender) < timeUpperBound); - AccountingRecord memory pre = this.saveAccountingRecord(sender, signallingEscrow); + uint256 senderAllowance = kevm.freshUInt(32); + // 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 <= pre.userBalance); - vm.assume(amount <= pre.allowance); + 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); @@ -55,10 +87,10 @@ contract EscrowLockUnlockTest is EscrowInvariants, DualGovernanceSetUp { this.signallingEscrowInvariants(Mode.Assume, signallingEscrow); this.escrowUserInvariants(Mode.Assume, signallingEscrow, sender); - ActivateNextStateMock mock = new ActivateNextStateMock(); - kevm.mockFunction( - address(dualGovernance), address(mock), abi.encodeWithSelector(mock.activateNextState.selector) - ); + // ActivateNextStateMock mock = new ActivateNextStateMock(); + // kevm.mockFunction( + // address(dualGovernance), address(mock), abi.encodeWithSelector(mock.activateNextState.selector) + // ); vm.startPrank(sender); signallingEscrow.lockStETH(amount); diff --git a/test/kontrol/lido-lemmas.k b/test/kontrol/lido-lemmas.k index 4c2a0249..29268804 100644 --- a/test/kontrol/lido-lemmas.k +++ b/test/kontrol/lido-lemmas.k @@ -48,7 +48,7 @@ module LIDO-LEMMAS 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 + // Further /Int and /Word arithmetic rule ( X *Int Y ) /Int Y => X requires Y =/=Int 0 [simplification, preserves-definedness] rule ( X *Int Y ) /Int X => Y requires X =/=Int 0 [simplification, preserves-definedness] rule ( X ==Int ( X *Int Y ) /Word Y ) orBool Y ==Int 0 => true [simplification, preserves-definedness] From 76553bca38e7f6ba81e19c108ad5bb0a3f405cc6 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Tue, 23 Jul 2024 21:07:42 +0200 Subject: [PATCH 04/12] minor adjustments --- test/kontrol/EscrowLockUnlock.t.sol | 3 +++ test/kontrol/lido-lemmas.k | 2 +- 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/test/kontrol/EscrowLockUnlock.t.sol b/test/kontrol/EscrowLockUnlock.t.sol index 291083f9..3acaad65 100644 --- a/test/kontrol/EscrowLockUnlock.t.sol +++ b/test/kontrol/EscrowLockUnlock.t.sol @@ -45,6 +45,9 @@ contract EscrowLockUnlockTest is EscrowInvariants, DualGovernanceSetUp { 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), diff --git a/test/kontrol/lido-lemmas.k b/test/kontrol/lido-lemmas.k index 29268804..bed22c7d 100644 --- a/test/kontrol/lido-lemmas.k +++ b/test/kontrol/lido-lemmas.k @@ -280,7 +280,7 @@ module LIDO-LEMMAS rule A |Int #asWord ( B1 +Bytes B2 ) => #asWord ( B1 +Bytes #buf ( lengthBytes(B2), A |Int #asWord ( B2 ) ) ) requires 0 <=Int A andBool A From b17021108b07e4d2729659b6a744a64ba4282898 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Wed, 24 Jul 2024 17:37:38 +0200 Subject: [PATCH 05/12] simplified mocks and more --- contracts/Escrow.sol | 6 +- test/kontrol/ActivateNextState.t.sol | 31 ++----- test/kontrol/EscrowLockUnlock.t.sol | 127 ++++++++++++++------------- test/kontrol/KontrolTest.sol | 6 ++ test/kontrol/lido-lemmas.k | 13 ++- 5 files changed, 91 insertions(+), 92 deletions(-) diff --git a/contracts/Escrow.sol b/contracts/Escrow.sol index a0d274b1..68417732 100644 --- a/contracts/Escrow.sol +++ b/contracts/Escrow.sol @@ -112,9 +112,9 @@ contract Escrow is IEscrow { // --- function lockStETH(uint256 amount) external returns (uint256 lockedStETHShares) { - lockedStETHShares = ST_ETH.getSharesByPooledEth(amount); - _accounting.accountStETHSharesLock(msg.sender, SharesValues.from(lockedStETHShares)); - ST_ETH.transferSharesFrom(msg.sender, address(this), lockedStETHShares); + // lockedStETHShares = ST_ETH.getSharesByPooledEth(amount); + // _accounting.accountStETHSharesLock(msg.sender, SharesValues.from(lockedStETHShares)); + // ST_ETH.transferSharesFrom(msg.sender, address(this), lockedStETHShares); _activateNextGovernanceState(); } diff --git a/test/kontrol/ActivateNextState.t.sol b/test/kontrol/ActivateNextState.t.sol index a67572d2..5bbdcbcd 100644 --- a/test/kontrol/ActivateNextState.t.sol +++ b/test/kontrol/ActivateNextState.t.sol @@ -7,11 +7,8 @@ import "test/kontrol/DualGovernanceSetUp.sol"; contract ActivateNextStateMock is StorageSetup { function activateNextState() external { DualGovernance dualGovernance = DualGovernance(address(this)); - IConfiguration config = dualGovernance.CONFIG(); Escrow signallingEscrow = Escrow(payable(dualGovernance.getVetoSignallingEscrow())); Escrow rageQuitEscrow = Escrow(payable(dualGovernance.getRageQuitEscrow())); - address sender = address(uint160(uint256(keccak256("sender")))); - AccountingRecord memory pre = this.saveAccountingRecord(sender, signallingEscrow); this.dualGovernanceStorageInvariants(Mode.Assert, dualGovernance); this.escrowStorageInvariants(Mode.Assert, signallingEscrow); @@ -19,29 +16,13 @@ contract ActivateNextStateMock is StorageSetup { this.escrowStorageInvariants(Mode.Assert, rageQuitEscrow); this.rageQuitEscrowStorageInvariants(Mode.Assert, rageQuitEscrow); - State initialState = dualGovernance.getCurrentState(); - uint256 rageQuitSupport = signallingEscrow.getRageQuitSupport(); - (,, Timestamp vetoSignallingActivationTime,) = dualGovernance.getVetoSignallingState(); + address escrowMasterCopy = signallingEscrow.MASTER_COPY(); + IEscrow newSignallingEscrow = IEscrow(Clones.clone(escrowMasterCopy)); + IEscrow newRageQuitEscrow = IEscrow(Clones.clone(escrowMasterCopy)); - if ( - (initialState == State.VetoSignalling || initialState == State.VetoSignallingDeactivation) - && rageQuitSupport > config.SECOND_SEAL_RAGE_QUIT_SUPPORT() - && Timestamps.now() > config.DYNAMIC_TIMELOCK_MAX_DURATION().addTo(vetoSignallingActivationTime) - ) { - address escrowMasterCopy = signallingEscrow.MASTER_COPY(); - IEscrow newSignallingEscrow = IEscrow(Clones.clone(escrowMasterCopy)); - - this.dualGovernanceInitializeStorage(dualGovernance, newSignallingEscrow, signallingEscrow); - this.signallingEscrowInitializeStorage(newSignallingEscrow, dualGovernance); - this.rageQuitEscrowInitializeStorage(signallingEscrow, dualGovernance); - } else { - this.dualGovernanceInitializeStorage(dualGovernance, signallingEscrow, rageQuitEscrow); - this.signallingEscrowInitializeStorage(signallingEscrow, dualGovernance); - this.rageQuitEscrowInitializeStorage(rageQuitEscrow, dualGovernance); - } - - AccountingRecord memory post = this.saveAccountingRecord(sender, signallingEscrow); - this.establishEqualAccountingRecords(Mode.Assume, pre, post); + this.dualGovernanceInitializeStorage(dualGovernance, newSignallingEscrow, newRageQuitEscrow); + this.signallingEscrowInitializeStorage(newSignallingEscrow, dualGovernance); + this.rageQuitEscrowInitializeStorage(newRageQuitEscrow, dualGovernance); } } diff --git a/test/kontrol/EscrowLockUnlock.t.sol b/test/kontrol/EscrowLockUnlock.t.sol index 3acaad65..ea8e434f 100644 --- a/test/kontrol/EscrowLockUnlock.t.sol +++ b/test/kontrol/EscrowLockUnlock.t.sol @@ -39,61 +39,61 @@ contract EscrowLockUnlockTest is EscrowInvariants, DualGovernanceSetUp { // 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 - ); + // 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 - ); + // 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 - ); + // 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); + // vm.assume(0 < amount); + // vm.assume(amount <= stEth.balanceOf(sender)); + // vm.assume(amount <= senderAllowance); - AccountingRecord memory pre = this.saveAccountingRecord(sender, signallingEscrow); + // AccountingRecord memory pre = this.saveAccountingRecord(sender, signallingEscrow); - uint256 amountInShares = stEth.getSharesByPooledEth(amount); - _assumeNoOverflow(pre.userSharesLocked, amountInShares); - _assumeNoOverflow(pre.totalSharesLocked, amountInShares); + // 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); + // this.escrowInvariants(Mode.Assume, signallingEscrow); + // this.signallingEscrowInvariants(Mode.Assume, signallingEscrow); + // this.escrowUserInvariants(Mode.Assume, signallingEscrow, sender); - // ActivateNextStateMock mock = new ActivateNextStateMock(); - // kevm.mockFunction( - // address(dualGovernance), address(mock), abi.encodeWithSelector(mock.activateNextState.selector) - // ); + ActivateNextStateMock mock = new ActivateNextStateMock(); + kevm.mockFunction( + address(dualGovernance), address(mock), abi.encodeWithSelector(mock.activateNextState.selector) + ); vm.startPrank(sender); signallingEscrow.lockStETH(amount); @@ -103,23 +103,24 @@ contract EscrowLockUnlockTest is EscrowInvariants, DualGovernanceSetUp { this.signallingEscrowInvariants(Mode.Assert, signallingEscrow); this.escrowUserInvariants(Mode.Assert, signallingEscrow, sender); - AccountingRecord memory post = this.saveAccountingRecord(sender, signallingEscrow); - assert(post.escrowState == EscrowState.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()); + // assert(EscrowState(_getCurrentState(signallingEscrow)) == EscrowState.SignallingEscrow); - // 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); + // 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()); - 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); + // // 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 { diff --git a/test/kontrol/KontrolTest.sol b/test/kontrol/KontrolTest.sol index 778cf4c3..dd0ea586 100644 --- a/test/kontrol/KontrolTest.sol +++ b/test/kontrol/KontrolTest.sol @@ -11,6 +11,12 @@ contract KontrolTest is Test, KontrolCheats { // 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, Assert diff --git a/test/kontrol/lido-lemmas.k b/test/kontrol/lido-lemmas.k index bed22c7d..1be1a546 100644 --- a/test/kontrol/lido-lemmas.k +++ b/test/kontrol/lido-lemmas.k @@ -65,6 +65,11 @@ module LIDO-LEMMAS rule B /Int C A *Int C >Int B requires 0 (A +Int 1) *Int C >Int B requires 0 true + requires C +Int D ==Int 0 [simplification, preserves-definedness] + + // Further generalization of: maxUIntXXX &Int #asWord ( BA ) rule X &Int #asWord ( BA ) => #asWord ( #range(BA, lengthBytes(BA) -Int (log2Int(X +Int 1) /Int 8), log2Int(X +Int 1) /Int 8) ) requires #rangeUInt(256, X) @@ -308,7 +313,13 @@ module LIDO-LEMMAS // // #lookup // - rule M:Map [ K1 <- _ ] [ K2 <- V2 ] [ K1 <- V3 ] => M:Map [ K2 <- V2 ] [ K1 <- V3 ] [simplification] + rule M:Map [ K1 <- _ ] [ K1 <- V2 ] => M:Map [ K1 <- V2 ] [simplification] + rule M:Map [ K1 <- _ ] [ K2 <- V2 ] [ K1 <- V3 ] => M:Map [ K2 <- V2 ] [ K1 <- V3 ] [simplification] + rule M:Map [ K1 <- _ ] [ K2 <- V2 ] [ K3 <- V3 ] [ K1 <- V4 ] => M:Map [ K2 <- V2 ] [ K3 <- V3 ] [ K1 <- V4 ] [simplification] + rule M:Map [ K1 <- _ ] [ K2 <- V2 ] [ K3 <- V3 ] [ K4 <- V4 ] [ K1 <- V5 ] => M:Map [ K2 <- V2 ] [ K3 <- V3 ] [ K4 <- V4 ] [ K1 <- V5 ] [simplification] + rule M:Map [ K1 <- _ ] [ K2 <- V2 ] [ K3 <- V3 ] [ K4 <- V4 ] [ K5 <- V5 ] [ K1 <- V6 ] => M:Map [ K2 <- V2 ] [ K3 <- V3 ] [ K4 <- V4 ] [ K5 <- V5 ] [ K1 <- V6 ] [simplification] + rule M:Map [ K1 <- _ ] [ K2 <- V2 ] [ K3 <- V3 ] [ K4 <- V4 ] [ K5 <- V5 ] [ K6 <- V6 ] [ K1 <- V7 ] => M:Map [ K2 <- V2 ] [ K3 <- V3 ] [ K4 <- V4 ] [ K5 <- V5 ] [ K6 <- V6 ] [ K1 <- V7 ] [simplification] + rule M:Map [ K1 <- _ ] [ K2 <- V2 ] [ K3 <- V3 ] [ K4 <- V4 ] [ K5 <- V5 ] [ K6 <- V6 ] [ K7 <- V7 ] [ K1 <- V8 ] => M:Map [ K2 <- V2 ] [ K3 <- V3 ] [ K4 <- V4 ] [ K5 <- V5 ] [ K6 <- V6 ] [ K7 <- V7 ] [ K1 <- V8 ] [simplification] // // keccak assumptions: these assumptions are not sound in principle, but are From 12b447b7ba44a499826da1bfc3321c5b96529b8a Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Wed, 24 Jul 2024 21:36:16 +0200 Subject: [PATCH 06/12] full test with full mock --- test/kontrol/ActivateNextState.t.sol | 22 +++-- test/kontrol/DualGovernanceSetUp.sol | 1 - test/kontrol/EscrowLockUnlock.t.sol | 134 +++++++++++++-------------- 3 files changed, 81 insertions(+), 76 deletions(-) diff --git a/test/kontrol/ActivateNextState.t.sol b/test/kontrol/ActivateNextState.t.sol index 5bbdcbcd..b153b923 100644 --- a/test/kontrol/ActivateNextState.t.sol +++ b/test/kontrol/ActivateNextState.t.sol @@ -5,24 +5,30 @@ import {State} from "contracts/libraries/DualGovernanceState.sol"; import "test/kontrol/DualGovernanceSetUp.sol"; contract ActivateNextStateMock is StorageSetup { + StorageSetup public immutable STORAGE_SETUP; + + constructor(address storageSetup) { + STORAGE_SETUP = StorageSetup(storageSetup); + } + function activateNextState() external { DualGovernance dualGovernance = DualGovernance(address(this)); Escrow signallingEscrow = Escrow(payable(dualGovernance.getVetoSignallingEscrow())); Escrow rageQuitEscrow = Escrow(payable(dualGovernance.getRageQuitEscrow())); - this.dualGovernanceStorageInvariants(Mode.Assert, dualGovernance); - this.escrowStorageInvariants(Mode.Assert, signallingEscrow); - this.signallingEscrowStorageInvariants(Mode.Assert, signallingEscrow); - this.escrowStorageInvariants(Mode.Assert, rageQuitEscrow); - this.rageQuitEscrowStorageInvariants(Mode.Assert, rageQuitEscrow); + 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); address escrowMasterCopy = signallingEscrow.MASTER_COPY(); IEscrow newSignallingEscrow = IEscrow(Clones.clone(escrowMasterCopy)); IEscrow newRageQuitEscrow = IEscrow(Clones.clone(escrowMasterCopy)); - this.dualGovernanceInitializeStorage(dualGovernance, newSignallingEscrow, newRageQuitEscrow); - this.signallingEscrowInitializeStorage(newSignallingEscrow, dualGovernance); - this.rageQuitEscrowInitializeStorage(newRageQuitEscrow, dualGovernance); + STORAGE_SETUP.dualGovernanceInitializeStorage(dualGovernance, newSignallingEscrow, newRageQuitEscrow); + STORAGE_SETUP.signallingEscrowInitializeStorage(newSignallingEscrow, dualGovernance); + STORAGE_SETUP.rageQuitEscrowInitializeStorage(newRageQuitEscrow, dualGovernance); } } diff --git a/test/kontrol/DualGovernanceSetUp.sol b/test/kontrol/DualGovernanceSetUp.sol index f3de8939..268cf541 100644 --- a/test/kontrol/DualGovernanceSetUp.sol +++ b/test/kontrol/DualGovernanceSetUp.sol @@ -42,7 +42,6 @@ contract DualGovernanceSetUp is StorageSetup { Escrow 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)))); diff --git a/test/kontrol/EscrowLockUnlock.t.sol b/test/kontrol/EscrowLockUnlock.t.sol index ea8e434f..ca8c7cdd 100644 --- a/test/kontrol/EscrowLockUnlock.t.sol +++ b/test/kontrol/EscrowLockUnlock.t.sol @@ -39,58 +39,58 @@ contract EscrowLockUnlockTest is EscrowInvariants, DualGovernanceSetUp { // 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); - - ActivateNextStateMock mock = new ActivateNextStateMock(); + 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); + + ActivateNextStateMock mock = new ActivateNextStateMock(address(this)); kevm.mockFunction( address(dualGovernance), address(mock), abi.encodeWithSelector(mock.activateNextState.selector) ); @@ -103,24 +103,24 @@ contract EscrowLockUnlockTest is EscrowInvariants, DualGovernanceSetUp { this.signallingEscrowInvariants(Mode.Assert, signallingEscrow); this.escrowUserInvariants(Mode.Assert, signallingEscrow, sender); - // assert(EscrowState(_getCurrentState(signallingEscrow)) == EscrowState.SignallingEscrow); + assert(EscrowState(_getCurrentState(signallingEscrow)) == EscrowState.SignallingEscrow); - // 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()); + 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); + // 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); + 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 { From 97feb0d81a6d6eba2bc87dc4d68a2070f0b6e0ad Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Wed, 24 Jul 2024 22:29:59 +0200 Subject: [PATCH 07/12] full test --- contracts/Escrow.sol | 6 +++--- test/kontrol/EscrowLockUnlock.t.sol | 2 -- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/contracts/Escrow.sol b/contracts/Escrow.sol index 68417732..a0d274b1 100644 --- a/contracts/Escrow.sol +++ b/contracts/Escrow.sol @@ -112,9 +112,9 @@ contract Escrow is IEscrow { // --- function lockStETH(uint256 amount) external returns (uint256 lockedStETHShares) { - // lockedStETHShares = ST_ETH.getSharesByPooledEth(amount); - // _accounting.accountStETHSharesLock(msg.sender, SharesValues.from(lockedStETHShares)); - // ST_ETH.transferSharesFrom(msg.sender, address(this), lockedStETHShares); + lockedStETHShares = ST_ETH.getSharesByPooledEth(amount); + _accounting.accountStETHSharesLock(msg.sender, SharesValues.from(lockedStETHShares)); + ST_ETH.transferSharesFrom(msg.sender, address(this), lockedStETHShares); _activateNextGovernanceState(); } diff --git a/test/kontrol/EscrowLockUnlock.t.sol b/test/kontrol/EscrowLockUnlock.t.sol index ca8c7cdd..f714a2c2 100644 --- a/test/kontrol/EscrowLockUnlock.t.sol +++ b/test/kontrol/EscrowLockUnlock.t.sol @@ -103,8 +103,6 @@ contract EscrowLockUnlockTest is EscrowInvariants, DualGovernanceSetUp { this.signallingEscrowInvariants(Mode.Assert, signallingEscrow); this.escrowUserInvariants(Mode.Assert, signallingEscrow, sender); - assert(EscrowState(_getCurrentState(signallingEscrow)) == EscrowState.SignallingEscrow); - AccountingRecord memory post = this.saveAccountingRecord(sender, signallingEscrow); assert(post.userShares == pre.userShares - amountInShares); assert(post.escrowShares == pre.escrowShares + amountInShares); From b19c812cb533ab707a86bc345c45a618774df357 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Fri, 26 Jul 2024 11:06:45 +0200 Subject: [PATCH 08/12] unlock test, further simplifications, streamlining of fresh variables --- test/kontrol/EscrowLockUnlock.t.sol | 44 +++++++++++++++++++++++++++-- test/kontrol/StorageSetup.sol | 10 +++++-- test/kontrol/lido-lemmas.k | 18 ++++++++++-- 3 files changed, 65 insertions(+), 7 deletions(-) diff --git a/test/kontrol/EscrowLockUnlock.t.sol b/test/kontrol/EscrowLockUnlock.t.sol index f714a2c2..199f45db 100644 --- a/test/kontrol/EscrowLockUnlock.t.sol +++ b/test/kontrol/EscrowLockUnlock.t.sol @@ -124,8 +124,42 @@ contract EscrowLockUnlockTest is EscrowInvariants, DualGovernanceSetUp { function testUnlockStEth() public { // 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(signallingEscrow, sender) < timeUpperBound); + 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 + ); AccountingRecord memory pre = this.saveAccountingRecord(sender, signallingEscrow); vm.assume(pre.userSharesLocked <= pre.totalSharesLocked); @@ -135,6 +169,11 @@ contract EscrowLockUnlockTest is EscrowInvariants, DualGovernanceSetUp { this.signallingEscrowInvariants(Mode.Assume, signallingEscrow); this.escrowUserInvariants(Mode.Assume, signallingEscrow, sender); + ActivateNextStateMock mock = new ActivateNextStateMock(address(this)); + kevm.mockFunction( + address(dualGovernance), address(mock), abi.encodeWithSelector(mock.activateNextState.selector) + ); + vm.startPrank(sender); signallingEscrow.unlockStETH(); vm.stopPrank(); @@ -144,7 +183,6 @@ contract EscrowLockUnlockTest is EscrowInvariants, DualGovernanceSetUp { this.escrowUserInvariants(Mode.Assert, signallingEscrow, sender); AccountingRecord memory post = this.saveAccountingRecord(sender, signallingEscrow); - assert(post.escrowState == EscrowState.SignallingEscrow); assert(post.userShares == pre.userShares + pre.userSharesLocked); assert(post.userSharesLocked == 0); assert(post.totalSharesLocked == pre.totalSharesLocked - pre.userSharesLocked); diff --git a/test/kontrol/StorageSetup.sol b/test/kontrol/StorageSetup.sol index 96351e14..9a78b2da 100644 --- a/test/kontrol/StorageSetup.sol +++ b/test/kontrol/StorageSetup.sol @@ -277,12 +277,16 @@ contract StorageSetup is KontrolTest { _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)); _storeUInt256(address(_escrow), 5, batchesQueueStatus); + } else { + _storeUInt256(address(_escrow), 5, 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)); uint32 rageQuitWithdrawalsTimelock = uint32(kevm.freshUInt(4)); uint40 rageQuitTimelockStartedAt = uint40(kevm.freshUInt(5)); @@ -297,6 +301,8 @@ contract StorageSetup is KontrolTest { slot9 := mload(add(slot9Abi, 0x20)) } _storeBytes32(address(_escrow), 9, slot9); + } else { + _storeUInt256(address(_escrow), 9, 0); } } diff --git a/test/kontrol/lido-lemmas.k b/test/kontrol/lido-lemmas.k index 1be1a546..42872168 100644 --- a/test/kontrol/lido-lemmas.k +++ b/test/kontrol/lido-lemmas.k @@ -37,6 +37,9 @@ module LIDO-LEMMAS requires #rangeUInt(256, A) andBool #rangeUInt(256, B) [concrete(B), simplification, comm, preserves-definedness] + // ==Int + rule [int-eq-refl]: X ==Int X => true [simplification] + // *Int rule A *Int B ==Int 0 => A ==Int 0 orBool B ==Int 0 [simplification] @@ -90,9 +93,20 @@ module LIDO-LEMMAS // >>Int rule [shift-to-div]: X >>Int N => X /Int (2 ^Int N) [simplification(60), concrete(N)] + // Boolean equality + rule B ==K false => notBool B [simplification(30), comm] + rule B ==K true => B [simplification(30), comm] + // bool2Word - rule [bool2Word-lt-true]: bool2Word(_:Bool) true requires 1 notBool B [simplification] + rule bool2Word(X) ==Int 0 => notBool X [simplification(30), comm] + rule bool2Word(X) =/=Int 0 => X [simplification(30), comm] + rule bool2Word(X) ==Int 1 => X [simplification(30), comm] + rule bool2Word(X) =/=Int 1 => notBool X [simplification(30), comm] + + rule [bool2Word-lt-true]: bool2Word(_:Bool) true requires 1 notBool B [simplification(30)] + rule [bool2Word-gt-zero]: 0 B [simplification(30)] + rule [bool2Word-gt-false]: X:Int false requires 1 Date: Fri, 26 Jul 2024 11:19:38 +0200 Subject: [PATCH 09/12] further merging --- test/kontrol/EscrowOperations.t.sol | 52 +++++++++++++++++++---------- 1 file changed, 34 insertions(+), 18 deletions(-) diff --git a/test/kontrol/EscrowOperations.t.sol b/test/kontrol/EscrowOperations.t.sol index c38f167b..c8442014 100644 --- a/test/kontrol/EscrowOperations.t.sol +++ b/test/kontrol/EscrowOperations.t.sol @@ -3,19 +3,33 @@ 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"; +import "test/kontrol/EscrowLockUnlock.t.sol"; + +contract EscrowOperationsTest is EscrowLockUnlockTest { + function _tryLockStETH(uint256 amount) internal returns (bool) { + try signallingEscrow.lockStETH(amount) { + return true; + } catch { + return false; + } + } + + function _tryUnlockStETH() internal returns (bool) { + try signallingEscrow.unlockStETH() { + return true; + } catch { + return false; + } + } -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(_getLastAssetsLockTimestamp(escrow, sender) < timeUpperBound); + vm.assume(_getLastAssetsLockTimestamp(signallingEscrow, sender) < timeUpperBound); AccountingRecord memory pre = this.saveAccountingRecord(sender, escrow); vm.assume(pre.escrowState == EscrowState.SignallingEscrow); @@ -25,8 +39,8 @@ contract EscrowOperationsTest is EscrowAccountingTest { if (Timestamps.now() < lockPeriod) { vm.prank(sender); - vm.expectRevert("Lock period not expired."); - escrow.unlockStETH(); + vm.expectRevert(abi.encodeWithSelector(AssetsAccounting.AssetsUnlockDelayNotPassed.selector, lockPeriod)); + signallingEscrow.unlockStETH(); } } @@ -34,8 +48,6 @@ contract EscrowOperationsTest is EscrowAccountingTest { * 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); @@ -55,16 +67,20 @@ contract EscrowOperationsTest is EscrowAccountingTest { this.escrowUserInvariants(Mode.Assume, escrow, sender); if (pre.escrowState == EscrowState.RageQuitEscrow) { - vm.prank(sender); - vm.expectRevert("Cannot lock in current state."); - escrow.lockStETH(amount); - - vm.prank(sender); - vm.expectRevert("Cannot unlock in current state."); - escrow.unlockStETH(); + 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); + signallingEscrow.lockStETH(amount); AccountingRecord memory afterLock = this.saveAccountingRecord(sender, escrow); vm.assume(afterLock.userShares < ethUpperBound); @@ -73,7 +89,7 @@ contract EscrowOperationsTest is EscrowAccountingTest { vm.assume(Timestamps.now() >= addTo(config.SIGNALLING_ESCROW_MIN_LOCK_TIME(), afterLock.userLastLockedTime)); vm.prank(sender); - escrow.unlockStETH(); + signallingEscrow.unlockStETH(); this.escrowInvariants(Mode.Assert, escrow); this.signallingEscrowInvariants(Mode.Assert, escrow); From acaf186e6aa26eb2d29dbaf5057c501f1d2b034d Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Fri, 26 Jul 2024 11:22:04 +0200 Subject: [PATCH 10/12] corrections --- test/kontrol/EscrowOperations.t.sol | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/test/kontrol/EscrowOperations.t.sol b/test/kontrol/EscrowOperations.t.sol index c8442014..566e4bcc 100644 --- a/test/kontrol/EscrowOperations.t.sol +++ b/test/kontrol/EscrowOperations.t.sol @@ -31,7 +31,7 @@ contract EscrowOperationsTest is EscrowLockUnlockTest { vm.assume(stEth.sharesOf(sender) < ethUpperBound); vm.assume(_getLastAssetsLockTimestamp(signallingEscrow, sender) < timeUpperBound); - AccountingRecord memory pre = this.saveAccountingRecord(sender, escrow); + AccountingRecord memory pre = this.saveAccountingRecord(sender, signallingEscrow); vm.assume(pre.escrowState == EscrowState.SignallingEscrow); vm.assume(pre.userSharesLocked <= pre.totalSharesLocked); @@ -53,7 +53,7 @@ contract EscrowOperationsTest is EscrowLockUnlockTest { vm.assume(stEth.sharesOf(sender) < ethUpperBound); vm.assume(stEth.balanceOf(sender) < ethUpperBound); - AccountingRecord memory pre = this.saveAccountingRecord(sender, escrow); + AccountingRecord memory pre = this.saveAccountingRecord(sender, signallingEscrow); vm.assume(0 < amount); vm.assume(amount <= pre.userBalance); vm.assume(amount <= pre.allowance); @@ -62,9 +62,9 @@ contract EscrowOperationsTest is EscrowLockUnlockTest { _assumeNoOverflow(pre.userSharesLocked, amountInShares); _assumeNoOverflow(pre.totalSharesLocked, amountInShares); - this.escrowInvariants(Mode.Assume, escrow); - this.signallingEscrowInvariants(Mode.Assume, escrow); - this.escrowUserInvariants(Mode.Assume, escrow, sender); + this.escrowInvariants(Mode.Assume, signallingEscrow); + this.signallingEscrowInvariants(Mode.Assume, signallingEscrow); + this.escrowUserInvariants(Mode.Assume, signallingEscrow, sender); if (pre.escrowState == EscrowState.RageQuitEscrow) { vm.startPrank(sender); @@ -82,7 +82,7 @@ contract EscrowOperationsTest is EscrowLockUnlockTest { vm.prank(sender); signallingEscrow.lockStETH(amount); - AccountingRecord memory afterLock = this.saveAccountingRecord(sender, escrow); + AccountingRecord memory afterLock = this.saveAccountingRecord(sender, signallingEscrow); vm.assume(afterLock.userShares < ethUpperBound); //vm.assume(afterLock.userLastLockedTime < timeUpperBound); vm.assume(afterLock.userSharesLocked <= afterLock.totalSharesLocked); @@ -91,11 +91,11 @@ contract EscrowOperationsTest is EscrowLockUnlockTest { vm.prank(sender); signallingEscrow.unlockStETH(); - this.escrowInvariants(Mode.Assert, escrow); - this.signallingEscrowInvariants(Mode.Assert, escrow); - this.escrowUserInvariants(Mode.Assert, escrow, sender); + this.escrowInvariants(Mode.Assert, signallingEscrow); + this.signallingEscrowInvariants(Mode.Assert, signallingEscrow); + this.escrowUserInvariants(Mode.Assert, signallingEscrow, sender); - AccountingRecord memory post = this.saveAccountingRecord(sender, escrow); + AccountingRecord memory post = this.saveAccountingRecord(sender, signallingEscrow); assert(post.escrowState == EscrowState.SignallingEscrow); assert(post.userShares == pre.userShares); assert(post.escrowShares == pre.escrowShares); From cfdb6a18e55fc5552c60a900ec846c5955f44c5e Mon Sep 17 00:00:00 2001 From: qian-hu <88806138+qian-hu@users.noreply.github.com> Date: Tue, 23 Jul 2024 19:19:00 -0400 Subject: [PATCH 11/12] Revert EscrowOperationsTest base to EscrowAccountingTest --- test/kontrol/EscrowAccounting.t.sol | 5 +++- test/kontrol/EscrowOperations.t.sol | 40 ++++++++++++++++------------- 2 files changed, 26 insertions(+), 19 deletions(-) diff --git a/test/kontrol/EscrowAccounting.t.sol b/test/kontrol/EscrowAccounting.t.sol index ab6762ab..5582054f 100644 --- a/test/kontrol/EscrowAccounting.t.sol +++ b/test/kontrol/EscrowAccounting.t.sol @@ -1,5 +1,7 @@ pragma solidity 0.8.23; +import "@openzeppelin/contracts/proxy/Clones.sol"; + import "contracts/Configuration.sol"; import "contracts/DualGovernance.sol"; import "contracts/EmergencyProtectedTimelock.sol"; @@ -35,7 +37,8 @@ contract EscrowAccountingTest is EscrowInvariants { config = new Configuration(adminExecutor, emergencyGovernance, new address[](0)); - escrow = new Escrow(address(stEth), address(wstEth), address(withdrawalQueue), address(config)); + Escrow escrowMasterCopy = new Escrow(address(stEth), address(wstEth), address(withdrawalQueue), address(config)); + escrow = Escrow(payable(Clones.clone(address(escrowMasterCopy)))); escrow.initialize(dualGovernanceAddress); // ?STORAGE diff --git a/test/kontrol/EscrowOperations.t.sol b/test/kontrol/EscrowOperations.t.sol index 566e4bcc..ff7e527c 100644 --- a/test/kontrol/EscrowOperations.t.sol +++ b/test/kontrol/EscrowOperations.t.sol @@ -3,11 +3,11 @@ pragma solidity 0.8.23; import {Duration, Durations} from "contracts/types/Duration.sol"; import {Timestamp, Timestamps} from "contracts/types/Timestamp.sol"; -import "test/kontrol/EscrowLockUnlock.t.sol"; +import "test/kontrol/EscrowAccounting.t.sol"; -contract EscrowOperationsTest is EscrowLockUnlockTest { +contract EscrowOperationsTest is EscrowAccountingTest { function _tryLockStETH(uint256 amount) internal returns (bool) { - try signallingEscrow.lockStETH(amount) { + try escrow.lockStETH(amount) { return true; } catch { return false; @@ -15,7 +15,7 @@ contract EscrowOperationsTest is EscrowLockUnlockTest { } function _tryUnlockStETH() internal returns (bool) { - try signallingEscrow.unlockStETH() { + try escrow.unlockStETH() { return true; } catch { return false; @@ -26,12 +26,14 @@ contract EscrowOperationsTest is EscrowLockUnlockTest { * 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(signallingEscrow, sender) < timeUpperBound); + vm.assume(_getLastAssetsLockTimestamp(escrow, sender) < timeUpperBound); - AccountingRecord memory pre = this.saveAccountingRecord(sender, signallingEscrow); + AccountingRecord memory pre = _saveAccountingRecord(sender, escrow); vm.assume(pre.escrowState == EscrowState.SignallingEscrow); vm.assume(pre.userSharesLocked <= pre.totalSharesLocked); @@ -40,7 +42,7 @@ contract EscrowOperationsTest is EscrowLockUnlockTest { if (Timestamps.now() < lockPeriod) { vm.prank(sender); vm.expectRevert(abi.encodeWithSelector(AssetsAccounting.AssetsUnlockDelayNotPassed.selector, lockPeriod)); - signallingEscrow.unlockStETH(); + escrow.unlockStETH(); } } @@ -48,12 +50,14 @@ contract EscrowOperationsTest is EscrowLockUnlockTest { * 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, signallingEscrow); + AccountingRecord memory pre = _saveAccountingRecord(sender, escrow); vm.assume(0 < amount); vm.assume(amount <= pre.userBalance); vm.assume(amount <= pre.allowance); @@ -62,9 +66,9 @@ contract EscrowOperationsTest is EscrowLockUnlockTest { _assumeNoOverflow(pre.userSharesLocked, amountInShares); _assumeNoOverflow(pre.totalSharesLocked, amountInShares); - this.escrowInvariants(Mode.Assume, signallingEscrow); - this.signallingEscrowInvariants(Mode.Assume, signallingEscrow); - this.escrowUserInvariants(Mode.Assume, signallingEscrow, sender); + _escrowInvariants(Mode.Assume, escrow); + _signallingEscrowInvariants(Mode.Assume, escrow); + _escrowUserInvariants(Mode.Assume, escrow, sender); if (pre.escrowState == EscrowState.RageQuitEscrow) { vm.startPrank(sender); @@ -80,22 +84,22 @@ contract EscrowOperationsTest is EscrowLockUnlockTest { vm.stopPrank; } else { vm.prank(sender); - signallingEscrow.lockStETH(amount); + escrow.lockStETH(amount); - AccountingRecord memory afterLock = this.saveAccountingRecord(sender, signallingEscrow); + AccountingRecord memory afterLock = _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); - signallingEscrow.unlockStETH(); + escrow.unlockStETH(); - this.escrowInvariants(Mode.Assert, signallingEscrow); - this.signallingEscrowInvariants(Mode.Assert, signallingEscrow); - this.escrowUserInvariants(Mode.Assert, signallingEscrow, sender); + _escrowInvariants(Mode.Assert, escrow); + _signallingEscrowInvariants(Mode.Assert, escrow); + _escrowUserInvariants(Mode.Assert, escrow, sender); - AccountingRecord memory post = this.saveAccountingRecord(sender, signallingEscrow); + AccountingRecord memory post = _saveAccountingRecord(sender, escrow); assert(post.escrowState == EscrowState.SignallingEscrow); assert(post.userShares == pre.userShares); assert(post.escrowShares == pre.escrowShares); From 83e85fa0d432b2a842f0bf1f26c4b2290de291eb Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Fri, 26 Jul 2024 11:24:22 +0200 Subject: [PATCH 12/12] further corrections --- test/kontrol/EscrowOperations.t.sol | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/test/kontrol/EscrowOperations.t.sol b/test/kontrol/EscrowOperations.t.sol index ff7e527c..406791d8 100644 --- a/test/kontrol/EscrowOperations.t.sol +++ b/test/kontrol/EscrowOperations.t.sol @@ -33,7 +33,7 @@ contract EscrowOperationsTest is EscrowAccountingTest { vm.assume(stEth.sharesOf(sender) < ethUpperBound); vm.assume(_getLastAssetsLockTimestamp(escrow, sender) < timeUpperBound); - AccountingRecord memory pre = _saveAccountingRecord(sender, escrow); + AccountingRecord memory pre = this.saveAccountingRecord(sender, escrow); vm.assume(pre.escrowState == EscrowState.SignallingEscrow); vm.assume(pre.userSharesLocked <= pre.totalSharesLocked); @@ -57,7 +57,7 @@ contract EscrowOperationsTest is EscrowAccountingTest { vm.assume(stEth.sharesOf(sender) < ethUpperBound); vm.assume(stEth.balanceOf(sender) < ethUpperBound); - AccountingRecord memory pre = _saveAccountingRecord(sender, escrow); + AccountingRecord memory pre = this.saveAccountingRecord(sender, escrow); vm.assume(0 < amount); vm.assume(amount <= pre.userBalance); vm.assume(amount <= pre.allowance); @@ -66,9 +66,9 @@ contract EscrowOperationsTest is EscrowAccountingTest { _assumeNoOverflow(pre.userSharesLocked, amountInShares); _assumeNoOverflow(pre.totalSharesLocked, amountInShares); - _escrowInvariants(Mode.Assume, escrow); - _signallingEscrowInvariants(Mode.Assume, escrow); - _escrowUserInvariants(Mode.Assume, escrow, sender); + this.escrowInvariants(Mode.Assume, escrow); + this.signallingEscrowInvariants(Mode.Assume, escrow); + this.escrowUserInvariants(Mode.Assume, escrow, sender); if (pre.escrowState == EscrowState.RageQuitEscrow) { vm.startPrank(sender); @@ -86,7 +86,7 @@ contract EscrowOperationsTest is EscrowAccountingTest { vm.prank(sender); escrow.lockStETH(amount); - AccountingRecord memory afterLock = _saveAccountingRecord(sender, escrow); + AccountingRecord memory afterLock = this.saveAccountingRecord(sender, escrow); vm.assume(afterLock.userShares < ethUpperBound); //vm.assume(afterLock.userLastLockedTime < timeUpperBound); vm.assume(afterLock.userSharesLocked <= afterLock.totalSharesLocked); @@ -95,11 +95,11 @@ contract EscrowOperationsTest is EscrowAccountingTest { vm.prank(sender); escrow.unlockStETH(); - _escrowInvariants(Mode.Assert, escrow); - _signallingEscrowInvariants(Mode.Assert, escrow); - _escrowUserInvariants(Mode.Assert, escrow, sender); + this.escrowInvariants(Mode.Assert, escrow); + this.signallingEscrowInvariants(Mode.Assert, escrow); + this.escrowUserInvariants(Mode.Assert, escrow, sender); - AccountingRecord memory post = _saveAccountingRecord(sender, escrow); + AccountingRecord memory post = this.saveAccountingRecord(sender, escrow); assert(post.escrowState == EscrowState.SignallingEscrow); assert(post.userShares == pre.userShares); assert(post.escrowShares == pre.escrowShares); @@ -122,7 +122,7 @@ contract EscrowOperationsTest is EscrowAccountingTest { vm.assume(stEth.sharesOf(sender) < ethUpperBound); vm.assume(stEth.balanceOf(sender) < ethUpperBound); - AccountingRecord memory pre = _saveAccountingRecord(sender, escrow); + AccountingRecord memory pre = this.saveAccountingRecord(sender, escrow); vm.assume(pre.escrowState == EscrowState.RageQuitEscrow); vm.assume(pre.userSharesLocked > 0); vm.assume(pre.userSharesLocked <= pre.totalSharesLocked); @@ -155,7 +155,7 @@ contract EscrowOperationsTest is EscrowAccountingTest { this.escrowInvariants(Mode.Assert); this.escrowUserInvariants(Mode.Assert, sender); - AccountingRecord memory post = _saveAccountingRecord(sender, escrow); + AccountingRecord memory post = this.saveAccountingRecord(sender, escrow); assert(post.userSharesLocked == 0); } }