diff --git a/certora/diff/token_ERC721_ERC721.sol.patch b/certora/diff/token_ERC721_ERC721.sol.patch deleted file mode 100644 index 399499eff..000000000 --- a/certora/diff/token_ERC721_ERC721.sol.patch +++ /dev/null @@ -1,14 +0,0 @@ ---- token/ERC721/ERC721.sol 2023-08-11 20:33:54 -+++ token/ERC721/ERC721.sol 2023-08-13 09:56:16 -@@ -214,6 +214,11 @@ - } - } - -+ // FV -+ function _getApproved(uint256 tokenId) internal view returns (address) { -+ return _tokenApprovals[tokenId]; -+ } -+ - /** - * @dev Unsafe write access to the balances, used by extensions that "mint" tokens using an {ownerOf} override. - * diff --git a/certora/harnesses/ERC721Harness.sol b/certora/harnesses/ERC721Harness.sol index b0afb589c..8cd9db9ef 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) {} @@ -24,7 +24,7 @@ contract ERC721Harness is ERC721 { } function tokenExists(uint256 tokenId) external view returns (bool) { - return _exists(tokenId); + return _ownerOf(tokenId) != address(0); } function unsafeOwnerOf(uint256 tokenId) external view returns (address) { diff --git a/certora/specs/ERC721.spec b/certora/specs/ERC721.spec index 9db13f45c..e7dc2e837 100644 --- a/certora/specs/ERC721.spec +++ b/certora/specs/ERC721.spec @@ -1,16 +1,17 @@ -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 tokenExists(uint256) external returns (bool) envfree; + function unsafeOwnerOf(uint256) external returns (address) envfree; + function unsafeGetApproved(uint256) external returns (address) envfree; } /* @@ -19,17 +20,21 @@ methods { └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ +function authSanity(env e) returns bool { + return e.msg.sender != 0; +} + // Could be broken in theory, but not in practice function balanceLimited(address account) returns bool { return 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 +45,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); @@ -58,21 +63,19 @@ function helperMintWithRevert(env e, method f, address to, uint256 tokenId) { │ 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 { +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); + ownedByUser[newOwner] = ownedByUser[newOwner] + to_mathint(newOwner != 0 ? 1 : 0); + ownedByUser[oldOwner] = ownedByUser[oldOwner] - to_mathint(oldOwner != 0 ? 1 : 0); - havoc ownedTotal assuming ownedTotal@new() == ownedTotal@old() - + to_uint256(newOwner != 0 ? 1 : 0) - - to_uint256(oldOwner != 0 ? 1 : 0); + ownedTotal = ownedTotal + to_mathint(newOwner != 0 ? 1 : 0) - to_mathint(oldOwner != 0 ? 1 : 0); } /* @@ -80,20 +83,20 @@ 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 sumOfBalances { + init_state axiom sumOfBalances == 0; } hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE { - havoc sumOfBalances assuming sumOfBalances@new() == sumOfBalances@old() + newValue - oldValue; + sumOfBalances = sumOfBalances - oldValue + newValue; } -ghost mapping(address => uint256) ghostBalanceOf { +ghost mapping(address => mathint) ghostBalanceOf { init_state axiom forall address a. ghostBalanceOf[a] == 0; } hook Sload uint256 value _balances[KEY address user] STORAGE { - require ghostBalanceOf[user] == value; + require ghostBalanceOf[user] == to_mathint(value); } /* @@ -102,7 +105,7 @@ hook Sload uint256 value _balances[KEY address user] STORAGE { └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ invariant ownedTotalIsSumOfBalances() - ownedTotal() == sumOfBalances() + ownedTotal == sumOfBalances; /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ @@ -110,8 +113,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)) == ghostBalanceOf[user] { preserved { require balanceLimited(user); @@ -139,7 +142,7 @@ invariant ownerHasBalance(uint256 tokenId) */ invariant notMintedUnset(uint256 tokenId) (!tokenExists(tokenId) <=> unsafeOwnerOf(tokenId) == 0) && - (!tokenExists(tokenId) => unsafeGetApproved(tokenId) == 0) + (!tokenExists(tokenId) => unsafeGetApproved(tokenId) == 0); /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ @@ -189,21 +192,21 @@ rule zeroAddressBalanceRevert() { └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule supplyChange(env e) { - uint256 supplyBefore = ownedTotal(); + mathint supplyBefore = ownedTotal; method f; calldataarg args; f(e, args); - uint256 supplyAfter = ownedTotal(); + mathint supplyAfter = ownedTotal; 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 +219,9 @@ rule balanceChange(env e, address account) { requireInvariant balanceOfConsistency(account); require balanceLimited(account); - uint256 balanceBefore = balanceOf(account); + mathint balanceBefore = balanceOf(account); method f; calldataarg args; f(e, args); - uint256 balanceAfter = balanceOf(account); + mathint balanceAfter = balanceOf(account); // balance can change by at most 1 assert balanceBefore != balanceAfter => ( @@ -228,13 +231,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 ); } @@ -249,19 +252,19 @@ rule ownershipChange(env e, uint256 tokenId) { 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 ); } @@ -277,13 +280,13 @@ rule approvalChange(env e, uint256 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 ) ); @@ -299,7 +302,7 @@ rule approvedForAllChange(env e, address owner, address spender) { method f; calldataarg args; f(e, args); 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 +312,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 +342,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 +360,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 +393,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 +419,7 @@ rule mint(env e, address to, uint256 tokenId) { require balanceLimited(to); - uint256 supplyBefore = ownedTotal(); + mathint supplyBefore = ownedTotal; uint256 balanceOfToBefore = balanceOf(to); uint256 balanceOfOtherBefore = balanceOf(otherAccount); address ownerBefore = unsafeOwnerOf(tokenId); @@ -431,9 +436,9 @@ rule mint(env e, address to, uint256 tokenId) { // effect assert success => ( - ownedTotal() == supplyBefore + 1 && - balanceOf(to) == balanceOfToBefore + 1 && - unsafeOwnerOf(tokenId) == to + ownedTotal == supplyBefore + 1 && + to_mathint(balanceOf(to)) == balanceOfToBefore + 1 && + unsafeOwnerOf(tokenId) == to ); // no side effect @@ -447,8 +452,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 +463,7 @@ rule safeMint(env e, method f, address to, uint256 tokenId) filtered { f -> require balanceLimited(to); - uint256 supplyBefore = ownedTotal(); + mathint supplyBefore = ownedTotal; uint256 balanceOfToBefore = balanceOf(to); uint256 balanceOfOtherBefore = balanceOf(otherAccount); address ownerBefore = unsafeOwnerOf(tokenId); @@ -474,9 +479,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 + ownedTotal == supplyBefore + 1 && + to_mathint(balanceOf(to)) == balanceOfToBefore + 1 && + unsafeOwnerOf(tokenId) == to ); // no side effect @@ -498,7 +503,7 @@ rule burn(env e, uint256 tokenId) { requireInvariant ownerHasBalance(tokenId); - uint256 supplyBefore = ownedTotal(); + mathint supplyBefore = ownedTotal; uint256 balanceOfFromBefore = balanceOf(from); uint256 balanceOfOtherBefore = balanceOf(otherAccount); address ownerBefore = unsafeOwnerOf(tokenId); @@ -515,10 +520,10 @@ rule burn(env e, uint256 tokenId) { // effect assert success => ( - ownedTotal() == supplyBefore - 1 && - balanceOf(from) == balanceOfFromBefore - 1 && - unsafeOwnerOf(tokenId) == 0 && - unsafeGetApproved(tokenId) == 0 + ownedTotal == supplyBefore - 1 && + to_mathint(balanceOf(from)) == balanceOfFromBefore - 1 && + unsafeOwnerOf(tokenId) == 0 && + unsafeGetApproved(tokenId) == 0 ); // no side effect @@ -534,6 +539,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 +553,6 @@ rule approve(env e, address spender, uint256 tokenId) { // liveness assert success <=> ( owner != 0 && - owner != spender && (owner == caller || isApprovedForAll(owner, caller)) ); @@ -576,7 +581,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/methods/IERC721.spec b/certora/specs/methods/IERC721.spec index e6d4e1e04..bbe8b375e 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); +}