Expand leanSpec E2E tests to subspecs/ layer (Tiers 8-12)

Add 5 new E2E test tiers running real leanSpec subspecs Python files:
koalabear/field.py (Fp arithmetic), ssz/ pipeline (constants, utils,
pack, merkleization, hash_tree_root via singledispatch), chain/config
constants, and containers (Slot, Checkpoint, Config). Fix bytes
__getitem__ to support slice tuples on subclass instances, and add
memoryview/frozenset/complex as builtin names.

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

Author: pirapira

LeanPython/Interpreter/Eval.lean

@@ -1751,6 +1751,14 @@ partial def callValueDispatch (callee : Value) (args : List Value)
             let i : Int := if idx < 0 then (b.size : Int) + idx else idx
             if i < 0 || i >= b.size then throwTypeError "index out of range"
             return .int (b[i.toNat]!.toNat : Int)
+          | [a, .tuple #[start, stop, step]] => do
+            let b ← extractBytes a
+            let (st, en, stp) ← computeSliceIndices b.size (some start) (some stop) (some step)
+            let indices := sliceIndices st en stp
+            let mut result := ByteArray.empty
+            for i in indices do
+              if i < b.size then result := result.push b[i]!
+            return .bytes result
           | _ => throwTypeError "bytes.__getitem__ takes 2 arguments"
         | "__contains__" => match args with
           | [a, .int byte_] => do
@@ -2757,7 +2765,8 @@ partial def evalSubscriptValue (obj idx : Value) : InterpM Value := do
   | .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
+    | "list" | "dict" | "set" | "tuple" | "frozenset" | "type"
+    | "memoryview" | "complex" => return .none
     | _ => throwTypeError s!"'{typeName obj}' object is not subscriptable"
   | _ => throwTypeError s!"'{typeName obj}' object is not subscriptable"
 

LeanPython/Runtime/Types.lean

@@ -350,6 +350,7 @@ def builtinNames : List String :=
    "hex", "oct", "bin", "round", "pow", "divmod", "map", "filter",
    "iter", "next", "hasattr", "getattr", "setattr", "callable",
    "issubclass", "super", "object", "bytes", "bytearray",
+   "memoryview", "frozenset", "complex",
    "staticmethod", "classmethod", "property",
    -- Dataclass
    "dataclass",

PLAN.md

@@ -787,6 +787,7 @@ For non-deterministic tests, structural equivalence is checked.
 | 9e | leanSpec: fork choice | Done (Store with block/state management, BlockLookup ancestors generator, LMD GHOST fork choice algorithm, compute_block_weights, update_head) |
 | 9f | leanSpec: cryptographic subspecs | Done (KoalaBear Fp field arithmetic with modular inverse/division, Poseidon2 width-16/24 permutation with reference test vectors, compression and sponge modes, int_to_base_p, SHAKE128-based PRF, tweak encoding, hash chain traversal with composition verification, hypercube layer size via math.comb + map_to_vertex round-trip, Merkle tree construction and path verification; interpreter: math.comb, os.urandom, list slice assignment, __bytes__ dunder) |
 | 9g | Match/case (structural pattern matching) | Done (MatchPattern AST with matchValue/matchClass/matchWildcard/matchCapture/matchOr, soft-keyword parser with attempt-based backtracking, interpreter pattern matching with isinstance + attribute extraction, class/value/wildcard/capture/guard patterns, real leanSpec XMSS encode_tweak test with match/case) |
+| 9h | leanSpec: subspecs E2E (ssz+koalabear+containers) | Done (real leanSpec subspecs files: koalabear/field.py Fp arithmetic, ssz/constants+utils+pack+merkleization+hash.py full hash_tree_root via singledispatch with 13 type handlers, chain/config.py constants, containers/slot.py+checkpoint.py+config.py; interpreter: memoryview/frozenset/complex builtins, bytes.__getitem__ slice support for subclass instances) |
 | 10 | Async runtime (optional) | Not started |
 
 ---