VetoCooldown

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

Hide file tree

Showing 2 changed files with 17 additions and 17 deletions.
diff --git a/test/kontrol/VetoCooldown.t.sol b/test/kontrol/VetoCooldown.t.sol
@@ -3,21 +3,21 @@ pragma solidity 0.8.23;
 import "forge-std/Vm.sol";
 import "kontrol-cheatcodes/KontrolCheats.sol";
 
-import {Duration, Durations} from "contracts/types/Duration.sol";
+import {addTo, Duration, Durations} from "contracts/types/Duration.sol";
 import {Timestamp, Timestamps} from "contracts/types/Timestamp.sol";
 
 import "test/kontrol/DualGovernanceSetUp.sol";
 
 contract VetoCooldownTest is DualGovernanceSetUp {
     function testVetoCooldownDuration() external {
         vm.assume(dualGovernance.getCurrentState() == State.VetoCooldown);
+        Timestamp timeEnteredAt = Timestamp.wrap(_getEnteredAt(dualGovernance));
+        Timestamp maxCooldownDuration = addTo(config.VETO_COOLDOWN_DURATION(), timeEnteredAt);
 
         dualGovernance.activateNextState();
 
         bool stillInVetoCooldown = (dualGovernance.getCurrentState() == State.VetoCooldown);
-        Timestamp timeEnteredAt = Timestamp.wrap(_getEnteredAt(dualGovernance));
-        Duration timeInVetoCooldown = Durations.between(Timestamps.now(), timeEnteredAt);
-        bool durationHasElapsed = (timeInVetoCooldown > config.VETO_COOLDOWN_DURATION());
+        bool durationHasElapsed = (Timestamps.now() > maxCooldownDuration);
         assert(stillInVetoCooldown != durationHasElapsed);
     }
 }
diff --git a/test/kontrol/VetoSignalling.t.sol b/test/kontrol/VetoSignalling.t.sol
@@ -261,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);