run prettier --write

certora/harnesses/AccessControlHarness.sol

@@ -5,6 +5,4 @@ pragma solidity ^0.8.0;
 
 import "../munged/access/AccessControl.sol";
 
-contract AccessControlHarness is AccessControl {
-    
-}
+contract AccessControlHarness is AccessControl {}

certora/harnesses/ERC1155/ERC1155BurnableHarness.sol

@@ -1,8 +1,5 @@
 import "../../munged/token/ERC1155/extensions/ERC1155Burnable.sol";
 
 contract ERC1155BurnableHarness is ERC1155Burnable {
-    constructor(string memory uri_)
-        ERC1155(uri_)
-    {}
+    constructor(string memory uri_) ERC1155(uri_) {}
 }
-

certora/harnesses/ERC1155/ERC1155Harness.sol

@@ -3,14 +3,16 @@ pragma solidity ^0.8.2;
 import "../../munged/token/ERC1155/ERC1155.sol";
 
 contract ERC1155Harness is ERC1155 {
+    constructor(string memory uri_) ERC1155(uri_) {}
 
-    constructor(string memory uri_)
-        ERC1155(uri_)
-    {}
-
-    function burn( address from, uint256 id, uint256 amount) public virtual {
+    function burn(
+        address from,
+        uint256 id,
+        uint256 amount
+    ) public virtual {
         _burn(from, id, amount);
     }
+
     function burnBatch(
         address from,
         uint256[] memory ids,
@@ -33,7 +35,7 @@ contract ERC1155Harness is ERC1155 {
         uint256[] memory ids,
         uint256[] memory amounts,
         bytes memory data
-    ) public virtual { 
+    ) public virtual {
         _mintBatch(to, ids, amounts, data);
     }
-}
+}

certora/harnesses/ERC1155/ERC1155PausableHarness.sol

@@ -1,9 +1,7 @@
 import "../../munged/token/ERC1155/extensions/ERC1155Pausable.sol";
 
 contract ERC1155PausableHarness is ERC1155Pausable {
-    constructor(string memory uri_)
-        ERC1155(uri_)
-    {}
+    constructor(string memory uri_) ERC1155(uri_) {}
 
     function pause() public {
         _pause();
@@ -13,10 +11,7 @@ contract ERC1155PausableHarness is ERC1155Pausable {
         _unpause();
     }
 
-    function onlyWhenPausedMethod() public whenPaused {
-    }
+    function onlyWhenPausedMethod() public whenPaused {}
 
-    function onlyWhenNotPausedMethod() public whenNotPaused {
-    }
+    function onlyWhenNotPausedMethod() public whenNotPaused {}
 }
-

certora/harnesses/ERC1155/ERC1155SupplyHarness.sol

@@ -1,8 +1,8 @@
 import "../../munged/token/ERC1155/extensions/ERC1155Supply.sol";
 
-
 contract ERC1155SupplyHarness is ERC1155Supply {
     address public owner;
+
     constructor(string memory uri_) ERC1155(uri_) {
         owner = msg.sender;
     }
@@ -12,19 +12,24 @@ contract ERC1155SupplyHarness is ERC1155Supply {
         return exists(id);
     }
 
-    // These rules were not implemented in the base but there are changes in supply 
-    // that are affected by the internal contracts so we implemented them. We assume 
-    // only the owner can call any of these functions to be able to test them but also 
+    // These rules were not implemented in the base but there are changes in supply
+    // that are affected by the internal contracts so we implemented them. We assume
+    // only the owner can call any of these functions to be able to test them but also
     // limit false positives.
 
-    modifier onlyOwner {
+    modifier onlyOwner() {
         require(msg.sender == owner);
         _;
     }
 
-    function burn( address from, uint256 id, uint256 amount) public virtual onlyOwner {
+    function burn(
+        address from,
+        uint256 id,
+        uint256 amount
+    ) public virtual onlyOwner {
         _burn(from, id, amount);
     }
+
     function burnBatch(
         address from,
         uint256[] memory ids,
@@ -47,7 +52,7 @@ contract ERC1155SupplyHarness is ERC1155Supply {
         uint256[] memory ids,
         uint256[] memory amounts,
         bytes memory data
-    ) public virtual onlyOwner { 
+    ) public virtual onlyOwner {
         _mintBatch(to, ids, amounts, data);
     }
 
@@ -58,4 +63,3 @@ contract ERC1155SupplyHarness is ERC1155Supply {
         return _balances[id][account];
     }
 }
-

certora/harnesses/ERC20PermitHarness.sol

@@ -1,9 +1,5 @@
 import "../munged/token/ERC20/extensions/draft-ERC20Permit.sol";
 
 contract ERC20PermitHarness is ERC20Permit {
-    constructor(string memory _name, string memory _symbol)
-        ERC20(_name, _symbol)
-        ERC20Permit(_name)
-    {}
+    constructor(string memory _name, string memory _symbol) ERC20(_name, _symbol) ERC20Permit(_name) {}
 }
-

certora/harnesses/ERC20VotesHarness.sol

@@ -6,7 +6,7 @@ contract ERC20VotesHarness is ERC20Votes {
     function ckptFromBlock(address account, uint32 pos) public view returns (uint32) {
         return _checkpoints[account][pos].fromBlock;
     }
-    
+
     function ckptVotes(address account, uint32 pos) public view returns (uint224) {
         return _checkpoints[account][pos].fromBlock;
     }
@@ -30,7 +30,5 @@ contract ERC20VotesHarness is ERC20Votes {
         uint8 v,
         bytes32 r,
         bytes32 s
-    ) public virtual override { }
-
+    ) public virtual override {}
 }
-

certora/harnesses/ERC20WrapperHarness.sol

@@ -1,11 +1,11 @@
 import "../munged/token/ERC20/extensions/ERC20Wrapper.sol";
 
 contract ERC20WrapperHarness is ERC20Wrapper {
-
-    constructor(IERC20 underlyingToken, string memory _name, string memory _symbol)
-        ERC20Wrapper(underlyingToken)
-        ERC20(_name, _symbol)
-    {}
+    constructor(
+        IERC20 underlyingToken,
+        string memory _name,
+        string memory _symbol
+    ) ERC20Wrapper(underlyingToken) ERC20(_name, _symbol) {}
 
     function underlyingTotalSupply() public view returns (uint256) {
         return underlying.totalSupply();
@@ -14,4 +14,4 @@ contract ERC20WrapperHarness is ERC20Wrapper {
     function underlyingBalanceOf(address account) public view returns (uint256) {
         return underlying.balanceOf(account);
     }
-}
+}

certora/harnesses/ERC721VotesHarness.sol

@@ -3,7 +3,7 @@ pragma solidity ^0.8.0;
 import "../munged/token/ERC721/extensions/draft-ERC721Votes.sol";
 
 contract ERC721VotesHarness is ERC721Votes {
-    constructor(string memory name, string memory symbol) ERC721(name, symbol) EIP712(name, symbol){}
+    constructor(string memory name, string memory symbol) ERC721(name, symbol) EIP712(name, symbol) {}
 
     function delegateBySig(
         address delegatee,
@@ -23,4 +23,4 @@ contract ERC721VotesHarness is ERC721Votes {
     function burn(uint256 tokenID) public {
         _burn(tokenID);
     }
-}
+}

certora/harnesses/GovernorPreventLateQuorumHarness.sol

@@ -9,10 +9,23 @@ import "../munged/governance/extensions/GovernorVotesQuorumFraction.sol";
 import "../munged/governance/extensions/GovernorTimelockControl.sol";
 import "../munged/token/ERC20/extensions/ERC20Votes.sol";
 
-contract GovernorPreventLateQuorumHarness is Governor, GovernorCountingSimple, GovernorVotes, GovernorVotesQuorumFraction, GovernorTimelockControl, GovernorPreventLateQuorum {
+contract GovernorPreventLateQuorumHarness is
+    Governor,
+    GovernorCountingSimple,
+    GovernorVotes,
+    GovernorVotesQuorumFraction,
+    GovernorTimelockControl,
+    GovernorPreventLateQuorum
+{
     using SafeCast for uint256;
     using Timers for Timers.BlockNumber;
-    constructor(IVotes _token, TimelockController _timelock, uint64 initialVoteExtension, uint256 quorumNumeratorValue)
+
+    constructor(
+        IVotes _token,
+        TimelockController _timelock,
+        uint64 initialVoteExtension,
+        uint256 quorumNumeratorValue
+    )
         Governor("Harness")
         GovernorVotes(_token)
         GovernorVotesQuorumFraction(quorumNumeratorValue)
@@ -26,65 +39,71 @@ contract GovernorPreventLateQuorumHarness is Governor, GovernorCountingSimple, G
     uint256 public latestCastVoteCall;
 
     // Harness from GovernorPreventLateQuorum //
-    
-    function getVoteExtension() public view returns(uint64) {
+
+    function getVoteExtension() public view returns (uint64) {
         return _voteExtension;
     }
 
-    function getExtendedDeadlineIsUnset(uint256 proposalId) public view returns(bool) {
+    function getExtendedDeadlineIsUnset(uint256 proposalId) public view returns (bool) {
         return _extendedDeadlines[proposalId].isUnset();
     }
 
-    function getExtendedDeadlineIsStarted(uint256 proposalId) public view returns(bool) {
+    function getExtendedDeadlineIsStarted(uint256 proposalId) public view returns (bool) {
         return _extendedDeadlines[proposalId].isStarted();
     }
 
-    function getExtendedDeadline(uint256 proposalId) public view returns(uint64) {
+    function getExtendedDeadline(uint256 proposalId) public view returns (uint64) {
         return _extendedDeadlines[proposalId].getDeadline();
     }
 
-    // Harness from GovernorCountingSimple // 
+    // Harness from GovernorCountingSimple //
 
-    function getAgainstVotes(uint256 proposalId) public view returns(uint256) {
+    function getAgainstVotes(uint256 proposalId) public view returns (uint256) {
         ProposalVote storage proposalvote = _proposalVotes[proposalId];
         return proposalvote.againstVotes;
     }
 
-    function getAbstainVotes(uint256 proposalId) public view returns(uint256) {
+    function getAbstainVotes(uint256 proposalId) public view returns (uint256) {
         ProposalVote storage proposalvote = _proposalVotes[proposalId];
         return proposalvote.abstainVotes;
     }
 
-    function getForVotes(uint256 proposalId) public view returns(uint256) {
+    function getForVotes(uint256 proposalId) public view returns (uint256) {
         ProposalVote storage proposalvote = _proposalVotes[proposalId];
         return proposalvote.forVotes;
     }
-    
-    function quorumReached(uint256 proposalId) public view returns(bool) {
+
+    function quorumReached(uint256 proposalId) public view returns (bool) {
         return _quorumReached(proposalId);
     }
 
-    function voteSucceeded(uint256 proposalId) public view returns(bool) {
+    function voteSucceeded(uint256 proposalId) public view returns (bool) {
         return _voteSucceeded(proposalId);
     }
 
     // Harness from Governor //
 
-    function getExecutor() public view returns (address){
+    function getExecutor() public view returns (address) {
         return _executor();
     }
 
     function isExecuted(uint256 proposalId) public view returns (bool) {
         return _proposals[proposalId].executed;
     }
-    
+
     function isCanceled(uint256 proposalId) public view returns (bool) {
         return _proposals[proposalId].canceled;
     }
 
     // The following functions are overrides required by Solidity added by Certora. //
 
-    function proposalDeadline(uint256 proposalId) public view virtual override(Governor, GovernorPreventLateQuorum, IGovernor) returns (uint256) {
+    function proposalDeadline(uint256 proposalId)
+        public
+        view
+        virtual
+        override(Governor, GovernorPreventLateQuorum, IGovernor)
+        returns (uint256)
+    {
         return super.proposalDeadline(proposalId);
     }
 
@@ -100,7 +119,7 @@ contract GovernorPreventLateQuorumHarness is Governor, GovernorCountingSimple, G
 
         // added to run GovernorCountingSimple.spec
         uint256 deltaWeight = super._castVote(proposalId, account, support, reason, params);
-        ghost_sum_vote_power_by_id[proposalId] += deltaWeight; 
+        ghost_sum_vote_power_by_id[proposalId] += deltaWeight;
 
         return deltaWeight;
     }
@@ -132,44 +151,39 @@ contract GovernorPreventLateQuorumHarness is Governor, GovernorCountingSimple, G
         return super.quorum(blockNumber);
     }
 
-    function state(uint256 proposalId)
-        public
-        view
-        override(Governor, GovernorTimelockControl)
-        returns (ProposalState)
-    {
+    function state(uint256 proposalId) public view override(Governor, GovernorTimelockControl) returns (ProposalState) {
         return super.state(proposalId);
     }
 
-    function propose(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, string memory description)
-        public
-        override(Governor, IGovernor)
-        returns (uint256)
-    {
+    function propose(
+        address[] memory targets,
+        uint256[] memory values,
+        bytes[] memory calldatas,
+        string memory description
+    ) public override(Governor, IGovernor) returns (uint256) {
         return super.propose(targets, values, calldatas, description);
     }
 
-    function _execute(uint256 proposalId, address[] memory targets, uint256[] memory values, bytes[] memory calldatas, bytes32 descriptionHash)
-        internal
-        override(Governor, GovernorTimelockControl)
-    {
+    function _execute(
+        uint256 proposalId,
+        address[] memory targets,
+        uint256[] memory values,
+        bytes[] memory calldatas,
+        bytes32 descriptionHash
+    ) internal override(Governor, GovernorTimelockControl) {
         super._execute(proposalId, targets, values, calldatas, descriptionHash);
     }
 
-    function _cancel(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, bytes32 descriptionHash)
-        internal
-        override(Governor, GovernorTimelockControl)
-        returns (uint256)
-    {
+    function _cancel(
+        address[] memory targets,
+        uint256[] memory values,
+        bytes[] memory calldatas,
+        bytes32 descriptionHash
+    ) internal override(Governor, GovernorTimelockControl) returns (uint256) {
         return super._cancel(targets, values, calldatas, descriptionHash);
     }
 
-    function _executor()
-        internal
-        view
-        override(Governor, GovernorTimelockControl)
-        returns (address)
-    {
+    function _executor() internal view override(Governor, GovernorTimelockControl) returns (address) {
         return super._executor();
     }
 
@@ -181,4 +195,4 @@ contract GovernorPreventLateQuorumHarness is Governor, GovernorCountingSimple, G
     {
         return super.supportsInterface(interfaceId);
     }
-}
+}

certora/harnesses/IERC3156FlashBorrowerHarness.sol

@@ -14,7 +14,7 @@ contract IERC3156FlashBorrowerHarness is IERC3156FlashBorrower {
         uint256 amount,
         uint256 fee,
         bytes calldata data
-    ) external override returns (bytes32){
+    ) external override returns (bytes32) {
         return somethingToReturn;
     }
 }

certora/harnesses/InitializableBasicHarness.sol

@@ -4,7 +4,6 @@ pragma solidity ^0.8.2;
 import "../munged/proxy/utils/Initializable.sol";
 
 contract InitializableBasicHarness is Initializable {
-
     uint256 public val;
     uint256 public a;
     uint256 public b;
@@ -19,13 +18,22 @@ contract InitializableBasicHarness is Initializable {
         _;
     }
 
-    function initialize(uint256 _val, uint256 _a, uint256 _b) public initializer {
+    function initialize(
+        uint256 _val,
+        uint256 _a,
+        uint256 _b
+    ) public initializer {
         a = _a;
         b = _b;
         val = _val;
     }
 
-    function reinitialize(uint256 _val, uint256 _a, uint256 _b, uint8 n) public reinitializer(n) {
+    function reinitialize(
+        uint256 _val,
+        uint256 _a,
+        uint256 _b,
+        uint8 n
+    ) public reinitializer(n) {
         a = _a;
         b = _b;
         val = _val;
@@ -33,41 +41,40 @@ contract InitializableBasicHarness is Initializable {
 
     // Versioned return functions for testing
 
-    function returnsV1() public view version1 returns(uint256) {
+    function returnsV1() public view version1 returns (uint256) {
         return val;
     }
 
-    function returnsVN(uint8 n) public view versionN(n) returns(uint256) {
+    function returnsVN(uint8 n) public view versionN(n) returns (uint256) {
         return val;
     }
-    
-    function returnsAV1() public view version1 returns(uint256) {
+
+    function returnsAV1() public view version1 returns (uint256) {
         return a;
     }
 
-    function returnsAVN(uint8 n) public view versionN(n) returns(uint256) {
+    function returnsAVN(uint8 n) public view versionN(n) returns (uint256) {
         return a;
     }
 
-    function returnsBV1() public view version1 returns(uint256) {
+    function returnsBV1() public view version1 returns (uint256) {
         return b;
     }
 
-    function returnsBVN(uint8 n) public view versionN(n) returns(uint256) {
+    function returnsBVN(uint8 n) public view versionN(n) returns (uint256) {
         return b;
     }
 
     // Harness //
-    function initialized() public view returns(uint8) {
+    function initialized() public view returns (uint8) {
         return _initialized;
     }
 
-    function initializing() public view returns(bool) {
+    function initializing() public view returns (bool) {
         return _initializing;
     }
 
-    function thisIsContract() public view returns(bool) {
+    function thisIsContract() public view returns (bool) {
         return !Address.isContract(address(this));
     }
-    
 }

certora/harnesses/InitializableComplexHarness.sol

@@ -5,7 +5,7 @@ import "../munged/proxy/utils/Initializable.sol";
 
 contract InitializableA is Initializable {
     uint256 public a;
-    
+
     modifier version1() {
         require(_initialized == 1);
         _;
@@ -15,30 +15,32 @@ contract InitializableA is Initializable {
         require(_initialized == n);
         _;
     }
+
     function __InitializableA_init(uint256 _a) internal onlyInitializing {
         a = _a;
     }
-    
-    function returnsAV1() public view version1 returns(uint256) {
+
+    function returnsAV1() public view version1 returns (uint256) {
         return a;
     }
 
-    function returnsAVN(uint8 n) public view versionN(n) returns(uint256) {
+    function returnsAVN(uint8 n) public view versionN(n) returns (uint256) {
         return a;
     }
 }
 
 contract InitializableB is Initializable, InitializableA {
     uint256 public b;
+
     function __InitializableB_init(uint256 _b) internal onlyInitializing {
         b = _b;
     }
 
-    function returnsBV1() public view version1 returns(uint256) {
+    function returnsBV1() public view version1 returns (uint256) {
         return b;
     }
 
-    function returnsBVN(uint8 n) public view versionN(n) returns(uint256) {
+    function returnsBVN(uint8 n) public view versionN(n) returns (uint256) {
         return b;
     }
 }
@@ -46,36 +48,45 @@ contract InitializableB is Initializable, InitializableA {
 contract InitializableComplexHarness is Initializable, InitializableB {
     uint256 public val;
 
-    function initialize(uint256 _val, uint256 _a, uint256 _b) initializer public {
+    function initialize(
+        uint256 _val,
+        uint256 _a,
+        uint256 _b
+    ) public initializer {
         val = _val;
         __InitializableA_init(_a);
         __InitializableB_init(_b);
     }
 
-    function reinitialize(uint256 _val, uint256 _a, uint256 _b, uint8 n) reinitializer(n) public {
+    function reinitialize(
+        uint256 _val,
+        uint256 _a,
+        uint256 _b,
+        uint8 n
+    ) public reinitializer(n) {
         val = _val;
         __InitializableA_init(_a);
         __InitializableB_init(_b);
     }
 
-    function returnsV1() public view version1 returns(uint256) {
+    function returnsV1() public view version1 returns (uint256) {
         return val;
     }
 
-    function returnsVN(uint8 n) public view versionN(n) returns(uint256) {
+    function returnsVN(uint8 n) public view versionN(n) returns (uint256) {
         return val;
     }
 
     // Harness //
-    function initialized() public view returns(uint8) {
+    function initialized() public view returns (uint8) {
         return _initialized;
     }
 
-    function initializing() public view returns(bool) {
+    function initializing() public view returns (bool) {
         return _initializing;
     }
 
-    function thisIsContract() public view returns(bool) {
+    function thisIsContract() public view returns (bool) {
         return !Address.isContract(address(this));
     }
 }

certora/harnesses/TimelockControllerHarness.sol

@@ -2,12 +2,10 @@ pragma solidity ^0.8.0;
 
 import "../munged/governance/TimelockController.sol";
 
- contract TimelockControllerHarness is TimelockController {
-     constructor(
+contract TimelockControllerHarness is TimelockController {
+    constructor(
         uint256 minDelay,
         address[] memory proposers,
         address[] memory executors
-     ) TimelockController(minDelay, proposers, executors) {
-
-     }
-}
+    ) TimelockController(minDelay, proposers, executors) {}
+}

certora/harnesses/WizardControlFirstPriority.sol

@@ -16,8 +16,20 @@ ERC20Votes
 TimelockController
 */
 
-contract WizardControlFirstPriority is Governor, GovernorProposalThreshold, GovernorCountingSimple, GovernorVotes, GovernorVotesQuorumFraction, GovernorTimelockControl {
-    constructor(ERC20Votes _token, TimelockController _timelock, string memory name, uint256 quorumFraction)
+contract WizardControlFirstPriority is
+    Governor,
+    GovernorProposalThreshold,
+    GovernorCountingSimple,
+    GovernorVotes,
+    GovernorVotesQuorumFraction,
+    GovernorTimelockControl
+{
+    constructor(
+        ERC20Votes _token,
+        TimelockController _timelock,
+        string memory name,
+        uint256 quorumFraction
+    )
         Governor(name)
         GovernorVotes(_token)
         GovernorVotesQuorumFraction(quorumFraction)
@@ -29,7 +41,7 @@ contract WizardControlFirstPriority is Governor, GovernorProposalThreshold, Gove
     function isExecuted(uint256 proposalId) public view returns (bool) {
         return _proposals[proposalId].executed;
     }
-    
+
     function isCanceled(uint256 proposalId) public view returns (bool) {
         return _proposals[proposalId].canceled;
     }
@@ -47,35 +59,36 @@ contract WizardControlFirstPriority is Governor, GovernorProposalThreshold, Gove
         address account,
         uint8 support,
         string memory reason
-    ) internal override virtual returns (uint256) {
-        
-        uint256 deltaWeight = super._castVote(proposalId, account, support, reason);  //HARNESS
+    ) internal virtual override returns (uint256) {
+        uint256 deltaWeight = super._castVote(proposalId, account, support, reason); //HARNESS
         ghost_sum_vote_power_by_id[proposalId] += deltaWeight;
 
-        return deltaWeight;        
+        return deltaWeight;
     }
-    
+
     function snapshot(uint256 proposalId) public view returns (uint64) {
         return _proposals[proposalId].voteStart._deadline;
     }
 
-
-    function getExecutor() public view returns (address){
+    function getExecutor() public view returns (address) {
         return _executor();
     }
 
     // original code, harnessed
 
-    function votingDelay() public view override returns (uint256) {     // HARNESS: pure -> view
-        return _votingDelay;                                            // HARNESS: parametric
+    function votingDelay() public view override returns (uint256) {
+        // HARNESS: pure -> view
+        return _votingDelay; // HARNESS: parametric
     }
 
-    function votingPeriod() public view override returns (uint256) {    // HARNESS: pure -> view
-        return _votingPeriod;                                           // HARNESS: parametric
+    function votingPeriod() public view override returns (uint256) {
+        // HARNESS: pure -> view
+        return _votingPeriod; // HARNESS: parametric
     }
 
-    function proposalThreshold() public view override returns (uint256) {   // HARNESS: pure -> view
-        return _proposalThreshold;                                          // HARNESS: parametric
+    function proposalThreshold() public view override returns (uint256) {
+        // HARNESS: pure -> view
+        return _proposalThreshold; // HARNESS: parametric
     }
 
     // original code, not harnessed
@@ -99,44 +112,39 @@ contract WizardControlFirstPriority is Governor, GovernorProposalThreshold, Gove
         return super.getVotes(account, blockNumber);
     }
 
-    function state(uint256 proposalId)
-        public
-        view
-        override(Governor, GovernorTimelockControl)
-        returns (ProposalState)
-    {
+    function state(uint256 proposalId) public view override(Governor, GovernorTimelockControl) returns (ProposalState) {
         return super.state(proposalId);
     }
 
-    function propose(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, string memory description)
-        public
-        override(Governor, GovernorProposalThreshold, IGovernor)
-        returns (uint256)
-    {
+    function propose(
+        address[] memory targets,
+        uint256[] memory values,
+        bytes[] memory calldatas,
+        string memory description
+    ) public override(Governor, GovernorProposalThreshold, IGovernor) returns (uint256) {
         return super.propose(targets, values, calldatas, description);
     }
 
-    function _execute(uint256 proposalId, address[] memory targets, uint256[] memory values, bytes[] memory calldatas, bytes32 descriptionHash)
-        internal
-        override(Governor, GovernorTimelockControl)
-    {
+    function _execute(
+        uint256 proposalId,
+        address[] memory targets,
+        uint256[] memory values,
+        bytes[] memory calldatas,
+        bytes32 descriptionHash
+    ) internal override(Governor, GovernorTimelockControl) {
         super._execute(proposalId, targets, values, calldatas, descriptionHash);
     }
 
-    function _cancel(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, bytes32 descriptionHash)
-        internal
-        override(Governor, GovernorTimelockControl)
-        returns (uint256)
-    {
+    function _cancel(
+        address[] memory targets,
+        uint256[] memory values,
+        bytes[] memory calldatas,
+        bytes32 descriptionHash
+    ) internal override(Governor, GovernorTimelockControl) returns (uint256) {
         return super._cancel(targets, values, calldatas, descriptionHash);
     }
 
-    function _executor()
-        internal
-        view
-        override(Governor, GovernorTimelockControl)
-        returns (address)
-    {
+    function _executor() internal view override(Governor, GovernorTimelockControl) returns (address) {
         return super._executor();
     }
 

certora/harnesses/WizardFirstTry.sol

@@ -14,8 +14,19 @@ ERC20Votes
 TimelockCompound
 */
 
-contract WizardFirstTry is Governor, GovernorCountingSimple, GovernorVotes, GovernorVotesQuorumFraction, GovernorTimelockCompound {
-    constructor(ERC20Votes _token, ICompoundTimelock _timelock, string memory name, uint256 quorumFraction)
+contract WizardFirstTry is
+    Governor,
+    GovernorCountingSimple,
+    GovernorVotes,
+    GovernorVotesQuorumFraction,
+    GovernorTimelockCompound
+{
+    constructor(
+        ERC20Votes _token,
+        ICompoundTimelock _timelock,
+        string memory name,
+        uint256 quorumFraction
+    )
         Governor(name)
         GovernorVotes(_token)
         GovernorVotesQuorumFraction(quorumFraction)
@@ -27,7 +38,7 @@ contract WizardFirstTry is Governor, GovernorCountingSimple, GovernorVotes, Gove
     function isExecuted(uint256 proposalId) public view returns (bool) {
         return _proposals[proposalId].executed;
     }
-    
+
     function isCanceled(uint256 proposalId) public view returns (bool) {
         return _proposals[proposalId].canceled;
     }
@@ -36,7 +47,7 @@ contract WizardFirstTry is Governor, GovernorCountingSimple, GovernorVotes, Gove
         return _proposals[proposalId].voteStart._deadline;
     }
 
-    function getExecutor() public view returns (address){
+    function getExecutor() public view returns (address) {
         return _executor();
     }
 
@@ -51,22 +62,23 @@ contract WizardFirstTry is Governor, GovernorCountingSimple, GovernorVotes, Gove
         address account,
         uint8 support,
         string memory reason
-    ) internal override virtual returns (uint256) {
-        
-        uint256 deltaWeight = super._castVote(proposalId, account, support, reason);  //HARNESS
+    ) internal virtual override returns (uint256) {
+        uint256 deltaWeight = super._castVote(proposalId, account, support, reason); //HARNESS
         ghost_sum_vote_power_by_id[proposalId] += deltaWeight;
 
-        return deltaWeight;        
+        return deltaWeight;
     }
 
     // original code, harnessed
 
-    function votingDelay() public view override virtual returns (uint256) {     // HARNESS: pure -> view
-        return _votingDelay;                                                    // HARNESS: parametric
+    function votingDelay() public view virtual override returns (uint256) {
+        // HARNESS: pure -> view
+        return _votingDelay; // HARNESS: parametric
     }
 
-    function votingPeriod() public view override virtual returns (uint256) {    // HARNESS: pure -> view
-        return _votingPeriod;                                                   // HARNESS: parametric
+    function votingPeriod() public view virtual override returns (uint256) {
+        // HARNESS: pure -> view
+        return _votingPeriod; // HARNESS: parametric
     }
 
     // original code, not harnessed
@@ -99,35 +111,35 @@ contract WizardFirstTry is Governor, GovernorCountingSimple, GovernorVotes, Gove
         return super.state(proposalId);
     }
 
-    function propose(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, string memory description)
-        public
-        override(Governor, IGovernor)
-        returns (uint256)
-    {
+    function propose(
+        address[] memory targets,
+        uint256[] memory values,
+        bytes[] memory calldatas,
+        string memory description
+    ) public override(Governor, IGovernor) returns (uint256) {
         return super.propose(targets, values, calldatas, description);
     }
 
-    function _execute(uint256 proposalId, address[] memory targets, uint256[] memory values, bytes[] memory calldatas, bytes32 descriptionHash)
-        internal
-        override(Governor, GovernorTimelockCompound)
-    {
+    function _execute(
+        uint256 proposalId,
+        address[] memory targets,
+        uint256[] memory values,
+        bytes[] memory calldatas,
+        bytes32 descriptionHash
+    ) internal override(Governor, GovernorTimelockCompound) {
         super._execute(proposalId, targets, values, calldatas, descriptionHash);
     }
 
-    function _cancel(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, bytes32 descriptionHash)
-        internal
-        override(Governor, GovernorTimelockCompound)
-        returns (uint256)
-    {
+    function _cancel(
+        address[] memory targets,
+        uint256[] memory values,
+        bytes[] memory calldatas,
+        bytes32 descriptionHash
+    ) internal override(Governor, GovernorTimelockCompound) returns (uint256) {
         return super._cancel(targets, values, calldatas, descriptionHash);
     }
 
-    function _executor()
-        internal
-        view
-        override(Governor, GovernorTimelockCompound)
-        returns (address)
-    {
+    function _executor() internal view override(Governor, GovernorTimelockCompound) returns (address) {
         return super._executor();
     }