Tests and Properties

[lucasmt]

_audits_lidofinance_dual-governance_fork/test/kontrol/report/DualGovernanceFormalVerificationReport.md

Lines 73 to 456 in dfe0fce

	The following are descriptions of each test contract and the tests that they contain, briefly summarizing the properties being verified by each test.
	## `EscrowAccounting.t.sol`
	This file consists of tests checking that the accounting performed by different functions of the `Escrow` contract are correct, including that funds are correctly transferred. It also checks certain consistency conditions of the `Escrow` contract are preserved by these functions, as specified in the `EscrowInvariants` file.
	### `testRageQuitSupport`
	Tests that the rage quit support returned by `Escrow.getRageQuitSupport` is calculated correctly based on the funds locked in the escrow.
	### `testEscrowInvariantsHoldInitially`
	Tests that the consistency conditions of the `Escrow` contract (see the `EscrowInvariants` file) hold when a signalling escrow is created.
	We check this by cloning a new escrow from the master copy (in the same way that the `DualGovernance` contract does when creating a new signalling escrow), then checking that the invarians hold in this initial state.
	### `testRequestNextWithdrawalsBatch`
	Tests that after calling `Escrow.requestNextWithdrawalsBatch` on the `RageQuitEscrow`, the number of stETH shares of the escrow is decreased by the amount corresponding to the withdrawal request (as long as there were enough shares to submit the request in the first place). Additionally, the `WithdrawalBatchesQueue` is closed if and only if the remaining stETH in the escrow is under the minimum withdrawable amount. For simplicity, the batch size of the request is only a single unstETH.
	### `testClaimNextWithdrawalsBatch`
	Tests that after calling `Escrow.claimNextWithdrawalsBatch` on the `RageQuitEscrow`, the amount of ETH received by the escrow from claiming the request is accounted in the `claimedETH` field of `AssetsAccounting`. For simplicity, the test only claims a single unstETH.
	## `EscrowLockUnlock.t.sol`
	This file consists of tests for the `Escrow.lockStETH` and `Escrow.unlockStETH` functions, checking their postconditions and that they preserve the invariants of the `SignallingEscrow` (as specified in the `EscrowInvariants` file).
	Because these two functions call `DualGovernance.activateNextState` twice each, these tests are particularly time-consuming and resource-intensive. Therefore, in practice we split them into 5 smaller tests each, where each of the smaller tests executes the base test starting from a different `DualGovernance` state.
	For the same reasons above, these tests also use the `kevm.forgetBranch` cheatcode, which causes Kontrol to forget certain complex formulas that are generated during the symbolic execution but are not actually necessary for verification, such as the precise calculation of the rage-quit support. If not discarded, these formulas can significantly increase the processing time of the logic solver used by Kontrol's backend.
	### `testLockStEth`
	Tests that after after a user calls `Escrow.lockStETH` in the `SignallingEscrow`, the user's and escrow's stETH balance change as expected, and the escrow's internal accounting is updated correctly. If `amount` is the value passed to `lockStETH` and `amountInShares` is the corresponding number of stETH shares for that amount, we check that
	* The user's stETH shares decrease by `amountInShares`.
	* The escrow's stETH shares increase by `amountInShares`.
	* The number of total locked shares in `AssetsAccounting` increases by `ammountInShares`.
	* The number of locked shares for that user in `AssetsAccounting` increases by `amountInShares`.
	* The user's `lastAssetsLockedTimestamp` in `AssetsAccounting` is set to the current timestamp.
	* The user's stETH balance decreases by at most `amount` and at least `amount - errorTerm`, where `errorTerm = StETH.getPooledEthByShares(1) + 1` is a small rounding error introduced by the conversion from and to shares.
	* The escrow's stETH balance increases by at most `amount` and at least `amount - errorTerm`.
	### `testUnlockStEth`
	Tests that after after a user calls `Escrow.unlockStETH` in the `SignallingEscrow`, the user's and escrow's stETH balance change as expected, and the escrow's internal accounting is updated correctly. If `shares` is the number of stETH shares that the user had previously locked in the escrow, and `amount` is the corresponding value in stETH, we check that
	* The user's stETH shares increase by `shares`.
	* The escrow's stETH shares decrease by `shares`.
	* The number of total locked shares in `AssetsAccounting` decreases by `shares`.
	* The number of locked shares for that user in `AssetsAccounting` is updated to 0.
	* The user's `lastAssetsLockedTimestamp` in `AssetsAccounting` remains the same.
	* The user's stETH balance increases by at least `amount` and at most `amount + 1`, due to rounding error introduced by the conversion from and to shares.
	* The escrow's stETH balance decreases by at least `amount` and at most `amount + 1`.
	## `EscrowOperations.t.sol`
	This file consists of tests checking various preconditions of operations from the `Escrow` contract, guaranteeing that the operations revert when these preconditions are violated.
	### `testCannotUnlockBeforeMinLockTime`
	Tests that `Escrow.unlockStETH` reverts if it's called before the min assets lock duration has passed since the last time the caller locked assets in the escrow.
	Since `unlockStETH` calls `DualGovernance.activateNextState`, the test needs to include an assumption that the `DualGovernance` will not transition into the `RageQuit` state under the current conditions. This transition would cause the `SignallingEscrow` to turn into a `RageQuitEscrow`, which is covered in the next test below.
	### `testCanotLockUnlockInRageQuitEscrowState`
	Tests that both `Escrow.lockStETH` and `Escrow.unlockStETH` revert if the escrow enters the `RageQuitEscrow` state.
	### `testCannotWithdrawBeforeEthClaimTimelockElapsed`
	Tests that when `Escrow.withdrawETH` is called on the `RageQuitEscrow` after the rage quit extension period has passed, then a) if the withdrawals delay period has not passed, the function reverts, or b) if it has, then it succeeds and withdraws all of the user's shares.
	## `ProposalOperations.t.sol`
	This file consists of tests checking preconditions for submitting and scheduling proposals based on the `DualGovernance` state, guaranteeing that an operation will revert if it is not allowed in the current state.
	### `testCannotProposeInInvalidState`
	Tests that `DualGovernance.submitProposal` reverts if the effective state is either `VetoSignallingDeactivation` or `VetoCooldown`.
	### `testCannotScheduleInInvalidStates`
	Tests that `DualGovernance.scheduleProposal` reverts if the effective state is either `VetoSignalling`, `VetoSignallingDeactivation` or `RageQuit`.
	### `testCannotScheduleSubmissionAfterLastVetoSignalling`
	Tests that, when the effective state is `VetoCooldown`, `DualGovernance.scheduleProposal` reverts if the proposal being scheduled was submitted after the last time the `VetoSignalling` state was entered.
	### `testOnlyProposalsCancellerCanCancelProposals`
	Tests that `DualGovernance.cancelAllPendingProposals` reverts if it is called by an address other than the proposals canceller.
	## `RageQuit.t.sol`
	This file consists of a single test, `testRageQuitDuration`, which checks that if the `DualGovernance` is in the `RageQuit` state, it will remain in the `RageQuit` state until the `RAGE_QUIT_EXTENSION_PERIOD_DURATION` has passed.
	## `TimelockInvariants.t.sol`
	This file consists of tests checking correctness properties of various functions of the `EmergencyProtectedTimelock` contract. These include that these functions produce the correct state changes and that they have the appropriate access protections.
	For simplicity, tests for functions that deal with proposal submission or execution use a proposal with a single call. When the proposal needs to be concretely executed or loaded into memory, we use a simple example proposal that sets a flag in an external contract.
	### `_checkStateRemainsUnchanged`
	Besides the properties exclusive to each test, all tests in this file also include the modifier `_checkStateRemainsUnchanged`, which checks that the function being tested doesn't modify any fields of the contract that it's not supposed to. This modifier does the following:
	1. Saves the state of the `TimelockState.Context` and `EmergencyProtection.Context` records before the test is executed.
	2. Executes the test.
	3. Saves the state of the `TimelockState.Context` and `EmergencyProtection.Context` records after the test is executed.
	4. For each field of the two records, checks if the function selector of the tested function corresponds to one that should modify the field. If not, compares the contents of the field before and after the test to check that they are the same.
	### `testSubmit`
	Tests that when `EmergencyProtectedTimelock.submit` is called by the governance address, it succeeds and the status of the new proposal ID is set as `Submitted`.
	### `testSubmitRevert`
	Tests that `EmergencyProtectedTimelock.submit` reverts when called by any address other than the governance address.
	### `testSchedule`
	Tests that when `EmergencyProtectedTimelock.schedule` is called by the governance address after the post-submission delay for the proposal has passed, it succeeds and the status of the proposal is set to `Scheduled`.
	### `testScheduleRevert`
	Tests that `EmergencyProtectedTimelock.schedule` reverts when called by any address other than the governance address.
	### `testScheduleDelayHasNotPassedRevert`
	Tests that `EmergencyProtectedTimelock.schedule` reverts when the after-submit delay for the proposal has not passed since it was submitted.
	### `testExecute`
	Tests that when `EmergencyProtectedTimelock.execute` is called by the governance address after the post-schedule delay for the proposal has passed, it succeeds and the following are true:
	1. The status of the proposal is set to `Executed`.
	2. The calls are performed to the target contract.
	3. Besides the call from the `EmergencyProtectedTimelock` to the `Executor` and from the `Executor` to the target contract, no other calls are executed.
	### `testExecuteNonScheduledRevert`
	Tests that `EmergencyProtectedTimelock.execute` reverts when the proposal has not been scheduled.
	### `testExecuteExecutedRevert`
	Tests that `EmergencyProtectedTimelock.execute` reverts when the proposal has already been executed.
	### `testExecuteDelayHasNotPassedRevert`
	Tests that `EmergencyProtectedTimelock.execute` reverts when the after-schedule delay for the proposal has not passed since it was scheduled.
	### `testCancelAllNonExecutedProposals`
	Tests that when `EmergencyProtectedTimelock.cancelAllNonExecutedProposals` is called by the governance address, any proposal whose status was not `Executed` has its status set to `Cancelled`.
	### `testOnlyGovernanceCanCancelProposals`
	Tests that `EmergencyProtectedTimelock.cancelAllNonExecutedProposals` reverts if it is called by any address except the governance address.
	### `testCancelledProposalsCannotBeScheduled`
	Tests that `EmergencyProtectedTimelock.schedule` reverts if it is called with a proposal ID that corresponds to a proposal whose status is `Cancelled`.
	### `testCancelledProposalsCannotBeExecuted`
	Tests that `EmergencyProtectedTimelock.execute` reverts if it is called with a proposal ID that corresponds to a proposal whose status is `Cancelled`.
	### `testCancelledProposalsCannotBeEmergencyExecuted`
	Tests that `EmergencyProtectedTimelock.emergencyExecute` reverts if it is called with a proposal ID that corresponds to a proposal whose status is `Cancelled`.
	### `testSetGovernance`
	Tests that when `EmergencyProtectedTimelock.setGovernance` is called by the admin executor, it updates the governance address in `EmergencyProtectedTimelock` to the provided address.
	### `testSetAfterSubmitDelay`
	Tests that when `EmergencyProtectedTimelock.setAfterSubmitDelay` is called by the admin executor, it updates the after-submit delay in `EmergencyProtectedTimelock` to the provided value.
	### `testSetAfterScheduleDelay`
	Tests that when `EmergencyProtectedTimelock.setAfterScheduleDelay` is called by the admin executor, it updates the after-schedule delay in `EmergencyProtectedTimelock` to the provided value.
	### `testTransferExecutorOwnership`
	Tests that when `EmergencyProtectedTimelock.transferExecutorOwnership` is called by the admin executor for an executor owned by the `EmergencyProtectedTimelock`, it updates the owner of the given executor to the provided address.
	### `testSetEmergencyProtectionActivationCommittee`
	Tests that when `EmergencyProtectedTimelock.setEmergencyProtectionActivationCommittee` is called by the admin executor, it updates the address of the emergency activation committee in `EmergencyProtectedTimelock` to the provided address.
	### `testSetEmergencyProtectionExecutionCommittee`
	Tests that when `EmergencyProtectedTimelock.setEmergencyProtectionExecutionCommittee` is called by the admin executor, it updates the address of the emergency execution committee in `EmergencyProtectedTimelock` to the provided address.
	### `testSetEmergencyProtectionEndDate`
	Tests that when `EmergencyProtectedTimelock.setEmergencyProtectionEndDate` is called by the admin executor, it updates the emergency-protection end date in `EmergencyProtectedTimelock` to the provided value.
	### `testSetEmergencyModeDuration`
	Tests that when `EmergencyProtectedTimelock.setEmergencyModeDuration` is called by the admin executor, it updates the emergency-mode duration in `EmergencyProtectedTimelock` to the provided value.
	### `testSetEmergencyGovernance`
	Tests that when `EmergencyProtectedTimelock.setEmergencyGovernance` is called by the admin executor, it updates the emergency-governance address in `EmergencyProtectedTimelock` to the provided address.
	### `testActivateEmergencyMode`
	Tests that when `EmergencyProtectedTimelock.activateEmergencyMode` is called by the address of the emergency activation committee and the emergency mode is not already active, the `EmergencyProtectedTimelock` enters the emergency mode.
	### `testActivateEmergencyModeRevert`
	Tests that `EmergencyProtectedTimelock.activateEmergencyMode` reverts when called by any address other than the emergency activation committee.
	### `testActivateEmergencyModeInEmergencyRevert`
	Tests that `EmergencyProtectedTimelock.activateEmergencyMode` reverts when the `EmergencyProtectedTimelock` is already in emergency mode.
	### `testActivateEmergencyAfterEndDateRevert`
	Tests that `EmergencyProtectedTimelock.activateEmergencyMode` reverts when the emergency-protection end date has already passed.
	### `testEmergencyExecute`
	Tests that when `EmergencyProtectedTimelock.emergencyExecute` is called by the emergency execution committee while the emergency mode is active, the calls are performed to the target contract and the status of the proposal is set to `Executed`.
	### `testEmergencyExecuteNonScheduledRevert`
	Tests that `EmergencyProtectedTimelock.emergencyExecute` reverts when the proposal has not been scheduled.
	### `testEmergencyExecuteExecutedRevert`
	Tests that `EmergencyProtectedTimelock.emergencyExecute` reverts when the proposal has already been executed.
	### `testEmergencyExecuteNormalModeRevert`
	Tests that `EmergencyProtectedTimelock.emergencyExecute` reverts when the `EmergencyProtectedTimelock` is not in emergency mode.
	### `testEmergencyExecuteRevert`
	Tests that `EmergencyProtectedTimelock.emergencyExecute` reverts when called by an address other than the emergency execution committee.
	### `testDeactivateEmergencyMode`
	Tests that when `EmergencyProtectedTimelock.deactivateEmergencyMode` is called, emergency mode is deactivated and all the following variables are zeroed out:
	* `emergencyActivationCommittee`
	* `emergencyExecutionCommittee`
	* `emergencyModeDuration`
	* `emergencyModeEndsAfter`
	* `emergencyProtectionEndsAfter`
	Additionally, any proposal whose status was not `Executed` has its status set to `Cancelled`.
	### `testDeactivateEmergencyModeNormalModeRevert`
	Tests that `EmergencyProtectedTimelock.deactivateEmergencyMode` reverts when the `EmergencyProtectedTimelock` is not in emergency mode.
	### `testDeactivateEmergencyModeRevert`
	Tests that `EmergencyProtectedTimelock.deactivateEmergencyMode` reverts when called by an address other than the admin executor.
	### `testEmergencyReset`
	Tests that `EmergencyProtectedTimelock.emergencyReset` deactivates emergency mode and cancels all non-executed proposals in the same way as `deactivateEmergencyMode`. Additionally, it also sets the governance address to the emergency governance.
	### `testEmergencyResetNormalModeRevert`
	Tests that `EmergencyProtectedTimelock.emergencyReset` reverts when the `EmergencyProtectedTimelock` is not in emergency mode.
	### `testEmergencyResetRevert`
	Tests that `EmergencyProtectedTimelock.emergencyReset` reverts when called by an address other than the emergency execution committee.
	### `testSetAdminExecutor`
	Tests that when `EmergencyProtectedTimelock.setAdminExecutor` is called by the admin executor, it updates the address of the admin executor in `EmergencyProtectedTimelock` to the new address.
	### `testSetGovernanceRevert`
	Tests that `EmergencyProtectedTimelock.setGovernance` reverts when called by an address other than the admin executor.
	### `testSetAfterSubmitDelayRevert`
	Tests that `EmergencyProtectedTimelock.setAfterSubmitDelay` reverts when called by an address other than the admin executor.
	### `testSetAfterScheduleDelayRevert`
	Tests that `EmergencyProtectedTimelock.setAfterScheduleDelay` reverts when called by an address other than the admin executor.
	### `testTransferExecutorOwnershipRevert`
	Tests that `EmergencyProtectedTimelock.transferExecutorOwnership` reverts when called by an address other than the admin executor.
	### `testSetAdminExecutorRevert`
	Tests that `EmergencyProtectedTimelock.setAdminExecutor` reverts when called by an address other than the admin executor.
	### `testSetEmergencyProtectionActivationCommitteeRevert`
	Tests that `EmergencyProtectedTimelock.setEmergencyProtectionActivationCommittee` reverts when called by an address other than the admin executor.
	### `testSetEmergencyProtectionExecutionCommitteeRevert`
	Tests that `EmergencyProtectedTimelock.setEmergencyProtectionExecutionCommittee` reverts when called by an address other than the admin executor.
	### `testSetEmergencyProtectionEndDateRevert`
	Tests that `EmergencyProtectedTimelock.setEmergencyProtectionEndDate` reverts when called by an address other than the admin executor.
	### `testSetEmergencyModeDurationRevert`
	Tests that `EmergencyProtectedTimelock.setEmergencyModeDuration` reverts when called by an address other than the admin executor.
	### `testSetEmergencyGovernanceRevert`
	Tests that `EmergencyProtectedTimelock.setEmergencyGovernance` reverts when called by an address other than the admin executor.
	## `TimelockedGovernance`
	This file contains tests for the `TimelockedGovernance` contract, checking that certain functions can only be called by the governance address.
	### `testSubmitProposalRevert`
	Tests that `TimelockedGovernance.submitProposal` reverts when called by an address other than the governance address.
	### `testCancelAllPendingProposalsRevert`
	Tests that `TimelockedGovernance.cancelAllPendingProposals` reverts when called by an address other than the governance address.
	## `VetoCooldown.t.sol`
	This file consists of a single test, `testVetoCooldownDuration`, which checks that if the `DualGovernance` is in the `VetoCooldown` state, it will remain in the state until the `VETO_COOLDOWN_DURATION` has passed.
	## `VetoSignalling.t.sol`
	This file consists of tests related to the duration of the `VetoSignalling` state. It defines certain invariants that must always hold when the `DualGovernance` is in the `VetoSignalling` state or its `VetoSignallingDeactivation` sub-state, then uses the tests to verify the following:
	1. The invariants hold when the `VetoSignalling` state is first entered (`testVetoSignallingInvariantsHoldInitially`).
	2. The invariants are preserved for as long as the `DualGovernance` remains in the `VetoSignalling` or `VetoSignallingDeactivation` states (`testVetoSignallingInvariantsArePreserved`).
	3. The invariants imply that the duration of the `VetoSignalling` state is bounded by the highest rage-quit support observed during the `VetoSignalling` period (`testDeactivationNotCancelled`).
	The relevant invariants are the following:
	* `_vetoSignallingTimesInvariant`: The `VetoSignalling` activation and reactivation times must have been in the past, and the reactivation time cannot be more than `VETO_SIGNALLING_MAX_DURATION` than the activation time.
	* `_vetoSignallingRageQuitInvariant`: The highest rage-quit support observed since the `VetoSignalling` state was activated cannot be smaller than the current rage-quit support, and cannot be smaller than `FIRST_SEAL_RAGE_QUIT_SUPPORT`.
	* `_vetoSignallingDeactivationInvariant`: The protocol is in the `VetoSignallingDeactivation` sub-state if and only if a) the `VetoSignalling` duration for the current rage-quit support has passed since activation, and b) `VETO_SIGNALLING_MIN_ACTIVE_DURATION` has passed since reactivation. Otherwise, it's in the parent state.
	* `_vetoSignallingMaxDelayInvariant`: If the `VetoSignalling` duration for the highest rage-quit support observed so far has passed since activation, then the protocol is necessarily in the `VetoSignallingDeactivation` sub-state.
	### `testTransitionNormalToVetoSignalling`
	Tests that if the `DualGovernance` is in the `Normal` state, it will transition to `VetoSignalling` if the total rage-quit support in the `SignallingEscrow` is greater than or equal to the `FIRST_SEAL_RAGE_QUIT_SUPPORT`.
	### `testVetoSignallingInvariantsHoldInitially`
	Tests that when the `DualGovernance` first transitions into the `VetoSignalling` state (from the `Normal`, `VetoCooldown` or `RageQuit` states), the `VetoSignalling` invariants hold.
	### `testVetoSignallingInvariantsArePreserved`
	Tests that `DualGovernance.activateNextState` preserves the `VetoSignalling` invariants. More specifically, it
	1. Assumes that the current state is either `VetoSignalling` or `VetoSignallingDeactivation`.
	2. Assumes that the `VetoSignalling` invariants hold.
	3. Calls `activateNextState`.
	4. Update the highest rage-quit support observed so far.
	5. Checks that, if the new state is still either `VetoSignalling` or `VetoSignallingDeactivation`, the invariants still hold.
	### `testDeactivationNotCancelled`
	Tests that `VetoSignallingDeactivation` cannot be exited back to `VetoSignalling` after the maximum `VetoSignalling` duration has passed. The "maximum `VetoSignalling` duration", in this case, means the `VetoSignalling` duration calculated for the highest rage-quit support observed since the `VetoSignalling` state was entered. In other words, if vetoers want to keep increasing the duration of the `VetoSignalling` state, they necessarily will need to keep increasing the funds locked in the `SignallingEscrow`.
	More specifically, this test does the following:
	1. Assumes that the current state is either `VetoSignalling` or `VetoSignallingDeactivation`.
	2. Assumes that the `VetoSignalling` invariants hold.
	3. Assumes that the maximum `VetoSignalling` duration has passed.
	4. Checks that, given these conditions, the state must be `VetoSignallingDeactivation`.
	5. Calls `DualGovernance.activateNextState`.
	6. Checks that the resulting state is either `VetoSignallingDeactivation`, if the `VETO_SIGNALLING_DEACTIVATION_MAX_DURATION` hasn't passed, or `VetoCooldown`, if it has.
	Along with the previous invariant tests, this implies that the duration of the `VetoSignalling` state is limited by the maximum amount of funds that the vetoers are able to amass at once, and this limit can't be unduly extended by locking and unlocking funds over time.