[pull] main from a16z:main

.git-blame-ignore-revs

@@ -1,2 +1,3 @@
 # Migrate code style to Black
 449404c7a2b318b8203dbccbeac11c87d20c422f
+00cc14c20659cbf717594451dfc7906b295dca98

.github/workflows/black.yml

@@ -6,5 +6,5 @@ jobs:
   lint:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - uses: psf/black@stable

.github/workflows/publish.yml

@@ -5,9 +5,10 @@ on:
 jobs:
   pypi:
     runs-on: ubuntu-latest
+    environment: release
     steps:
       - name: Checkout
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           fetch-depth: 0
       - name: Build

.github/workflows/test-external.yml

@@ -0,0 +1,71 @@
+name: Test external projects
+
+on:
+  push:
+    branches: [main]
+# pull_request:
+#   branches: [main]
+  workflow_dispatch:
+
+jobs:
+  test:
+    runs-on: macos-latest
+
+    strategy:
+      fail-fast: false
+      matrix:
+        include:
+          - repo: "morpho-org/morpho-data-structures"
+            dir: "morpho-data-structures"
+            cmd: "halmos --function testProve --loop 4 --symbolic-storage"
+            branch: ""
+          - repo: "a16z/cicada"
+            dir: "cicada"
+            cmd: "halmos --contract LibUint1024Test --function testProve --loop 256"
+            branch: ""
+          - repo: "a16z/cicada"
+            dir: "cicada"
+            cmd: "halmos --contract LibPrimeTest --function testProve --loop 256"
+            branch: ""
+          - repo: "farcasterxyz/contracts"
+            dir: "farcaster-contracts"
+            cmd: "halmos"
+            branch: ""
+          - repo: "zobront/halmos-solady"
+            dir: "halmos-solady"
+            cmd: "halmos --function testCheck"
+            branch: ""
+
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+        with:
+          path: halmos
+          # we won't be needing tests/lib for this workflow
+          submodules: false
+
+      - name: Checkout external repo
+        uses: actions/checkout@v4
+        with:
+          repository: ${{ matrix.repo }}
+          path: ${{ matrix.dir }}
+          ref: ${{ matrix.branch }}
+          submodules: recursive
+
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+
+      - name: Set up Python
+        uses: actions/setup-python@v5
+        with:
+          python-version: "3.11"
+
+      - name: Install dependencies
+        run: python -m pip install --upgrade pip
+
+      - name: Install Halmos
+        run: python -m pip install -e ./halmos
+
+      - name: Test external repo
+        run: ${{ matrix.cmd }} -v -st --solver-timeout-assertion 0 --solver-threads 2
+        working-directory: ${{ matrix.dir }}

.github/workflows/test-ffi.yml

@@ -0,0 +1,41 @@
+name: Test FFI
+
+on:
+  push:
+    branches: [main]
+  pull_request:
+    branches: [main]
+
+jobs:
+  test:
+    runs-on: macos-latest
+
+    strategy:
+      fail-fast: false
+      matrix:
+        include:
+        - testname: "tests/ffi"
+
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+
+      - name: Set up Python
+        uses: actions/setup-python@v5
+        with:
+          python-version: "3.11"
+
+      - name: Install dependencies
+        run: |
+          python -m pip install --upgrade pip
+          python -m pip install pytest
+
+      - name: Install Halmos
+        run: python -m pip install -e .
+
+      - name: Run pytest
+        run: pytest -v tests/test_halmos.py -k ${{ matrix.testname }} --halmos-options="--ffi -v -st --solver-timeout-assertion 0"

.github/workflows/test-long.yml

@@ -0,0 +1,45 @@
+name: Test long
+
+on:
+  push:
+    branches: [main]
+# pull_request:
+#   branches: [main]
+  workflow_dispatch:
+
+jobs:
+  test:
+    runs-on: macos-latest
+
+    strategy:
+      fail-fast: false
+      matrix:
+        include:
+        - testname: "tests/solver"
+        - testname: "examples/simple"
+        - testname: "examples/tokens/ERC20"
+        - testname: "examples/tokens/ERC721"
+
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+
+      - name: Set up Python
+        uses: actions/setup-python@v5
+        with:
+          python-version: "3.11"
+
+      - name: Install dependencies
+        run: |
+          python -m pip install --upgrade pip
+          python -m pip install pytest
+
+      - name: Install Halmos
+        run: python -m pip install -e .
+
+      - name: Run pytest
+        run: pytest -x -v tests/test_halmos.py -k ${{ matrix.testname }} --halmos-options="-v -st --solver-timeout-assertion 0 --solver-threads 2" -s --log-cli-level=

.github/workflows/test.yml

@@ -11,38 +11,33 @@ jobs:
     runs-on: ${{ matrix.os }}
 
     strategy:
+      fail-fast: false
       matrix:
-        os: ["ubuntu-latest", "windows-2022"]
-        python-version: ["3.8", "3.9", "3.10", "3.11", "3.8.13", "3.9.13", "3.10.6"]
-        parallel: ["", "--test-parallel", "--solver-parallel", "--test-parallel --solver-parallel"]
-        exclude:
-          # python 3.8.13 is not available in windows-2022
-          - os: "windows-2022"
-            python-version: "3.8.13"
+        os: ["macos-latest", "ubuntu-latest", "windows-latest"]
+        python-version: ["3.9", "3.10", "3.11"]
+        parallel: ["", "--test-parallel"]
+        storage-layout: ["solidity", "generic"]
 
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
         with:
           submodules: recursive
 
       - name: Install Foundry
         uses: foundry-rs/foundry-toolchain@v1
 
       - name: Set up Python ${{ matrix.python-version }}
-        uses: actions/setup-python@v4
+        uses: actions/setup-python@v5
         with:
           python-version: ${{ matrix.python-version }}
 
       - name: Install dependencies
         run: |
           python -m pip install --upgrade pip
-          pip install pytest
+          python -m pip install pytest
 
       - name: Install Halmos
-        run: pip install -e .
+        run: python -m pip install -e .
 
       - name: Run pytest
-        run: pytest
-
-      - name: Test Halmos
-        run: halmos --root tests --symbolic-storage --function test ${{ matrix.parallel }}
+        run: pytest -v -k "not long and not ffi" --ignore=tests/lib --halmos-options="-v -st ${{ matrix.parallel }} --storage-layout ${{ matrix.storage-layout }} --solver-timeout-assertion 0"

.gitignore

@@ -19,5 +19,5 @@ env/
 venv/
 
 # Foundry build files
-*/cache/
-*/out/
+cache/
+out/

.gitmodules

@@ -1,3 +1,18 @@
 [submodule "tests/lib/forge-std"]
 	path = tests/lib/forge-std
 	url = https://github.com/foundry-rs/forge-std
+[submodule "tests/lib/halmos-cheatcodes"]
+	path = tests/lib/halmos-cheatcodes
+	url = https://github.com/a16z/halmos-cheatcodes
+[submodule "tests/lib/openzeppelin-contracts"]
+	path = tests/lib/openzeppelin-contracts
+	url = https://github.com/OpenZeppelin/openzeppelin-contracts
+[submodule "tests/lib/solmate"]
+	path = tests/lib/solmate
+	url = https://github.com/transmissions11/solmate
+[submodule "tests/lib/solady"]
+	path = tests/lib/solady
+	url = https://github.com/Vectorized/solady
+[submodule "tests/lib/multicaller"]
+	path = tests/lib/multicaller
+	url = https://github.com/Vectorized/multicaller

CONTRIBUTING.md

@@ -0,0 +1,60 @@
+# Contributing to Halmos
+
+We greatly appreciate your feedback, suggestions, and contributions to make Halmos a better tool for everyone!
+
+Join the [Halmos Telegram Group][chat] for any inquiries or further discussions.
+
+[chat]: <https://t.me/+4UhzHduai3MzZmUx>
+
+## Development Setup
+
+If you want to submit a pull request, fork the repository:
+
+```sh
+gh repo fork a16z/halmos
+```
+
+Or, if you just want to develop locally, clone it:
+
+```sh
+git clone [email protected]:a16z/halmos.git
+```
+
+Create and activate a virtual environment:
+
+```sh
+python3.11 -m venv .venv
+source .venv/bin/activate
+```
+
+Install the dependencies:
+
+```sh
+python -m pip install -r requirements.txt
+python -m pip install -r requirements-dev.txt
+```
+
+Install and run the git hook scripts:
+
+```sh
+pre-commit install
+pre-commit run --all-files
+```
+
+## Coding Style
+
+We recommend enabling the [black] formatter in your editor, but you can run it manually if needed:
+
+```sh
+python -m black .
+```
+
+[black]: <https://black.readthedocs.io/en/stable/>
+
+## License
+
+By contributing, you agree that your contributions will be licensed under its [AGPL-3.0](LICENSE) License.
+
+## Disclaimer
+
+_These smart contracts and code are being provided as is. No guarantee, representation or warranty is being made, express or implied, as to the safety or correctness of the user interface or the smart contracts and code. They have not been audited and as such there can be no assurance they will work as intended, and users may experience delays, failures, errors, omissions or loss of transmitted information. THE SMART CONTRACTS AND CODE CONTAINED HEREIN ARE FURNISHED AS IS, WHERE IS, WITH ALL FAULTS AND WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING ANY WARRANTY OF MERCHANTABILITY, NON-INFRINGEMENT OR FITNESS FOR ANY PARTICULAR PURPOSE. Further, use of any of these smart contracts and code may be restricted or prohibited under applicable law, including securities laws, and it is therefore strongly advised for you to contact a reputable attorney in any jurisdiction where these smart contracts and code may be accessible for any questions or concerns with respect thereto. Further, no information provided in this repo should be construed as investment advice or legal advice for any particular facts or circumstances, and is not meant to replace competent counsel. a16z is not liable for any use of the foregoing, and users should proceed with caution and use at their own risk. See a16z.com/disclosures for more info._