-
-
Notifications
You must be signed in to change notification settings - Fork 60
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
♻️ Use Configuration File for
halmos-Based Symbolic Tests (#249)
### 🕓 Changelog The PRs a16z/halmos#296 and a16z/halmos#298 have added support for configuration files in `halmos` (https://github.com/a16z/halmos). This PR refactors the configurations currently used inline via the CLI and moves them to the new configuration file `halmos.toml`, which is located in the `test/` subdirectory. I also rename the configuration file `echidna-config.yaml` to `echidna.yaml` and move it to the subdirectory `test/` as well. Eventually, I bump the submodules `FreshCryptoLib` (https://github.com/rdubois-crypto/FreshCryptoLib) and `properties` (https://github.com/crytic/properties) to the latest available commit. --------- Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
- Loading branch information
1 parent
303be48
commit 0abe10f
Showing
8 changed files
with
59 additions
and
38 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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`. |
Submodule properties
updated
11 files
File renamed without changes.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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. |