ERC721 properties

.gitmodules

@@ -5,7 +5,7 @@
 [submodule "lib/solmate"]
 	path = lib/solmate
 	url = https://github.com/transmissions11/solmate
-        tag = v6
+    	tag = v6
 [submodule "lib/ERC4626"]
 	path = lib/ERC4626
 	url = https://github.com/fubuloubu/ERC4626

PROPERTIES.md

@@ -12,6 +12,10 @@ This file lists all the currently implemented Echidna property tests for ERC20,
     - [Tests for mintable tokens](#tests-for-mintable-tokens)
     - [Tests for pausable tokens](#tests-for-pausable-tokens)
     - [Tests for tokens implementing `increaseAllowance` and `decreaseAllowance`](#tests-for-tokens-implementing-increaseallowance-and-decreaseallowance)
+  - [ERC721](#erc721)
+    - [Basic properties for standard functions](#basic-properties-for-standard-functions-1)
+    - [Tests for burnable tokens](#tests-for-burnable-tokens-1)
+    - [Tests for mintable tokens](#tests-for-mintable-tokens-1)
   - [ERC4626](#erc4626)
   - [ABDKMath64x64](#abdkmath64x64)
 
@@ -67,6 +71,43 @@ This file lists all the currently implemented Echidna property tests for ERC20,
 | ERC20-ALLOWANCE-001 | [test_ERC20_setAndIncreaseAllowance](https://github.com/crytic/properties/blob/main/contracts/ERC20/internal/properties/ERC20IncreaseAllowanceProperties.sol#L17) | Allowance should be updated correctly when `increaseAllowance` is called. |
 | ERC20-ALLOWANCE-002 | [test_ERC20_setAndDecreaseAllowance](https://github.com/crytic/properties/blob/main/contracts/ERC20/internal/properties/ERC20IncreaseAllowanceProperties.sol#L28) | Allowance should be updated correctly when `decreaseAllowance` is called. |
 
+# ERC721
+
+### Basic properties for standard functions
+
+| ID |  Name | Invariant tested |
+|---|---|---|
+| ERC721-BASE-001 | [test_ERC721_balanceOfZeroAddressMustRevert](https://github.com/crytic/properties/blob/main/contracts/ERC721/internal/properties/ERC721BasicProperties.sol#L13) | Calling `balanceOf` for the zero address should revert. |
+| ERC721-BASE-002 | [test_ERC721_ownerOfInvalidTokenMustRevert](https://github.com/crytic/properties/blob/main/contracts/ERC721/internal/properties/ERC721BasicProperties.sol#L19) | Calling ownerOf for an invalid token should revert. |
+| ERC721-BASE-003 | [test_ERC721_approvingInvalidTokenMustRevert](https://github.com/crytic/properties/blob/main/contracts/ERC721/internal/properties/ERC721BasicProperties.sol#L26) | `approve()` should revert on invalid token. |
+| ERC721-BASE-004 | [test_ERC721_transferFromNotApproved](https://github.com/crytic/properties/blob/main/contracts/ERC721/internal/properties/ERC721BasicProperties.sol#L33) | `transferFrom()` should revert if caller is not operator. |
+| ERC721-BASE-005 | [test_ERC721_transferFromResetApproval](https://github.com/crytic/properties/blob/main/contracts/ERC721/internal/properties/ERC721BasicProperties.sol#L51) | `transferFrom()` should reset approvals. |
+| ERC721-BASE-006 | [test_ERC721_transferFromUpdatesOwner](https://github.com/crytic/properties/blob/main/contracts/ERC721/internal/properties/ERC721BasicProperties.sol#L67) | `transferFrom()` should update the token owner. |
+| ERC721-BASE-007 | [test_ERC721_transferFromZeroAddress](https://github.com/crytic/properties/blob/main/contracts/ERC721/internal/properties/ERC721BasicProperties.sol#L81) | `transferFrom()` should revert if `from` is the zero address. |
+| ERC721-BASE-008 | [test_ERC721_transferToZeroAddress](https://github.com/crytic/properties/blob/main/contracts/ERC721/internal/properties/ERC721BasicProperties.sol#L90) | `transferFrom()` should revert if `to` is the zero address. |
+| ERC721-BASE-009 | [test_ERC721_transferFromSelf](https://github.com/crytic/properties/blob/main/contracts/ERC721/internal/properties/ERC721BasicProperties.sol#L101) | `transferFrom()` to self should not break accounting. |
+| ERC721-BASE-010 | [test_ERC721_transferFromSelfResetsApproval](https://github.com/crytic/properties/blob/main/contracts/ERC721/internal/properties/ERC721BasicProperties.sol#L115) | `transferFrom()` to self should reset approvals.  |
+| ERC721-BASE-011 | [test_ERC721_safeTransferFromRevertsOnNoncontractReceiver](https://github.com/crytic/properties/blob/main/contracts/ERC721/internal/properties/ERC721BasicProperties.sol#L128) | `safeTransferFrom()` should revert if receiver is a contract that does not implement `onERC721Received()`  |
+
+### Tests for burnable tokens
+
+| ID |  Name | Invariant tested |
+|---|---|---|
+| ERC721-BURNABLE-001 | [test_ERC721_burnReducesTotalSupply](https://github.com/crytic/properties/blob/main/contracts/ERC721/internal/properties/ERC721BurnableProperties.sol#L14) | User balance and total supply should be updated correctly when `burn` is called.   |
+| ERC721-BURNABLE-002 | [test_ERC721_burnRevertOnTransferFromPreviousOwner](https://github.com/crytic/properties/blob/main/contracts/ERC721/internal/properties/ERC721BurnableProperties.sol#L29) | A token that has been burned cannot be transferred.   |
+| ERC721-BURNABLE-003 | [test_ERC721_burnRevertOnTransferFromZeroAddress](https://github.com/crytic/properties/blob/main/contracts/ERC721/internal/properties/ERC721BurnableProperties.sol#L40) | A token that has been burned cannot be transferred.   |
+| ERC721-BURNABLE-004 | [test_ERC721_burnRevertOnApprove](https://github.com/crytic/properties/blob/main/contracts/ERC721/internal/properties/ERC721BurnableProperties.sol#L51) | A burned token should have its approvals reset.   |
+| ERC721-BURNABLE-005 | [test_ERC721_burnRevertOnGetApproved](https://github.com/crytic/properties/blob/main/contracts/ERC721/internal/properties/ERC721BurnableProperties.sol#L62) | `getApproved()` should revert if the token is burned.   |
+| ERC721-BURNABLE-006 | [test_ERC721_burnRevertOnOwnerOf](https://github.com/crytic/properties/blob/main/contracts/ERC721/internal/properties/ERC721BurnableProperties.sol#L73) | `ownerOf()` should revert if the token has been burned.  |
+
+### Tests for mintable tokens
+
+| ID |  Name | Invariant tested |
+|---|---|---|
+| ERC721-MINTABLE-001 | [test_ERC721_mintIncreasesSupply](https://github.com/crytic/properties/blob/main/contracts/ERC721/internal/properties/ERC721MintableProperties.sol#L11) | User balance and total supply should be updated correctly after minting.  |
+| ERC721-MINTABLE-002 | [test_ERC721_mintCreatesFreshToken](https://github.com/crytic/properties/blob/main/contracts/ERC721/internal/properties/ERC721MintableProperties.sol#L22) | User balance and total supply should be updated correctly after minting.  |
+
+
 ## ERC4626
 
 | ID          | Name                                                                                                                                                 | Invariant tested                                         |

README.md

@@ -4,6 +4,7 @@
 - [Properties](#properties)
   - [Testing the properties with fuzzing](#testing-the-properties-with-fuzzing)
     - [ERC20 tests](#erc20-tests)
+    - [ERC721 Tests](#erc721-tests)
     - [ERC4626 Tests](#erc4626-tests)
     - [ABDKMath64x64 tests](#abdkmath64x64-tests)
   - [Additional resources](#additional-resources)
@@ -22,6 +23,7 @@
 This repository contains 168 code properties for:
 
 - [ERC20](https://ethereum.org/en/developers/docs/standards/tokens/erc-20/) token: mintable, burnable, pausable and transferable invariants ([25 properties](PROPERTIES.md#erc20)).
+- [ERC721](https://ethereum.org/en/developers/docs/standards/tokens/erc-721/) token: mintable, burnable, and transferable invariants ([19 properties](PROPERTIES.md#erc721)).
 - [ERC4626](https://ethereum.org/en/developers/docs/standards/tokens/erc-4626/) vaults: strict specification and additional security invariants ([37 properties](PROPERTIES.md#erc4626)).
 - [ABDKMath64x64](https://github.com/abdk-consulting/abdk-libraries-solidity/blob/master/ABDKMath64x64.md) fixed-point library invariants ([106 properties](PROPERTIES.md#abdkmath64x64)).
 
@@ -56,9 +58,10 @@ 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 advantanges 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`:
 
@@ -189,14 +192,137 @@ Event sequence: Panic(1), AssertEqFail("Equal assertion failed. Message: Failed
 ...
 ```
 
-### ERC4626 Tests
+### ERC721 tests
 
-To test an ERC4626 token, follow these steps:
+To test an ERC721 token, follow these steps:
 
 1. [Integration](#integration-1)
 2. [Configuration](#configuration-1)
 3. [Run](#run-1)
 
+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). 
+
+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";
+import "./MyToken.sol";
+contract CryticERC721InternalHarness is MyToken, CryticERC721BasicProperties {
+
+    constructor() {
+    }
+}
+```
+
+For external testing, create two contracts: the `CryticERC721ExternalHarness` and the `TokenMock` as shown below.
+In the `CryticERC721ExternalHarness` contract you can specify which properties to test, via inheritance. In the `TokenMock` contract, you will need to modify the `isMintableOrBurnable` variable if your contract is able to mint or burn tokens.
+
+```Solidity
+pragma solidity ^0.8.0;
+import "./MyToken.sol";
+import {ITokenMock} from "@crytic/properties/contracts/ERC721/external/util/ITokenMock.sol";
+import {CryticERC721ExternalBasicProperties} from "@crytic/properties/contracts/ERC721/external/properties/ERC721ExternalBasicProperties.sol";
+import {PropertiesConstants} from "@crytic/properties/contracts/util/PropertiesConstants.sol";
+
+
+contract CryticERC721ExternalHarness is CryticERC721ExternalBasicProperties {   
+    constructor() {
+        // Deploy ERC721
+        token = ITokenMock(address(new CryticTokenMock()));
+    }
+}
+
+contract CryticTokenMock is MyToken, PropertiesConstants {
+
+    bool public isMintableOrBurnable;
+
+    constructor () {
+        isMintableOrBurnable = true;
+    }
+}
+```
+
+#### Configuration
+Create the following Echidna config file
+
+```yaml
+corpusDir: "tests/crytic/erc721/echidna-corpus-internal"
+testMode: assertion
+testLimit: 100000
+deployer: "0x10000"
+sender: ["0x10000", "0x20000", "0x30000"]
+```
+
+If you're using external testing, you will also need to specify:
+
+```yaml
+multi-abi: 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. 
+
+#### Run
+Run Echidna: 
+- For internal testing: `echidna-test . --contract CryticERC721InternalHarness --config tests/crytic/erc721/echidna-internal.yaml` 
+- For external testing: `echidna-test . --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-test . --contract CryticERC721InternalHarness --config tests/echidna.config.yaml 
+Loaded total of 23 transactions from corpus/coverage
+Analyzing contract: contracts/ERC721/CryticERC721InternalHarness.sol:CryticERC721InternalHarness
+name():  passed! 🎉
+test_ERC721_external_transferFromNotApproved():  passed! 🎉
+approve(address,uint256):  passed! 🎉
+test_ERC721_external_transferFromUpdatesOwner():  passed! 🎉
+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-test . --contract CryticERC721ExternalHarness --config tests/echidna.config.yaml
+Loaded total of 25 transactions from corpus/coverage
+Analyzing contract: contracts/ERC721/CryticERC721ExternalHarness.sol:CryticERC721ExternalHarness
+name():  passed! 🎉
+test_ERC721_external_transferFromUpdatesOwner():  passed! 🎉
+approve(address,uint256):  passed! 🎉
+...
+test_ERC721_external_balanceOfZeroAddressMustRevert(): failed!💥  
+  Call sequence:
+    test_ERC721_external_balanceOfZeroAddressMustRevert()
+
+Event sequence: Panic(1), AssertFail("address(0) balance query should have reverted") from: ERC721PropertyTests@0x00a329c0648769A73afAc7F9381E08FB43dBEA72
+...
+```
+
+### 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`):
@@ -267,8 +393,9 @@ ABDKMath64x64 library implements [19 arithmetic operations](https://github.com/a
 
 We provide a number of tests related with fundamental mathematical properties of the floating point numbers. To include these tests into your repository, follow these steps:
 
-1. [Integration](#integration-2)
-2. [Run](#run-2)
+1. [Integration](#integration-3)
+2. [Run](#run-3)
+
 
 #### Integration
 

contracts/ERC4626/test/Solmate4626.sol

@@ -29,6 +29,6 @@ contract TestHarness is CryticERC4626PropertyTests {
     constructor() {
         TestERC20Token _asset = new TestERC20Token("Test Token", "TT", 18);
         ERC4626 _vault = new Solmate4626(ERC20(address(_asset)));
-        initialize(address(_vault), address(_asset));
+        initialize(address(_vault), address(_asset), false);
     }
 }