From e7ba2f778487c9adf708552565ed00491e619482 Mon Sep 17 00:00:00 2001 From: NishantKoyalwar <122688383+NishantKoyalwar@users.noreply.github.com> Date: Tue, 5 Sep 2023 01:47:16 +0530 Subject: [PATCH 1/7] Move beneficiary zero address check to Ownable (#4531) Co-authored-by: Hadrien Croubois Co-authored-by: Francisco --- .changeset/clever-bats-kick.md | 5 +++++ contracts/access/Ownable.sol | 3 +++ contracts/finance/VestingWallet.sol | 9 --------- test/access/Ownable.test.js | 4 ++++ test/finance/VestingWallet.test.js | 2 +- 5 files changed, 13 insertions(+), 10 deletions(-) create mode 100644 .changeset/clever-bats-kick.md diff --git a/.changeset/clever-bats-kick.md b/.changeset/clever-bats-kick.md new file mode 100644 index 000000000..b35301b73 --- /dev/null +++ b/.changeset/clever-bats-kick.md @@ -0,0 +1,5 @@ +--- +'openzeppelin-solidity': patch +--- + +`Ownable`: Prevent using address(0) as the initial owner. diff --git a/contracts/access/Ownable.sol b/contracts/access/Ownable.sol index aa495ff4d..3cf113782 100644 --- a/contracts/access/Ownable.sol +++ b/contracts/access/Ownable.sol @@ -36,6 +36,9 @@ abstract contract Ownable is Context { * @dev Initializes the contract setting the address provided by the deployer as the initial owner. */ constructor(address initialOwner) { + if (initialOwner == address(0)) { + revert OwnableInvalidOwner(address(0)); + } _transferOwnership(initialOwner); } diff --git a/contracts/finance/VestingWallet.sol b/contracts/finance/VestingWallet.sol index 7b50e699e..f014e59c4 100644 --- a/contracts/finance/VestingWallet.sol +++ b/contracts/finance/VestingWallet.sol @@ -31,11 +31,6 @@ contract VestingWallet is Context, Ownable { event EtherReleased(uint256 amount); event ERC20Released(address indexed token, uint256 amount); - /** - * @dev The `beneficiary` is not a valid account. - */ - error VestingWalletInvalidBeneficiary(address beneficiary); - uint256 private _released; mapping(address token => uint256) private _erc20Released; uint64 private immutable _start; @@ -46,10 +41,6 @@ contract VestingWallet is Context, Ownable { * vesting duration of the vesting wallet. */ constructor(address beneficiary, uint64 startTimestamp, uint64 durationSeconds) payable Ownable(beneficiary) { - if (beneficiary == address(0)) { - revert VestingWalletInvalidBeneficiary(address(0)); - } - _start = startTimestamp; _duration = durationSeconds; } diff --git a/test/access/Ownable.test.js b/test/access/Ownable.test.js index 079d694d7..f85daec5d 100644 --- a/test/access/Ownable.test.js +++ b/test/access/Ownable.test.js @@ -14,6 +14,10 @@ contract('Ownable', function (accounts) { this.ownable = await Ownable.new(owner); }); + it('rejects zero address for initialOwner', async function () { + await expectRevertCustomError(Ownable.new(constants.ZERO_ADDRESS), 'OwnableInvalidOwner', [constants.ZERO_ADDRESS]); + }); + it('has an owner', async function () { expect(await this.ownable.owner()).to.equal(owner); }); diff --git a/test/finance/VestingWallet.test.js b/test/finance/VestingWallet.test.js index d79aea195..918e56345 100644 --- a/test/finance/VestingWallet.test.js +++ b/test/finance/VestingWallet.test.js @@ -23,7 +23,7 @@ contract('VestingWallet', function (accounts) { it('rejects zero address for beneficiary', async function () { await expectRevertCustomError( VestingWallet.new(constants.ZERO_ADDRESS, this.start, duration), - 'VestingWalletInvalidBeneficiary', + 'OwnableInvalidOwner', [constants.ZERO_ADDRESS], ); }); From 1523a4f071f101d4bcbffcd4b87dd1b03080ec26 Mon Sep 17 00:00:00 2001 From: Ownerless Inc <90667119+0xneves@users.noreply.github.com> Date: Mon, 4 Sep 2023 18:05:42 -0300 Subject: [PATCH 2/7] Fix accuracy of docs for ERC20._burn (#4574) Co-authored-by: Francisco --- contracts/token/ERC20/ERC20.sol | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/contracts/token/ERC20/ERC20.sol b/contracts/token/ERC20/ERC20.sol index 343881ff3..8eeb3149b 100644 --- a/contracts/token/ERC20/ERC20.sol +++ b/contracts/token/ERC20/ERC20.sol @@ -287,7 +287,7 @@ abstract contract ERC20 is Context, IERC20, IERC20Metadata, IERC20Errors { } /** - * @dev Destroys a `value` amount of tokens from `account`, by transferring it to address(0). + * @dev Destroys a `value` amount of tokens from `account`, lowering the total supply. * Relies on the `_update` mechanism. * * Emits a {Transfer} event with `to` set to the zero address. From 9ef69c03d13230aeff24d91cb54c9d24c4de7c8b Mon Sep 17 00:00:00 2001 From: "renovate[bot]" <29139614+renovate[bot]@users.noreply.github.com> Date: Mon, 4 Sep 2023 21:38:01 +0000 Subject: [PATCH 3/7] Update actions/checkout action to v4 (#4572) Co-authored-by: renovate[bot] <29139614+renovate[bot]@users.noreply.github.com> Co-authored-by: Francisco Giordano --- .github/workflows/actionlint.yml | 2 +- .github/workflows/changeset.yml | 2 +- .github/workflows/checks.yml | 14 +++++++------- .github/workflows/docs.yml | 2 +- .github/workflows/formal-verification.yml | 4 ++-- .github/workflows/release-cycle.yml | 14 +++++++------- .github/workflows/upgradeable.yml | 2 +- 7 files changed, 20 insertions(+), 20 deletions(-) diff --git a/.github/workflows/actionlint.yml b/.github/workflows/actionlint.yml index 8193109cf..3e42c8a26 100644 --- a/.github/workflows/actionlint.yml +++ b/.github/workflows/actionlint.yml @@ -9,7 +9,7 @@ jobs: lint: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 - name: Add problem matchers run: | # https://github.com/rhysd/actionlint/blob/3a2f2c7/docs/usage.md#problem-matchers diff --git a/.github/workflows/changeset.yml b/.github/workflows/changeset.yml index 5fe70cfcc..efc5c5347 100644 --- a/.github/workflows/changeset.yml +++ b/.github/workflows/changeset.yml @@ -19,7 +19,7 @@ jobs: runs-on: ubuntu-latest if: ${{ !contains(github.event.pull_request.labels.*.name, 'ignore-changeset') }} steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 with: fetch-depth: 0 # Include history so Changesets finds merge-base - name: Set up environment diff --git a/.github/workflows/checks.yml b/.github/workflows/checks.yml index 199d9e36f..0ba977525 100644 --- a/.github/workflows/checks.yml +++ b/.github/workflows/checks.yml @@ -20,7 +20,7 @@ jobs: lint: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 - name: Set up environment uses: ./.github/actions/setup - run: npm run lint @@ -31,7 +31,7 @@ jobs: FORCE_COLOR: 1 GAS: true steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 - name: Set up environment uses: ./.github/actions/setup - name: Run tests and generate gas report @@ -50,7 +50,7 @@ jobs: env: FORCE_COLOR: 1 steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 with: fetch-depth: 0 # Include history so patch conflicts are resolved automatically - name: Set up environment @@ -70,7 +70,7 @@ jobs: tests-foundry: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 with: submodules: recursive - name: Install Foundry @@ -83,7 +83,7 @@ jobs: coverage: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 - name: Set up environment uses: ./.github/actions/setup - run: npm run coverage @@ -94,7 +94,7 @@ jobs: slither: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 - name: Set up environment uses: ./.github/actions/setup - run: rm foundry.toml @@ -105,7 +105,7 @@ jobs: codespell: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 - name: Run CodeSpell uses: codespell-project/actions-codespell@v2.0 with: diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 4b54ea6ee..04b8131cb 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -11,7 +11,7 @@ jobs: build: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 - name: Set up environment uses: ./.github/actions/setup - run: bash scripts/git-user-config.sh diff --git a/.github/workflows/formal-verification.yml b/.github/workflows/formal-verification.yml index a86f255fb..6b4ca2cad 100644 --- a/.github/workflows/formal-verification.yml +++ b/.github/workflows/formal-verification.yml @@ -20,7 +20,7 @@ jobs: apply-diff: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 - name: Apply patches run: make -C certora apply @@ -28,7 +28,7 @@ jobs: runs-on: ubuntu-latest if: github.event_name != 'pull_request' || contains(github.event.pull_request.labels.*.name, 'formal-verification') steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 with: fetch-depth: 0 - name: Set up environment diff --git a/.github/workflows/release-cycle.yml b/.github/workflows/release-cycle.yml index 9d35022dc..21d77abb9 100644 --- a/.github/workflows/release-cycle.yml +++ b/.github/workflows/release-cycle.yml @@ -27,7 +27,7 @@ jobs: pull-requests: read runs-on: ubuntu-latest steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 - name: Set up environment uses: ./.github/actions/setup - id: state @@ -58,7 +58,7 @@ jobs: if: needs.state.outputs.start == 'true' runs-on: ubuntu-latest steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 - name: Set up environment uses: ./.github/actions/setup - run: bash scripts/git-user-config.sh @@ -81,7 +81,7 @@ jobs: if: needs.state.outputs.promote == 'true' runs-on: ubuntu-latest steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 - name: Set up environment uses: ./.github/actions/setup - run: bash scripts/git-user-config.sh @@ -102,7 +102,7 @@ jobs: if: needs.state.outputs.changesets == 'true' runs-on: ubuntu-latest steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 with: fetch-depth: 0 # To get all tags - name: Set up environment @@ -134,7 +134,7 @@ jobs: if: needs.state.outputs.publish == 'true' runs-on: ubuntu-latest steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 - name: Set up environment uses: ./.github/actions/setup - id: pack @@ -171,7 +171,7 @@ jobs: name: Tarball Integrity Check runs-on: ubuntu-latest steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 - name: Download tarball artifact id: artifact # Replace with actions/upload-artifact@v3 when @@ -195,7 +195,7 @@ jobs: env: MERGE_BRANCH: merge/${{ github.ref_name }} steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 with: fetch-depth: 0 # All branches - name: Set up environment diff --git a/.github/workflows/upgradeable.yml b/.github/workflows/upgradeable.yml index 649596abb..ed63a6dbe 100644 --- a/.github/workflows/upgradeable.yml +++ b/.github/workflows/upgradeable.yml @@ -11,7 +11,7 @@ jobs: environment: push-upgradeable runs-on: ubuntu-latest steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 with: repository: OpenZeppelin/openzeppelin-contracts-upgradeable fetch-depth: 0 From 095c8e120c0cc0d9003db358708740bcbc4276a1 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Mon, 11 Sep 2023 17:07:25 +0200 Subject: [PATCH 4/7] Remove SafeERC20.safePermit (#4582) Co-authored-by: Francisco --- .changeset/green-pumpkins-end.md | 5 + .../mocks/token/ERC20PermitNoRevertMock.sol | 35 ----- contracts/token/ERC20/README.adoc | 8 +- .../token/ERC20/extensions/ERC20Permit.sol | 6 +- .../token/ERC20/extensions/IERC20Permit.sol | 30 +++++ contracts/token/ERC20/utils/SafeERC20.sol | 22 ---- test/token/ERC20/utils/SafeERC20.test.js | 123 ------------------ 7 files changed, 43 insertions(+), 186 deletions(-) create mode 100644 .changeset/green-pumpkins-end.md delete mode 100644 contracts/mocks/token/ERC20PermitNoRevertMock.sol diff --git a/.changeset/green-pumpkins-end.md b/.changeset/green-pumpkins-end.md new file mode 100644 index 000000000..03cfe023f --- /dev/null +++ b/.changeset/green-pumpkins-end.md @@ -0,0 +1,5 @@ +--- +'openzeppelin-solidity': major +--- + +`SafeERC20`: Removed `safePermit` in favor of documentation-only `permit` recommendations. diff --git a/contracts/mocks/token/ERC20PermitNoRevertMock.sol b/contracts/mocks/token/ERC20PermitNoRevertMock.sol deleted file mode 100644 index 64e82b6f3..000000000 --- a/contracts/mocks/token/ERC20PermitNoRevertMock.sol +++ /dev/null @@ -1,35 +0,0 @@ -// SPDX-License-Identifier: MIT - -pragma solidity ^0.8.20; - -import {ERC20Permit} from "../../token/ERC20/extensions/ERC20Permit.sol"; - -abstract contract ERC20PermitNoRevertMock is ERC20Permit { - function permitThatMayRevert( - address owner, - address spender, - uint256 value, - uint256 deadline, - uint8 v, - bytes32 r, - bytes32 s - ) public virtual { - super.permit(owner, spender, value, deadline, v, r, s); - } - - function permit( - address owner, - address spender, - uint256 value, - uint256 deadline, - uint8 v, - bytes32 r, - bytes32 s - ) public virtual override { - try this.permitThatMayRevert(owner, spender, value, deadline, v, r, s) { - // do nothing - } catch { - // do nothing - } - } -} diff --git a/contracts/token/ERC20/README.adoc b/contracts/token/ERC20/README.adoc index 9482b581b..2c508802d 100644 --- a/contracts/token/ERC20/README.adoc +++ b/contracts/token/ERC20/README.adoc @@ -15,10 +15,10 @@ There are a few core contracts that implement the behavior specified in the EIP: Additionally there are multiple custom extensions, including: +* {ERC20Permit}: gasless approval of tokens (standardized as ERC2612). * {ERC20Burnable}: destruction of own tokens. * {ERC20Capped}: enforcement of a cap to the total supply when minting tokens. * {ERC20Pausable}: ability to pause token transfers. -* {ERC20Permit}: gasless approval of tokens (standardized as ERC2612). * {ERC20FlashMint}: token level support for flash loans through the minting and burning of ephemeral tokens (standardized as ERC3156). * {ERC20Votes}: support for voting and vote delegation. * {ERC20Wrapper}: wrapper to create an ERC20 backed by another ERC20, with deposit and withdraw methods. Useful in conjunction with {ERC20Votes}. @@ -44,14 +44,16 @@ NOTE: This core set of contracts is designed to be unopinionated, allowing devel == Extensions +{{IERC20Permit}} + +{{ERC20Permit}} + {{ERC20Burnable}} {{ERC20Capped}} {{ERC20Pausable}} -{{ERC20Permit}} - {{ERC20Votes}} {{ERC20Wrapper}} diff --git a/contracts/token/ERC20/extensions/ERC20Permit.sol b/contracts/token/ERC20/extensions/ERC20Permit.sol index d6efb477e..4165fbaca 100644 --- a/contracts/token/ERC20/extensions/ERC20Permit.sol +++ b/contracts/token/ERC20/extensions/ERC20Permit.sol @@ -39,7 +39,7 @@ abstract contract ERC20Permit is ERC20, IERC20Permit, EIP712, Nonces { constructor(string memory name) EIP712(name, "1") {} /** - * @dev See {IERC20Permit-permit}. + * @inheritdoc IERC20Permit */ function permit( address owner, @@ -67,14 +67,14 @@ abstract contract ERC20Permit is ERC20, IERC20Permit, EIP712, Nonces { } /** - * @dev See {IERC20Permit-nonces}. + * @inheritdoc IERC20Permit */ function nonces(address owner) public view virtual override(IERC20Permit, Nonces) returns (uint256) { return super.nonces(owner); } /** - * @dev See {IERC20Permit-DOMAIN_SEPARATOR}. + * @inheritdoc IERC20Permit */ // solhint-disable-next-line func-name-mixedcase function DOMAIN_SEPARATOR() external view virtual returns (bytes32) { diff --git a/contracts/token/ERC20/extensions/IERC20Permit.sol b/contracts/token/ERC20/extensions/IERC20Permit.sol index 237041006..b3260f305 100644 --- a/contracts/token/ERC20/extensions/IERC20Permit.sol +++ b/contracts/token/ERC20/extensions/IERC20Permit.sol @@ -10,6 +10,34 @@ pragma solidity ^0.8.20; * Adds the {permit} method, which can be used to change an account's ERC20 allowance (see {IERC20-allowance}) by * presenting a message signed by the account. By not relying on {IERC20-approve}, the token holder account doesn't * need to send a transaction, and thus is not required to hold Ether at all. + * + * ==== Security Considerations + * + * There are two important considerations concerning the use of `permit`. The first is that a valid permit signature + * expresses an allowance, and it should not be assumed to convey additional meaning. In particular, it should not be + * considered as an intention to spend the allowance in any specific way. The second is that because permits have + * built-in replay protection and can be submitted by anyone, they can be frontrun. A protocol that uses permits should + * take this into consideration and allow a `permit` call to fail. Combining these two aspects, a pattern that may be + * generally recommended is: + * + * ```solidity + * function doThingWithPermit(..., uint256 value, uint256 deadline, uint8 v, bytes32 r, bytes32 s) public { + * try token.permit(msg.sender, address(this), value, deadline, v, r, s) {} catch {} + * doThing(..., value); + * } + * + * function doThing(..., uint256 value) public { + * token.safeTransferFrom(msg.sender, address(this), value); + * ... + * } + * ``` + * + * Observe that: 1) `msg.sender` is used as the owner, leaving no ambiguity as to the signer intent, and 2) the use of + * `try/catch` allows the permit to fail and makes the code tolerant to frontrunning. (See also + * {SafeERC20-safeTransferFrom}). + * + * Additionally, note that smart contract wallets (such as Argent or Safe) are not able to produce permit signatures, so + * contracts should have entry points that don't rely on permit. */ interface IERC20Permit { /** @@ -32,6 +60,8 @@ interface IERC20Permit { * For more information on the signature format, see the * https://eips.ethereum.org/EIPS/eip-2612#specification[relevant EIP * section]. + * + * CAUTION: See Security Considerations above. */ function permit( address owner, diff --git a/contracts/token/ERC20/utils/SafeERC20.sol b/contracts/token/ERC20/utils/SafeERC20.sol index fcdbbae76..e8b699cb0 100644 --- a/contracts/token/ERC20/utils/SafeERC20.sol +++ b/contracts/token/ERC20/utils/SafeERC20.sol @@ -82,28 +82,6 @@ library SafeERC20 { } } - /** - * @dev Use a ERC-2612 signature to set the `owner` approval toward `spender` on `token`. - * Revert on invalid signature. - */ - function safePermit( - IERC20Permit token, - address owner, - address spender, - uint256 value, - uint256 deadline, - uint8 v, - bytes32 r, - bytes32 s - ) internal { - uint256 nonceBefore = token.nonces(owner); - token.permit(owner, spender, value, deadline, v, r, s); - uint256 nonceAfter = token.nonces(owner); - if (nonceAfter != nonceBefore + 1) { - revert SafeERC20FailedOperation(address(token)); - } - } - /** * @dev Imitates a Solidity high-level call (i.e. a regular function call to a contract), relaxing the requirement * on the return value: the return value is optional (but if data is returned, it must not be false). diff --git a/test/token/ERC20/utils/SafeERC20.test.js b/test/token/ERC20/utils/SafeERC20.test.js index eb6e26755..4ff27f14d 100644 --- a/test/token/ERC20/utils/SafeERC20.test.js +++ b/test/token/ERC20/utils/SafeERC20.test.js @@ -4,16 +4,10 @@ const SafeERC20 = artifacts.require('$SafeERC20'); const ERC20ReturnFalseMock = artifacts.require('$ERC20ReturnFalseMock'); const ERC20ReturnTrueMock = artifacts.require('$ERC20'); // default implementation returns true const ERC20NoReturnMock = artifacts.require('$ERC20NoReturnMock'); -const ERC20PermitNoRevertMock = artifacts.require('$ERC20PermitNoRevertMock'); const ERC20ForceApproveMock = artifacts.require('$ERC20ForceApproveMock'); -const { getDomain, domainType, Permit } = require('../../../helpers/eip712'); const { expectRevertCustomError } = require('../../../helpers/customError'); -const { fromRpcSig } = require('ethereumjs-util'); -const ethSigUtil = require('eth-sig-util'); -const Wallet = require('ethereumjs-wallet').default; - const name = 'ERC20Mock'; const symbol = 'ERC20Mock'; @@ -122,123 +116,6 @@ contract('SafeERC20', function (accounts) { shouldOnlyRevertOnErrors(accounts); }); - describe("with token that doesn't revert on invalid permit", function () { - const wallet = Wallet.generate(); - const owner = wallet.getAddressString(); - const spender = hasNoCode; - - beforeEach(async function () { - this.token = await ERC20PermitNoRevertMock.new(name, symbol, name); - - this.data = await getDomain(this.token).then(domain => ({ - primaryType: 'Permit', - types: { EIP712Domain: domainType(domain), Permit }, - domain, - message: { owner, spender, value: '42', nonce: '0', deadline: constants.MAX_UINT256 }, - })); - - this.signature = fromRpcSig(ethSigUtil.signTypedMessage(wallet.getPrivateKey(), { data: this.data })); - }); - - it('accepts owner signature', async function () { - expect(await this.token.nonces(owner)).to.be.bignumber.equal('0'); - expect(await this.token.allowance(owner, spender)).to.be.bignumber.equal('0'); - - await this.mock.$safePermit( - this.token.address, - this.data.message.owner, - this.data.message.spender, - this.data.message.value, - this.data.message.deadline, - this.signature.v, - this.signature.r, - this.signature.s, - ); - - expect(await this.token.nonces(owner)).to.be.bignumber.equal('1'); - expect(await this.token.allowance(owner, spender)).to.be.bignumber.equal(this.data.message.value); - }); - - it('revert on reused signature', async function () { - expect(await this.token.nonces(owner)).to.be.bignumber.equal('0'); - // use valid signature and consume nounce - await this.mock.$safePermit( - this.token.address, - this.data.message.owner, - this.data.message.spender, - this.data.message.value, - this.data.message.deadline, - this.signature.v, - this.signature.r, - this.signature.s, - ); - expect(await this.token.nonces(owner)).to.be.bignumber.equal('1'); - // invalid call does not revert for this token implementation - await this.token.permit( - this.data.message.owner, - this.data.message.spender, - this.data.message.value, - this.data.message.deadline, - this.signature.v, - this.signature.r, - this.signature.s, - ); - expect(await this.token.nonces(owner)).to.be.bignumber.equal('1'); - // invalid call revert when called through the SafeERC20 library - await expectRevertCustomError( - this.mock.$safePermit( - this.token.address, - this.data.message.owner, - this.data.message.spender, - this.data.message.value, - this.data.message.deadline, - this.signature.v, - this.signature.r, - this.signature.s, - ), - 'SafeERC20FailedOperation', - [this.token.address], - ); - expect(await this.token.nonces(owner)).to.be.bignumber.equal('1'); - }); - - it('revert on invalid signature', async function () { - // signature that is not valid for owner - const invalidSignature = { - v: 27, - r: '0x71753dc5ecb5b4bfc0e3bc530d79ce5988760ed3f3a234c86a5546491f540775', - s: '0x0049cedee5aed990aabed5ad6a9f6e3c565b63379894b5fa8b512eb2b79e485d', - }; - - // invalid call does not revert for this token implementation - await this.token.permit( - this.data.message.owner, - this.data.message.spender, - this.data.message.value, - this.data.message.deadline, - invalidSignature.v, - invalidSignature.r, - invalidSignature.s, - ); - - // invalid call revert when called through the SafeERC20 library - await expectRevertCustomError( - this.mock.$safePermit( - this.token.address, - this.data.message.owner, - this.data.message.spender, - this.data.message.value, - this.data.message.deadline, - invalidSignature.v, - invalidSignature.r, - invalidSignature.s, - ), - 'SafeERC20FailedOperation', - [this.token.address], - ); - }); - }); - describe('with usdt approval beaviour', function () { const spender = hasNoCode; From b6111faac8e22958ac031df305c7a5923063f543 Mon Sep 17 00:00:00 2001 From: Francisco Date: Mon, 11 Sep 2023 16:32:10 -0300 Subject: [PATCH 5/7] Use namespaced storage for upgradeable contracts (#4534) --- .changeset/wet-bears-heal.md | 5 ++ .github/actions/setup/action.yml | 2 +- contracts/governance/Governor.sol | 6 +- .../governance/extensions/GovernorVotes.sol | 17 ++++-- .../GovernorVotesQuorumFraction.sol | 2 +- package-lock.json | 56 ++++++++++++++++--- package.json | 2 +- scripts/upgradeable/transpile.sh | 6 +- 8 files changed, 75 insertions(+), 21 deletions(-) create mode 100644 .changeset/wet-bears-heal.md diff --git a/.changeset/wet-bears-heal.md b/.changeset/wet-bears-heal.md new file mode 100644 index 000000000..2df32f39a --- /dev/null +++ b/.changeset/wet-bears-heal.md @@ -0,0 +1,5 @@ +--- +'openzeppelin-solidity': major +--- + +Upgradeable contracts now use namespaced storage (EIP-7201). diff --git a/.github/actions/setup/action.yml b/.github/actions/setup/action.yml index 680fba0c6..84ebe823a 100644 --- a/.github/actions/setup/action.yml +++ b/.github/actions/setup/action.yml @@ -5,7 +5,7 @@ runs: steps: - uses: actions/setup-node@v3 with: - node-version: 14.x + node-version: 16.x - uses: actions/cache@v3 id: cache with: diff --git a/contracts/governance/Governor.sol b/contracts/governance/Governor.sol index b4abaa695..f5d68f654 100644 --- a/contracts/governance/Governor.sol +++ b/contracts/governance/Governor.sol @@ -299,8 +299,8 @@ abstract contract Governor is Context, ERC165, EIP712, Nonces, IGovernor, IERC72 bytes[] memory calldatas, string memory description, address proposer - ) internal virtual returns (uint256) { - uint256 proposalId = hashProposal(targets, values, calldatas, keccak256(bytes(description))); + ) internal virtual returns (uint256 proposalId) { + proposalId = hashProposal(targets, values, calldatas, keccak256(bytes(description))); if (targets.length != values.length || targets.length != calldatas.length || targets.length == 0) { revert GovernorInvalidProposalLength(targets.length, calldatas.length, values.length); @@ -329,7 +329,7 @@ abstract contract Governor is Context, ERC165, EIP712, Nonces, IGovernor, IERC72 description ); - return proposalId; + // Using a named return variable to avoid stack too deep errors } /** diff --git a/contracts/governance/extensions/GovernorVotes.sol b/contracts/governance/extensions/GovernorVotes.sol index 45447da51..3ea1bd2bf 100644 --- a/contracts/governance/extensions/GovernorVotes.sol +++ b/contracts/governance/extensions/GovernorVotes.sol @@ -12,10 +12,17 @@ import {SafeCast} from "../../utils/math/SafeCast.sol"; * @dev Extension of {Governor} for voting weight extraction from an {ERC20Votes} token, or since v4.5 an {ERC721Votes} token. */ abstract contract GovernorVotes is Governor { - IERC5805 public immutable token; + IERC5805 private immutable _token; constructor(IVotes tokenAddress) { - token = IERC5805(address(tokenAddress)); + _token = IERC5805(address(tokenAddress)); + } + + /** + * @dev The token that voting power is sourced from. + */ + function token() public view virtual returns (IERC5805) { + return _token; } /** @@ -23,7 +30,7 @@ abstract contract GovernorVotes is Governor { * does not implement EIP-6372. */ function clock() public view virtual override returns (uint48) { - try token.clock() returns (uint48 timepoint) { + try token().clock() returns (uint48 timepoint) { return timepoint; } catch { return SafeCast.toUint48(block.number); @@ -35,7 +42,7 @@ abstract contract GovernorVotes is Governor { */ // solhint-disable-next-line func-name-mixedcase function CLOCK_MODE() public view virtual override returns (string memory) { - try token.CLOCK_MODE() returns (string memory clockmode) { + try token().CLOCK_MODE() returns (string memory clockmode) { return clockmode; } catch { return "mode=blocknumber&from=default"; @@ -50,6 +57,6 @@ abstract contract GovernorVotes is Governor { uint256 timepoint, bytes memory /*params*/ ) internal view virtual override returns (uint256) { - return token.getPastVotes(account, timepoint); + return token().getPastVotes(account, timepoint); } } diff --git a/contracts/governance/extensions/GovernorVotesQuorumFraction.sol b/contracts/governance/extensions/GovernorVotesQuorumFraction.sol index cc2e85b45..100758e3b 100644 --- a/contracts/governance/extensions/GovernorVotesQuorumFraction.sol +++ b/contracts/governance/extensions/GovernorVotesQuorumFraction.sol @@ -71,7 +71,7 @@ abstract contract GovernorVotesQuorumFraction is GovernorVotes { * @dev Returns the quorum for a timepoint, in terms of number of votes: `supply * numerator / denominator`. */ function quorum(uint256 timepoint) public view virtual override returns (uint256) { - return (token.getPastTotalSupply(timepoint) * quorumNumerator(timepoint)) / quorumDenominator(); + return (token().getPastTotalSupply(timepoint) * quorumNumerator(timepoint)) / quorumDenominator(); } /** diff --git a/package-lock.json b/package-lock.json index 22fe93cb7..fdcda1e7b 100644 --- a/package-lock.json +++ b/package-lock.json @@ -44,7 +44,7 @@ "semver": "^7.3.5", "solhint": "^3.3.6", "solhint-plugin-openzeppelin": "file:scripts/solhint-custom", - "solidity-ast": "^0.4.25", + "solidity-ast": "^0.4.50", "solidity-coverage": "^0.8.0", "solidity-docgen": "^0.6.0-beta.29", "undici": "^5.22.1", @@ -3221,6 +3221,25 @@ "url": "https://github.com/sponsors/ljharb" } }, + "node_modules/array.prototype.findlast": { + "version": "1.2.2", + "resolved": "https://registry.npmjs.org/array.prototype.findlast/-/array.prototype.findlast-1.2.2.tgz", + "integrity": "sha512-p1YDNPNqA+P6cPX9ATsxg7DKir7gOmJ+jh5dEP3LlumMNYVC1F2Jgnyh6oI3n/qD9FeIkqR2jXfd73G68ImYUQ==", + "dev": true, + "dependencies": { + "call-bind": "^1.0.2", + "define-properties": "^1.1.4", + "es-abstract": "^1.20.4", + "es-shim-unscopables": "^1.0.0", + "get-intrinsic": "^1.1.3" + }, + "engines": { + "node": ">= 0.4" + }, + "funding": { + "url": "https://github.com/sponsors/ljharb" + } + }, "node_modules/array.prototype.flat": { "version": "1.3.1", "resolved": "https://registry.npmjs.org/array.prototype.flat/-/array.prototype.flat-1.3.1.tgz", @@ -12569,10 +12588,13 @@ } }, "node_modules/solidity-ast": { - "version": "0.4.49", - "resolved": "https://registry.npmjs.org/solidity-ast/-/solidity-ast-0.4.49.tgz", - "integrity": "sha512-Pr5sCAj1SFqzwFZw1HPKSq0PehlQNdM8GwKyAVYh2DOn7/cCK8LUKD1HeHnKtTgBW7hi9h4nnnan7hpAg5RhWQ==", - "dev": true + "version": "0.4.50", + "resolved": "https://registry.npmjs.org/solidity-ast/-/solidity-ast-0.4.50.tgz", + "integrity": "sha512-WpIhaUibbjcBY4bg8TO2UXFWl8PQPhtH1QtMYJUqFUGxx0rRiEFsVLV+ow8XiWEnSPeu4xPp1/K43P4esxuK1Q==", + "dev": true, + "dependencies": { + "array.prototype.findlast": "^1.2.2" + } }, "node_modules/solidity-comments": { "version": "0.0.2", @@ -17853,6 +17875,19 @@ "es-shim-unscopables": "^1.0.0" } }, + "array.prototype.findlast": { + "version": "1.2.2", + "resolved": "https://registry.npmjs.org/array.prototype.findlast/-/array.prototype.findlast-1.2.2.tgz", + "integrity": "sha512-p1YDNPNqA+P6cPX9ATsxg7DKir7gOmJ+jh5dEP3LlumMNYVC1F2Jgnyh6oI3n/qD9FeIkqR2jXfd73G68ImYUQ==", + "dev": true, + "requires": { + "call-bind": "^1.0.2", + "define-properties": "^1.1.4", + "es-abstract": "^1.20.4", + "es-shim-unscopables": "^1.0.0", + "get-intrinsic": "^1.1.3" + } + }, "array.prototype.flat": { "version": "1.3.1", "resolved": "https://registry.npmjs.org/array.prototype.flat/-/array.prototype.flat-1.3.1.tgz", @@ -25144,10 +25179,13 @@ "version": "file:scripts/solhint-custom" }, "solidity-ast": { - "version": "0.4.49", - "resolved": "https://registry.npmjs.org/solidity-ast/-/solidity-ast-0.4.49.tgz", - "integrity": "sha512-Pr5sCAj1SFqzwFZw1HPKSq0PehlQNdM8GwKyAVYh2DOn7/cCK8LUKD1HeHnKtTgBW7hi9h4nnnan7hpAg5RhWQ==", - "dev": true + "version": "0.4.50", + "resolved": "https://registry.npmjs.org/solidity-ast/-/solidity-ast-0.4.50.tgz", + "integrity": "sha512-WpIhaUibbjcBY4bg8TO2UXFWl8PQPhtH1QtMYJUqFUGxx0rRiEFsVLV+ow8XiWEnSPeu4xPp1/K43P4esxuK1Q==", + "dev": true, + "requires": { + "array.prototype.findlast": "^1.2.2" + } }, "solidity-comments": { "version": "0.0.2", diff --git a/package.json b/package.json index ffa868ac7..c71139f3e 100644 --- a/package.json +++ b/package.json @@ -85,7 +85,7 @@ "semver": "^7.3.5", "solhint": "^3.3.6", "solhint-plugin-openzeppelin": "file:scripts/solhint-custom", - "solidity-ast": "^0.4.25", + "solidity-ast": "^0.4.50", "solidity-coverage": "^0.8.0", "solidity-docgen": "^0.6.0-beta.29", "undici": "^5.22.1", diff --git a/scripts/upgradeable/transpile.sh b/scripts/upgradeable/transpile.sh index c0cb9ff5e..05de96d34 100644 --- a/scripts/upgradeable/transpile.sh +++ b/scripts/upgradeable/transpile.sh @@ -22,6 +22,8 @@ fi # -i: use included Initializable # -x: exclude proxy-related contracts with a few exceptions # -p: emit public initializer +# -n: use namespaces +# -N: exclude from namespaces transformation npx @openzeppelin/upgrade-safe-transpiler@latest -D \ -b "$build_info" \ -i contracts/proxy/utils/Initializable.sol \ @@ -32,7 +34,9 @@ npx @openzeppelin/upgrade-safe-transpiler@latest -D \ -x '!contracts/proxy/ERC1967/ERC1967Utils.sol' \ -x '!contracts/proxy/utils/UUPSUpgradeable.sol' \ -x '!contracts/proxy/beacon/IBeacon.sol' \ - -p 'contracts/**/presets/**/*' + -p 'contracts/**/presets/**/*' \ + -n \ + -N 'contracts/mocks/**/*' # delete compilation artifacts of vanilla code npm run clean From 36bf1e46fa811f0f07d38eb9cfbc69a955f300ce Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ernesto=20Garc=C3=ADa?= Date: Mon, 11 Sep 2023 14:15:51 -0600 Subject: [PATCH 6/7] Migrate FV specs to CVL2 (#4527) Co-authored-by: Hadrien Croubois --- certora/diff/token_ERC721_ERC721.sol.patch | 14 - .../AccessControlDefaultAdminRulesHarness.sol | 3 +- certora/harnesses/AccessControlHarness.sol | 3 +- certora/harnesses/DoubleEndedQueueHarness.sol | 3 +- certora/harnesses/ERC20PermitHarness.sol | 3 +- certora/harnesses/ERC20WrapperHarness.sol | 15 +- .../harnesses/ERC3156FlashBorrowerHarness.sol | 2 +- certora/harnesses/ERC721Harness.sol | 6 +- certora/harnesses/EnumerableMapHarness.sol | 2 +- certora/harnesses/EnumerableSetHarness.sol | 2 +- certora/harnesses/InitializableHarness.sol | 18 +- certora/harnesses/Ownable2StepHarness.sol | 7 +- certora/harnesses/OwnableHarness.sol | 7 +- certora/harnesses/PausableHarness.sol | 3 +- .../harnesses/TimelockControllerHarness.sol | 3 +- certora/run.js | 8 +- certora/specs/AccessControl.spec | 245 ++++++------ .../specs/AccessControlDefaultAdminRules.spec | 56 +-- certora/specs/ERC20.spec | 80 ++-- certora/specs/ERC20FlashMint.spec | 39 +- certora/specs/ERC20Wrapper.spec | 62 +-- certora/specs/ERC721.spec | 372 +++++++++++------- certora/specs/EnumerableMap.spec | 65 ++- certora/specs/EnumerableSet.spec | 49 ++- certora/specs/Initializable.spec | 38 +- certora/specs/Ownable.spec | 155 ++++---- certora/specs/Ownable2Step.spec | 216 +++++----- certora/specs/Pausable.spec | 192 ++++----- certora/specs/TimelockController.spec | 123 +++--- certora/specs/methods/IAccessControl.spec | 11 +- .../IAccessControlDefaultAdminRules.spec | 32 +- certora/specs/methods/IERC20.spec | 18 +- certora/specs/methods/IERC2612.spec | 6 +- certora/specs/methods/IERC3156.spec | 5 - .../specs/methods/IERC3156FlashBorrower.spec | 3 + .../specs/methods/IERC3156FlashLender.spec | 5 + certora/specs/methods/IERC5313.spec | 2 +- certora/specs/methods/IERC721.spec | 27 +- certora/specs/methods/IERC721Receiver.spec | 3 + certora/specs/methods/IOwnable.spec | 6 +- certora/specs/methods/IOwnable2Step.spec | 10 +- requirements.txt | 2 +- 42 files changed, 1008 insertions(+), 913 deletions(-) delete mode 100644 certora/diff/token_ERC721_ERC721.sol.patch delete mode 100644 certora/specs/methods/IERC3156.spec create mode 100644 certora/specs/methods/IERC3156FlashBorrower.spec create mode 100644 certora/specs/methods/IERC3156FlashLender.spec create mode 100644 certora/specs/methods/IERC721Receiver.spec diff --git a/certora/diff/token_ERC721_ERC721.sol.patch b/certora/diff/token_ERC721_ERC721.sol.patch deleted file mode 100644 index c3eae357a..000000000 --- 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 145f65b76..e96883fa2 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 42a536af1..e862d3eca 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 54852a739..d684c7382 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 1041c1715..08113f4ea 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 5e55e4b72..ca183ad92 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 81dfdaf31..1c76da2d4 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 b0afb589c..69c4c205a 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 2b9a8e47c..5c2f3229b 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 1f4cac7d9..3d18b183b 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 0d0c0a4e4..743d677dd 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 aed6f5854..09a5faa23 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 45666772a..79b4b1b6c 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 12f946709..5977b9202 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 476a8376c..95ae40621 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 68f34aab2..7b65534ea 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 cd5af2a99..70b067218 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 58b9d1202..2f5bb9d45 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 3bd2b38ba..ee601bd19 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 70a7c0795..5c87f0ded 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; +ghost mapping(address => mathint) trackedMintAmount; +ghost mapping(address => mathint) trackedBurnAmount; +ghost mapping(address => mapping(address => mathint)) 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; } +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 badfa7a28..04e67042a 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 + 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; - depositFor(address, uint256) returns(bool) - withdrawTo(address, uint256) returns(bool) - recover(address) returns(uint256) + 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 9db13f45c..bad4c4737 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) + function mint(address,uint256) external; + function safeMint(address,uint256) external; + function safeMint(address,uint256,bytes) external; + function burn(uint256) external; - tokenExists(uint256) returns (bool) envfree - unsafeOwnerOf(uint256) returns (address) envfree - unsafeGetApproved(uint256) returns (address) envfree + 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; +} + +ghost mapping(address => mathint) _balances { + init_state axiom forall address a. _balances[a] == 0; } hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE { - havoc sumOfBalances assuming sumOfBalances@new() == sumOfBalances@old() + newValue - oldValue; -} - -ghost mapping(address => uint256) ghostBalanceOf { - init_state axiom forall address a. ghostBalanceOf[a] == 0; + _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); @@ -132,47 +211,6 @@ invariant ownerHasBalance(uint256 tokenId) } } -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Invariant: tokens that do not exist are not owned and not approved │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -invariant notMintedUnset(uint256 tokenId) - (!tokenExists(tokenId) <=> unsafeOwnerOf(tokenId) == 0) && - (!tokenExists(tokenId) => unsafeGetApproved(tokenId) == 0) - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Rule: ownerOf and getApproved revert if token does not exist │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -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); -} - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Rule: unsafeOwnerOf and unsafeGetApproved don't revert │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -rule unsafeDontRevert(uint256 tokenId) { - unsafeOwnerOf@withrevert(tokenId); - assert !lastReverted; - - unsafeGetApproved@withrevert(tokenId); - assert !lastReverted; -} - /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Rule: balance of address(0) is 0 │ @@ -183,27 +221,74 @@ rule zeroAddressBalanceRevert() { assert lastReverted; } +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: address(0) has no authorized operator │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant zeroAddressHasNoApprovedOperator(address a) + !isApprovedForAll(0, a) + { + preserved with (env e) { + require nonzerosender(e); + } + } + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: tokens that do not exist are not owned and not approved │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant notMintedUnset(uint256 tokenId) + unsafeOwnerOf(tokenId) == 0 => unsafeGetApproved(tokenId) == 0; + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: unsafeOwnerOf and unsafeGetApproved don't revert + ownerOf and getApproved revert if token does not exist │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +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; +} + /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Rules: total supply can only change through mint and burn │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ 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 dea5d85ec..7b503031f 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 d63c556aa..3db515838 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 0e0b1b714..07c2930c2 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 4bf9e3005..0d50813cf 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 47b1b8d75..d13c6d3e6 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 aea38003f..a7aff9cc1 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 05ecb1340..5123768da 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 + 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; - hashOperation(address, uint256, bytes, bytes32, bytes32) returns(bytes32) envfree - hashOperationBatch(address[], uint256[], bytes[], bytes32, bytes32) returns(bytes32) envfree + function hashOperation(address, uint256, bytes, bytes32, bytes32) external returns(bytes32) envfree; + function hashOperationBatch(address[], uint256[], bytes[], bytes32, bytes32) external 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) + 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; - updateDelay(uint256) + 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 4d41ffda7..5c395b088 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 a9dd08b7f..d02db180d 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 cfa454e13..100901a04 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 0c1689da4..4ecc17b49 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 18c10c515..000000000 --- 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 000000000..733c168c7 --- /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 000000000..66ed14cd1 --- /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 d4c5a0412..f1d469faf 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 e6d4e1e04..34ff50bd1 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 000000000..e6bdf4283 --- /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 cfa15f95f..4d7c925c5 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 c8e671d27..e6a99570a 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 b92a2728d..fd0ec3019 100644 --- a/requirements.txt +++ b/requirements.txt @@ -1 +1 @@ -certora-cli==4.3.1 +certora-cli==4.8.0 From 60e3ffe6a3cc38ab94cae995bc1de081eed79335 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Tue, 12 Sep 2023 16:59:48 +0200 Subject: [PATCH 7/7] Remove non-standard increaseAllowance and decreaseAllowance from ERC20 (#4585) Co-authored-by: Francisco --- .changeset/six-frogs-turn.md | 5 + certora/specs/ERC20.spec | 72 -------------- contracts/token/ERC20/ERC20.sol | 52 ----------- test/token/ERC20/ERC20.test.js | 161 -------------------------------- 4 files changed, 5 insertions(+), 285 deletions(-) create mode 100644 .changeset/six-frogs-turn.md diff --git a/.changeset/six-frogs-turn.md b/.changeset/six-frogs-turn.md new file mode 100644 index 000000000..9c5668b6d --- /dev/null +++ b/.changeset/six-frogs-turn.md @@ -0,0 +1,5 @@ +--- +'openzeppelin-solidity': major +--- + +`ERC20`: Remove the non-standard `increaseAllowance` and `decreaseAllowance` functions. diff --git a/certora/specs/ERC20.spec b/certora/specs/ERC20.spec index ee601bd19..21a033585 100644 --- a/certora/specs/ERC20.spec +++ b/certora/specs/ERC20.spec @@ -3,10 +3,6 @@ import "methods/IERC20.spec"; import "methods/IERC2612.spec"; methods { - // non standard ERC20 functions - function increaseAllowance(address,uint256) external returns (bool); - function decreaseAllowance(address,uint256) external returns (bool); - // exposed for FV function mint(address,uint256) external; function burn(address,uint256) external; @@ -117,7 +113,6 @@ rule onlyHolderOfSpenderCanChangeAllowance(env e) { allowanceAfter > allowanceBefore ) => ( (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) ); @@ -126,7 +121,6 @@ rule onlyHolderOfSpenderCanChangeAllowance(env e) { ) => ( (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) ); } @@ -307,72 +301,6 @@ rule approve(env e) { } } -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Rule: increaseAllowance behavior and side effects │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -rule increaseAllowance(env e) { - require nonpayable(e); - - address holder = e.msg.sender; - address spender; - address otherHolder; - address otherSpender; - uint256 amount; - - // cache state - uint256 allowanceBefore = allowance(holder, spender); - uint256 otherAllowanceBefore = allowance(otherHolder, otherSpender); - - // run transaction - increaseAllowance@withrevert(e, spender, amount); - - // check outcome - if (lastReverted) { - assert holder == 0 || spender == 0 || allowanceBefore + amount > max_uint256; - } else { - // allowance is updated - assert to_mathint(allowance(holder, spender)) == allowanceBefore + amount; - - // other allowances are untouched - assert allowance(otherHolder, otherSpender) != otherAllowanceBefore => (otherHolder == holder && otherSpender == spender); - } -} - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Rule: decreaseAllowance behavior and side effects │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -rule decreaseAllowance(env e) { - require nonpayable(e); - - address holder = e.msg.sender; - address spender; - address otherHolder; - address otherSpender; - uint256 amount; - - // cache state - uint256 allowanceBefore = allowance(holder, spender); - uint256 otherAllowanceBefore = allowance(otherHolder, otherSpender); - - // run transaction - decreaseAllowance@withrevert(e, spender, amount); - - // check outcome - if (lastReverted) { - assert holder == 0 || spender == 0 || allowanceBefore < amount; - } else { - // allowance is updated - assert to_mathint(allowance(holder, spender)) == allowanceBefore - amount; - - // other allowances are untouched - assert allowance(otherHolder, otherSpender) != otherAllowanceBefore => (otherHolder == holder && otherSpender == spender); - } -} - /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Rule: permit behavior and side effects │ diff --git a/contracts/token/ERC20/ERC20.sol b/contracts/token/ERC20/ERC20.sol index 8eeb3149b..692fde828 100644 --- a/contracts/token/ERC20/ERC20.sol +++ b/contracts/token/ERC20/ERC20.sol @@ -30,10 +30,6 @@ import {IERC20Errors} from "../../interfaces/draft-IERC6093.sol"; * This allows applications to reconstruct the allowance for all accounts just * by listening to said events. Other implementations of the EIP may not emit * these events, as it isn't required by the specification. - * - * Finally, the non-standard {decreaseAllowance} and {increaseAllowance} - * functions have been added to mitigate the well-known issues around setting - * allowances. See {IERC20-approve}. */ abstract contract ERC20 is Context, IERC20, IERC20Metadata, IERC20Errors { mapping(address account => uint256) private _balances; @@ -167,54 +163,6 @@ abstract contract ERC20 is Context, IERC20, IERC20Metadata, IERC20Errors { return true; } - /** - * @dev Atomically increases the allowance granted to `spender` by the caller. - * - * This is an alternative to {approve} that can be used as a mitigation for - * problems described in {IERC20-approve}. - * - * Emits an {Approval} event indicating the updated allowance. - * - * Requirements: - * - * - `spender` cannot be the zero address. - */ - function increaseAllowance(address spender, uint256 addedValue) public virtual returns (bool) { - address owner = _msgSender(); - _approve(owner, spender, allowance(owner, spender) + addedValue); - return true; - } - - /** - * @dev Atomically decreases the allowance granted to `spender` by the caller. - * - * This is an alternative to {approve} that can be used as a mitigation for - * problems described in {IERC20-approve}. - * - * Emits an {Approval} event indicating the updated allowance. - * - * Requirements: - * - * - `spender` cannot be the zero address. - * - `spender` must have allowance for the caller of at least - * `requestedDecrease`. - * - * NOTE: Although this function is designed to avoid double spending with {approval}, - * it can still be frontrunned, preventing any attempt of allowance reduction. - */ - function decreaseAllowance(address spender, uint256 requestedDecrease) public virtual returns (bool) { - address owner = _msgSender(); - uint256 currentAllowance = allowance(owner, spender); - if (currentAllowance < requestedDecrease) { - revert ERC20FailedDecreaseAllowance(spender, currentAllowance, requestedDecrease); - } - unchecked { - _approve(owner, spender, currentAllowance - requestedDecrease); - } - - return true; - } - /** * @dev Moves a `value` amount of tokens from `from` to `to`. * diff --git a/test/token/ERC20/ERC20.test.js b/test/token/ERC20/ERC20.test.js index a63df5239..2191fd8cb 100644 --- a/test/token/ERC20/ERC20.test.js +++ b/test/token/ERC20/ERC20.test.js @@ -42,167 +42,6 @@ contract('ERC20', function (accounts) { expect(await this.token.decimals()).to.be.bignumber.equal('18'); }); - describe('decrease allowance', function () { - describe('when the spender is not the zero address', function () { - const spender = recipient; - - function shouldDecreaseApproval(value) { - describe('when there was no approved value before', function () { - it('reverts', async function () { - const allowance = await this.token.allowance(initialHolder, spender); - await expectRevertCustomError( - this.token.decreaseAllowance(spender, value, { from: initialHolder }), - 'ERC20FailedDecreaseAllowance', - [spender, allowance, value], - ); - }); - }); - - describe('when the spender had an approved value', function () { - const approvedValue = value; - - beforeEach(async function () { - await this.token.approve(spender, approvedValue, { from: initialHolder }); - }); - - it('emits an approval event', async function () { - expectEvent( - await this.token.decreaseAllowance(spender, approvedValue, { from: initialHolder }), - 'Approval', - { owner: initialHolder, spender: spender, value: new BN(0) }, - ); - }); - - it('decreases the spender allowance subtracting the requested value', async function () { - await this.token.decreaseAllowance(spender, approvedValue.subn(1), { from: initialHolder }); - - expect(await this.token.allowance(initialHolder, spender)).to.be.bignumber.equal('1'); - }); - - it('sets the allowance to zero when all allowance is removed', async function () { - await this.token.decreaseAllowance(spender, approvedValue, { from: initialHolder }); - expect(await this.token.allowance(initialHolder, spender)).to.be.bignumber.equal('0'); - }); - - it('reverts when more than the full allowance is removed', async function () { - await expectRevertCustomError( - this.token.decreaseAllowance(spender, approvedValue.addn(1), { from: initialHolder }), - 'ERC20FailedDecreaseAllowance', - [spender, approvedValue, approvedValue.addn(1)], - ); - }); - }); - } - - describe('when the sender has enough balance', function () { - const value = initialSupply; - - shouldDecreaseApproval(value); - }); - - describe('when the sender does not have enough balance', function () { - const value = initialSupply.addn(1); - - shouldDecreaseApproval(value); - }); - }); - - describe('when the spender is the zero address', function () { - const value = initialSupply; - const spender = ZERO_ADDRESS; - - it('reverts', async function () { - await expectRevertCustomError( - this.token.decreaseAllowance(spender, value, { from: initialHolder }), - 'ERC20FailedDecreaseAllowance', - [spender, 0, value], - ); - }); - }); - }); - - describe('increase allowance', function () { - const value = initialSupply; - - describe('when the spender is not the zero address', function () { - const spender = recipient; - - describe('when the sender has enough balance', function () { - it('emits an approval event', async function () { - expectEvent(await this.token.increaseAllowance(spender, value, { from: initialHolder }), 'Approval', { - owner: initialHolder, - spender: spender, - value: value, - }); - }); - - describe('when there was no approved value before', function () { - it('approves the requested value', async function () { - await this.token.increaseAllowance(spender, value, { from: initialHolder }); - - expect(await this.token.allowance(initialHolder, spender)).to.be.bignumber.equal(value); - }); - }); - - describe('when the spender had an approved value', function () { - beforeEach(async function () { - await this.token.approve(spender, new BN(1), { from: initialHolder }); - }); - - it('increases the spender allowance adding the requested value', async function () { - await this.token.increaseAllowance(spender, value, { from: initialHolder }); - - expect(await this.token.allowance(initialHolder, spender)).to.be.bignumber.equal(value.addn(1)); - }); - }); - }); - - describe('when the sender does not have enough balance', function () { - const value = initialSupply.addn(1); - - it('emits an approval event', async function () { - expectEvent(await this.token.increaseAllowance(spender, value, { from: initialHolder }), 'Approval', { - owner: initialHolder, - spender: spender, - value: value, - }); - }); - - describe('when there was no approved value before', function () { - it('approves the requested value', async function () { - await this.token.increaseAllowance(spender, value, { from: initialHolder }); - - expect(await this.token.allowance(initialHolder, spender)).to.be.bignumber.equal(value); - }); - }); - - describe('when the spender had an approved value', function () { - beforeEach(async function () { - await this.token.approve(spender, new BN(1), { from: initialHolder }); - }); - - it('increases the spender allowance adding the requested value', async function () { - await this.token.increaseAllowance(spender, value, { from: initialHolder }); - - expect(await this.token.allowance(initialHolder, spender)).to.be.bignumber.equal(value.addn(1)); - }); - }); - }); - }); - - describe('when the spender is the zero address', function () { - const spender = ZERO_ADDRESS; - - it('reverts', async function () { - await expectRevertCustomError( - this.token.increaseAllowance(spender, value, { from: initialHolder }), - 'ERC20InvalidSpender', - [ZERO_ADDRESS], - ); - }); - }); - }); - describe('_mint', function () { const value = new BN(50); it('rejects a null account', async function () {