adding VetoSignalling invariant

runtimeverification · Aug 8, 2024 · 485e593 · 485e593
1 parent 73aef2a
commit 485e593
Show file tree

Hide file tree

Showing 4 changed files with 20 additions and 28 deletions.
diff --git a/contracts/libraries/DualGovernanceState.sol b/contracts/libraries/DualGovernanceState.sol
@@ -388,7 +388,7 @@ library DualGovernanceState {
         Duration dynamicTimelockMinDuration = config.dynamicTimelockMinDuration;
         Duration dynamicTimelockMaxDuration = config.dynamicTimelockMaxDuration;
 
-        if (rageQuitSupport < firstSealRageQuitSupport) {
+        if (rageQuitSupport <= firstSealRageQuitSupport) {
             return Durations.ZERO;
         }
 

diff --git a/test/kontrol/EscrowLockUnlock.t.sol b/test/kontrol/EscrowLockUnlock.t.sol
@@ -90,11 +90,6 @@ contract EscrowLockUnlockTest is EscrowInvariants, DualGovernanceSetUp {
         this.signallingEscrowInvariants(Mode.Assume, signallingEscrow);
         this.escrowUserInvariants(Mode.Assume, signallingEscrow, sender);
 
-        ActivateNextStateMock mock = new ActivateNextStateMock(address(this), sender);
-        kevm.mockFunction(
-            address(dualGovernance), address(mock), abi.encodeWithSelector(mock.activateNextState.selector)
-        );
-
         vm.startPrank(sender);
         signallingEscrow.lockStETH(amount);
         vm.stopPrank();
@@ -117,11 +112,7 @@ contract EscrowLockUnlockTest is EscrowInvariants, DualGovernanceSetUp {
 
         uint256 errorTerm = stEth.getPooledEthByShares(1) + 1;
         assert(post.userBalance <= pre.userBalance - amount + errorTerm);
-        // Rewritten to avoid branching
-        //assert(pre.escrowBalance + amount < errorTerm || pre.escrowBalance + amount - errorTerm <= post.escrowBalance);
         assert(pre.escrowBalance + amount <= post.escrowBalance + errorTerm);
-        // Rewritten to avoid branching
-        //assert(pre.totalEth + amount < errorTerm || pre.totalEth + amount - errorTerm <= post.totalEth);
         assert(pre.totalEth + amount <= post.totalEth + errorTerm);
     }
 

diff --git a/test/kontrol/VetoSignalling.t.sol b/test/kontrol/VetoSignalling.t.sol
@@ -57,6 +57,7 @@ contract VetoSignallingTest is DualGovernanceSetUp {
         return (
             _establish(mode, sr.timestamp <= Timestamps.now()) && _establish(mode, sr.activationTime <= sr.timestamp)
                 && _establish(mode, sr.reactivationTime <= sr.timestamp)
+                && _establish(mode, sr.reactivationTime <= addTo(config.DYNAMIC_TIMELOCK_MAX_DURATION(), sr.activationTime))
         );
     }
 
@@ -74,7 +75,7 @@ contract VetoSignallingTest is DualGovernanceSetUp {
     }
 
     function _calculateDynamicTimelock(Configuration _config, uint256 rageQuitSupport) public view returns (Duration) {
-        if (rageQuitSupport < _config.FIRST_SEAL_RAGE_QUIT_SUPPORT()) {
+        if (rageQuitSupport <= _config.FIRST_SEAL_RAGE_QUIT_SUPPORT()) {
             return Durations.ZERO;
         } else if (rageQuitSupport < _config.SECOND_SEAL_RAGE_QUIT_SUPPORT()) {
             return _linearInterpolation(_config, rageQuitSupport);
@@ -113,7 +114,7 @@ contract VetoSignallingTest is DualGovernanceSetUp {
         if (
             sr.timestamp
                 <= addTo(
-                    config.VETO_SIGNALLING_MIN_ACTIVE_DURATION(), _maxTimestamp(sr.reactivationTime, sr.activationTime)
+                    config.VETO_SIGNALLING_MIN_ACTIVE_DURATION(), _maxTimestamp(sr.activationTime, sr.reactivationTime)
                 )
         ) {
             return _establish(mode, sr.state == State.VetoSignalling);
@@ -260,19 +261,19 @@ contract VetoSignallingTest is DualGovernanceSetUp {
                 // Establish third invariant
                 _vetoSignallingDeactivationInvariant(Mode.Assert, current);
             }
-            // Try establishing fourth invariant
-            if (!_vetoSignallingMaxDelayInvariant(Mode.Try, current)) {
-                // Assume third invariant if not already assumed
-                if (!assumedDeactivationInvariant) {
-                    _vetoSignallingDeactivationInvariant(Mode.Assume, previous);
-                }
-                // Assume fourth invariant if not already assumed
-                if (!assumedMaxDelayInvariant) {
-                    _vetoSignallingMaxDelayInvariant(Mode.Assume, previous);
-                }
-                // Establish fourth invariant
-                _vetoSignallingMaxDelayInvariant(Mode.Assert, current);
-            }
+            // // Try establishing fourth invariant
+            // if (!_vetoSignallingMaxDelayInvariant(Mode.Try, current)) {
+            //     // Assume third invariant if not already assumed
+            //     if (!assumedDeactivationInvariant) {
+            //         _vetoSignallingDeactivationInvariant(Mode.Assume, previous);
+            //     }
+            //     // Assume fourth invariant if not already assumed
+            //     if (!assumedMaxDelayInvariant) {
+            //         _vetoSignallingMaxDelayInvariant(Mode.Assume, previous);
+            //     }
+            //     // Establish fourth invariant
+            //     _vetoSignallingMaxDelayInvariant(Mode.Assert, current);
+            // }
             return;
         }
         vm.assume(currentState == State.VetoSignalling || currentState == State.VetoSignallingDeactivation);

diff --git a/test/kontrol/lido-lemmas.k b/test/kontrol/lido-lemmas.k
@@ -114,6 +114,9 @@ module LIDO-LEMMAS
     rule [bool2Word-gt-zero]:  0 <Int bool2Word(B:Bool)     => B                           [simplification(30)]
     rule [bool2Word-gt-false]: X:Int <Int bool2Word(_:Bool) => false     requires 1 <Int X [simplification(30), concrete(X)]
 
+    rule 0 <=Int bool2Word(X) => true [simplification, smt-lemma]
+    rule bool2Word(X) <=Int 1 => true [simplification, smt-lemma]
+
     //
     // .Bytes
     //
@@ -407,9 +410,6 @@ module LIDO-LEMMAS
         requires #rangeUInt(256, VALUE)
         [simplification]
 
-    rule bool2Word ( X ) <=Int 1 => true
-        [simplification, smt-lemma]
-
     rule chop ( X -Int Y ) => X -Int Y
         requires #rangeUInt(256, X)
          andBool #rangeUInt(256, Y)