Properties to formally verify

[lucasmt]

• Restrictions on operations:
  • Proposals cannot be submitted in the VetoSignallingDeactivation and VetoCooldown states.
  • A proposal cannot be scheduled for execution before ProposalExecutionMinTimelock has passed since its submission.
  • A proposal cannot be scheduled for execution if the Dual Governance state is not Normal or VetoCooldown.
  • A proposal cannot be scheduled for execution if it was submitted after the last time the VetoSignalling state was entered.
  • A proposal cannot be executed until the emergency protection timelock has passed since it was scheduled.
  • A staker cannot unlock funds from the escrow until SignallingEscrowMinLockTime has passed since the last time that user has locked tokens.
  • Funds cannot be locked and unlocked if the escrow is in the RageQuitEscrow state.
  • A user cannot withdraw funds from the escrow until the RageQuitEthClaimTimelock has elapsed after the RageQuitExtensionDelay period.
• Bounds on state duration:
  • After entering the VetoSignalling state, the Deactivation sub-state will be entered after at most T_{lock}(R_{max}) + VetoSignallingMinActiveDuration, where R_{max} is the maximum rage quit support since the state was entered. Then, if no greater rage quit support that R_{max} is observed, the state will transition to VetoCooldown after VetoSignallingDeactivationMaxDuration.
  • The VetoCooldown state lasts for exactly VetoCooldownDuration.
  • The RageQuit state cannot be exited until the current rage quit is finalized (including the RageQuitExtensionDelay period).
• Accounting in the Escrow contract:
  • The rage quit support is calculated correctly.
  • The totals accounted in the Escrow for a token correspond to the balance of the Escrow in that token.
  • The total amount across all withdrawal requests must be less than or equal to the amount of funds in the Escrow.
  • The total amount claimed must be less than or equal to the total amount of withdrawals requested.
  • A user cannot unlock/withdraw more than they have locked in the Escrow.

[Psirex]

Thank you for providing such a comprehensive set of rules🙏🏻. I believe they are essential for verifying the solution's correctness. I would also like to propose a couple of additional invariants that may be worth considering:

Restrictions on Operations:

• Actions that are cancelled or executed cannot be rescheduled.
• The tiebreaker committee can only schedule actions when specific requirements are met, as outlined in the mechanism and specification documents.
• Only admin proposers have the authority to cancel proposals.

Bounds on State Duration:

• The cost of an indefinite governance "lock" must be at least X% of the total stETH supply. The concept is that with each successive RageQuit iteration, the RageQuitEthClaimTimelock increases, requiring the attacker to lock up progressively larger amounts of ETH. Eventually, this makes the attack prohibitively expensive. (This rule might need better phrasing to convey the idea more clearly.)