Workaround for fixing voteYays_revert

makerdao · Oct 8, 2024 · 48e7a8e · 48e7a8e
1 parent 0f38292
commit 48e7a8e
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 14 deletions.
diff --git a/certora/VoteDelegate.conf b/certora/VoteDelegate.conf
@@ -6,20 +6,8 @@
         "certora/harness/ChiefMock.sol",
         "certora/harness/PollingMock.sol"
     ],
-    "solc_map": {
-        "VoteDelegate": "solc-0.8.21",
-        "GovMock": "solc-0.8.21",
-        "IouMock": "solc-0.8.21",
-        "ChiefMock": "solc-0.8.21",
-        "PollingMock": "solc-0.8.21"
-    },
-    "solc_optimize_map": {
-        "VoteDelegate": "200",
-        "GovMock": "200",
-        "IouMock": "200",
-        "ChiefMock": "200",
-        "PollingMock": "200"
-    },
+    "solc": "solc-0.8.21",
+    "solc_optimize": "200",
     "link": [
         "VoteDelegate:gov=GovMock",
         "VoteDelegate:chief=ChiefMock",

diff --git a/certora/VoteDelegate.spec b/certora/VoteDelegate.spec
@@ -223,6 +223,10 @@ rule voteYays(address[] yays) {
 rule voteYays_revert(address[] yays) {
     env e;
 
+    require(forall uint256 i. (
+        i >= yays.length || to_mathint(yays[i]) < 2^160
+    ));
+
     address delegate = delegate();
 
     vote@withrevert(e, yays);