Merge branch 'main' into quiet-metadata-warning

.github/workflows/test-external.yml

@@ -3,8 +3,6 @@ name: Test external projects
 on:
   push:
     branches: [main, chore-workflows]
-    paths:
-      - .github/workflows/test-external.yml
   workflow_dispatch:
     inputs:
       halmos-options:

.github/workflows/test-ffi.yml

@@ -3,8 +3,6 @@ name: Test FFI
 on:
   push:
     branches: [main, chore-workflows]
-    paths:
-      - .github/workflows/test-ffi.yml
   pull_request:
     branches: [main]
   workflow_dispatch:

.github/workflows/test-long.yml

@@ -3,8 +3,6 @@ name: Test long
 on:
   push:
     branches: [main, chore-workflows]
-    paths:
-      - .github/workflows/test-long.yml
   workflow_dispatch:
     inputs:
       halmos-options:

.github/workflows/test.yml

@@ -3,8 +3,6 @@ name: Test
 on:
   push:
     branches: [main, chore-workflows]
-    paths:
-      - .github/workflows/test.yml
   pull_request:
     branches: [main]
   workflow_dispatch:
@@ -28,7 +26,7 @@ jobs:
       fail-fast: false
       matrix:
         os: ["macos-latest", "ubuntu-latest", "windows-latest"]
-        python-version: ["3.9", "3.10", "3.11", "3.12"]
+        python-version: ["3.11", "3.12"]
         parallel: ["", "--test-parallel"]
         storage-layout: ["solidity", "generic"]
 

.gitmodules

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

packages/halmos-builder/Dockerfile

@@ -18,4 +18,3 @@ COPY --from=ghcr.io/foundry-rs/foundry:latest \
 ADD --chmod=755 https://astral.sh/uv/install.sh /install.sh
 RUN /install.sh && rm /install.sh
 ENV PATH="/root/.cargo/bin:${PATH}"
-

packages/halmos/Dockerfile

@@ -1,7 +1,4 @@
-# FROM ghcr.io/a16z/halmos-builder:latest
-
-# TODO: switch to :latest as soon as the image is available
-FROM ghcr.io/a16z/halmos-builder:chore-workflows
+FROM ghcr.io/a16z/halmos-builder:latest
 
 # Enable the virtual environment
 ENV PATH="/halmos/.venv/bin:$PATH"

packages/solvers/README.md

@@ -45,6 +45,21 @@ done
 | Z3 | 4.13.1 | [Z3Prover/z3](https://github.com/Z3Prover/z3) | Includes a [Dockerfile](https://github.com/Z3Prover/z3/blob/master/docker/ubuntu-20-04.Dockerfile) and a package but no `latest` tag |
 
 
+## Contributing
+
+Everyone is welcome to contribute new solvers or new versions to the image via pull requests. If a solver is competitive at [SMT-COMP](https://smt-comp.github.io), it would be great to have it included in the image. 
+
+When possible, we prefer release binaries from an official source like the Github releases for the project to minimize the time it takes to build the image. If you're unsure about a particular solver or how to integrate it, consider reaching out on the [Halmos Dev Chat](https://t.me/+4UhzHduai3MzZmUx). 
+
+Before opening the pull request, please test your changes by verifying:
+
+* that you can build the image locally
+* that you can correctly invoke the solver as described in the [Quick Start](https://github.com/a16z/halmos/tree/main/packages/solvers#quick-start) section
+* update this README with the name, version and source of the solver
+
+Thank you in advance!
+
+
 ## Credit
 
 Based on [EmperorOrokuSaki/solvers](https://github.com/EmperorOrokuSaki/solvers)

pyproject.toml

@@ -20,7 +20,7 @@ classifiers = [
     "License :: OSI Approved :: GNU Affero General Public License v3",
     "Operating System :: OS Independent",
 ]
-requires-python = ">=3.9"
+requires-python = ">=3.11"
 dependencies = [
     "sortedcontainers>=2.4.0",
     "toml>=0.10.2",
@@ -35,7 +35,7 @@ halmos = "halmos.__main__:main"
 "Homepage" = "https://github.com/a16z/halmos"
 
 [tool.black]
-target-version = ["py39", "py310", "py311", "py312"]
+target-version = ["py311", "py312"]
 
 [tool.pytest.ini_options]
 # TODO: re-add test_traces.py when we have a better way to support it in CI

src/halmos/sevm.py

@@ -37,6 +37,7 @@
 Steps = Dict[int, Dict[str, Any]]  # execution tree
 
 EMPTY_BYTES = ByteVec()
+EMPTY_KECCAK = con(0xC5D2460186F7233C927E7DB2DCC703C0E500B653CA82273B7BFAD8045D85A470)
 MAX_CALL_DEPTH = 1024
 
 # TODO: make this configurable
@@ -844,7 +845,7 @@ def sha3_data(self, data: Bytes) -> Word:
             )
             sha3_expr = f_sha3(data)
         else:
-            sha3_expr = BitVec("f_sha3_0", BitVecSort256)
+            sha3_expr = EMPTY_KECCAK
 
         # assume hash values are sufficiently smaller than the uint max
         self.path.append(ULE(sha3_expr, 2**256 - 2**64))
@@ -2311,15 +2312,47 @@ def finalize(ex: Exec):
                             ex.path.append(codesize > 0)
                     ex.st.push(codesize)
 
-                # TODO: define f_extcodehash for known addresses in advance
+                elif opcode == EVM.EXTCODECOPY:
+                    account: Address = uint160(ex.st.pop())
+                    loc: int = int_of(ex.st.pop(), "symbolic EXTCODECOPY offset")
+                    offset: int = int_of(ex.st.pop(), "symbolic EXTCODECOPY offset")
+                    size: int = int_of(ex.st.pop(), "symbolic EXTCODECOPY size")
+
+                    if size > 0:
+                        end_loc = loc + size
+                        if end_loc > MAX_MEMORY_SIZE:
+                            raise HalmosException("EXTCODECOPY > MAX_MEMORY_SIZE")
+
+                        # TODO: handle the case where account may alias multiple addresses
+                        account_addr = self.resolve_address_alias(ex, account)
+                        if account_addr is None:
+                            # this could be unsound if the solver in resolve_address_alias
+                            # returns unknown, meaning that there is in fact a must-alias
+                            # address, but we didn't find it in time
+                            warn(
+                                f"EXTCODECOPY: unknown address {hexify(account)} "
+                                "is assumed to have empty bytecode"
+                            )
+
+                        account_code: Contract = ex.code.get(account_addr) or ByteVec()
+                        codeslice: ByteVec = account_code._code.slice(
+                            offset, offset + size
+                        )
+                        ex.st.memory.set_slice(loc, end_loc, codeslice)
+
                 elif opcode == EVM.EXTCODEHASH:
-                    account = uint160(ex.st.pop())
-                    account_addr = self.resolve_address_alias(ex, account)
+                    account_addr = uint160(ex.st.pop())
+                    alias_addr = self.resolve_address_alias(ex, account_addr)
+                    addr = alias_addr if alias_addr is not None else account_addr
+
+                    account_code: Optional[Contract] = ex.code.get(addr, None)
+
                     codehash = (
-                        f_extcodehash(account_addr)
-                        if account_addr is not None
-                        else f_extcodehash(account)
+                        f_extcodehash(addr)
+                        if account_code is None
+                        else ex.sha3_data(account_code._code.unwrap())
                     )
+
                     ex.st.push(codehash)
 
                 elif opcode == EVM.CODESIZE:

tests/expected/all.json

@@ -786,6 +786,89 @@
                 "num_bounded_loops": null
             }
         ],
+        "test/Extcodehash.t.sol:ExtcodehashTest": [
+            {
+                "name": "check_extcodehash_a1_eq_a2()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_extcodehash_a1_eq_directHash()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_extcodehash_a1_eq_runtimeCodeHash()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_extcodehash_a1_ne_b1()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_extcodehash_after_etch()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_extcodehash_empty()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_extcodehash_eq_directHash()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_extcodehash_unknown_addr_eq_0()",
+                "exitcode": 1,
+                "num_models": 1,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_extcodehash_unknown_addr_noteq_0()",
+                "exitcode": 1,
+                "num_models": 1,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            }
+        ],
         "test/Foundry.t.sol:DeepFailer": [
             {
                 "name": "check_fail_cheatcode()",