Partially finish ERC721

certora/diff/token_ERC721_ERC721.sol.patch

@@ -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.
-      *

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) {

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)
-
-    tokenExists(uint256) returns (bool) envfree
-    unsafeOwnerOf(uint256) returns (address) envfree
-    unsafeGetApproved(uint256) returns (address) envfree
+    function mint(address,uint256) external;
+    function safeMint(address,uint256) external;
+    function safeMint(address,uint256,bytes) external;
+    function burn(uint256) external;
+
+    function 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;

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);
 }

certora/specs/methods/IERC721Receiver.spec

@@ -0,0 +1,3 @@
+methods {
+  function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true);
+}