From b671f84c04d7eec07281326eb9152328b69004d3 Mon Sep 17 00:00:00 2001 From: ernestognw Date: Mon, 14 Aug 2023 22:14:39 -0600 Subject: [PATCH] Finish TimelockController --- certora/specs/TimelockController.spec | 68 +++++++++++++-------------- 1 file changed, 34 insertions(+), 34 deletions(-) diff --git a/certora/specs/TimelockController.spec b/certora/specs/TimelockController.spec index d40ebda84..5123768da 100644 --- a/certora/specs/TimelockController.spec +++ b/certora/specs/TimelockController.spec @@ -2,13 +2,13 @@ import "helpers/helpers.spec"; import "methods/IAccessControl.spec"; methods { - function PROPOSER_ROLE() returns (bytes32) envfree - function EXECUTOR_ROLE() returns (bytes32) envfree - function CANCELLER_ROLE() returns (bytes32) envfree - function isOperation(bytes32) external returns (bool) envfree; - function isOperationPending(bytes32) external returns (bool) envfree; + function PROPOSER_ROLE() external returns (bytes32) envfree; + function EXECUTOR_ROLE() external returns (bytes32) envfree; + function CANCELLER_ROLE() external returns (bytes32) envfree; + function isOperation(bytes32) external returns (bool); + function isOperationPending(bytes32) external returns (bool); function isOperationReady(bytes32) external returns (bool); - function isOperationDone(bytes32) external returns (bool) envfree; + function isOperationDone(bytes32) external returns (bool); function getTimestamp(bytes32) external returns (uint256) envfree; function getMinDelay() external returns (uint256) envfree; @@ -71,30 +71,30 @@ definition UNSET() returns uint8 = 0x1; definition PENDING() returns uint8 = 0x2; definition DONE() returns uint8 = 0x4; -definition isUnset(bytes32 id) returns bool = !isOperation(id); -definition isPending(bytes32 id) returns bool = isOperationPending(id); -definition isDone(bytes32 id) returns bool = isOperationDone(id); -definition state(bytes32 id) returns uint8 = (isUnset(id) ? UNSET() : 0) | (isPending(id) ? PENDING() : 0) | (isDone(id) ? DONE() : 0); +definition isUnset(env e, bytes32 id) returns bool = !isOperation(e, id); +definition isPending(env e, bytes32 id) returns bool = isOperationPending(e, id); +definition isDone(env e, bytes32 id) returns bool = isOperationDone(e, id); +definition state(env e, bytes32 id) returns uint8 = (isUnset(e, id) ? UNSET() : 0) | (isPending(e, id) ? PENDING() : 0) | (isDone(e, id) ? DONE() : 0); /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Invariants: consistency of accessors │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -invariant isOperationCheck(bytes32 id) - isOperation(id) <=> getTimestamp(id) > 0 +invariant isOperationCheck(env e, bytes32 id) + isOperation(e, id) <=> getTimestamp(id) > 0 filtered { f -> !f.isView } -invariant isOperationPendingCheck(bytes32 id) - isOperationPending(id) <=> getTimestamp(id) > DONE_TIMESTAMP() +invariant isOperationPendingCheck(env e, bytes32 id) + isOperationPending(e, id) <=> getTimestamp(id) > DONE_TIMESTAMP() filtered { f -> !f.isView } -invariant isOperationDoneCheck(bytes32 id) - isOperationDone(id) <=> getTimestamp(id) == DONE_TIMESTAMP() +invariant isOperationDoneCheck(env e, bytes32 id) + isOperationDone(e, id) <=> getTimestamp(id) == DONE_TIMESTAMP() filtered { f -> !f.isView } invariant isOperationReadyCheck(env e, bytes32 id) - isOperationReady(e, id) <=> (isOperationPending(id) && getTimestamp(id) <= e.block.timestamp) + isOperationReady(e, id) <=> (isOperationPending(e, id) && getTimestamp(id) <= e.block.timestamp) filtered { f -> !f.isView } /* @@ -104,15 +104,15 @@ invariant isOperationReadyCheck(env e, bytes32 id) */ invariant stateConsistency(bytes32 id, env e) // Check states are mutually exclusive - (isUnset(id) <=> (!isPending(id) && !isDone(id) )) && - (isPending(id) <=> (!isUnset(id) && !isDone(id) )) && - (isDone(id) <=> (!isUnset(id) && !isPending(id))) && + (isUnset(e, id) <=> (!isPending(e, id) && !isDone(e, id) )) && + (isPending(e, id) <=> (!isUnset(e, id) && !isDone(e, id) )) && + (isDone(e, id) <=> (!isUnset(e, id) && !isPending(e, id))) && // Check that the state helper behaves as expected: - (isUnset(id) <=> state(id) == UNSET() ) && - (isPending(id) <=> state(id) == PENDING() ) && - (isDone(id) <=> state(id) == DONE() ) && + (isUnset(e, id) <=> state(e, id) == UNSET() ) && + (isPending(e, id) <=> state(e, id) == PENDING() ) && + (isDone(e, id) <=> state(e, id) == DONE() ) && // Check substate - isOperationReady(e, id) => isPending(id) + isOperationReady(e, id) => isPending(e, id) filtered { f -> !f.isView } /* @@ -123,9 +123,9 @@ invariant stateConsistency(bytes32 id, env e) rule stateTransition(bytes32 id, env e, method f, calldataarg args) { require e.block.timestamp > 1; // Sanity - uint8 stateBefore = state(id); + uint8 stateBefore = state(e, id); f(e, args); - uint8 stateAfter = state(id); + uint8 stateAfter = state(e, id); // Cannot jump from UNSET to DONE assert stateBefore == UNSET() => stateAfter != DONE(); @@ -183,7 +183,7 @@ rule schedule(env e, method f, bytes32 id, uint256 delay) filtered { f -> bytes32 otherId; uint256 otherTimestamp = getTimestamp(otherId); - uint8 stateBefore = state(id); + uint8 stateBefore = state(e, id); bool isDelaySufficient = delay >= getMinDelay(); bool isProposerBefore = hasRole(PROPOSER_ROLE(), e.msg.sender); @@ -198,8 +198,8 @@ rule schedule(env e, method f, bytes32 id, uint256 delay) filtered { f -> ); // effect - assert success => state(id) == PENDING(), "State transition violation"; - assert success => getTimestamp(id) == to_uint256(e.block.timestamp + delay), "Proposal timestamp not correctly set"; + assert success => state(e, id) == PENDING(), "State transition violation"; + assert success => getTimestamp(id) == require_uint256(e.block.timestamp + delay), "Proposal timestamp not correctly set"; // no side effect assert otherTimestamp != getTimestamp(otherId) => id == otherId, "Other proposal affected"; @@ -216,10 +216,10 @@ rule execute(env e, method f, bytes32 id, bytes32 predecessor) filtered { f -> } { bytes32 otherId; uint256 otherTimestamp = getTimestamp(otherId); - uint8 stateBefore = state(id); + uint8 stateBefore = state(e, id); bool isOperationReadyBefore = isOperationReady(e, id); bool isExecutorOrOpen = hasRole(EXECUTOR_ROLE(), e.msg.sender) || hasRole(EXECUTOR_ROLE(), 0); - bool predecessorDependency = predecessor == 0 || isDone(predecessor); + bool predecessorDependency = predecessor == to_bytes32(0) || isDone(e, predecessor); helperExecuteWithRevert(e, f, id, predecessor); bool success = !lastReverted; @@ -238,7 +238,7 @@ rule execute(env e, method f, bytes32 id, bytes32 predecessor) filtered { f -> ); // effect - assert success => state(id) == DONE(), "State transition violation"; + assert success => state(e, id) == DONE(), "State transition violation"; // no side effect assert otherTimestamp != getTimestamp(otherId) => id == otherId, "Other proposal affected"; @@ -254,7 +254,7 @@ rule cancel(env e, bytes32 id) { bytes32 otherId; uint256 otherTimestamp = getTimestamp(otherId); - uint8 stateBefore = state(id); + uint8 stateBefore = state(e, id); bool isCanceller = hasRole(CANCELLER_ROLE(), e.msg.sender); cancel@withrevert(e, id); @@ -267,7 +267,7 @@ rule cancel(env e, bytes32 id) { ); // effect - assert success => state(id) == UNSET(), "State transition violation"; + assert success => state(e, id) == UNSET(), "State transition violation"; // no side effect assert otherTimestamp != getTimestamp(otherId) => id == otherId, "Other proposal affected";