♻️ Use Configuration File for halmos-Based Symbolic Tests

.github/workflows/halmos.yml

@@ -22,7 +22,7 @@ jobs:
         architecture:
           - x64
         halmos:
-          - "--function testHalmos --storage-layout generic --solver-command=yices-smt2 --solver-parallel --test-parallel --early-exit --ffi --statistics -v"
+          - "--config test/halmos.toml"
 
     steps:
       - name: Checkout

.github/workflows/test-contracts.yml

@@ -20,7 +20,7 @@ jobs:
         node_version:
           - 20
         echidna:
-          - "--config test/tokens/echidna/echidna-config.yaml"
+          - "--config test/echidna.yaml"
 
     steps:
       - name: Checkout

README.md

@@ -141,7 +141,7 @@ pnpm add --save-dev snekmate
 
 ## 🔧 Usage
 
-🐍Vyper favours code reuse through composition rather than inheritance (Solidity inheritance makes it easy to break the [Liskov substitution principle](https://en.wikipedia.org/wiki/Liskov_substitution_principle)). A 🐍Vyper module encapsulates everything required for code reuse, from type and function declarations to state. **All 🐍 snekmate contracts are 🐍Vyper modules.** Thus, many of the 🐍 snekmate contracts do not compile independently, but you must `import` and `initializes` them. Please note that if a module is _stateless_, it does not require the keyword `initializes` (or `uses`) for initialisation (or usage). Each module contract has an associated mock contract in the `mock/` directory, which is part of the associated contract subdirectory. These mock contracts are very illustrative of how 🐍 snekmate contracts can be used as 🐍Vyper modules.
+🐍Vyper favours code reuse through composition rather than inheritance (Solidity inheritance makes it easy to break the [Liskov Substitution Principle](https://en.wikipedia.org/wiki/Liskov_substitution_principle)). A 🐍Vyper module encapsulates everything required for code reuse, from type and function declarations to state. **All 🐍 snekmate contracts are 🐍Vyper modules.** Thus, many of the 🐍 snekmate contracts do not compile independently, but you must `import` and `initializes` them. Please note that if a module is _stateless_, it does not require the keyword `initializes` (or `uses`) for initialisation (or usage). Each module contract has an associated mock contract in the `mock/` directory, which is part of the associated contract subdirectory. These mock contracts are very illustrative of how 🐍 snekmate contracts can be used as 🐍Vyper modules.
 
 > [!IMPORTANT]
 > All 🐍 snekmate contracts are very well documented in the form of general code and [NatSpec](https://docs.vyperlang.org/en/latest/natspec.html) comments. There are no shortcuts – if you are importing specific logic, read the documentation!
@@ -185,26 +185,29 @@ Furthermore, the [`echidna`](https://github.com/crytic/echidna)-based [property]
 
 ```console
 # Run Echidna ERC-20 property tests.
-~$ FOUNDRY_PROFILE=echidna echidna test/tokens/echidna/ERC20Properties.sol --contract CryticERC20ExternalHarness --config test/tokens/echidna/echidna-config.yaml
+~$ FOUNDRY_PROFILE=echidna echidna test/tokens/echidna/ERC20Properties.sol --contract CryticERC20ExternalHarness --config test/echidna.yaml
 
 # Run Echidna ERC-721 property tests.
-~$ FOUNDRY_PROFILE=echidna echidna test/tokens/echidna/ERC721Properties.sol --contract CryticERC721ExternalHarness --config test/tokens/echidna/echidna-config.yaml
+~$ FOUNDRY_PROFILE=echidna echidna test/tokens/echidna/ERC721Properties.sol --contract CryticERC721ExternalHarness --config test/echidna.yaml
 ```
 
 Eventually, the [`halmos`](https://github.com/a16z/halmos)-based symbolic tests for the [`erc20`](./src/snekmate/tokens/erc20.vy), [`erc721`](./src/snekmate/tokens/erc721.vy), [`erc1155`](./src/snekmate/tokens/erc1155.vy), and [`math`](./src/snekmate/utils/math.vy) contracts are available in the [`test/tokens/halmos/`](./test/tokens/halmos) and [`test/utils/halmos/`](./test/utils/halmos) directories. You can run the tests by invoking:
 
+> [!IMPORTANT]
+> You must install the [Yices 2 SMT solver](https://github.com/SRI-CSL/yices2) before invoking the [`halmos`](https://github.com/a16z/halmos)-based symbolic tests.
+
 ```console
 # Run Halmos ERC-20 symbolic tests.
-~$ FOUNDRY_PROFILE=halmos halmos --contract ERC20TestHalmos --function testHalmos --storage-layout generic --ffi
+~$ FOUNDRY_PROFILE=halmos halmos --contract ERC20TestHalmos --config test/halmos.toml
 
 # Run Halmos ERC-721 symbolic tests. Be careful, this is a very time-consuming operation.
-~$ FOUNDRY_PROFILE=halmos halmos --contract ERC721TestHalmos --function testHalmos --storage-layout generic --ffi
+~$ FOUNDRY_PROFILE=halmos halmos --contract ERC721TestHalmos --config test/halmos.toml
 
 # Run Halmos ERC-1155 symbolic tests. Be careful, this is a very time-consuming operation.
-~$ FOUNDRY_PROFILE=halmos halmos --contract ERC1155TestHalmos --function testHalmos --storage-layout generic --ffi
+~$ FOUNDRY_PROFILE=halmos halmos --contract ERC1155TestHalmos --config test/halmos.toml
 
 # Run Halmos math symbolic tests.
-~$ FOUNDRY_PROFILE=halmos halmos --contract MathTestHalmos --function testHalmos --storage-layout generic --ffi
+~$ FOUNDRY_PROFILE=halmos halmos --contract MathTestHalmos --config test/halmos.toml
 ```
 
 > [!TIP]

foundry.toml

@@ -1,34 +1,37 @@
-## defaults for all profiles
+# Defaults for all profiles.
 [profile.default]
-src = "src"                                                 # the source directory
-test = "test"                                               # the test directory
-out = "out"                                                 # the output directory (for artifacts)
-libs = ["lib"]                                              # a list of library directories
-cache = true                                                # whether to cache builds or not
-cache_path = "cache"                                        # where the cache is stored if enabled
-force = false                                               # whether to ignore the cache (clean build)
-fuzz = { runs = 256 }                                       # the number of fuzz runs for tests
-invariant = { runs = 256, depth = 15 }                      # the number of runs and calls (executed in one run) for each invariant test group
-ffi = true                                                  # whether to enable foreign function interface (ffi) cheatcodes or not
-verbosity = 3                                               # the verbosity of tests
-fs_permissions = [{ access = "read-write", path = "./" }]   # set read-write access to project root
-solc_version = "0.8.26"                                     # override for the solc version
-evm_version = "cancun"                                      # set the EVM target version
-no_match_path = "test/**/{echidna,halmos}/**/*"             # only run tests in test directory that do not match the specified glob pattern
+src = "src"                                               # Set the source directory.
+test = "test"                                             # Set the test directory.
+out = "out"                                               # Set the output directory for the artifacts.
+libs = ["lib"]                                            # Configure an array of library directories.
+cache = true                                              # Enable caching.
+cache_path = "cache"                                      # Set the path to the cache.
+force = false                                             # Do not ignore the cache.
+solc_version = "0.8.26"                                   # Set the Solidity compiler version.
+evm_version = "cancun"                                    # Set the EVM target version.
+optimizer = true                                          # Enable the Solidity compiler optimiser.
+optimizer_runs = 200                                      # Configure the number of optimiser runs.
+via_ir = false                                            # Prevent the compilation pipeline from running through the Yul intermediate representation.
+verbosity = 3                                             # Set the verbosity level for the tests.
+ffi = true                                                # Enable the foreign function interface (ffi) cheatcode.
+no_match_path = "test/**/{echidna,halmos}/**/*"           # Run only tests in the test directory that do not match the specified glob pattern.
+fs_permissions = [{ access = "read-write", path = "./" }] # Configure read-write access to the project root.
+fuzz = { runs = 256, max_test_rejects = 65_536 }          # Configure the number of fuzz runs and maximum number of combined inputs that may be rejected for the tests.
+invariant = { runs = 256, depth = 15 }                    # Configure the number of runs and calls (executed in one run) for each invariant test group.
 
-## default overrides for the CI runs
+# Default overrides for the CI runs.
 [profile.ci]
-force = true                                                # always perform a clean build
-fuzz = { runs = 10_000, max_test_rejects = 350_000 }        # increase the number of fuzz runs and maximum number of combined inputs that may be rejected for the tests
-invariant = { runs = 375, depth = 500 }                     # increase the number of runs (while preserving the default depth) for each invariant test group
-verbosity = 4                                               # increase the verbosity of tests
+force = true                                              # Perform always a clean build.
+verbosity = 4                                             # Increase the verbosity level for the tests.
+fuzz = { runs = 10_000, max_test_rejects = 350_000 }      # Increase the number of fuzz runs and maximum number of combined inputs that may be rejected for the tests.
+invariant = { runs = 375, depth = 500 }                   # Increase the number of runs (while preserving the default depth) for each invariant test group.
 
-## default overrides for the Echidna tests
+# Default overrides for the Echidna tests.
 [profile.echidna]
-force = true                                                # always perform a clean build
-evm_version = "shanghai"                                    # set the EVM target version to `shanghai`
+force = true                                              # Perform always a clean build.
+evm_version = "shanghai"                                  # Set the EVM target version to `shanghai`.
 
-## default overrides for the Halmos tests
+# Default overrides for the Halmos tests.
 [profile.halmos]
-force = true                                                # always perform a clean build
-evm_version = "shanghai"                                    # set the EVM target version to `shanghai`
+force = true                                              # Perform always a clean build.
+evm_version = "shanghai"                                  # Set the EVM target version to `shanghai`.

test/halmos.toml

@@ -0,0 +1,15 @@
+[global]
+# Test settings.
+function = "testHalmos"       # Run tests matching the given prefix.
+storage-layout = "generic"    # Set the generic storage layout model.
+test-parallel = true          # Run tests in parallel.
+early-exit = true             # Stop after a counterexample is found.
+ffi = true                    # Enable the foreign function interface (ffi) cheatcode.
+
+# Debugging settings.
+statistics = true             # Print the statistics.
+verbose = 1                   # Set the verbosity level for the tests.
+
+# Solver settings.
+solver-command = "yices-smt2" # Use the Yices 2 SMT solver.
+solver-parallel = true        # Run assertion solvers in parallel.