fix: preserve integer arithmetic and loop dtype semantics

docs/architecture.md

@@ -33,7 +33,9 @@ flowchart LR
 - **optimize** (`optimize/`) — IR-level constant folding, dead-code
   elimination, and common-subexpression elimination on the scalar program.
 - **codegen** (`codegen/`) — emits readable Python source from the lowered
-  IR (SSA names, real loop structure).
+  IR (SSA names, real loop structure). Conditions proven to depend only
+  on loop indices select whole branches in Python; array conditions use
+  `xp.where`.
 - **exec + wrap** (`emit.py`) — compiles the source and wraps it so the
   namespace is taken from the call arguments
   (`array_api_compat.array_namespace`); `vec.source` and
@@ -57,7 +59,9 @@ generated code calls small runtime helpers injected into its globals:
   for boolean/maybe-boolean/uint64 operands: implements the layered
   [exactness lattice](semantics.md#integer-exactness-lattice), including
   per-lane-exact uint64 `mod`/`floordiv` formulas for negative divisors
-  and result-aware subtraction.
+  and result-aware subtraction. Integer true division uses binary long
+  division with guard/sticky bits for correctly rounded float64 ratios,
+  without extracting array values into Python.
 
 The helpers live in `array_vectorize/runtime/` (`minmax.py`, `arith.py`,
 `dtype.py`), a stdlib-only leaf (enforced, with the other import

docs/semantics.md

@@ -15,6 +15,11 @@ enclosing where-select) and out of domain — live lanes are never touched
 disappear. Loop bodies and cross-function (helper) dead lanes are not
 tracked (conservative).
 
+Conditions built only from constant-trip loop indices and literals select
+one whole-array branch using Python selection. They do not promote the
+selected branch to the unused branch's dtype. Array-dependent conditions
+continue to select per lane with `xp.where`.
+
 ### `and`/`or`/`not` are exact
 
 Numeric operands lower to value-selects
@@ -40,6 +45,15 @@ call and checked at runtime on the actual values:
 4. **float64** only when per-lane results fit no single dtype (a huge
    uint64 plus a negative signed value, or mixed-magnitude differences).
 
+True division converts integer and boolean operands to floating arrays,
+including inputs whose dtype is known only at call time. Integer ratios
+round once to float64, without first rounding large integer operands.
+This uses a fixed bit loop, which costs more at call time and first JIT
+compilation than floating-point division. Negative integer
+literals (also when assigned to local names) use the exact unsigned
+remainder and floor-division paths. Unknown loop-carried entry values may
+be boolean, so their arithmetic also uses runtime dtype dispatch.
+
 ### Reject over miscompile
 
 Anything not provably translatable raises `VectorizationError` with all
@@ -63,4 +77,4 @@ values. These are deliberate, tested, and inherent:
 | bool arithmetic is integer (`True + True == 2`) | exact: bool operands are cast to float64 (strict backends reject bool arithmetic) |
 | scalar exceptions inside `verify=` | expected `NaN` lanes |
 | mixed int/float `min`/`max` siblings | strict backends require matching array dtypes; literals adopt a provably-int sibling's dtype, else float64 |
-| uint64 + signed arrays with mixed-sign per-lane results | float64 approximation (no single dtype holds both operand ranges) |
+| integer arithmetic with results outside every integer array dtype | float64 approximation (including uint64 divided by a negative literal below int64-min) |

src/array_vectorize/codegen/emitter.py

@@ -79,7 +79,30 @@ def _gen_literal(lit: ir.Literal, ns: str) -> ast.expr:
     return ast.Constant(value=value)
 
 
-def _gen_expr(node: ir.Node, ns: str) -> ast.expr:
+def _is_python_scalar(node: ir.Node, names: frozenset[str]) -> bool:
+    """Prove raw scalar expressions built only from literals and loop indices."""
+    match node:
+        case ir.Literal():
+            return True
+        case ir.Ref():
+            return node.name in names
+        case ir.BinOp():
+            return (
+                node.op in _BINOP_AST
+                and _is_python_scalar(node.left, names)
+                and _is_python_scalar(node.right, names)
+            )
+        case ir.UnaryOp():
+            return _is_python_scalar(node.operand, names)
+        case ir.Compare():
+            return _is_python_scalar(node.left, names) and _is_python_scalar(node.right, names)
+        case ir.Logical():
+            return all(_is_python_scalar(part, names) for part in node.parts)
+        case _:
+            return False
+
+
+def _gen_expr(node: ir.Node, ns: str, scalar_names: frozenset[str] = frozenset()) -> ast.expr:
     match node:
         case ir.Literal():
             return _gen_literal(node, ns)
@@ -91,43 +114,69 @@ def _gen_expr(node: ir.Node, ns: str) -> ast.expr:
             if node.op in _BINOP_AST:
                 return ast.BinOp(
                     op=_BINOP_AST[node.op](),
-                    left=_gen_expr(node.left, ns),
-                    right=_gen_expr(node.right, ns),
+                    left=_gen_expr(node.left, ns, scalar_names),
+                    right=_gen_expr(node.right, ns, scalar_names),
                 )
             return _xp_call(
-                ns, _BINOP_XP[node.op], [_gen_expr(node.left, ns), _gen_expr(node.right, ns)]
+                ns,
+                _BINOP_XP[node.op],
+                [_gen_expr(node.left, ns, scalar_names), _gen_expr(node.right, ns, scalar_names)],
             )
         case ir.UnaryOp():
             if node.op == "neg":
-                return ast.UnaryOp(op=ast.USub(), operand=_gen_expr(node.operand, ns))
+                return ast.UnaryOp(op=ast.USub(), operand=_gen_expr(node.operand, ns, scalar_names))
             if node.op == "pos":
-                return ast.UnaryOp(op=ast.UAdd(), operand=_gen_expr(node.operand, ns))
+                return ast.UnaryOp(op=ast.UAdd(), operand=_gen_expr(node.operand, ns, scalar_names))
             if node.op == "invert":
-                return ast.UnaryOp(op=ast.Invert(), operand=_gen_expr(node.operand, ns))
-            return _xp_call(ns, "logical_not", [_gen_expr(node.operand, ns)])
+                return ast.UnaryOp(
+                    op=ast.Invert(), operand=_gen_expr(node.operand, ns, scalar_names)
+                )
+            if _is_python_scalar(node.operand, scalar_names):
+                return ast.UnaryOp(op=ast.Not(), operand=_gen_expr(node.operand, ns, scalar_names))
+            return _xp_call(ns, "logical_not", [_gen_expr(node.operand, ns, scalar_names)])
         case ir.Compare():
             return ast.Compare(
-                left=_gen_expr(node.left, ns),
+                left=_gen_expr(node.left, ns, scalar_names),
                 ops=[_CMPOP_AST[node.op]()],
-                comparators=[_gen_expr(node.right, ns)],
+                comparators=[_gen_expr(node.right, ns, scalar_names)],
             )
         case ir.Logical():
+            if _is_python_scalar(node, scalar_names):
+                return ast.BoolOp(
+                    op=ast.And() if node.op == "and" else ast.Or(),
+                    values=[_gen_expr(part, ns, scalar_names) for part in node.parts],
+                )
             fn = "logical_and" if node.op == "and" else "logical_or"
-            folded = _gen_expr(node.parts[0], ns)
+            folded = _gen_expr(node.parts[0], ns, scalar_names)
             for part in node.parts[1:]:
-                folded = _xp_call(ns, fn, [folded, _gen_expr(part, ns)])
+                folded = _xp_call(ns, fn, [folded, _gen_expr(part, ns, scalar_names)])
             return folded
         case ir.Where():
+            if _is_python_scalar(node.cond, scalar_names):
+                # A loop-index condition selects one whole-array branch.
+                # Python selection preserves its dtype without sending a
+                # raw bool or incompatible branch dtypes to xp.where (D6).
+                return ast.IfExp(
+                    test=_gen_expr(node.cond, ns, scalar_names),
+                    body=_gen_expr(node.then, ns, scalar_names),
+                    orelse=_gen_expr(node.other, ns, scalar_names),
+                )
             return _xp_call(
                 ns,
                 "where",
-                [_gen_expr(node.cond, ns), _gen_expr(node.then, ns), _gen_expr(node.other, ns)],
+                [
+                    _gen_expr(node.cond, ns, scalar_names),
+                    _gen_expr(node.then, ns, scalar_names),
+                    _gen_expr(node.other, ns, scalar_names),
+                ],
             )
         case ir.Call():
-            return _xp_call(ns, node.fn, [_gen_expr(a, ns) for a in node.args])
+            return _xp_call(ns, node.fn, [_gen_expr(a, ns, scalar_names) for a in node.args])
         case ir.FuncCall():
             return ast.Call(
-                func=_load(node.fn), args=[_gen_expr(a, ns) for a in node.args], keywords=[]
+                func=_load(node.fn),
+                args=[_gen_expr(a, ns, scalar_names) for a in node.args],
+                keywords=[],
             )
         case _:
             assert_never(node)
@@ -200,15 +249,17 @@ def _gen_range_call(loop: ir.Loop, ns: str) -> ast.Call:
     return ast.Call(func=_load("range"), args=args, keywords=[])
 
 
-def _gen_stmt(stmt: ir.Stmt, ns: str) -> ast.stmt:
+def _gen_stmt(stmt: ir.Stmt, ns: str, scalar_names: frozenset[str] = frozenset()) -> ast.stmt:
     match stmt:
         case ir.Binding():
             return ast.Assign(
                 targets=[ast.Name(id=stmt.name, ctx=ast.Store())],
-                value=_gen_expr(stmt.expr, ns),
+                value=_gen_expr(stmt.expr, ns, scalar_names),
             )
         case ir.Loop():
-            body: list[ast.stmt] = [_gen_stmt(inner, ns) for inner in stmt.body]
+            body: list[ast.stmt] = [
+                _gen_stmt(inner, ns, scalar_names | {stmt.var}) for inner in stmt.body
+            ]
             if not body:
                 # (15) a retained loop with a fully dead body still needs a statement
                 body = [ast.Pass()]

src/array_vectorize/lower/expressions.py

@@ -15,6 +15,7 @@
 from array_vectorize import ir
 from array_vectorize.frontend import tables
 from array_vectorize.lower import sanitize
+from array_vectorize.optimize import constfold
 from array_vectorize.runtime import registry
 
 __all__ = ["_ExpressionLowerer"]
@@ -344,22 +345,46 @@ def _maybe_bool_result(self, node: ir.Node) -> bool:
 
     def _lower_binop(self, op: ast.operator, left: ir.Node, right: ir.Node) -> ir.Node:
         """Build a BinOp with the exactness fixes shared by `a op b` and `a op= b`."""
+        if isinstance(op, ast.FloorDiv | ast.Mod):
+            literal_left, literal_right = self._literal_value(left), self._literal_value(right)
+            if literal_left is not None and literal_right is not None:
+                # Keep foldable constants usable as loop bounds, while
+                # zero divisors and overflow retain runtime dispatch.
+                folded = constfold._fold_binop(_BINOPS[type(op)], literal_left, literal_right)
+                if folded is not None:
+                    return folded
         # Python bool arithmetic is integer (True + True == 2), but array
         # backends either saturate (bool + bool == True) or reject bools in
-        # arithmetic outright (strict backends). Cast bool-typed operands to
-        # float64: exact for bools (0/1) and ints up to 2**53, and a no-op
-        # for floats — so loop-carried variables whose kind changes across
-        # iterations stay correct too.
+        # arithmetic outright (strict backends). Runtime dispatch chooses
+        # a numeric dtype without rounding integer operands, including
+        # loop-carried values whose kind changes across iterations.
         if isinstance(op, ast.Add | ast.Sub | ast.Mult | ast.Div | ast.FloorDiv | ast.Mod) and (
             "bool" in (self._numeric_kind(left), self._numeric_kind(right))
             or self._maybe_bool_result(left)
             or self._maybe_bool_result(right)
+            # True division requires floating operands even when input
+            # kinds are unknown. Negative integer literals cannot be
+            # promoted into uint64 by a bare backend operator.
+            or (
+                isinstance(op, ast.Div)
+                and (self._numeric_kind(left) != "float" or self._numeric_kind(right) != "float")
+            )
+            or (
+                isinstance(op, ast.FloorDiv | ast.Mod)
+                and (
+                    self._is_negative_int(self._literal_value(left) or left)
+                    or self._is_negative_int(self._literal_value(right) or right)
+                )
+            )
         ):
             # the whole operation goes through the runtime _vec_arith
             # helper: bools need a numeric representation, strict
             # backends require single-dtype or float operands, and the
             # uint64 integer paths are exact per lane (modular for
             # add/sub/mul; int64 magnitudes for negative divisors)
+            if isinstance(op, ast.FloorDiv | ast.Mod):
+                left = self._literal_value(left) or left
+                right = self._literal_value(right) or right
             ir_op = _BINOPS[type(op)]
             return ir.FuncCall(
                 self.arith_name,

src/array_vectorize/lower/kinds.py

@@ -17,8 +17,8 @@
   Python scalar (parameter default, loop variable, literal binding, or a
   local computed from one). Operators promote scalars fine; ``xp.*``
   function arguments do not (strict backends reject plain scalars).
-- ``maybe_bool`` (was ``_maybe_bool_names``): the value is a min/max
-  result with unknown static kind whose runtime dtype may be boolean, so
+- ``maybe_bool`` (was ``_maybe_bool_names``): an unknown min/max result
+  or loop-carried entry value may have boolean dtype at runtime, so
   arithmetic must use the runtime-polymorphic intify.
 - carried-assign kinds (was ``_carried_assign_kinds``): per active loop,
   the kinds assigned to loop-carried names in the body; a carried

src/array_vectorize/lower/loops.py

@@ -125,7 +125,9 @@ def lower_for(self, stmt: ast.For) -> None:
             # scalar stays a raw scalar, so track that for call sites
             if self.kinds.is_scalar(pre_name):
                 self.kinds.mark_scalar(loop_carried_name)
-            if self.kinds.is_maybe_bool(pre_name):
+            if self.kinds.kind(pre_name) is None or self.kinds.is_maybe_bool(pre_name):
+                # Unknown entry values can be boolean arrays even when
+                # every body assignment has the same unknown static kind.
                 self.kinds.mark_maybe_bool(loop_carried_name)
 
         phi_end = len(self.bindings)

src/array_vectorize/lower/statements.py

@@ -46,8 +46,8 @@ def lower_assign(self, stmt: ast.Assign | ast.AugAssign) -> None:
         self.definite[var] = name
         kind = self._numeric_kind(value)
         self.kinds.set_kind(name, kind)
-        if isinstance(value, ir.Literal):
-            self.kinds.set_literal(name, value)
+        if (literal := self._literal_value(value)) is not None:
+            self.kinds.set_literal(name, literal)
         else:
             self.kinds.drop_literal(name)
         if self._possibly_scalar(value):