From 0df6a47e08a1389957fa4c064358d5a2c49c4578 Mon Sep 17 00:00:00 2001 From: sunbreak1211 Date: Thu, 12 Feb 2026 16:18:50 -0300 Subject: [PATCH 1/5] Certora specs: BeamState and Configurator --- .gitignore | 3 + Makefile | 3 + certora/BeamState.conf | 10 + certora/BeamState.spec | 972 ++++++++++++++++++++++++++ certora/Configurator.conf | 12 + certora/Configurator.spec | 301 ++++++++ certora/harness/RateLimitsHarness.sol | 70 ++ 7 files changed, 1371 insertions(+) create mode 100644 Makefile create mode 100644 certora/BeamState.conf create mode 100644 certora/BeamState.spec create mode 100644 certora/Configurator.conf create mode 100644 certora/Configurator.spec create mode 100644 certora/harness/RateLimitsHarness.sol diff --git a/.gitignore b/.gitignore index 85198aa..8c30259 100644 --- a/.gitignore +++ b/.gitignore @@ -12,3 +12,6 @@ docs/ # Dotenv file .env + +# Certora +.certora_internal diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..907e875 --- /dev/null +++ b/Makefile @@ -0,0 +1,3 @@ +PATH := ~/.solc-select/artifacts/solc-0.8.24:$(PATH) +certora-state :; PATH=${PATH} certoraRun certora/BeamState.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,) +certora-configurator :; PATH=${PATH} certoraRun certora/Configurator.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,) diff --git a/certora/BeamState.conf b/certora/BeamState.conf new file mode 100644 index 0000000..eb5118b --- /dev/null +++ b/certora/BeamState.conf @@ -0,0 +1,10 @@ +{ + "files": ["src/BeamState.sol"], + "verify": "BeamState:certora/BeamState.spec", + "solc": "solc-0.8.24", + "optimistic_loop": true, + "rule_sanity": "basic", + "multi_assert_check": true, + "optimistic_hashing": true, + "msg": "BeamState" +} diff --git a/certora/BeamState.spec b/certora/BeamState.spec new file mode 100644 index 0000000..527cca2 --- /dev/null +++ b/certora/BeamState.spec @@ -0,0 +1,972 @@ +// SPDX-FileCopyrightText: © 2026 Dai Foundation +// SPDX-License-Identifier: AGPL-3.0-or-later +// +// BeamState.spec -- Formal verification spec for BeamState + +using BeamState as beamState; + +// --- Methods block --- + +methods { + // Storage getters + function wards(address) external returns (uint256) envfree; + function userRoles(address) external returns (bytes32) envfree; + function actionsRoles(bytes4) external returns (bytes32) envfree; + function rateLimits(address) external returns (uint256) envfree; + function controllers(address) external returns (uint256) envfree; + function cBeams(address) external returns (uint256) envfree; + function rateLimitsCBeams(address, address) external returns (uint256) envfree; + function controllersCBeams(address, address) external returns (uint256) envfree; + function initRateLimits(bytes32, address) external returns (uint256, uint256) envfree; + function initControllerActions(bytes32, address) external returns (uint256) envfree; + function hop(address) external returns (uint256) envfree; + function maxChange(address) external returns (uint256) envfree; + function stopped() external returns (bool) envfree; + + // View functions + function hasUserRole(address, uint8) external returns (bool) envfree; + function isActionInRole(bytes4, uint8) external returns (bool) envfree; + function getHop(address) external returns (uint256) envfree; + function getMaxChange(address) external returns (uint256) envfree; + function getInitRateLimits(bytes32, address) external returns (BeamState.DefaultRateLimits) envfree; + function isControllerActionEnabled(bytes32, address) external returns (bool) envfree; +} + +// --- Definitions --- + +definition WAD() returns mathint = 10^18; + +// --- Storage Affected Rule --- + +rule storageAffected(method f) filtered { f -> !f.isView } { + env e; + calldataarg args; + + address anyAddr; + address anyAddr2; + bytes4 anySig; + bytes32 anyKey; + + uint256 wardsBefore = wards(anyAddr); + bytes32 userRolesBefore = userRoles(anyAddr); + bytes32 actionsRolesBefore = actionsRoles(anySig); + bool stoppedBefore = stopped(); + uint256 rateLimitsBefore = rateLimits(anyAddr); + uint256 controllersBefore = controllers(anyAddr); + uint256 cBeamsBefore = cBeams(anyAddr); + uint256 rateLimitsCBeamsBefore = rateLimitsCBeams(anyAddr, anyAddr2); + uint256 controllersCBeamsBefore = controllersCBeams(anyAddr, anyAddr2); + uint256 hopBefore = hop(anyAddr); + uint256 maxChangeBefore = maxChange(anyAddr); + uint256 initRateLimitsMaxAmountBefore; + uint256 initRateLimitsSlopeBefore; + initRateLimitsMaxAmountBefore, initRateLimitsSlopeBefore = initRateLimits(anyKey, anyAddr); + uint256 initControllerActionsBefore = initControllerActions(anyKey, anyAddr); + + f(e, args); + + uint256 wardsAfter = wards(anyAddr); + bytes32 userRolesAfter = userRoles(anyAddr); + bytes32 actionsRolesAfter = actionsRoles(anySig); + bool stoppedAfter = stopped(); + uint256 rateLimitsAfter = rateLimits(anyAddr); + uint256 controllersAfter = controllers(anyAddr); + uint256 cBeamsAfter = cBeams(anyAddr); + uint256 rateLimitsCBeamsAfter = rateLimitsCBeams(anyAddr, anyAddr2); + uint256 controllersCBeamsAfter = controllersCBeams(anyAddr, anyAddr2); + uint256 hopAfter = hop(anyAddr); + uint256 maxChangeAfter = maxChange(anyAddr); + uint256 initRateLimitsMaxAmountAfter; + uint256 initRateLimitsSlopeAfter; + initRateLimitsMaxAmountAfter, initRateLimitsSlopeAfter = initRateLimits(anyKey, anyAddr); + uint256 initControllerActionsAfter = initControllerActions(anyKey, anyAddr); + + assert wardsAfter != wardsBefore => + f.selector == sig:rely(address).selector || + f.selector == sig:deny(address).selector; + assert userRolesAfter != userRolesBefore => + f.selector == sig:setUserRole(address, uint8, bool).selector; + assert actionsRolesAfter != actionsRolesBefore => + f.selector == sig:setRoleAction(uint8, bytes4, bool).selector; + assert stoppedAfter != stoppedBefore => + f.selector == sig:stop().selector || + f.selector == sig:start().selector; + assert rateLimitsAfter != rateLimitsBefore => + f.selector == sig:addRateLimits(address).selector || + f.selector == sig:delRateLimits(address).selector; + assert controllersAfter != controllersBefore => + f.selector == sig:addController(address).selector || + f.selector == sig:delController(address).selector; + assert cBeamsAfter != cBeamsBefore => + f.selector == sig:addCBeam(address).selector || + f.selector == sig:delCBeam(address).selector; + assert rateLimitsCBeamsAfter != rateLimitsCBeamsBefore => + f.selector == sig:setCBeamForRateLimits(address, address).selector || + f.selector == sig:unsetCBeamForRateLimits(address, address).selector; + assert controllersCBeamsAfter != controllersCBeamsBefore => + f.selector == sig:setCBeamForController(address, address).selector || + f.selector == sig:unsetCBeamForController(address, address).selector; + assert hopAfter != hopBefore => + f.selector == sig:setHop(address, uint256).selector; + assert maxChangeAfter != maxChangeBefore => + f.selector == sig:setMaxChange(address, uint256).selector; + assert (initRateLimitsMaxAmountAfter != initRateLimitsMaxAmountBefore || initRateLimitsSlopeAfter != initRateLimitsSlopeBefore) => + f.selector == sig:addInitRateLimits(bytes32, address, uint256, uint256).selector || + f.selector == sig:delInitRateLimits(bytes32, address).selector; + assert initControllerActionsAfter != initControllerActionsBefore => + f.selector == sig:addInitControllerActions(bytes, address).selector || + f.selector == sig:delInitControllerActions(bytes32, address).selector; +} + +// --- Invariants --- + +// Binary value invariants +invariant wardsIsBinary(address usr) + wards(usr) == 0 || wards(usr) == 1; + +invariant rateLimitsIsBinary(address rl) + rateLimits(rl) == 0 || rateLimits(rl) == 1; + +invariant controllersIsBinary(address c) + controllers(c) == 0 || controllers(c) == 1; + +invariant cBeamsIsBinary(address cb) + cBeams(cb) == 0 || cBeams(cb) == 1; + +invariant rateLimitsCBeamsIsBinary(address rl, address cb) + rateLimitsCBeams(rl, cb) == 0 || rateLimitsCBeams(rl, cb) == 1; + +invariant controllersCBeamsIsBinary(address c, address cb) + controllersCBeams(c, cb) == 0 || controllersCBeams(c, cb) == 1; + +invariant initControllerActionsIsBinary(bytes32 key, address c) + initControllerActions(key, c) == 0 || initControllerActions(key, c) == 1; + +// maxChange must be >= WAD when set (enforced by setMaxChange require) +invariant maxChangeMinimum(address rl) + maxChange(rl) == 0 || maxChange(rl) >= WAD(); + +// --- View function correctness --- + +// hasUserRole correctly checks the bit in userRoles +rule hasUserRoleCorrectness(address usr, uint8 role) { + bytes32 userRolesUsr = userRoles(usr); + bytes32 mask = to_bytes32(assert_uint256(2 ^ role)); + bool result = hasUserRole(usr, role); + + assert result <=> (userRolesUsr & mask != to_bytes32(0)); +} + +// isActionInRole correctly checks the bit in actionsRoles +rule isActionInRoleCorrectness(bytes4 sig_, uint8 role) { + bytes32 actionsRolesSig = actionsRoles(sig_); + bytes32 mask = to_bytes32(assert_uint256(2 ^ role)); + bool result = isActionInRole(sig_, role); + + assert result <=> (actionsRolesSig & mask != to_bytes32(0)); +} + +// getHop returns hop[rl] if set, otherwise falls back to hop[address(0)] +rule getHopCorrectness(address rl) { + uint256 hopRl = hop(rl); + uint256 hopZero = hop(0); + uint256 result = getHop(rl); + + assert hopRl != 0 => result == hopRl; + assert hopRl == 0 => result == hopZero; +} + +// getMaxChange returns maxChange[rl] if set, otherwise falls back to maxChange[address(0)] +rule getMaxChangeCorrectness(address rl) { + uint256 maxChangeRl = maxChange(rl); + uint256 maxChangeZero = maxChange(0); + uint256 result = getMaxChange(rl); + + assert maxChangeRl != 0 => result == maxChangeRl; + assert maxChangeRl == 0 => result == maxChangeZero; +} + +// isControllerActionEnabled checks address(0) OR specific controller +rule isControllerActionEnabledCorrectness(bytes32 key, address controller) { + uint256 initControllerActionsKeyZero = initControllerActions(key, 0); + uint256 initControllerActionsKeyController = initControllerActions(key, controller); + bool result = isControllerActionEnabled(key, controller); + + assert result <=> (initControllerActionsKeyZero == 1 || initControllerActionsKeyController == 1); +} + +// --- Auth functions: rely --- + +rule rely(address usr) { + env e; + + address other; + require other != usr; + + uint256 wardsOtherBefore = wards(other); + + rely(e, usr); + + uint256 wardsUsrAfter = wards(usr); + uint256 wardsOtherAfter = wards(other); + + assert wardsUsrAfter == 1; + assert wardsOtherAfter == wardsOtherBefore; +} + +rule rely_revert(address usr) { + env e; + + uint256 wardsSender = wards(e.msg.sender); + + rely@withrevert(e, usr); + + bool revert1 = e.msg.value > 0; + bool revert2 = wardsSender != 1; + + assert lastReverted <=> revert1 || revert2; +} + +// --- Auth functions: deny --- + +rule deny(address usr) { + env e; + + address other; + require other != usr; + + uint256 wardsOtherBefore = wards(other); + + deny(e, usr); + + uint256 wardsUsrAfter = wards(usr); + uint256 wardsOtherAfter = wards(other); + + assert wardsUsrAfter == 0; + assert wardsOtherAfter == wardsOtherBefore; +} + +rule deny_revert(address usr) { + env e; + + uint256 wardsSender = wards(e.msg.sender); + + deny@withrevert(e, usr); + + bool revert1 = e.msg.value > 0; + bool revert2 = wardsSender != 1; + + assert lastReverted <=> revert1 || revert2; +} + +// --- Auth functions: setUserRole --- + +rule setUserRole(address who, uint8 role, bool enabled) { + env e; + + address other; + require other != who; + + bytes32 userRolesWhoBefore = userRoles(who); + bytes32 userRolesOtherBefore = userRoles(other); + + bytes32 mask = to_bytes32(assert_uint256(2 ^ role)); + bytes32 expectedUserRolesWho; + if (enabled) { + expectedUserRolesWho = userRolesWhoBefore | mask; + } else { + expectedUserRolesWho = userRolesWhoBefore & ~mask; + } + + setUserRole(e, who, role, enabled); + + bytes32 userRolesWhoAfter = userRoles(who); + bytes32 userRolesOtherAfter = userRoles(other); + + assert userRolesWhoAfter == expectedUserRolesWho; + assert userRolesOtherAfter == userRolesOtherBefore; +} + +rule setUserRole_revert(address who, uint8 role, bool enabled) { + env e; + + uint256 wardsSender = wards(e.msg.sender); + + setUserRole@withrevert(e, who, role, enabled); + + bool revert1 = e.msg.value > 0; + bool revert2 = wardsSender != 1; + + assert lastReverted <=> revert1 || revert2; +} + +// --- Auth functions: setRoleAction --- + +rule setRoleAction(uint8 role, bytes4 sig_, bool enabled) { + env e; + + bytes4 otherSig; + require otherSig != sig_; + + bytes32 actionsRolesSigBefore = actionsRoles(sig_); + bytes32 actionsRolesOtherSigBefore = actionsRoles(otherSig); + + bytes32 mask = to_bytes32(assert_uint256(2 ^ role)); + bytes32 expectedActionsRolesSig; + if (enabled) { + expectedActionsRolesSig = actionsRolesSigBefore | mask; + } else { + expectedActionsRolesSig = actionsRolesSigBefore & ~mask; + } + + setRoleAction(e, role, sig_, enabled); + + bytes32 actionsRolesSigAfter = actionsRoles(sig_); + bytes32 actionsRolesOtherSigAfter = actionsRoles(otherSig); + + assert actionsRolesSigAfter == expectedActionsRolesSig; + assert actionsRolesOtherSigAfter == actionsRolesOtherSigBefore; +} + +rule setRoleAction_revert(uint8 role, bytes4 sig_, bool enabled) { + env e; + + uint256 wardsSender = wards(e.msg.sender); + + setRoleAction@withrevert(e, role, sig_, enabled); + + bool revert1 = e.msg.value > 0; + bool revert2 = wardsSender != 1; + + assert lastReverted <=> revert1 || revert2; +} + +// --- RoleAuth functions: stop --- + +rule stop() { + env e; + + stop(e); + + assert stopped() == true; +} + +rule stop_revert() { + env e; + + uint256 wardsSender = wards(e.msg.sender); + bytes32 userRolesSender = userRoles(e.msg.sender); + bytes32 actionsRolesStop = actionsRoles(to_bytes4(sig:stop().selector)); + + stop@withrevert(e); + + bool revert1 = e.msg.value > 0; + bool revert2 = (userRolesSender & actionsRolesStop == to_bytes32(0)) && wardsSender != 1; + + assert lastReverted <=> revert1 || revert2; +} + +// --- RoleAuth functions: start --- + +rule start() { + env e; + + start(e); + + assert stopped() == false; +} + +rule start_revert() { + env e; + + uint256 wardsSender = wards(e.msg.sender); + bytes32 userRolesSender = userRoles(e.msg.sender); + bytes32 actionsRolesStart = actionsRoles(to_bytes4(sig:start().selector)); + + start@withrevert(e); + + bool revert1 = e.msg.value > 0; + bool revert2 = (userRolesSender & actionsRolesStart == to_bytes32(0)) && wardsSender != 1; + + assert lastReverted <=> revert1 || revert2; +} + +// --- RoleAuth functions: setHop --- + +rule setHop(address rateLimits_, uint256 value) { + env e; + + address other; + require other != rateLimits_; + + uint256 hopOtherBefore = hop(other); + + setHop(e, rateLimits_, value); + + uint256 hopRateLimitsAfter = hop(rateLimits_); + uint256 hopOtherAfter = hop(other); + + assert hopRateLimitsAfter == value; + assert hopOtherAfter == hopOtherBefore; +} + +rule setHop_revert(address rateLimits_, uint256 value) { + env e; + + uint256 wardsSender = wards(e.msg.sender); + bytes32 userRolesSender = userRoles(e.msg.sender); + bytes32 actionsRolesSetHop = actionsRoles(to_bytes4(sig:setHop(address, uint256).selector)); + + setHop@withrevert(e, rateLimits_, value); + + bool revert1 = e.msg.value > 0; + bool revert2 = (userRolesSender & actionsRolesSetHop == to_bytes32(0)) && wardsSender != 1; + + assert lastReverted <=> revert1 || revert2; +} + +// --- RoleAuth functions: setMaxChange --- + +rule setMaxChange(address rateLimits_, uint256 value) { + env e; + + address other; + require other != rateLimits_; + + uint256 maxChangeOtherBefore = maxChange(other); + + setMaxChange(e, rateLimits_, value); + + uint256 maxChangeRateLimitsAfter = maxChange(rateLimits_); + uint256 maxChangeOtherAfter = maxChange(other); + + assert maxChangeRateLimitsAfter == value; + assert maxChangeOtherAfter == maxChangeOtherBefore; +} + +rule setMaxChange_revert(address rateLimits_, uint256 value) { + env e; + + uint256 wardsSender = wards(e.msg.sender); + bytes32 userRolesSender = userRoles(e.msg.sender); + bytes32 actionsRolesSetMaxChange = actionsRoles(to_bytes4(sig:setMaxChange(address, uint256).selector)); + + setMaxChange@withrevert(e, rateLimits_, value); + + bool revert1 = e.msg.value > 0; + bool revert2 = (userRolesSender & actionsRolesSetMaxChange == to_bytes32(0)) && wardsSender != 1; + bool revert3 = value < WAD(); + + assert lastReverted <=> revert1 || revert2 || revert3; +} + +// --- RoleAuth functions: addRateLimits --- + +rule addRateLimits(address rateLimits_) { + env e; + + address other; + require other != rateLimits_; + + uint256 rateLimitsOtherBefore = rateLimits(other); + + addRateLimits(e, rateLimits_); + + uint256 rateLimitsRateLimitsAfter = rateLimits(rateLimits_); + uint256 rateLimitsOtherAfter = rateLimits(other); + + assert rateLimitsRateLimitsAfter == 1; + assert rateLimitsOtherAfter == rateLimitsOtherBefore; +} + +rule addRateLimits_revert(address rateLimits_) { + env e; + + uint256 wardsSender = wards(e.msg.sender); + bytes32 userRolesSender = userRoles(e.msg.sender); + bytes32 actionsRolesAddRateLimits = actionsRoles(to_bytes4(sig:addRateLimits(address).selector)); + + addRateLimits@withrevert(e, rateLimits_); + + bool revert1 = e.msg.value > 0; + bool revert2 = (userRolesSender & actionsRolesAddRateLimits == to_bytes32(0)) && wardsSender != 1; + + assert lastReverted <=> revert1 || revert2; +} + +// --- RoleAuth functions: delRateLimits --- + +rule delRateLimits(address rateLimits_) { + env e; + + address other; + require other != rateLimits_; + + uint256 rateLimitsOtherBefore = rateLimits(other); + + delRateLimits(e, rateLimits_); + + uint256 rateLimitsRateLimitsAfter = rateLimits(rateLimits_); + uint256 rateLimitsOtherAfter = rateLimits(other); + + assert rateLimitsRateLimitsAfter == 0; + assert rateLimitsOtherAfter == rateLimitsOtherBefore; +} + +rule delRateLimits_revert(address rateLimits_) { + env e; + + uint256 wardsSender = wards(e.msg.sender); + bytes32 userRolesSender = userRoles(e.msg.sender); + bytes32 actionsRolesDelRateLimits = actionsRoles(to_bytes4(sig:delRateLimits(address).selector)); + + delRateLimits@withrevert(e, rateLimits_); + + bool revert1 = e.msg.value > 0; + bool revert2 = (userRolesSender & actionsRolesDelRateLimits == to_bytes32(0)) && wardsSender != 1; + + assert lastReverted <=> revert1 || revert2; +} + +// --- RoleAuth functions: addController --- + +rule addController(address controller) { + env e; + + address other; + require other != controller; + + uint256 controllersOtherBefore = controllers(other); + + addController(e, controller); + + uint256 controllersControllerAfter = controllers(controller); + uint256 controllersOtherAfter = controllers(other); + + assert controllersControllerAfter == 1; + assert controllersOtherAfter == controllersOtherBefore; +} + +rule addController_revert(address controller) { + env e; + + uint256 wardsSender = wards(e.msg.sender); + bytes32 userRolesSender = userRoles(e.msg.sender); + bytes32 actionsRolesAddController = actionsRoles(to_bytes4(sig:addController(address).selector)); + + addController@withrevert(e, controller); + + bool revert1 = e.msg.value > 0; + bool revert2 = (userRolesSender & actionsRolesAddController == to_bytes32(0)) && wardsSender != 1; + + assert lastReverted <=> revert1 || revert2; +} + +// --- RoleAuth functions: delController --- + +rule delController(address controller) { + env e; + + address other; + require other != controller; + + uint256 controllersOtherBefore = controllers(other); + + delController(e, controller); + + uint256 controllersControllerAfter = controllers(controller); + uint256 controllersOtherAfter = controllers(other); + + assert controllersControllerAfter == 0; + assert controllersOtherAfter == controllersOtherBefore; +} + +rule delController_revert(address controller) { + env e; + + uint256 wardsSender = wards(e.msg.sender); + bytes32 userRolesSender = userRoles(e.msg.sender); + bytes32 actionsRolesDelController = actionsRoles(to_bytes4(sig:delController(address).selector)); + + delController@withrevert(e, controller); + + bool revert1 = e.msg.value > 0; + bool revert2 = (userRolesSender & actionsRolesDelController == to_bytes32(0)) && wardsSender != 1; + + assert lastReverted <=> revert1 || revert2; +} + +// --- RoleAuth functions: addCBeam --- + +rule addCBeam(address cBeam) { + env e; + + address other; + require other != cBeam; + + uint256 cBeamsOtherBefore = cBeams(other); + + addCBeam(e, cBeam); + + uint256 cBeamsCBeamAfter = cBeams(cBeam); + uint256 cBeamsOtherAfter = cBeams(other); + + assert cBeamsCBeamAfter == 1; + assert cBeamsOtherAfter == cBeamsOtherBefore; +} + +rule addCBeam_revert(address cBeam) { + env e; + + uint256 wardsSender = wards(e.msg.sender); + bytes32 userRolesSender = userRoles(e.msg.sender); + bytes32 actionsRolesAddCBeam = actionsRoles(to_bytes4(sig:addCBeam(address).selector)); + + addCBeam@withrevert(e, cBeam); + + bool revert1 = e.msg.value > 0; + bool revert2 = (userRolesSender & actionsRolesAddCBeam == to_bytes32(0)) && wardsSender != 1; + + assert lastReverted <=> revert1 || revert2; +} + +// --- RoleAuth functions: delCBeam --- + +rule delCBeam(address cBeam) { + env e; + + address other; + require other != cBeam; + + uint256 cBeamsOtherBefore = cBeams(other); + + delCBeam(e, cBeam); + + uint256 cBeamsCBeamAfter = cBeams(cBeam); + uint256 cBeamsOtherAfter = cBeams(other); + + assert cBeamsCBeamAfter == 0; + assert cBeamsOtherAfter == cBeamsOtherBefore; +} + +rule delCBeam_revert(address cBeam) { + env e; + + uint256 wardsSender = wards(e.msg.sender); + bytes32 userRolesSender = userRoles(e.msg.sender); + bytes32 actionsRolesDelCBeam = actionsRoles(to_bytes4(sig:delCBeam(address).selector)); + + delCBeam@withrevert(e, cBeam); + + bool revert1 = e.msg.value > 0; + bool revert2 = (userRolesSender & actionsRolesDelCBeam == to_bytes32(0)) && wardsSender != 1; + + assert lastReverted <=> revert1 || revert2; +} + +// --- RoleAuth functions: setCBeamForRateLimits --- + +rule setCBeamForRateLimits(address rateLimits_, address cBeam) { + env e; + + address otherRl; + address otherCb; + require otherRl != rateLimits_ || otherCb != cBeam; + + uint256 rateLimitsCBeamsOtherRlOtherCbBefore = rateLimitsCBeams(otherRl, otherCb); + + setCBeamForRateLimits(e, rateLimits_, cBeam); + + uint256 rateLimitsCBeamsRateLimitsCBeamAfter = rateLimitsCBeams(rateLimits_, cBeam); + uint256 rateLimitsCBeamsOtherRlOtherCbAfter = rateLimitsCBeams(otherRl, otherCb); + + assert rateLimitsCBeamsRateLimitsCBeamAfter == 1; + assert rateLimitsCBeamsOtherRlOtherCbAfter == rateLimitsCBeamsOtherRlOtherCbBefore; +} + +rule setCBeamForRateLimits_revert(address rateLimits_, address cBeam) { + env e; + + uint256 wardsSender = wards(e.msg.sender); + bytes32 userRolesSender = userRoles(e.msg.sender); + bytes32 actionsRolesSetCBeamForRateLimits = actionsRoles(to_bytes4(sig:setCBeamForRateLimits(address, address).selector)); + uint256 rateLimitsRateLimits = rateLimits(rateLimits_); + uint256 cBeamsCBeam = cBeams(cBeam); + + setCBeamForRateLimits@withrevert(e, rateLimits_, cBeam); + + bool revert1 = e.msg.value > 0; + bool revert2 = (userRolesSender & actionsRolesSetCBeamForRateLimits == to_bytes32(0)) && wardsSender != 1; + bool revert3 = rateLimitsRateLimits != 1; + bool revert4 = cBeamsCBeam != 1; + + assert lastReverted <=> revert1 || revert2 || revert3 || revert4; +} + +// --- RoleAuth functions: unsetCBeamForRateLimits --- + +rule unsetCBeamForRateLimits(address rateLimits_, address cBeam) { + env e; + + address otherRl; + address otherCb; + require otherRl != rateLimits_ || otherCb != cBeam; + + uint256 rateLimitsCBeamsOtherRlOtherCbBefore = rateLimitsCBeams(otherRl, otherCb); + + unsetCBeamForRateLimits(e, rateLimits_, cBeam); + + uint256 rateLimitsCBeamsRateLimitsCBeamAfter = rateLimitsCBeams(rateLimits_, cBeam); + uint256 rateLimitsCBeamsOtherRlOtherCbAfter = rateLimitsCBeams(otherRl, otherCb); + + assert rateLimitsCBeamsRateLimitsCBeamAfter == 0; + assert rateLimitsCBeamsOtherRlOtherCbAfter == rateLimitsCBeamsOtherRlOtherCbBefore; +} + +rule unsetCBeamForRateLimits_revert(address rateLimits_, address cBeam) { + env e; + + uint256 wardsSender = wards(e.msg.sender); + bytes32 userRolesSender = userRoles(e.msg.sender); + bytes32 actionsRolesUnsetCBeamForRateLimits = actionsRoles(to_bytes4(sig:unsetCBeamForRateLimits(address, address).selector)); + + unsetCBeamForRateLimits@withrevert(e, rateLimits_, cBeam); + + bool revert1 = e.msg.value > 0; + bool revert2 = (userRolesSender & actionsRolesUnsetCBeamForRateLimits == to_bytes32(0)) && wardsSender != 1; + + assert lastReverted <=> revert1 || revert2; +} + +// --- RoleAuth functions: setCBeamForController --- + +rule setCBeamForController(address controller, address cBeam) { + env e; + + address otherC; + address otherCb; + require otherC != controller || otherCb != cBeam; + + uint256 controllersCBeamsOtherCOtherCbBefore = controllersCBeams(otherC, otherCb); + + setCBeamForController(e, controller, cBeam); + + uint256 controllersCBeamsControllerCBeamAfter = controllersCBeams(controller, cBeam); + uint256 controllersCBeamsOtherCOtherCbAfter = controllersCBeams(otherC, otherCb); + + assert controllersCBeamsControllerCBeamAfter == 1; + assert controllersCBeamsOtherCOtherCbAfter == controllersCBeamsOtherCOtherCbBefore; +} + +rule setCBeamForController_revert(address controller, address cBeam) { + env e; + + uint256 wardsSender = wards(e.msg.sender); + bytes32 userRolesSender = userRoles(e.msg.sender); + bytes32 actionsRolesSetCBeamForController = actionsRoles(to_bytes4(sig:setCBeamForController(address, address).selector)); + uint256 controllersController = controllers(controller); + uint256 cBeamsCBeam = cBeams(cBeam); + + setCBeamForController@withrevert(e, controller, cBeam); + + bool revert1 = e.msg.value > 0; + bool revert2 = (userRolesSender & actionsRolesSetCBeamForController == to_bytes32(0)) && wardsSender != 1; + bool revert3 = controllersController != 1; + bool revert4 = cBeamsCBeam != 1; + + assert lastReverted <=> revert1 || revert2 || revert3 || revert4; +} + +// --- RoleAuth functions: unsetCBeamForController --- + +rule unsetCBeamForController(address controller, address cBeam) { + env e; + + address otherC; + address otherCb; + require otherC != controller || otherCb != cBeam; + + uint256 controllersCBeamsOtherCOtherCbBefore = controllersCBeams(otherC, otherCb); + + unsetCBeamForController(e, controller, cBeam); + + uint256 controllersCBeamsControllerCBeamAfter = controllersCBeams(controller, cBeam); + uint256 controllersCBeamsOtherCOtherCbAfter = controllersCBeams(otherC, otherCb); + + assert controllersCBeamsControllerCBeamAfter == 0; + assert controllersCBeamsOtherCOtherCbAfter == controllersCBeamsOtherCOtherCbBefore; +} + +rule unsetCBeamForController_revert(address controller, address cBeam) { + env e; + + uint256 wardsSender = wards(e.msg.sender); + bytes32 userRolesSender = userRoles(e.msg.sender); + bytes32 actionsRolesUnsetCBeamForController = actionsRoles(to_bytes4(sig:unsetCBeamForController(address, address).selector)); + + unsetCBeamForController@withrevert(e, controller, cBeam); + + bool revert1 = e.msg.value > 0; + bool revert2 = (userRolesSender & actionsRolesUnsetCBeamForController == to_bytes32(0)) && wardsSender != 1; + + assert lastReverted <=> revert1 || revert2; +} + +// --- RoleAuth functions: addInitRateLimits --- + +rule addInitRateLimits(bytes32 key, address rateLimits_, uint256 maxAmount, uint256 slope) { + env e; + + bytes32 otherKey; + address otherRl; + require otherKey != key || otherRl != rateLimits_; + + uint256 initRateLimitsOtherKeyOtherRlMaxAmountBefore; + uint256 initRateLimitsOtherKeyOtherRlSlopeBefore; + initRateLimitsOtherKeyOtherRlMaxAmountBefore, initRateLimitsOtherKeyOtherRlSlopeBefore = initRateLimits(otherKey, otherRl); + + addInitRateLimits(e, key, rateLimits_, maxAmount, slope); + + uint256 initRateLimitsKeyRateLimitsMaxAmountAfter; + uint256 initRateLimitsKeyRateLimitsSlopeAfter; + initRateLimitsKeyRateLimitsMaxAmountAfter, initRateLimitsKeyRateLimitsSlopeAfter = initRateLimits(key, rateLimits_); + + uint256 initRateLimitsOtherKeyOtherRlMaxAmountAfter; + uint256 initRateLimitsOtherKeyOtherRlSlopeAfter; + initRateLimitsOtherKeyOtherRlMaxAmountAfter, initRateLimitsOtherKeyOtherRlSlopeAfter = initRateLimits(otherKey, otherRl); + + assert initRateLimitsKeyRateLimitsMaxAmountAfter == maxAmount; + assert initRateLimitsKeyRateLimitsSlopeAfter == slope; + assert initRateLimitsOtherKeyOtherRlMaxAmountAfter == initRateLimitsOtherKeyOtherRlMaxAmountBefore; + assert initRateLimitsOtherKeyOtherRlSlopeAfter == initRateLimitsOtherKeyOtherRlSlopeBefore; +} + +rule addInitRateLimits_revert(bytes32 key, address rateLimits_, uint256 maxAmount, uint256 slope) { + env e; + + uint256 wardsSender = wards(e.msg.sender); + bytes32 userRolesSender = userRoles(e.msg.sender); + bytes32 actionsRolesAddInitRateLimits = actionsRoles(to_bytes4(sig:addInitRateLimits(bytes32, address, uint256, uint256).selector)); + + addInitRateLimits@withrevert(e, key, rateLimits_, maxAmount, slope); + + bool revert1 = e.msg.value > 0; + bool revert2 = (userRolesSender & actionsRolesAddInitRateLimits == to_bytes32(0)) && wardsSender != 1; + + assert lastReverted <=> revert1 || revert2; +} + +// --- RoleAuth functions: delInitRateLimits --- + +rule delInitRateLimits(bytes32 key, address rateLimits_) { + env e; + + bytes32 otherKey; + address otherRl; + require otherKey != key || otherRl != rateLimits_; + + uint256 initRateLimitsOtherKeyOtherRlMaxAmountBefore; + uint256 initRateLimitsOtherKeyOtherRlSlopeBefore; + initRateLimitsOtherKeyOtherRlMaxAmountBefore, initRateLimitsOtherKeyOtherRlSlopeBefore = initRateLimits(otherKey, otherRl); + + delInitRateLimits(e, key, rateLimits_); + + uint256 initRateLimitsKeyRateLimitsMaxAmountAfter; + uint256 initRateLimitsKeyRateLimitsSlopeAfter; + initRateLimitsKeyRateLimitsMaxAmountAfter, initRateLimitsKeyRateLimitsSlopeAfter = initRateLimits(key, rateLimits_); + + uint256 initRateLimitsOtherKeyOtherRlMaxAmountAfter; + uint256 initRateLimitsOtherKeyOtherRlSlopeAfter; + initRateLimitsOtherKeyOtherRlMaxAmountAfter, initRateLimitsOtherKeyOtherRlSlopeAfter = initRateLimits(otherKey, otherRl); + + assert initRateLimitsKeyRateLimitsMaxAmountAfter == 0; + assert initRateLimitsKeyRateLimitsSlopeAfter == 0; + assert initRateLimitsOtherKeyOtherRlMaxAmountAfter == initRateLimitsOtherKeyOtherRlMaxAmountBefore; + assert initRateLimitsOtherKeyOtherRlSlopeAfter == initRateLimitsOtherKeyOtherRlSlopeBefore; +} + +rule delInitRateLimits_revert(bytes32 key, address rateLimits_) { + env e; + + uint256 wardsSender = wards(e.msg.sender); + bytes32 userRolesSender = userRoles(e.msg.sender); + bytes32 actionsRolesDelInitRateLimits = actionsRoles(to_bytes4(sig:delInitRateLimits(bytes32, address).selector)); + + delInitRateLimits@withrevert(e, key, rateLimits_); + + bool revert1 = e.msg.value > 0; + bool revert2 = (userRolesSender & actionsRolesDelInitRateLimits == to_bytes32(0)) && wardsSender != 1; + + assert lastReverted <=> revert1 || revert2; +} + +// --- RoleAuth functions: addInitControllerActions --- + +rule addInitControllerActions(bytes data, address controller) { + env e; + + bytes32 otherKey; + address otherController; + bytes32 key = keccak256(data); + require otherKey != key || otherController != controller; + + uint256 initControllerActionsOtherKeyOtherControllerBefore = initControllerActions(otherKey, otherController); + + addInitControllerActions(e, data, controller); + + uint256 initControllerActionsKeyControllerAfter = initControllerActions(key, controller); + uint256 initControllerActionsOtherKeyOtherControllerAfter = initControllerActions(otherKey, otherController); + + assert initControllerActionsKeyControllerAfter == 1; + assert initControllerActionsOtherKeyOtherControllerAfter == initControllerActionsOtherKeyOtherControllerBefore; +} + +rule addInitControllerActions_revert(bytes data, address controller) { + env e; + + uint256 wardsSender = wards(e.msg.sender); + bytes32 userRolesSender = userRoles(e.msg.sender); + bytes32 actionsRolesAddInitControllerActions = actionsRoles(to_bytes4(sig:addInitControllerActions(bytes, address).selector)); + + addInitControllerActions@withrevert(e, data, controller); + + bool revert1 = e.msg.value > 0; + bool revert2 = (userRolesSender & actionsRolesAddInitControllerActions == to_bytes32(0)) && wardsSender != 1; + + assert lastReverted <=> revert1 || revert2; +} + +// --- RoleAuth functions: delInitControllerActions --- + +rule delInitControllerActions(bytes32 key, address controller) { + env e; + + bytes32 otherKey; + address otherController; + require otherKey != key || otherController != controller; + + uint256 initControllerActionsOtherKeyOtherControllerBefore = initControllerActions(otherKey, otherController); + + delInitControllerActions(e, key, controller); + + uint256 initControllerActionsKeyControllerAfter = initControllerActions(key, controller); + uint256 initControllerActionsOtherKeyOtherControllerAfter = initControllerActions(otherKey, otherController); + + assert initControllerActionsKeyControllerAfter == 0; + assert initControllerActionsOtherKeyOtherControllerAfter == initControllerActionsOtherKeyOtherControllerBefore; +} + +rule delInitControllerActions_revert(bytes32 key, address controller) { + env e; + + uint256 wardsSender = wards(e.msg.sender); + bytes32 userRolesSender = userRoles(e.msg.sender); + bytes32 actionsRolesDelInitControllerActions = actionsRoles(to_bytes4(sig:delInitControllerActions(bytes32, address).selector)); + + delInitControllerActions@withrevert(e, key, controller); + + bool revert1 = e.msg.value > 0; + bool revert2 = (userRolesSender & actionsRolesDelInitControllerActions == to_bytes32(0)) && wardsSender != 1; + + assert lastReverted <=> revert1 || revert2; +} diff --git a/certora/Configurator.conf b/certora/Configurator.conf new file mode 100644 index 0000000..128087a --- /dev/null +++ b/certora/Configurator.conf @@ -0,0 +1,12 @@ +{ + "files": ["src/Configurator.sol", "src/BeamState.sol", "certora/harness/RateLimitsHarness.sol"], + "verify": "Configurator:certora/Configurator.spec", + "link": ["Configurator:beamState=BeamState"], + "solc": "solc-0.8.24", + "optimistic_loop": true, + "rule_sanity": "basic", + "multi_assert_check": true, + "optimistic_hashing": true, + "parametric_contracts": ["Configurator"], + "msg": "Configurator" +} diff --git a/certora/Configurator.spec b/certora/Configurator.spec new file mode 100644 index 0000000..8b77465 --- /dev/null +++ b/certora/Configurator.spec @@ -0,0 +1,301 @@ +// SPDX-FileCopyrightText: © 2026 Dai Foundation +// SPDX-License-Identifier: AGPL-3.0-or-later +// +// Configurator.spec -- Formal verification spec for Configurator + +using Configurator as configurator; +using BeamState as beamState; +using RateLimitsHarness as rateLimitsHarness; + +// --- Methods block --- + +methods { + // Configurator storage getters + function zzz(address, bytes32) external returns (uint256) envfree; + + // Configurator immutable getter + function beamState() external returns (address) envfree; + + // BeamState functions used by Configurator + function beamState.stopped() external returns (bool) envfree; + function beamState.rateLimitsCBeams(address, address) external returns (uint256) envfree; + function beamState.controllersCBeams(address, address) external returns (uint256) envfree; + function beamState.getHop(address) external returns (uint256) envfree; + function beamState.getMaxChange(address) external returns (uint256) envfree; + function beamState.getInitRateLimits(bytes32, address) external returns (BeamState.DefaultRateLimits) envfree; + function beamState.isControllerActionEnabled(bytes32, address) external returns (bool) envfree; + + // RateLimitsHarness functions + function rateLimitsHarness.getMaxAmount(bytes32) external returns (uint256) envfree; + function rateLimitsHarness.getSlope(bytes32) external returns (uint256) envfree; + function rateLimitsHarness.getLastAmount(bytes32) external returns (uint256) envfree; + function rateLimitsHarness.getLastUpdated(bytes32) external returns (uint256) envfree; + + function _.getRateLimitData(bytes32) external => DISPATCHER(true); + function _.getCurrentRateLimit(bytes32) external => DISPATCHER(true); + function _.setRateLimitData(bytes32, uint256, uint256, uint256, uint256) external => DISPATCHER(true); + function _.setUnlimitedRateLimitData(bytes32) external => DISPATCHER(true); +} + +// --- Definitions --- + +definition WAD() returns mathint = 10^18; + +// Helper to compute max of two values +definition _max(uint256 x, uint256 y) returns uint256 = x > y ? x : y; + +// Helper to compute min of two values +definition _min(uint256 x, uint256 y) returns uint256 = x < y ? x : y; + +// --- Storage Affected Rule --- + +rule storageAffected(method f) filtered { f -> !f.isView } { + env e; + calldataarg args; + + address anyAddr; + bytes32 anyKey; + + uint256 zzzBefore = zzz(anyAddr, anyKey); + + f(e, args); + + uint256 zzzAfter = zzz(anyAddr, anyKey); + + assert zzzAfter != zzzBefore => + f.selector == sig:setRateLimit(address, bytes32, uint256, uint256).selector; +} + +// --- setRateLimit rules --- + +// Verifies that setRateLimit correctly handles the unlimited case +rule setRateLimit_unlimited(bytes32 key, uint256 maxAmount, uint256 slope) { + env e; + + // Setup: unlimited defaults (maxAmount == type(uint256).max && slope == 0) + BeamState.DefaultRateLimits defLimits = beamState.getInitRateLimits(key, rateLimitsHarness); + require defLimits.maxAmount == max_uint256; + require defLimits.slope == 0; + + // Pre-state + uint256 zzzBefore = zzz(rateLimitsHarness, key); + + setRateLimit(e, rateLimitsHarness, key, maxAmount, slope); + + // Post-state + uint256 maxAmountAfter = rateLimitsHarness.getMaxAmount(key); + uint256 slopeAfter = rateLimitsHarness.getSlope(key); + uint256 lastAmountAfter = rateLimitsHarness.getLastAmount(key); + uint256 zzzAfter = zzz(rateLimitsHarness, key); + + // When unlimited: setUnlimitedRateLimitData sets maxAmount = max_uint256, slope = 0, lastAmount = max_uint256 + assert maxAmountAfter == max_uint256; + assert slopeAfter == 0; + assert lastAmountAfter == max_uint256; + // zzz should NOT be updated for unlimited + assert zzzAfter == zzzBefore; +} + +// Verifies that setRateLimit correctly handles decrements (no hop required, zzz not updated) +rule setRateLimit_decrement(bytes32 key, uint256 maxAmount, uint256 slope) { + env e; + + // Setup: NOT unlimited defaults + BeamState.DefaultRateLimits defLimits = beamState.getInitRateLimits(key, rateLimitsHarness); + require !(defLimits.maxAmount == max_uint256 && defLimits.slope == 0); + + // Current values + uint256 currentMaxAmount = rateLimitsHarness.getMaxAmount(key); + uint256 currentSlope = rateLimitsHarness.getSlope(key); + + // This is a decrement (both params <= current) + require maxAmount <= currentMaxAmount; + require slope <= currentSlope; + + // Pre-state + uint256 zzzBefore = zzz(rateLimitsHarness, key); + + setRateLimit(e, rateLimitsHarness, key, maxAmount, slope); + + // Post-state + uint256 maxAmountAfter = rateLimitsHarness.getMaxAmount(key); + uint256 slopeAfter = rateLimitsHarness.getSlope(key); + uint256 zzzAfter = zzz(rateLimitsHarness, key); + + // Values should be set as requested + assert maxAmountAfter == maxAmount; + assert slopeAfter == slope; + // zzz should NOT be updated on decrement + assert zzzAfter == zzzBefore; +} + +// Verifies that setRateLimit correctly handles increments (hop required, zzz updated) +rule setRateLimit_increment(bytes32 key, uint256 maxAmount, uint256 slope) { + env e; + + // Setup: NOT unlimited defaults + BeamState.DefaultRateLimits defLimits = beamState.getInitRateLimits(key, rateLimitsHarness); + require !(defLimits.maxAmount == max_uint256 && defLimits.slope == 0); + + // Current values + uint256 currentMaxAmount = rateLimitsHarness.getMaxAmount(key); + uint256 currentSlope = rateLimitsHarness.getSlope(key); + + // This is an increment (at least one param > current) + require maxAmount > currentMaxAmount || slope > currentSlope; + + setRateLimit(e, rateLimitsHarness, key, maxAmount, slope); + + // Post-state + uint256 maxAmountAfter = rateLimitsHarness.getMaxAmount(key); + uint256 slopeAfter = rateLimitsHarness.getSlope(key); + uint256 zzzAfter = zzz(rateLimitsHarness, key); + + // Values should be set as requested + assert maxAmountAfter == maxAmount; + assert slopeAfter == slope; + // zzz should be updated to block.timestamp on increment + assert zzzAfter == e.block.timestamp; +} + +// Verifies that lastAmount is set correctly (min of maxAmount and currentRateLimit) +rule setRateLimit_lastAmount(bytes32 key, uint256 maxAmount, uint256 slope) { + env e; + + // Setup: NOT unlimited defaults + BeamState.DefaultRateLimits defLimits = beamState.getInitRateLimits(key, rateLimitsHarness); + require !(defLimits.maxAmount == max_uint256 && defLimits.slope == 0); + + // Get currentRateLimit before the call + uint256 currentRateLimit = rateLimitsHarness.getCurrentRateLimit(e, key); + + setRateLimit(e, rateLimitsHarness, key, maxAmount, slope); + + // Post-state + uint256 lastAmountAfter = rateLimitsHarness.getLastAmount(key); + uint256 lastUpdatedAfter = rateLimitsHarness.getLastUpdated(key); + + // lastAmount = _min(maxAmount, currentRateLimit) + assert lastAmountAfter == _min(maxAmount, currentRateLimit); + // lastUpdated should be set to block.timestamp + assert lastUpdatedAfter == e.block.timestamp; +} + +// Verifies zzz is not updated for other (rateLimits_, key) pairs +rule setRateLimit_zzz_no_side_effects(bytes32 key, uint256 maxAmount, uint256 slope) { + env e; + + address otherRl; + bytes32 otherKey; + require otherRl != rateLimitsHarness || otherKey != key; + + uint256 zzzOtherBefore = zzz(otherRl, otherKey); + + setRateLimit(e, rateLimitsHarness, key, maxAmount, slope); + + uint256 zzzOtherAfter = zzz(otherRl, otherKey); + + assert zzzOtherAfter == zzzOtherBefore; +} + +// Verifies that rateLimitsHarness data is not modified for other keys +rule setRateLimit_rateLimits_no_side_effects(bytes32 key, uint256 maxAmount, uint256 slope) { + env e; + + bytes32 otherKey; + require otherKey != key; + + uint256 otherMaxAmountBefore = rateLimitsHarness.getMaxAmount(otherKey); + uint256 otherSlopeBefore = rateLimitsHarness.getSlope(otherKey); + uint256 otherLastAmountBefore = rateLimitsHarness.getLastAmount(otherKey); + uint256 otherLastUpdatedBefore = rateLimitsHarness.getLastUpdated(otherKey); + + setRateLimit(e, rateLimitsHarness, key, maxAmount, slope); + + uint256 otherMaxAmountAfter = rateLimitsHarness.getMaxAmount(otherKey); + uint256 otherSlopeAfter = rateLimitsHarness.getSlope(otherKey); + uint256 otherLastAmountAfter = rateLimitsHarness.getLastAmount(otherKey); + uint256 otherLastUpdatedAfter = rateLimitsHarness.getLastUpdated(otherKey); + + assert otherMaxAmountAfter == otherMaxAmountBefore; + assert otherSlopeAfter == otherSlopeBefore; + assert otherLastAmountAfter == otherLastAmountBefore; + assert otherLastUpdatedAfter == otherLastUpdatedBefore; +} + +// --- Revert rules --- + +rule setRateLimit_revert(bytes32 key, uint256 maxAmount, uint256 slope) { + env e; + + bool stopped = beamState.stopped(); + uint256 rateLimitsCBeamsSender = beamState.rateLimitsCBeams(rateLimitsHarness, e.msg.sender); + + BeamState.DefaultRateLimits defLimits = beamState.getInitRateLimits(key, rateLimitsHarness); + uint256 defMaxAmount = defLimits.maxAmount; + uint256 defSlope = defLimits.slope; + + uint256 currentMaxAmount = rateLimitsHarness.getMaxAmount(key); + uint256 currentSlope = rateLimitsHarness.getSlope(key); + uint256 currentLastUpdated = rateLimitsHarness.getLastUpdated(key); + uint256 currentLastAmount = rateLimitsHarness.getLastAmount(key); + + uint256 hop_ = beamState.getHop(rateLimitsHarness); + uint256 maxChange_ = beamState.getMaxChange(rateLimitsHarness); + uint256 zzzValue = zzz(rateLimitsHarness, key); + + bool isUnlimited = defMaxAmount == max_uint256 && defSlope == 0; + bool isIncrement = maxAmount > currentMaxAmount || slope > currentSlope; + + // Avoid overflows + require currentMaxAmount * maxChange_ <= max_uint256; + require currentSlope * maxChange_ <= max_uint256; + require zzzValue + hop_ <= max_uint256 || zzzValue + hop_ >= zzzValue; + require e.block.timestamp >= currentLastUpdated; + require currentSlope * (e.block.timestamp - currentLastUpdated) + currentLastAmount <= max_uint256; + + setRateLimit@withrevert(e, rateLimitsHarness, key, maxAmount, slope); + + bool revert1 = e.msg.value > 0; + bool revert2 = stopped; + bool revert3 = rateLimitsCBeamsSender != 1; + bool revert4 = isUnlimited && !(maxAmount == max_uint256 && slope == 0); + bool revert5 = !isUnlimited && maxAmount > _max(require_uint256(currentMaxAmount * maxChange_ / WAD()), defMaxAmount); + bool revert6 = !isUnlimited && slope > _max(require_uint256(currentSlope * maxChange_ / WAD()), defSlope); + bool revert7 = !isUnlimited && isIncrement && hop_ == 0; + bool revert8 = !isUnlimited && isIncrement && e.block.timestamp < zzzValue + hop_; + + assert lastReverted <=> revert1 || revert2 || revert3 || revert4 || revert5 || revert6 || revert7 || revert8; +} + +// --- callControllerAction rules --- + +rule callControllerAction_revert(address controller, bytes data) { + env e; + + bool stopped = beamState.stopped(); + uint256 controllersCBeamsSender = beamState.controllersCBeams(controller, e.msg.sender); + bool isControllerActionEnabled = beamState.isControllerActionEnabled(keccak256(data), controller); + + callControllerAction@withrevert(e, controller, data); + + bool revert1 = e.msg.value > 0; + bool revert2 = stopped; + bool revert3 = controllersCBeamsSender != 1; + bool revert4 = !isControllerActionEnabled; + + // Note: Additional revert from external controller call is not covered here + assert revert1 || revert2 || revert3 || revert4 => lastReverted; +} + +// When stopped, all non-view functions revert +rule whenStoppedAllFunctionsRevert(method f) filtered { f -> !f.isView } { + env e; + calldataarg args; + + require beamState.stopped(); + + f@withrevert(e, args); + + assert lastReverted; +} diff --git a/certora/harness/RateLimitsHarness.sol b/certora/harness/RateLimitsHarness.sol new file mode 100644 index 0000000..a35c98f --- /dev/null +++ b/certora/harness/RateLimitsHarness.sol @@ -0,0 +1,70 @@ +// SPDX-FileCopyrightText: © 2026 Dai Foundation +// SPDX-License-Identifier: AGPL-3.0-or-later +// +// RateLimitsHarness.sol -- Certora harness for RateLimits interface + +pragma solidity ^0.8.24; + +contract RateLimitsHarness { + + struct RateLimitData { + uint256 maxAmount; + uint256 slope; + uint256 lastAmount; + uint256 lastUpdated; + } + + mapping(bytes32 key => RateLimitData) public rateLimitData; + + function _min(uint256 a, uint256 b) internal pure returns (uint256) { + return a < b ? a : b; + } + + function setRateLimitData( + bytes32 key, + uint256 maxAmount, + uint256 slope, + uint256 lastAmount, + uint256 lastUpdated + ) external { + rateLimitData[key] = RateLimitData(maxAmount, slope, lastAmount, lastUpdated); + } + + function setUnlimitedRateLimitData(bytes32 key) external { + rateLimitData[key] = RateLimitData(type(uint256).max, 0, type(uint256).max, block.timestamp); + } + + function getRateLimitData(bytes32 key) external view returns (RateLimitData memory) { + return rateLimitData[key]; + } + + // Mimics real RateLimits: regenerates based on slope and elapsed time + function getCurrentRateLimit(bytes32 key) external view returns (uint256) { + RateLimitData memory d = rateLimitData[key]; + if (d.maxAmount == type(uint256).max) { + return type(uint256).max; + } + return _min( + d.slope * (block.timestamp - d.lastUpdated) + d.lastAmount, + d.maxAmount + ); + } + + // --- Getters for individual struct fields (for Certora) --- + + function getMaxAmount(bytes32 key) external view returns (uint256) { + return rateLimitData[key].maxAmount; + } + + function getSlope(bytes32 key) external view returns (uint256) { + return rateLimitData[key].slope; + } + + function getLastAmount(bytes32 key) external view returns (uint256) { + return rateLimitData[key].lastAmount; + } + + function getLastUpdated(bytes32 key) external view returns (uint256) { + return rateLimitData[key].lastUpdated; + } +} From afcb0ad63110bf75bb16ba891829354d408ba2d3 Mon Sep 17 00:00:00 2001 From: sunbreak1211 Date: Fri, 13 Feb 2026 17:24:46 -0300 Subject: [PATCH 2/5] Certora: Timelock --- Makefile | 1 + certora/Timelock.conf | 12 + certora/Timelock.spec | 629 ++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 642 insertions(+) create mode 100644 certora/Timelock.conf create mode 100644 certora/Timelock.spec diff --git a/Makefile b/Makefile index 907e875..daa41a2 100644 --- a/Makefile +++ b/Makefile @@ -1,3 +1,4 @@ PATH := ~/.solc-select/artifacts/solc-0.8.24:$(PATH) certora-state :; PATH=${PATH} certoraRun certora/BeamState.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,) certora-configurator :; PATH=${PATH} certoraRun certora/Configurator.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,) +certora-timelock :; PATH=${PATH} certoraRun certora/Timelock.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,) diff --git a/certora/Timelock.conf b/certora/Timelock.conf new file mode 100644 index 0000000..869ff1d --- /dev/null +++ b/certora/Timelock.conf @@ -0,0 +1,12 @@ +{ + "files": ["src/timelock/Timelock.sol"], + "verify": "Timelock:certora/Timelock.spec", + "solc": "solc-0.8.24", + "optimistic_loop": true, + "loop_iter": 5, + "rule_sanity": "basic", + "multi_assert_check": true, + "optimistic_hashing": true, + "parametric_contracts": ["Timelock"], + "msg": "Timelock" +} diff --git a/certora/Timelock.spec b/certora/Timelock.spec new file mode 100644 index 0000000..96740ab --- /dev/null +++ b/certora/Timelock.spec @@ -0,0 +1,629 @@ +// SPDX-FileCopyrightText: © 2026 Dai Foundation +// SPDX-License-Identifier: AGPL-3.0-or-later +// +// Timelock.spec -- Formal verification spec for Timelock + +using Timelock as timelock; + +// --- Methods block --- + +methods { + // Timelock linked list getters + function getFirstOperationId() external returns (bytes32) envfree; + function getLastOperationId() external returns (bytes32) envfree; + function getOperationsCount() external returns (uint256) envfree; + function getPrevOperationId(bytes32) external returns (bytes32) envfree; + function getNextOperationId(bytes32) external returns (bytes32) envfree; + function getOperationExists(bytes32) external returns (bool) envfree; + + // Timelock operation data getters + function getOperationLength(bytes32) external returns (uint256) envfree; + function getOperationTarget(bytes32, uint256) external returns (address) envfree; + function getOperationValue(bytes32, uint256) external returns (uint256) envfree; + function getOperationPredecessor(bytes32) external returns (bytes32) envfree; + function getOperationSalt(bytes32) external returns (bytes32) envfree; + + // Inherited from Pausable + function paused() external returns (bool) envfree; + + // Inherited from TimelockController + function getMinDelay() external returns (uint256) envfree; + function getTimestamp(bytes32) external returns (uint256) envfree; + function hashOperationBatch(address[], uint256[], bytes[], bytes32, bytes32) external returns (bytes32) envfree; + function isOperationReady(bytes32, uint256) external returns (bool); + + // Inherited from AccessControl + function hasRole(bytes32, address) external returns (bool) envfree; + function PAUSER_ROLE() external returns (bytes32) envfree; + function PROPOSER_ROLE() external returns (bytes32) envfree; + function CANCELLER_ROLE() external returns (bytes32) envfree; + function EXECUTOR_ROLE() external returns (bytes32) envfree; + function DEFAULT_ADMIN_ROLE() external returns (bytes32) envfree; + + // // External call summaries - treat external calls as non-deterministic + // function _._ external => NONDET; +} + +// --- Definitions --- + +definition DONE_TIMESTAMP() returns uint256 = 1; + +// --- Storage Affected Rule --- + +rule storageAffected(method f) filtered { f -> !f.isView } { + env e; + calldataarg args; + + bytes32 anyId; + + // Linked list state + bytes32 firstBefore = getFirstOperationId(); + bytes32 lastBefore = getLastOperationId(); + uint256 countBefore = getOperationsCount(); + bytes32 prevBefore = getPrevOperationId(anyId); + bytes32 nextBefore = getNextOperationId(anyId); + bool existsBefore = getOperationExists(anyId); + + // Operation data + uint256 lengthBefore = getOperationLength(anyId); + bytes32 predecessorBefore = getOperationPredecessor(anyId); + bytes32 saltBefore = getOperationSalt(anyId); + + // Pausable state + bool pausedBefore = paused(); + + // TimelockController state + uint256 minDelayBefore = getMinDelay(); + + f(e, args); + + // Linked list state + bytes32 firstAfter = getFirstOperationId(); + bytes32 lastAfter = getLastOperationId(); + uint256 countAfter = getOperationsCount(); + bytes32 prevAfter = getPrevOperationId(anyId); + bytes32 nextAfter = getNextOperationId(anyId); + bool existsAfter = getOperationExists(anyId); + + // Operation data + uint256 lengthAfter = getOperationLength(anyId); + bytes32 predecessorAfter = getOperationPredecessor(anyId); + bytes32 saltAfter = getOperationSalt(anyId); + + // Pausable state + bool pausedAfter = paused(); + + // TimelockController state + uint256 minDelayAfter = getMinDelay(); + + // Linked list can only be modified by scheduleBatch, cancel, executeBatch + assert (firstAfter != firstBefore || lastAfter != lastBefore || countAfter != countBefore || + existsAfter != existsBefore || prevAfter != prevBefore || nextAfter != nextBefore) => + f.selector == sig:scheduleBatch(address[],uint256[],bytes[],bytes32,bytes32,uint256).selector || + f.selector == sig:cancel(bytes32).selector || + f.selector == sig:executeBatch(address[],uint256[],bytes[],bytes32,bytes32).selector; + + // Operation data can only be modified by scheduleBatch, cancel, executeBatch + assert (lengthAfter != lengthBefore || predecessorAfter != predecessorBefore || saltAfter != saltBefore) => + f.selector == sig:scheduleBatch(address[],uint256[],bytes[],bytes32,bytes32,uint256).selector || + f.selector == sig:cancel(bytes32).selector || + f.selector == sig:executeBatch(address[],uint256[],bytes[],bytes32,bytes32).selector; + + // paused can only be modified by pause, unpause + assert pausedAfter != pausedBefore => + f.selector == sig:pause().selector || + f.selector == sig:unpause().selector; + + // minDelay can only be modified by updateDelayImmediately (and inherited updateDelay, but it requires self-call) + assert minDelayAfter != minDelayBefore => + f.selector == sig:updateDelay(uint256).selector || + f.selector == sig:updateDelayImmediately(uint256).selector; +} + +// --- Pausing rules --- + +rule pause() { + env e; + + pause(e); + + assert paused() == true; +} + +rule pause_revert() { + env e; + + bool isPauser = hasRole(PAUSER_ROLE(), e.msg.sender); + bool isPausedBefore = paused(); + + pause@withrevert(e); + + bool revert1 = e.msg.value > 0; + bool revert2 = !isPauser; + bool revert3 = isPausedBefore; + + assert lastReverted <=> revert1 || revert2 || revert3; +} + +rule unpause() { + env e; + + unpause(e); + + assert paused() == false; +} + +rule unpause_revert() { + env e; + + bool isAdmin = hasRole(DEFAULT_ADMIN_ROLE(), e.msg.sender); + bool isPausedBefore = paused(); + + unpause@withrevert(e); + + bool revert1 = e.msg.value > 0; + bool revert2 = !isAdmin; + bool revert3 = !isPausedBefore; + + assert lastReverted <=> revert1 || revert2 || revert3; +} + +// --- Schedule rules --- + +rule schedule_always_reverts(address target, uint256 value, bytes payload, bytes32 predecessor, bytes32 salt, uint256 delay) { + env e; + + schedule@withrevert(e, target, value, payload, predecessor, salt, delay); + + assert lastReverted; +} + +rule scheduleBatch_adds_to_list( + address[] targets, + uint256[] values, + bytes[] payloads, + bytes32 predecessor, + bytes32 salt, + uint256 delay +) { + env e; + + uint256 countBefore = getOperationsCount(); + bytes32 id = hashOperationBatch(targets, values, payloads, predecessor, salt); + + require !getOperationExists(id); + + scheduleBatch(e, targets, values, payloads, predecessor, salt, delay); + + uint256 countAfter = getOperationsCount(); + bool existsAfter = getOperationExists(id); + bytes32 lastAfter = getLastOperationId(); + + assert countAfter == countBefore + 1; + assert existsAfter == true; + assert lastAfter == id; +} + +rule scheduleBatch_no_side_effects( + address[] targets, + uint256[] values, + bytes[] payloads, + bytes32 predecessor, + bytes32 salt, + uint256 delay +) { + env e; + + bytes32 otherId; + bytes32 id = hashOperationBatch(targets, values, payloads, predecessor, salt); + require otherId != id; + + bool otherExistsBefore = getOperationExists(otherId); + bytes32 otherPrevBefore = getPrevOperationId(otherId); + uint256 otherLengthBefore = getOperationLength(otherId); + bytes32 otherPredecessorBefore = getOperationPredecessor(otherId); + bytes32 otherSaltBefore = getOperationSalt(otherId); + + scheduleBatch(e, targets, values, payloads, predecessor, salt, delay); + + bool otherExistsAfter = getOperationExists(otherId); + bytes32 otherPrevAfter = getPrevOperationId(otherId); + uint256 otherLengthAfter = getOperationLength(otherId); + bytes32 otherPredecessorAfter = getOperationPredecessor(otherId); + bytes32 otherSaltAfter = getOperationSalt(otherId); + + // Note: next pointer of the previous last element will change if otherId was the last element + assert otherExistsAfter == otherExistsBefore; + assert otherPrevAfter == otherPrevBefore; + assert otherLengthAfter == otherLengthBefore; + assert otherPredecessorAfter == otherPredecessorBefore; + assert otherSaltAfter == otherSaltBefore; +} + +rule scheduleBatch_revert( + address[] targets, + uint256[] values, + bytes[] payloads, + bytes32 predecessor, + bytes32 salt, + uint256 delay +) { + env e; + + bool isPaused = paused(); + bool isProposer = hasRole(PROPOSER_ROLE(), e.msg.sender); + bytes32 id = hashOperationBatch(targets, values, payloads, predecessor, salt); + bool isOp = isOperation(e, id); + uint256 minDelay = getMinDelay(); + + // Check array lengths match + require targets.length == values.length; + require targets.length == payloads.length; + + scheduleBatch@withrevert(e, targets, values, payloads, predecessor, salt, delay); + + bool revert1 = e.msg.value > 0; + bool revert2 = isPaused; + bool revert3 = !isProposer; + bool revert4 = isOp; // Operation already exists in TimelockController + bool revert5 = delay < minDelay; + // revert6: self-call check - one of targets == address(this) + // revert7: linked list add fails (id == 0 or already exists) - covered by revert4 + + assert revert1 || revert2 || revert3 || revert4 || revert5 => lastReverted; +} + +// --- Cancel rules --- + +rule cancel_removes_from_list(bytes32 id) { + env e; + + uint256 countBefore = getOperationsCount(); + + require getOperationExists(id); + + cancel(e, id); + + uint256 countAfter = getOperationsCount(); + bool existsAfter = getOperationExists(id); + uint256 lengthAfter = getOperationLength(id); + + assert countAfter == countBefore - 1; + assert existsAfter == false; + assert lengthAfter == 0; +} + +rule cancel_no_side_effects(bytes32 id) { + env e; + + bytes32 otherId; + require otherId != id; + + bool otherExistsBefore = getOperationExists(otherId); + uint256 otherLengthBefore = getOperationLength(otherId); + bytes32 otherPredecessorBefore = getOperationPredecessor(otherId); + bytes32 otherSaltBefore = getOperationSalt(otherId); + + cancel(e, id); + + bool otherExistsAfter = getOperationExists(otherId); + uint256 otherLengthAfter = getOperationLength(otherId); + bytes32 otherPredecessorAfter = getOperationPredecessor(otherId); + bytes32 otherSaltAfter = getOperationSalt(otherId); + + // Note: prev/next pointers of adjacent nodes may change + assert otherExistsAfter == otherExistsBefore; + assert otherLengthAfter == otherLengthBefore; + assert otherPredecessorAfter == otherPredecessorBefore; + assert otherSaltAfter == otherSaltBefore; +} + +rule cancel_revert(bytes32 id) { + env e; + + bool isPaused = paused(); + bool isCanceller = hasRole(CANCELLER_ROLE(), e.msg.sender); + bool isPending = isOperationPending(e, id); + bool opExists = getOperationExists(id); + + cancel@withrevert(e, id); + + bool revert1 = e.msg.value > 0; + bool revert2 = isPaused; + bool revert3 = !isCanceller; + bool revert4 = !isPending; + bool revert5 = !opExists; + + assert revert1 || revert2 || revert3 || revert4 || revert5 => lastReverted; +} + +rule cancel_revert_length_0(bytes32 id) { + env e; + + bool isPaused = paused(); + bool isCanceller = hasRole(CANCELLER_ROLE(), e.msg.sender); + bool isPending = isOperationPending(e, id); + bool opExists = getOperationExists(id); + + require getOperationsCount() > 0; + + require currentContract._operations[id].payloads.length == 0; + + cancel@withrevert(e, id); + + bool revert1 = e.msg.value > 0; + bool revert2 = isPaused; + bool revert3 = !isCanceller; + bool revert4 = !isPending; + bool revert5 = !opExists; + + assert lastReverted <=> revert1 || revert2 || revert3 || revert4 || revert5; +} + +// --- Execute rules --- + +rule execute_always_reverts(address target, uint256 value, bytes payload, bytes32 predecessor, bytes32 salt) { + env e; + + execute@withrevert(e, target, value, payload, predecessor, salt); + + assert lastReverted; +} + +rule executeBatch_removes_from_list( + address[] targets, + uint256[] values, + bytes[] payloads, + bytes32 predecessor, + bytes32 salt +) { + env e; + + uint256 countBefore = getOperationsCount(); + bytes32 id = hashOperationBatch(targets, values, payloads, predecessor, salt); + + require getOperationExists(id); + + executeBatch(e, targets, values, payloads, predecessor, salt); + + uint256 countAfter = getOperationsCount(); + bool existsAfter = getOperationExists(id); + uint256 lengthAfter = getOperationLength(id); + + assert countAfter == countBefore - 1; + assert existsAfter == false; + assert lengthAfter == 0; +} + +rule executeBatch_revert( + address[] targets, + uint256[] values, + bytes[] payloads, + bytes32 predecessor, + bytes32 salt +) { + env e; + + bool isPaused = paused(); + bytes32 id = hashOperationBatch(targets, values, payloads, predecessor, salt); + bool isReady = isOperationReady(e, id); + bool predecessorDone = predecessor == to_bytes32(0) || isOperationDone(e, predecessor); + + // Check array lengths match + require targets.length == values.length; + require targets.length == payloads.length; + + executeBatch@withrevert(e, targets, values, payloads, predecessor, salt); + + bool revert1 = e.msg.value > 0 && e.msg.value != values[0]; // Only fails if value mismatch + bool revert2 = isPaused; + bool revert3 = !isReady; + bool revert4 = !predecessorDone; + // revert5: external call fails + // revert6: linked list remove fails (doesn't exist) + + assert revert2 || revert3 || revert4 => lastReverted; +} + +// --- Delay management rules --- + +rule updateDelayImmediately(uint256 newDelay) { + env e; + + updateDelayImmediately(e, newDelay); + + uint256 minDelayAfter = getMinDelay(); + + assert minDelayAfter == newDelay; +} + +rule updateDelayImmediately_revert(uint256 newDelay) { + env e; + + bool isAdmin = hasRole(DEFAULT_ADMIN_ROLE(), e.msg.sender); + + updateDelayImmediately@withrevert(e, newDelay); + + bool revert1 = e.msg.value > 0; + bool revert2 = !isAdmin; + + assert lastReverted <=> revert1 || revert2; +} + +// --- Linked list invariants --- + +invariant emptyListConsistency() + getOperationsCount() == 0 <=> (getFirstOperationId() == to_bytes32(0) && getLastOperationId() == to_bytes32(0)) + { + preserved scheduleBatch(address[] targets, uint256[] values, bytes[] payloads, bytes32 predecessor, bytes32 salt, uint256 delay) with (env e) { + // Hash cannot be zero for valid operations + require hashOperationBatch(targets, values, payloads, predecessor, salt) != to_bytes32(0); + } + } + +// // --- Linked list structure invariants --- + +// // First element has no predecessor +// invariant firstHasNoPrev() +// getFirstOperationId() != to_bytes32(0) => getPrevOperationId(getFirstOperationId()) == to_bytes32(0) +// { +// preserved scheduleBatch(address[] targets, uint256[] values, bytes[] payloads, bytes32 predecessor, bytes32 salt, uint256 delay) with (env e) { +// require hashOperationBatch(targets, values, payloads, predecessor, salt) != to_bytes32(0); +// } +// } + +// // Last element has no successor +// invariant lastHasNoNext() +// getLastOperationId() != to_bytes32(0) => getNextOperationId(getLastOperationId()) == to_bytes32(0) +// { +// preserved scheduleBatch(address[] targets, uint256[] values, bytes[] payloads, bytes32 predecessor, bytes32 salt, uint256 delay) with (env e) { +// require hashOperationBatch(targets, values, payloads, predecessor, salt) != to_bytes32(0); +// } +// } + +// // If an operation exists, count must be positive +// invariant existsImpliesPositiveCount(bytes32 id) +// getOperationExists(id) => getOperationsCount() > 0 +// { +// preserved scheduleBatch(address[] targets, uint256[] values, bytes[] payloads, bytes32 predecessor, bytes32 salt, uint256 delay) with (env e) { +// require hashOperationBatch(targets, values, payloads, predecessor, salt) != to_bytes32(0); +// } +// } + +// // If operation exists in linked list, it has data (at least one target) +// invariant operationExistsImpliesData(bytes32 id) +// getOperationExists(id) => getOperationLength(id) > 0 +// { +// preserved scheduleBatch(address[] targets, uint256[] values, bytes[] payloads, bytes32 predecessor, bytes32 salt, uint256 delay) with (env e) { +// require hashOperationBatch(targets, values, payloads, predecessor, salt) != to_bytes32(0); +// require targets.length > 0; +// } +// } + +// --- Access control rules --- + +rule onlyPauserCanPause() { + env e; + + require !hasRole(PAUSER_ROLE(), e.msg.sender); + + pause@withrevert(e); + + assert lastReverted; +} + +rule onlyAdminCanUnpause() { + env e; + + require !hasRole(DEFAULT_ADMIN_ROLE(), e.msg.sender); + + unpause@withrevert(e); + + assert lastReverted; +} + +rule onlyAdminCanUpdateDelay() { + env e; + uint256 newDelay; + + require !hasRole(DEFAULT_ADMIN_ROLE(), e.msg.sender); + + updateDelayImmediately@withrevert(e, newDelay); + + assert lastReverted; +} + +rule onlyProposerCanSchedule( + address[] targets, + uint256[] values, + bytes[] payloads, + bytes32 predecessor, + bytes32 salt, + uint256 delay +) { + env e; + + require !hasRole(PROPOSER_ROLE(), e.msg.sender); + + scheduleBatch@withrevert(e, targets, values, payloads, predecessor, salt, delay); + + assert lastReverted; +} + +rule onlyCancellerCanCancel(bytes32 id) { + env e; + + require !hasRole(CANCELLER_ROLE(), e.msg.sender); + + cancel@withrevert(e, id); + + assert lastReverted; +} + +// --- Paused state rules --- + +rule whenPausedScheduleReverts( + address[] targets, + uint256[] values, + bytes[] payloads, + bytes32 predecessor, + bytes32 salt, + uint256 delay +) { + env e; + + require paused(); + + scheduleBatch@withrevert(e, targets, values, payloads, predecessor, salt, delay); + + assert lastReverted; +} + +rule whenPausedCancelReverts(bytes32 id) { + env e; + + require paused(); + + cancel@withrevert(e, id); + + assert lastReverted; +} + +rule whenPausedExecuteReverts( + address[] targets, + uint256[] values, + bytes[] payloads, + bytes32 predecessor, + bytes32 salt +) { + env e; + + require paused(); + + executeBatch@withrevert(e, targets, values, payloads, predecessor, salt); + + assert lastReverted; +} + +// --- Self-call prevention --- + +// This rule verifies that scheduleBatch reverts when any target is the timelock itself +// Note: This is a property check that should be verified +rule selfCallPrevention( + address[] targets, + uint256[] values, + bytes[] payloads, + bytes32 predecessor, + bytes32 salt, + uint256 delay +) { + env e; + + // Assume first target is the contract itself + require targets.length > 0; + require targets[0] == currentContract; + + scheduleBatch@withrevert(e, targets, values, payloads, predecessor, salt, delay); + + assert lastReverted; +} From 1ec7306a6659face35c0013c437b2e304da9c91c Mon Sep 17 00:00:00 2001 From: sunbreak1211 Date: Fri, 4 Sep 2026 19:46:15 -0300 Subject: [PATCH 3/5] Update specs --- .github/workflows/certora.yml | 47 +++ Makefile | 1 + certora/BeamState.spec | 82 +++-- certora/Configurator.conf | 15 +- certora/Configurator.spec | 107 ++++--- certora/PASMom.conf | 12 + certora/PASMom.spec | 166 ++++++++++ certora/Timelock.conf | 16 +- certora/Timelock.spec | 429 ++++++++++++++++---------- certora/harness/ControllerHarness.sol | 19 ++ 10 files changed, 635 insertions(+), 259 deletions(-) create mode 100644 .github/workflows/certora.yml create mode 100644 certora/PASMom.conf create mode 100644 certora/PASMom.spec create mode 100644 certora/harness/ControllerHarness.sol diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml new file mode 100644 index 0000000..4fc9d15 --- /dev/null +++ b/.github/workflows/certora.yml @@ -0,0 +1,47 @@ +name: Certora + +on: [push, pull_request] + +jobs: + certora: + name: Certora + runs-on: ubuntu-latest + strategy: + fail-fast: false + matrix: + pas: + - state + - configurator + - timelock + - mom + + steps: + - name: Checkout + uses: actions/checkout@v4 + with: + submodules: recursive + + - uses: actions/setup-java@v2 + with: + distribution: 'zulu' + java-version: '11' + java-package: jre + + - name: Set up Python 3.13 + uses: actions/setup-python@v5 + with: + python-version: '3.13' + + - name: Install solc-select + run: pip3 install solc-select + + - name: Solc Select 0.8.24 + run: solc-select install 0.8.24 + + - name: Install Certora + run: pip3 install certora-cli-beta + + - name: Verify ${{ matrix.pas }} + run: make certora-${{ matrix.pas }} results=1 + env: + CERTORAKEY: ${{ secrets.CERTORAKEY }} diff --git a/Makefile b/Makefile index daa41a2..d62e2ca 100644 --- a/Makefile +++ b/Makefile @@ -2,3 +2,4 @@ PATH := ~/.solc-select/artifacts/solc-0.8.24:$(PATH) certora-state :; PATH=${PATH} certoraRun certora/BeamState.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,) certora-configurator :; PATH=${PATH} certoraRun certora/Configurator.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,) certora-timelock :; PATH=${PATH} certoraRun certora/Timelock.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,) +certora-mom :; PATH=${PATH} certoraRun certora/PASMom.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,) diff --git a/certora/BeamState.spec b/certora/BeamState.spec index 527cca2..21ca768 100644 --- a/certora/BeamState.spec +++ b/certora/BeamState.spec @@ -1,7 +1,4 @@ -// SPDX-FileCopyrightText: © 2026 Dai Foundation -// SPDX-License-Identifier: AGPL-3.0-or-later -// -// BeamState.spec -- Formal verification spec for BeamState +// BeamState.spec using BeamState as beamState; @@ -50,36 +47,36 @@ rule storageAffected(method f) filtered { f -> !f.isView } { uint256 wardsBefore = wards(anyAddr); bytes32 userRolesBefore = userRoles(anyAddr); bytes32 actionsRolesBefore = actionsRoles(anySig); - bool stoppedBefore = stopped(); uint256 rateLimitsBefore = rateLimits(anyAddr); uint256 controllersBefore = controllers(anyAddr); uint256 cBeamsBefore = cBeams(anyAddr); uint256 rateLimitsCBeamsBefore = rateLimitsCBeams(anyAddr, anyAddr2); uint256 controllersCBeamsBefore = controllersCBeams(anyAddr, anyAddr2); - uint256 hopBefore = hop(anyAddr); - uint256 maxChangeBefore = maxChange(anyAddr); uint256 initRateLimitsMaxAmountBefore; uint256 initRateLimitsSlopeBefore; initRateLimitsMaxAmountBefore, initRateLimitsSlopeBefore = initRateLimits(anyKey, anyAddr); uint256 initControllerActionsBefore = initControllerActions(anyKey, anyAddr); + uint256 hopBefore = hop(anyAddr); + uint256 maxChangeBefore = maxChange(anyAddr); + bool stoppedBefore = stopped(); f(e, args); uint256 wardsAfter = wards(anyAddr); bytes32 userRolesAfter = userRoles(anyAddr); bytes32 actionsRolesAfter = actionsRoles(anySig); - bool stoppedAfter = stopped(); uint256 rateLimitsAfter = rateLimits(anyAddr); uint256 controllersAfter = controllers(anyAddr); uint256 cBeamsAfter = cBeams(anyAddr); uint256 rateLimitsCBeamsAfter = rateLimitsCBeams(anyAddr, anyAddr2); uint256 controllersCBeamsAfter = controllersCBeams(anyAddr, anyAddr2); - uint256 hopAfter = hop(anyAddr); - uint256 maxChangeAfter = maxChange(anyAddr); uint256 initRateLimitsMaxAmountAfter; uint256 initRateLimitsSlopeAfter; initRateLimitsMaxAmountAfter, initRateLimitsSlopeAfter = initRateLimits(anyKey, anyAddr); uint256 initControllerActionsAfter = initControllerActions(anyKey, anyAddr); + uint256 hopAfter = hop(anyAddr); + uint256 maxChangeAfter = maxChange(anyAddr); + bool stoppedAfter = stopped(); assert wardsAfter != wardsBefore => f.selector == sig:rely(address).selector || @@ -88,9 +85,6 @@ rule storageAffected(method f) filtered { f -> !f.isView } { f.selector == sig:setUserRole(address, uint8, bool).selector; assert actionsRolesAfter != actionsRolesBefore => f.selector == sig:setRoleAction(uint8, bytes4, bool).selector; - assert stoppedAfter != stoppedBefore => - f.selector == sig:stop().selector || - f.selector == sig:start().selector; assert rateLimitsAfter != rateLimitsBefore => f.selector == sig:addRateLimits(address).selector || f.selector == sig:delRateLimits(address).selector; @@ -106,46 +100,21 @@ rule storageAffected(method f) filtered { f -> !f.isView } { assert controllersCBeamsAfter != controllersCBeamsBefore => f.selector == sig:setCBeamForController(address, address).selector || f.selector == sig:unsetCBeamForController(address, address).selector; - assert hopAfter != hopBefore => - f.selector == sig:setHop(address, uint256).selector; - assert maxChangeAfter != maxChangeBefore => - f.selector == sig:setMaxChange(address, uint256).selector; assert (initRateLimitsMaxAmountAfter != initRateLimitsMaxAmountBefore || initRateLimitsSlopeAfter != initRateLimitsSlopeBefore) => f.selector == sig:addInitRateLimits(bytes32, address, uint256, uint256).selector || f.selector == sig:delInitRateLimits(bytes32, address).selector; assert initControllerActionsAfter != initControllerActionsBefore => f.selector == sig:addInitControllerActions(bytes, address).selector || f.selector == sig:delInitControllerActions(bytes32, address).selector; + assert hopAfter != hopBefore => + f.selector == sig:setHop(address, uint256).selector; + assert maxChangeAfter != maxChangeBefore => + f.selector == sig:setMaxChange(address, uint256).selector; + assert stoppedAfter != stoppedBefore => + f.selector == sig:stop().selector || + f.selector == sig:start().selector; } -// --- Invariants --- - -// Binary value invariants -invariant wardsIsBinary(address usr) - wards(usr) == 0 || wards(usr) == 1; - -invariant rateLimitsIsBinary(address rl) - rateLimits(rl) == 0 || rateLimits(rl) == 1; - -invariant controllersIsBinary(address c) - controllers(c) == 0 || controllers(c) == 1; - -invariant cBeamsIsBinary(address cb) - cBeams(cb) == 0 || cBeams(cb) == 1; - -invariant rateLimitsCBeamsIsBinary(address rl, address cb) - rateLimitsCBeams(rl, cb) == 0 || rateLimitsCBeams(rl, cb) == 1; - -invariant controllersCBeamsIsBinary(address c, address cb) - controllersCBeams(c, cb) == 0 || controllersCBeams(c, cb) == 1; - -invariant initControllerActionsIsBinary(bytes32 key, address c) - initControllerActions(key, c) == 0 || initControllerActions(key, c) == 1; - -// maxChange must be >= WAD when set (enforced by setMaxChange require) -invariant maxChangeMinimum(address rl) - maxChange(rl) == 0 || maxChange(rl) >= WAD(); - // --- View function correctness --- // hasUserRole correctly checks the bit in userRoles @@ -186,6 +155,24 @@ rule getMaxChangeCorrectness(address rl) { assert maxChangeRl == 0 => result == maxChangeZero; } +// getInitRateLimits returns initRateLimits[key][rl] if set, otherwise falls back to initRateLimits[key][address(0)] +rule getInitRateLimitsCorrectness(bytes32 key, address rl) { + uint256 initRateLimitsKeyRlMaxAmount; + uint256 initRateLimitsKeyRlSlope; + initRateLimitsKeyRlMaxAmount, initRateLimitsKeyRlSlope = initRateLimits(key, rl); + + uint256 initRateLimitsKeyZeroMaxAmount; + uint256 initRateLimitsKeyZeroSlope; + initRateLimitsKeyZeroMaxAmount, initRateLimitsKeyZeroSlope = initRateLimits(key, 0); + + BeamState.DefaultRateLimits result = getInitRateLimits(key, rl); + + assert (initRateLimitsKeyRlMaxAmount != 0 || initRateLimitsKeyRlSlope != 0) => + result.maxAmount == initRateLimitsKeyRlMaxAmount && result.slope == initRateLimitsKeyRlSlope; + assert (initRateLimitsKeyRlMaxAmount == 0 && initRateLimitsKeyRlSlope == 0) => + result.maxAmount == initRateLimitsKeyZeroMaxAmount && result.slope == initRateLimitsKeyZeroSlope; +} + // isControllerActionEnabled checks address(0) OR specific controller rule isControllerActionEnabledCorrectness(bytes32 key, address controller) { uint256 initControllerActionsKeyZero = initControllerActions(key, 0); @@ -455,7 +442,7 @@ rule setMaxChange_revert(address rateLimits_, uint256 value) { bool revert1 = e.msg.value > 0; bool revert2 = (userRolesSender & actionsRolesSetMaxChange == to_bytes32(0)) && wardsSender != 1; - bool revert3 = value < WAD(); + bool revert3 = value > 0 && value < WAD(); assert lastReverted <=> revert1 || revert2 || revert3; } @@ -912,11 +899,12 @@ rule addInitControllerActions(bytes data, address controller) { uint256 initControllerActionsOtherKeyOtherControllerBefore = initControllerActions(otherKey, otherController); - addInitControllerActions(e, data, controller); + bytes32 retKey = addInitControllerActions(e, data, controller); uint256 initControllerActionsKeyControllerAfter = initControllerActions(key, controller); uint256 initControllerActionsOtherKeyOtherControllerAfter = initControllerActions(otherKey, otherController); + assert retKey == key; assert initControllerActionsKeyControllerAfter == 1; assert initControllerActionsOtherKeyOtherControllerAfter == initControllerActionsOtherKeyOtherControllerBefore; } diff --git a/certora/Configurator.conf b/certora/Configurator.conf index 128087a..e72f44c 100644 --- a/certora/Configurator.conf +++ b/certora/Configurator.conf @@ -1,12 +1,21 @@ { - "files": ["src/Configurator.sol", "src/BeamState.sol", "certora/harness/RateLimitsHarness.sol"], + "files": [ + "src/Configurator.sol", + "src/BeamState.sol", + "certora/harness/RateLimitsHarness.sol", + "certora/harness/ControllerHarness.sol" + ], "verify": "Configurator:certora/Configurator.spec", - "link": ["Configurator:beamState=BeamState"], + "link": [ + "Configurator:beamState=BeamState" + ], "solc": "solc-0.8.24", "optimistic_loop": true, "rule_sanity": "basic", "multi_assert_check": true, "optimistic_hashing": true, - "parametric_contracts": ["Configurator"], + "parametric_contracts": [ + "Configurator" + ], "msg": "Configurator" } diff --git a/certora/Configurator.spec b/certora/Configurator.spec index 8b77465..fa1d1fc 100644 --- a/certora/Configurator.spec +++ b/certora/Configurator.spec @@ -1,11 +1,9 @@ -// SPDX-FileCopyrightText: © 2026 Dai Foundation -// SPDX-License-Identifier: AGPL-3.0-or-later -// -// Configurator.spec -- Formal verification spec for Configurator +// Configurator.spec using Configurator as configurator; using BeamState as beamState; using RateLimitsHarness as rateLimitsHarness; +using ControllerHarness as controllerHarness; // --- Methods block --- @@ -31,22 +29,40 @@ methods { function rateLimitsHarness.getLastAmount(bytes32) external returns (uint256) envfree; function rateLimitsHarness.getLastUpdated(bytes32) external returns (uint256) envfree; + // ControllerHarness functions + function controllerHarness.calls() external returns (uint256) envfree; + function _.getRateLimitData(bytes32) external => DISPATCHER(true); function _.getCurrentRateLimit(bytes32) external => DISPATCHER(true); function _.setRateLimitData(bytes32, uint256, uint256, uint256, uint256) external => DISPATCHER(true); function _.setUnlimitedRateLimitData(bytes32) external => DISPATCHER(true); + + // Configurator forwards a low-level call with symbolic calldata to an arbitrary controller. + // optimistic=true replaces the fallthrough branch with ASSUME FALSE, forcing the call to resolve + // to ControllerHarness.action() instead of letting the solver escape through `default`. + // use_fallback=true routes every non-matching sighash to the harness fallback, so `data` stays + // fully symbolic instead of being pinned to action()'s selector. + // Neither harness entry point can revert (the increments are unchecked), so `require(ok)` is + // proven not to fire rather than assumed away. + unresolved external in Configurator.callControllerAction(address, bytes) => DISPATCH(optimistic=true) [ + ControllerHarness.action() + ]; } // --- Definitions --- definition WAD() returns mathint = 10^18; -// Helper to compute max of two values -definition _max(uint256 x, uint256 y) returns uint256 = x > y ? x : y; - // Helper to compute min of two values definition _min(uint256 x, uint256 y) returns uint256 = x < y ? x : y; +// Mirrors the contract's unlimited branch condition: +// defMaxAmount == type(uint256).max && defSlope == 0 || +// current.maxAmount == type(uint256).max && current.slope == 0 && defMaxAmount == 0 && defSlope == 0 +definition isUnlimited(uint256 defMaxAmount, uint256 defSlope, uint256 curMaxAmount, uint256 curSlope) returns bool = + (defMaxAmount == max_uint256 && defSlope == 0) || + (curMaxAmount == max_uint256 && curSlope == 0 && defMaxAmount == 0 && defSlope == 0); + // --- Storage Affected Rule --- rule storageAffected(method f) filtered { f -> !f.isView } { @@ -68,14 +84,17 @@ rule storageAffected(method f) filtered { f -> !f.isView } { // --- setRateLimit rules --- -// Verifies that setRateLimit correctly handles the unlimited case +// Verifies that setRateLimit correctly handles the unlimited case, covering both the +// BeamState-registered branch and the pre-existing-unlimited-key branch rule setRateLimit_unlimited(bytes32 key, uint256 maxAmount, uint256 slope) { env e; - // Setup: unlimited defaults (maxAmount == type(uint256).max && slope == 0) BeamState.DefaultRateLimits defLimits = beamState.getInitRateLimits(key, rateLimitsHarness); - require defLimits.maxAmount == max_uint256; - require defLimits.slope == 0; + uint256 currentMaxAmount = rateLimitsHarness.getMaxAmount(key); + uint256 currentSlope = rateLimitsHarness.getSlope(key); + + // Setup: the key is locked as unlimited + require isUnlimited(defLimits.maxAmount, defLimits.slope, currentMaxAmount, currentSlope); // Pre-state uint256 zzzBefore = zzz(rateLimitsHarness, key); @@ -88,6 +107,8 @@ rule setRateLimit_unlimited(bytes32 key, uint256 maxAmount, uint256 slope) { uint256 lastAmountAfter = rateLimitsHarness.getLastAmount(key); uint256 zzzAfter = zzz(rateLimitsHarness, key); + // A successful call on a locked key can only have carried (max, 0): it can never be lowered + assert maxAmount == max_uint256 && slope == 0; // When unlimited: setUnlimitedRateLimitData sets maxAmount = max_uint256, slope = 0, lastAmount = max_uint256 assert maxAmountAfter == max_uint256; assert slopeAfter == 0; @@ -100,14 +121,15 @@ rule setRateLimit_unlimited(bytes32 key, uint256 maxAmount, uint256 slope) { rule setRateLimit_decrement(bytes32 key, uint256 maxAmount, uint256 slope) { env e; - // Setup: NOT unlimited defaults + // Setup: the key is NOT locked as unlimited BeamState.DefaultRateLimits defLimits = beamState.getInitRateLimits(key, rateLimitsHarness); - require !(defLimits.maxAmount == max_uint256 && defLimits.slope == 0); // Current values uint256 currentMaxAmount = rateLimitsHarness.getMaxAmount(key); uint256 currentSlope = rateLimitsHarness.getSlope(key); + require !isUnlimited(defLimits.maxAmount, defLimits.slope, currentMaxAmount, currentSlope); + // This is a decrement (both params <= current) require maxAmount <= currentMaxAmount; require slope <= currentSlope; @@ -133,14 +155,15 @@ rule setRateLimit_decrement(bytes32 key, uint256 maxAmount, uint256 slope) { rule setRateLimit_increment(bytes32 key, uint256 maxAmount, uint256 slope) { env e; - // Setup: NOT unlimited defaults + // Setup: the key is NOT locked as unlimited BeamState.DefaultRateLimits defLimits = beamState.getInitRateLimits(key, rateLimitsHarness); - require !(defLimits.maxAmount == max_uint256 && defLimits.slope == 0); // Current values uint256 currentMaxAmount = rateLimitsHarness.getMaxAmount(key); uint256 currentSlope = rateLimitsHarness.getSlope(key); + require !isUnlimited(defLimits.maxAmount, defLimits.slope, currentMaxAmount, currentSlope); + // This is an increment (at least one param > current) require maxAmount > currentMaxAmount || slope > currentSlope; @@ -162,9 +185,12 @@ rule setRateLimit_increment(bytes32 key, uint256 maxAmount, uint256 slope) { rule setRateLimit_lastAmount(bytes32 key, uint256 maxAmount, uint256 slope) { env e; - // Setup: NOT unlimited defaults + // Setup: the key is NOT locked as unlimited BeamState.DefaultRateLimits defLimits = beamState.getInitRateLimits(key, rateLimitsHarness); - require !(defLimits.maxAmount == max_uint256 && defLimits.slope == 0); + require !isUnlimited( + defLimits.maxAmount, defLimits.slope, + rateLimitsHarness.getMaxAmount(key), rateLimitsHarness.getSlope(key) + ); // Get currentRateLimit before the call uint256 currentRateLimit = rateLimitsHarness.getCurrentRateLimit(e, key); @@ -244,8 +270,8 @@ rule setRateLimit_revert(bytes32 key, uint256 maxAmount, uint256 slope) { uint256 maxChange_ = beamState.getMaxChange(rateLimitsHarness); uint256 zzzValue = zzz(rateLimitsHarness, key); - bool isUnlimited = defMaxAmount == max_uint256 && defSlope == 0; - bool isIncrement = maxAmount > currentMaxAmount || slope > currentSlope; + bool isUnlimited_ = isUnlimited(defMaxAmount, defSlope, currentMaxAmount, currentSlope); + bool isIncrement = maxAmount > currentMaxAmount || slope > currentSlope; // Avoid overflows require currentMaxAmount * maxChange_ <= max_uint256; @@ -259,17 +285,35 @@ rule setRateLimit_revert(bytes32 key, uint256 maxAmount, uint256 slope) { bool revert1 = e.msg.value > 0; bool revert2 = stopped; bool revert3 = rateLimitsCBeamsSender != 1; - bool revert4 = isUnlimited && !(maxAmount == max_uint256 && slope == 0); - bool revert5 = !isUnlimited && maxAmount > _max(require_uint256(currentMaxAmount * maxChange_ / WAD()), defMaxAmount); - bool revert6 = !isUnlimited && slope > _max(require_uint256(currentSlope * maxChange_ / WAD()), defSlope); - bool revert7 = !isUnlimited && isIncrement && hop_ == 0; - bool revert8 = !isUnlimited && isIncrement && e.block.timestamp < zzzValue + hop_; + bool revert4 = isUnlimited_ && !(maxAmount == max_uint256 && slope == 0); + // Negation of the contract's 3-way OR: + // maxAmount <= defMaxAmount || maxAmount <= current.maxAmount || maxAmount <= current.maxAmount * maxChange / WAD + bool revert5 = !isUnlimited_ && maxAmount > defMaxAmount + && maxAmount > currentMaxAmount + && maxAmount > require_uint256(currentMaxAmount * maxChange_ / WAD()); + bool revert6 = !isUnlimited_ && slope > defSlope + && slope > currentSlope + && slope > require_uint256(currentSlope * maxChange_ / WAD()); + bool revert7 = !isUnlimited_ && isIncrement && hop_ == 0; + bool revert8 = !isUnlimited_ && isIncrement && e.block.timestamp < zzzValue + hop_; assert lastReverted <=> revert1 || revert2 || revert3 || revert4 || revert5 || revert6 || revert7 || revert8; } // --- callControllerAction rules --- +rule callControllerAction(address controller, bytes data) { + env e; + + require controllerHarness.calls() == 0; + + callControllerAction(e, controller, data); + + assert controllerHarness.calls() == 1; +} + +// Exhaustive revert conditions. The controller call is dispatched to ControllerHarness.action(), +// which never reverts, so `require(ok)` is not an additional revert cause here. rule callControllerAction_revert(address controller, bytes data) { env e; @@ -284,18 +328,5 @@ rule callControllerAction_revert(address controller, bytes data) { bool revert3 = controllersCBeamsSender != 1; bool revert4 = !isControllerActionEnabled; - // Note: Additional revert from external controller call is not covered here - assert revert1 || revert2 || revert3 || revert4 => lastReverted; -} - -// When stopped, all non-view functions revert -rule whenStoppedAllFunctionsRevert(method f) filtered { f -> !f.isView } { - env e; - calldataarg args; - - require beamState.stopped(); - - f@withrevert(e, args); - - assert lastReverted; + assert lastReverted <=> revert1 || revert2 || revert3 || revert4; } diff --git a/certora/PASMom.conf b/certora/PASMom.conf new file mode 100644 index 0000000..47a6996 --- /dev/null +++ b/certora/PASMom.conf @@ -0,0 +1,12 @@ +{ + "files": ["src/PASMom.sol", "src/BeamState.sol", "src/timelock/Timelock.sol"], + "verify": "PASMom:certora/PASMom.spec", + "link": ["PASMom:beamState=BeamState", "PASMom:timelock=Timelock"], + "solc": "solc-0.8.24", + "optimistic_loop": true, + "rule_sanity": "basic", + "multi_assert_check": true, + "optimistic_hashing": true, + "parametric_contracts": ["PASMom"], + "msg": "PASMom" +} diff --git a/certora/PASMom.spec b/certora/PASMom.spec new file mode 100644 index 0000000..6224b6a --- /dev/null +++ b/certora/PASMom.spec @@ -0,0 +1,166 @@ +// PASMom.spec + +using BeamState as beamState; +using Timelock as timelock; + +// --- Methods block --- + +methods { + // PASMom storage getters + function owner() external returns (address) envfree; + function authority() external returns (address) envfree; + + // PASMom immutable getters + function beamState() external returns (address) envfree; + function timelock() external returns (address) envfree; + + // BeamState functions reached through PASMom.stop + function beamState.stopped() external returns (bool) envfree; + function beamState.wards(address) external returns (uint256) envfree; + function beamState.userRoles(address) external returns (bytes32) envfree; + function beamState.actionsRoles(bytes4) external returns (bytes32) envfree; + + // Timelock functions reached through PASMom.pause + function timelock.paused() external returns (bool) envfree; + function timelock.hasRole(bytes32, address) external returns (bool) envfree; + function timelock.PAUSER_ROLE() external returns (bytes32) envfree; + + // The authority is not part of the scene, its answer is modelled by a ghost so that + // both the `authority == 0` and the `authority != 0` branches stay reachable + function _.canCall(address src, address dst, bytes4 sig_) external => canCallGhost(src, dst, sig_) expect bool; +} + +ghost canCallGhost(address, address, bytes4) returns bool; + +// --- Storage Affected Rule --- + +rule storageAffected(method f) filtered { f -> !f.isView } { + env e; + calldataarg args; + + address ownerBefore = owner(); + address authorityBefore = authority(); + + f(e, args); + + address ownerAfter = owner(); + address authorityAfter = authority(); + + assert ownerAfter != ownerBefore => + f.selector == sig:setOwner(address).selector; + assert authorityAfter != authorityBefore => + f.selector == sig:setAuthority(address).selector; +} + +// --- Admin functions: setOwner --- + +rule setOwner(address owner_) { + env e; + + setOwner(e, owner_); + + assert owner() == owner_; +} + +rule setOwner_revert(address owner_) { + env e; + + address ownerBefore = owner(); + + setOwner@withrevert(e, owner_); + + bool revert1 = e.msg.value > 0; + bool revert2 = e.msg.sender != ownerBefore; + + assert lastReverted <=> revert1 || revert2; +} + +// --- Admin functions: setAuthority --- + +rule setAuthority(address authority_) { + env e; + + setAuthority(e, authority_); + + assert authority() == authority_; +} + +rule setAuthority_revert(address authority_) { + env e; + + address ownerBefore = owner(); + + setAuthority@withrevert(e, authority_); + + bool revert1 = e.msg.value > 0; + bool revert2 = e.msg.sender != ownerBefore; + + assert lastReverted <=> revert1 || revert2; +} + +// --- Emergency functions: stop --- + +rule stop() { + env e; + + stop(e); + + assert beamState.stopped() == true; +} + +rule stop_revert() { + env e; + + address ownerBefore = owner(); + address authorityBefore = authority(); + bool canCall = canCallGhost(e.msg.sender, currentContract, to_bytes4(sig:stop().selector)); + + // BeamState.stop() is roleAuth'd on PASMom as the caller. + // Note: PASMom.stop() and BeamState.stop() share the same `stop()` selector. + uint256 beamStateWards = beamState.wards(currentContract); + bytes32 beamStateUserRoles = beamState.userRoles(currentContract); + bytes32 beamStateActionsRoles = beamState.actionsRoles(to_bytes4(sig:stop().selector)); + + stop@withrevert(e); + + bool revert1 = e.msg.value > 0; + // isAuthorized: the owner always passes, anyone else needs a non-zero authority that allows it + bool revert2 = e.msg.sender != ownerBefore && (authorityBefore == 0 || !canCall); + // BeamState.roleAuth, with PASMom as the caller + bool revert3 = (beamStateUserRoles & beamStateActionsRoles == to_bytes32(0)) && beamStateWards != 1; + + assert lastReverted <=> revert1 || revert2 || revert3; +} + +// --- Emergency functions: pause --- + +rule pause() { + env e; + + pause(e); + + assert timelock.paused() == true; +} + +rule pause_revert() { + env e; + + address ownerBefore = owner(); + address authorityBefore = authority(); + bool canCall = canCallGhost(e.msg.sender, currentContract, to_bytes4(sig:pause().selector)); + + // Timelock.pause() requires PAUSER_ROLE on PASMom and is blocked while already paused. + // Note: PASMom.pause() and Timelock.pause() share the same `pause()` selector. + bool timelockIsPauser = timelock.hasRole(timelock.PAUSER_ROLE(), currentContract); + bool timelockIsPaused = timelock.paused(); + + pause@withrevert(e); + + bool revert1 = e.msg.value > 0; + // isAuthorized: the owner always passes, anyone else needs a non-zero authority that allows it + bool revert2 = e.msg.sender != ownerBefore && (authorityBefore == 0 || !canCall); + bool revert3 = !timelockIsPauser; + bool revert4 = timelockIsPaused; + + assert lastReverted <=> revert1 || revert2 || revert3 || revert4; +} diff --git a/certora/Timelock.conf b/certora/Timelock.conf index 869ff1d..012f933 100644 --- a/certora/Timelock.conf +++ b/certora/Timelock.conf @@ -1,12 +1,20 @@ { - "files": ["src/timelock/Timelock.sol"], + "files": [ + "src/timelock/Timelock.sol" + ], "verify": "Timelock:certora/Timelock.spec", "solc": "solc-0.8.24", "optimistic_loop": true, - "loop_iter": 5, + "loop_iter": 3, "rule_sanity": "basic", "multi_assert_check": true, "optimistic_hashing": true, - "parametric_contracts": ["Timelock"], - "msg": "Timelock" + "hashing_length_bound": 640, + "parametric_contracts": [ + "Timelock" + ], + "msg": "Timelock", + "prover_args": [ + "-splitParallel true" + ] } diff --git a/certora/Timelock.spec b/certora/Timelock.spec index 96740ab..adc41f4 100644 --- a/certora/Timelock.spec +++ b/certora/Timelock.spec @@ -1,7 +1,4 @@ -// SPDX-FileCopyrightText: © 2026 Dai Foundation -// SPDX-License-Identifier: AGPL-3.0-or-later -// -// Timelock.spec -- Formal verification spec for Timelock +// Timelock.spec using Timelock as timelock; @@ -20,6 +17,7 @@ methods { function getOperationLength(bytes32) external returns (uint256) envfree; function getOperationTarget(bytes32, uint256) external returns (address) envfree; function getOperationValue(bytes32, uint256) external returns (uint256) envfree; + function getOperationPayload(bytes32, uint256) external returns (bytes) envfree; function getOperationPredecessor(bytes32) external returns (bytes32) envfree; function getOperationSalt(bytes32) external returns (bytes32) envfree; @@ -30,18 +28,28 @@ methods { function getMinDelay() external returns (uint256) envfree; function getTimestamp(bytes32) external returns (uint256) envfree; function hashOperationBatch(address[], uint256[], bytes[], bytes32, bytes32) external returns (bytes32) envfree; - function isOperationReady(bytes32, uint256) external returns (bool); + function isOperationReady(bytes32) external returns (bool); // Inherited from AccessControl function hasRole(bytes32, address) external returns (bool) envfree; + function getRoleAdmin(bytes32) external returns (bytes32) envfree; + + // Inherited from ERC721Holder / ERC1155Holder + function onERC721Received(address, address, uint256, bytes) external returns (bytes4); + function onERC1155Received(address, address, uint256, uint256, bytes) external returns (bytes4); + function onERC1155BatchReceived(address, address, uint256[], uint256[], bytes) external returns (bytes4); function PAUSER_ROLE() external returns (bytes32) envfree; function PROPOSER_ROLE() external returns (bytes32) envfree; function CANCELLER_ROLE() external returns (bytes32) envfree; function EXECUTOR_ROLE() external returns (bytes32) envfree; function DEFAULT_ADMIN_ROLE() external returns (bytes32) envfree; - // // External call summaries - treat external calls as non-deterministic - // function _._ external => NONDET; + // executeBatch forwards to arbitrary targets. Left unresolved they havoc all contract state, + // which breaks the list bookkeeping assertions (countBefore is read before the calls) and is + // very expensive to solve. Scoped to executeBatch so that the legitimate `this.updateDelay` + // self-call in updateDelayImmediately is still executed for real. + // Assumption: the executed calls succeed and do not re-enter the Timelock. + unresolved external in Timelock.executeBatch(address[],uint256[],bytes[],bytes32,bytes32) => NONDET; } // --- Definitions --- @@ -50,11 +58,24 @@ definition DONE_TIMESTAMP() returns uint256 = 1; // --- Storage Affected Rule --- -rule storageAffected(method f) filtered { f -> !f.isView } { +rule storageAffected(method f) filtered { + f -> !f.isView && + f.selector != sig:execute(address,uint256,bytes,bytes32,bytes32).selector +} { env e; calldataarg args; bytes32 anyId; + bytes32 anyElemId; + uint256 anyIdx; + bytes32 anyRole; + address anyAccount; + + // Element reads panic out of bounds, so the index is pinned inside the array. A separate id is + // used for them so that this assumption does not also narrow the checks below, which apply to + // any id. Methods that do not touch _operations leave the length alone, so the post-state read + // stays in range for them. + require anyIdx < getOperationLength(anyElemId); // Linked list state bytes32 firstBefore = getFirstOperationId(); @@ -68,12 +89,20 @@ rule storageAffected(method f) filtered { f -> !f.isView } { uint256 lengthBefore = getOperationLength(anyId); bytes32 predecessorBefore = getOperationPredecessor(anyId); bytes32 saltBefore = getOperationSalt(anyId); + address targetBefore = getOperationTarget(anyElemId, anyIdx); + uint256 valueBefore = getOperationValue(anyElemId, anyIdx); + bytes payloadBefore = getOperationPayload(anyElemId, anyIdx); // Pausable state bool pausedBefore = paused(); // TimelockController state uint256 minDelayBefore = getMinDelay(); + uint256 timestampBefore = getTimestamp(anyId); + + // AccessControl state + bool hasRoleBefore = hasRole(anyRole, anyAccount); + bytes32 roleAdminBefore = getRoleAdmin(anyRole); f(e, args); @@ -89,12 +118,20 @@ rule storageAffected(method f) filtered { f -> !f.isView } { uint256 lengthAfter = getOperationLength(anyId); bytes32 predecessorAfter = getOperationPredecessor(anyId); bytes32 saltAfter = getOperationSalt(anyId); + address targetAfter = getOperationTarget(anyElemId, anyIdx); + uint256 valueAfter = getOperationValue(anyElemId, anyIdx); + bytes payloadAfter = getOperationPayload(anyElemId, anyIdx); // Pausable state bool pausedAfter = paused(); // TimelockController state uint256 minDelayAfter = getMinDelay(); + uint256 timestampAfter = getTimestamp(anyId); + + // AccessControl state + bool hasRoleAfter = hasRole(anyRole, anyAccount); + bytes32 roleAdminAfter = getRoleAdmin(anyRole); // Linked list can only be modified by scheduleBatch, cancel, executeBatch assert (firstAfter != firstBefore || lastAfter != lastBefore || countAfter != countBefore || @@ -103,8 +140,11 @@ rule storageAffected(method f) filtered { f -> !f.isView } { f.selector == sig:cancel(bytes32).selector || f.selector == sig:executeBatch(address[],uint256[],bytes[],bytes32,bytes32).selector; - // Operation data can only be modified by scheduleBatch, cancel, executeBatch - assert (lengthAfter != lengthBefore || predecessorAfter != predecessorBefore || saltAfter != saltBefore) => + // Operation data, including the targets/values/payloads contents, can only be modified by + // scheduleBatch, cancel, executeBatch + assert (lengthAfter != lengthBefore || predecessorAfter != predecessorBefore || + saltAfter != saltBefore || targetAfter != targetBefore || + valueAfter != valueBefore || payloadAfter != payloadBefore) => f.selector == sig:scheduleBatch(address[],uint256[],bytes[],bytes32,bytes32,uint256).selector || f.selector == sig:cancel(bytes32).selector || f.selector == sig:executeBatch(address[],uint256[],bytes[],bytes32,bytes32).selector; @@ -118,6 +158,21 @@ rule storageAffected(method f) filtered { f -> !f.isView } { assert minDelayAfter != minDelayBefore => f.selector == sig:updateDelay(uint256).selector || f.selector == sig:updateDelayImmediately(uint256).selector; + + // _timestamps is written by _schedule, deleted by cancel and set to DONE by _afterCall + assert timestampAfter != timestampBefore => + f.selector == sig:scheduleBatch(address[],uint256[],bytes[],bytes32,bytes32,uint256).selector || + f.selector == sig:cancel(bytes32).selector || + f.selector == sig:executeBatch(address[],uint256[],bytes[],bytes32,bytes32).selector; + + // Role membership can only be modified by the AccessControl mutators + assert hasRoleAfter != hasRoleBefore => + f.selector == sig:grantRole(bytes32,address).selector || + f.selector == sig:revokeRole(bytes32,address).selector || + f.selector == sig:renounceRole(bytes32,address).selector; + + // _setRoleAdmin is internal and never called, so role admins never change after construction + assert roleAdminAfter == roleAdminBefore; } // --- Pausing rules --- @@ -168,6 +223,32 @@ rule unpause_revert() { assert lastReverted <=> revert1 || revert2 || revert3; } + +// --- Delay management rules --- + +rule updateDelayImmediately(uint256 newDelay) { + env e; + + updateDelayImmediately(e, newDelay); + + uint256 minDelayAfter = getMinDelay(); + + assert minDelayAfter == newDelay; +} + +rule updateDelayImmediately_revert(uint256 newDelay) { + env e; + + bool isAdmin = hasRole(DEFAULT_ADMIN_ROLE(), e.msg.sender); + + updateDelayImmediately@withrevert(e, newDelay); + + bool revert1 = e.msg.value > 0; + bool revert2 = !isAdmin; + + assert lastReverted <=> revert1 || revert2; +} + // --- Schedule rules --- rule schedule_always_reverts(address target, uint256 value, bytes payload, bytes32 predecessor, bytes32 salt, uint256 delay) { @@ -190,6 +271,7 @@ rule scheduleBatch_adds_to_list( uint256 countBefore = getOperationsCount(); bytes32 id = hashOperationBatch(targets, values, payloads, predecessor, salt); + uint256 idx; require !getOperationExists(id); @@ -199,9 +281,26 @@ rule scheduleBatch_adds_to_list( bool existsAfter = getOperationExists(id); bytes32 lastAfter = getLastOperationId(); + bool targetMatches = true; + bool valueMatches = true; + if (targets.length > 0) { + require idx < targets.length; + targetMatches = getOperationTarget(id, idx) == targets[idx]; + valueMatches = getOperationValue(id, idx) == values[idx]; + } + assert countAfter == countBefore + 1; - assert existsAfter == true; + assert existsAfter; assert lastAfter == id; + + // The stored operation mirrors what was scheduled + assert getOperationLength(id) == targets.length; + assert getOperationPredecessor(id) == predecessor; + assert getOperationSalt(id) == salt; + // _schedule sets _timestamps[id] = block.timestamp + delay + assert getTimestamp(id) == assert_uint256(e.block.timestamp + delay); + assert targetMatches; + assert valueMatches; } rule scheduleBatch_no_side_effects( @@ -256,21 +355,39 @@ rule scheduleBatch_revert( bool isOp = isOperation(e, id); uint256 minDelay = getMinDelay(); - // Check array lengths match - require targets.length == values.length; - require targets.length == payloads.length; + bool existsBefore = getOperationExists(id); + uint256 countBefore = getOperationsCount(); scheduleBatch@withrevert(e, targets, values, payloads, predecessor, salt, delay); - bool revert1 = e.msg.value > 0; - bool revert2 = isPaused; - bool revert3 = !isProposer; - bool revert4 = isOp; // Operation already exists in TimelockController - bool revert5 = delay < minDelay; - // revert6: self-call check - one of targets == address(this) - // revert7: linked list add fails (id == 0 or already exists) - covered by revert4 - - assert revert1 || revert2 || revert3 || revert4 || revert5 => lastReverted; + bool revert1 = e.msg.value > 0; + bool revert2 = isPaused; + bool revert3 = exists uint256 i. i < targets.length && targets[i] == currentContract; + bool revert4 = !isProposer; + bool revert5 = targets.length != values.length || targets.length != payloads.length; + bool revert6 = isOp; // Operation already scheduled in TimelockController + bool revert7 = delay < minDelay; + // Linked list add fails. Note _operationIds.exists and TimelockController's _timestamps are + // separate storage, so this is not implied by revert5. + bool revert8 = id == to_bytes32(0) || existsBefore; + // _schedule writes _timestamps[id] = block.timestamp + delay under checked arithmetic + bool revert9 = e.block.timestamp + delay > max_uint256; + // Bytes32LinkedList.add does a checked count++ + bool revert10 = countBefore == max_uint256; + // A target equal to the timelock also reverts; that case is proven by selfCallPrevention, + // which covers an arbitrary index without needing a quantifier here. + + // Necessary direction only. The converse is not provable: writing _operations[id] makes + // Solidity clear and overwrite the previous payloads, and from an unconstrained pre-state the + // stale storage slots at and past the array length can hold an invalid byte-array encoding, + // which panics (Panic 0x22). That is unreachable in practice -- only the contract ever writes + // those slots -- but it is also not expressible as a CVL assumption, because constraining + // `payloads.length` says nothing about the element slots beyond the length. This is the same + // wall that keeps cancel_revert_length_0 restricted to the empty-payloads case. + assert revert1 || revert2 || revert3 || + revert4 || revert5 || revert6 || + revert7 || revert8 || revert9 || + revert10 => lastReverted; } // --- Cancel rules --- @@ -291,6 +408,8 @@ rule cancel_removes_from_list(bytes32 id) { assert countAfter == countBefore - 1; assert existsAfter == false; assert lengthAfter == 0; + // cancel deletes _timestamps[id] + assert getTimestamp(id) == 0; } rule cancel_no_side_effects(bytes32 id) { @@ -393,6 +512,8 @@ rule executeBatch_removes_from_list( assert countAfter == countBefore - 1; assert existsAfter == false; assert lengthAfter == 0; + // _afterCall marks the operation done rather than clearing it + assert getTimestamp(id) == DONE_TIMESTAMP(); } rule executeBatch_revert( @@ -409,221 +530,195 @@ rule executeBatch_revert( bool isReady = isOperationReady(e, id); bool predecessorDone = predecessor == to_bytes32(0) || isOperationDone(e, predecessor); - // Check array lengths match - require targets.length == values.length; - require targets.length == payloads.length; + // Execution is permissionless only while EXECUTOR_ROLE is held by address(0), which the + // constructor grants but which cannot be assumed from an arbitrary pre-state + bool isOpenExecutor = hasRole(EXECUTOR_ROLE(), 0); + bool isExecutor = hasRole(EXECUTOR_ROLE(), e.msg.sender); - executeBatch@withrevert(e, targets, values, payloads, predecessor, salt); + bool existsBefore = getOperationExists(id); + uint256 countBefore = getOperationsCount(); - bool revert1 = e.msg.value > 0 && e.msg.value != values[0]; // Only fails if value mismatch - bool revert2 = isPaused; - bool revert3 = !isReady; - bool revert4 = !predecessorDone; - // revert5: external call fails - // revert6: linked list remove fails (doesn't exist) + executeBatch@withrevert(e, targets, values, payloads, predecessor, salt); - assert revert2 || revert3 || revert4 => lastReverted; + bool revert1 = isPaused; // whenNotPaused on the override + bool revert2 = !isOpenExecutor && !isExecutor; // onlyRoleOrOpenRole(EXECUTOR_ROLE) + bool revert3 = targets.length != values.length || + targets.length != payloads.length; // TimelockInvalidOperationLength + bool revert4 = !isReady; // _beforeCall, re-checked by _afterCall + bool revert5 = !predecessorDone; // _beforeCall + bool revert6 = !existsBefore; // require(_operationIds.remove(id)) + bool revert7 = countBefore == 0; // checked count-- inside remove + + // Necessary direction only. Two causes are not stated: `delete _operations[id]` clears the + // stored payloads, and stale slots from an unconstrained pre-state can hold an invalid + // byte-array encoding that panics (Panic 0x22) -- unreachable in practice but not expressible + // as a CVL assumption; and forwarding values[i] fails once the running balance is short, whose + // exact condition is a prefix sum over a symbolic-length calldata array. Both would have to be + // assumed away to reach `<=>`, which is not worth narrowing this rule for. + // The target calls themselves are summarized NONDET, so "external call fails" is not a cause. + assert revert1 || revert2 || revert3 || revert4 || + revert5 || revert6 || revert7 => lastReverted; } -// --- Delay management rules --- +// --- Access control mutators --- -rule updateDelayImmediately(uint256 newDelay) { +rule grantRole(bytes32 role, address account) { env e; - updateDelayImmediately(e, newDelay); + bytes32 otherRole; + address otherAccount; + require otherRole != role || otherAccount != account; - uint256 minDelayAfter = getMinDelay(); + bool otherBefore = hasRole(otherRole, otherAccount); - assert minDelayAfter == newDelay; + grantRole(e, role, account); + + assert hasRole(role, account); + assert hasRole(otherRole, otherAccount) == otherBefore; } -rule updateDelayImmediately_revert(uint256 newDelay) { +rule grantRole_revert(bytes32 role, address account) { env e; - bool isAdmin = hasRole(DEFAULT_ADMIN_ROLE(), e.msg.sender); + bool isRoleAdmin = hasRole(getRoleAdmin(role), e.msg.sender); - updateDelayImmediately@withrevert(e, newDelay); + grantRole@withrevert(e, role, account); bool revert1 = e.msg.value > 0; - bool revert2 = !isAdmin; + bool revert2 = !isRoleAdmin; assert lastReverted <=> revert1 || revert2; } -// --- Linked list invariants --- +rule revokeRole(bytes32 role, address account) { + env e; -invariant emptyListConsistency() - getOperationsCount() == 0 <=> (getFirstOperationId() == to_bytes32(0) && getLastOperationId() == to_bytes32(0)) - { - preserved scheduleBatch(address[] targets, uint256[] values, bytes[] payloads, bytes32 predecessor, bytes32 salt, uint256 delay) with (env e) { - // Hash cannot be zero for valid operations - require hashOperationBatch(targets, values, payloads, predecessor, salt) != to_bytes32(0); - } - } + bytes32 otherRole; + address otherAccount; + require otherRole != role || otherAccount != account; -// // --- Linked list structure invariants --- - -// // First element has no predecessor -// invariant firstHasNoPrev() -// getFirstOperationId() != to_bytes32(0) => getPrevOperationId(getFirstOperationId()) == to_bytes32(0) -// { -// preserved scheduleBatch(address[] targets, uint256[] values, bytes[] payloads, bytes32 predecessor, bytes32 salt, uint256 delay) with (env e) { -// require hashOperationBatch(targets, values, payloads, predecessor, salt) != to_bytes32(0); -// } -// } - -// // Last element has no successor -// invariant lastHasNoNext() -// getLastOperationId() != to_bytes32(0) => getNextOperationId(getLastOperationId()) == to_bytes32(0) -// { -// preserved scheduleBatch(address[] targets, uint256[] values, bytes[] payloads, bytes32 predecessor, bytes32 salt, uint256 delay) with (env e) { -// require hashOperationBatch(targets, values, payloads, predecessor, salt) != to_bytes32(0); -// } -// } - -// // If an operation exists, count must be positive -// invariant existsImpliesPositiveCount(bytes32 id) -// getOperationExists(id) => getOperationsCount() > 0 -// { -// preserved scheduleBatch(address[] targets, uint256[] values, bytes[] payloads, bytes32 predecessor, bytes32 salt, uint256 delay) with (env e) { -// require hashOperationBatch(targets, values, payloads, predecessor, salt) != to_bytes32(0); -// } -// } - -// // If operation exists in linked list, it has data (at least one target) -// invariant operationExistsImpliesData(bytes32 id) -// getOperationExists(id) => getOperationLength(id) > 0 -// { -// preserved scheduleBatch(address[] targets, uint256[] values, bytes[] payloads, bytes32 predecessor, bytes32 salt, uint256 delay) with (env e) { -// require hashOperationBatch(targets, values, payloads, predecessor, salt) != to_bytes32(0); -// require targets.length > 0; -// } -// } - -// --- Access control rules --- - -rule onlyPauserCanPause() { - env e; - - require !hasRole(PAUSER_ROLE(), e.msg.sender); + bool otherBefore = hasRole(otherRole, otherAccount); - pause@withrevert(e); + revokeRole(e, role, account); - assert lastReverted; + assert !hasRole(role, account); + assert hasRole(otherRole, otherAccount) == otherBefore; } -rule onlyAdminCanUnpause() { +rule revokeRole_revert(bytes32 role, address account) { env e; - require !hasRole(DEFAULT_ADMIN_ROLE(), e.msg.sender); + bool isRoleAdmin = hasRole(getRoleAdmin(role), e.msg.sender); - unpause@withrevert(e); + revokeRole@withrevert(e, role, account); - assert lastReverted; + bool revert1 = e.msg.value > 0; + bool revert2 = !isRoleAdmin; + + assert lastReverted <=> revert1 || revert2; } -rule onlyAdminCanUpdateDelay() { +// Renouncing takes no role admin: any account may drop its own role, and only its own +rule renounceRole(bytes32 role, address callerConfirmation) { env e; - uint256 newDelay; - require !hasRole(DEFAULT_ADMIN_ROLE(), e.msg.sender); + bytes32 otherRole; + address otherAccount; + require otherRole != role || otherAccount != callerConfirmation; - updateDelayImmediately@withrevert(e, newDelay); + bool otherBefore = hasRole(otherRole, otherAccount); - assert lastReverted; + renounceRole(e, role, callerConfirmation); + + assert !hasRole(role, callerConfirmation); + assert hasRole(otherRole, otherAccount) == otherBefore; } -rule onlyProposerCanSchedule( - address[] targets, - uint256[] values, - bytes[] payloads, - bytes32 predecessor, - bytes32 salt, - uint256 delay -) { +rule renounceRole_revert(bytes32 role, address callerConfirmation) { env e; - require !hasRole(PROPOSER_ROLE(), e.msg.sender); + renounceRole@withrevert(e, role, callerConfirmation); - scheduleBatch@withrevert(e, targets, values, payloads, predecessor, salt, delay); + bool revert1 = e.msg.value > 0; + bool revert2 = callerConfirmation != e.msg.sender; // AccessControlBadConfirmation - assert lastReverted; + assert lastReverted <=> revert1 || revert2; } -rule onlyCancellerCanCancel(bytes32 id) { +// --- Inherited updateDelay --- + +// The inherited updateDelay is callable only by the timelock itself, which is what stops a +// proposal from rewriting the min delay; updateDelayImmediately reaches it via an external +// self-call after checking DEFAULT_ADMIN_ROLE +rule updateDelay(uint256 newDelay) { env e; - require !hasRole(CANCELLER_ROLE(), e.msg.sender); + require e.msg.sender == currentContract; - cancel@withrevert(e, id); + updateDelay(e, newDelay); - assert lastReverted; + assert getMinDelay() == newDelay; } -// --- Paused state rules --- - -rule whenPausedScheduleReverts( - address[] targets, - uint256[] values, - bytes[] payloads, - bytes32 predecessor, - bytes32 salt, - uint256 delay -) { +rule updateDelay_revert(uint256 newDelay) { env e; - require paused(); + updateDelay@withrevert(e, newDelay); - scheduleBatch@withrevert(e, targets, values, payloads, predecessor, salt, delay); + bool revert1 = e.msg.value > 0; + bool revert2 = e.msg.sender != currentContract; // TimelockUnauthorizedCaller - assert lastReverted; + assert lastReverted <=> revert1 || revert2; } -rule whenPausedCancelReverts(bytes32 id) { +// --- Token receiver hooks --- + +// The holder hooks accept transfers unconditionally and touch no storage; storageAffected already +// covers the absence of side effects, these pin the returned magic values +rule onERC721Received_returns_selector(address operator, address from, uint256 tokenId, bytes data) { env e; - require paused(); + bytes4 ret = onERC721Received(e, operator, from, tokenId, data); - cancel@withrevert(e, id); - - assert lastReverted; + assert ret == to_bytes4(sig:onERC721Received(address,address,uint256,bytes).selector); } -rule whenPausedExecuteReverts( - address[] targets, - uint256[] values, - bytes[] payloads, - bytes32 predecessor, - bytes32 salt -) { +rule onERC721Received_revert(address operator, address from, uint256 tokenId, bytes data) { env e; - require paused(); + onERC721Received@withrevert(e, operator, from, tokenId, data); - executeBatch@withrevert(e, targets, values, payloads, predecessor, salt); + assert lastReverted <=> e.msg.value > 0; +} - assert lastReverted; +rule onERC1155Received_returns_selector(address operator, address from, uint256 id, uint256 value, bytes data) { + env e; + + bytes4 ret = onERC1155Received(e, operator, from, id, value, data); + + assert ret == to_bytes4(sig:onERC1155Received(address,address,uint256,uint256,bytes).selector); } -// --- Self-call prevention --- +rule onERC1155Received_revert(address operator, address from, uint256 id, uint256 value, bytes data) { + env e; -// This rule verifies that scheduleBatch reverts when any target is the timelock itself -// Note: This is a property check that should be verified -rule selfCallPrevention( - address[] targets, - uint256[] values, - bytes[] payloads, - bytes32 predecessor, - bytes32 salt, - uint256 delay -) { + onERC1155Received@withrevert(e, operator, from, id, value, data); + + assert lastReverted <=> e.msg.value > 0; +} + +rule onERC1155BatchReceived_returns_selector(address operator, address from, uint256[] ids, uint256[] values, bytes data) { env e; - // Assume first target is the contract itself - require targets.length > 0; - require targets[0] == currentContract; + bytes4 ret = onERC1155BatchReceived(e, operator, from, ids, values, data); - scheduleBatch@withrevert(e, targets, values, payloads, predecessor, salt, delay); + assert ret == to_bytes4(sig:onERC1155BatchReceived(address,address,uint256[],uint256[],bytes).selector); +} - assert lastReverted; +rule onERC1155BatchReceived_revert(address operator, address from, uint256[] ids, uint256[] values, bytes data) { + env e; + + onERC1155BatchReceived@withrevert(e, operator, from, ids, values, data); + + assert lastReverted <=> e.msg.value > 0; } diff --git a/certora/harness/ControllerHarness.sol b/certora/harness/ControllerHarness.sol new file mode 100644 index 0000000..fa8940d --- /dev/null +++ b/certora/harness/ControllerHarness.sol @@ -0,0 +1,19 @@ +// SPDX-FileCopyrightText: © 2026 Dai Foundation +// SPDX-License-Identifier: AGPL-3.0-or-later +// +// ControllerHarness.sol -- Certora harness standing in for a controller called by Configurator + +pragma solidity ^0.8.24; + +contract ControllerHarness { + + uint256 public calls; + + // The increments are unchecked so that this harness can never revert: a checked `calls++` + // reverts once calls == type(uint256).max, which would make the `require(ok)` in + // Configurator.callControllerAction an additional revert cause. + + function action() external { + unchecked { calls++; } + } +} From 0c3a60e9be16c153bb1f49da6eecd62036f01f2c Mon Sep 17 00:00:00 2001 From: sunbreak1211 Date: Fri, 4 Sep 2026 19:57:41 -0300 Subject: [PATCH 4/5] Add remappings --- remappings.txt | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 remappings.txt diff --git a/remappings.txt b/remappings.txt new file mode 100644 index 0000000..ff0ea2c --- /dev/null +++ b/remappings.txt @@ -0,0 +1,7 @@ +@openzeppelin/contracts/=lib/openzeppelin-contracts/contracts/ +dss-interfaces/=lib/dss-test/lib/dss-interfaces/src/ +dss-test/=lib/dss-test/src/ +erc4626-tests/=lib/openzeppelin-contracts/lib/erc4626-tests/ +forge-std/=lib/forge-std/src/ +halmos-cheatcodes/=lib/openzeppelin-contracts/lib/halmos-cheatcodes/src/ +openzeppelin-contracts/=lib/openzeppelin-contracts/ From b9bacc224aa418424f0183103a3ef6f07fc046c9 Mon Sep 17 00:00:00 2001 From: sunbreak1211 Date: Fri, 4 Sep 2026 20:12:06 -0300 Subject: [PATCH 5/5] Set contract solc options correctly --- certora/BeamState.conf | 6 +++++- certora/Configurator.conf | 2 ++ certora/PASMom.conf | 17 ++++++++++++++--- certora/Timelock.conf | 2 ++ 4 files changed, 23 insertions(+), 4 deletions(-) diff --git a/certora/BeamState.conf b/certora/BeamState.conf index eb5118b..d33d3bd 100644 --- a/certora/BeamState.conf +++ b/certora/BeamState.conf @@ -1,7 +1,11 @@ { - "files": ["src/BeamState.sol"], + "files": [ + "src/BeamState.sol" + ], "verify": "BeamState:certora/BeamState.spec", "solc": "solc-0.8.24", + "solc_optimize": "200", + "solc_evm_version": "cancun", "optimistic_loop": true, "rule_sanity": "basic", "multi_assert_check": true, diff --git a/certora/Configurator.conf b/certora/Configurator.conf index e72f44c..9334116 100644 --- a/certora/Configurator.conf +++ b/certora/Configurator.conf @@ -10,6 +10,8 @@ "Configurator:beamState=BeamState" ], "solc": "solc-0.8.24", + "solc_optimize": "200", + "solc_evm_version": "cancun", "optimistic_loop": true, "rule_sanity": "basic", "multi_assert_check": true, diff --git a/certora/PASMom.conf b/certora/PASMom.conf index 47a6996..7353987 100644 --- a/certora/PASMom.conf +++ b/certora/PASMom.conf @@ -1,12 +1,23 @@ { - "files": ["src/PASMom.sol", "src/BeamState.sol", "src/timelock/Timelock.sol"], + "files": [ + "src/PASMom.sol", + "src/BeamState.sol", + "src/timelock/Timelock.sol" + ], "verify": "PASMom:certora/PASMom.spec", - "link": ["PASMom:beamState=BeamState", "PASMom:timelock=Timelock"], + "link": [ + "PASMom:beamState=BeamState", + "PASMom:timelock=Timelock" + ], "solc": "solc-0.8.24", + "solc_optimize": "200", + "solc_evm_version": "cancun", "optimistic_loop": true, "rule_sanity": "basic", "multi_assert_check": true, "optimistic_hashing": true, - "parametric_contracts": ["PASMom"], + "parametric_contracts": [ + "PASMom" + ], "msg": "PASMom" } diff --git a/certora/Timelock.conf b/certora/Timelock.conf index 012f933..c887942 100644 --- a/certora/Timelock.conf +++ b/certora/Timelock.conf @@ -4,6 +4,8 @@ ], "verify": "Timelock:certora/Timelock.spec", "solc": "solc-0.8.24", + "solc_optimize": "200", + "solc_evm_version": "cancun", "optimistic_loop": true, "loop_iter": 3, "rule_sanity": "basic",