Begin Phase 9a: built-in type subclassing for leanSpec primitive types

Enable Python patterns like `class BaseUint(int, SSZType)` by introducing
synthetic class objects for built-in types (int, bytes, object) that
participate in MRO computation and provide dunder method dispatch.

Key changes:
- Add wrappedValue to InstanceData for int/bytes subclass instances
- Create synthetic classObj for int/bytes/object with full dunder namespaces
- Implement int.__new__ via super().__new__ for subclass construction
- Add all int arithmetic/bitwise/comparison dunder methods as builtins
- Fix super() to work in __new__ (cls fallback) and with classObj instances
- Support custom exception class hierarchy (construction, raise, except)
- Make typing.override a callable identity decorator
- Improve tuple hashing and isinstance for built-in type subclasses

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

Author: pirapira

LeanPython/Interpreter/Eval.lean

@@ -52,6 +52,7 @@ structure InterpreterState where
   currentFile    : Option String
   currentPackage : Option String
   defaultFactories : Std.HashMap Nat Value := {}
+  builtinTypeClasses : Std.HashMap String Value := {}
   deriving Inhabited
 
 /-- Create a fresh interpreter state. -/

LeanPython/Interpreter/Types.lean

@@ -98,6 +98,7 @@ partial def builtinType (args : List Value) : InterpM Value := do
     | .instance ref => do
       let id_ ← heapGetInstanceData ref
       return id_.cls
+    | .exception typeName _ => return .builtin typeName
     | _ => return .str s!"<class '{typeName v}'>"
   | _ => throwTypeError "type() takes 1 or 3 arguments"
 
@@ -112,6 +113,11 @@ def builtinInt (args : List Value) : InterpM Value := do
     match s.toList.dropWhile Char.isWhitespace |>.reverse |>.dropWhile Char.isWhitespace |>.reverse |> String.ofList |>.toInt? with
     | some n => return .int n
     | none => throwValueError s!"invalid literal for int() with base 10: '{s}'"
+  | [.instance iref] => do
+    let id_ ← heapGetInstanceData iref
+    match id_.wrappedValue with
+    | some (.int n) => return .int n
+    | _ => throwTypeError "int() argument must be a string or a number"
   | _ => throwTypeError "int() argument must be a string or a number"
 
 /-- `float(x)` - convert to float. -/
@@ -320,6 +326,7 @@ partial def builtinIsinstance (args : List Value) : InterpM Value := do
     match name with
     | "object" => return .bool true  -- everything is an instance of object
     | _ =>
+      -- First check if it's a direct built-in value match
       let tn := typeName obj
       let isMatch := match name with
         | "int" => tn == "int" || tn == "bool"
@@ -332,7 +339,24 @@ partial def builtinIsinstance (args : List Value) : InterpM Value := do
         | "set" => tn == "set"
         | "bytes" => tn == "bytes"
         | _ => false
-      return .bool isMatch
+      if isMatch then return .bool true
+      -- For instances, check if any class in MRO is the synthetic built-in type
+      match obj with
+      | .instance iref => do
+        let id_ ← heapGetInstanceData iref
+        match id_.cls with
+        | .classObj cref => do
+          let cd ← heapGetClassData cref
+          let mut found := false
+          for mroEntry in cd.mro do
+            match mroEntry with
+            | .classObj mref => do
+              let mcd ← heapGetClassData mref
+              if mcd.name == name then found := true
+            | _ => pure ()
+          return .bool found
+        | _ => return .bool false
+      | _ => return .bool false
   | [.instance instRef, .classObj _] =>
     return .bool (← isInstanceOfClass instRef args[1]!)
   | [.instance instRef, .tuple classes] => do
@@ -341,22 +365,52 @@ partial def builtinIsinstance (args : List Value) : InterpM Value := do
       match cls with
       | .classObj _ =>
         if ← isInstanceOfClass instRef cls then return .bool true
-      | .builtin "object" => return .bool true
+      | .builtin bname => do
+        if bname == "object" then return .bool true
+        -- Check MRO for synthetic built-in type
+        let id_ ← heapGetInstanceData instRef
+        match id_.cls with
+        | .classObj cref => do
+          let cd ← heapGetClassData cref
+          for mroEntry in cd.mro do
+            match mroEntry with
+            | .classObj mref => do
+              let mcd ← heapGetClassData mref
+              if mcd.name == bname then return .bool true
+            | _ => pure ()
+        | _ => pure ()
       | _ => pure ()
     return .bool false
   | [_, .classObj _] => return .bool false  -- non-instance is not an instance of a custom class
   | _ => throwTypeError "isinstance() takes 2 arguments"
 
+/-- Hash a single value for tuple/object hashing. -/
+private partial def hashValue : Value → InterpM Int
+  | .int n => pure n
+  | .bool b => pure (if b then 1 else 0)
+  | .str s => pure (hash s).toNat
+  | .none => pure 0x345678
+  | .float f => pure (hash (toString f)).toNat
+  | .tuple items => do
+    -- Combine element hashes using simple mixing
+    let mut h : Int := 0x345678
+    for item in items do
+      let ih ← hashValue item
+      h := h * 1000003 + ih
+    pure h
+  | .classObj ref => pure ref
+  | .instance iref => do
+    let id_ ← heapGetInstanceData iref
+    match id_.wrappedValue with
+    | some v => hashValue v
+    | none => pure iref  -- use heap ref as fallback
+  | _ => pure 0
+
 /-- `hash(obj)` - basic hash. -/
-def builtinHash (args : List Value) : InterpM Value := do
+partial def builtinHash (args : List Value) : InterpM Value := do
   match args with
-  | [.int n] => return .int n
-  | [.bool b] => return .int (if b then 1 else 0)
-  | [.str s] => return .int (hash s).toNat
-  | [.none] => return .int 0
-  | [.float _f] => return .int 0  -- stub
-  | [.tuple _] => return .int 0  -- stub
-  | _ => throwTypeError "unhashable type"
+  | [v] => return .int (← hashValue v)
+  | _ => throwTypeError "hash() takes exactly 1 argument"
 
 /-- `id(obj)` - identity (stub). -/
 def builtinId (args : List Value) : InterpM Value := do
@@ -528,10 +582,13 @@ partial def callBuiltin (name : String) (args : List Value)
   | "super" => do
     match args with
     | [] => do
-      -- Implicit super(): look up __class__ and self from current scope
+      -- Implicit super(): look up __class__ and first param from current scope
       let cls ← lookupVariable "__class__"
-      let self ← lookupVariable "self"
-      return .superObj cls self
+      -- Try "self" first, then "cls" (for __new__/classmethods)
+      let inst ← try lookupVariable "self"
+        catch _ => try lookupVariable "cls"
+          catch _ => throwTypeError "super(): __class__ cell not found"
+      return .superObj cls inst
     | [cls, inst] => return .superObj cls inst
     | _ => throwTypeError "super() takes 0 or 2 arguments"
   | "hash"       => builtinHash args
@@ -775,6 +832,10 @@ partial def callBuiltin (name : String) (args : List Value)
     match args with
     | [f] => return f
     | _ => throwTypeError "abstractmethod() takes exactly 1 argument"
+  | "typing.override" => do
+    match args with
+    | [f] => return f
+    | _ => throwTypeError "override() takes exactly 1 argument"
   -- ============================================================
   -- dataclasses module functions
   -- ============================================================

LeanPython/Runtime/Builtins.lean

@@ -178,9 +178,7 @@ partial def valueToStr (v : Value) : InterpM String :=
     return s!"<function {fd.name}>"
   | .builtin name => return s!"<built-in function {name}>"
   | .boundMethod _ method => return s!"<bound method {method}>"
-  | .exception typeName msg =>
-    if msg.isEmpty then return typeName
-    else return s!"{typeName}({msg})"
+  | .exception _typeName msg => return msg
   | .generator _ => return "<generator object>"
   | .classObj ref => do
     let cd ← heapGetClassData ref

LeanPython/Runtime/Ops.lean

@@ -85,10 +85,13 @@ structure ClassData where
   ns        : Std.HashMap String Value
   slots     : Option (Array String) := none
 
-/-- Runtime instance data stored on the heap. -/
+/-- Runtime instance data stored on the heap.
+    `wrappedValue` stores the underlying built-in value for subclasses of int/bytes
+    (e.g., `class Uint64(int, SSZType)` produces instances with `wrappedValue := some (.int n)`). -/
 structure InstanceData where
   cls   : Value
   attrs : Std.HashMap String Value
+  wrappedValue : Option Value := none
 
 /-- Runtime module data stored on the heap. -/
 structure ModuleData where
@@ -133,6 +136,7 @@ inductive RuntimeError where
   | runtimeError    : String → RuntimeError
   | importError     : String → RuntimeError
   | moduleNotFound  : String → RuntimeError
+  | customError     : String → String → List String → RuntimeError  -- typeName, message, parentTypeNames
   deriving Repr
 
 instance : ToString RuntimeError where
@@ -151,6 +155,7 @@ instance : ToString RuntimeError where
     | .runtimeError s    => s!"RuntimeError: {s}"
     | .importError s     => s!"ImportError: {s}"
     | .moduleNotFound s  => s!"ModuleNotFoundError: No module named '{s}'"
+    | .customError tn msg _ => if msg.isEmpty then tn else s!"{tn}: {msg}"
 
 -- ============================================================
 -- BEq Value (needed for dict lookup, == operator, in operator)
@@ -221,9 +226,10 @@ partial def Value.toStr : Value → String
   | .int n => toString n
   | .float f =>
     let s := toString f
-    -- Lean's Float.toString may not match Python exactly, but good enough
     s
   | .str s => s
+  -- str(exception) returns just the message (not the type name)
+  | .exception _typeName msg => msg
   | .bytes _b => "b'...'"
   | .list _ => "[...]"
   | .tuple elems =>
@@ -237,7 +243,6 @@ partial def Value.toStr : Value → String
   | .builtin name => s!"<built-in function {name}>"
   | .ellipsis => "Ellipsis"
   | .boundMethod _ method => s!"<bound method {method}>"
-  | .exception typeName msg => if msg.isEmpty then typeName else s!"{typeName}({msg})"
   | .generator _ => "<generator object>"
   | .classObj _ => "<class>"
   | .instance _ => "<instance>"
@@ -268,7 +273,7 @@ partial def Value.toRepr : Value → String
   | .builtin name => s!"<built-in function {name}>"
   | .ellipsis => "Ellipsis"
   | .boundMethod _ method => s!"<bound method {method}>"
-  | .exception typeName msg => if msg.isEmpty then typeName else s!"{typeName}({msg})"
+  | .exception typeName msg => if msg.isEmpty then typeName else s!"{typeName}('{msg}')"
   | .generator _ => "<generator object>"
   | .classObj _ => "<class>"
   | .instance _ => "<instance>"
@@ -301,6 +306,7 @@ def runtimeErrorTypeName : RuntimeError → String
   | .runtimeError _   => "RuntimeError"
   | .importError _    => "ImportError"
   | .moduleNotFound _ => "ModuleNotFoundError"
+  | .customError tn _ _ => tn
 
 /-- Get the message portion of a RuntimeError. -/
 def runtimeErrorMessage : RuntimeError → String
@@ -309,6 +315,7 @@ def runtimeErrorMessage : RuntimeError → String
   | .attributeError s | .overflowError s | .notImplemented s
   | .runtimeError s | .importError s | .moduleNotFound s => s
   | .stopIteration => ""
+  | .customError _ msg _ => msg
 
 /-- Check if an exception type matches a handler type, respecting the hierarchy.
     `Exception` catches all standard errors, `BaseException` catches everything. -/
@@ -321,6 +328,14 @@ def exceptionMatches (errorTypeName handlerTypeName : String) : Bool :=
   else
     errorTypeName == handlerTypeName
 
+/-- Check if a custom exception matches a handler, considering parent type names. -/
+def customExceptionMatches (error : RuntimeError) (handlerTypeName : String) : Bool :=
+  match error with
+  | .customError tn _ parents =>
+    if handlerTypeName == "BaseException" || handlerTypeName == "Exception" then true
+    else tn == handlerTypeName || parents.any (· == handlerTypeName)
+  | other => exceptionMatches (runtimeErrorTypeName other) handlerTypeName
+
 -- ============================================================
 -- Builtin name table
 -- ============================================================
@@ -350,4 +365,18 @@ def builtinNames : List String :=
 def isBuiltinName (name : String) : Bool :=
   builtinNames.contains name
 
+/-- Check if a name is a built-in exception class. -/
+def isBuiltinExceptionName (name : String) : Bool :=
+  name == "Exception" || name == "BaseException" ||
+  name == "ValueError" || name == "TypeError" ||
+  name == "KeyError" || name == "IndexError" ||
+  name == "RuntimeError" || name == "ZeroDivisionError" ||
+  name == "AssertionError" || name == "AttributeError" ||
+  name == "OverflowError" || name == "StopIteration" ||
+  name == "NotImplementedError" || name == "NameError" ||
+  name == "OSError" || name == "IOError" ||
+  name == "FileNotFoundError" || name == "ImportError" ||
+  name == "ModuleNotFoundError" || name == "SystemExit" ||
+  name == "KeyboardInterrupt" || name == "GeneratorExit"
+
 end LeanPython.Runtime

LeanPython/Runtime/Types.lean

@@ -239,8 +239,8 @@ private def assertPyError (source errSubstr : String) : IO Unit := do
 -- Bare except catches everything
 #eval assertPy "try:\n    raise ValueError(\"x\")\nexcept:\n    print(\"caught\")\n" "caught\n"
 
--- Exception as binding gives exception value
-#eval assertPy "try:\n    raise ValueError(\"bad value\")\nexcept ValueError as e:\n    print(e)\n" "ValueError(bad value)\n"
+-- Exception as binding gives message string
+#eval assertPy "try:\n    raise ValueError(\"bad value\")\nexcept ValueError as e:\n    print(e)\n" "bad value\n"
 
 -- Finally always runs
 #eval assertPy "try:\n    raise ValueError(\"x\")\nexcept ValueError:\n    print(\"caught\")\nfinally:\n    print(\"done\")\n" "caught\ndone\n"

LeanPythonTest/Interpreter.lean

@@ -735,3 +735,52 @@ private def assertPyError (source errSubstr : String) : IO Unit := do
 
 -- __get_pydantic_core_schema__ classmethod is callable and returns schema
 #eval assertPy "from pydantic_core import core_schema\nclass BoundedInt:\n    @classmethod\n    def __get_pydantic_core_schema__(cls, source_type, handler):\n        return core_schema.int_schema(ge=0, lt=100)\nresult = BoundedInt.__get_pydantic_core_schema__(None, None)\nprint(result['type'])" "int\n"
+
+-- ============================================================
+-- Phase 9a: leanSpec primitive type support
+-- ============================================================
+
+-- Exception hierarchy
+#eval assertPy "class SSZError(Exception):\n    pass\nclass SSZTypeError(SSZError):\n    pass\ntry:\n    raise SSZTypeError('bad type')\nexcept SSZError as e:\n    print(type(e).__name__)\n    print(str(e))" "SSZTypeError\nbad type\n"
+
+-- ABC with classmethod + abstractmethod
+#eval assertPy "from abc import ABC, abstractmethod\nclass SSZType(ABC):\n    @classmethod\n    @abstractmethod\n    def is_fixed_size(cls):\n        pass\nclass Concrete(SSZType):\n    @classmethod\n    def is_fixed_size(cls):\n        return True\nprint(Concrete.is_fixed_size())" "True\n"
+
+-- @override decorator (identity, doesn't fail)
+#eval assertPy "from typing import override\ndef base():\n    return 1\n@override\ndef child():\n    return 2\nprint(child())" "2\n"
+
+-- Multiple inheritance from int: basic construction
+#eval assertPy "from abc import ABC, abstractmethod\nclass SSZType(ABC):\n    @classmethod\n    @abstractmethod\n    def is_fixed_size(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    def is_fixed_size(cls):\n        return True\nclass Uint64(BaseUint):\n    BITS = 64\nx = Uint64(42)\nprint(int(x))\nprint(type(x).__name__)" "42\nUint64\n"
+
+-- isinstance checks for int subclass
+#eval assertPy "from abc import ABC, abstractmethod\nclass SSZType(ABC):\n    @classmethod\n    @abstractmethod\n    def is_fixed_size(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    def is_fixed_size(cls):\n        return True\nclass Uint64(BaseUint):\n    BITS = 64\nx = Uint64(42)\nprint(isinstance(x, Uint64))\nprint(isinstance(x, BaseUint))\nprint(isinstance(x, int))\nprint(isinstance(x, SSZType))" "True\nTrue\nTrue\nTrue\n"
+
+-- Arithmetic on int subclasses via dunder methods
+#eval assertPy "class BaseUint(int):\n    BITS = 64\n    def __new__(cls, value):\n        return super().__new__(cls, int(value))\n    def __add__(self, other):\n        return type(self)(super().__add__(other))\nclass Uint64(BaseUint):\n    BITS = 64\nx = Uint64(10)\ny = Uint64(20)\nz = x + y\nprint(int(z))\nprint(type(z).__name__)" "30\nUint64\n"
+
+-- Comparison operators on int subclasses
+#eval assertPy "class BaseUint(int):\n    BITS = 64\n    def __new__(cls, value):\n        return super().__new__(cls, int(value))\nclass Uint64(BaseUint):\n    BITS = 64\na = Uint64(10)\nb = Uint64(20)\nprint(a < b)\nprint(a == Uint64(10))\nprint(a > b)" "True\nTrue\nFalse\n"
+
+-- Range validation in __new__
+#eval assertPyError "class SSZValueError(Exception):\n    pass\nclass BaseUint(int):\n    BITS = 8\n    def __new__(cls, value):\n        if not isinstance(value, int) or isinstance(value, bool):\n            raise TypeError('Expected int')\n        int_value = int(value)\n        max_value = 2 ** cls.BITS - 1\n        if not (0 <= int_value <= max_value):\n            raise SSZValueError('out of range')\n        return super().__new__(cls, int_value)\nclass Uint8(BaseUint):\n    BITS = 8\nUint8(256)" "out of range"
+
+-- Negative value rejected
+#eval assertPyError "class SSZValueError(Exception):\n    pass\nclass BaseUint(int):\n    BITS = 8\n    def __new__(cls, value):\n        if not isinstance(value, int) or isinstance(value, bool):\n            raise TypeError('Expected int')\n        int_value = int(value)\n        if not (0 <= int_value <= 2 ** cls.BITS - 1):\n            raise SSZValueError('out of range')\n        return super().__new__(cls, int_value)\nclass Uint8(BaseUint):\n    BITS = 8\nUint8(-1)" "out of range"
+
+-- Bool rejected (isinstance(True, int) is True, but we check isinstance(value, bool))
+#eval assertPyError "class BaseUint(int):\n    BITS = 8\n    def __new__(cls, value):\n        if not isinstance(value, int) or isinstance(value, bool):\n            raise TypeError('Expected int')\n        return super().__new__(cls, int(value))\nclass Uint8(BaseUint):\n    BITS = 8\nUint8(True)" "Expected int"
+
+-- Bitwise operations on int subclasses
+#eval assertPy "class BaseUint(int):\n    BITS = 8\n    def __new__(cls, value):\n        return super().__new__(cls, int(value))\n    def __and__(self, other):\n        return type(self)(super().__and__(other))\n    def __or__(self, other):\n        return type(self)(super().__or__(other))\n    def __xor__(self, other):\n        return type(self)(super().__xor__(other))\nclass Uint8(BaseUint):\n    BITS = 8\na = Uint8(0b1100)\nb = Uint8(0b1010)\nprint(int(a & b))\nprint(int(a | b))\nprint(int(a ^ b))" "8\n14\n6\n"
+
+-- to_bytes on int subclass instance
+#eval assertPy "class BaseUint(int):\n    BITS = 64\n    def __new__(cls, value):\n        return super().__new__(cls, int(value))\n    def serialize_to_bytes(self):\n        return int(self).to_bytes(self.BITS // 8, 'little')\nclass Uint64(BaseUint):\n    BITS = 64\nx = Uint64(256)\nb = x.serialize_to_bytes()\nprint(len(b))\nprint(b[0])\nprint(b[1])" "8\n0\n1\n"
+
+-- hash() works on int subclass instances (for Pydantic frozen models)
+#eval assertPy "class BaseUint(int):\n    BITS = 8\n    def __new__(cls, value):\n        return super().__new__(cls, int(value))\n    def __hash__(self):\n        return hash((type(self).__name__, int(self)))\nclass Uint8(BaseUint):\n    BITS = 8\nx = Uint8(42)\nh = hash(x)\nprint(isinstance(h, int))\nprint(h != 0)" "True\nTrue\n"
+
+-- ClassVar accessible on subclasses
+#eval assertPy "class BaseUint(int):\n    BITS = 0\n    def __new__(cls, value):\n        return super().__new__(cls, int(value))\nclass Uint8(BaseUint):\n    BITS = 8\nclass Uint64(BaseUint):\n    BITS = 64\nprint(Uint8.BITS)\nprint(Uint64.BITS)" "8\n64\n"
+
+-- Multiple Uint subclasses
+#eval assertPy "class BaseUint(int):\n    BITS = 0\n    def __new__(cls, value):\n        return super().__new__(cls, int(value))\nclass Uint8(BaseUint):\n    BITS = 8\nclass Uint16(BaseUint):\n    BITS = 16\nclass Uint32(BaseUint):\n    BITS = 32\nclass Uint64(BaseUint):\n    BITS = 64\nprint(int(Uint8(255)))\nprint(int(Uint16(1000)))\nprint(int(Uint32(100000)))\nprint(int(Uint64(2**40)))" "255\n1000\n100000\n1099511627776\n"