Enhance div_xy_y to support signed and unsigned division simplification

src/halmos/bitvec.py

@@ -545,8 +545,6 @@ def mul(
     def div(
         self, other: BV, *, abstraction: FuncDeclRef | None = None
     ) -> "HalmosBitVec":
-        # TODO: div_xy_y
-
         size = self._size
         assert size == other.size
 
@@ -578,7 +576,6 @@ def div(
     def sdiv(
         self, other: BV, *, abstraction: FuncDeclRef | None = None
     ) -> "HalmosBitVec":
-        # TODO: sdiv_xy_y
         size = self._size
         assert size == other.size
 

src/halmos/sevm.py

@@ -2102,30 +2102,40 @@ def __init__(self, options: HalmosConfig, fun_info: FunctionInfo) -> None:
         is_generic = self.options.storage_layout == "generic"
         self.storage_model = GenericStorage if is_generic else SolidityStorage
 
-    def div_xy_y(self, w1: Word, w2: Word) -> Word:
+    def div_xy_y(self, w1: Word, w2: Word, signed: bool = False) -> Word:
         # return the number of bits required to represent the given value. default = 256
         def bitsize(w: Word) -> int:
+            z3w = w.as_z3() if hasattr(w, "as_z3") else w
             if (
-                w.decl().name() == "concat"
-                and is_bv_value(w.arg(0))
-                and int(str(w.arg(0))) == 0
+                z3w.decl().name() == "concat"
+                and is_bv_value(z3w.arg(0))
+                and int(str(z3w.arg(0))) == 0
             ):
-                return 256 - w.arg(0).size()
+                return 256 - z3w.arg(0).size()
             return 256
 
-        w1 = normalize(w1)
-
-        if w1.decl().name() == "bvmul" and w1.num_args() == 2:
-            x = w1.arg(0)
-            y = w1.arg(1)
-            if eq(w2, x) or eq(w2, y):  # xy/x or xy/y
-                size_x = bitsize(x)
-                size_y = bitsize(y)
-                if size_x + size_y <= 256:
-                    if eq(w2, x):  # xy/x == y
-                        return y
-                    else:  # xy/y == x
-                        return x
+        w1_z3 = w1.as_z3() if hasattr(w1, "as_z3") else w1
+        w2_z3 = w2.as_z3() if hasattr(w2, "as_z3") else w2
+
+        if w1_z3.decl().name() == "bvmul" and w1_z3.num_args() == 2:
+            x = w1_z3.arg(0)
+            y = w1_z3.arg(1)
+            if eq(w2_z3, x) or eq(w2_z3, y):  # xy/x or xy/y
+                if signed:
+                    # Signed division: safe to simplify if divisor exactly matches factor
+                    if eq(w2_z3, x):
+                        return BV(y, w1.size)  # wrap back
+                    elif eq(w2_z3, y):
+                        return BV(x, w1.size)
+                else:
+                    # Unsigned division: check for overflow
+                    size_x = bitsize(x)
+                    size_y = bitsize(y)
+                    if size_x + size_y <= 256:
+                        if eq(w2_z3, x):  # xy/x == y
+                            return BV(y, w1.size)  # wrap back
+                        else:  # xy/y == x
+                            return BV(x, w1.size)
         return None
 
     def mk_div(self, ex: Exec, x: Any, y: Any) -> Any:
@@ -2150,7 +2160,11 @@ def arith(self, ex: Exec, op: int, w1: Word, w2: Word) -> Word:
             return w1.mul(w2, abstraction=f_mul[w1.size])
 
         if op == OP_DIV:
-            # TODO: div_xy_y
+            # Check: div_xy_y
+            #   Try simplification first: (x * y) / x → y, (x * y) / y → x
+            simplified_div = self.div_xy_y(w1, w2)
+            if simplified_div is not None:
+                return simplified_div
 
             term = w1.div(w2, abstraction=f_div)
             if term.is_symbolic:
@@ -2166,6 +2180,11 @@ def arith(self, ex: Exec, op: int, w1: Word, w2: Word) -> Word:
             return term
 
         if op == OP_SDIV:
+            # Try signed simplification first
+            simplified_sdiv = self.div_xy_y(w1, w2, signed=True)
+            if simplified_sdiv is not None:
+                return simplified_sdiv
+
             return w1.sdiv(w2, abstraction=f_sdiv)
 
         if op == OP_SMOD:

tests/regression/foundry.lock

@@ -0,0 +1,17 @@
+{
+  "../lib/forge-std": {
+    "rev": "1eea5bae12ae557d589f9f0f0edae2faa47cb262"
+  },
+  "../lib/halmos-cheatcodes": {
+    "rev": "6da4e692c357ba6d641a2e677a28298cac9f76ab"
+  },
+  "../lib/openzeppelin-contracts": {
+    "rev": "dbb6104ce834628e473d2173bbc9d47f81a9eec3"
+  },
+  "../lib/solady": {
+    "rev": "4d4a7572ad01e84e96370e42bd10d1cc16c1fb65"
+  },
+  "../lib/solmate": {
+    "rev": "bfc9c25865a274a7827fea5abf6e4fb64fc64e6c"
+  }
+}