diff --git a/certora/diff/token_ERC721_ERC721.sol.patch b/certora/diff/token_ERC721_ERC721.sol.patch deleted file mode 100644 index c3eae357a4c..00000000000 --- a/certora/diff/token_ERC721_ERC721.sol.patch +++ /dev/null @@ -1,14 +0,0 @@ ---- token/ERC721/ERC721.sol 2023-03-07 10:48:47.736822221 +0100 -+++ token/ERC721/ERC721.sol 2023-03-09 19:49:39.669338673 +0100 -@@ -199,6 +199,11 @@ - return _owners[tokenId]; - } - -+ // FV -+ function _getApproved(uint256 tokenId) internal view returns (address) { -+ return _tokenApprovals[tokenId]; -+ } -+ - /** - * @dev Returns whether `tokenId` exists. - * diff --git a/certora/harnesses/AccessControlDefaultAdminRulesHarness.sol b/certora/harnesses/AccessControlDefaultAdminRulesHarness.sol index 145f65b7674..e96883fa2cc 100644 --- a/certora/harnesses/AccessControlDefaultAdminRulesHarness.sol +++ b/certora/harnesses/AccessControlDefaultAdminRulesHarness.sol @@ -1,8 +1,7 @@ // SPDX-License-Identifier: MIT - pragma solidity ^0.8.20; -import "../patched/access/AccessControlDefaultAdminRules.sol"; +import {AccessControlDefaultAdminRules} from "../patched/access/extensions/AccessControlDefaultAdminRules.sol"; contract AccessControlDefaultAdminRulesHarness is AccessControlDefaultAdminRules { uint48 private _delayIncreaseWait; diff --git a/certora/harnesses/AccessControlHarness.sol b/certora/harnesses/AccessControlHarness.sol index 42a536af160..e862d3eca5b 100644 --- a/certora/harnesses/AccessControlHarness.sol +++ b/certora/harnesses/AccessControlHarness.sol @@ -1,7 +1,6 @@ // SPDX-License-Identifier: MIT - pragma solidity ^0.8.20; -import "../patched/access/AccessControl.sol"; +import {AccessControl} from "../patched/access/AccessControl.sol"; contract AccessControlHarness is AccessControl {} diff --git a/certora/harnesses/DoubleEndedQueueHarness.sol b/certora/harnesses/DoubleEndedQueueHarness.sol index 54852a739e8..d684c7382a4 100644 --- a/certora/harnesses/DoubleEndedQueueHarness.sol +++ b/certora/harnesses/DoubleEndedQueueHarness.sol @@ -1,8 +1,7 @@ // SPDX-License-Identifier: MIT - pragma solidity ^0.8.20; -import "../patched/utils/structs/DoubleEndedQueue.sol"; +import {DoubleEndedQueue} from "../patched/utils/structs/DoubleEndedQueue.sol"; contract DoubleEndedQueueHarness { using DoubleEndedQueue for DoubleEndedQueue.Bytes32Deque; diff --git a/certora/harnesses/ERC20PermitHarness.sol b/certora/harnesses/ERC20PermitHarness.sol index 1041c1715fa..08113f4ea62 100644 --- a/certora/harnesses/ERC20PermitHarness.sol +++ b/certora/harnesses/ERC20PermitHarness.sol @@ -1,8 +1,7 @@ // SPDX-License-Identifier: MIT - pragma solidity ^0.8.20; -import "../patched/token/ERC20/extensions/ERC20Permit.sol"; +import {ERC20Permit, ERC20} from "../patched/token/ERC20/extensions/ERC20Permit.sol"; contract ERC20PermitHarness is ERC20Permit { constructor(string memory name, string memory symbol) ERC20(name, symbol) ERC20Permit(name) {} diff --git a/certora/harnesses/ERC20WrapperHarness.sol b/certora/harnesses/ERC20WrapperHarness.sol index 5e55e4b7292..ca183ad928c 100644 --- a/certora/harnesses/ERC20WrapperHarness.sol +++ b/certora/harnesses/ERC20WrapperHarness.sol @@ -2,10 +2,15 @@ pragma solidity ^0.8.20; -import "../patched/token/ERC20/extensions/ERC20Wrapper.sol"; +import {ERC20Permit} from "../patched/token/ERC20/extensions/ERC20Permit.sol"; +import {ERC20Wrapper, IERC20, ERC20} from "../patched/token/ERC20/extensions/ERC20Wrapper.sol"; -contract ERC20WrapperHarness is ERC20Wrapper { - constructor(IERC20 _underlying, string memory _name, string memory _symbol) ERC20(_name, _symbol) ERC20Wrapper(_underlying) {} +contract ERC20WrapperHarness is ERC20Permit, ERC20Wrapper { + constructor( + IERC20 _underlying, + string memory _name, + string memory _symbol + ) ERC20(_name, _symbol) ERC20Permit(_name) ERC20Wrapper(_underlying) {} function underlyingTotalSupply() public view returns (uint256) { return underlying().totalSupply(); @@ -22,4 +27,8 @@ contract ERC20WrapperHarness is ERC20Wrapper { function recover(address account) public returns (uint256) { return _recover(account); } + + function decimals() public view override(ERC20Wrapper, ERC20) returns (uint8) { + return super.decimals(); + } } diff --git a/certora/harnesses/ERC3156FlashBorrowerHarness.sol b/certora/harnesses/ERC3156FlashBorrowerHarness.sol index 81dfdaf318d..1c76da2d4ab 100644 --- a/certora/harnesses/ERC3156FlashBorrowerHarness.sol +++ b/certora/harnesses/ERC3156FlashBorrowerHarness.sol @@ -1,6 +1,6 @@ // SPDX-License-Identifier: MIT -import "../patched/interfaces/IERC3156FlashBorrower.sol"; +import {IERC3156FlashBorrower} from "../patched/interfaces/IERC3156FlashBorrower.sol"; pragma solidity ^0.8.20; diff --git a/certora/harnesses/ERC721Harness.sol b/certora/harnesses/ERC721Harness.sol index b0afb589c60..69c4c205a18 100644 --- a/certora/harnesses/ERC721Harness.sol +++ b/certora/harnesses/ERC721Harness.sol @@ -2,7 +2,7 @@ pragma solidity ^0.8.20; -import "../patched/token/ERC721/ERC721.sol"; +import {ERC721} from "../patched/token/ERC721/ERC721.sol"; contract ERC721Harness is ERC721 { constructor(string memory name, string memory symbol) ERC721(name, symbol) {} @@ -23,10 +23,6 @@ contract ERC721Harness is ERC721 { _burn(tokenId); } - function tokenExists(uint256 tokenId) external view returns (bool) { - return _exists(tokenId); - } - function unsafeOwnerOf(uint256 tokenId) external view returns (address) { return _ownerOf(tokenId); } diff --git a/certora/harnesses/EnumerableMapHarness.sol b/certora/harnesses/EnumerableMapHarness.sol index 2b9a8e47c74..5c2f3229b84 100644 --- a/certora/harnesses/EnumerableMapHarness.sol +++ b/certora/harnesses/EnumerableMapHarness.sol @@ -2,7 +2,7 @@ pragma solidity ^0.8.20; -import "../patched/utils/structs/EnumerableMap.sol"; +import {EnumerableMap} from "../patched/utils/structs/EnumerableMap.sol"; contract EnumerableMapHarness { using EnumerableMap for EnumerableMap.Bytes32ToBytes32Map; diff --git a/certora/harnesses/EnumerableSetHarness.sol b/certora/harnesses/EnumerableSetHarness.sol index 1f4cac7d93d..3d18b183b2b 100644 --- a/certora/harnesses/EnumerableSetHarness.sol +++ b/certora/harnesses/EnumerableSetHarness.sol @@ -2,7 +2,7 @@ pragma solidity ^0.8.20; -import "../patched/utils/structs/EnumerableSet.sol"; +import {EnumerableSet} from "../patched/utils/structs/EnumerableSet.sol"; contract EnumerableSetHarness { using EnumerableSet for EnumerableSet.Bytes32Set; diff --git a/certora/harnesses/InitializableHarness.sol b/certora/harnesses/InitializableHarness.sol index 0d0c0a4e4e4..743d677dd5f 100644 --- a/certora/harnesses/InitializableHarness.sol +++ b/certora/harnesses/InitializableHarness.sol @@ -1,19 +1,19 @@ // SPDX-License-Identifier: MIT pragma solidity ^0.8.20; -import "../patched/proxy/utils/Initializable.sol"; +import {Initializable} from "../patched/proxy/utils/Initializable.sol"; contract InitializableHarness is Initializable { - function initialize() public initializer {} - function reinitialize(uint8 n) public reinitializer(n) {} - function disable() public { _disableInitializers(); } + function initialize() public initializer {} + function reinitialize(uint64 n) public reinitializer(n) {} + function disable() public { _disableInitializers(); } - function nested_init_init() public initializer { initialize(); } - function nested_init_reinit(uint8 m) public initializer { reinitialize(m); } - function nested_reinit_init(uint8 n) public reinitializer(n) { initialize(); } - function nested_reinit_reinit(uint8 n, uint8 m) public reinitializer(n) { reinitialize(m); } + function nested_init_init() public initializer { initialize(); } + function nested_init_reinit(uint64 m) public initializer { reinitialize(m); } + function nested_reinit_init(uint64 n) public reinitializer(n) { initialize(); } + function nested_reinit_reinit(uint64 n, uint64 m) public reinitializer(n) { reinitialize(m); } - function version() public view returns (uint8) { + function version() public view returns (uint64) { return _getInitializedVersion(); } diff --git a/certora/harnesses/Ownable2StepHarness.sol b/certora/harnesses/Ownable2StepHarness.sol index aed6f585472..09a5faa23a5 100644 --- a/certora/harnesses/Ownable2StepHarness.sol +++ b/certora/harnesses/Ownable2StepHarness.sol @@ -1,9 +1,10 @@ // SPDX-License-Identifier: MIT - pragma solidity ^0.8.20; -import "../patched/access/Ownable2Step.sol"; +import {Ownable2Step, Ownable} from "../patched/access/Ownable2Step.sol"; contract Ownable2StepHarness is Ownable2Step { - function restricted() external onlyOwner {} + constructor(address initialOwner) Ownable(initialOwner) {} + + function restricted() external onlyOwner {} } diff --git a/certora/harnesses/OwnableHarness.sol b/certora/harnesses/OwnableHarness.sol index 45666772a88..79b4b1b6c56 100644 --- a/certora/harnesses/OwnableHarness.sol +++ b/certora/harnesses/OwnableHarness.sol @@ -1,9 +1,10 @@ // SPDX-License-Identifier: MIT - pragma solidity ^0.8.20; -import "../patched/access/Ownable.sol"; +import {Ownable} from "../patched/access/Ownable.sol"; contract OwnableHarness is Ownable { - function restricted() external onlyOwner {} + constructor(address initialOwner) Ownable(initialOwner) {} + + function restricted() external onlyOwner {} } diff --git a/certora/harnesses/PausableHarness.sol b/certora/harnesses/PausableHarness.sol index 12f94670904..5977b92022c 100644 --- a/certora/harnesses/PausableHarness.sol +++ b/certora/harnesses/PausableHarness.sol @@ -1,8 +1,7 @@ // SPDX-License-Identifier: MIT - pragma solidity ^0.8.20; -import "../patched/utils/Pausable.sol"; +import {Pausable} from "../patched/utils/Pausable.sol"; contract PausableHarness is Pausable { function pause() external { diff --git a/certora/harnesses/TimelockControllerHarness.sol b/certora/harnesses/TimelockControllerHarness.sol index 476a8376cbb..95ae4062115 100644 --- a/certora/harnesses/TimelockControllerHarness.sol +++ b/certora/harnesses/TimelockControllerHarness.sol @@ -1,6 +1,7 @@ +// SPDX-License-Identifier: MIT pragma solidity ^0.8.20; -import "../patched/governance/TimelockController.sol"; +import {TimelockController} from "../patched/governance/TimelockController.sol"; contract TimelockControllerHarness is TimelockController { constructor( diff --git a/certora/run.js b/certora/run.js index 68f34aab27c..7b65534ea1d 100755 --- a/certora/run.js +++ b/certora/run.js @@ -64,7 +64,13 @@ if (process.exitCode) { } for (const { spec, contract, files, options = [] } of specs) { - limit(runCertora, spec, contract, files, [...options.flatMap(opt => opt.split(' ')), ...argv.options]); + limit( + runCertora, + spec, + contract, + files, + [...options, ...argv.options].flatMap(opt => opt.split(' ')), + ); } // Run certora, aggregate the output and print it at the end diff --git a/certora/specs/AccessControl.spec b/certora/specs/AccessControl.spec index cd5af2a99c0..70b06721802 100644 --- a/certora/specs/AccessControl.spec +++ b/certora/specs/AccessControl.spec @@ -1,126 +1,119 @@ -import "helpers/helpers.spec" -import "methods/IAccessControl.spec" - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Definitions │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -definition DEFAULT_ADMIN_ROLE() returns bytes32 = 0x0000000000000000000000000000000000000000000000000000000000000000; - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Identify entrypoints: only grantRole, revokeRole and renounceRole can alter permissions │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -rule onlyGrantCanGrant(env e, method f, bytes32 role, address account) { - calldataarg args; - - bool hasRoleBefore = hasRole(role, account); - f(e, args); - bool hasRoleAfter = hasRole(role, account); - - assert ( - !hasRoleBefore && - hasRoleAfter - ) => ( - f.selector == grantRole(bytes32, address).selector - ); - - assert ( - hasRoleBefore && - !hasRoleAfter - ) => ( - f.selector == revokeRole(bytes32, address).selector || - f.selector == renounceRole(bytes32, address).selector - ); -} - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Function correctness: grantRole only affects the specified user/role combo │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -rule grantRoleEffect(env e, bytes32 role) { - require nonpayable(e); - - bytes32 otherRole; - address account; - address otherAccount; - - bool isCallerAdmin = hasRole(getRoleAdmin(role), e.msg.sender); - bool hasOtherRoleBefore = hasRole(otherRole, otherAccount); - - grantRole@withrevert(e, role, account); - bool success = !lastReverted; - - bool hasOtherRoleAfter = hasRole(otherRole, otherAccount); - - // liveness - assert success <=> isCallerAdmin; - - // effect - assert success => hasRole(role, account); - - // no side effect - assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount); -} - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Function correctness: revokeRole only affects the specified user/role combo │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -rule revokeRoleEffect(env e, bytes32 role) { - require nonpayable(e); - - bytes32 otherRole; - address account; - address otherAccount; - - bool isCallerAdmin = hasRole(getRoleAdmin(role), e.msg.sender); - bool hasOtherRoleBefore = hasRole(otherRole, otherAccount); - - revokeRole@withrevert(e, role, account); - bool success = !lastReverted; - - bool hasOtherRoleAfter = hasRole(otherRole, otherAccount); - - // liveness - assert success <=> isCallerAdmin; - - // effect - assert success => !hasRole(role, account); - - // no side effect - assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount); -} - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Function correctness: renounceRole only affects the specified user/role combo │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -rule renounceRoleEffect(env e, bytes32 role) { - require nonpayable(e); - - bytes32 otherRole; - address account; - address otherAccount; - - bool hasOtherRoleBefore = hasRole(otherRole, otherAccount); - - renounceRole@withrevert(e, role, account); - bool success = !lastReverted; - - bool hasOtherRoleAfter = hasRole(otherRole, otherAccount); - - // liveness - assert success <=> account == e.msg.sender; - - // effect - assert success => !hasRole(role, account); - - // no side effect - assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount); -} +import "helpers/helpers.spec"; +import "methods/IAccessControl.spec"; + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Identify entrypoints: only grantRole, revokeRole and renounceRole can alter permissions │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule onlyGrantCanGrant(env e, method f, bytes32 role, address account) { + calldataarg args; + + bool hasRoleBefore = hasRole(role, account); + f(e, args); + bool hasRoleAfter = hasRole(role, account); + + assert ( + !hasRoleBefore && + hasRoleAfter + ) => ( + f.selector == sig:grantRole(bytes32, address).selector + ); + + assert ( + hasRoleBefore && + !hasRoleAfter + ) => ( + f.selector == sig:revokeRole(bytes32, address).selector || + f.selector == sig:renounceRole(bytes32, address).selector + ); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function correctness: grantRole only affects the specified user/role combo │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule grantRoleEffect(env e, bytes32 role) { + require nonpayable(e); + + bytes32 otherRole; + address account; + address otherAccount; + + bool isCallerAdmin = hasRole(getRoleAdmin(role), e.msg.sender); + bool hasOtherRoleBefore = hasRole(otherRole, otherAccount); + + grantRole@withrevert(e, role, account); + bool success = !lastReverted; + + bool hasOtherRoleAfter = hasRole(otherRole, otherAccount); + + // liveness + assert success <=> isCallerAdmin; + + // effect + assert success => hasRole(role, account); + + // no side effect + assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function correctness: revokeRole only affects the specified user/role combo │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule revokeRoleEffect(env e, bytes32 role) { + require nonpayable(e); + + bytes32 otherRole; + address account; + address otherAccount; + + bool isCallerAdmin = hasRole(getRoleAdmin(role), e.msg.sender); + bool hasOtherRoleBefore = hasRole(otherRole, otherAccount); + + revokeRole@withrevert(e, role, account); + bool success = !lastReverted; + + bool hasOtherRoleAfter = hasRole(otherRole, otherAccount); + + // liveness + assert success <=> isCallerAdmin; + + // effect + assert success => !hasRole(role, account); + + // no side effect + assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function correctness: renounceRole only affects the specified user/role combo │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule renounceRoleEffect(env e, bytes32 role) { + require nonpayable(e); + + bytes32 otherRole; + address account; + address otherAccount; + + bool hasOtherRoleBefore = hasRole(otherRole, otherAccount); + + renounceRole@withrevert(e, role, account); + bool success = !lastReverted; + + bool hasOtherRoleAfter = hasRole(otherRole, otherAccount); + + // liveness + assert success <=> account == e.msg.sender; + + // effect + assert success => !hasRole(role, account); + + // no side effect + assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount); +} diff --git a/certora/specs/AccessControlDefaultAdminRules.spec b/certora/specs/AccessControlDefaultAdminRules.spec index 58b9d1202aa..2f5bb9d4538 100644 --- a/certora/specs/AccessControlDefaultAdminRules.spec +++ b/certora/specs/AccessControlDefaultAdminRules.spec @@ -1,28 +1,28 @@ -import "helpers/helpers.spec" -import "methods/IAccessControlDefaultAdminRules.spec" -import "methods/IAccessControl.spec" -import "AccessControl.spec" +import "helpers/helpers.spec"; +import "methods/IAccessControlDefaultAdminRules.spec"; +import "methods/IAccessControl.spec"; +import "AccessControl.spec"; use rule onlyGrantCanGrant filtered { - f -> f.selector != acceptDefaultAdminTransfer().selector + f -> f.selector != sig:acceptDefaultAdminTransfer().selector } /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Helpers │ +│ Definitions │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ definition timeSanity(env e) returns bool = - e.block.timestamp > 0 && e.block.timestamp + defaultAdminDelay(e) < max_uint48(); + e.block.timestamp > 0 && e.block.timestamp + defaultAdminDelay(e) < max_uint48; definition delayChangeWaitSanity(env e, uint48 newDelay) returns bool = - e.block.timestamp + delayChangeWait_(e, newDelay) < max_uint48(); + e.block.timestamp + delayChangeWait_(e, newDelay) < max_uint48; definition isSet(uint48 schedule) returns bool = schedule != 0; definition hasPassed(env e, uint48 schedule) returns bool = - schedule < e.block.timestamp; + assert_uint256(schedule) < e.block.timestamp; definition increasingDelaySchedule(env e, uint48 newDelay) returns mathint = e.block.timestamp + min(newDelay, defaultAdminDelayIncreaseWait()); @@ -63,7 +63,7 @@ invariant singleDefaultAdmin(address account, address another) └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ invariant defaultAdminRoleAdminConsistency() - getRoleAdmin(DEFAULT_ADMIN_ROLE()) == DEFAULT_ADMIN_ROLE() + getRoleAdmin(DEFAULT_ADMIN_ROLE()) == DEFAULT_ADMIN_ROLE(); /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ @@ -71,7 +71,7 @@ invariant defaultAdminRoleAdminConsistency() └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ invariant ownerConsistency() - defaultAdmin() == owner() + defaultAdmin() == owner(); /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ @@ -136,7 +136,7 @@ rule renounceRoleEffect(env e, bytes32 role) { account == e.msg.sender && ( role != DEFAULT_ADMIN_ROLE() || - account != adminBefore || + account != adminBefore || ( pendingAdminBefore == 0 && isSet(scheduleBefore) && @@ -185,8 +185,8 @@ rule noDefaultAdminChange(env e, method f, calldataarg args) { address adminAfter = defaultAdmin(); assert adminBefore != adminAfter => ( - f.selector == acceptDefaultAdminTransfer().selector || - f.selector == renounceRole(bytes32,address).selector + f.selector == sig:acceptDefaultAdminTransfer().selector || + f.selector == sig:renounceRole(bytes32,address).selector ), "default admin is only affected by accepting an admin transfer or renoucing"; } @@ -199,19 +199,19 @@ rule noDefaultAdminChange(env e, method f, calldataarg args) { */ rule noPendingDefaultAdminChange(env e, method f, calldataarg args) { address pendingAdminBefore = pendingDefaultAdmin_(); - address scheduleBefore = pendingDefaultAdminSchedule_(); + uint48 scheduleBefore = pendingDefaultAdminSchedule_(); f(e, args); address pendingAdminAfter = pendingDefaultAdmin_(); - address scheduleAfter = pendingDefaultAdminSchedule_(); + uint48 scheduleAfter = pendingDefaultAdminSchedule_(); assert ( pendingAdminBefore != pendingAdminAfter || scheduleBefore != scheduleAfter ) => ( - f.selector == beginDefaultAdminTransfer(address).selector || - f.selector == acceptDefaultAdminTransfer().selector || - f.selector == cancelDefaultAdminTransfer().selector || - f.selector == renounceRole(bytes32,address).selector + f.selector == sig:beginDefaultAdminTransfer(address).selector || + f.selector == sig:acceptDefaultAdminTransfer().selector || + f.selector == sig:cancelDefaultAdminTransfer().selector || + f.selector == sig:renounceRole(bytes32,address).selector ), "pending admin and its schedule is only affected by beginning, completing, or cancelling an admin transfer"; } @@ -241,8 +241,8 @@ rule noPendingDefaultAdminDelayChange(env e, method f, calldataarg args) { uint48 pendingDelayAfter = pendingDelay_(e); assert pendingDelayBefore != pendingDelayAfter => ( - f.selector == changeDefaultAdminDelay(uint48).selector || - f.selector == rollbackDefaultAdminDelay().selector + f.selector == sig:changeDefaultAdminDelay(uint48).selector || + f.selector == sig:rollbackDefaultAdminDelay().selector ), "pending delay is only affected by changeDefaultAdminDelay or rollbackDefaultAdminDelay"; } @@ -282,7 +282,7 @@ rule beginDefaultAdminTransfer(env e, address newAdmin) { // effect assert success => pendingDefaultAdmin_() == newAdmin, "pending default admin is set"; - assert success => pendingDefaultAdminSchedule_() == e.block.timestamp + defaultAdminDelay(e), + assert success => to_mathint(pendingDefaultAdminSchedule_()) == e.block.timestamp + defaultAdminDelay(e), "pending default admin delay is set"; } @@ -307,7 +307,7 @@ rule pendingDefaultAdminDelayEnforced(env e1, env e2, method f, calldataarg args // change can only happen towards the newAdmin, with the delay assert adminAfter != adminBefore => ( adminAfter == newAdmin && - e2.block.timestamp >= e1.block.timestamp + delayBefore + to_mathint(e2.block.timestamp) >= e1.block.timestamp + delayBefore ), "The admin can only change after the enforced delay and to the previously scheduled new admin"; } @@ -393,7 +393,7 @@ rule changeDefaultAdminDelay(env e, uint48 newDelay) { "pending delay is set"; assert success => ( - pendingDelaySchedule_(e) > e.block.timestamp || + assert_uint256(pendingDelaySchedule_(e)) > e.block.timestamp || delayBefore == newDelay || // Interpreted as decreasing, x - x = 0 defaultAdminDelayIncreaseWait() == 0 ), @@ -419,7 +419,7 @@ rule pendingDelayWaitEnforced(env e1, env e2, method f, calldataarg args, uint48 assert delayAfter != delayBefore => ( delayAfter == newDelay && - e2.block.timestamp >= delayWait + to_mathint(e2.block.timestamp) >= delayWait ), "A delay can only change after the applied schedule"; } @@ -433,9 +433,9 @@ rule pendingDelayWait(env e, uint48 newDelay) { uint48 oldDelay = defaultAdminDelay(e); changeDefaultAdminDelay(e, newDelay); - assert newDelay > oldDelay => pendingDelaySchedule_(e) == increasingDelaySchedule(e, newDelay), + assert newDelay > oldDelay => to_mathint(pendingDelaySchedule_(e)) == increasingDelaySchedule(e, newDelay), "Delay wait is the minimum between the new delay and a threshold when the delay is increased"; - assert newDelay <= oldDelay => pendingDelaySchedule_(e) == decreasingDelaySchedule(e, newDelay), + assert newDelay <= oldDelay => to_mathint(pendingDelaySchedule_(e)) == decreasingDelaySchedule(e, newDelay), "Delay wait is the difference between the current and the new delay when the delay is decreased"; } diff --git a/certora/specs/ERC20.spec b/certora/specs/ERC20.spec index 3bd2b38ba1c..ee601bd19da 100644 --- a/certora/specs/ERC20.spec +++ b/certora/specs/ERC20.spec @@ -1,15 +1,15 @@ -import "helpers/helpers.spec" -import "methods/IERC20.spec" -import "methods/IERC2612.spec" +import "helpers/helpers.spec"; +import "methods/IERC20.spec"; +import "methods/IERC2612.spec"; methods { // non standard ERC20 functions - increaseAllowance(address,uint256) returns (bool) - decreaseAllowance(address,uint256) returns (bool) + function increaseAllowance(address,uint256) external returns (bool); + function decreaseAllowance(address,uint256) external returns (bool); // exposed for FV - mint(address,uint256) - burn(address,uint256) + function mint(address,uint256) external; + function burn(address,uint256) external; } /* @@ -17,12 +17,22 @@ methods { │ Ghost & hooks: sum of all balances │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -ghost sumOfBalances() returns uint256 { - init_state axiom sumOfBalances() == 0; +ghost mathint sumOfBalances { + init_state axiom sumOfBalances == 0; +} + +// Because `balance` has a uint256 type, any balance addition in CVL1 behaved as a `require_uint256()` casting, +// leaving out the possibility of overflow. This is not the case in CVL2 where casting became more explicit. +// A counterexample in CVL2 is having an initial state where Alice initial balance is larger than totalSupply, which +// overflows Alice's balance when receiving a transfer. This is not possible unless the contract is deployed into an +// already used address (or upgraded from corrupted state). +// We restrict such behavior by making sure no balance is greater than the sum of balances. +hook Sload uint256 balance _balances[KEY address addr] STORAGE { + require sumOfBalances >= to_mathint(balance); } hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE { - havoc sumOfBalances assuming sumOfBalances@new() == sumOfBalances@old() + newValue - oldValue; + sumOfBalances = sumOfBalances - oldValue + newValue; } /* @@ -31,7 +41,7 @@ hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STOR └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ invariant totalSupplyIsSumOfBalances() - totalSupply() == sumOfBalances() + to_mathint(totalSupply()) == sumOfBalances; /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ @@ -39,7 +49,7 @@ invariant totalSupplyIsSumOfBalances() └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ invariant zeroAddressNoBalance() - balanceOf(0) == 0 + balanceOf(0) == 0; /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ @@ -56,8 +66,8 @@ rule noChangeTotalSupply(env e) { f(e, args); uint256 totalSupplyAfter = totalSupply(); - assert totalSupplyAfter > totalSupplyBefore => f.selector == mint(address,uint256).selector; - assert totalSupplyAfter < totalSupplyBefore => f.selector == burn(address,uint256).selector; + assert totalSupplyAfter > totalSupplyBefore => f.selector == sig:mint(address,uint256).selector; + assert totalSupplyAfter < totalSupplyBefore => f.selector == sig:burn(address,uint256).selector; } /* @@ -80,9 +90,9 @@ rule onlyAuthorizedCanTransfer(env e) { assert ( balanceAfter < balanceBefore ) => ( - f.selector == burn(address,uint256).selector || + f.selector == sig:burn(address,uint256).selector || e.msg.sender == account || - balanceBefore - balanceAfter <= allowanceBefore + balanceBefore - balanceAfter <= to_mathint(allowanceBefore) ); } @@ -106,18 +116,18 @@ rule onlyHolderOfSpenderCanChangeAllowance(env e) { assert ( allowanceAfter > allowanceBefore ) => ( - (f.selector == approve(address,uint256).selector && e.msg.sender == holder) || - (f.selector == increaseAllowance(address,uint256).selector && e.msg.sender == holder) || - (f.selector == permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector) + (f.selector == sig:approve(address,uint256).selector && e.msg.sender == holder) || + (f.selector == sig:increaseAllowance(address,uint256).selector && e.msg.sender == holder) || + (f.selector == sig:permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector) ); assert ( allowanceAfter < allowanceBefore ) => ( - (f.selector == transferFrom(address,address,uint256).selector && e.msg.sender == spender) || - (f.selector == approve(address,uint256).selector && e.msg.sender == holder ) || - (f.selector == decreaseAllowance(address,uint256).selector && e.msg.sender == holder ) || - (f.selector == permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector) + (f.selector == sig:transferFrom(address,address,uint256).selector && e.msg.sender == spender) || + (f.selector == sig:approve(address,uint256).selector && e.msg.sender == holder ) || + (f.selector == sig:decreaseAllowance(address,uint256).selector && e.msg.sender == holder ) || + (f.selector == sig:permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector) ); } @@ -147,8 +157,8 @@ rule mint(env e) { assert to == 0 || totalSupplyBefore + amount > max_uint256; } else { // updates balance and totalSupply - assert balanceOf(to) == toBalanceBefore + amount; - assert totalSupply() == totalSupplyBefore + amount; + assert to_mathint(balanceOf(to)) == toBalanceBefore + amount; + assert to_mathint(totalSupply()) == totalSupplyBefore + amount; // no other balance is modified assert balanceOf(other) != otherBalanceBefore => other == to; @@ -181,8 +191,8 @@ rule burn(env e) { assert from == 0 || fromBalanceBefore < amount; } else { // updates balance and totalSupply - assert balanceOf(from) == fromBalanceBefore - amount; - assert totalSupply() == totalSupplyBefore - amount; + assert to_mathint(balanceOf(from)) == fromBalanceBefore - amount; + assert to_mathint(totalSupply()) == totalSupplyBefore - amount; // no other balance is modified assert balanceOf(other) != otherBalanceBefore => other == from; @@ -216,8 +226,8 @@ rule transfer(env e) { assert holder == 0 || recipient == 0 || amount > holderBalanceBefore; } else { // balances of holder and recipient are updated - assert balanceOf(holder) == holderBalanceBefore - (holder == recipient ? 0 : amount); - assert balanceOf(recipient) == recipientBalanceBefore + (holder == recipient ? 0 : amount); + assert to_mathint(balanceOf(holder)) == holderBalanceBefore - (holder == recipient ? 0 : amount); + assert to_mathint(balanceOf(recipient)) == recipientBalanceBefore + (holder == recipient ? 0 : amount); // no other balance is modified assert balanceOf(other) != otherBalanceBefore => (other == holder || other == recipient); @@ -254,11 +264,11 @@ rule transferFrom(env e) { } else { // allowance is valid & updated assert allowanceBefore >= amount; - assert allowance(holder, spender) == (allowanceBefore == max_uint256 ? to_uint256(max_uint256) : allowanceBefore - amount); + assert to_mathint(allowance(holder, spender)) == (allowanceBefore == max_uint256 ? max_uint256 : allowanceBefore - amount); // balances of holder and recipient are updated - assert balanceOf(holder) == holderBalanceBefore - (holder == recipient ? 0 : amount); - assert balanceOf(recipient) == recipientBalanceBefore + (holder == recipient ? 0 : amount); + assert to_mathint(balanceOf(holder)) == holderBalanceBefore - (holder == recipient ? 0 : amount); + assert to_mathint(balanceOf(recipient)) == recipientBalanceBefore + (holder == recipient ? 0 : amount); // no other balance is modified assert balanceOf(other) != otherBalanceBefore => (other == holder || other == recipient); @@ -323,7 +333,7 @@ rule increaseAllowance(env e) { assert holder == 0 || spender == 0 || allowanceBefore + amount > max_uint256; } else { // allowance is updated - assert allowance(holder, spender) == allowanceBefore + amount; + assert to_mathint(allowance(holder, spender)) == allowanceBefore + amount; // other allowances are untouched assert allowance(otherHolder, otherSpender) != otherAllowanceBefore => (otherHolder == holder && otherSpender == spender); @@ -356,7 +366,7 @@ rule decreaseAllowance(env e) { assert holder == 0 || spender == 0 || allowanceBefore < amount; } else { // allowance is updated - assert allowance(holder, spender) == allowanceBefore - amount; + assert to_mathint(allowance(holder, spender)) == allowanceBefore - amount; // other allowances are untouched assert allowance(otherHolder, otherSpender) != otherAllowanceBefore => (otherHolder == holder && otherSpender == spender); @@ -402,7 +412,7 @@ rule permit(env e) { } else { // allowance and nonce are updated assert allowance(holder, spender) == amount; - assert nonces(holder) == nonceBefore + 1; + assert to_mathint(nonces(holder)) == nonceBefore + 1; // deadline was respected assert deadline >= e.block.timestamp; diff --git a/certora/specs/ERC20FlashMint.spec b/certora/specs/ERC20FlashMint.spec index 70a7c07951f..5c87f0ded79 100644 --- a/certora/specs/ERC20FlashMint.spec +++ b/certora/specs/ERC20FlashMint.spec @@ -1,15 +1,14 @@ -import "helpers/helpers.spec" -import "methods/IERC20.spec" -import "methods/IERC3156.spec" +import "helpers/helpers.spec"; +import "methods/IERC20.spec"; +import "methods/IERC3156FlashLender.spec"; +import "methods/IERC3156FlashBorrower.spec"; methods { // non standard ERC3156 functions - flashFeeReceiver() returns (address) envfree + function flashFeeReceiver() external returns (address) envfree; // function summaries below - _mint(address account, uint256 amount) => specMint(account, amount) - _burn(address account, uint256 amount) => specBurn(account, amount) - _transfer(address from, address to, uint256 amount) => specTransfer(from, to, amount) + function _._update(address from, address to, uint256 amount) internal => specUpdate(from, to, amount) expect void ALL; } /* @@ -17,13 +16,21 @@ methods { │ Ghost: track mint and burns in the CVL │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -ghost mapping(address => uint256) trackedMintAmount; -ghost mapping(address => uint256) trackedBurnAmount; -ghost mapping(address => mapping(address => uint256)) trackedTransferedAmount; - -function specMint(address account, uint256 amount) returns bool { trackedMintAmount[account] = amount; return true; } -function specBurn(address account, uint256 amount) returns bool { trackedBurnAmount[account] = amount; return true; } -function specTransfer(address from, address to, uint256 amount) returns bool { trackedTransferedAmount[from][to] = amount; return true; } +ghost mapping(address => mathint) trackedMintAmount; +ghost mapping(address => mathint) trackedBurnAmount; +ghost mapping(address => mapping(address => mathint)) trackedTransferedAmount; + +function specUpdate(address from, address to, uint256 amount) { + if (from == 0 && to == 0) { assert(false); } // defensive + + if (from == 0) { + trackedMintAmount[to] = amount; + } else if (to == 0) { + trackedBurnAmount[from] = amount; + } else { + trackedTransferedAmount[from][to] = amount; + } +} /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ @@ -42,7 +49,7 @@ rule checkMintAndBurn(env e) { flashLoan(e, receiver, token, amount, data); - assert trackedMintAmount[receiver] == amount; - assert trackedBurnAmount[receiver] == amount + (recipient == 0 ? fees : 0); - assert (fees > 0 && recipient != 0) => trackedTransferedAmount[receiver][recipient] == fees; + assert trackedMintAmount[receiver] == to_mathint(amount); + assert trackedBurnAmount[receiver] == amount + to_mathint(recipient == 0 ? fees : 0); + assert (fees > 0 && recipient != 0) => trackedTransferedAmount[receiver][recipient] == to_mathint(fees); } diff --git a/certora/specs/ERC20Wrapper.spec b/certora/specs/ERC20Wrapper.spec index badfa7a2848..04e67042a35 100644 --- a/certora/specs/ERC20Wrapper.spec +++ b/certora/specs/ERC20Wrapper.spec @@ -1,31 +1,29 @@ -import "helpers/helpers.spec" -import "ERC20.spec" +import "helpers/helpers.spec"; +import "ERC20.spec"; methods { - underlying() returns(address) envfree - underlyingTotalSupply() returns(uint256) envfree - underlyingBalanceOf(address) returns(uint256) envfree - underlyingAllowanceToThis(address) returns(uint256) envfree - - depositFor(address, uint256) returns(bool) - withdrawTo(address, uint256) returns(bool) - recover(address) returns(uint256) + function underlying() external returns(address) envfree; + function underlyingTotalSupply() external returns(uint256) envfree; + function underlyingBalanceOf(address) external returns(uint256) envfree; + function underlyingAllowanceToThis(address) external returns(uint256) envfree; + + function depositFor(address, uint256) external returns(bool); + function withdrawTo(address, uint256) external returns(bool); + function recover(address) external returns(uint256); } -use invariant totalSupplyIsSumOfBalances +use invariant totalSupplyIsSumOfBalances; /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Helper: consequence of `totalSupplyIsSumOfBalances` applied to underlying │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -function underlyingBalancesLowerThanUnderlyingSupply(address a) returns bool { - return underlyingBalanceOf(a) <= underlyingTotalSupply(); -} +definition underlyingBalancesLowerThanUnderlyingSupply(address a) returns bool = + underlyingBalanceOf(a) <= underlyingTotalSupply(); -function sumOfUnderlyingBalancesLowerThanUnderlyingSupply(address a, address b) returns bool { - return a != b => underlyingBalanceOf(a) + underlyingBalanceOf(b) <= underlyingTotalSupply(); -} +definition sumOfUnderlyingBalancesLowerThanUnderlyingSupply(address a, address b) returns bool = + a != b => underlyingBalanceOf(a) + underlyingBalanceOf(b) <= to_mathint(underlyingTotalSupply()); /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ @@ -47,7 +45,7 @@ invariant totalSupplyIsSmallerThanUnderlyingBalance() } invariant noSelfWrap() - currentContract != underlying() + currentContract != underlying(); /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ @@ -85,6 +83,7 @@ rule depositFor(env e) { assert success <=> ( sender != currentContract && // invalid sender sender != 0 && // invalid sender + receiver != currentContract && // invalid receiver receiver != 0 && // invalid receiver amount <= senderUnderlyingBalanceBefore && // deposit doesn't exceed balance amount <= senderUnderlyingAllowanceBefore // deposit doesn't exceed allowance @@ -92,10 +91,10 @@ rule depositFor(env e) { // effects assert success => ( - balanceOf(receiver) == balanceBefore + amount && - totalSupply() == supplyBefore + amount && - underlyingBalanceOf(currentContract) == wrapperUnderlyingBalanceBefore + amount && - underlyingBalanceOf(sender) == senderUnderlyingBalanceBefore - amount + to_mathint(balanceOf(receiver)) == balanceBefore + amount && + to_mathint(totalSupply()) == supplyBefore + amount && + to_mathint(underlyingBalanceOf(currentContract)) == wrapperUnderlyingBalanceBefore + amount && + to_mathint(underlyingBalanceOf(sender)) == senderUnderlyingBalanceBefore - amount ); // no side effect @@ -137,17 +136,18 @@ rule withdrawTo(env e) { // liveness assert success <=> ( - sender != 0 && // invalid sender - receiver != 0 && // invalid receiver - amount <= balanceBefore // withdraw doesn't exceed balance + sender != 0 && // invalid sender + receiver != currentContract && // invalid receiver + receiver != 0 && // invalid receiver + amount <= balanceBefore // withdraw doesn't exceed balance ); // effects assert success => ( - balanceOf(sender) == balanceBefore - amount && - totalSupply() == supplyBefore - amount && - underlyingBalanceOf(currentContract) == wrapperUnderlyingBalanceBefore - (currentContract != receiver ? amount : 0) && - underlyingBalanceOf(receiver) == receiverUnderlyingBalanceBefore + (currentContract != receiver ? amount : 0) + to_mathint(balanceOf(sender)) == balanceBefore - amount && + to_mathint(totalSupply()) == supplyBefore - amount && + to_mathint(underlyingBalanceOf(currentContract)) == wrapperUnderlyingBalanceBefore - (currentContract != receiver ? amount : 0) && + to_mathint(underlyingBalanceOf(receiver)) == receiverUnderlyingBalanceBefore + (currentContract != receiver ? amount : 0) ); // no side effect @@ -172,7 +172,7 @@ rule recover(env e) { requireInvariant totalSupplyIsSumOfBalances; requireInvariant totalSupplyIsSmallerThanUnderlyingBalance; - uint256 value = underlyingBalanceOf(currentContract) - totalSupply(); + mathint value = underlyingBalanceOf(currentContract) - totalSupply(); uint256 supplyBefore = totalSupply(); uint256 balanceBefore = balanceOf(receiver); @@ -187,8 +187,8 @@ rule recover(env e) { // effect assert success => ( - balanceOf(receiver) == balanceBefore + value && - totalSupply() == supplyBefore + value && + to_mathint(balanceOf(receiver)) == balanceBefore + value && + to_mathint(totalSupply()) == supplyBefore + value && totalSupply() == underlyingBalanceOf(currentContract) ); diff --git a/certora/specs/ERC721.spec b/certora/specs/ERC721.spec index 9db13f45cbe..bad4c473772 100644 --- a/certora/specs/ERC721.spec +++ b/certora/specs/ERC721.spec @@ -1,16 +1,16 @@ -import "helpers/helpers.spec" -import "methods/IERC721.spec" +import "helpers/helpers.spec"; +import "methods/IERC721.spec"; +import "methods/IERC721Receiver.spec"; methods { // exposed for FV - mint(address,uint256) - safeMint(address,uint256) - safeMint(address,uint256,bytes) - burn(uint256) - - tokenExists(uint256) returns (bool) envfree - unsafeOwnerOf(uint256) returns (address) envfree - unsafeGetApproved(uint256) returns (address) envfree + function mint(address,uint256) external; + function safeMint(address,uint256) external; + function safeMint(address,uint256,bytes) external; + function burn(uint256) external; + + function unsafeOwnerOf(uint256) external returns (address) envfree; + function unsafeGetApproved(uint256) external returns (address) envfree; } /* @@ -19,17 +19,17 @@ methods { └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ +definition authSanity(env e) returns bool = e.msg.sender != 0; + // Could be broken in theory, but not in practice -function balanceLimited(address account) returns bool { - return balanceOf(account) < max_uint256; -} +definition balanceLimited(address account) returns bool = balanceOf(account) < max_uint256; function helperTransferWithRevert(env e, method f, address from, address to, uint256 tokenId) { - if (f.selector == transferFrom(address,address,uint256).selector) { + if (f.selector == sig:transferFrom(address,address,uint256).selector) { transferFrom@withrevert(e, from, to, tokenId); - } else if (f.selector == safeTransferFrom(address,address,uint256).selector) { + } else if (f.selector == sig:safeTransferFrom(address,address,uint256).selector) { safeTransferFrom@withrevert(e, from, to, tokenId); - } else if (f.selector == safeTransferFrom(address,address,uint256,bytes).selector) { + } else if (f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector) { bytes params; require params.length < 0xffff; safeTransferFrom@withrevert(e, from, to, tokenId, params); @@ -40,11 +40,11 @@ function helperTransferWithRevert(env e, method f, address from, address to, uin } function helperMintWithRevert(env e, method f, address to, uint256 tokenId) { - if (f.selector == mint(address,uint256).selector) { + if (f.selector == sig:mint(address,uint256).selector) { mint@withrevert(e, to, tokenId); - } else if (f.selector == safeMint(address,uint256).selector) { + } else if (f.selector == sig:safeMint(address,uint256).selector) { safeMint@withrevert(e, to, tokenId); - } else if (f.selector == safeMint(address,uint256,bytes).selector) { + } else if (f.selector == sig:safeMint(address,uint256,bytes).selector) { bytes params; require params.length < 0xffff; safeMint@withrevert(e, to, tokenId, params); @@ -53,26 +53,70 @@ function helperMintWithRevert(env e, method f, address to, uint256 tokenId) { } } +function helperSoundFnCall(env e, method f) { + if (f.selector == sig:mint(address,uint256).selector) { + address to; uint256 tokenId; + require balanceLimited(to); + requireInvariant notMintedUnset(tokenId); + mint(e, to, tokenId); + } else if (f.selector == sig:safeMint(address,uint256).selector) { + address to; uint256 tokenId; + require balanceLimited(to); + requireInvariant notMintedUnset(tokenId); + safeMint(e, to, tokenId); + } else if (f.selector == sig:safeMint(address,uint256,bytes).selector) { + address to; uint256 tokenId; bytes data; + require data.length < 0xffff; + require balanceLimited(to); + requireInvariant notMintedUnset(tokenId); + safeMint(e, to, tokenId, data); + } else if (f.selector == sig:burn(uint256).selector) { + uint256 tokenId; + requireInvariant ownerHasBalance(tokenId); + requireInvariant notMintedUnset(tokenId); + burn(e, tokenId); + } else if (f.selector == sig:transferFrom(address,address,uint256).selector) { + address from; address to; uint256 tokenId; + require balanceLimited(to); + requireInvariant ownerHasBalance(tokenId); + requireInvariant notMintedUnset(tokenId); + transferFrom(e, from, to, tokenId); + } else if (f.selector == sig:safeTransferFrom(address,address,uint256).selector) { + address from; address to; uint256 tokenId; + require balanceLimited(to); + requireInvariant ownerHasBalance(tokenId); + requireInvariant notMintedUnset(tokenId); + safeTransferFrom(e, from, to, tokenId); + } else if (f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector) { + address from; address to; uint256 tokenId; bytes data; + require data.length < 0xffff; + require balanceLimited(to); + requireInvariant ownerHasBalance(tokenId); + requireInvariant notMintedUnset(tokenId); + safeTransferFrom(e, from, to, tokenId, data); + } else { + calldataarg args; + f(e, args); + } +} + /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Ghost & hooks: ownership count │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -ghost ownedTotal() returns uint256 { - init_state axiom ownedTotal() == 0; +ghost mathint _ownedTotal { + init_state axiom _ownedTotal == 0; } -ghost mapping(address => uint256) ownedByUser { - init_state axiom forall address a. ownedByUser[a] == 0; +ghost mapping(address => mathint) _ownedByUser { + init_state axiom forall address a. _ownedByUser[a] == 0; } hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) STORAGE { - ownedByUser[newOwner] = ownedByUser[newOwner] + to_uint256(newOwner != 0 ? 1 : 0); - ownedByUser[oldOwner] = ownedByUser[oldOwner] - to_uint256(oldOwner != 0 ? 1 : 0); - - havoc ownedTotal assuming ownedTotal@new() == ownedTotal@old() - + to_uint256(newOwner != 0 ? 1 : 0) - - to_uint256(oldOwner != 0 ? 1 : 0); + _ownedByUser[newOwner] = _ownedByUser[newOwner] + to_mathint(newOwner != 0 ? 1 : 0); + _ownedByUser[oldOwner] = _ownedByUser[oldOwner] - to_mathint(oldOwner != 0 ? 1 : 0); + _ownedTotal = _ownedTotal + to_mathint(newOwner != 0 ? 1 : 0) - to_mathint(oldOwner != 0 ? 1 : 0); } /* @@ -80,29 +124,64 @@ hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) STO │ Ghost & hooks: sum of all balances │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -ghost sumOfBalances() returns uint256 { - init_state axiom sumOfBalances() == 0; +ghost mathint _supply { + init_state axiom _supply == 0; } -hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE { - havoc sumOfBalances assuming sumOfBalances@new() == sumOfBalances@old() + newValue - oldValue; +ghost mapping(address => mathint) _balances { + init_state axiom forall address a. _balances[a] == 0; } -ghost mapping(address => uint256) ghostBalanceOf { - init_state axiom forall address a. ghostBalanceOf[a] == 0; +hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE { + _supply = _supply - oldValue + newValue; } +// TODO: This used to not be necessary. We should try to remove it. In order to do so, we will probably need to add +// many "preserved" directive that require the "balanceOfConsistency" invariant on the accounts involved. hook Sload uint256 value _balances[KEY address user] STORAGE { - require ghostBalanceOf[user] == value; + require _balances[user] == to_mathint(value); } /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Invariant: ownedTotal is the sum of all balances │ +│ Invariant: number of owned tokens is the sum of all balances │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ invariant ownedTotalIsSumOfBalances() - ownedTotal() == sumOfBalances() + _ownedTotal == _supply + { + preserved mint(address to, uint256 tokenId) with (env e) { + require balanceLimited(to); + } + preserved safeMint(address to, uint256 tokenId) with (env e) { + require balanceLimited(to); + } + preserved safeMint(address to, uint256 tokenId, bytes data) with (env e) { + require balanceLimited(to); + } + preserved burn(uint256 tokenId) with (env e) { + requireInvariant ownerHasBalance(tokenId); + requireInvariant balanceOfConsistency(ownerOf(tokenId)); + } + preserved transferFrom(address from, address to, uint256 tokenId) with (env e) { + require balanceLimited(to); + requireInvariant ownerHasBalance(tokenId); + requireInvariant balanceOfConsistency(from); + requireInvariant balanceOfConsistency(to); + } + preserved safeTransferFrom(address from, address to, uint256 tokenId) with (env e) { + require balanceLimited(to); + requireInvariant ownerHasBalance(tokenId); + requireInvariant balanceOfConsistency(from); + requireInvariant balanceOfConsistency(to); + } + preserved safeTransferFrom(address from, address to, uint256 tokenId, bytes data) with (env e) { + require balanceLimited(to); + requireInvariant ownerHasBalance(tokenId); + requireInvariant balanceOfConsistency(from); + requireInvariant balanceOfConsistency(to); + } + } /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ @@ -110,8 +189,8 @@ invariant ownedTotalIsSumOfBalances() └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ invariant balanceOfConsistency(address user) - balanceOf(user) == ownedByUser[user] && - balanceOf(user) == ghostBalanceOf[user] + to_mathint(balanceOf(user)) == _ownedByUser[user] && + to_mathint(balanceOf(user)) == _balances[user] { preserved { require balanceLimited(user); @@ -134,53 +213,56 @@ invariant ownerHasBalance(uint256 tokenId) /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Invariant: tokens that do not exist are not owned and not approved │ +│ Rule: balance of address(0) is 0 │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -invariant notMintedUnset(uint256 tokenId) - (!tokenExists(tokenId) <=> unsafeOwnerOf(tokenId) == 0) && - (!tokenExists(tokenId) => unsafeGetApproved(tokenId) == 0) +rule zeroAddressBalanceRevert() { + balanceOf@withrevert(0); + assert lastReverted; +} /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Rule: ownerOf and getApproved revert if token does not exist │ +│ Invariant: address(0) has no authorized operator │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -rule notMintedRevert(uint256 tokenId) { - requireInvariant notMintedUnset(tokenId); - - bool e = tokenExists(tokenId); - - address owner = ownerOf@withrevert(tokenId); - assert e <=> !lastReverted; - assert e => owner == unsafeOwnerOf(tokenId); // notMintedUnset tells us this is non-zero - - address approved = getApproved@withrevert(tokenId); - assert e <=> !lastReverted; - assert e => approved == unsafeGetApproved(tokenId); -} +invariant zeroAddressHasNoApprovedOperator(address a) + !isApprovedForAll(0, a) + { + preserved with (env e) { + require nonzerosender(e); + } + } /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Rule: unsafeOwnerOf and unsafeGetApproved don't revert │ +│ Invariant: tokens that do not exist are not owned and not approved │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -rule unsafeDontRevert(uint256 tokenId) { - unsafeOwnerOf@withrevert(tokenId); - assert !lastReverted; - - unsafeGetApproved@withrevert(tokenId); - assert !lastReverted; -} +invariant notMintedUnset(uint256 tokenId) + unsafeOwnerOf(tokenId) == 0 => unsafeGetApproved(tokenId) == 0; /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Rule: balance of address(0) is 0 │ +│ Rule: unsafeOwnerOf and unsafeGetApproved don't revert + ownerOf and getApproved revert if token does not exist │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -rule zeroAddressBalanceRevert() { - balanceOf@withrevert(0); - assert lastReverted; +rule notMintedRevert(uint256 tokenId) { + requireInvariant notMintedUnset(tokenId); + + address _owner = unsafeOwnerOf@withrevert(tokenId); + assert !lastReverted; + + address _approved = unsafeGetApproved@withrevert(tokenId); + assert !lastReverted; + + address owner = ownerOf@withrevert(tokenId); + assert lastReverted <=> _owner == 0; + assert !lastReverted => _owner == owner; + + address approved = getApproved@withrevert(tokenId); + assert lastReverted <=> _owner == 0; + assert !lastReverted => _approved == approved; } /* @@ -189,21 +271,24 @@ rule zeroAddressBalanceRevert() { └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule supplyChange(env e) { - uint256 supplyBefore = ownedTotal(); - method f; calldataarg args; f(e, args); - uint256 supplyAfter = ownedTotal(); + require nonzerosender(e); + requireInvariant zeroAddressHasNoApprovedOperator(e.msg.sender); + + mathint supplyBefore = _supply; + method f; helperSoundFnCall(e, f); + mathint supplyAfter = _supply; assert supplyAfter > supplyBefore => ( supplyAfter == supplyBefore + 1 && ( - f.selector == mint(address,uint256).selector || - f.selector == safeMint(address,uint256).selector || - f.selector == safeMint(address,uint256,bytes).selector + f.selector == sig:mint(address,uint256).selector || + f.selector == sig:safeMint(address,uint256).selector || + f.selector == sig:safeMint(address,uint256,bytes).selector ) ); assert supplyAfter < supplyBefore => ( supplyAfter == supplyBefore - 1 && - f.selector == burn(uint256).selector + f.selector == sig:burn(uint256).selector ); } @@ -216,9 +301,9 @@ rule balanceChange(env e, address account) { requireInvariant balanceOfConsistency(account); require balanceLimited(account); - uint256 balanceBefore = balanceOf(account); - method f; calldataarg args; f(e, args); - uint256 balanceAfter = balanceOf(account); + mathint balanceBefore = balanceOf(account); + method f; helperSoundFnCall(e, f); + mathint balanceAfter = balanceOf(account); // balance can change by at most 1 assert balanceBefore != balanceAfter => ( @@ -228,13 +313,13 @@ rule balanceChange(env e, address account) { // only selected function can change balances assert balanceBefore != balanceAfter => ( - f.selector == transferFrom(address,address,uint256).selector || - f.selector == safeTransferFrom(address,address,uint256).selector || - f.selector == safeTransferFrom(address,address,uint256,bytes).selector || - f.selector == mint(address,uint256).selector || - f.selector == safeMint(address,uint256).selector || - f.selector == safeMint(address,uint256,bytes).selector || - f.selector == burn(uint256).selector + f.selector == sig:transferFrom(address,address,uint256).selector || + f.selector == sig:safeTransferFrom(address,address,uint256).selector || + f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector || + f.selector == sig:mint(address,uint256).selector || + f.selector == sig:safeMint(address,uint256).selector || + f.selector == sig:safeMint(address,uint256,bytes).selector || + f.selector == sig:burn(uint256).selector ); } @@ -244,24 +329,27 @@ rule balanceChange(env e, address account) { └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule ownershipChange(env e, uint256 tokenId) { + require nonzerosender(e); + requireInvariant zeroAddressHasNoApprovedOperator(e.msg.sender); + address ownerBefore = unsafeOwnerOf(tokenId); - method f; calldataarg args; f(e, args); + method f; helperSoundFnCall(e, f); address ownerAfter = unsafeOwnerOf(tokenId); assert ownerBefore == 0 && ownerAfter != 0 => ( - f.selector == mint(address,uint256).selector || - f.selector == safeMint(address,uint256).selector || - f.selector == safeMint(address,uint256,bytes).selector + f.selector == sig:mint(address,uint256).selector || + f.selector == sig:safeMint(address,uint256).selector || + f.selector == sig:safeMint(address,uint256,bytes).selector ); assert ownerBefore != 0 && ownerAfter == 0 => ( - f.selector == burn(uint256).selector + f.selector == sig:burn(uint256).selector ); assert (ownerBefore != ownerAfter && ownerBefore != 0 && ownerAfter != 0) => ( - f.selector == transferFrom(address,address,uint256).selector || - f.selector == safeTransferFrom(address,address,uint256).selector || - f.selector == safeTransferFrom(address,address,uint256,bytes).selector + f.selector == sig:transferFrom(address,address,uint256).selector || + f.selector == sig:safeTransferFrom(address,address,uint256).selector || + f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector ); } @@ -272,18 +360,18 @@ rule ownershipChange(env e, uint256 tokenId) { */ rule approvalChange(env e, uint256 tokenId) { address approvalBefore = unsafeGetApproved(tokenId); - method f; calldataarg args; f(e, args); + method f; helperSoundFnCall(e, f); address approvalAfter = unsafeGetApproved(tokenId); // approve can set any value, other functions reset assert approvalBefore != approvalAfter => ( - f.selector == approve(address,uint256).selector || + f.selector == sig:approve(address,uint256).selector || ( ( - f.selector == transferFrom(address,address,uint256).selector || - f.selector == safeTransferFrom(address,address,uint256).selector || - f.selector == safeTransferFrom(address,address,uint256,bytes).selector || - f.selector == burn(uint256).selector + f.selector == sig:transferFrom(address,address,uint256).selector || + f.selector == sig:safeTransferFrom(address,address,uint256).selector || + f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector || + f.selector == sig:burn(uint256).selector ) && approvalAfter == 0 ) ); @@ -296,10 +384,10 @@ rule approvalChange(env e, uint256 tokenId) { */ rule approvedForAllChange(env e, address owner, address spender) { bool approvedForAllBefore = isApprovedForAll(owner, spender); - method f; calldataarg args; f(e, args); + method f; helperSoundFnCall(e, f); bool approvedForAllAfter = isApprovedForAll(owner, spender); - assert approvedForAllBefore != approvedForAllAfter => f.selector == setApprovalForAll(address,bool).selector; + assert approvedForAllBefore != approvedForAllAfter => f.selector == sig:setApprovalForAll(address,bool).selector; } /* @@ -309,6 +397,7 @@ rule approvedForAllChange(env e, address owner, address spender) { */ rule transferFrom(env e, address from, address to, uint256 tokenId) { require nonpayable(e); + require authSanity(e); address operator = e.msg.sender; uint256 otherTokenId; @@ -338,10 +427,10 @@ rule transferFrom(env e, address from, address to, uint256 tokenId) { // effect assert success => ( - balanceOf(from) == balanceOfFromBefore - to_uint256(from != to ? 1 : 0) && - balanceOf(to) == balanceOfToBefore + to_uint256(from != to ? 1 : 0) && - unsafeOwnerOf(tokenId) == to && - unsafeGetApproved(tokenId) == 0 + to_mathint(balanceOf(from)) == balanceOfFromBefore - assert_uint256(from != to ? 1 : 0) && + to_mathint(balanceOf(to)) == balanceOfToBefore + assert_uint256(from != to ? 1 : 0) && + unsafeOwnerOf(tokenId) == to && + unsafeGetApproved(tokenId) == 0 ); // no side effect @@ -356,10 +445,11 @@ rule transferFrom(env e, address from, address to, uint256 tokenId) { └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule safeTransferFrom(env e, method f, address from, address to, uint256 tokenId) filtered { f -> - f.selector == safeTransferFrom(address,address,uint256).selector || - f.selector == safeTransferFrom(address,address,uint256,bytes).selector + f.selector == sig:safeTransferFrom(address,address,uint256).selector || + f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector } { require nonpayable(e); + require authSanity(e); address operator = e.msg.sender; uint256 otherTokenId; @@ -388,10 +478,10 @@ rule safeTransferFrom(env e, method f, address from, address to, uint256 tokenId // effect assert success => ( - balanceOf(from) == balanceOfFromBefore - to_uint256(from != to ? 1: 0) && - balanceOf(to) == balanceOfToBefore + to_uint256(from != to ? 1: 0) && - unsafeOwnerOf(tokenId) == to && - unsafeGetApproved(tokenId) == 0 + to_mathint(balanceOf(from)) == balanceOfFromBefore - assert_uint256(from != to ? 1: 0) && + to_mathint(balanceOf(to)) == balanceOfToBefore + assert_uint256(from != to ? 1: 0) && + unsafeOwnerOf(tokenId) == to && + unsafeGetApproved(tokenId) == 0 ); // no side effect @@ -414,7 +504,7 @@ rule mint(env e, address to, uint256 tokenId) { require balanceLimited(to); - uint256 supplyBefore = ownedTotal(); + mathint supplyBefore = _supply; uint256 balanceOfToBefore = balanceOf(to); uint256 balanceOfOtherBefore = balanceOf(otherAccount); address ownerBefore = unsafeOwnerOf(tokenId); @@ -431,9 +521,9 @@ rule mint(env e, address to, uint256 tokenId) { // effect assert success => ( - ownedTotal() == supplyBefore + 1 && - balanceOf(to) == balanceOfToBefore + 1 && - unsafeOwnerOf(tokenId) == to + _supply == supplyBefore + 1 && + to_mathint(balanceOf(to)) == balanceOfToBefore + 1 && + unsafeOwnerOf(tokenId) == to ); // no side effect @@ -447,8 +537,8 @@ rule mint(env e, address to, uint256 tokenId) { └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule safeMint(env e, method f, address to, uint256 tokenId) filtered { f -> - f.selector == safeMint(address,uint256).selector || - f.selector == safeMint(address,uint256,bytes).selector + f.selector == sig:safeMint(address,uint256).selector || + f.selector == sig:safeMint(address,uint256,bytes).selector } { require nonpayable(e); requireInvariant notMintedUnset(tokenId); @@ -458,7 +548,7 @@ rule safeMint(env e, method f, address to, uint256 tokenId) filtered { f -> require balanceLimited(to); - uint256 supplyBefore = ownedTotal(); + mathint supplyBefore = _supply; uint256 balanceOfToBefore = balanceOf(to); uint256 balanceOfOtherBefore = balanceOf(otherAccount); address ownerBefore = unsafeOwnerOf(tokenId); @@ -474,9 +564,9 @@ rule safeMint(env e, method f, address to, uint256 tokenId) filtered { f -> // effect assert success => ( - ownedTotal() == supplyBefore + 1 && - balanceOf(to) == balanceOfToBefore + 1 && - unsafeOwnerOf(tokenId) == to + _supply == supplyBefore + 1 && + to_mathint(balanceOf(to)) == balanceOfToBefore + 1 && + unsafeOwnerOf(tokenId) == to ); // no side effect @@ -498,7 +588,7 @@ rule burn(env e, uint256 tokenId) { requireInvariant ownerHasBalance(tokenId); - uint256 supplyBefore = ownedTotal(); + mathint supplyBefore = _supply; uint256 balanceOfFromBefore = balanceOf(from); uint256 balanceOfOtherBefore = balanceOf(otherAccount); address ownerBefore = unsafeOwnerOf(tokenId); @@ -515,10 +605,10 @@ rule burn(env e, uint256 tokenId) { // effect assert success => ( - ownedTotal() == supplyBefore - 1 && - balanceOf(from) == balanceOfFromBefore - 1 && - unsafeOwnerOf(tokenId) == 0 && - unsafeGetApproved(tokenId) == 0 + _supply == supplyBefore - 1 && + to_mathint(balanceOf(from)) == balanceOfFromBefore - 1 && + unsafeOwnerOf(tokenId) == 0 && + unsafeGetApproved(tokenId) == 0 ); // no side effect @@ -534,6 +624,7 @@ rule burn(env e, uint256 tokenId) { */ rule approve(env e, address spender, uint256 tokenId) { require nonpayable(e); + require authSanity(e); address caller = e.msg.sender; address owner = unsafeOwnerOf(tokenId); @@ -547,7 +638,6 @@ rule approve(env e, address spender, uint256 tokenId) { // liveness assert success <=> ( owner != 0 && - owner != spender && (owner == caller || isApprovedForAll(owner, caller)) ); @@ -576,7 +666,7 @@ rule setApprovalForAll(env e, address operator, bool approved) { bool success = !lastReverted; // liveness - assert success <=> owner != operator; + assert success <=> operator != 0; // effect assert success => isApprovedForAll(owner, operator) == approved; diff --git a/certora/specs/EnumerableMap.spec b/certora/specs/EnumerableMap.spec index dea5d85ecb0..7b503031f36 100644 --- a/certora/specs/EnumerableMap.spec +++ b/certora/specs/EnumerableMap.spec @@ -1,19 +1,19 @@ -import "helpers/helpers.spec" +import "helpers/helpers.spec"; methods { // library - set(bytes32,bytes32) returns (bool) envfree - remove(bytes32) returns (bool) envfree - contains(bytes32) returns (bool) envfree - length() returns (uint256) envfree - key_at(uint256) returns (bytes32) envfree - value_at(uint256) returns (bytes32) envfree - tryGet_contains(bytes32) returns (bool) envfree - tryGet_value(bytes32) returns (bytes32) envfree - get(bytes32) returns (bytes32) envfree + function set(bytes32,bytes32) external returns (bool) envfree; + function remove(bytes32) external returns (bool) envfree; + function contains(bytes32) external returns (bool) envfree; + function length() external returns (uint256) envfree; + function key_at(uint256) external returns (bytes32) envfree; + function value_at(uint256) external returns (bytes32) envfree; + function tryGet_contains(bytes32) external returns (bool) envfree; + function tryGet_value(bytes32) external returns (bytes32) envfree; + function get(bytes32) external returns (bytes32) envfree; // FV - _indexOf(bytes32) returns (uint256) envfree + function _indexOf(bytes32) external returns (uint256) envfree; } /* @@ -21,9 +21,8 @@ methods { │ Helpers │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -function sanity() returns bool { - return length() < max_uint256; -} +definition sanity() returns bool = + length() < max_uint256; /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ @@ -31,7 +30,7 @@ function sanity() returns bool { └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ invariant noValueIfNotContained(bytes32 key) - !contains(key) => tryGet_value(key) == 0 + !contains(key) => tryGet_value(key) == to_bytes32(0) { preserved set(bytes32 otherKey, bytes32 someValue) { require sanity(); @@ -48,7 +47,7 @@ invariant indexedContained(uint256 index) { preserved { requireInvariant consistencyIndex(index); - requireInvariant consistencyIndex(to_uint256(length() - 1)); + requireInvariant consistencyIndex(require_uint256(length() - 1)); } } @@ -61,8 +60,8 @@ invariant atUniqueness(uint256 index1, uint256 index2) index1 == index2 <=> key_at(index1) == key_at(index2) { preserved remove(bytes32 key) { - requireInvariant atUniqueness(index1, to_uint256(length() - 1)); - requireInvariant atUniqueness(index2, to_uint256(length() - 1)); + requireInvariant atUniqueness(index1, require_uint256(length() - 1)); + requireInvariant atUniqueness(index2, require_uint256(length() - 1)); } } @@ -76,10 +75,10 @@ invariant atUniqueness(uint256 index1, uint256 index2) └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ invariant consistencyIndex(uint256 index) - index < length() => _indexOf(key_at(index)) == index + 1 + index < length() => to_mathint(_indexOf(key_at(index))) == index + 1 { preserved remove(bytes32 key) { - requireInvariant consistencyIndex(to_uint256(length() - 1)); + requireInvariant consistencyIndex(require_uint256(length() - 1)); } } @@ -87,14 +86,14 @@ invariant consistencyKey(bytes32 key) contains(key) => ( _indexOf(key) > 0 && _indexOf(key) <= length() && - key_at(to_uint256(_indexOf(key) - 1)) == key + key_at(require_uint256(_indexOf(key) - 1)) == key ) { preserved remove(bytes32 otherKey) { requireInvariant consistencyKey(otherKey); requireInvariant atUniqueness( - to_uint256(_indexOf(key) - 1), - to_uint256(_indexOf(otherKey) - 1) + require_uint256(_indexOf(key) - 1), + require_uint256(_indexOf(otherKey) - 1) ); } } @@ -121,18 +120,18 @@ rule stateChange(env e, bytes32 key) { bytes32 valueAfter = tryGet_value(key); assert lengthBefore != lengthAfter => ( - (f.selector == set(bytes32,bytes32).selector && lengthAfter == lengthBefore + 1) || - (f.selector == remove(bytes32).selector && lengthAfter == lengthBefore - 1) + (f.selector == sig:set(bytes32,bytes32).selector && to_mathint(lengthAfter) == lengthBefore + 1) || + (f.selector == sig:remove(bytes32).selector && to_mathint(lengthAfter) == lengthBefore - 1) ); assert containsBefore != containsAfter => ( - (f.selector == set(bytes32,bytes32).selector && containsAfter) || - (f.selector == remove(bytes32).selector && !containsAfter) + (f.selector == sig:set(bytes32,bytes32).selector && containsAfter) || + (f.selector == sig:remove(bytes32).selector && !containsAfter) ); assert valueBefore != valueAfter => ( - (f.selector == set(bytes32,bytes32).selector && containsAfter) || - (f.selector == remove(bytes32).selector && !containsAfter && valueAfter == 0) + (f.selector == sig:set(bytes32,bytes32).selector && containsAfter) || + (f.selector == sig:remove(bytes32).selector && !containsAfter && valueAfter == to_bytes32(0)) ); } @@ -192,7 +191,7 @@ rule getAndTryGet(bytes32 key) { assert contained == tryContained; assert contained => tryValue == value; - assert !contained => tryValue == 0; + assert !contained => tryValue == to_bytes32(0); } /* @@ -217,7 +216,7 @@ rule set(bytes32 key, bytes32 value, bytes32 otherKey) { assert added <=> !containsBefore, "return value: added iff not contained"; - assert length() == lengthBefore + to_mathint(added ? 1 : 0), + assert to_mathint(length()) == lengthBefore + to_mathint(added ? 1 : 0), "effect: length increases iff added"; assert added => (key_at(lengthBefore) == key && value_at(lengthBefore) == value), @@ -253,7 +252,7 @@ rule remove(bytes32 key, bytes32 otherKey) { assert removed <=> containsBefore, "return value: removed iff contained"; - assert length() == lengthBefore - to_mathint(removed ? 1 : 0), + assert to_mathint(length()) == lengthBefore - to_mathint(removed ? 1 : 0), "effect: length decreases iff removed"; assert containsOtherBefore != contains(otherKey) => (removed && key == otherKey), @@ -295,7 +294,7 @@ rule setEnumerability(bytes32 key, bytes32 value, uint256 index) { └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule removeEnumerability(bytes32 key, uint256 index) { - uint256 last = length() - 1; + uint256 last = require_uint256(length() - 1); requireInvariant consistencyKey(key); requireInvariant consistencyIndex(index); diff --git a/certora/specs/EnumerableSet.spec b/certora/specs/EnumerableSet.spec index d63c556aa71..3db515838ff 100644 --- a/certora/specs/EnumerableSet.spec +++ b/certora/specs/EnumerableSet.spec @@ -1,15 +1,15 @@ -import "helpers/helpers.spec" +import "helpers/helpers.spec"; methods { // library - add(bytes32) returns (bool) envfree - remove(bytes32) returns (bool) envfree - contains(bytes32) returns (bool) envfree - length() returns (uint256) envfree - at_(uint256) returns (bytes32) envfree + function add(bytes32) external returns (bool) envfree; + function remove(bytes32) external returns (bool) envfree; + function contains(bytes32) external returns (bool) envfree; + function length() external returns (uint256) envfree; + function at_(uint256) external returns (bytes32) envfree; // FV - _indexOf(bytes32) returns (uint256) envfree + function _indexOf(bytes32) external returns (uint256) envfree; } /* @@ -17,9 +17,8 @@ methods { │ Helpers │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -function sanity() returns bool { - return length() < max_uint256; -} +definition sanity() returns bool = + length() < max_uint256; /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ @@ -31,7 +30,7 @@ invariant indexedContained(uint256 index) { preserved { requireInvariant consistencyIndex(index); - requireInvariant consistencyIndex(to_uint256(length() - 1)); + requireInvariant consistencyIndex(require_uint256(length() - 1)); } } @@ -44,8 +43,8 @@ invariant atUniqueness(uint256 index1, uint256 index2) index1 == index2 <=> at_(index1) == at_(index2) { preserved remove(bytes32 key) { - requireInvariant atUniqueness(index1, to_uint256(length() - 1)); - requireInvariant atUniqueness(index2, to_uint256(length() - 1)); + requireInvariant atUniqueness(index1, require_uint256(length() - 1)); + requireInvariant atUniqueness(index2, require_uint256(length() - 1)); } } @@ -59,10 +58,10 @@ invariant atUniqueness(uint256 index1, uint256 index2) └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ invariant consistencyIndex(uint256 index) - index < length() => _indexOf(at_(index)) == index + 1 + index < length() => _indexOf(at_(index)) == require_uint256(index + 1) { preserved remove(bytes32 key) { - requireInvariant consistencyIndex(to_uint256(length() - 1)); + requireInvariant consistencyIndex(require_uint256(length() - 1)); } } @@ -70,14 +69,14 @@ invariant consistencyKey(bytes32 key) contains(key) => ( _indexOf(key) > 0 && _indexOf(key) <= length() && - at_(to_uint256(_indexOf(key) - 1)) == key + at_(require_uint256(_indexOf(key) - 1)) == key ) { preserved remove(bytes32 otherKey) { requireInvariant consistencyKey(otherKey); requireInvariant atUniqueness( - to_uint256(_indexOf(key) - 1), - to_uint256(_indexOf(otherKey) - 1) + require_uint256(_indexOf(key) - 1), + require_uint256(_indexOf(otherKey) - 1) ); } } @@ -102,13 +101,13 @@ rule stateChange(env e, bytes32 key) { bool containsAfter = contains(key); assert lengthBefore != lengthAfter => ( - (f.selector == add(bytes32).selector && lengthAfter == lengthBefore + 1) || - (f.selector == remove(bytes32).selector && lengthAfter == lengthBefore - 1) + (f.selector == sig:add(bytes32).selector && lengthAfter == require_uint256(lengthBefore + 1)) || + (f.selector == sig:remove(bytes32).selector && lengthAfter == require_uint256(lengthBefore - 1)) ); assert containsBefore != containsAfter => ( - (f.selector == add(bytes32).selector && containsAfter) || - (f.selector == remove(bytes32).selector && containsBefore) + (f.selector == sig:add(bytes32).selector && containsAfter) || + (f.selector == sig:remove(bytes32).selector && containsBefore) ); } @@ -158,7 +157,7 @@ rule add(bytes32 key, bytes32 otherKey) { assert added <=> !containsBefore, "return value: added iff not contained"; - assert length() == lengthBefore + to_mathint(added ? 1 : 0), + assert length() == require_uint256(lengthBefore + to_mathint(added ? 1 : 0)), "effect: length increases iff added"; assert added => at_(lengthBefore) == key, @@ -190,7 +189,7 @@ rule remove(bytes32 key, bytes32 otherKey) { assert removed <=> containsBefore, "return value: removed iff contained"; - assert length() == lengthBefore - to_mathint(removed ? 1 : 0), + assert length() == require_uint256(lengthBefore - to_mathint(removed ? 1 : 0)), "effect: length decreases iff removed"; assert containsOtherBefore != contains(otherKey) => (removed && key == otherKey), @@ -220,7 +219,7 @@ rule addEnumerability(bytes32 key, uint256 index) { └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule removeEnumerability(bytes32 key, uint256 index) { - uint256 last = length() - 1; + uint256 last = require_uint256(length() - 1); requireInvariant consistencyKey(key); requireInvariant consistencyIndex(index); diff --git a/certora/specs/Initializable.spec b/certora/specs/Initializable.spec index 0e0b1b71419..07c2930c208 100644 --- a/certora/specs/Initializable.spec +++ b/certora/specs/Initializable.spec @@ -1,19 +1,19 @@ -import "helpers/helpers.spec" +import "helpers/helpers.spec"; methods { // initialize, reinitialize, disable - initialize() envfree - reinitialize(uint8) envfree - disable() envfree + function initialize() external envfree; + function reinitialize(uint64) external envfree; + function disable() external envfree; - nested_init_init() envfree - nested_init_reinit(uint8) envfree - nested_reinit_init(uint8) envfree - nested_reinit_reinit(uint8,uint8) envfree + function nested_init_init() external envfree; + function nested_init_reinit(uint64) external envfree; + function nested_reinit_init(uint64) external envfree; + function nested_reinit_reinit(uint64,uint64) external envfree; // view - version() returns uint8 envfree - initializing() returns bool envfree + function version() external returns uint64 envfree; + function initializing() external returns bool envfree; } /* @@ -23,7 +23,7 @@ methods { */ definition isUninitialized() returns bool = version() == 0; definition isInitialized() returns bool = version() > 0; -definition isDisabled() returns bool = version() == 255; +definition isDisabled() returns bool = version() == max_uint64; /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ @@ -31,7 +31,7 @@ definition isDisabled() returns bool = version() == 255; └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ invariant notInitializing() - !initializing() + !initializing(); /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ @@ -39,7 +39,7 @@ invariant notInitializing() └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule increasingVersion(env e) { - uint8 versionBefore = version(); + uint64 versionBefore = version(); bool disabledBefore = isDisabled(); method f; calldataarg args; @@ -83,7 +83,7 @@ rule cannotInitializeOnceDisabled() { rule cannotReinitializeOnceDisabled() { require isDisabled(); - uint8 n; + uint64 n; reinitialize@withrevert(n); assert lastReverted, "contract is disabled"; @@ -99,17 +99,17 @@ rule cannotNestInitializers_init_init() { assert lastReverted, "nested initializers"; } -rule cannotNestInitializers_init_reinit(uint8 m) { +rule cannotNestInitializers_init_reinit(uint64 m) { nested_init_reinit@withrevert(m); assert lastReverted, "nested initializers"; } -rule cannotNestInitializers_reinit_init(uint8 n) { +rule cannotNestInitializers_reinit_init(uint64 n) { nested_reinit_init@withrevert(n); assert lastReverted, "nested initializers"; } -rule cannotNestInitializers_reinit_reinit(uint8 n, uint8 m) { +rule cannotNestInitializers_reinit_reinit(uint64 n, uint64 m) { nested_reinit_reinit@withrevert(n, m); assert lastReverted, "nested initializers"; } @@ -139,9 +139,9 @@ rule initializeEffects() { rule reinitializeEffects() { requireInvariant notInitializing(); - uint8 versionBefore = version(); + uint64 versionBefore = version(); - uint8 n; + uint64 n; reinitialize@withrevert(n); bool success = !lastReverted; diff --git a/certora/specs/Ownable.spec b/certora/specs/Ownable.spec index 4bf9e300553..0d50813cf92 100644 --- a/certora/specs/Ownable.spec +++ b/certora/specs/Ownable.spec @@ -1,78 +1,77 @@ -import "helpers/helpers.spec" -import "methods/IOwnable.spec" - -methods { - restricted() -} - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Function correctness: transferOwnership changes ownership │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -rule transferOwnership(env e) { - require nonpayable(e); - - address newOwner; - address current = owner(); - - transferOwnership@withrevert(e, newOwner); - bool success = !lastReverted; - - assert success <=> (e.msg.sender == current && newOwner != 0), "unauthorized caller or invalid arg"; - assert success => owner() == newOwner, "current owner changed"; -} - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Function correctness: renounceOwnership removes the owner │ - -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -rule renounceOwnership(env e) { - require nonpayable(e); - - address current = owner(); - - renounceOwnership@withrevert(e); - bool success = !lastReverted; - - assert success <=> e.msg.sender == current, "unauthorized caller"; - assert success => owner() == 0, "owner not cleared"; -} - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Access control: only current owner can call restricted functions │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -rule onlyCurrentOwnerCanCallOnlyOwner(env e) { - require nonpayable(e); - - address current = owner(); - - calldataarg args; - restricted@withrevert(e, args); - - assert !lastReverted <=> e.msg.sender == current, "access control failed"; -} - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Rule: ownership can only change in specific ways │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -rule onlyOwnerOrPendingOwnerCanChangeOwnership(env e) { - address oldCurrent = owner(); - - method f; calldataarg args; - f(e, args); - - address newCurrent = owner(); - - // If owner changes, must be either transferOwnership or renounceOwnership - assert oldCurrent != newCurrent => ( - (e.msg.sender == oldCurrent && newCurrent != 0 && f.selector == transferOwnership(address).selector) || - (e.msg.sender == oldCurrent && newCurrent == 0 && f.selector == renounceOwnership().selector) - ); -} +import "helpers/helpers.spec"; +import "methods/IOwnable.spec"; + +methods { + function restricted() external; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function correctness: transferOwnership changes ownership │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule transferOwnership(env e) { + require nonpayable(e); + + address newOwner; + address current = owner(); + + transferOwnership@withrevert(e, newOwner); + bool success = !lastReverted; + + assert success <=> (e.msg.sender == current && newOwner != 0), "unauthorized caller or invalid arg"; + assert success => owner() == newOwner, "current owner changed"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function correctness: renounceOwnership removes the owner │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule renounceOwnership(env e) { + require nonpayable(e); + + address current = owner(); + + renounceOwnership@withrevert(e); + bool success = !lastReverted; + + assert success <=> e.msg.sender == current, "unauthorized caller"; + assert success => owner() == 0, "owner not cleared"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Access control: only current owner can call restricted functions │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule onlyCurrentOwnerCanCallOnlyOwner(env e) { + require nonpayable(e); + + address current = owner(); + + calldataarg args; + restricted@withrevert(e, args); + + assert !lastReverted <=> e.msg.sender == current, "access control failed"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: ownership can only change in specific ways │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule onlyOwnerOrPendingOwnerCanChangeOwnership(env e) { + address oldCurrent = owner(); + + method f; calldataarg args; + f(e, args); + + address newCurrent = owner(); + + // If owner changes, must be either transferOwnership or renounceOwnership + assert oldCurrent != newCurrent => ( + (e.msg.sender == oldCurrent && newCurrent != 0 && f.selector == sig:transferOwnership(address).selector) || + (e.msg.sender == oldCurrent && newCurrent == 0 && f.selector == sig:renounceOwnership().selector) + ); +} diff --git a/certora/specs/Ownable2Step.spec b/certora/specs/Ownable2Step.spec index 47b1b8d75eb..d13c6d3e639 100644 --- a/certora/specs/Ownable2Step.spec +++ b/certora/specs/Ownable2Step.spec @@ -1,108 +1,108 @@ -import "helpers/helpers.spec" -import "methods/IOwnable2Step.spec" - -methods { - restricted() -} - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Function correctness: transferOwnership sets the pending owner │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -rule transferOwnership(env e) { - require nonpayable(e); - - address newOwner; - address current = owner(); - - transferOwnership@withrevert(e, newOwner); - bool success = !lastReverted; - - assert success <=> e.msg.sender == current, "unauthorized caller"; - assert success => pendingOwner() == newOwner, "pending owner not set"; - assert success => owner() == current, "current owner changed"; -} - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Function correctness: renounceOwnership removes the owner and the pendingOwner │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -rule renounceOwnership(env e) { - require nonpayable(e); - - address current = owner(); - - renounceOwnership@withrevert(e); - bool success = !lastReverted; - - assert success <=> e.msg.sender == current, "unauthorized caller"; - assert success => pendingOwner() == 0, "pending owner not cleared"; - assert success => owner() == 0, "owner not cleared"; -} - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Function correctness: acceptOwnership changes owner and reset pending owner │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -rule acceptOwnership(env e) { - - require nonpayable(e); - - address current = owner(); - address pending = pendingOwner(); - - acceptOwnership@withrevert(e); - bool success = !lastReverted; - - assert success <=> e.msg.sender == pending, "unauthorized caller"; - assert success => pendingOwner() == 0, "pending owner not cleared"; - assert success => owner() == pending, "owner not transferred"; -} - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Access control: only current owner can call restricted functions │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -rule onlyCurrentOwnerCanCallOnlyOwner(env e) { - require nonpayable(e); - - address current = owner(); - - calldataarg args; - restricted@withrevert(e, args); - - assert !lastReverted <=> e.msg.sender == current, "access control failed"; -} - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Rule: ownership and pending ownership can only change in specific ways │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -rule ownerOrPendingOwnerChange(env e, method f) { - address oldCurrent = owner(); - address oldPending = pendingOwner(); - - calldataarg args; - f(e, args); - - address newCurrent = owner(); - address newPending = pendingOwner(); - - // If owner changes, must be either acceptOwnership or renounceOwnership - assert oldCurrent != newCurrent => ( - (e.msg.sender == oldPending && newCurrent == oldPending && newPending == 0 && f.selector == acceptOwnership().selector) || - (e.msg.sender == oldCurrent && newCurrent == 0 && newPending == 0 && f.selector == renounceOwnership().selector) - ); - - // If pending changes, must be either acceptance or reset - assert oldPending != newPending => ( - (e.msg.sender == oldCurrent && newCurrent == oldCurrent && f.selector == transferOwnership(address).selector) || - (e.msg.sender == oldPending && newCurrent == oldPending && newPending == 0 && f.selector == acceptOwnership().selector) || - (e.msg.sender == oldCurrent && newCurrent == 0 && newPending == 0 && f.selector == renounceOwnership().selector) - ); -} +import "helpers/helpers.spec"; +import "methods/IOwnable2Step.spec"; + +methods { + function restricted() external; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function correctness: transferOwnership sets the pending owner │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule transferOwnership(env e) { + require nonpayable(e); + + address newOwner; + address current = owner(); + + transferOwnership@withrevert(e, newOwner); + bool success = !lastReverted; + + assert success <=> e.msg.sender == current, "unauthorized caller"; + assert success => pendingOwner() == newOwner, "pending owner not set"; + assert success => owner() == current, "current owner changed"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function correctness: renounceOwnership removes the owner and the pendingOwner │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule renounceOwnership(env e) { + require nonpayable(e); + + address current = owner(); + + renounceOwnership@withrevert(e); + bool success = !lastReverted; + + assert success <=> e.msg.sender == current, "unauthorized caller"; + assert success => pendingOwner() == 0, "pending owner not cleared"; + assert success => owner() == 0, "owner not cleared"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function correctness: acceptOwnership changes owner and reset pending owner │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule acceptOwnership(env e) { + + require nonpayable(e); + + address current = owner(); + address pending = pendingOwner(); + + acceptOwnership@withrevert(e); + bool success = !lastReverted; + + assert success <=> e.msg.sender == pending, "unauthorized caller"; + assert success => pendingOwner() == 0, "pending owner not cleared"; + assert success => owner() == pending, "owner not transferred"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Access control: only current owner can call restricted functions │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule onlyCurrentOwnerCanCallOnlyOwner(env e) { + require nonpayable(e); + + address current = owner(); + + calldataarg args; + restricted@withrevert(e, args); + + assert !lastReverted <=> e.msg.sender == current, "access control failed"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: ownership and pending ownership can only change in specific ways │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule ownerOrPendingOwnerChange(env e, method f) { + address oldCurrent = owner(); + address oldPending = pendingOwner(); + + calldataarg args; + f(e, args); + + address newCurrent = owner(); + address newPending = pendingOwner(); + + // If owner changes, must be either acceptOwnership or renounceOwnership + assert oldCurrent != newCurrent => ( + (e.msg.sender == oldPending && newCurrent == oldPending && newPending == 0 && f.selector == sig:acceptOwnership().selector) || + (e.msg.sender == oldCurrent && newCurrent == 0 && newPending == 0 && f.selector == sig:renounceOwnership().selector) + ); + + // If pending changes, must be either acceptance or reset + assert oldPending != newPending => ( + (e.msg.sender == oldCurrent && newCurrent == oldCurrent && f.selector == sig:transferOwnership(address).selector) || + (e.msg.sender == oldPending && newCurrent == oldPending && newPending == 0 && f.selector == sig:acceptOwnership().selector) || + (e.msg.sender == oldCurrent && newCurrent == 0 && newPending == 0 && f.selector == sig:renounceOwnership().selector) + ); +} diff --git a/certora/specs/Pausable.spec b/certora/specs/Pausable.spec index aea38003f39..a7aff9cc142 100644 --- a/certora/specs/Pausable.spec +++ b/certora/specs/Pausable.spec @@ -1,96 +1,96 @@ -import "helpers/helpers.spec" - -methods { - paused() returns (bool) envfree - pause() - unpause() - onlyWhenPaused() - onlyWhenNotPaused() -} - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Function correctness: _pause pauses the contract │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -rule pause(env e) { - require nonpayable(e); - - bool pausedBefore = paused(); - - pause@withrevert(e); - bool success = !lastReverted; - - bool pausedAfter = paused(); - - // liveness - assert success <=> !pausedBefore, "works if and only if the contract was not paused before"; - - // effect - assert success => pausedAfter, "contract must be paused after a successful call"; -} - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Function correctness: _unpause unpauses the contract │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -rule unpause(env e) { - require nonpayable(e); - - bool pausedBefore = paused(); - - unpause@withrevert(e); - bool success = !lastReverted; - - bool pausedAfter = paused(); - - // liveness - assert success <=> pausedBefore, "works if and only if the contract was paused before"; - - // effect - assert success => !pausedAfter, "contract must be unpaused after a successful call"; -} - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Function correctness: whenPaused modifier can only be called if the contract is paused │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -rule whenPaused(env e) { - require nonpayable(e); - - onlyWhenPaused@withrevert(e); - assert !lastReverted <=> paused(), "works if and only if the contract is paused"; -} - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Function correctness: whenNotPaused modifier can only be called if the contract is not paused │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -rule whenNotPaused(env e) { - require nonpayable(e); - - onlyWhenNotPaused@withrevert(e); - assert !lastReverted <=> !paused(), "works if and only if the contract is not paused"; -} - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Rules: only _pause and _unpause can change paused status │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -rule noPauseChange(env e) { - method f; - calldataarg args; - - bool pausedBefore = paused(); - f(e, args); - bool pausedAfter = paused(); - - assert pausedBefore != pausedAfter => ( - (!pausedAfter && f.selector == unpause().selector) || - (pausedAfter && f.selector == pause().selector) - ), "contract's paused status can only be changed by _pause() or _unpause()"; -} +import "helpers/helpers.spec"; + +methods { + function paused() external returns (bool) envfree; + function pause() external; + function unpause() external; + function onlyWhenPaused() external; + function onlyWhenNotPaused() external; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function correctness: _pause pauses the contract │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule pause(env e) { + require nonpayable(e); + + bool pausedBefore = paused(); + + pause@withrevert(e); + bool success = !lastReverted; + + bool pausedAfter = paused(); + + // liveness + assert success <=> !pausedBefore, "works if and only if the contract was not paused before"; + + // effect + assert success => pausedAfter, "contract must be paused after a successful call"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function correctness: _unpause unpauses the contract │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule unpause(env e) { + require nonpayable(e); + + bool pausedBefore = paused(); + + unpause@withrevert(e); + bool success = !lastReverted; + + bool pausedAfter = paused(); + + // liveness + assert success <=> pausedBefore, "works if and only if the contract was paused before"; + + // effect + assert success => !pausedAfter, "contract must be unpaused after a successful call"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function correctness: whenPaused modifier can only be called if the contract is paused │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule whenPaused(env e) { + require nonpayable(e); + + onlyWhenPaused@withrevert(e); + assert !lastReverted <=> paused(), "works if and only if the contract is paused"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function correctness: whenNotPaused modifier can only be called if the contract is not paused │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule whenNotPaused(env e) { + require nonpayable(e); + + onlyWhenNotPaused@withrevert(e); + assert !lastReverted <=> !paused(), "works if and only if the contract is not paused"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rules: only _pause and _unpause can change paused status │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule noPauseChange(env e) { + method f; + calldataarg args; + + bool pausedBefore = paused(); + f(e, args); + bool pausedAfter = paused(); + + assert pausedBefore != pausedAfter => ( + (!pausedAfter && f.selector == sig:unpause().selector) || + (pausedAfter && f.selector == sig:pause().selector) + ), "contract's paused status can only be changed by _pause() or _unpause()"; +} diff --git a/certora/specs/TimelockController.spec b/certora/specs/TimelockController.spec index 05ecb1340f0..5123768da12 100644 --- a/certora/specs/TimelockController.spec +++ b/certora/specs/TimelockController.spec @@ -1,28 +1,27 @@ -import "helpers/helpers.spec" -import "methods/IAccessControl.spec" +import "helpers/helpers.spec"; +import "methods/IAccessControl.spec"; methods { - TIMELOCK_ADMIN_ROLE() returns (bytes32) envfree - PROPOSER_ROLE() returns (bytes32) envfree - EXECUTOR_ROLE() returns (bytes32) envfree - CANCELLER_ROLE() returns (bytes32) envfree - isOperation(bytes32) returns (bool) envfree - isOperationPending(bytes32) returns (bool) envfree - isOperationReady(bytes32) returns (bool) - isOperationDone(bytes32) returns (bool) envfree - getTimestamp(bytes32) returns (uint256) envfree - getMinDelay() returns (uint256) envfree - - hashOperation(address, uint256, bytes, bytes32, bytes32) returns(bytes32) envfree - hashOperationBatch(address[], uint256[], bytes[], bytes32, bytes32) returns(bytes32) envfree - - schedule(address, uint256, bytes, bytes32, bytes32, uint256) - scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256) - execute(address, uint256, bytes, bytes32, bytes32) - executeBatch(address[], uint256[], bytes[], bytes32, bytes32) - cancel(bytes32) - - updateDelay(uint256) + function PROPOSER_ROLE() external returns (bytes32) envfree; + function EXECUTOR_ROLE() external returns (bytes32) envfree; + function CANCELLER_ROLE() external returns (bytes32) envfree; + function isOperation(bytes32) external returns (bool); + function isOperationPending(bytes32) external returns (bool); + function isOperationReady(bytes32) external returns (bool); + function isOperationDone(bytes32) external returns (bool); + function getTimestamp(bytes32) external returns (uint256) envfree; + function getMinDelay() external returns (uint256) envfree; + + function hashOperation(address, uint256, bytes, bytes32, bytes32) external returns(bytes32) envfree; + function hashOperationBatch(address[], uint256[], bytes[], bytes32, bytes32) external returns(bytes32) envfree; + + function schedule(address, uint256, bytes, bytes32, bytes32, uint256) external; + function scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256) external; + function execute(address, uint256, bytes, bytes32, bytes32) external; + function executeBatch(address[], uint256[], bytes[], bytes32, bytes32) external; + function cancel(bytes32) external; + + function updateDelay(uint256) external; } /* @@ -32,11 +31,11 @@ methods { */ // Uniformly handle scheduling of batched and non-batched operations. function helperScheduleWithRevert(env e, method f, bytes32 id, uint256 delay) { - if (f.selector == schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector) { + if (f.selector == sig:schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector) { address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt; require hashOperation(target, value, data, predecessor, salt) == id; // Correlation schedule@withrevert(e, target, value, data, predecessor, salt, delay); - } else if (f.selector == scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector) { + } else if (f.selector == sig:scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector) { address[] targets; uint256[] values; bytes[] payloads; bytes32 predecessor; bytes32 salt; require hashOperationBatch(targets, values, payloads, predecessor, salt) == id; // Correlation scheduleBatch@withrevert(e, targets, values, payloads, predecessor, salt, delay); @@ -48,11 +47,11 @@ function helperScheduleWithRevert(env e, method f, bytes32 id, uint256 delay) { // Uniformly handle execution of batched and non-batched operations. function helperExecuteWithRevert(env e, method f, bytes32 id, bytes32 predecessor) { - if (f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector) { + if (f.selector == sig:execute(address, uint256, bytes, bytes32, bytes32).selector) { address target; uint256 value; bytes data; bytes32 salt; require hashOperation(target, value, data, predecessor, salt) == id; // Correlation execute@withrevert(e, target, value, data, predecessor, salt); - } else if (f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector) { + } else if (f.selector == sig:executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector) { address[] targets; uint256[] values; bytes[] payloads; bytes32 salt; require hashOperationBatch(targets, values, payloads, predecessor, salt) == id; // Correlation executeBatch@withrevert(e, targets, values, payloads, predecessor, salt); @@ -72,30 +71,30 @@ definition UNSET() returns uint8 = 0x1; definition PENDING() returns uint8 = 0x2; definition DONE() returns uint8 = 0x4; -definition isUnset(bytes32 id) returns bool = !isOperation(id); -definition isPending(bytes32 id) returns bool = isOperationPending(id); -definition isDone(bytes32 id) returns bool = isOperationDone(id); -definition state(bytes32 id) returns uint8 = (isUnset(id) ? UNSET() : 0) | (isPending(id) ? PENDING() : 0) | (isDone(id) ? DONE() : 0); +definition isUnset(env e, bytes32 id) returns bool = !isOperation(e, id); +definition isPending(env e, bytes32 id) returns bool = isOperationPending(e, id); +definition isDone(env e, bytes32 id) returns bool = isOperationDone(e, id); +definition state(env e, bytes32 id) returns uint8 = (isUnset(e, id) ? UNSET() : 0) | (isPending(e, id) ? PENDING() : 0) | (isDone(e, id) ? DONE() : 0); /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Invariants: consistency of accessors │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -invariant isOperationCheck(bytes32 id) - isOperation(id) <=> getTimestamp(id) > 0 +invariant isOperationCheck(env e, bytes32 id) + isOperation(e, id) <=> getTimestamp(id) > 0 filtered { f -> !f.isView } -invariant isOperationPendingCheck(bytes32 id) - isOperationPending(id) <=> getTimestamp(id) > DONE_TIMESTAMP() +invariant isOperationPendingCheck(env e, bytes32 id) + isOperationPending(e, id) <=> getTimestamp(id) > DONE_TIMESTAMP() filtered { f -> !f.isView } -invariant isOperationDoneCheck(bytes32 id) - isOperationDone(id) <=> getTimestamp(id) == DONE_TIMESTAMP() +invariant isOperationDoneCheck(env e, bytes32 id) + isOperationDone(e, id) <=> getTimestamp(id) == DONE_TIMESTAMP() filtered { f -> !f.isView } invariant isOperationReadyCheck(env e, bytes32 id) - isOperationReady(e, id) <=> (isOperationPending(id) && getTimestamp(id) <= e.block.timestamp) + isOperationReady(e, id) <=> (isOperationPending(e, id) && getTimestamp(id) <= e.block.timestamp) filtered { f -> !f.isView } /* @@ -105,15 +104,15 @@ invariant isOperationReadyCheck(env e, bytes32 id) */ invariant stateConsistency(bytes32 id, env e) // Check states are mutually exclusive - (isUnset(id) <=> (!isPending(id) && !isDone(id) )) && - (isPending(id) <=> (!isUnset(id) && !isDone(id) )) && - (isDone(id) <=> (!isUnset(id) && !isPending(id))) && + (isUnset(e, id) <=> (!isPending(e, id) && !isDone(e, id) )) && + (isPending(e, id) <=> (!isUnset(e, id) && !isDone(e, id) )) && + (isDone(e, id) <=> (!isUnset(e, id) && !isPending(e, id))) && // Check that the state helper behaves as expected: - (isUnset(id) <=> state(id) == UNSET() ) && - (isPending(id) <=> state(id) == PENDING() ) && - (isDone(id) <=> state(id) == DONE() ) && + (isUnset(e, id) <=> state(e, id) == UNSET() ) && + (isPending(e, id) <=> state(e, id) == PENDING() ) && + (isDone(e, id) <=> state(e, id) == DONE() ) && // Check substate - isOperationReady(e, id) => isPending(id) + isOperationReady(e, id) => isPending(e, id) filtered { f -> !f.isView } /* @@ -124,28 +123,28 @@ invariant stateConsistency(bytes32 id, env e) rule stateTransition(bytes32 id, env e, method f, calldataarg args) { require e.block.timestamp > 1; // Sanity - uint8 stateBefore = state(id); + uint8 stateBefore = state(e, id); f(e, args); - uint8 stateAfter = state(id); + uint8 stateAfter = state(e, id); // Cannot jump from UNSET to DONE assert stateBefore == UNSET() => stateAfter != DONE(); // UNSET → PENDING: schedule or scheduleBatch assert stateBefore == UNSET() && stateAfter == PENDING() => ( - f.selector == schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector || - f.selector == scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector + f.selector == sig:schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector || + f.selector == sig:scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector ); // PENDING → UNSET: cancel assert stateBefore == PENDING() && stateAfter == UNSET() => ( - f.selector == cancel(bytes32).selector + f.selector == sig:cancel(bytes32).selector ); // PENDING → DONE: execute or executeBatch assert stateBefore == PENDING() && stateAfter == DONE() => ( - f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector || - f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector + f.selector == sig:execute(address, uint256, bytes, bytes32, bytes32).selector || + f.selector == sig:executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector ); // DONE is final @@ -163,7 +162,7 @@ rule minDelayOnlyChange(env e) { method f; calldataarg args; f(e, args); - assert delayBefore != getMinDelay() => (e.msg.sender == currentContract && f.selector == updateDelay(uint256).selector), "Unauthorized delay update"; + assert delayBefore != getMinDelay() => (e.msg.sender == currentContract && f.selector == sig:updateDelay(uint256).selector), "Unauthorized delay update"; } /* @@ -172,8 +171,8 @@ rule minDelayOnlyChange(env e) { └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule schedule(env e, method f, bytes32 id, uint256 delay) filtered { f -> - f.selector == schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector || - f.selector == scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector + f.selector == sig:schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector || + f.selector == sig:scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector } { require nonpayable(e); @@ -184,7 +183,7 @@ rule schedule(env e, method f, bytes32 id, uint256 delay) filtered { f -> bytes32 otherId; uint256 otherTimestamp = getTimestamp(otherId); - uint8 stateBefore = state(id); + uint8 stateBefore = state(e, id); bool isDelaySufficient = delay >= getMinDelay(); bool isProposerBefore = hasRole(PROPOSER_ROLE(), e.msg.sender); @@ -199,8 +198,8 @@ rule schedule(env e, method f, bytes32 id, uint256 delay) filtered { f -> ); // effect - assert success => state(id) == PENDING(), "State transition violation"; - assert success => getTimestamp(id) == to_uint256(e.block.timestamp + delay), "Proposal timestamp not correctly set"; + assert success => state(e, id) == PENDING(), "State transition violation"; + assert success => getTimestamp(id) == require_uint256(e.block.timestamp + delay), "Proposal timestamp not correctly set"; // no side effect assert otherTimestamp != getTimestamp(otherId) => id == otherId, "Other proposal affected"; @@ -212,15 +211,15 @@ rule schedule(env e, method f, bytes32 id, uint256 delay) filtered { f -> └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule execute(env e, method f, bytes32 id, bytes32 predecessor) filtered { f -> - f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector || - f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector + f.selector == sig:execute(address, uint256, bytes, bytes32, bytes32).selector || + f.selector == sig:executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector } { bytes32 otherId; uint256 otherTimestamp = getTimestamp(otherId); - uint8 stateBefore = state(id); + uint8 stateBefore = state(e, id); bool isOperationReadyBefore = isOperationReady(e, id); bool isExecutorOrOpen = hasRole(EXECUTOR_ROLE(), e.msg.sender) || hasRole(EXECUTOR_ROLE(), 0); - bool predecessorDependency = predecessor == 0 || isDone(predecessor); + bool predecessorDependency = predecessor == to_bytes32(0) || isDone(e, predecessor); helperExecuteWithRevert(e, f, id, predecessor); bool success = !lastReverted; @@ -239,7 +238,7 @@ rule execute(env e, method f, bytes32 id, bytes32 predecessor) filtered { f -> ); // effect - assert success => state(id) == DONE(), "State transition violation"; + assert success => state(e, id) == DONE(), "State transition violation"; // no side effect assert otherTimestamp != getTimestamp(otherId) => id == otherId, "Other proposal affected"; @@ -255,7 +254,7 @@ rule cancel(env e, bytes32 id) { bytes32 otherId; uint256 otherTimestamp = getTimestamp(otherId); - uint8 stateBefore = state(id); + uint8 stateBefore = state(e, id); bool isCanceller = hasRole(CANCELLER_ROLE(), e.msg.sender); cancel@withrevert(e, id); @@ -268,7 +267,7 @@ rule cancel(env e, bytes32 id) { ); // effect - assert success => state(id) == UNSET(), "State transition violation"; + assert success => state(e, id) == UNSET(), "State transition violation"; // no side effect assert otherTimestamp != getTimestamp(otherId) => id == otherId, "Other proposal affected"; diff --git a/certora/specs/methods/IAccessControl.spec b/certora/specs/methods/IAccessControl.spec index 4d41ffda72e..5c395b088e3 100644 --- a/certora/specs/methods/IAccessControl.spec +++ b/certora/specs/methods/IAccessControl.spec @@ -1,7 +1,8 @@ methods { - hasRole(bytes32, address) returns(bool) envfree - getRoleAdmin(bytes32) returns(bytes32) envfree - grantRole(bytes32, address) - revokeRole(bytes32, address) - renounceRole(bytes32, address) + function DEFAULT_ADMIN_ROLE() external returns (bytes32) envfree; + function hasRole(bytes32, address) external returns(bool) envfree; + function getRoleAdmin(bytes32) external returns(bytes32) envfree; + function grantRole(bytes32, address) external; + function revokeRole(bytes32, address) external; + function renounceRole(bytes32, address) external; } diff --git a/certora/specs/methods/IAccessControlDefaultAdminRules.spec b/certora/specs/methods/IAccessControlDefaultAdminRules.spec index a9dd08b7f0b..d02db180d8c 100644 --- a/certora/specs/methods/IAccessControlDefaultAdminRules.spec +++ b/certora/specs/methods/IAccessControlDefaultAdminRules.spec @@ -1,36 +1,36 @@ -import "./IERC5313.spec" +import "./IERC5313.spec"; methods { // === View == // Default Admin - defaultAdmin() returns(address) envfree - pendingDefaultAdmin() returns(address, uint48) envfree + function defaultAdmin() external returns(address) envfree; + function pendingDefaultAdmin() external returns(address, uint48) envfree; // Default Admin Delay - defaultAdminDelay() returns(uint48) - pendingDefaultAdminDelay() returns(uint48, uint48) - defaultAdminDelayIncreaseWait() returns(uint48) envfree + function defaultAdminDelay() external returns(uint48); + function pendingDefaultAdminDelay() external returns(uint48, uint48); + function defaultAdminDelayIncreaseWait() external returns(uint48) envfree; // === Mutations == // Default Admin - beginDefaultAdminTransfer(address) - cancelDefaultAdminTransfer() - acceptDefaultAdminTransfer() + function beginDefaultAdminTransfer(address) external; + function cancelDefaultAdminTransfer() external; + function acceptDefaultAdminTransfer() external; // Default Admin Delay - changeDefaultAdminDelay(uint48) - rollbackDefaultAdminDelay() + function changeDefaultAdminDelay(uint48) external; + function rollbackDefaultAdminDelay() external; // == FV == // Default Admin - pendingDefaultAdmin_() returns (address) envfree - pendingDefaultAdminSchedule_() returns (uint48) envfree + function pendingDefaultAdmin_() external returns (address) envfree; + function pendingDefaultAdminSchedule_() external returns (uint48) envfree; // Default Admin Delay - pendingDelay_() returns (uint48) - pendingDelaySchedule_() returns (uint48) - delayChangeWait_(uint48) returns (uint48) + function pendingDelay_() external returns (uint48); + function pendingDelaySchedule_() external returns (uint48); + function delayChangeWait_(uint48) external returns (uint48); } diff --git a/certora/specs/methods/IERC20.spec b/certora/specs/methods/IERC20.spec index cfa454e13a6..100901a0425 100644 --- a/certora/specs/methods/IERC20.spec +++ b/certora/specs/methods/IERC20.spec @@ -1,11 +1,11 @@ methods { - name() returns (string) envfree => DISPATCHER(true) - symbol() returns (string) envfree => DISPATCHER(true) - decimals() returns (uint8) envfree => DISPATCHER(true) - totalSupply() returns (uint256) envfree => DISPATCHER(true) - balanceOf(address) returns (uint256) envfree => DISPATCHER(true) - allowance(address,address) returns (uint256) envfree => DISPATCHER(true) - approve(address,uint256) returns (bool) => DISPATCHER(true) - transfer(address,uint256) returns (bool) => DISPATCHER(true) - transferFrom(address,address,uint256) returns (bool) => DISPATCHER(true) + function name() external returns (string) envfree; + function symbol() external returns (string) envfree; + function decimals() external returns (uint8) envfree; + function totalSupply() external returns (uint256) envfree; + function balanceOf(address) external returns (uint256) envfree; + function allowance(address,address) external returns (uint256) envfree; + function approve(address,uint256) external returns (bool); + function transfer(address,uint256) external returns (bool); + function transferFrom(address,address,uint256) external returns (bool); } diff --git a/certora/specs/methods/IERC2612.spec b/certora/specs/methods/IERC2612.spec index 0c1689da4c1..4ecc17b494a 100644 --- a/certora/specs/methods/IERC2612.spec +++ b/certora/specs/methods/IERC2612.spec @@ -1,5 +1,5 @@ methods { - permit(address,address,uint256,uint256,uint8,bytes32,bytes32) => DISPATCHER(true) - nonces(address) returns (uint256) envfree => DISPATCHER(true) - DOMAIN_SEPARATOR() returns (bytes32) envfree => DISPATCHER(true) + function permit(address,address,uint256,uint256,uint8,bytes32,bytes32) external; + function nonces(address) external returns (uint256) envfree; + function DOMAIN_SEPARATOR() external returns (bytes32) envfree; } diff --git a/certora/specs/methods/IERC3156.spec b/certora/specs/methods/IERC3156.spec deleted file mode 100644 index 18c10c51592..00000000000 --- a/certora/specs/methods/IERC3156.spec +++ /dev/null @@ -1,5 +0,0 @@ -methods { - maxFlashLoan(address) returns (uint256) envfree => DISPATCHER(true) - flashFee(address,uint256) returns (uint256) envfree => DISPATCHER(true) - flashLoan(address,address,uint256,bytes) returns (bool) => DISPATCHER(true) -} diff --git a/certora/specs/methods/IERC3156FlashBorrower.spec b/certora/specs/methods/IERC3156FlashBorrower.spec new file mode 100644 index 00000000000..733c168c7af --- /dev/null +++ b/certora/specs/methods/IERC3156FlashBorrower.spec @@ -0,0 +1,3 @@ +methods { + function _.onFlashLoan(address,address,uint256,uint256,bytes) external => DISPATCHER(true); +} diff --git a/certora/specs/methods/IERC3156FlashLender.spec b/certora/specs/methods/IERC3156FlashLender.spec new file mode 100644 index 00000000000..66ed14cd13e --- /dev/null +++ b/certora/specs/methods/IERC3156FlashLender.spec @@ -0,0 +1,5 @@ +methods { + function maxFlashLoan(address) external returns (uint256) envfree; + function flashFee(address,uint256) external returns (uint256) envfree; + function flashLoan(address,address,uint256,bytes) external returns (bool); +} diff --git a/certora/specs/methods/IERC5313.spec b/certora/specs/methods/IERC5313.spec index d4c5a0412c8..f1d469fafd7 100644 --- a/certora/specs/methods/IERC5313.spec +++ b/certora/specs/methods/IERC5313.spec @@ -1,3 +1,3 @@ methods { - owner() returns (address) envfree + function owner() external returns (address) envfree; } diff --git a/certora/specs/methods/IERC721.spec b/certora/specs/methods/IERC721.spec index e6d4e1e04d6..34ff50bd1da 100644 --- a/certora/specs/methods/IERC721.spec +++ b/certora/specs/methods/IERC721.spec @@ -1,20 +1,17 @@ methods { // IERC721 - balanceOf(address) returns (uint256) envfree => DISPATCHER(true) - ownerOf(uint256) returns (address) envfree => DISPATCHER(true) - getApproved(uint256) returns (address) envfree => DISPATCHER(true) - isApprovedForAll(address,address) returns (bool) envfree => DISPATCHER(true) - safeTransferFrom(address,address,uint256,bytes) => DISPATCHER(true) - safeTransferFrom(address,address,uint256) => DISPATCHER(true) - transferFrom(address,address,uint256) => DISPATCHER(true) - approve(address,uint256) => DISPATCHER(true) - setApprovalForAll(address,bool) => DISPATCHER(true) + function balanceOf(address) external returns (uint256) envfree; + function ownerOf(uint256) external returns (address) envfree; + function getApproved(uint256) external returns (address) envfree; + function isApprovedForAll(address,address) external returns (bool) envfree; + function safeTransferFrom(address,address,uint256,bytes) external; + function safeTransferFrom(address,address,uint256) external; + function transferFrom(address,address,uint256) external; + function approve(address,uint256) external; + function setApprovalForAll(address,bool) external; // IERC721Metadata - name() returns (string) => DISPATCHER(true) - symbol() returns (string) => DISPATCHER(true) - tokenURI(uint256) returns (string) => DISPATCHER(true) - - // IERC721Receiver - onERC721Received(address,address,uint256,bytes) returns (bytes4) => DISPATCHER(true) + function name() external returns (string); + function symbol() external returns (string); + function tokenURI(uint256) external returns (string); } diff --git a/certora/specs/methods/IERC721Receiver.spec b/certora/specs/methods/IERC721Receiver.spec new file mode 100644 index 00000000000..e6bdf42835b --- /dev/null +++ b/certora/specs/methods/IERC721Receiver.spec @@ -0,0 +1,3 @@ +methods { + function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true); +} diff --git a/certora/specs/methods/IOwnable.spec b/certora/specs/methods/IOwnable.spec index cfa15f95ff1..4d7c925c52d 100644 --- a/certora/specs/methods/IOwnable.spec +++ b/certora/specs/methods/IOwnable.spec @@ -1,5 +1,5 @@ methods { - owner() returns (address) envfree - transferOwnership(address) - renounceOwnership() + function owner() external returns (address) envfree; + function transferOwnership(address) external; + function renounceOwnership() external; } diff --git a/certora/specs/methods/IOwnable2Step.spec b/certora/specs/methods/IOwnable2Step.spec index c8e671d272c..e6a99570a62 100644 --- a/certora/specs/methods/IOwnable2Step.spec +++ b/certora/specs/methods/IOwnable2Step.spec @@ -1,7 +1,7 @@ methods { - owner() returns (address) envfree - pendingOwner() returns (address) envfree - transferOwnership(address) - acceptOwnership() - renounceOwnership() + function owner() external returns (address) envfree; + function pendingOwner() external returns (address) envfree; + function transferOwnership(address) external; + function acceptOwnership() external; + function renounceOwnership() external; } diff --git a/requirements.txt b/requirements.txt index b92a2728d53..fd0ec301991 100644 --- a/requirements.txt +++ b/requirements.txt @@ -1 +1 @@ -certora-cli==4.3.1 +certora-cli==4.8.0