fix: use bit size for sha256/ripemd160/modexp precompile input sorts

src/halmos/sevm.py

@@ -2483,7 +2483,7 @@ def call_unknown() -> None:
             elif to == SHA256_PRECOMPILE:
                 exit_code = ONE
                 f_sha256 = Function(
-                    f"f_sha256_{arg_size}", BitVecSorts[arg_size], BitVecSort256
+                    f"f_sha256_{arg_size}", BitVecSorts[arg_size * 8], BitVecSort256
                 )
 
                 unwrapped = arg.unwrap()
@@ -2495,7 +2495,7 @@ def call_unknown() -> None:
             elif to == RIPEMD160_PRECOMPILE:
                 exit_code = ONE
                 f_ripemd160 = Function(
-                    f"f_ripemd160_{arg_size}", BitVecSorts[arg_size], BitVecSort160
+                    f"f_ripemd160_{arg_size}", BitVecSorts[arg_size * 8], BitVecSort160
                 )
 
                 unwrapped = arg.unwrap()
@@ -2513,8 +2513,8 @@ def call_unknown() -> None:
                 modulus_size = ex.int_of(arg.get_word(64))
                 f_modexp = Function(
                     f"f_modexp_{arg_size}_{modulus_size}",
-                    BitVecSorts[arg_size],
-                    BitVecSorts[modulus_size],
+                    BitVecSorts[arg_size * 8],
+                    BitVecSorts[modulus_size * 8],
                 )
 
                 unwrapped = arg.unwrap()

tests/expected/all.json

@@ -4388,6 +4388,35 @@
                 "num_bounded_loops": null
             }
         ],
+        "test/Precompile.t.sol:PrecompileTest": [
+            {
+                "name": "check_modexp_symbolic(uint256,uint256,uint256)",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_ripemd160_symbolic(bytes32,bytes32)",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_sha256_symbolic(bytes32,bytes32)",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            }
+        ],
         "test/Proxy.t.sol:ProxyTest": [
             {
                 "name": "check_foo(uint256,uint256,address)",

tests/regression/test/Precompile.t.sol

@@ -0,0 +1,26 @@
+// SPDX-License-Identifier: AGPL-3.0
+pragma solidity >=0.8.0 <0.9.0;
+
+import "forge-std/Test.sol";
+
+/// Precompiles that are modeled as uninterpreted functions over symbolic input.
+/// The function input sorts must be sized in bits (input byte length * 8).
+contract PrecompileTest is Test {
+    function check_sha256_symbolic(bytes32 x, bytes32 y) public view {
+        assertEq(sha256(abi.encode(x, y)), sha256(abi.encode(x, y)));
+    }
+
+    function check_ripemd160_symbolic(bytes32 x, bytes32 y) public view {
+        assertEq(ripemd160(abi.encode(x, y)), ripemd160(abi.encode(x, y)));
+    }
+
+    function check_modexp_symbolic(uint256 base, uint256 exp, uint256 mod) public view {
+        // base_len, exp_len, mod_len are all 32 bytes
+        bytes memory input = abi.encode(uint256(32), uint256(32), uint256(32), base, exp, mod);
+
+        (bool success, bytes memory retdata) = address(0x05).staticcall(input);
+
+        assertTrue(success);
+        assertEq(retdata.length, 32); // mod_len bytes
+    }
+}