Adapting the test to the latest client code

.github/workflows/lido-ci.yml

@@ -1,9 +1,12 @@
 ---
   name: "Test Proofs"
   on:
+    workflow_dispatch:
     push:
       branches:
         - develop
+        - rvdevelop
+        - tests-on-client-code
   jobs:
     test:
       runs-on: ubuntu-latest
@@ -23,10 +26,9 @@
               -H "Authorization: Bearer ${{ secrets.RV_COMPUTE_TOKEN }}" \
               https://api.github.com/repos/runtimeverification/_kaas_lidofinance_dual-governance/actions/workflows/lido-ci.yml/dispatches \
               -d '{
-                "ref": "develop",
+                "ref": "master",
                 "inputs": {
                 "branch_name": "'"${{ github.event.pull_request.head.sha || github.sha }}"'",
-                "extra_args": "script",
                 "statuses_sha": "'$sha'",
                 "org": "${{ github.repository_owner }}",
                 "repository": "${{ github.event.repository.name }}",

contracts/interfaces/IStETH.sol

@@ -9,10 +9,11 @@ interface IStETH is IERC20 {
 
     function getPooledEthByShares(uint256 sharesAmount) external view returns (uint256);
 
-    function transferShares(address to, uint256 amount) external;
+    function transferShares(address to, uint256 amount) external returns (uint256);
     function transferSharesFrom(
         address _sender,
         address _recipient,
         uint256 _sharesAmount
     ) external returns (uint256);
+    function sharesOf(address _account) external view returns (uint256);
 }

contracts/libraries/DualGovernanceState.sol

@@ -2,6 +2,7 @@
 pragma solidity 0.8.23;
 
 import {Clones} from "@openzeppelin/contracts/proxy/Clones.sol";
+import {Math} from "@openzeppelin/contracts/utils/math/Math.sol";
 
 import {IEscrow} from "../interfaces/IEscrow.sol";
 import {ISealable} from "../interfaces/ISealable.sol";
@@ -297,14 +298,14 @@ library DualGovernanceState {
         DualGovernanceConfig memory config,
         uint256 rageQuitSupport
     ) private pure returns (bool) {
-        return rageQuitSupport > config.firstSealRageQuitSupport;
+        return rageQuitSupport >= config.firstSealRageQuitSupport;
     }
 
     function _isSecondSealRageQuitSupportCrossed(
         DualGovernanceConfig memory config,
         uint256 rageQuitSupport
     ) private pure returns (bool) {
-        return rageQuitSupport > config.secondSealRageQuitSupport;
+        return rageQuitSupport >= config.secondSealRageQuitSupport;
     }
 
     function _isDynamicTimelockMaxDurationPassed(
@@ -327,7 +328,17 @@ library DualGovernanceState {
         Store storage self,
         DualGovernanceConfig memory config
     ) private view returns (bool) {
-        return Timestamps.now() > config.vetoSignallingMinActiveDuration.addTo(self.vetoSignallingReactivationTime);
+        return Timestamps.now()
+            > config.vetoSignallingMinActiveDuration.addTo(
+                Timestamp.wrap(
+                    uint40(
+                        Math.max(
+                            Timestamp.unwrap(self.vetoSignallingActivationTime),
+                            Timestamp.unwrap(self.vetoSignallingReactivationTime)
+                        )
+                    )
+                )
+            );
     }
 
     function _isVetoSignallingDeactivationMaxDurationPassed(
@@ -381,15 +392,15 @@ library DualGovernanceState {
             return Durations.ZERO;
         }
 
-        if (rageQuitSupport >= secondSealRageQuitSupport) {
-            return dynamicTimelockMaxDuration;
+        if (rageQuitSupport < secondSealRageQuitSupport) {
+            return dynamicTimelockMinDuration
+                + Durations.from(
+                    (rageQuitSupport - firstSealRageQuitSupport)
+                        * (dynamicTimelockMaxDuration - dynamicTimelockMinDuration).toSeconds()
+                        / (secondSealRageQuitSupport - firstSealRageQuitSupport)
+                );
         }
 
-        duration_ = dynamicTimelockMinDuration
-            + Durations.from(
-                (rageQuitSupport - firstSealRageQuitSupport)
-                    * (dynamicTimelockMaxDuration - dynamicTimelockMinDuration).toSeconds()
-                    / (secondSealRageQuitSupport - firstSealRageQuitSupport)
-            );
+        return dynamicTimelockMaxDuration;
     }
 }

contracts/libraries/WithdrawalBatchesQueue.sol

@@ -7,17 +7,6 @@ import {SafeCast} from "@openzeppelin/contracts/utils/math/SafeCast.sol";
 import {ArrayUtils} from "../utils/arrays.sol";
 import {SequentialBatch, SequentialBatches} from "../types/SequentialBatches.sol";
 
-enum Status {
-    // The default status of the WithdrawalsBatchesQueue. In the closed state the only action allowed
-    // to be called is open(), which transfers it into Opened state.
-    Empty,
-    // In the Opened state WithdrawalsBatchesQueue allows to add batches into the queue
-    Opened,
-    // When the WithdrawalsBatchesQueue enters Filled queue - it's not allowed to add batches and
-    // only allowed to mark batches claimed
-    Closed
-}
-
 struct QueueIndex {
     uint32 batchIndex;
     uint16 valueIndex;
@@ -26,6 +15,17 @@ struct QueueIndex {
 library WithdrawalsBatchesQueue {
     using SafeCast for uint256;
 
+    enum Status {
+        // The default status of the WithdrawalsBatchesQueue. In the closed state the only action allowed
+        // to be called is open(), which transfers it into Opened state.
+        Empty,
+        // In the Opened state WithdrawalsBatchesQueue allows to add batches into the queue
+        Opened,
+        // When the WithdrawalsBatchesQueue enters Filled queue - it's not allowed to add batches and
+        // only allowed to mark batches claimed
+        Closed
+    }
+
     struct State {
         Status status;
         QueueIndex lastClaimedUnstETHIdIndex;

contracts/model/DualGovernance.sol → contracts/model/DualGovernanceModel.sol

@@ -3,8 +3,8 @@ pragma solidity ^0.8.0;
 
 import "@openzeppelin/contracts/utils/math/Math.sol";
 
-import "./EmergencyProtectedTimelock.sol";
-import "./Escrow.sol";
+import "./EmergencyProtectedTimelockModel.sol";
+import "./EscrowModel.sol";
 
 /**
  * @title Dual Governance Mechanism
@@ -13,7 +13,7 @@ import "./Escrow.sol";
  */
 
 // DualGovernance contract to handle proposal submissions and lifecycle management.
-contract DualGovernance {
+contract DualGovernanceModel {
     enum State {
         Normal,
         VetoSignalling,
@@ -22,13 +22,12 @@ contract DualGovernance {
         RageQuit
     }
 
-    EmergencyProtectedTimelock public emergencyProtectedTimelock;
-    Escrow public signallingEscrow;
-    Escrow public rageQuitEscrow;
+    EmergencyProtectedTimelockModel public emergencyProtectedTimelock;
+    EscrowModel public signallingEscrow;
+    EscrowModel public rageQuitEscrow;
     address public fakeETH;
 
     // State Variables
-    State public currentState;
     mapping(address => bool) public proposers;
     mapping(address => bool) public admin_proposers;
     uint256 public lastStateChangeTime;
@@ -37,6 +36,8 @@ contract DualGovernance {
     uint256 public lastVetoSignallingTime;
     uint256 public rageQuitSequenceNumber;
 
+    State public currentState;
+
     // Constants
     uint256 public constant FIRST_SEAL_RAGE_QUIT_SUPPORT = 10 ** 16; // Threshold required for transition from Normal to Veto Signalling state (1%).
     uint256 public constant SECOND_SEAL_RAGE_QUIT_SUPPORT = 10 ** 17; // Transition to Rage Quit occurs if t - t^S_{act} > DynamicTimelockMaxDuration and R > SecondSealRageQuitSupport (10%).
@@ -52,8 +53,8 @@ contract DualGovernance {
         currentState = State.Normal;
         lastStateChangeTime = block.timestamp;
         fakeETH = _fakeETH;
-        emergencyProtectedTimelock = new EmergencyProtectedTimelock(address(this), emergencyProtectionTimelock);
-        signallingEscrow = new Escrow(address(this), _fakeETH);
+        emergencyProtectedTimelock = new EmergencyProtectedTimelockModel(address(this), emergencyProtectionTimelock);
+        signallingEscrow = new EscrowModel(address(this), _fakeETH);
     }
 
     // Operations
@@ -86,7 +87,7 @@ contract DualGovernance {
             "Proposals can only be scheduled in Normal or Veto Cooldown states."
         );
         if (currentState == State.VetoCooldown) {
-            (,,, uint256 submissionTime,) = emergencyProtectedTimelock.proposals(proposalId);
+            (,, uint256 submissionTime,,) = emergencyProtectedTimelock.proposals(proposalId);
             require(
                 submissionTime < lastVetoSignallingTime,
                 "Proposal submitted after the last time Veto Signalling state was entered."
@@ -117,7 +118,7 @@ contract DualGovernance {
     function calculateDynamicTimelock(uint256 rageQuitSupport) public pure returns (uint256) {
         if (rageQuitSupport <= FIRST_SEAL_RAGE_QUIT_SUPPORT) {
             return 0;
-        } else if (rageQuitSupport < SECOND_SEAL_RAGE_QUIT_SUPPORT) {
+        } else if (rageQuitSupport <= SECOND_SEAL_RAGE_QUIT_SUPPORT) {
             return linearInterpolation(rageQuitSupport);
         } else {
             return DYNAMIC_TIMELOCK_MAX_DURATION;
@@ -132,6 +133,13 @@ contract DualGovernance {
     function linearInterpolation(uint256 rageQuitSupport) private pure returns (uint256) {
         uint256 L_min = DYNAMIC_TIMELOCK_MIN_DURATION;
         uint256 L_max = DYNAMIC_TIMELOCK_MAX_DURATION;
+        // Assumption: No underflow
+        require(FIRST_SEAL_RAGE_QUIT_SUPPORT <= rageQuitSupport);
+        // Assumption: No overflow
+        require(
+            ((rageQuitSupport - FIRST_SEAL_RAGE_QUIT_SUPPORT) * (L_max - L_min)) / (L_max - L_min)
+                == (rageQuitSupport - FIRST_SEAL_RAGE_QUIT_SUPPORT)
+        );
         return L_min
             + ((rageQuitSupport - FIRST_SEAL_RAGE_QUIT_SUPPORT) * (L_max - L_min))
                 / (SECOND_SEAL_RAGE_QUIT_SUPPORT - FIRST_SEAL_RAGE_QUIT_SUPPORT);
@@ -149,7 +157,7 @@ contract DualGovernance {
             signallingEscrow.startRageQuit();
             rageQuitSequenceNumber++;
             rageQuitEscrow = signallingEscrow;
-            signallingEscrow = new Escrow(address(this), fakeETH);
+            signallingEscrow = new EscrowModel(address(this), fakeETH);
         }
 
         lastStateChangeTime = block.timestamp;
@@ -180,6 +188,11 @@ contract DualGovernance {
     // State Transitions
 
     function activateNextState() public {
+        // Assumption: various time stamps are in the past
+        require(lastStateChangeTime <= block.timestamp);
+        require(lastSubStateActivationTime <= block.timestamp);
+        require(lastStateReactivationTime <= block.timestamp);
+
         uint256 rageQuitSupport = signallingEscrow.getRageQuitSupport();
 
         State previousState;
@@ -224,12 +237,14 @@ contract DualGovernance {
 
         // Check the conditions for transitioning to RageQuit or Veto Deactivation based on the time elapsed and support level.
         if (
-            block.timestamp - lastStateChangeTime > DYNAMIC_TIMELOCK_MAX_DURATION
+            block.timestamp != lastStateChangeTime
+                && block.timestamp - lastStateChangeTime > DYNAMIC_TIMELOCK_MAX_DURATION
                 && rageQuitSupport > SECOND_SEAL_RAGE_QUIT_SUPPORT
         ) {
             transitionState(State.RageQuit);
         } else if (
-            block.timestamp - lastStateChangeTime > calculateDynamicTimelock(rageQuitSupport)
+            block.timestamp != lastStateChangeTime
+                && block.timestamp - lastStateChangeTime > calculateDynamicTimelock(rageQuitSupport)
                 && block.timestamp - Math.max(lastStateChangeTime, lastStateReactivationTime)
                     > VETO_SIGNALLING_MIN_ACTIVE_DURATION
         ) {
@@ -247,7 +262,8 @@ contract DualGovernance {
         uint256 elapsed = block.timestamp - lastSubStateActivationTime;
         // Check the conditions for transitioning to VetoCooldown or back to VetoSignalling
         if (
-            block.timestamp - lastStateChangeTime <= calculateDynamicTimelock(rageQuitSupport)
+            block.timestamp == lastStateChangeTime
+                || block.timestamp - lastStateChangeTime <= calculateDynamicTimelock(rageQuitSupport)
                 || rageQuitSupport > SECOND_SEAL_RAGE_QUIT_SUPPORT
         ) {
             exitSubState(State.VetoSignalling);
@@ -264,7 +280,7 @@ contract DualGovernance {
         require(currentState == State.VetoCooldown, "Must be in Veto Cooldown state.");
 
         // Ensure the Veto Cooldown has lasted for at least the minimum duration.
-        if (block.timestamp - lastStateChangeTime > VETO_COOLDOWN_DURATION) {
+        if (block.timestamp != lastStateChangeTime && block.timestamp - lastStateChangeTime > VETO_COOLDOWN_DURATION) {
             // Depending on the level of rage quit support, transition to Normal or Veto Signalling.
             if (rageQuitSupport <= FIRST_SEAL_RAGE_QUIT_SUPPORT) {
                 transitionState(State.Normal);
@@ -279,7 +295,7 @@ contract DualGovernance {
      * Checks if withdrawal process is complete, cooldown period expired.
      * Transitions to VetoCooldown if support has decreased below the threshold; otherwise, transitions to VetoSignalling.
      */
-    function fromRageQuit(uint256 rageQuitSupport) private {
+    function fromRageQuit(uint256 rageQuitSupport) public {
         require(currentState == State.RageQuit, "Must be in Rage Quit state.");
 
         // Check if the withdrawal process is completed and if the RageQuitExtensionDelay has elapsed

contracts/model/EmergencyProtectedTimelock.sol → contracts/model/EmergencyProtectedTimelockModel.sol

@@ -26,7 +26,7 @@ struct Proposal {
 
 // This contract manages the timelocking of proposals with emergency intervention capabilities.
 // It provides controls for entering and managing emergency states as well as executing proposals under normal and emergency conditions.
-contract EmergencyProtectedTimelock {
+contract EmergencyProtectedTimelockModel {
     // Addresses associated with governance roles and permissions.
     address public governance;
     address public emergencyGovernance;
@@ -124,11 +124,13 @@ contract EmergencyProtectedTimelock {
     function cancelAllNonExecutedProposals() public {
         require(msg.sender == governance, "Caller is not authorized to cancel proposal.");
 
-        // Loop through all the proposals stored in the contract.
-        for (uint256 i = 0; i < nextProposalId; i++) {
-            // Ensure that only proposals in 'Submitted' or 'Scheduled' status are canceled.
-            if (proposals[i].status != ProposalStatus.Executed) {
-                proposals[i].status = ProposalStatus.Canceled;
+        if (nextProposalId > 0) {
+            // Loop through all the proposals stored in the contract.
+            for (uint256 i = 0; i < nextProposalId; i++) {
+                // Ensure that only proposals in 'Submitted' or 'Scheduled' status are canceled.
+                if (proposals[i].status != ProposalStatus.Executed) {
+                    proposals[i].status = ProposalStatus.Canceled;
+                }
             }
         }
     }