💥 Add echidna-Based Property Tests (#239)

### 🕓 Changelog This PR adds the `echidna`-based [property](https://github.com/crytic/properties) tests for the `ERC20` and `ERC721` contracts (closes #184). The `ERC4626` properties are not integrated as they are already covered by [`erc4626-tests`](https://github.com/a16z/erc4626-tests). Please note that [`hevm`](https://github.com/ethereum/hevm) doesn't strip whitespace characters (!) and since Foundry doesn't easily allow for piping of commands, I wrote a Python scripts [`compile.py`](https://github.com/pcaversaccio/snekmate/blob/feat/echidna/lib/utils/compile.py) that strips away all whitespace characters. --------- Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
pcaversaccio · Apr 25, 2024 · afcf7cc · afcf7cc
1 parent a070840
commit afcf7cc
Show file tree

Hide file tree

Showing 21 changed files with 566 additions and 308 deletions.
diff --git a/.gas-snapshot b/.gas-snapshot
diff --git a/.github/workflows/checks.yml b/.github/workflows/checks.yml
@@ -15,6 +15,8 @@ jobs:
           - ubuntu-latest
         architecture:
           - x64
+        python_version:
+          - 3.11
         node_version:
           - 20
 
@@ -52,6 +54,18 @@ jobs:
       - name: Prettier and lint
         run: pnpm lint:check
 
+      - name: Setup Python
+        uses: actions/setup-python@v5
+        with:
+          python-version: ${{ matrix.python_version }}
+          architecture: ${{ matrix.architecture }}
+
+      - name: Check formatting with Black
+        uses: psf/black@stable
+        with:
+          options: "--check --verbose"
+          src: "./lib/utils"
+
   codespell:
     runs-on: ${{ matrix.os }}
     strategy:
@@ -94,6 +108,6 @@ jobs:
       - name: Validate URLs
         run: |
           awesome_bot ./*.md src/snekmate/**/*.vy src/snekmate/**/mocks/*.vy src/snekmate/**/interfaces/*.vyi \
-          test/**/*.sol test/**/interfaces/*.sol test/**/mocks/*.sol test/**/scripts/*.js \
+          test/**/*.sol test/**/interfaces/*.sol test/**/mocks/*.sol test/**/scripts/*.js lib/utils/*.py \
           --allow-dupe --allow-redirect --request-delay 0.4 \
           --white-list https://www.wagmi.xyz,https://github.com/pcaversaccio/snekmate.git@,https://github.com/pcaversaccio/snekmate/releases/tag/v0.1.0,https://github.com/pcaversaccio/snekmate/blob/v0.1.0,https://github.com/pcaversaccio/snekmate/compare/v0.0.5...v0.1.0
diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml
@@ -17,6 +17,7 @@ jobs:
           - ubuntu-latest
         language:
           - javascript-typescript
+          - python
 
     steps:
       - name: Checkout

diff --git a/.github/workflows/test-contracts.yml b/.github/workflows/test-contracts.yml
@@ -94,6 +94,23 @@ jobs:
           FOUNDRY_PROFILE: default
 
       - name: Run snapshot
-        run: NO_COLOR=1 forge snapshot >> $GITHUB_STEP_SUMMARY
+        run: NO_COLOR=1 forge snapshot --build-info >> $GITHUB_STEP_SUMMARY
         env:
           FOUNDRY_PROFILE: default
+
+      - name: Install Homebrew
+        uses: Homebrew/actions/setup-homebrew@master
+
+      - name: Install Echidna
+        run: brew install echidna
+
+      - name: Show the Echidna version
+        run: echidna --version
+
+      - name: Run Echidna ERC-20 property tests
+        run: |
+          echidna test/tokens/echidna/ERC20Properties.sol --contract CryticERC20ExternalHarness --config test/tokens/echidna/echidna-config.yaml --crytic-args --ignore-compile
+
+      - name: Run Echidna ERC-721 property tests
+        run: |
+          echidna test/tokens/echidna/ERC721Properties.sol --contract CryticERC721ExternalHarness --config test/tokens/echidna/echidna-config.yaml --crytic-args --ignore-compile
diff --git a/.gitignore b/.gitignore
@@ -60,3 +60,7 @@ dist
 
 # Ape build files
 .build
+
+# Echidna files
+echidna-corpus
+crytic-export
diff --git a/.gitmodules b/.gitmodules
@@ -13,6 +13,9 @@
 [submodule "lib/forge-std"]
 	path = lib/forge-std
 	url = https://github.com/foundry-rs/forge-std.git
+[submodule "lib/properties"]
+	path = lib/properties
+	url = https://github.com/crytic/properties.git
 [submodule "lib/create-util"]
 	path = lib/create-util
 	url = https://github.com/pcaversaccio/create-util.git

diff --git a/.prettierignore b/.prettierignore
@@ -4,10 +4,13 @@ lib/solady
 lib/solmate
 lib/prb-test
 lib/forge-std
+lib/properties
 lib/create-util
 lib/erc4626-tests
 lib/solidity-bytes-utils
 lib/openzeppelin-contracts
+echidna-corpus
+crytic-export
 cache
 out
 dist

diff --git a/.solhintignore b/.solhintignore
@@ -4,10 +4,13 @@ lib/solady
 lib/solmate
 lib/prb-test
 lib/forge-std
+lib/properties
 lib/create-util
 lib/erc4626-tests
 lib/solidity-bytes-utils
 lib/openzeppelin-contracts
+echidna-corpus
+crytic-export
 cache
 out
 dist

diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -1,6 +1,6 @@
 # 🕓 Changelog
 
-## [`0.1.0`](https://github.com/pcaversaccio/snekmate/releases/tag/v0.0.1) (Unreleased)
+## [`0.1.0`](https://github.com/pcaversaccio/snekmate/releases/tag/v0.1.0) (Unreleased)
 
 ### ♻️ Refactoring
 
@@ -31,6 +31,12 @@
 - **Vyper Contract Deployer**
   - [`VyperDeployer`](https://github.com/pcaversaccio/snekmate/blob/v0.1.0/lib/utils/VyperDeployer.sol): Improve error message in the event of a Vyper compilation error. ([#219](https://github.com/pcaversaccio/snekmate/pull/219))
 
+### 🥢 Test Coverage
+
+- **Tokens**
+  - [`ERC20`](https://github.com/pcaversaccio/snekmate/blob/v0.1.0/src/snekmate/tokens/ERC20.vy): Add `echidna`-based `ERC20` property tests. ([#239](https://github.com/pcaversaccio/snekmate/pull/239))
+  - [`ERC721`](https://github.com/pcaversaccio/snekmate/blob/v0.1.0/src/snekmate/tokens/ERC721.vy): Add `echidna`-based `ERC721` property tests. ([#239](https://github.com/pcaversaccio/snekmate/pull/239))
+
 ### 👀 Full Changelog
 
 - [`v0.0.5...v0.1.0`](https://github.com/pcaversaccio/snekmate/compare/v0.0.5...v0.1.0)

diff --git a/README.md b/README.md
@@ -100,7 +100,8 @@ You can install 🐍 snekmate via submodules using [Foundry](https://github.com/
 forge install pcaversaccio/snekmate
 ```
 
-> If you want to leverage 🐍 snekmate's [`VyperDeployer`](./lib/utils/VyperDeployer.sol) contract for your own testing, ensure that you compile the Vyper contracts with the same EVM version as configured in your `foundry.toml` file. The [`VyperDeployer`](./lib/utils/VyperDeployer.sol) contract offers two overloaded `deployContract` functions that allow the configuration of the target EVM version. Please note that since Vyper version [`0.3.8`](https://github.com/vyperlang/vyper/releases/tag/v0.3.8) the default EVM version is set to `shanghai`.
+> [!NOTE]
+> If you want to leverage 🐍 snekmate's [`VyperDeployer`](./lib/utils/VyperDeployer.sol) contract for your own testing, ensure that you compile the Vyper contracts with the same EVM version as configured in your `foundry.toml` file. The [`VyperDeployer`](./lib/utils/VyperDeployer.sol) contract offers two overloaded `deployContract` functions that allow the configuration of the target EVM version. Please note that since Vyper version [`0.3.8`](https://github.com/vyperlang/vyper/releases/tag/v0.3.8) the default EVM version is set to `shanghai`. Furthermore, the [`VyperDeployer`](./lib/utils/VyperDeployer.sol) contract relies on the Python script [`compile.py`](./lib/utils/compile.py) for successful compilation and deployment. Always use the [`VyperDeployer`](./lib/utils/VyperDeployer.sol) contract alongside with the aforementioned script.
 
 ### 2️⃣ PyPI
 
@@ -167,6 +168,21 @@ This repository contains [Foundry](https://github.com/foundry-rs/foundry)-based
 
 ✅ Test Type Implemented &emsp; ❌ Test Type Not Implemented
 
+Furthermore, the [`echidna`](https://github.com/crytic/echidna)-based [property](https://github.com/crytic/properties) tests for the [`ERC20`](./src/snekmate/tokens/ERC20.vy) and [`ERC721`](./src/snekmate/tokens/ERC721.vy) contracts are available in the [`test/tokens/echidna/`](./test/tokens/echidna) directory. You can run the tests by invoking:
+
+```console
+echidna test/tokens/echidna/ERC20Properties.sol --contract CryticERC20ExternalHarness --config test/tokens/echidna/echidna-config.yaml --crytic-args --ignore-compile
+```
+
+and
+
+```console
+echidna test/tokens/echidna/ERC721Properties.sol --contract CryticERC721ExternalHarness --config test/tokens/echidna/echidna-config.yaml --crytic-args --ignore-compile
+```
+
+> [!TIP]
+> If you encounter any issues, please ensure that you have the latest Vyper version installed locally.
+
 ## 🙏🏼 Acknowledgements
 
 This repository is inspired by or directly modified from many sources, primarily:

diff --git a/eslint.config.js b/eslint.config.js
@@ -19,10 +19,13 @@ module.exports = [
       "lib/solmate/**",
       "lib/prb-test/**",
       "lib/forge-std/**",
+      "lib/properties/**",
       "lib/create-util/**",
       "lib/erc4626-tests/**",
       "lib/solidity-bytes-utils/**",
       "lib/openzeppelin-contracts/**",
+      "echidna-corpus/**",
+      "crytic-export/**",
       "cache/**",
       "out/**",
       "dist/**",

diff --git a/foundry.toml b/foundry.toml
@@ -14,6 +14,7 @@ verbosity = 3                                               # the verbosity of t
 fs_permissions = [{ access = "read-write", path = "./"}]    # set read-write access to project root
 solc_version = '0.8.25'                                     # override for the solc version
 evm_version = 'shanghai'                                    # set the EVM target version
+no_match_path = 'test/tokens/echidna/**/*'                  # only run tests in test directory that do not match the specified glob pattern
 
 ## default overrides for the CI runs
 [profile.ci]

diff --git a/lib/properties b/lib/properties
diff --git a/lib/utils/VyperDeployer.sol b/lib/utils/VyperDeployer.sol
@@ -65,9 +65,10 @@ contract VyperDeployer is Create {
          * @dev Create a list of strings with the commands necessary
          * to compile Vyper contracts.
          */
-        string[] memory cmds = new string[](2);
-        cmds[0] = "vyper";
-        cmds[1] = string.concat(path, fileName, ".vy");
+        string[] memory cmds = new string[](3);
+        cmds[0] = "python";
+        cmds[1] = "lib/utils/compile.py";
+        cmds[2] = string.concat(path, fileName, ".vy");
 
         /**
          * @dev Compile the Vyper contract and return the bytecode.
@@ -122,9 +123,10 @@ contract VyperDeployer is Create {
          * @dev Create a list of strings with the commands necessary
          * to compile Vyper contracts.
          */
-        string[] memory cmds = new string[](2);
-        cmds[0] = "vyper";
-        cmds[1] = string.concat(path, fileName, ".vy");
+        string[] memory cmds = new string[](3);
+        cmds[0] = "python";
+        cmds[1] = "lib/utils/compile.py";
+        cmds[2] = string.concat(path, fileName, ".vy");
 
         /**
          * @dev Compile the Vyper contract and return the bytecode.
@@ -187,11 +189,12 @@ contract VyperDeployer is Create {
          * @dev Create a list of strings with the commands necessary
          * to compile Vyper contracts.
          */
-        string[] memory cmds = new string[](4);
-        cmds[0] = "vyper";
-        cmds[1] = string.concat(path, fileName, ".vy");
-        cmds[2] = "--evm-version";
-        cmds[3] = evmVersion;
+        string[] memory cmds = new string[](5);
+        cmds[0] = "python";
+        cmds[1] = "lib/utils/compile.py";
+        cmds[2] = string.concat(path, fileName, ".vy");
+        cmds[3] = "--evm-version";
+        cmds[4] = evmVersion;
 
         /**
          * @dev Compile the Vyper contract and return the bytecode.
@@ -252,11 +255,12 @@ contract VyperDeployer is Create {
          * @dev Create a list of strings with the commands necessary
          * to compile Vyper contracts.
          */
-        string[] memory cmds = new string[](4);
-        cmds[0] = "vyper";
-        cmds[1] = string.concat(path, fileName, ".vy");
-        cmds[2] = "--evm-version";
-        cmds[3] = evmVersion;
+        string[] memory cmds = new string[](5);
+        cmds[0] = "python";
+        cmds[1] = "lib/utils/compile.py";
+        cmds[2] = string.concat(path, fileName, ".vy");
+        cmds[3] = "--evm-version";
+        cmds[4] = evmVersion;
 
         /**
          * @dev Compile the Vyper contract and return the bytecode.

diff --git a/lib/utils/compile.py b/lib/utils/compile.py
@@ -0,0 +1,9 @@
+import sys, subprocess
+
+result = subprocess.run(["vyper"] + sys.argv[1:], capture_output=True, text=True)
+if result.returncode != 0:
+    raise Exception("Error compiling: " + sys.argv[1])
+
+# Remove any leading and trailing whitespace characters
+# from the compilation result.
+sys.stdout.write(result.stdout.strip())
diff --git a/remappings.txt b/remappings.txt
@@ -5,6 +5,7 @@ solmate/=lib/solmate/src/
 prb/test/=lib/prb-test/src/
 forge-std/=lib/forge-std/src/
 erc4626-tests/=lib/erc4626-tests/
+properties/=lib/properties/contracts/
 create-util/=lib/create-util/contracts/
 openzeppelin/=lib/openzeppelin-contracts/contracts/
 solidity-bytes-utils/=lib/solidity-bytes-utils/contracts/
diff --git a/src/snekmate/tokens/mocks/ERC20Mock.vy b/src/snekmate/tokens/mocks/ERC20Mock.vy
@@ -60,6 +60,12 @@ initializes: erc20[ownable := ow]
 exports: erc20.__interface__
 
 
+# @dev The following two parameters are required for the Echidna
+# fuzzing test integration: https://github.com/crytic/properties.
+isMintableOrBurnable: public(constant(bool)) = True
+initialSupply: public(uint256)
+
+
 @deploy
 @payable
 def __init__(name_: String[25], symbol_: String[5], decimals_: uint8, initial_supply_: uint256, name_eip712_: String[50], version_eip712_: String[20]):
@@ -92,3 +98,26 @@ def __init__(name_: String[25], symbol_: String[5], decimals_: uint8, initial_su
     # supply to the `msg.sender`, which takes the
     # underlying `decimals` value into account.
     erc20._mint(msg.sender, initial_supply_ * 10 ** convert(decimals_, uint256))
+
+    # We assign the initial token supply required by
+    # the Echidna external harness contract.
+    self.initialSupply = erc20.totalSupply
+
+
+# @dev Duplicate implementation of the `external` function
+# `burn_from` to enable the Echidna tests for the external
+# burnable properties.
+@external
+def burnFrom(owner: address, amount: uint256):
+    """
+    @dev Destroys `amount` tokens from `owner`,
+         deducting from the caller's allowance.
+    @notice Note that `owner` cannot be the
+            zero address. Also, the caller must
+            have an allowance for `owner`'s tokens
+            of at least `amount`.
+    @param owner The 20-byte owner address.
+    @param amount The 32-byte token amount to be destroyed.
+    """
+    erc20._spend_allowance(owner, msg.sender, amount)
+    erc20._burn(owner, amount)
diff --git a/src/snekmate/tokens/mocks/ERC721Mock.vy b/src/snekmate/tokens/mocks/ERC721Mock.vy
@@ -99,6 +99,12 @@ initializes: erc721[ownable := ow]
 exports: erc721.__interface__
 
 
+# @dev The following two parameters are required for the Echidna
+# fuzzing test integration: https://github.com/crytic/properties.
+isMintableOrBurnable: public(constant(bool)) = True
+usedId: public(HashMap[uint256, bool])
+
+
 @deploy
 @payable
 def __init__(name_: String[25], symbol_: String[5], base_uri_: String[80], name_eip712_: String[50], version_eip712_: String[20]):
@@ -125,3 +131,22 @@ def __init__(name_: String[25], symbol_: String[5], base_uri_: String[80], name_
     # to the `msg.sender`.
     ow.__init__()
     erc721.__init__(name_, symbol_, base_uri_, name_eip712_, version_eip712_)
+
+
+# @dev Custom implementation of the `external` function `safe_mint`
+# without access restriction and {IERC721Receiver-onERC721Received}
+# check to enable the Echidna tests for the external mintable properties.
+@external
+def _customMint(owner: address, amount: uint256):
+    """
+    @dev Creates `amount` tokens and assigns them to
+         `owner`, increasing the total supply.
+    @notice Note that each `token_id` must not exist
+            and `owner` cannot be the zero address.
+    @param owner The 20-byte owner address.
+    @param amount The 32-byte token amount to be created.
+    """
+    for _: uint256 in range(amount, bound=64):
+        token_id: uint256 = erc721._counter
+        erc721._counter = token_id + 1
+        erc721._mint(owner, token_id)
diff --git a/test/tokens/echidna/ERC20Properties.sol b/test/tokens/echidna/ERC20Properties.sol
@@ -0,0 +1,43 @@
+// SPDX-License-Identifier: WTFPL
+pragma solidity ^0.8.25;
+
+import {VyperDeployer} from "utils/VyperDeployer.sol";
+
+import {ITokenMock} from "properties/ERC20/external/util/ITokenMock.sol";
+
+import {CryticERC20ExternalBasicProperties} from "properties/ERC20/external/properties/ERC20ExternalBasicProperties.sol";
+import {CryticERC20ExternalBurnableProperties} from "properties/ERC20/external/properties/ERC20ExternalBurnableProperties.sol";
+import {CryticERC20ExternalMintableProperties} from "properties/ERC20/external/properties/ERC20ExternalMintableProperties.sol";
+
+contract CryticERC20ExternalHarness is
+    CryticERC20ExternalBasicProperties,
+    CryticERC20ExternalBurnableProperties,
+    CryticERC20ExternalMintableProperties
+{
+    string private constant _NAME = "MyToken";
+    string private constant _SYMBOL = "WAGMI";
+    uint8 private constant _DECIMALS = 18;
+    string private constant _NAME_EIP712 = "MyToken";
+    string private constant _VERSION_EIP712 = "1";
+    uint256 private constant _INITIAL_SUPPLY = type(uint8).max;
+
+    VyperDeployer private vyperDeployer = new VyperDeployer();
+
+    constructor() {
+        bytes memory args = abi.encode(
+            _NAME,
+            _SYMBOL,
+            _DECIMALS,
+            _INITIAL_SUPPLY,
+            _NAME_EIP712,
+            _VERSION_EIP712
+        );
+        token = ITokenMock(
+            vyperDeployer.deployContract(
+                "src/snekmate/tokens/mocks/",
+                "ERC20Mock",
+                args
+            )
+        );
+    }
+}