From 4242fdace40ae239610bfa0853053aac0ba81e39 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Mon, 27 Feb 2023 16:19:18 +0100 Subject: [PATCH] isOperationReady envfree --- certora/specs/TimelockController.spec | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/certora/specs/TimelockController.spec b/certora/specs/TimelockController.spec index b2595d76b..87e0798a5 100644 --- a/certora/specs/TimelockController.spec +++ b/certora/specs/TimelockController.spec @@ -54,7 +54,7 @@ filtered { f -> !f.isView } // STATUS - verified // `isOperationReady()` correctness check invariant readyCheck(env e, bytes32 id) - (e.block.timestamp >= getTimestamp(id) && getTimestamp(id) > 1) <=> isOperationReady(e, id) + (e.block.timestamp >= getTimestamp(id) && getTimestamp(id) > 1) <=> isOperationReady(id) filtered { f -> !f.isView } // STATUS - verified @@ -109,7 +109,7 @@ rule unsetPendingTransitionMethods(method f, env e){ rule readyDoneTransition(method f, env e){ bytes32 id; - require isOperationReady(e, id); + require isOperationReady(id); calldataarg args; f(e, args); @@ -189,7 +189,7 @@ rule cannotCallExecute(method f, env e){ bytes32 id; hashIdCorrelation(id, target, value, data, predecessor, salt); - require isOperationPending(id) && !isOperationReady(e, id); + require isOperationPending(id) && !isOperationReady(id); execute@withrevert(e, target, value, data, predecessor, salt); @@ -219,12 +219,12 @@ rule executeRevertsEffectCheck(method f, env e){ bytes32 id; hashIdCorrelation(id, target, value, data, predecessor, salt); - require isOperationPending(id) && !isOperationReady(e, id); + require isOperationPending(id) && !isOperationReady(id); execute@withrevert(e, target, value, data, predecessor, salt); bool reverted = lastReverted; - assert lastReverted => isOperationPending(id) && !isOperationReady(e, id), "you go against execution nature"; + assert lastReverted => isOperationPending(id) && !isOperationReady(id), "you go against execution nature"; } @@ -278,7 +278,7 @@ rule cooldown(method f, env e, env e2){ calldataarg args; f(e, args); - assert isOperationReady(e2, id) => (e2.block.timestamp - e.block.timestamp >= minDelay), "No rush! When I'm ready, I'm ready"; + assert isOperationReady(id) => (e2.block.timestamp - e.block.timestamp >= minDelay), "No rush! When I'm ready, I'm ready"; }