fix: model SHA-256 precompile input widths in bits

src/halmos/sevm.py

@@ -2482,15 +2482,26 @@ def call_unknown() -> None:
 
             elif to == SHA256_PRECOMPILE:
                 exit_code = ONE
-                f_sha256 = Function(
-                    f"f_sha256_{arg_size}", BitVecSorts[arg_size], BitVecSort256
-                )
-
                 unwrapped = arg.unwrap()
-                wrapped = (
-                    unwrapped if is_bv(unwrapped) else bytes_to_bv_value(unwrapped)
-                )
-                ret = ByteVec(f_sha256(wrapped))
+                if arg_size == 0:
+                    # Z3 has no zero-width bitvectors. Model SHA-256 of the
+                    # empty byte string as a stable symbolic constant instead.
+                    sha256 = BitVec("f_sha256_0", BitVecSort256)
+                else:
+                    # EVM memory sizes are bytes; Z3 bitvector sorts are bits.
+                    f_sha256 = Function(
+                        f"f_sha256_{arg_size}",
+                        BitVecSorts[arg_size * 8],
+                        BitVecSort256,
+                    )
+                    wrapped = (
+                        unwrapped
+                        if is_bv(unwrapped)
+                        else bytes_to_bv_value(unwrapped)
+                    )
+                    sha256 = f_sha256(wrapped)
+
+                ret = ByteVec(sha256)
 
             elif to == RIPEMD160_PRECOMPILE:
                 exit_code = ONE

tests/expected/all.json

@@ -4538,6 +4538,35 @@
                 "num_bounded_loops": null
             }
         ],
+        "test/Sha256Precompile.t.sol:Sha256PrecompileTest": [
+            {
+                "name": "check_sha256_inputs()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_sha256_symbolic_byte(bytes1)",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "invariant_marker_zero()",
+                "exitcode": 1,
+                "num_models": 1,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            }
+        ],
         "test/Sha3.t.sol:Sha3Test": [
             {
                 "name": "check_address_collision_pass(uint256,uint256)",
@@ -6734,4 +6763,4 @@
             }
         ]
     }
-}
+}

tests/regression/test/Sha256Precompile.t.sol

@@ -0,0 +1,51 @@
+// SPDX-License-Identifier: AGPL-3.0
+pragma solidity >=0.8.0 <0.9.0;
+
+import "forge-std/Test.sol";
+
+contract Sha256Target {
+    uint256 public marker;
+
+    function hashOneByte() external {
+        marker = 1;
+        (bool success, bytes memory output) = address(2).staticcall(hex"01");
+        require(success && output.length == 32);
+    }
+
+    function hashEmpty() external view {
+        (bool success, bytes memory output) = address(2).staticcall("");
+        require(success && output.length == 32);
+    }
+}
+
+contract Sha256PrecompileTest is Test {
+    Sha256Target target;
+
+    function setUp() public {
+        target = new Sha256Target();
+        targetContract(address(target));
+    }
+
+    function check_sha256_inputs() public {
+        target.hashEmpty();
+        target.hashOneByte();
+        assertEq(target.marker(), 1);
+    }
+
+    function check_sha256_symbolic_byte(bytes1 input) public view {
+        bytes memory data = abi.encodePacked(input);
+        (bool successFirst, bytes memory first) = address(2).staticcall(data);
+        (bool successSecond, bytes memory second) = address(2).staticcall(data);
+
+        assertTrue(successFirst && successSecond);
+        assertEq(first.length, 32);
+        assertEq(second.length, 32);
+        assertEq(first, second);
+    }
+
+    /// @custom:halmos --invariant-depth 1
+    function invariant_marker_zero() public view {
+        // Expected counterexample: hashOneByte() reaches this state.
+        assertEq(target.marker(), 0);
+    }
+}