erc20votes pointers workaround and preset

certora/munged/governance/TimelockController.sol

@@ -353,4 +353,4 @@ contract TimelockController is AccessControl {
         emit MinDelayChange(_minDelay, newDelay);
         _minDelay = newDelay;
     }
-}
+} 

certora/munged/token/ERC20/extensions/ERC20Votes.sol

@@ -163,7 +163,7 @@ abstract contract ERC20Votes is IVotes, ERC20Permit {
         super._mint(account, amount);
         require(totalSupply() <= _maxSupply(), "ERC20Votes: total supply risks overflowing votes");
 
-        _writeCheckpoint(_totalSupplyCheckpoints, _add, amount);
+        _writeCheckpointAdd(_totalSupplyCheckpoints, amount);           // HARNESS: new version without pointer
     }
 
     /**
@@ -172,7 +172,7 @@ abstract contract ERC20Votes is IVotes, ERC20Permit {
     function _burn(address account, uint256 amount) internal virtual override {
         super._burn(account, amount);
 
-        _writeCheckpoint(_totalSupplyCheckpoints, _subtract, amount);
+        _writeCheckpointSub(_totalSupplyCheckpoints, amount);           // HARNESS: new version without pointer
     }
 
     /**
@@ -187,7 +187,7 @@ abstract contract ERC20Votes is IVotes, ERC20Permit {
     ) internal virtual override {
         super._afterTokenTransfer(from, to, amount);
 
-        _moveVotingPower(delegates(from), delegates(to), amount);
+        _moveVotingPower(delegates(from), delegates(to), amount);       
     }
 
     /**
@@ -212,25 +212,25 @@ abstract contract ERC20Votes is IVotes, ERC20Permit {
     ) private {
         if (src != dst && amount > 0) {
             if (src != address(0)) {
-                (uint256 oldWeight, uint256 newWeight) = _writeCheckpoint(_checkpoints[src], _subtract, amount);
+                (uint256 oldWeight, uint256 newWeight) = _writeCheckpointSub(_checkpoints[src], amount);        // HARNESS: new version without pointer
                 emit DelegateVotesChanged(src, oldWeight, newWeight);
             }
 
             if (dst != address(0)) {
-                (uint256 oldWeight, uint256 newWeight) = _writeCheckpoint(_checkpoints[dst], _add, amount);
+                (uint256 oldWeight, uint256 newWeight) = _writeCheckpointAdd(_checkpoints[dst], amount);        // HARNESS: new version without pointer
                 emit DelegateVotesChanged(dst, oldWeight, newWeight);
             }
         }
     }
 
-    function _writeCheckpoint(
+    // HARNESS: split _writeCheckpoint() to two functions as a workaround for function pointers that cannot be managed by the tool
+    function _writeCheckpointAdd(
         Checkpoint[] storage ckpts,
-        function(uint256, uint256) view returns (uint256) op,
         uint256 delta
     ) private returns (uint256 oldWeight, uint256 newWeight) {
         uint256 pos = ckpts.length;
         oldWeight = pos == 0 ? 0 : ckpts[pos - 1].votes;
-        newWeight = op(oldWeight, delta);
+        newWeight = _add(oldWeight, delta);
 
         if (pos > 0 && ckpts[pos - 1].fromBlock == block.number) {
             ckpts[pos - 1].votes = SafeCast.toUint224(newWeight);
@@ -239,6 +239,39 @@ abstract contract ERC20Votes is IVotes, ERC20Permit {
         }
     }
 
+    function _writeCheckpointSub(
+        Checkpoint[] storage ckpts,
+        uint256 delta
+    ) private returns (uint256 oldWeight, uint256 newWeight) {
+        uint256 pos = ckpts.length;
+        oldWeight = pos == 0 ? 0 : ckpts[pos - 1].votes;
+        newWeight = _subtract(oldWeight, delta);
+
+        if (pos > 0 && ckpts[pos - 1].fromBlock == block.number) {
+            ckpts[pos - 1].votes = SafeCast.toUint224(newWeight);
+        } else {
+            ckpts.push(Checkpoint({fromBlock: SafeCast.toUint32(block.number), votes: SafeCast.toUint224(newWeight)}));
+        }
+    }
+
+    // backup of original function
+    //
+    // function _writeCheckpoint(
+    //     Checkpoint[] storage ckpts,
+    //     function(uint256, uint256) view returns (uint256) op,
+    //     uint256 delta
+    // ) private returns (uint256 oldWeight, uint256 newWeight) {
+    //     uint256 pos = ckpts.length;
+    //     oldWeight = pos == 0 ? 0 : ckpts[pos - 1].votes;
+    //     newWeight = op(oldWeight, delta);
+    //
+    //     if (pos > 0 && ckpts[pos - 1].fromBlock == block.number) {
+    //         ckpts[pos - 1].votes = SafeCast.toUint224(newWeight);
+    //     } else {
+    //         ckpts.push(Checkpoint({fromBlock: SafeCast.toUint32(block.number), votes: SafeCast.toUint224(newWeight)}));
+    //     }
+    // }
+
     function _add(uint256 a, uint256 b) private pure returns (uint256) {
         return a + b;
     }

certora/scripts/sanity.sh

@@ -14,22 +14,22 @@
 # done
 
 # TimelockController
-# certoraRun \
-#     certora/harnesses/TimelockControllerHarness.sol \
-#     --verify TimelockControllerHarness:certora/specs/sanity.spec \
-#     --solc solc8.2 \
-#     --optimistic_loop \
-#     --cloud \
-#     --msg "sanity"
-
-
-# Votes
 certoraRun \
-    certora/harnesses/VotesHarness.sol \
-    --verify VotesHarness:certora/specs/sanity.spec \
+    certora/harnesses/TimelockControllerHarness.sol \
+    --verify TimelockControllerHarness:certora/specs/sanity.spec \
     --solc solc8.2 \
     --optimistic_loop \
     --cloud \
-    --settings -strictDecompiler=false,-assumeUnwindCond \
-    --msg "sanityVotes"
+    --msg "sanity and keccak check"
+
+
+# Votes
+# certoraRun \
+#     certora/harnesses/VotesHarness.sol \
+#     --verify VotesHarness:certora/specs/sanity.spec \
+#     --solc solc8.2 \
+#     --optimistic_loop \
+#     --cloud \
+#     --settings -strictDecompiler=false,-assumeUnwindCond \
+#     --msg "sanityVotes"
 

certora/scripts/verifyERC20Votes.sh

@@ -0,0 +1,8 @@
+certoraRun \
+    certora/harnesses/ERC20VotesHarness.sol \
+    --verify ERC20VotesHarness:certora/specs/ERC20Votes.spec \
+    --solc solc8.2 \
+    --optimistic_loop \
+    --cloud \
+    --settings -strictDecompiler=false,-assumeUnwindCond \
+    --msg "sanityVotes"

certora/scripts/verifyTimelock.sh

@@ -0,0 +1,7 @@
+certoraRun \
+    certora/harnesses/TimelockControllerHarness.sol \
+    --verify TimelockControllerHarness:certora/specs/TimelockController.spec \
+    --solc solc8.2 \
+    --optimistic_loop \
+    --cloud \
+    --msg "sanity"

certora/specs/ERC20Votes.spec

@@ -0,0 +1,6 @@
+rule sanity(method f) {
+    env e;
+    calldataarg arg;
+    f(e, arg);
+    assert false;
+}

certora/specs/TimelockController.spec

@@ -0,0 +1,36 @@
+methods {
+    // hashOperation(address target, uint256 value, bytes data, bytes32 predecessor, bytes32 salt) returns(bytes32) => uniqueHashGhost(target, value, data, predecessor, salt)
+}
+
+// ghost uniqueHashGhost(address, uint256, bytes, bytes32, bytes32) returns bytes32;
+//
+// Assuming the hash is deterministic, and correlates the trio properly
+// function hashUniquness(address target1, uint256 value1, bytes data1, bytes32 predecessor1, bytes32 salt1, 
+//                             address target2, uint256 value2, bytes data2, bytes32 predecessor2, bytes32 salt2){
+//     require ((target1 != target2) || (value1 != value2) || (data1 != data2) || (predecessor1 != predecessor2) || (salt1 != salt2)) <=> 
+//     (uniqueHashGhost(target1, value1, data1, predecessor1, salt1) != uniqueHashGhost(target2, value2, data2, predecessor2, salt2));
+// }
+// 
+// 
+// rule keccakCheck(method f, env e){
+//     address target;
+//     uint256 value;
+//     bytes data;
+//     bytes32 predecessor;
+//     bytes32 salt;
+// 
+//     hashUniquness(target, value, data, predecessor, salt, 
+//                          target, value, data, predecessor, salt);
+// 
+//     bytes32 a = hashOperation(e, target, value, data, predecessor, salt);
+//     bytes32 b = hashOperation(e, target, value, data, predecessor, salt);
+// 
+//     assert a == b, "hashes are different";
+// }
+
+rule sanity(method f) {
+    env e;
+    calldataarg arg;
+    f(e, arg);
+    assert false;
+}

certora/specs/sanity.spec

@@ -5,7 +5,8 @@ How it works:
     - If there is a non-reverting execution path, we reach the false assertion, and the sanity fails.
     - If all execution paths are reverting, we never call the assertion, and the method will pass this rule vacuously.
 */
-	
+
+
 rule sanity(method f) {
     env e;
     calldataarg arg;