diff --git a/test/kontrol/ActivateNextState.t.sol b/test/kontrol/ActivateNextState.t.sol index 36ad1b66..b153b923 100644 --- a/test/kontrol/ActivateNextState.t.sol +++ b/test/kontrol/ActivateNextState.t.sol @@ -5,43 +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)); - 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 = _saveAccountingRecord(sender, signallingEscrow); - - _dualGovernanceStorageInvariants(Mode.Assert, dualGovernance); - _escrowStorageInvariants(Mode.Assert, signallingEscrow); - _signallingEscrowStorageInvariants(Mode.Assert, signallingEscrow); - _escrowStorageInvariants(Mode.Assert, rageQuitEscrow); - _rageQuitEscrowStorageInvariants(Mode.Assert, rageQuitEscrow); - - State initialState = dualGovernance.getCurrentState(); - uint256 rageQuitSupport = signallingEscrow.getRageQuitSupport(); - (,, Timestamp vetoSignallingActivationTime,) = dualGovernance.getVetoSignallingState(); - 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)); + 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); - _dualGovernanceInitializeStorage(dualGovernance, newSignallingEscrow, signallingEscrow); - _signallingEscrowInitializeStorage(newSignallingEscrow, dualGovernance); - _rageQuitEscrowInitializeStorage(signallingEscrow, dualGovernance); - } else { - _dualGovernanceInitializeStorage(dualGovernance, signallingEscrow, rageQuitEscrow); - _signallingEscrowInitializeStorage(signallingEscrow, dualGovernance); - _rageQuitEscrowInitializeStorage(rageQuitEscrow, dualGovernance); - } + address escrowMasterCopy = signallingEscrow.MASTER_COPY(); + IEscrow newSignallingEscrow = IEscrow(Clones.clone(escrowMasterCopy)); + IEscrow newRageQuitEscrow = IEscrow(Clones.clone(escrowMasterCopy)); - AccountingRecord memory post = _saveAccountingRecord(sender, signallingEscrow); - _establishEqualAccountingRecords(Mode.Assume, pre, post); + STORAGE_SETUP.dualGovernanceInitializeStorage(dualGovernance, newSignallingEscrow, newRageQuitEscrow); + STORAGE_SETUP.signallingEscrowInitializeStorage(newSignallingEscrow, dualGovernance); + STORAGE_SETUP.rageQuitEscrowInitializeStorage(newRageQuitEscrow, dualGovernance); } } @@ -51,7 +38,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 +51,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 b289ecae..5582054f 100644 --- a/test/kontrol/EscrowAccounting.t.sol +++ b/test/kontrol/EscrowAccounting.t.sol @@ -45,7 +45,7 @@ contract EscrowAccountingTest is EscrowInvariants { // ?WORD: totalPooledEther // ?WORD0: totalShares // ?WORD1: shares[escrow] - _stEthStorageSetup(stEth, escrow); + this.stEthStorageSetup(stEth, escrow); } function _setUpGenericState() public { @@ -64,7 +64,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 { @@ -82,9 +82,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 { @@ -94,10 +94,10 @@ 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); + this.escrowInvariants(Mode.Assume, escrow); + this.escrowUserInvariants(Mode.Assume, escrow, sender); // Only request one withdrawal for simplicity uint256[] memory stEthAmounts = new uint256[](1); @@ -107,10 +107,10 @@ 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 = _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()); @@ -123,11 +123,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 { @@ -139,8 +139,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; @@ -149,7 +149,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 f23dc367..199f45db 100644 --- a/test/kontrol/EscrowLockUnlock.t.sol +++ b/test/kontrol/EscrowLockUnlock.t.sol @@ -38,24 +38,59 @@ 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 = _saveAccountingRecord(sender, signallingEscrow); + 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 <= 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); _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(); + ActivateNextStateMock mock = new ActivateNextStateMock(address(this)); kevm.mockFunction( address(dualGovernance), address(mock), abi.encodeWithSelector(mock.activateNextState.selector) ); @@ -64,12 +99,11 @@ 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 = _saveAccountingRecord(sender, signallingEscrow); - assert(post.escrowState == 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); @@ -90,27 +124,65 @@ 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); - AccountingRecord memory pre = _saveAccountingRecord(sender, signallingEscrow); + 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); 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); + + ActivateNextStateMock mock = new ActivateNextStateMock(address(this)); + kevm.mockFunction( + address(dualGovernance), address(mock), abi.encodeWithSelector(mock.activateNextState.selector) + ); 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 = _saveAccountingRecord(sender, signallingEscrow); - assert(post.escrowState == EscrowState.SignallingEscrow); + AccountingRecord memory post = this.saveAccountingRecord(sender, signallingEscrow); assert(post.userShares == pre.userShares + pre.userSharesLocked); assert(post.userSharesLocked == 0); assert(post.totalSharesLocked == pre.totalSharesLocked - pre.userSharesLocked); diff --git a/test/kontrol/EscrowOperations.t.sol b/test/kontrol/EscrowOperations.t.sol index c9dd24dc..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); @@ -130,8 +130,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()); @@ -152,10 +152,10 @@ 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); + AccountingRecord memory post = this.saveAccountingRecord(sender, escrow); assert(post.userSharesLocked == 0); } } 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/StorageSetup.sol b/test/kontrol/StorageSetup.sol index 1ba38e45..6c765154 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)); @@ -109,7 +109,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); @@ -124,7 +124,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); @@ -138,14 +138,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) { @@ -212,13 +212,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); @@ -231,15 +231,15 @@ 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)); } - 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); @@ -253,7 +253,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 { @@ -291,13 +291,17 @@ 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)); vm.assume(batchesQueueStatus < 3); _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)); vm.assume(rageQuitExtensionDelay <= block.timestamp); vm.assume(rageQuitExtensionDelay < timeUpperBound); @@ -318,10 +322,12 @@ contract StorageSetup is KontrolTest { slot9 := mload(add(slot9Abi, 0x20)) } _storeBytes32(address(_escrow), 9, slot9); + } else { + _storeUInt256(address(_escrow), 9, 0); } } - 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); @@ -333,7 +339,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); @@ -351,17 +357,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); @@ -373,19 +379,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..42872168 100644 --- a/test/kontrol/lido-lemmas.k +++ b/test/kontrol/lido-lemmas.k @@ -27,38 +27,18 @@ 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 [int-eq-refl]: X ==Int X => true [simplification] // *Int rule A *Int B ==Int 0 => A ==Int 0 orBool B ==Int 0 [simplification] @@ -71,9 +51,11 @@ 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] + 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 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) @@ -94,14 +81,32 @@ module LIDO-LEMMAS andBool (log2Int (X +Int 1)) /Int 8 <=Int lengthBytes(BA) andBool lengthBytes(BA) <=Int 32 [simplification, concrete(X), preserves-definedness] - // &Int distributivity - rule X &Int ( Y |Int Z ) => ( X &Int Y ) |Int ( X &Int Z ) [simplification, concrete(X)] - rule X &Int ( Y &Int Z ) => ( X &Int Y ) &Int ( X &Int Z ) [simplification, concrete(X)] + // #asWord + rule #asWord ( B1 +Bytes B2 ) => #asWord ( B2 ) + requires #asWord ( B1 ) ==Int 0 + [simplification, concrete(B1)] - // KEVM simplification - rule #asWord(WS) >>Int M => #asWord(#range(WS, 0, lengthBytes(WS) -Int (M /Int 8) )) - requires 0 <=Int M andBool M modInt 8 ==Int 0 - [simplification, preserves-definedness] + rule #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] + + // >>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(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 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] + 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 + // 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 +416,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 +430,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