Complete Phase 7b: stdlib data handling (struct, io, bisect, base64, json, re)

Add data handling stdlib modules needed for SSZ serialization and fixtures:
- struct: pack/unpack/calcsize with format parsing and big/little-endian support
- io: BytesIO/StringIO as heap-backed instances with read/write/seek/context manager
- bisect: bisect_left/bisect_right/insort with binary search
- base64: b64encode/decode, urlsafe variants, b16encode/decode
- json: dumps serializer and loads recursive-descent parser with JsonVal AST
- re: stub module (not needed for core leanSpec spec)

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

Author: pirapira

CLAUDE.md

@@ -48,6 +48,11 @@ LeanPython/
   Stdlib.lean        — stdlib umbrella import
   Stdlib/
     Math.lean        — Pure math helpers (ceil, floor, sqrt, log, etc.)
+    Struct.lean      — struct.pack/unpack/calcsize (binary data packing)
+    IO.lean          — io.BytesIO/StringIO (in-memory stream objects)
+    Bisect.lean      — bisect_left/bisect_right/insort (binary search)
+    Base64.lean      — b64encode/decode, b16encode/decode, urlsafe variants
+    Json.lean        — json.dumps (serializer) and json.loads (parser)
 Main.lean            — CLI entry point (reads .py file, parses, interprets)
 LeanPythonTest.lean      — test driver root
 LeanPythonTest/

LeanPython/Interpreter/Eval.lean

@@ -13,6 +13,7 @@ open LeanPython.Runtime.Ops
 open LeanPython.Runtime.Builtins
 open LeanPython.Interpreter
 open LeanPython.Parser (parse)
+open LeanPython.Stdlib.IO
 open LeanPython.Lexer (SourceSpan SourcePos)
 
 -- ============================================================
@@ -724,6 +725,40 @@ partial def callValueDispatch (callee : Value) (args : List Value)
         match args with
         | [obj] => getAttributeValue obj attrName
         | _ => throwTypeError "attrgetter object takes exactly 1 argument"
+      else if name == "io.BytesIO" then do
+        -- Construct a BytesIO instance with _buffer and _pos attrs
+        let initBuf := match args with
+          | [.bytes b] => b
+          | [] => ByteArray.empty
+          | _ => ByteArray.empty
+        let mut attrs : Std.HashMap String Value := {}
+        attrs := attrs.insert "_buffer" (.bytes initBuf)
+        attrs := attrs.insert "_pos" (.int 0)
+        -- Create a class object for BytesIO (lightweight)
+        let cls ← allocClassObj {
+          name := "BytesIO", bases := #[], mro := #[], ns := {}, slots := none }
+        match cls with
+        | .classObj cref => heapSetClassData cref {
+            name := "BytesIO", bases := #[], mro := #[cls], ns := {}, slots := none }
+        | _ => pure ()
+        let instRef ← heapAlloc (.instanceObjData { cls := cls, attrs := attrs })
+        return .instance instRef
+      else if name == "io.StringIO" then do
+        let initBuf := match args with
+          | [.str s] => s
+          | [] => ""
+          | _ => ""
+        let mut attrs : Std.HashMap String Value := {}
+        attrs := attrs.insert "_buffer" (.str initBuf)
+        attrs := attrs.insert "_pos" (.int 0)
+        let cls ← allocClassObj {
+          name := "StringIO", bases := #[], mro := #[], ns := {}, slots := none }
+        match cls with
+        | .classObj cref => heapSetClassData cref {
+            name := "StringIO", bases := #[], mro := #[cls], ns := {}, slots := none }
+        | _ => pure ()
+        let instRef ← heapAlloc (.instanceObjData { cls := cls, attrs := attrs })
+        return .instance instRef
       else
         callBuiltin name args kwargs
   | .function ref => do
@@ -1052,6 +1087,17 @@ partial def getAttributeValue (obj : Value) (attr : String) : InterpM Value := d
     match id_.cls with
     | .classObj cref => do
       let cd ← heapGetClassData cref
+      -- Builtin instance types: return bound methods for known method names
+      if cd.name == "BytesIO" && ["write", "read", "getvalue", "seek", "tell",
+            "__enter__", "__exit__", "close"].contains attr then
+        match obj with
+        | .instance _ => return .boundMethod obj attr
+        | _ => pure ()
+      if cd.name == "StringIO" && ["write", "read", "getvalue", "seek", "tell",
+            "__enter__", "__exit__", "close"].contains attr then
+        match obj with
+        | .instance _ => return .boundMethod obj attr
+        | _ => pure ()
       -- First pass: check for data descriptors (property with getter)
       for mroEntry in cd.mro do
         match mroEntry with
@@ -1470,6 +1516,46 @@ partial def getBuiltinModule (name : String) : InterpM (Option Value) := do
               "Callable", "Hashable", "Sized", "Container"] do
       ns := ns.insert n .none
     some <$> mkMod ns
+  | "struct" =>
+    let mut ns : Std.HashMap String Value := {}
+    ns := ns.insert "pack"     (.builtin "struct.pack")
+    ns := ns.insert "unpack"   (.builtin "struct.unpack")
+    ns := ns.insert "calcsize" (.builtin "struct.calcsize")
+    some <$> mkMod ns
+  | "io" =>
+    let mut ns : Std.HashMap String Value := {}
+    ns := ns.insert "BytesIO"  (.builtin "io.BytesIO")
+    ns := ns.insert "StringIO" (.builtin "io.StringIO")
+    some <$> mkMod ns
+  | "bisect" =>
+    let mut ns : Std.HashMap String Value := {}
+    ns := ns.insert "bisect_left"  (.builtin "bisect.bisect_left")
+    ns := ns.insert "bisect_right" (.builtin "bisect.bisect_right")
+    ns := ns.insert "bisect"       (.builtin "bisect.bisect")
+    ns := ns.insert "insort"       (.builtin "bisect.insort")
+    ns := ns.insert "insort_right" (.builtin "bisect.insort_right")
+    ns := ns.insert "insort_left"  (.builtin "bisect.insort_left")
+    some <$> mkMod ns
+  | "base64" =>
+    let mut ns : Std.HashMap String Value := {}
+    ns := ns.insert "b64encode"         (.builtin "base64.b64encode")
+    ns := ns.insert "b64decode"         (.builtin "base64.b64decode")
+    ns := ns.insert "urlsafe_b64encode" (.builtin "base64.urlsafe_b64encode")
+    ns := ns.insert "urlsafe_b64decode" (.builtin "base64.urlsafe_b64decode")
+    ns := ns.insert "b16encode"         (.builtin "base64.b16encode")
+    ns := ns.insert "b16decode"         (.builtin "base64.b16decode")
+    some <$> mkMod ns
+  | "json" =>
+    let mut ns : Std.HashMap String Value := {}
+    ns := ns.insert "dumps" (.builtin "json.dumps")
+    ns := ns.insert "loads" (.builtin "json.loads")
+    some <$> mkMod ns
+  | "re" =>
+    let mut ns : Std.HashMap String Value := {}
+    for n in ["compile", "match", "search", "sub", "findall", "split",
+              "IGNORECASE", "MULTILINE", "DOTALL", "VERBOSE"] do
+      ns := ns.insert n (.builtin s!"re.{n}")
+    some <$> mkMod ns
   | _ => return none
 
 /-- Load a module by fully-qualified name and file path.
@@ -2190,8 +2276,12 @@ partial def callBoundMethod (receiver : Value) (method : String) (args : List Va
   | .instance iref => do
     -- Look up method in instance's class MRO and call with self
     let id_ ← heapGetInstanceData iref
+    -- Check for builtin instance types (BytesIO, StringIO)
     match id_.cls with
     | .classObj cref => do
+      let cd_ ← heapGetClassData cref
+      if cd_.name == "BytesIO" then return ← callBytesIOMethod iref method args
+      if cd_.name == "StringIO" then return ← callStringIOMethod iref method args
       let cd ← heapGetClassData cref
       let mut found : Option (Value × Value) := none  -- (function, defining class)
       for mroEntry in cd.mro do

LeanPython/Runtime/Builtins.lean

@@ -1,5 +1,10 @@
 import LeanPython.Runtime.Ops
 import LeanPython.Stdlib.Math
+import LeanPython.Stdlib.Struct
+import LeanPython.Stdlib.IO
+import LeanPython.Stdlib.Bisect
+import LeanPython.Stdlib.Base64
+import LeanPython.Stdlib.Json
 
 set_option autoImplicit false
 
@@ -9,6 +14,10 @@ open LeanPython.Runtime
 open LeanPython.Runtime.Ops
 open LeanPython.Interpreter
 open LeanPython.Stdlib.Math
+open LeanPython.Stdlib.Struct
+open LeanPython.Stdlib.Bisect
+open LeanPython.Stdlib.Base64
+open LeanPython.Stdlib.Json
 
 -- ============================================================
 -- Individual builtin implementations
@@ -790,6 +799,35 @@ partial def callBuiltin (name : String) (args : List Value)
     match args with
     | [_] => return .tuple #[]
     | _ => throwTypeError "dataclasses.fields() takes exactly 1 argument"
+  -- ============================================================
+  -- struct module functions
+  -- ============================================================
+  | "struct.pack"     => structPack args
+  | "struct.unpack"   => structUnpack args
+  | "struct.calcsize" => structCalcsize args
+  -- ============================================================
+  -- bisect module functions
+  -- ============================================================
+  | "bisect.bisect_left"  => bisectLeft args kwargs
+  | "bisect.bisect_right" => bisectRight args kwargs
+  | "bisect.bisect"       => bisectRight args kwargs  -- bisect is alias for bisect_right
+  | "bisect.insort"       => bisectInsort args kwargs
+  | "bisect.insort_right" => bisectInsort args kwargs
+  | "bisect.insort_left"  => bisectInsort args kwargs  -- simplified
+  -- ============================================================
+  -- base64 module functions
+  -- ============================================================
+  | "base64.b64encode"           => b64encode args
+  | "base64.b64decode"           => b64decode args
+  | "base64.urlsafe_b64encode"   => urlsafeB64encode args
+  | "base64.urlsafe_b64decode"   => urlsafeB64decode args
+  | "base64.b16encode"           => b16encode args
+  | "base64.b16decode"           => b16decode args
+  -- ============================================================
+  -- json module functions
+  -- ============================================================
+  | "json.dumps" => jsonDumps args kwargs
+  | "json.loads" => jsonLoads args
   | _ => throwNotImplemented s!"builtin '{name}' is not implemented"
 
 end LeanPython.Runtime.Builtins

LeanPython/Stdlib.lean

@@ -1 +1,6 @@
 import LeanPython.Stdlib.Math
+import LeanPython.Stdlib.Struct
+import LeanPython.Stdlib.IO
+import LeanPython.Stdlib.Bisect
+import LeanPython.Stdlib.Base64
+import LeanPython.Stdlib.Json

LeanPython/Stdlib/Base64.lean

@@ -0,0 +1,171 @@
+import LeanPython.Interpreter.Types
+
+set_option autoImplicit false
+
+namespace LeanPython.Stdlib.Base64
+
+open LeanPython.Runtime
+open LeanPython.Interpreter
+
+-- ============================================================
+-- Base64 encoding/decoding
+-- ============================================================
+
+private def stdAlphabet : String := "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/"
+private def urlAlphabet : String := "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789-_"
+
+private def charToIndex (c : Char) (urlSafe : Bool) : Option Nat :=
+  let alpha := if urlSafe then urlAlphabet else stdAlphabet
+  alpha.toList.findIdx? (· == c) |>.map id
+
+private partial def encodeBase64 (data : ByteArray) (urlSafe : Bool) : ByteArray := Id.run do
+  let alpha := if urlSafe then urlAlphabet else stdAlphabet
+  let alphaArr := alpha.toList.toArray
+  let mut result := ByteArray.empty
+  let mut i : Nat := 0
+  while i + 2 < data.size do
+    let b0 := (data.get! i).toNat
+    let b1 := (data.get! (i + 1)).toNat
+    let b2 := (data.get! (i + 2)).toNat
+    let n := b0 * 65536 + b1 * 256 + b2
+    result := result.push (alphaArr[n >>> 18 &&& 63]!).toUInt8
+    result := result.push (alphaArr[n >>> 12 &&& 63]!).toUInt8
+    result := result.push (alphaArr[n >>> 6 &&& 63]!).toUInt8
+    result := result.push (alphaArr[n &&& 63]!).toUInt8
+    i := i + 3
+  let remaining := data.size - i
+  if remaining == 2 then
+    let b0 := (data.get! i).toNat
+    let b1 := (data.get! (i + 1)).toNat
+    let n := b0 * 256 + b1
+    result := result.push (alphaArr[n >>> 10 &&& 63]!).toUInt8
+    result := result.push (alphaArr[n >>> 4 &&& 63]!).toUInt8
+    result := result.push (alphaArr[(n <<< 2) &&& 63]!).toUInt8
+    result := result.push '='.toUInt8
+  else if remaining == 1 then
+    let b0 := (data.get! i).toNat
+    result := result.push (alphaArr[b0 >>> 2]!).toUInt8
+    result := result.push (alphaArr[(b0 <<< 4) &&& 63]!).toUInt8
+    result := result.push '='.toUInt8
+    result := result.push '='.toUInt8
+  return result
+
+private partial def decodeBase64 (data : ByteArray) (urlSafe : Bool) : Except String ByteArray := do
+  -- Strip padding and whitespace
+  let chars := data.toList.filter (fun b => b.toNat != '='.toNat && b.toNat != '\n'.toNat && b.toNat != '\r'.toNat)
+  let mut result := ByteArray.empty
+  let mut buf : Nat := 0
+  let mut bits : Nat := 0
+  for b in chars do
+    let c := Char.ofNat b.toNat
+    match charToIndex c urlSafe with
+    | some idx =>
+      buf := (buf <<< 6) ||| idx
+      bits := bits + 6
+      if bits >= 8 then
+        bits := bits - 8
+        result := result.push ((buf >>> bits) &&& 255).toUInt8
+        buf := buf &&& ((1 <<< bits) - 1)
+    | none => .error s!"Invalid character in base64: '{c}'"
+  return result
+
+-- ============================================================
+-- Base16 (hex) encoding/decoding
+-- ============================================================
+
+private def hexCharsUpper : String := "0123456789ABCDEF"
+
+private partial def encodeBase16 (data : ByteArray) : ByteArray := Id.run do
+  let hexArr := hexCharsUpper.toList.toArray
+  let mut result := ByteArray.empty
+  for i in [:data.size] do
+    let b := (data.get! i).toNat
+    result := result.push (hexArr[b >>> 4]!).toUInt8
+    result := result.push (hexArr[b &&& 15]!).toUInt8
+  return result
+
+private def hexCharToNibble (c : Char) : Option Nat :=
+  if '0' ≤ c && c ≤ '9' then some (c.toNat - '0'.toNat)
+  else if 'A' ≤ c && c ≤ 'F' then some (c.toNat - 'A'.toNat + 10)
+  else if 'a' ≤ c && c ≤ 'f' then some (c.toNat - 'a'.toNat + 10)
+  else none
+
+private partial def decodeBase16 (data : ByteArray) : Except String ByteArray := do
+  if data.size % 2 != 0 then .error "Odd-length string"
+  let mut result := ByteArray.empty
+  let mut i : Nat := 0
+  while i + 1 < data.size do
+    let c1 := Char.ofNat (data.get! i).toNat
+    let c2 := Char.ofNat (data.get! (i + 1)).toNat
+    match hexCharToNibble c1, hexCharToNibble c2 with
+    | some h, some l => result := result.push (h * 16 + l).toUInt8
+    | _, _ => .error s!"Non-hexadecimal digit found"
+    i := i + 2
+  return result
+
+-- ============================================================
+-- Python-facing functions
+-- ============================================================
+
+/-- Coerce args to ByteArray for base64 functions. -/
+private def toByteArray (v : Value) : InterpM ByteArray := do
+  match v with
+  | .bytes b => return b
+  | .str s => return s.toUTF8
+  | _ => throwTypeError "a bytes-like object is required"
+
+/-- Python base64.b64encode(s) -/
+partial def b64encode (args : List Value) : InterpM Value := do
+  match args with
+  | [v] => do
+    let data ← toByteArray v
+    return .bytes (encodeBase64 data false)
+  | _ => throwTypeError "b64encode() takes exactly 1 argument"
+
+/-- Python base64.b64decode(s) -/
+partial def b64decode (args : List Value) : InterpM Value := do
+  match args with
+  | [v] => do
+    let data ← toByteArray v
+    match decodeBase64 data false with
+    | .ok result => return .bytes result
+    | .error e => throwValueError e
+  | _ => throwTypeError "b64decode() takes exactly 1 argument"
+
+/-- Python base64.urlsafe_b64encode(s) -/
+partial def urlsafeB64encode (args : List Value) : InterpM Value := do
+  match args with
+  | [v] => do
+    let data ← toByteArray v
+    return .bytes (encodeBase64 data true)
+  | _ => throwTypeError "urlsafe_b64encode() takes exactly 1 argument"
+
+/-- Python base64.urlsafe_b64decode(s) -/
+partial def urlsafeB64decode (args : List Value) : InterpM Value := do
+  match args with
+  | [v] => do
+    let data ← toByteArray v
+    match decodeBase64 data true with
+    | .ok result => return .bytes result
+    | .error e => throwValueError e
+  | _ => throwTypeError "urlsafe_b64decode() takes exactly 1 argument"
+
+/-- Python base64.b16encode(s) -/
+partial def b16encode (args : List Value) : InterpM Value := do
+  match args with
+  | [v] => do
+    let data ← toByteArray v
+    return .bytes (encodeBase16 data)
+  | _ => throwTypeError "b16encode() takes exactly 1 argument"
+
+/-- Python base64.b16decode(s) -/
+partial def b16decode (args : List Value) : InterpM Value := do
+  match args with
+  | [v] => do
+    let data ← toByteArray v
+    match decodeBase16 data with
+    | .ok result => return .bytes result
+    | .error e => throwValueError e
+  | _ => throwTypeError "b16decode() takes exactly 1 argument"
+
+end LeanPython.Stdlib.Base64