fix: use consistent hex prefix handling

Using [2:] to strip the "0x" prefix from hexstrings is problematic, because hex(int) or hexify(val) return 0x-prefixed strings, but bytes.hex() doesn't. So occasionally we would mistakenly eat the first byte instead of the prefix:

before: hex"487b710000000000000000000000000000000000000000000000000000000000000032"
after:  hex"4e487b710000000000000000000000000000000000000000000000000000000000000032"

src/halmos/cheatcodes.py

@@ -45,11 +45,9 @@ def extract_string_array_argument(calldata: BitVecRef, arg_idx: int):
 def stringified_bytes_to_bytes(hexstring: str):
     """Converts a string of bytes to a bytes memory type"""
 
-    if hexstring.startswith("0x"):
-        hexstring = hexstring[2:]
-
+    hexstring = stripped(hexstring)
     hexstring_len = (len(hexstring) + 1) // 2
-    hexstring_len_enc = hex(hexstring_len)[2:].rjust(64, "0")
+    hexstring_len_enc = stripped(hex(hexstring_len)).rjust(64, "0")
     hexstring_len_ceil = (hexstring_len + 31) // 32 * 32
 
     ret_bytes = bytes.fromhex(
@@ -308,7 +306,7 @@ def handle(sevm, ex, arg: BitVec) -> BitVec:
 
         # vm.getCode(string)
         elif funsig == hevm_cheat_code.get_code_sig:
-            calldata = bytes.fromhex(hex(arg.as_long())[2:])
+            calldata = bv_value_to_bytes(arg)
             path_len = int.from_bytes(calldata[36:68], "big")
             path = calldata[68 : 68 + path_len].decode("utf-8")
 

src/halmos/sevm.py

@@ -551,14 +551,11 @@ def from_hexcode(hexcode: str):
         if len(hexcode) % 2 != 0:
             raise ValueError(hexcode)
 
-        if hexcode.startswith("0x"):
-            hexcode = hexcode[2:]
-
         if "__" in hexcode:
             warn(LIBRARY_PLACEHOLDER, f"contract hexcode contains library placeholder")
 
         try:
-            return Contract(bytes.fromhex(hexcode))
+            return Contract(bytes.fromhex(stripped(hexcode)))
         except ValueError as e:
             raise ValueError(f"{e} (hexcode={hexcode})")
 
@@ -1069,7 +1066,7 @@ def resolve_libs(self, creation_hexcode, deployed_hexcode, lib_references) -> st
                 )
 
                 placeholder = lib_references[lib]["placeholder"]
-                hex_address = hex(address.as_long())[2:].zfill(40)
+                hex_address = stripped(hex(address.as_long())).zfill(40)
 
                 creation_hexcode = creation_hexcode.replace(placeholder, hex_address)
                 deployed_hexcode = deployed_hexcode.replace(placeholder, hex_address)

src/halmos/utils.py

@@ -186,9 +186,7 @@ def extract_funsig(calldata: BitVecRef):
 
 
 def bv_value_to_bytes(x: BitVecNumRef) -> bytes:
-    if x.size() % 8 != 0:
-        raise ValueError(x, x.size())
-    return x.as_long().to_bytes(x.size() // 8, "big")
+    return x.as_long().to_bytes(byte_length(x, strict=True), "big")
 
 
 def unbox_int(x: Any) -> Any:
@@ -228,12 +226,15 @@ def byte_length(x: Any, strict=True) -> int:
     raise HalmosException(f"byte_length({x}) of type {type(x)}")
 
 
+def stripped(hexstring: str) -> str:
+    """Remove 0x prefix from hexstring"""
+    return hexstring[2:] if hexstring.startswith("0x") else hexstring
+
+
 def decode_hex(hexstring: str) -> Optional[bytes]:
-    if hexstring.startswith("0x"):
-        hexstring = hexstring[2:]
     try:
         # not checking if length is even because fromhex accepts spaces
-        return bytes.fromhex(hexstring)
+        return bytes.fromhex(stripped(hexstring))
     except ValueError:
         return None
 
@@ -276,15 +277,15 @@ def render_bool(b: BitVecRef) -> str:
 
 
 def render_string(s: BitVecRef) -> str:
-    str_val = bytes.fromhex(hexify(s)[2:]).decode("utf-8")
+    str_val = bytes.fromhex(stripped(hexify(s))).decode("utf-8")
     return f'"{str_val}"'
 
 
 def render_bytes(b: UnionType[BitVecRef, bytes]) -> str:
     if is_bv(b):
         return hexify(b) + f" ({byte_length(b, strict=False)} bytes)"
     else:
-        return f'hex"{b.hex()[2:]}"'
+        return f'hex"{stripped(b.hex())}"'
 
 
 def render_address(a: BitVecRef) -> str: