removedHarnessesAnsSummariesAddedComments

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
+    //scheduleBatch(address[],uint256[],bytes[],bytes32,bytes32,uint256) => DISPATCHER(true)
-    executeBatch(address[], uint256[], bytes[], bytes32, bytes32) => NONDET
+    //executeBatch(address[], uint256[], bytes[], bytes32, bytes32) => DISPATCHER(true)
 }
 
 //////////////////////////////////////////////////////////////////////////////
@@ -192,7 +192,6 @@ rule doubleVoting(uint256 pId, uint8 sup, method f) filtered { f-> f.selector ==
         f@withrevert(e, args);
     }
     
-
     assert votedCheck => lastReverted, "double voting accured";
 }
 

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, "");
     }
 

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
     }
 
     /**

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);
     }
 
     /**