💥 Add halmos-Based Symbolic Tests (#240)

### 🕓 Changelog This PR adds [`halmos`](https://github.com/a16z/halmos)-based symbolic tests for the `erc20`, `erc721`, `erc1155`, and `math` contracts (closes #180). The `erc721` and `erc1155` tests each take substantial amount of time as part of the CI. Hence, we run the new `halmos` CI pipeline each day at 03:30 a.m. (= "nightly" tests) as scheduled `cron` job instead of integrating it into the normal `push` and `pull_request` pipeline. Furthermore, the `halmos`-based `math` tests `testHalmosAssertMulDiv`, `testHalmosAssertWadLn`, `testHalmosAssertWadExp`, `testHalmosAssertCbrt`, and `testHalmosAssertWadCbrt` face out of memory issues as the timeout for the Z3 solver does not work for the queries of these tests. Thus, these tests are currently commented out. Additionally, the test `testHalmosAssertNoBackdoor` in the `erc721` and `erc1155` contracts is currently commented out due to performance and reverting path issues in `halmos`. Eventually, we target the `main` `halmos` branch (= "nightly" version) in the CI pipeline and use the [Yices 2 SMT solver](https://github.com/SRI-CSL/yices2). --------- Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
pcaversaccio · May 22, 2024 · 459ec3f · 459ec3f
1 parent f20faf7
commit 459ec3f
Show file tree

Hide file tree

Showing 28 changed files with 1,223 additions and 219 deletions.
diff --git a/.gas-snapshot b/.gas-snapshot
diff --git a/.github/workflows/checks.yml b/.github/workflows/checks.yml
@@ -3,7 +3,7 @@ name: 👮‍♂️ Sanity checks
 on: [push, pull_request, workflow_dispatch]
 
 concurrency:
-  group: ${{github.workflow}}-${{github.ref}}
+  group: ${{ github.workflow }}-${{ github.ref }}
   cancel-in-progress: true
 
 jobs:
@@ -13,10 +13,10 @@ jobs:
       matrix:
         os:
           - ubuntu-latest
-        architecture:
-          - x64
         python_version:
           - 3.12
+        architecture:
+          - x64
         node_version:
           - 20
 

diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml
@@ -3,7 +3,7 @@ name: 🔍️ CodeQL
 on: [push, pull_request, workflow_dispatch]
 
 concurrency:
-  group: ${{github.workflow}}-${{github.ref}}
+  group: ${{ github.workflow }}-${{ github.ref }}
   cancel-in-progress: true
 
 jobs:
@@ -35,4 +35,4 @@ jobs:
       - name: Perform CodeQL analysis
         uses: github/codeql-action/analyze@v3
         with:
-          category: "/language:${{matrix.language}}"
+          category: "/language:${{ matrix.language }}"
diff --git a/.github/workflows/halmos.yml b/.github/workflows/halmos.yml
@@ -0,0 +1,87 @@
+name: 👁️ Halmos symbolic tests
+
+on:
+  schedule:
+    - cron: "30 3 * * *"
+  workflow_dispatch:
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  halmos-tests:
+    runs-on: ${{ matrix.os }}
+    strategy:
+      matrix:
+        os:
+          - ubuntu-latest
+        python_version:
+          - 3.12
+        architecture:
+          - x64
+        halmos:
+          - "--function testHalmos --storage-layout generic --solver-command=yices-smt2 --solver-parallel --test-parallel --early-exit --ffi --statistics -v"
+
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: Setup Python
+        uses: actions/setup-python@v5
+        with:
+          python-version: ${{ matrix.python_version }}
+          architecture: ${{ matrix.architecture }}
+
+      - name: Install Vyper
+        run: pip install git+https://github.com/vyperlang/vyper.git@master
+
+      - name: Show the Vyper version
+        run: vyper --version
+
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+        with:
+          version: nightly
+
+      - name: Install `setuptools`
+        run: pip install setuptools
+
+      - name: Install Halmos
+        run: pip install git+https://github.com/a16z/halmos.git@main
+
+      - name: Show the Halmos version
+        run: halmos --version
+
+      - name: Install Homebrew
+        uses: Homebrew/actions/setup-homebrew@master
+
+      - name: Install Yices 2 SMT solver
+        run: brew install SRI-CSL/sri-csl/yices2
+
+      - name: Show the Foundry Halmos config
+        run: forge config
+        env:
+          FOUNDRY_PROFILE: halmos
+
+      - name: Run Halmos ERC-20 symbolic tests
+        run: halmos --contract ERC20TestHalmos ${{ matrix.halmos }}
+        env:
+          FOUNDRY_PROFILE: halmos
+
+      - name: Run Halmos ERC-721 symbolic tests
+        run: halmos --contract ERC721TestHalmos ${{ matrix.halmos }}
+        env:
+          FOUNDRY_PROFILE: halmos
+
+      - name: Run Halmos ERC-1155 symbolic tests
+        run: halmos --contract ERC1155TestHalmos ${{ matrix.halmos }}
+        env:
+          FOUNDRY_PROFILE: halmos
+
+      - name: Run Halmos math symbolic tests
+        run: halmos --contract MathTestHalmos ${{ matrix.halmos }}
+        env:
+          FOUNDRY_PROFILE: halmos
diff --git a/.github/workflows/publish-pypi.yml b/.github/workflows/publish-pypi.yml
@@ -17,10 +17,10 @@ jobs:
       matrix:
         os:
           - ubuntu-latest
-        architecture:
-          - x64
         python_version:
           - 3.12
+        architecture:
+          - x64
 
     steps:
       - name: Checkout

diff --git a/.github/workflows/publish-test-pypi.yml b/.github/workflows/publish-test-pypi.yml
@@ -14,10 +14,10 @@ jobs:
       matrix:
         os:
           - ubuntu-latest
-        architecture:
-          - x64
         python_version:
           - 3.12
+        architecture:
+          - x64
 
     steps:
       - name: Checkout

diff --git a/.github/workflows/test-contracts.yml b/.github/workflows/test-contracts.yml
@@ -3,7 +3,7 @@ name: 🕵️‍♂️ Test smart contracts
 on: [push, pull_request, workflow_dispatch]
 
 concurrency:
-  group: ${{github.workflow}}-${{github.ref}}
+  group: ${{ github.workflow }}-${{ github.ref }}
   cancel-in-progress: true
 
 jobs:
@@ -13,12 +13,14 @@ jobs:
       matrix:
         os:
           - ubuntu-latest
-        architecture:
-          - x64
         python_version:
           - 3.12
+        architecture:
+          - x64
         node_version:
           - 20
+        echidna:
+          - "--config test/tokens/echidna/echidna-config.yaml"
 
     steps:
       - name: Checkout
@@ -118,13 +120,11 @@ jobs:
           FOUNDRY_PROFILE: echidna
 
       - name: Run Echidna ERC-20 property tests
-        run: |
-          echidna test/tokens/echidna/ERC20Properties.sol --contract CryticERC20ExternalHarness --config test/tokens/echidna/echidna-config.yaml
+        run: echidna test/tokens/echidna/ERC20Properties.sol --contract CryticERC20ExternalHarness ${{ matrix.echidna }}
         env:
           FOUNDRY_PROFILE: echidna
 
       - name: Run Echidna ERC-721 property tests
-        run: |
-          echidna test/tokens/echidna/ERC721Properties.sol --contract CryticERC721ExternalHarness --config test/tokens/echidna/echidna-config.yaml
+        run: echidna test/tokens/echidna/ERC721Properties.sol --contract CryticERC721ExternalHarness ${{ matrix.echidna }}
         env:
           FOUNDRY_PROFILE: echidna
diff --git a/.gitmodules b/.gitmodules
@@ -25,6 +25,9 @@
 [submodule "lib/FreshCryptoLib"]
 	path = lib/FreshCryptoLib
 	url = https://github.com/rdubois-crypto/FreshCryptoLib.git
+[submodule "lib/halmos-cheatcodes"]
+	path = lib/halmos-cheatcodes
+	url = https://github.com/a16z/halmos-cheatcodes.git
 [submodule "lib/solidity-bytes-utils"]
 	path = lib/solidity-bytes-utils
 	url = https://github.com/GNSPS/solidity-bytes-utils.git

diff --git a/.prettierignore b/.prettierignore
@@ -8,6 +8,7 @@ lib/properties
 lib/create-util
 lib/erc4626-tests
 lib/FreshCryptoLib
+lib/halmos-cheatcodes
 lib/solidity-bytes-utils
 lib/openzeppelin-contracts
 echidna-corpus

diff --git a/.solhintignore b/.solhintignore
@@ -8,6 +8,7 @@ lib/properties
 lib/create-util
 lib/erc4626-tests
 lib/FreshCryptoLib
+lib/halmos-cheatcodes
 lib/solidity-bytes-utils
 lib/openzeppelin-contracts
 echidna-corpus

diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -36,8 +36,15 @@
 ### 🥢 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))
+  - [`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))
+    - Add `halmos`-based `erc20` symbolic tests. ([#240](https://github.com/pcaversaccio/snekmate/pull/240))
+  - [`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))
+    - Add `halmos`-based `erc721` symbolic tests. ([#240](https://github.com/pcaversaccio/snekmate/pull/240))
+  - [`erc1155`](https://github.com/pcaversaccio/snekmate/blob/v0.1.0/src/snekmate/tokens/erc1155.vy): Add `halmos`-based `erc1155` symbolic tests. ([#240](https://github.com/pcaversaccio/snekmate/pull/240))
+- **Utility Functions**
+  - [`math`](https://github.com/pcaversaccio/snekmate/blob/v0.1.0/src/snekmate/utils/math.vy): Add `halmos`-based `math` symbolic tests. ([#240](https://github.com/pcaversaccio/snekmate/pull/240))
 
 ### ❗️ Breaking Changes
 

diff --git a/README.md b/README.md
@@ -182,6 +182,22 @@ Furthermore, the [`echidna`](https://github.com/crytic/echidna)-based [property]
 ~$ FOUNDRY_PROFILE=echidna echidna test/tokens/echidna/ERC721Properties.sol --contract CryticERC721ExternalHarness --config test/tokens/echidna/echidna-config.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:
+
+```console
+# Run Halmos ERC-20 symbolic tests.
+~$ FOUNDRY_PROFILE=halmos halmos --contract ERC20TestHalmos --function testHalmos --storage-layout generic --ffi
+
+# 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
+
+# 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
+
+# Run Halmos math symbolic tests.
+~$ FOUNDRY_PROFILE=halmos halmos --contract MathTestHalmos --function testHalmos --storage-layout generic --ffi
+```
+
 > [!TIP]
 > If you encounter any issues, please ensure that you have the [latest](https://github.com/vyperlang/vyper/releases) Vyper version installed locally.
 

diff --git a/eslint.config.js b/eslint.config.js
@@ -23,6 +23,7 @@ module.exports = [
       "lib/create-util/**",
       "lib/erc4626-tests/**",
       "lib/FreshCryptoLib/**",
+      "lib/halmos-cheatcodes/**",
       "lib/solidity-bytes-utils/**",
       "lib/openzeppelin-contracts/**",
       "echidna-corpus/**",

diff --git a/foundry.toml b/foundry.toml
@@ -1,20 +1,20 @@
 ## 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
+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
+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 }                                  # the number of runs that must execute 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.25'                                     # override for the solc version
-evm_version = 'cancun'                                      # 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
+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 = "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
 
 ## default overrides for the CI runs
 [profile.ci]
@@ -26,4 +26,9 @@ verbosity = 4                                               # increase the verbo
 ## 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`
+evm_version = "shanghai"                                    # set the EVM target version to `shanghai`
+
+## 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`
diff --git a/lib/halmos-cheatcodes b/lib/halmos-cheatcodes