Timelock hash bug, example for Alex

3 years ago · 8d9ab176d7
parent 62d60a5890
commit 8d9ab176d7
2 changed files with 3 additions and 2 deletions
--- a/certora/munged/governance/TimelockController.sol
+++ b/certora/munged/governance/TimelockController.sol
@ -357,6 +357,7 @@ contract TimelockController is AccessControl {


    function scheduleCheck1(bytes32 id) public virtual onlyRole(PROPOSER_ROLE) {
-        require(false);
+        bool tmp = false;
+        require(tmp);
    }
 } 
--- a/certora/specs/TimelockController.spec
+++ b/certora/specs/TimelockController.spec
@ -249,7 +249,7 @@ rule executeRevertFromUnset(method f, env e, env e2){

    // hashIdCorrelation(id, target, value, data, predecessor, salt);
    require data.length < 4;
-    require hashOperation(target, value, data, predecessor, salt) == id;
+    // require hashOperation(target, value, data, predecessor, salt) == id;
    require unset(id);

    scheduleCheck1@withrevert(e, id);