crytic
`usedId` purpose in `ERC721`
In the IERC721Internal interface you define the following function usedId:
function usedId(uint256 tokenId) external view returns (bool);
I'm having a hard time to understand what is the reason behind using this as part of the interface. In your ERC721Compliant contract, you declare it but not use it:
https://github.com/crytic/properties/blob/58fcb6fd856b1d9a9b970cb366ee841baafed6f2/contracts/ERC721/external/test/ERC721Compliant.sol#L11
If someone adds something like usedId[id] = true to the _customMint function, the following property always fails obviously: https://github.com/crytic/properties/blob/58fcb6fd856b1d9a9b970cb366ee841baafed6f2/contracts/ERC721/external/properties/ERC721ExternalMintableProperties.sol#L33
If you want to track the used ids, you should update it after the above test assertion to make sense.
Furthermore, the README section on the ERC721 is outdated. There is no ITokenMock in the ERC721 case for example, but IERC721Internal. I would recommend making it consistent with the ERC20 example tho & updating the docs about the latest status quo.
Hey @pcaversaccio , appreciate you opening an issue. I think usedId was just to facilitate checking that the same tokenId cannot be minted more than once, but it might not have been implemented fully/properly. Good point on the README being outdated, I can probably get to fixing this sometime next week.
