Advance leanSpec E2E integration to Tier 5 & 6 (byte_arrays, bitfields, collections, union)

Add support for remaining SSZ type files from leanSpec, bringing E2E tests
from 7 to 11 — all passing. Key interpreter fixes: @overload/@runtime_checkable
as identity decorators, cast() returning second arg, __init_subclass__ hook,
cross-type valueEq for int subclass instances, PEP 604 type unions, inline
function bodies, trailing comma in parenthesized imports, and int.to_bytes/
from_bytes keyword argument support.

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

Author: pirapira

LeanPython/Interpreter/Eval.lean

@@ -2754,6 +2754,11 @@ partial def evalSubscriptValue (obj idx : Value) : InterpM Value := do
     match cd.ns["__class_getitem__"]? with
     | some fn => callValueDispatch fn [idx] []
     | none => return .none  -- default: subscripting a class returns .none (for typing)
+  | .builtin name =>
+    -- Allow subscripting on builtin type names for type annotations (list[int], dict[str, int], etc.)
+    match name with
+    | "list" | "dict" | "set" | "tuple" | "frozenset" | "type" => return .none
+    | _ => throwTypeError s!"'{typeName obj}' object is not subscriptable"
   | _ => throwTypeError s!"'{typeName obj}' object is not subscriptable"
 
 -- Assignment target resolution
@@ -2979,30 +2984,37 @@ partial def getBuiltinModule (name : String) : InterpM (Option Value) := do
     -- Stub common typing names as none so imports don't fail
     for n in ["Any", "Optional", "List", "Dict", "Set", "Tuple", "FrozenSet",
               "Self", "Union", "Callable", "Protocol",
-              "runtime_checkable", "NamedTuple",
+              "NamedTuple",
               "NoReturn", "SupportsInt", "SupportsIndex",
               "TypeAlias", "Literal", "IO", "Sequence", "Mapping",
               "Iterator", "Iterable", "Generator", "Coroutine",
               "Awaitable", "AsyncIterator", "AsyncGenerator",
               "Type", "Generic", "Annotated",
-              "overload", "cast", "no_type_check"] do
+              "no_type_check"] do
       ns := ns.insert n .none
     -- ClassVar and Final are distinct markers (not .none) so Pydantic can skip them
     ns := ns.insert "ClassVar" (.builtin "typing.ClassVar")
     ns := ns.insert "Final" (.builtin "typing.Final")
     -- TypeVar is callable (returns .none as a stub type variable)
     ns := ns.insert "TypeVar" (.builtin "typing.TypeVar")
-    -- override is a callable identity decorator (not .none)
+    -- Identity decorators (return their argument unchanged)
     ns := ns.insert "override" (.builtin "typing.override")
+    ns := ns.insert "overload" (.builtin "typing.overload")
+    ns := ns.insert "runtime_checkable" (.builtin "typing.runtime_checkable")
+    -- cast(type, value) returns the value unchanged
+    ns := ns.insert "cast" (.builtin "typing.cast")
     some <$> mkMod ns
   | "typing_extensions" =>
     -- Alias for typing for compatibility
     let mut ns : Std.HashMap String Value := {}
     ns := ns.insert "TYPE_CHECKING" (.bool false)
-    for n in ["Self", "Protocol", "runtime_checkable",
+    for n in ["Self", "Protocol",
               "Annotated", "TypeAlias", "get_type_hints"] do
       ns := ns.insert n .none
     ns := ns.insert "override" (.builtin "typing.override")
+    ns := ns.insert "overload" (.builtin "typing.overload")
+    ns := ns.insert "runtime_checkable" (.builtin "typing.runtime_checkable")
+    ns := ns.insert "cast" (.builtin "typing.cast")
     some <$> mkMod ns
   | "abc" => do
     -- Create real ABC base class
@@ -3740,6 +3752,30 @@ partial def execStmt (s : Stmt) : InterpM Unit := do
       let cd' ← heapGetClassData cref
       heapSetClassData cref { cd' with mro := mro }
     | _ => pure ()
+    -- Call __init_subclass__ on each direct base class (Python semantics)
+    for base in bases do
+      match base with
+      | .classObj bref => do
+        let bcd ← heapGetClassData bref
+        match bcd.ns["__init_subclass__"]? with
+        | some fn => do
+          -- __init_subclass__ is a classmethod; call with the new class as cls
+          let actualFn := match fn with
+            | .classMethod inner => inner
+            | other => other
+          -- Inject __class__ into the function's scope for super() support
+          match actualFn with
+          | .function fref => do
+            let fd ← heapGetFunc fref
+            let scope ← bindFuncParams fd.params [classVal] [] fd.defaults fd.kwDefaults
+            let scopeWithClass := scope.insert "__class__" base
+            let _ ← callRegularFunc fd scopeWithClass
+            pure ()
+          | _ =>
+            let _ ← callValueDispatch actualFn [classVal] []
+            pure ()
+        | none => pure ()
+      | _ => pure ()
     -- Post-process Pydantic BaseModel subclasses
     let isPydanticModel ← isBaseModelSubclass bases.toArray
     if isPydanticModel then
@@ -4165,14 +4201,28 @@ partial def callBoundMethod (receiver : Value) (method : String) (args : List Va
     let args' ← if kwargs.isEmpty then pure args else
       match method with
       | "to_bytes" =>
-        let length := kwargs.find? (·.1 == "length") |>.map (·.2) |>.getD (.int 1)
-        let byteorder := kwargs.find? (·.1 == "byteorder") |>.map (·.2) |>.getD (.str "big")
-        pure (args ++ [length, byteorder])
+        -- Support: .to_bytes(length, byteorder), .to_bytes(length, byteorder=...), .to_bytes(byteorder=..., length=...)
+        let posLength := args.head?
+        let length := posLength.orElse fun _ => (kwargs.find? (·.1 == "length") |>.map (·.2))
+        let posByteorder := if args.length > 1 then args.tail.head? else none
+        let byteorder := posByteorder.orElse fun _ => (kwargs.find? (·.1 == "byteorder") |>.map (·.2))
+        pure [length.getD (.int 1), byteorder.getD (.str "big")]
       | _ => pure args
     callIntMethod n method args'
   | .bytes b => callBytesMethod b method args
   | .tuple arr => callTupleMethod arr method args
-  | .builtin name => callBuiltinTypeMethod name method args
+  | .builtin name => do
+    -- Convert kwargs to positional for builtin type methods
+    let args' ← if kwargs.isEmpty then pure args else
+      match name, method with
+      | "int", "from_bytes" =>
+        let posBytes := args.head?
+        let bytes_ := posBytes.orElse fun _ => (kwargs.find? (·.1 == "bytes") |>.map (·.2))
+        let posByteorder := if args.length > 1 then args.tail.head? else none
+        let byteorder := posByteorder.orElse fun _ => (kwargs.find? (·.1 == "byteorder") |>.map (·.2))
+        pure [bytes_.getD (.bytes ByteArray.empty), byteorder.getD (.str "big")]
+      | _, _ => pure args
+    callBuiltinTypeMethod name method args'
   | .generator ref => callGeneratorMethod ref method args
   | .property getter setter deleter =>
     match method with
@@ -4328,7 +4378,10 @@ partial def callBoundMethod (receiver : Value) (method : String) (args : List Va
           -- Builtins in synthetic type classes: prepend inst (self/cls)
           callValueDispatch fn (inst :: args) kwargs
         | _ => callValueDispatch fn (inst :: args) kwargs
-      | none => throwAttributeError s!"'super' object has no attribute '{method}'"
+      | none =>
+          -- object.__init_subclass__ is a no-op in Python
+          if method == "__init_subclass__" then return .none
+          else throwAttributeError s!"'super' object has no attribute '{method}'"
     | _ => throwAttributeError s!"'super' object has no attribute '{method}'"
   | _ => throwAttributeError s!"'{typeName receiver}' object has no attribute '{method}'"
 

LeanPython/Parser/Stmt.lean

@@ -120,11 +120,18 @@ partial def parseFromImportAlias : ParserM Alias := do
 
 /-- Parse an indented block: NEWLINE INDENT stmt+ DEDENT. -/
 partial def parseBlock : ParserM (List Stmt) := do
-  discard expectNewline
-  discard expectIndent
-  let stmts ← parseStatements
-  discard expectDedent
-  return stmts
+  -- Check for inline body (e.g., `def foo(): pass` or `def foo(): ...`)
+  match ← peekKind with
+  | some .newline =>
+    discard expectNewline
+    discard expectIndent
+    let stmts ← parseStatements
+    discard expectDedent
+    return stmts
+  | _ =>
+    -- Inline body: parse simple statements on the same line
+    let stmts ← parseSimpleStmts
+    return stmts
 
 /-- Parse one or more statements (until DEDENT or ENDMARKER). -/
 partial def parseStatements : ParserM (List Stmt) := do
@@ -269,9 +276,21 @@ partial def parseFromImport : ParserM Stmt := do
     let lvl := if level > 0 then some level else none
     return .importFrom modName aliases lvl (← spanFrom start)
   let hasParen ← if ← isDelimiter .lpar then do discard advance; pure true else pure false
-  let aliases ← sepBy1 parseFromImportAlias (discard (expectDelimiter .comma))
+  -- Parse comma-separated import aliases; trailing comma is allowed inside parens
+  let first ← parseFromImportAlias
+  let mut aliases := [first]
+  while true do
+    match ← attempt (discard (expectDelimiter .comma)) with
+    | none => break
+    | some _ =>
+      -- After comma, try to parse another alias; if it fails (trailing comma), stop
+      if hasParen then
+        match ← attempt parseFromImportAlias with
+        | some a => aliases := aliases ++ [a]
+        | none => break
+      else
+        aliases := aliases ++ [← parseFromImportAlias]
   if hasParen then
-    if ← isDelimiter .comma then discard advance
     discard (expectDelimiter .rpar)
   let lvl := if level > 0 then some level else none
   return .importFrom modName aliases lvl (← spanFrom start)

LeanPython/Runtime/Builtins.lean

@@ -448,6 +448,7 @@ partial def builtinIsinstance (args : List Value) : InterpM Value := do
       | _ => pure ()
     return .bool false
   | [_, .classObj _] => return .bool false  -- non-instance is not an instance of a custom class
+  | [_, .none] => return .bool false  -- isinstance(x, None-stub) gracefully returns False
   | _ => throwTypeError "isinstance() takes 2 arguments"
 
 /-- Hash a single value for tuple/object hashing. -/
@@ -985,6 +986,18 @@ partial def callBuiltin (name : String) (args : List Value)
     match args with
     | [f] => return f
     | _ => throwTypeError "override() takes exactly 1 argument"
+  | "typing.overload" => do
+    match args with
+    | [f] => return f
+    | _ => throwTypeError "overload() takes exactly 1 argument"
+  | "typing.runtime_checkable" => do
+    match args with
+    | [f] => return f
+    | _ => throwTypeError "runtime_checkable() takes exactly 1 argument"
+  | "typing.cast" => do
+    match args with
+    | [_, v] => return v
+    | _ => throwTypeError "cast() takes exactly 2 arguments"
   | "typing.TypeVar" => do
     -- TypeVar('T', bound=SomeType) — stub that returns .none
     return .none

LeanPython/Runtime/Ops.lean

@@ -158,6 +158,17 @@ partial def valueEq (a b : Value) : InterpM Bool :=
     match ad.wrappedValue, bd.wrappedValue with
     | some va, some vb => valueEq va vb
     | _, _ => return false
+  -- Cross-type: instance with wrappedValue vs plain value
+  | .instance iref, other => do
+    let id_ ← heapGetInstanceData iref
+    match id_.wrappedValue with
+    | some wrapped => valueEq wrapped other
+    | none => return false
+  | other, .instance iref => do
+    let id_ ← heapGetInstanceData iref
+    match id_.wrappedValue with
+    | some wrapped => valueEq other wrapped
+    | none => return false
   | _, _ => return false
 
 -- ============================================================
@@ -530,6 +541,13 @@ partial def evalBinOp (op : BinOp) (left right : Value) : InterpM Value := do
               result := result.set! i (k, v); found := true; break
           if !found then result := result.push (k, v)
         allocDict result
+      -- Type union syntax: X | Y in annotations (PEP 604), e.g. int | str
+      | .none, _ => return .none
+      | _, .none => return .none
+      | .builtin _, .builtin _ => return .none
+      | .classObj _, .classObj _ => return .none
+      | .builtin _, .classObj _ => return .none
+      | .classObj _, .builtin _ => return .none
       | _, _ => throwTypeError s!"unsupported operand type(s) for |: '{typeName left}' and '{typeName right}'"
   | .bitAnd =>
     match toInt left, toInt right with