Continue Phase 9a: int/bytes subclass interop with builtins

Enable int/bytes subclass instances to work seamlessly with Python
builtins and operators. Key changes: hex/bin/oct/range/divmod accept
instances with wrappedValue, list indexing/slicing coerces instance
indices, comparison operators unwrap instances for sorted() support,
and bytes gains __radd__/__lt__/__le__/__gt__/__ge__ dunder dispatch.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: pirapira

LeanPython/Interpreter/Eval.lean

@@ -60,21 +60,47 @@ private def dummySpan : SourceSpan :=
   { start := { line := 0, column := 0, offset := 0 }
     stop := { line := 0, column := 0, offset := 0 } }
 
-private def computeSliceIndices (len : Int) (startOpt stopOpt stepOpt : Option Value)
+/-- Try to coerce a Value to Int for indexing (handles int subclass instances). -/
+private def coerceToInt (v : Value) : Option Int :=
+  match v with
+  | .int n => some n
+  | .bool b => some (if b then 1 else 0)
+  | _ => none
+
+/-- Try to coerce a Value to Int, including instances with wrappedValue. -/
+private partial def coerceToIntM (v : Value) : InterpM (Option Int) := do
+  match v with
+  | .int n => pure (some n)
+  | .bool b => pure (some (if b then 1 else 0))
+  | .instance iref => do
+    let id_ ← heapGetInstanceData iref
+    match id_.wrappedValue with
+    | some (.int n) => pure (some n)
+    | _ => pure none
+  | _ => pure none
+
+private partial def computeSliceIndices (len : Int) (startOpt stopOpt stepOpt : Option Value)
     : InterpM (Int × Int × Int) := do
-  let step : Int := match stepOpt with
-    | some (.int s) => s
-    | some (.none) | none => 1
-    | _ => 1
+  let extractSliceInt (v : Value) : InterpM (Option Int) := coerceToIntM v
+  let step : Int ← match stepOpt with
+    | some v => do
+      match ← extractSliceInt v with
+      | some s => pure s
+      | none => pure 1
+    | none => pure 1
   if step == 0 then throwValueError "slice step cannot be zero"
-  let start : Int := match startOpt with
-    | some (.int s) => if s < 0 then max 0 (len + s) else min s len
-    | some (.none) | none => if step > 0 then 0 else len - 1
-    | _ => if step > 0 then 0 else len - 1
-  let stop : Int := match stopOpt with
-    | some (.int s) => if s < 0 then max 0 (len + s) else min s len
-    | some (.none) | none => if step > 0 then len else -1
-    | _ => if step > 0 then len else -1
+  let start : Int ← match startOpt with
+    | some v => do
+      match ← extractSliceInt v with
+      | some s => pure (if s < 0 then max 0 (len + s) else min s len)
+      | none => pure (if step > 0 then 0 else len - 1)
+    | none => pure (if step > 0 then 0 else len - 1)
+  let stop : Int ← match stopOpt with
+    | some v => do
+      match ← extractSliceInt v with
+      | some s => pure (if s < 0 then max 0 (len + s) else min s len)
+      | none => pure (if step > 0 then len else -1)
+    | none => pure (if step > 0 then len else -1)
   return (start, stop, step)
 
 private def sliceIndices (start stop step : Int) : List Nat :=
@@ -1659,6 +1685,9 @@ partial def callValueDispatch (callee : Value) (args : List Value)
         | "__add__" => match args with
           | [a, b] => return .bytes ((← extractBytes a) ++ (← extractBytes b))
           | _ => throwTypeError "bytes.__add__ takes 2 arguments"
+        | "__radd__" => match args with
+          | [a, b] => return .bytes ((← extractBytes b) ++ (← extractBytes a))
+          | _ => throwTypeError "bytes.__radd__ takes 2 arguments"
         | "__mul__" | "__rmul__" => match args with
           | [a, .int n] => do
             let b ← extractBytes a
@@ -1674,6 +1703,26 @@ partial def callValueDispatch (callee : Value) (args : List Value)
         | "__ne__" => match args with
           | [a, b] => return .bool ((← extractBytes a) != (← extractBytes b))
           | _ => throwTypeError "bytes.__ne__ takes 2 arguments"
+        | "__lt__" => match args with
+          | [a, b] => do
+            let ba ← extractBytes a; let bb ← extractBytes b
+            return .bool (ba.toList < bb.toList)
+          | _ => throwTypeError "bytes.__lt__ takes 2 arguments"
+        | "__le__" => match args with
+          | [a, b] => do
+            let ba ← extractBytes a; let bb ← extractBytes b
+            return .bool (ba.toList < bb.toList || ba == bb)
+          | _ => throwTypeError "bytes.__le__ takes 2 arguments"
+        | "__gt__" => match args with
+          | [a, b] => do
+            let ba ← extractBytes a; let bb ← extractBytes b
+            return .bool (bb.toList < ba.toList)
+          | _ => throwTypeError "bytes.__gt__ takes 2 arguments"
+        | "__ge__" => match args with
+          | [a, b] => do
+            let ba ← extractBytes a; let bb ← extractBytes b
+            return .bool (bb.toList < ba.toList || ba == bb)
+          | _ => throwTypeError "bytes.__ge__ takes 2 arguments"
         | "__hash__" => match args with
           | [a] => do
             let b ← extractBytes a
@@ -2382,6 +2431,15 @@ partial def getAttributeValue (obj : Value) (attr : String) : InterpM Value := d
 
 -- Subscript access
 partial def evalSubscriptValue (obj idx : Value) : InterpM Value := do
+  -- Coerce instance indices with wrappedValue to plain .int
+  let idx ← do
+    match idx with
+    | .instance iref =>
+      let id_ ← heapGetInstanceData iref
+      match id_.wrappedValue with
+      | some (.int n) => pure (.int n)
+      | _ => pure idx
+    | _ => pure idx
   match obj with
   | .list ref => do
     let arr ← heapGetList ref

LeanPython/Runtime/Builtins.lean

@@ -36,6 +36,22 @@ open LeanPython.Stdlib.Os
 open LeanPython.Stdlib.Time
 open LeanPython.Stdlib.Logging
 
+-- ============================================================
+-- Helpers
+-- ============================================================
+
+/-- Extract an Int from a Value, handling int subclass instances (wrappedValue). -/
+partial def extractIntValue (v : Value) : InterpM Int := do
+  match v with
+  | .int n => pure n
+  | .bool b => pure (if b then 1 else 0)
+  | .instance iref => do
+    let id_ ← heapGetInstanceData iref
+    match id_.wrappedValue with
+    | some (.int n) => pure n
+    | _ => throwTypeError s!"'{typeName v}' cannot be interpreted as an integer"
+  | _ => throwTypeError s!"'{typeName v}' cannot be interpreted as an integer"
+
 -- ============================================================
 -- Individual builtin implementations
 -- ============================================================
@@ -71,10 +87,11 @@ partial def builtinLen (args : List Value) : InterpM Value := do
 /-- `range(stop)` or `range(start, stop[, step])` - materializes to list. -/
 partial def builtinRange (args : List Value) : InterpM Value := do
   let (start_, stop_, step_) ← match args with
-    | [.int n] => pure (0, n, (1 : Int))
-    | [.int s, .int e] => pure (s, e, (1 : Int))
-    | [.int s, .int e, .int st] => pure (s, e, st)
-    | [.bool b] => pure (0, (if b then 1 else 0 : Int), (1 : Int))
+    | [a] => do let n ← extractIntValue a; pure (0, n, (1 : Int))
+    | [a, b] => do let s ← extractIntValue a; let e ← extractIntValue b; pure (s, e, (1 : Int))
+    | [a, b, c] => do
+      let s ← extractIntValue a; let e ← extractIntValue b; let st ← extractIntValue c
+      pure (s, e, st)
     | _ => throwTypeError "range() requires int arguments"
   if step_ == 0 then
     throwValueError "range() arg 3 must not be zero"
@@ -482,9 +499,11 @@ def builtinPow (args : List Value) : InterpM Value := do
   | _ => throwTypeError "pow() takes 2 or 3 arguments"
 
 /-- `divmod(a, b)` -/
-def builtinDivmod (args : List Value) : InterpM Value := do
+partial def builtinDivmod (args : List Value) : InterpM Value := do
   match args with
-  | [.int a, .int b] =>
+  | [va, vb] => do
+    let a ← extractIntValue va
+    let b ← extractIntValue vb
     if b == 0 then throwZeroDivision "integer division or modulo by zero"
     else return .tuple #[.int (Int.fdiv a b), .int (Int.fmod a b)]
   | _ => throwTypeError "divmod() requires two integer arguments"
@@ -634,23 +653,26 @@ partial def callBuiltin (name : String) (args : List Value)
     | _ => throwTypeError "input() takes at most 1 argument"
   | "hex" => do
     match args with
-    | [.int n] =>
+    | [v] => do
+      let n ← extractIntValue v
       let digits := Nat.toDigits 16 n.natAbs
       let s := String.ofList digits
       if n >= 0 then return .str s!"0x{s}"
       else return .str s!"-0x{s}"
     | _ => throwTypeError "hex() takes exactly one argument"
   | "oct" => do
     match args with
-    | [.int n] =>
+    | [v] => do
+      let n ← extractIntValue v
       let digits := Nat.toDigits 8 n.natAbs
       let s := String.ofList digits
       if n >= 0 then return .str s!"0o{s}"
       else return .str s!"-0o{s}"
     | _ => throwTypeError "oct() takes exactly one argument"
   | "bin" => do
     match args with
-    | [.int n] =>
+    | [v] => do
+      let n ← extractIntValue v
       let digits := Nat.toDigits 2 n.natAbs
       let s := String.ofList digits
       if n >= 0 then return .str s!"0b{s}"

LeanPython/Runtime/Ops.lean

@@ -594,42 +594,59 @@ private def isIdentical : Value → Value → Bool
   | .instance a, .instance b => a == b
   | _, _ => false
 
+/-- Unwrap an instance's wrappedValue to a primitive value for comparison. -/
+private partial def unwrapForCmp (v : Value) : InterpM Value := do
+  match v with
+  | .instance iref =>
+    let id_ ← heapGetInstanceData iref
+    match id_.wrappedValue with
+    | some inner => pure inner
+    | none => pure v
+  | _ => pure v
+
 /-- Evaluate a single comparison operation. -/
-partial def evalCmpOp (op : CmpOp) (left right : Value) : InterpM Bool :=
+partial def evalCmpOp (op : CmpOp) (left right : Value) : InterpM Bool := do
+  -- Unwrap instances with wrappedValue for comparison dispatch
+  let left' ← unwrapForCmp left
+  let right' ← unwrapForCmp right
   match op with
   | .eq => valueEq left right
   | .notEq => do return !(← valueEq left right)
   | .lt => do
-    match ← numericCompare left right with
+    match ← numericCompare left' right' with
     | some .lt => return true
     | some _ => return false
     | none =>
-      match left, right with
+      match left', right' with
       | .str a, .str b => return (a < b)
+      | .bytes a, .bytes b => return (a.toList < b.toList)
       | _, _ => throwTypeError s!"'<' not supported between instances of '{typeName left}' and '{typeName right}'"
   | .ltE => do
-    match ← numericCompare left right with
+    match ← numericCompare left' right' with
     | some .gt => return false
     | some _ => return true
     | none =>
-      match left, right with
+      match left', right' with
       | .str a, .str b => return (decide (a ≤ b))
+      | .bytes a, .bytes b => return (a.toList < b.toList || a == b)
       | _, _ => throwTypeError s!"'<=' not supported between instances of '{typeName left}' and '{typeName right}'"
   | .gt => do
-    match ← numericCompare left right with
+    match ← numericCompare left' right' with
     | some .gt => return true
     | some _ => return false
     | none =>
-      match left, right with
+      match left', right' with
       | .str a, .str b => return (decide (a > b))
+      | .bytes a, .bytes b => return (b.toList < a.toList)
       | _, _ => throwTypeError s!"'>' not supported between instances of '{typeName left}' and '{typeName right}'"
   | .gtE => do
-    match ← numericCompare left right with
+    match ← numericCompare left' right' with
     | some .lt => return false
     | some _ => return true
     | none =>
-      match left, right with
+      match left', right' with
       | .str a, .str b => return (decide (a ≥ b))
+      | .bytes a, .bytes b => return (b.toList < a.toList || a == b)
       | _, _ => throwTypeError s!"'>=' not supported between instances of '{typeName left}' and '{typeName right}'"
   | .is_ => return (isIdentical left right)
   | .isNot => return (!isIdentical left right)

LeanPythonTest/Stdlib.lean

@@ -826,3 +826,61 @@ private def assertPyError (source errSubstr : String) : IO Unit := do
 
 -- @classmethod + @override stacking (leanSpec pattern)
 #eval assertPy "from abc import ABC, abstractmethod\nfrom typing import override\nclass SSZType(ABC):\n    @classmethod\n    @abstractmethod\n    def is_fixed_size(cls):\n        pass\n    @classmethod\n    @abstractmethod\n    def get_byte_length(cls):\n        pass\nclass BaseUint(int, SSZType):\n    __slots__ = ()\n    BITS = 64\n    def __new__(cls, value):\n        return super().__new__(cls, int(value))\n    @classmethod\n    @override\n    def is_fixed_size(cls):\n        return True\n    @classmethod\n    @override\n    def get_byte_length(cls):\n        return cls.BITS // 8\nclass Uint64(BaseUint):\n    BITS = 64\nprint(Uint64.is_fixed_size())\nprint(Uint64.get_byte_length())" "True\n8\n"
+
+-- ============================================================
+-- Phase 9a continued: int/bytes subclass interop with builtins
+-- ============================================================
+
+-- hex() on int subclass instance
+#eval assertPy "class BaseUint(int):\n    def __new__(cls, value):\n        return super().__new__(cls, int(value))\nclass Uint64(BaseUint):\n    pass\nprint(hex(Uint64(42)))\nprint(hex(Uint64(255)))" "0x2a\n0xff\n"
+
+-- bin() on int subclass instance
+#eval assertPy "class BaseUint(int):\n    def __new__(cls, value):\n        return super().__new__(cls, int(value))\nclass Uint8(BaseUint):\n    pass\nprint(bin(Uint8(42)))" "0b101010\n"
+
+-- oct() on int subclass instance
+#eval assertPy "class BaseUint(int):\n    def __new__(cls, value):\n        return super().__new__(cls, int(value))\nclass Uint8(BaseUint):\n    pass\nprint(oct(Uint8(42)))" "0o52\n"
+
+-- range() with int subclass instances
+#eval assertPy "class BaseUint(int):\n    def __new__(cls, value):\n        return super().__new__(cls, int(value))\nclass Uint8(BaseUint):\n    pass\nresult = list(range(Uint8(5)))\nprint(result)" "[0, 1, 2, 3, 4]\n"
+
+-- range(start, stop, step) with int subclass instances
+#eval assertPy "class BaseUint(int):\n    def __new__(cls, value):\n        return super().__new__(cls, int(value))\nclass Uint8(BaseUint):\n    pass\nresult = list(range(Uint8(2), Uint8(8), Uint8(2)))\nprint(result)" "[2, 4, 6]\n"
+
+-- divmod() with int subclass instances
+#eval assertPy "class BaseUint(int):\n    def __new__(cls, value):\n        return super().__new__(cls, int(value))\nclass Uint64(BaseUint):\n    pass\nresult = divmod(Uint64(100), Uint64(3))\nprint(result[0])\nprint(result[1])" "33\n1\n"
+
+-- List indexing with int subclass instance
+#eval assertPy "class BaseUint(int):\n    def __new__(cls, value):\n        return super().__new__(cls, int(value))\nclass Uint64(BaseUint):\n    pass\ndata = ['a', 'b', 'c', 'd', 'e']\nprint(data[Uint64(2)])\nprint(data[Uint64(0)])\nprint(data[Uint64(4)])" "c\na\ne\n"
+
+-- Slice with int subclass instances
+#eval assertPy "class BaseUint(int):\n    def __new__(cls, value):\n        return super().__new__(cls, int(value))\nclass Uint8(BaseUint):\n    pass\ndata = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9]\nprint(data[Uint8(2):Uint8(7)])" "[2, 3, 4, 5, 6]\n"
+
+-- repr() and str() on int subclass via Python-defined __repr__/__str__
+#eval assertPy "class BaseUint(int):\n    def __new__(cls, value):\n        return super().__new__(cls, int(value))\n    def __repr__(self):\n        return type(self).__name__ + '(' + str(int(self)) + ')'\n    def __str__(self):\n        return str(int(self))\nclass Uint64(BaseUint):\n    pass\nx = Uint64(42)\nprint(repr(x))\nprint(str(x))" "Uint64(42)\n42\n"
+
+-- int() conversion of int subclass instance
+#eval assertPy "class BaseUint(int):\n    def __new__(cls, value):\n        return super().__new__(cls, int(value))\nclass Uint64(BaseUint):\n    pass\nx = Uint64(42)\nresult = int(x)\nprint(result)\nprint(result == 42)" "42\nTrue\n"
+
+-- bytes.__radd__: b"\xff" + bytes_subclass_instance
+#eval assertPy "class BaseBytes(bytes):\n    def __new__(cls, value=b''):\n        return super().__new__(cls, value)\nclass Bytes4(BaseBytes):\n    pass\nx = Bytes4(b'\\x01\\x02\\x03\\x04')\nresult = b'\\xff' + x\nprint(len(result))\nprint(result[0])\nprint(result[4])" "5\n255\n4\n"
+
+-- sorted() on bytes subclass instances (lexicographic)
+#eval assertPy "class BaseBytes(bytes):\n    def __new__(cls, value=b''):\n        return super().__new__(cls, value)\nclass Bytes4(BaseBytes):\n    pass\na = Bytes4(b'\\x00\\x00\\x00\\x02')\nb = Bytes4(b'\\x00\\x00\\x00\\x01')\nc = Bytes4(b'\\xff\\xff\\xff\\xff')\nresult = sorted([c, a, b])\nprint(bytes(result[0]).hex())\nprint(bytes(result[1]).hex())\nprint(bytes(result[2]).hex())" "00000001\n00000002\nffffffff\n"
+
+-- In-place operators: x += Uint64(5)
+#eval assertPy "class BaseUint(int):\n    def __new__(cls, value):\n        return super().__new__(cls, int(value))\n    def __add__(self, other):\n        return type(self)(int(self) + int(other))\nclass Uint64(BaseUint):\n    pass\nx = Uint64(10)\ny = x\nx += Uint64(5)\nprint(int(x))\nprint(type(x).__name__)\nprint(int(y))" "15\nUint64\n10\n"
+
+-- Reverse operators: plain int + Uint raises TypeError when __radd__ checks type
+#eval assertPy "class BaseUint(int):\n    def __new__(cls, value):\n        return super().__new__(cls, int(value))\n    def __radd__(self, other):\n        if not isinstance(other, BaseUint):\n            raise TypeError('bad type for +')\n        return type(self)(int(other) + int(self))\nclass Uint64(BaseUint):\n    pass\ntry:\n    result = 100 + Uint64(3)\n    print('no error')\nexcept TypeError as e:\n    print(str(e))" "bad type for +\n"
+
+-- io.BytesIO seek and read round-trip
+#eval assertPy "import io\nstream = io.BytesIO()\nstream.write(b'\\x01\\x02\\x03\\x04')\nstream.seek(0)\ndata = stream.read()\nprint(len(data))\nprint(data[0])\nprint(data[3])" "4\n1\n4\n"
+
+-- BaseBytes __add__ returns raw bytes
+#eval assertPy "class BaseBytes(bytes):\n    def __new__(cls, value=b''):\n        return super().__new__(cls, value)\nclass Bytes4(BaseBytes):\n    pass\na = Bytes4(b'\\x01\\x02\\x03\\x04')\nb = Bytes4(b'\\x05\\x06\\x07\\x08')\nresult = a + b\nprint(len(result))\nprint(result[0])\nprint(result[7])" "8\n1\n8\n"
+
+-- Boolean type: construction, validation, arithmetic rejection
+#eval assertPy "class Boolean(int):\n    def __new__(cls, value):\n        if not isinstance(value, int):\n            raise TypeError('Expected bool or int')\n        if value not in (0, 1):\n            raise ValueError('Boolean value must be 0 or 1')\n        return super().__new__(cls, value)\n    def __add__(self, other):\n        raise TypeError('Arithmetic not supported for Boolean.')\n    def __eq__(self, other):\n        return isinstance(other, int) and int(self) == int(other)\nbt = Boolean(True)\nbf = Boolean(False)\nprint(int(bt))\nprint(int(bf))\nprint(bt == 1)\nprint(bf == 0)\ntry:\n    bt + bf\nexcept TypeError as e:\n    print(str(e))" "1\n0\nTrue\nTrue\nArithmetic not supported for Boolean.\n"
+
+-- Boolean rejects invalid values
+#eval assertPyError "class Boolean(int):\n    def __new__(cls, value):\n        if value not in (0, 1):\n            raise ValueError('must be 0 or 1')\n        return super().__new__(cls, value)\nBoolean(2)" "must be 0 or 1"