From ff8e17ec2f4cb717af7cb568fab39703f440353f Mon Sep 17 00:00:00 2001
From: Aleksander Kryukov <firealexkryukov@gmail.com>
Date: Mon, 22 Nov 2021 12:17:41 +0200
Subject: [PATCH] removedHarnessesAnsSummariesAddedComments

---
 certora/specs/GovernorBase.spec                            | 7 +++----
 contracts/governance/Governor.sol                          | 2 +-
 contracts/governance/TimelockController.sol                | 1 +
 .../governance/extensions/GovernorTimelockControl.sol      | 6 ++----
 4 files changed, 7 insertions(+), 9 deletions(-)

diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec
index c2ae24606..b976c790b 100644
--- a/certora/specs/GovernorBase.spec
+++ b/certora/specs/GovernorBase.spec
@@ -32,8 +32,8 @@ methods {
     erc20votes.getPastTotalSupply(uint256) returns uint256
     erc20votes.getPastVotes(address, uint256) returns uint256
 
-    scheduleBatch(address[],uint256[],bytes[],bytes32,bytes32,uint256) => NONDET
-    executeBatch(address[], uint256[], bytes[], bytes32, bytes32) => NONDET
+    //scheduleBatch(address[],uint256[],bytes[],bytes32,bytes32,uint256) => DISPATCHER(true)
+    //executeBatch(address[], uint256[], bytes[], bytes32, bytes32) => DISPATCHER(true)
 }
 
 //////////////////////////////////////////////////////////////////////////////
@@ -191,8 +191,7 @@ rule doubleVoting(uint256 pId, uint8 sup, method f) filtered { f-> f.selector ==
     } else{
         f@withrevert(e, args);
     }
-
-
+    
     assert votedCheck => lastReverted, "double voting accured";
 }
 
diff --git a/contracts/governance/Governor.sol b/contracts/governance/Governor.sol
index f8bbb42c4..e8d369452 100644
--- a/contracts/governance/Governor.sol
+++ b/contracts/governance/Governor.sol
@@ -320,7 +320,7 @@ abstract contract Governor is Context, ERC165, EIP712, IGovernor {
             v,
             r,
             s
-        );
+        ); // mention that we assume that hashing works correctly
         return _castVote(proposalId, voter, support, "");
     }
 
diff --git a/contracts/governance/TimelockController.sol b/contracts/governance/TimelockController.sol
index affcbbdc6..b3b551dde 100644
--- a/contracts/governance/TimelockController.sol
+++ b/contracts/governance/TimelockController.sol
@@ -299,6 +299,7 @@ contract TimelockController is AccessControl {
             _call(id, i, targets[i], values[i], datas[i]);
         }
         _afterCall(id);
+        // ASSUME THAT THERE IS NO REENTRANCY IN WIZARDHARNESS1
     }
 
     /**
diff --git a/contracts/governance/extensions/GovernorTimelockControl.sol b/contracts/governance/extensions/GovernorTimelockControl.sol
index b75879b19..892ec3a55 100644
--- a/contracts/governance/extensions/GovernorTimelockControl.sol
+++ b/contracts/governance/extensions/GovernorTimelockControl.sol
@@ -92,8 +92,7 @@ abstract contract GovernorTimelockControl is IGovernorTimelock, Governor {
 
         uint256 delay = _timelock.getMinDelay();
         _timelockIds[proposalId] = _timelock.hashOperationBatch(targets, values, calldatas, 0, descriptionHash);
-        // HARNESS
-        //_timelock.scheduleBatch(targets, values, calldatas, 0, descriptionHash, delay);
+        _timelock.scheduleBatch(targets, values, calldatas, 0, descriptionHash, delay);
 
         emit ProposalQueued(proposalId, block.timestamp + delay);
 
@@ -110,8 +109,7 @@ abstract contract GovernorTimelockControl is IGovernorTimelock, Governor {
         bytes[] memory calldatas,
         bytes32 descriptionHash
     ) internal virtual override {
-        // HARNESS
-        // _timelock.executeBatch{value: msg.value}(targets, values, calldatas, 0, descriptionHash);
+         _timelock.executeBatch{value: msg.value}(targets, values, calldatas, 0, descriptionHash);
     }
 
     /**