From 96553597fa2944c7bfb89469532bcc8fe02c8194 Mon Sep 17 00:00:00 2001
From: Hadrien Croubois <hadrien.croubois@gmail.com>
Date: Wed, 15 Mar 2023 21:18:50 +0100
Subject: [PATCH] disable GovernorFunctions

---
 certora/specs.js                             | 45 ++++++++++----------
 certora/specs/GovernorPreventLateQuorum.spec |  4 +-
 2 files changed, 24 insertions(+), 25 deletions(-)

diff --git a/certora/specs.js b/certora/specs.js
index e013e8891..3591f6bba 100644
--- a/certora/specs.js
+++ b/certora/specs.js
@@ -1,6 +1,6 @@
 const product = (...arrays) => arrays.reduce((a, b) => a.flatMap(ai => b.map(bi => [ai, bi].flat())));
 
-module.exports = [
+module.exports = [].concat(
   // AccessControl
   {
     spec: 'AccessControl',
@@ -42,35 +42,34 @@ module.exports = [
     contract: 'InitializableHarness',
     files: ['certora/harnesses/InitializableHarness.sol'],
   },
-  // TimelockController
+  // Governance
   {
     spec: 'TimelockController',
     contract: 'TimelockControllerHarness',
     files: ['certora/harnesses/TimelockControllerHarness.sol'],
     options: ['--optimistic_hashing', '--optimistic_loop'],
   },
-  // Governor
-  ...product(
-    ['GovernorInvariants', 'GovernorBaseRules', 'GovernorChanges', 'GovernorStates'],
+  // Govenor: carthesian product of (spec + harness contract) and (token)
+  product(
+    [].concat(
+      ['GovernorInvariants', 'GovernorBaseRules', 'GovernorChanges', 'GovernorStates'].map(spec => ({
+        contract: 'GovernorHarness',
+        spec,
+      })),
+      ['GovernorPreventLateHarness'].map(spec => ({ contract: 'GovernorPreventLateHarness', spec })),
+    ),
     ['ERC20VotesBlocknumberHarness', 'ERC20VotesTimestampHarness'],
-  ).map(([spec, token]) => ({
+  ).map(([{ contract, spec }, token]) => ({
     spec,
-    contract: 'GovernorHarness',
-    files: ['certora/harnesses/GovernorHarness.sol', `certora/harnesses/${token}.sol`],
+    contract,
+    files: [`certora/harnesses/${contract}.sol`, `certora/harnesses/${token}.sol`],
     options: [`--link GovernorHarness:token=${token}`, '--optimistic_loop', '--optimistic_hashing'],
   })),
-  // WIP part
-  ...product(['GovernorFunctions'], ['ERC20VotesBlocknumberHarness']).map(([spec, token]) => ({
-    spec,
-    contract: 'GovernorHarness',
-    files: ['certora/harnesses/GovernorHarness.sol', `certora/harnesses/${token}.sol`],
-    options: [`--link GovernorHarness:token=${token}`, '--optimistic_loop', '--optimistic_hashing'],
-  })),
-  // WIP prevent late quorum
-  ...product(['GovernorPreventLateQuorum'], ['ERC20VotesBlocknumberHarness']).map(([spec, token]) => ({
-    spec,
-    contract: 'GovernorPreventLateHarness',
-    files: ['certora/harnesses/GovernorPreventLateHarness.sol', `certora/harnesses/${token}.sol`],
-    options: [`--link GovernorPreventLateHarness:token=${token}`, '--optimistic_loop', '--optimistic_hashing'],
-  })),
-];
+  /// WIP part
+  // product(['GovernorFunctions'], ['ERC20VotesBlocknumberHarness']).map(([spec, token]) => ({
+  //   spec,
+  //   contract: 'GovernorHarness',
+  //   files: ['certora/harnesses/GovernorHarness.sol', `certora/harnesses/${token}.sol`],
+  //   options: [`--link GovernorHarness:token=${token}`, '--optimistic_loop', '--optimistic_hashing'],
+  // })),
+);
diff --git a/certora/specs/GovernorPreventLateQuorum.spec b/certora/specs/GovernorPreventLateQuorum.spec
index 5ed48a555..25cc03888 100644
--- a/certora/specs/GovernorPreventLateQuorum.spec
+++ b/certora/specs/GovernorPreventLateQuorum.spec
@@ -26,8 +26,8 @@ rule deadlineChangeToPreventLateQuorum(uint256 pId, env e, method f, calldataarg
     requireInvariant proposalStateConsistency(pId);
     requireInvariant votesImplySnapshotPassed(pId);
 
-    // This is not (easily) provable because the prover think `_totalSupplyCheckpoints` can arbitrarily change,
-    // which causes the quorum() to change. Not sure how to fix that.
+    // This is not (easily) provable as an invariant because the prover think `_totalSupplyCheckpoints`
+    // can arbitrarily change, which causes the quorum() to change. Not sure how to fix that.
     require !quorumReached(pId) <=> getExtendedDeadline(pId) == 0;
 
     uint256 deadlineBefore         = proposalDeadline(pId);