Fix #56: Remove redundant usedId from ERC721 implementation

The usedId mapping was declared but never properly utilized. Since the
counter++ mechanism already ensures unique token IDs are minted, usedId
was redundant and has been removed.

Changes:
- Remove usedId from IERC721Internal interface
- Remove usedId mapping from ERC721Compliant
- Remove usedId mapping from ERC721IncorrectMintable
- Remove usedId assertion from ERC721ExternalMintableProperties
- Update README to fix interface name (ITokenMock -> IERC721Internal)
  and remove usedId references from example code

Author: nisedo

README.md

@@ -73,10 +73,9 @@ To test an ERC20 token, follow these steps:
 
 You can see the output for a [compliant token](#example-output-for-a-compliant-token), and [non compliant token](#example-output-for-a-non-compliant-token).
 
-
 #### Integration
 
-Decide if you want to do internal or external testing. Both approaches have advantages and disadvantages, you can check more information about them [here](https://secure-contracts.com/program-analysis/echidna/basic/common-testing-approaches.html). 
+Decide if you want to do internal or external testing. Both approaches have advantages and disadvantages, you can check more information about them [here](https://secure-contracts.com/program-analysis/echidna/basic/common-testing-approaches.html).
 
 For internal testing, create a new Solidity file containing the `CryticERC20InternalHarness` contract. `USER1`, `USER2` and `USER3` constants are initialized by default in `PropertiesConstants` contract to be the addresses from where echidna sends transactions, and `INITIAL_BALANCE` is by default `1000e18`:
 
@@ -147,44 +146,40 @@ sender: ["0x10000", "0x20000", "0x30000"]
 #allContracts: true
 ```
 
-**Medusa** 
+**Medusa**
 
 Create the following Medusa config file:
 
 ```json
 {
-	"fuzzing": {
+  "fuzzing": {
     "testLimit": 100000,
-		"corpusDirectory": "tests/medusa-corpus",
-		"deployerAddress": "0x10000",
-		"senderAddresses": [
-			"0x10000",
-			"0x20000",
-			"0x30000"
-		],
-		"assertionTesting": {
-			"enabled": true
-		},
-		"propertyTesting": {
-			"enabled": false
-		},
+    "corpusDirectory": "tests/medusa-corpus",
+    "deployerAddress": "0x10000",
+    "senderAddresses": ["0x10000", "0x20000", "0x30000"],
+    "assertionTesting": {
+      "enabled": true
+    },
+    "propertyTesting": {
+      "enabled": false
+    },
     "optimizationTesting": {
-				"enabled": false,
-		},
-	},
-// Uncomment the following lines for external testing
-//		"testing": {
-//			"testAllContracts": true
-//    },
-	"compilation": {
-		"platform": "crytic-compile",
-		"platformConfig": {
-			"target": ".",
-			"solcVersion": "",
-			"exportDirectory": "",
-			"args": ["--foundry-compile-all"]
-		}
-	}
+      "enabled": false
+    }
+  },
+  // Uncomment the following lines for external testing
+  //		"testing": {
+  //			"testAllContracts": true
+  //    },
+  "compilation": {
+    "platform": "crytic-compile",
+    "platformConfig": {
+      "target": ".",
+      "solcVersion": "",
+      "exportDirectory": "",
+      "args": ["--foundry-compile-all"]
+    }
+  }
 }
 ```
 
@@ -260,11 +255,12 @@ To test an ERC721 token, follow these steps:
 
 You can see the output for a [compliant token](#example-output-for-a-compliant-token-1), and [non compliant token](#example-output-for-a-non-compliant-token-1).
 
-
 #### Integration
-Decide if you want to do internal or external testing. Both approaches have advantages and disadvantages, you can check more information about them [here](https://secure-contracts.com/program-analysis/echidna/basic/common-testing-approaches.html). 
+
+Decide if you want to do internal or external testing. Both approaches have advantages and disadvantages, you can check more information about them [here](https://secure-contracts.com/program-analysis/echidna/basic/common-testing-approaches.html).
 
 For internal testing, create a new Solidity file containing the `CryticERC721InternalHarness` contract. `USER1`, `USER2` and `USER3` constants are initialized by default in `PropertiesConstants` contract to be the addresses from where echidna sends transactions.
+
 ```Solidity
 pragma solidity ^0.8.0;
 import "@crytic/properties/contracts/ERC721/internal/properties/ERC721BasicProperties.sol";
@@ -287,7 +283,7 @@ import {CryticERC721ExternalBasicProperties} from "@crytic/properties/contracts/
 import {PropertiesConstants} from "@crytic/properties/contracts/util/PropertiesConstants.sol";
 
 
-contract CryticERC721ExternalHarness is CryticERC721ExternalBasicProperties {   
+contract CryticERC721ExternalHarness is CryticERC721ExternalBasicProperties {
     constructor() {
         // Deploy ERC721
         token = ITokenMock(address(new CryticTokenMock()));
@@ -301,10 +297,24 @@ contract CryticTokenMock is MyToken, PropertiesConstants {
     constructor () {
         isMintableOrBurnable = true;
     }
+<<<<<<< Updated upstream
+=======
+
+    function burn(uint256 tokenId) public {
+        _burn(tokenId);
+    }
+
+    function _customMint(address to, uint256 amount) public {
+        for (uint256 i; i < amount; i++) {
+            _mint(to, counter++);
+        }
+    }
+>>>>>>> Stashed changes
 }
 ```
 
 #### Configuration
+
 Create the following Echidna config file
 
 ```yaml
@@ -323,20 +333,23 @@ allContracts: true
 
 To perform more than one test, save the files with a descriptive path, to identify what test each file or corpus belongs to. For these examples, we use `tests/crytic/erc721/echidna-internal.yaml` and `tests/crytic/erc721/echidna-external.yaml` for the Echidna tests for ERC721. We recommended to modify the `corpusDir` for external tests accordingly.
 
-The above configuration will start Echidna in assertion mode. Contract will be deployed from address `0x10000`, and transactions will be sent from the owner and two different users (`0x20000` and `0x30000`). There is an initial limit of `100000` tests, but depending on the token code complexity, this can be increased. Finally, once Echidna finishes the fuzzing campaign, corpus and coverage results will be available in the `tests/crytic/erc721/echidna-corpus-internal` directory. 
+The above configuration will start Echidna in assertion mode. Contract will be deployed from address `0x10000`, and transactions will be sent from the owner and two different users (`0x20000` and `0x30000`). There is an initial limit of `100000` tests, but depending on the token code complexity, this can be increased. Finally, once Echidna finishes the fuzzing campaign, corpus and coverage results will be available in the `tests/crytic/erc721/echidna-corpus-internal` directory.
 
 #### Run
-Run Echidna: 
-- For internal testing: `echidna . --contract CryticERC721InternalHarness --config tests/crytic/erc721/echidna-internal.yaml` 
-- For external testing: `echidna . --contract CryticERC721ExternalHarness --config tests/crytic/erc721/echidna-external.yaml` 
-  
+
+Run Echidna:
+
+- For internal testing: `echidna . --contract CryticERC721InternalHarness --config tests/crytic/erc721/echidna-internal.yaml`
+- For external testing: `echidna . --contract CryticERC721ExternalHarness --config tests/crytic/erc721/echidna-external.yaml`
+
 Finally, inspect the coverage report in `tests/crytic/erc721/echidna-corpus-internal` or `tests/crytic/erc721/echidna-corpus-external` when it finishes.
 
 #### Example: Output for a compliant token
 
 If the token under test is compliant and no properties will fail during fuzzing, the Echidna output should be similar to the screen below:
+
 ```
-$ echidna . --contract CryticERC721InternalHarness --config tests/echidna.config.yaml 
+$ echidna . --contract CryticERC721InternalHarness --config tests/echidna.config.yaml
 Loaded total of 23 transactions from corpus/coverage
 Analyzing contract: contracts/ERC721/CryticERC721InternalHarness.sol:CryticERC721InternalHarness
 name():  passed! 🎉
@@ -350,13 +363,15 @@ totalSupply():  passed! 🎉
 #### Example: Output for a non-compliant token
 
 For this example, the ExampleToken's balanceOf function was modified so it does not check that `owner` is the zero address:
+
 ```
 function balanceOf(address owner) public view virtual override returns (uint256) {
     return _balances[owner];
 }
 ```
 
 In this case, the Echidna output should be similar to the screen below, notice that all functions that rely on `balanceOf()` to work correctly will have their assertions broken, and will report the situation.
+
 ```
 $ echidna . --contract CryticERC721ExternalHarness --config tests/echidna.config.yaml
 Loaded total of 25 transactions from corpus/coverage
@@ -365,7 +380,7 @@ name():  passed! 🎉
 test_ERC721_external_transferFromUpdatesOwner():  passed! 🎉
 approve(address,uint256):  passed! 🎉
 ...
-test_ERC721_external_balanceOfZeroAddressMustRevert(): failed!💥  
+test_ERC721_external_balanceOfZeroAddressMustRevert(): failed!💥
   Call sequence:
     test_ERC721_external_balanceOfZeroAddressMustRevert()
 
@@ -376,11 +391,11 @@ Event sequence: Panic(1), AssertFail("address(0) balance query should have rever
 ### ERC4626 Tests
 
 To test an ERC4626 token, follow these steps:
+
 1. [Integration](#integration-2)
 2. [Configuration](#configuration-2)
 3. [Run](#run-2)
 
-
 #### Integration
 
 Create a new Solidity file containing the `CryticERC4626Harness` contract. Make sure it properly initializes your ERC4626 vault with a test token (`TestERC20Token`):
@@ -454,7 +469,6 @@ We provide a number of tests related with fundamental mathematical properties of
 1. [Integration](#integration-3)
 2. [Run](#run-3)
 
-
 #### Integration
 
 Create a new Solidity file containing the `ABDKMath64x64Harness` contract:

contracts/ERC721/external/properties/ERC721ExternalMintableProperties.sol

@@ -3,36 +3,59 @@ pragma solidity ^0.8.13;
 
 import "../util/ERC721ExternalTestBase.sol";
 
-abstract contract CryticERC721ExternalMintableProperties is CryticERC721ExternalTestBase {
+abstract contract CryticERC721ExternalMintableProperties is
+    CryticERC721ExternalTestBase
+{
     using Address for address;
 
     ////////////////////////////////////////
     // Properties
     // mint increases the total supply.
-    function test_ERC721_external_mintIncreasesSupply(uint256 amount) public virtual {
+    function test_ERC721_external_mintIncreasesSupply(
+        uint256 amount
+    ) public virtual {
         require(token.isMintableOrBurnable());
-        
+
         uint256 selfBalance = token.balanceOf(address(this));
         uint256 oldTotalSupply = token.totalSupply();
 
         try token._customMint(address(this), amount) {
-            assertEq(oldTotalSupply + amount, token.totalSupply(), "Total supply was not correctly increased");
-            assertEq(selfBalance + amount, token.balanceOf(address(this)), "Receiver supply was not correctly increased");
+            assertEq(
+                oldTotalSupply + amount,
+                token.totalSupply(),
+                "Total supply was not correctly increased"
+            );
+            assertEq(
+                selfBalance + amount,
+                token.balanceOf(address(this)),
+                "Receiver supply was not correctly increased"
+            );
         } catch {
             assertWithMsg(false, "Minting unexpectedly reverted");
         }
     }
 
     // mint creates a fresh token.
-    function test_ERC721_external_mintCreatesFreshToken(uint256 amount) public virtual {
+    function test_ERC721_external_mintCreatesFreshToken(
+        uint256 amount
+    ) public virtual {
         require(token.isMintableOrBurnable());
 
         uint256 selfBalance = token.balanceOf(address(this));
         try token._customMint(address(this), amount) {
-            uint256 tokenId = token.tokenOfOwnerByIndex(address(this), selfBalance);
-            assertWithMsg(token.ownerOf(tokenId) == address(this), "Token ID was not minted to receiver");
-            assertWithMsg(!token.usedId(tokenId), "Token ID minted is not new");
-            assertEq(selfBalance + amount, token.balanceOf(address(this)), "Receiver supply was not correctly increased");
+            uint256 tokenId = token.tokenOfOwnerByIndex(
+                address(this),
+                selfBalance
+            );
+            assertWithMsg(
+                token.ownerOf(tokenId) == address(this),
+                "Token ID was not minted to receiver"
+            );
+            assertEq(
+                selfBalance + amount,
+                token.balanceOf(address(this)),
+                "Receiver supply was not correctly increased"
+            );
         } catch {
             assertWithMsg(false, "Minting unexpectedly reverted");
         }

contracts/ERC721/external/test/ERC721Compliant.sol

@@ -6,12 +6,10 @@ import "@openzeppelin/contracts/token/ERC721/extensions/ERC721Enumerable.sol";
 import {IERC721Internal} from "../../util/IERC721Internal.sol";
 
 contract ERC721Compliant is ERC721, ERC721Enumerable, IERC721Internal {
-    
     uint256 public counter;
     bool public isMintableOrBurnable;
-    mapping(uint256 => bool) public usedId;
 
-    constructor() ERC721("OZERC721","OZ") {
+    constructor() ERC721("OZERC721", "OZ") {
         isMintableOrBurnable = true;
     }
 
@@ -20,21 +18,24 @@ contract ERC721Compliant is ERC721, ERC721Enumerable, IERC721Internal {
     }
 
     function _customMint(address to, uint256 amount) public virtual {
-        for(uint256 i; i < amount; i++) {
+        for (uint256 i; i < amount; i++) {
             _mint(to, counter++);
         }
     }
-    
+
     // The following functions are overrides required by Solidity.
-    function _beforeTokenTransfer(address from, address to, uint256 tokenId, uint256 batchSize)
-        internal
-        virtual
-        override(ERC721, ERC721Enumerable)
-    {
+    function _beforeTokenTransfer(
+        address from,
+        address to,
+        uint256 tokenId,
+        uint256 batchSize
+    ) internal virtual override(ERC721, ERC721Enumerable) {
         super._beforeTokenTransfer(from, to, tokenId, batchSize);
     }
 
-    function supportsInterface(bytes4 interfaceId)
+    function supportsInterface(
+        bytes4 interfaceId
+    )
         public
         view
         virtual
@@ -43,4 +44,4 @@ contract ERC721Compliant is ERC721, ERC721Enumerable, IERC721Internal {
     {
         return super.supportsInterface(interfaceId);
     }
-}
+}