Merge pull request #48 from runtimeverification/rv/update

Fixes to formal verification code
lidofinance · Jun 13, 2024 · 2a382ff · 2a382ff
2 parents f74516e + ac35908
commit 2a382ff
Show file tree

Hide file tree

Showing 7 changed files with 24 additions and 27 deletions.
diff --git a/.github/workflows/lido-ci.yml b/.github/workflows/lido-ci.yml
@@ -1,9 +1,9 @@
 ---
   name: "Test Proofs"
   on:
-    pull_request:
+    push:
       branches:
-        - main
+        - develop
   jobs:
     test:
       runs-on: ubuntu-latest
@@ -23,13 +23,13 @@
               -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": "master",
+                "ref": "develop",
                 "inputs": {
                 "branch_name": "'"${{ github.event.pull_request.head.sha || github.sha }}"'",
                 "extra_args": "script",
                 "statuses_sha": "'$sha'",
-                "org": "lidofinance",
-                "repository": "dual-governance",
+                "org": "${{ github.repository_owner }}",
+                "repository": "${{ github.event.repository.name }}",
                 "auth_token": "'"${{ secrets.LIDO_STATUS_TOKEN }}"'"
                 }
               }')

diff --git a/contracts/model/DualGovernance.sol b/contracts/model/DualGovernance.sol
@@ -1,6 +1,8 @@
 // SPDX-License-Identifier: MIT
 pragma solidity ^0.8.0;
 
+import "@openzeppelin/contracts/utils/math/Math.sol";
+
 import "./EmergencyProtectedTimelock.sol";
 import "./Escrow.sol";
 
@@ -84,8 +86,9 @@ contract DualGovernance {
             "Proposals can only be scheduled in Normal or Veto Cooldown states."
         );
         if (currentState == State.VetoCooldown) {
+            uint256 submissionTime = emergencyProtectedTimelock.proposals(proposalId).submissionTime;
             require(
-                block.timestamp < lastVetoSignallingTime,
+                submissionTime < lastVetoSignallingTime,
                 "Proposal submitted after the last time Veto Signalling state was entered."
             );
         }
@@ -174,10 +177,6 @@ contract DualGovernance {
         currentState = parentState;
     }
 
-    function max(uint256 a, uint256 b) private pure returns (uint256) {
-        return a > b ? a : b;
-    }
-
     // State Transitions
 
     function activateNextState() public {
@@ -231,7 +230,7 @@ contract DualGovernance {
             transitionState(State.RageQuit);
         } else if (
             block.timestamp - lastStateChangeTime > calculateDynamicTimelock(rageQuitSupport)
-                && block.timestamp - max(lastStateChangeTime, lastStateReactivationTime)
+                && block.timestamp - Math.max(lastStateChangeTime, lastStateReactivationTime)
                     > VETO_SIGNALLING_MIN_ACTIVE_DURATION
         ) {
             enterSubState(State.VetoSignallingDeactivation);

diff --git a/contracts/model/EmergencyProtectedTimelock.sol b/contracts/model/EmergencyProtectedTimelock.sol
@@ -55,8 +55,6 @@ contract EmergencyProtectedTimelock {
     function submit(address executor, ExecutorCall[] memory calls) external returns (uint256 proposalId) {
         // Ensure that only the governance can submit new proposals.
         require(msg.sender == governance, "Only governance can submit proposal.");
-        // Establish the minimum timelock duration for the proposal's execution.
-        uint256 executionDelay = PROPOSAL_EXECUTION_MIN_TIMELOCK;
 
         proposals[nextProposalId].id = nextProposalId;
         proposals[nextProposalId].proposer = executor;

diff --git a/contracts/model/Escrow.sol b/contracts/model/Escrow.sol
@@ -67,7 +67,7 @@ contract Escrow {
         require(currentState == State.SignallingEscrow, "Cannot lock in current state.");
         require(amount > 0, "Amount must be greater than zero.");
         require(fakeETH.allowance(msg.sender, address(this)) >= amount, "Need allowance to transfer tokens.");
-        require(fakeETH.balanceOf(msg.sender) <= amount, "Not enough balance.");
+        require(fakeETH.balanceOf(msg.sender) >= amount, "Not enough balance.");
         fakeETH.transferFrom(msg.sender, address(this), amount);
         balances[msg.sender] += amount;
         totalStaked += amount;

diff --git a/foundry.toml b/foundry.toml
@@ -5,6 +5,12 @@ libs = ['node_modules', 'lib']
 test = 'test'
 cache_path  = 'cache_forge'
 solc-version = "0.8.23"
+no-match-path = 'test/kontrol/*'
+
+[profile.kprove]
+src = 'test/kontrol'
+out = 'kout'
+test = 'test/kontrol'
 
 [fmt]
 multiline_func_header = 'params_first'
diff --git a/test/kontrol/VetoSignalling.t.sol b/test/kontrol/VetoSignalling.t.sol
@@ -26,7 +26,7 @@ contract VetoSignallingTest is Test, KontrolCheats {
     // Note: there are lemmas dependent on `ethUpperBound`
     uint256 constant ethMaxWidth = 96;
     uint256 constant ethUpperBound = 2 ** ethMaxWidth;
-    uint256 constant timeUpperBound = 2 ** 40 - 1;
+    uint256 constant timeUpperBound = 2 ** 40;
 
     enum Mode {
         Assume,
@@ -150,7 +150,7 @@ contract VetoSignallingTest is Test, KontrolCheats {
         _storeUInt256(address(rageQuitEscrow), 5, totalClaimedEthAmount);
         // Slot 11
         uint256 rageQuitExtensionDelayPeriodEnd = kevm.freshUInt(32); // ?WORD10
-        _storeUInt256(address(signallingEscrow), 11, rageQuitExtensionDelayPeriodEnd);
+        _storeUInt256(address(rageQuitEscrow), 11, rageQuitExtensionDelayPeriodEnd);
     }
 
     function _storeBytes32(address contractAddress, uint256 slot, bytes32 value) internal {
@@ -345,15 +345,6 @@ contract VetoSignallingTest is Test, KontrolCheats {
         vm.assume(previousRageQuitSupport < ethUpperBound);
         vm.assume(maxRageQuitSupport < ethUpperBound);
 
-        // Temporary assumptions
-        vm.assume(previousRageQuitSupport <= 1);
-        vm.assume(10 <= maxRageQuitSupport);
-        vm.assume(
-            lastInteractionTimestamp
-                <= dualGovernance.lastStateChangeTime() + dualGovernance.calculateDynamicTimelock(previousRageQuitSupport)
-        );
-        // Temparary assumptions
-
         StateRecord memory previous =
             _recordPreviousState(lastInteractionTimestamp, previousRageQuitSupport, maxRageQuitSupport);
 
@@ -385,9 +376,12 @@ contract VetoSignallingTest is Test, KontrolCheats {
         uint256 previousRageQuitSupport,
         uint256 maxRageQuitSupport
     ) external {
+        vm.assume(block.timestamp < timeUpperBound);
+
         StateRecord memory previous =
             _recordPreviousState(lastInteractionTimestamp, previousRageQuitSupport, maxRageQuitSupport);
 
+        vm.assume(previous.maxRageQuitSupport <= dualGovernance.SECOND_SEAL_RAGE_QUIT_SUPPORT());
         vm.assume(_maxDeactivationDelayPassed(previous));
         vm.assume(signallingEscrow.getRageQuitSupport() <= previous.maxRageQuitSupport);
 

diff --git a/test/kontrol/scripts/run-kontrol.sh b/test/kontrol/scripts/run-kontrol.sh
@@ -5,9 +5,9 @@ SCRIPT_HOME="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
 # shellcheck source=/dev/null
 source "$SCRIPT_HOME/common.sh"
 export RUN_KONTROL=true
-CUSTOM_FOUNDRY_PROFILE=default
+CUSTOM_FOUNDRY_PROFILE=kprove
 export FOUNDRY_PROFILE=$CUSTOM_FOUNDRY_PROFILE
-export OUT_DIR=out # out dir of $FOUNDRY_PROFILE
+export OUT_DIR=kout # out dir of $FOUNDRY_PROFILE
 parse_args "$@"
 
 #############