Complete Phase 9e: Fork choice — Store, LMD GHOST, ancestors

Add interpreter features needed for fork choice:
- max()/min() with key= parameter via builtinMinWithKey/builtinMaxWithKey
- set.update() method for in-place set merging
- time.perf_counter() function
- zip() with strict=True kwarg for length validation
- Tuple lexicographic comparison (<, <=, >, >=)

Tests cover: ancestors generator, walrus-in-while pattern, LMD GHOST
algorithm with forking block tree, and full Store end-to-end with
from_anchor, on_block, update_head, and attestation processing.

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

Author: pirapira

LeanPython/Interpreter/Eval.lean

@@ -20,7 +20,7 @@ open LeanPython.Stdlib.Hmac
 open LeanPython.Stdlib.Secrets
 open LeanPython.Stdlib.Sys
 open LeanPython.Stdlib.Os
-open LeanPython.Stdlib.Time (timeTime timeMonotonic timeSleep)
+open LeanPython.Stdlib.Time (timeTime timeMonotonic timePerfCounter timeSleep)
 open LeanPython.Stdlib.Datetime
 open LeanPython.Stdlib.Pathlib
 open LeanPython.Stdlib.Logging
@@ -138,7 +138,7 @@ private def knownDictMethods : List String :=
   ["get", "keys", "values", "items", "pop", "update", "clear", "copy", "setdefault"]
 
 private def knownSetMethods : List String :=
-  ["add", "remove", "discard", "clear", "copy", "union", "intersection",
+  ["add", "remove", "discard", "clear", "copy", "update", "union", "intersection",
    "difference", "symmetric_difference", "issubset", "issuperset", "isdisjoint"]
 
 private def knownIntMethods : List String :=
@@ -759,6 +759,16 @@ partial def callValueDispatch (callee : Value) (args : List Value)
     match name with
     | "map" => builtinMap args
     | "filter" => builtinFilter args
+    | "min" => do
+      let keyKw := kwargs.find? (fun (k, _) => k == "key")
+      match keyKw with
+      | some (_, keyFn) => builtinMinWithKey args keyFn
+      | none => callBuiltin name args kwargs
+    | "max" => do
+      let keyKw := kwargs.find? (fun (k, _) => k == "key")
+      match keyKw with
+      | some (_, keyFn) => builtinMaxWithKey args keyFn
+      | none => callBuiltin name args kwargs
     | "functools.reduce" => builtinFunctoolsReduce args
     | "itertools.accumulate" => builtinItertoolsAccumulate args kwargs
     | "collections.defaultdict" => do
@@ -3135,9 +3145,10 @@ partial def getBuiltinModule (name : String) : InterpM (Option Value) := do
     some <$> mkMod ns
   | "time" =>
     let mut ns : Std.HashMap String Value := {}
-    ns := ns.insert "time"      (.builtin "time.time")
-    ns := ns.insert "monotonic" (.builtin "time.monotonic")
-    ns := ns.insert "sleep"     (.builtin "time.sleep")
+    ns := ns.insert "time"         (.builtin "time.time")
+    ns := ns.insert "monotonic"    (.builtin "time.monotonic")
+    ns := ns.insert "perf_counter" (.builtin "time.perf_counter")
+    ns := ns.insert "sleep"        (.builtin "time.sleep")
     some <$> mkMod ns
   | "datetime" =>
     let mut ns : Std.HashMap String Value := {}
@@ -4182,6 +4193,42 @@ partial def builtinFilter (args : List Value) : InterpM Value := do
     allocList result
   | _ => throwTypeError "filter() requires exactly two arguments"
 
+-- ============================================================
+-- min/max with key= (need callValueDispatch, so must be in mutual block)
+-- ============================================================
+
+partial def builtinMinWithKey (args : List Value) (keyFn : Value) : InterpM Value := do
+  let items : List Value ← match args with
+    | [v] => do let arr ← iterValuesExt v; pure arr.toList
+    | xs => pure xs
+  match items with
+  | [] => throwValueError "min() arg is an empty sequence"
+  | first :: rest => do
+    let mut best := first
+    let mut bestKey ← callValueDispatch keyFn [first] []
+    for v in rest do
+      let vKey ← callValueDispatch keyFn [v] []
+      if ← evalCmpOp .lt vKey bestKey then
+        best := v
+        bestKey := vKey
+    return best
+
+partial def builtinMaxWithKey (args : List Value) (keyFn : Value) : InterpM Value := do
+  let items : List Value ← match args with
+    | [v] => do let arr ← iterValuesExt v; pure arr.toList
+    | xs => pure xs
+  match items with
+  | [] => throwValueError "max() arg is an empty sequence"
+  | first :: rest => do
+    let mut best := first
+    let mut bestKey ← callValueDispatch keyFn [first] []
+    for v in rest do
+      let vKey ← callValueDispatch keyFn [v] []
+      if ← evalCmpOp .gt vKey bestKey then
+        best := v
+        bestKey := vKey
+    return best
+
 -- ============================================================
 -- Enum support: check if any base class is an Enum
 -- ============================================================
@@ -4891,6 +4938,18 @@ partial def callSetMethod (ref : HeapRef) (method : String) (args : List Value)
         if !found then result := result.push elem
       allocSet result
     | _ => throwTypeError "union() takes exactly one argument"
+  | "update" =>
+    match args with
+    | [other] => do
+      let mut arr ← heapGetSet ref
+      let b ← iterValuesExt other
+      for elem in b do
+        let mut found := false
+        for existing in arr do
+          if ← valueEq existing elem then found := true; break
+        if !found then arr := arr.push elem
+      heapSetSet ref arr; return .none
+    | _ => throwTypeError "update() takes exactly one argument"
   | "intersection" =>
     match args with
     | [other] => do

LeanPython/Runtime/Builtins.lean

@@ -300,12 +300,20 @@ partial def builtinEnumerate (args : List Value) : InterpM Value := do
     idx := idx + 1
   allocList result
 
-/-- `zip(*iterables)` - returns list of tuples. -/
-partial def builtinZip (args : List Value) : InterpM Value := do
+/-- `zip(*iterables, strict=False)` - returns list of tuples. -/
+partial def builtinZip (args : List Value) (kwargs : List (String × Value)) : InterpM Value := do
   let iterables ← args.mapM iterValues
   if iterables.isEmpty then
     allocList #[]
   else
+    let strict := match kwargs.find? (fun (k, _) => k == "strict") with
+      | some (_, .bool true) => true
+      | _ => false
+    if strict then
+      let firstLen := iterables.head!.size
+      for iter in iterables do
+        if iter.size != firstLen then
+          throwValueError "zip() has arguments with different lengths"
     let minLen := iterables.foldl (fun acc arr => min acc arr.size) iterables.head!.size
     let mut result : Array Value := #[]
     for i in [:minLen] do
@@ -622,7 +630,7 @@ partial def callBuiltin (name : String) (args : List Value)
   | "sorted"     => builtinSorted args
   | "reversed"   => builtinReversed args
   | "enumerate"  => builtinEnumerate args
-  | "zip"        => builtinZip args
+  | "zip"        => builtinZip args kwargs
   | "list"       => builtinList args
   | "tuple"      => builtinTuple args
   | "isinstance" => builtinIsinstance args
@@ -1076,6 +1084,7 @@ partial def callBuiltin (name : String) (args : List Value)
   -- ============================================================
   | "time.time" => timeTime args
   | "time.monotonic" => timeMonotonic args
+  | "time.perf_counter" => timePerfCounter args
   | "time.sleep" => timeSleep args
   -- ============================================================
   -- logging module functions

LeanPython/Runtime/Ops.lean

@@ -639,6 +639,7 @@ partial def evalCmpOp (op : CmpOp) (left right : Value) : InterpM Bool := do
       match left', right' with
       | .str a, .str b => return (a < b)
       | .bytes a, .bytes b => return (a.toList < b.toList)
+      | .tuple a, .tuple b => tupleLt a b
       | _, _ => throwTypeError s!"'<' not supported between instances of '{typeName left}' and '{typeName right}'"
   | .ltE => do
     match ← numericCompare left' right' with
@@ -648,6 +649,11 @@ partial def evalCmpOp (op : CmpOp) (left right : Value) : InterpM Bool := do
       match left', right' with
       | .str a, .str b => return (decide (a ≤ b))
       | .bytes a, .bytes b => return (a.toList < b.toList || a == b)
+      | .tuple a, .tuple b => do
+        let lt ← tupleLt a b
+        if lt then return true
+        let gt ← tupleLt b a
+        return !gt
       | _, _ => throwTypeError s!"'<=' not supported between instances of '{typeName left}' and '{typeName right}'"
   | .gt => do
     match ← numericCompare left' right' with
@@ -657,6 +663,7 @@ partial def evalCmpOp (op : CmpOp) (left right : Value) : InterpM Bool := do
       match left', right' with
       | .str a, .str b => return (decide (a > b))
       | .bytes a, .bytes b => return (b.toList < a.toList)
+      | .tuple a, .tuple b => tupleLt b a
       | _, _ => throwTypeError s!"'>' not supported between instances of '{typeName left}' and '{typeName right}'"
   | .gtE => do
     match ← numericCompare left' right' with
@@ -666,11 +673,25 @@ partial def evalCmpOp (op : CmpOp) (left right : Value) : InterpM Bool := do
       match left', right' with
       | .str a, .str b => return (decide (a ≥ b))
       | .bytes a, .bytes b => return (b.toList < a.toList || a == b)
+      | .tuple a, .tuple b => do
+        let lt ← tupleLt b a
+        if lt then return true
+        let gt ← tupleLt a b
+        return !gt
       | _, _ => throwTypeError s!"'>=' not supported between instances of '{typeName left}' and '{typeName right}'"
   | .is_ => return (isIdentical left right)
   | .isNot => return (!isIdentical left right)
   | .in_ => valueContains right left
   | .notIn => do return !(← valueContains right left)
+where
+  /-- Lexicographic less-than for tuples. -/
+  tupleLt (a b : Array Value) : InterpM Bool := do
+    let minLen := min a.size b.size
+    for i in [:minLen] do
+      let eq ← valueEq a[i]! b[i]!
+      if !eq then
+        return ← evalCmpOp .lt a[i]! b[i]!
+    return (a.size < b.size)
 
 -- ============================================================
 -- Bool operators (short-circuit)

LeanPython/Stdlib/Time.lean

@@ -21,6 +21,11 @@ partial def timeMonotonic (_args : List Value) : InterpM Value := do
   let ms ← (IO.monoMsNow : BaseIO Nat)
   return .float (Nat.toFloat ms / 1000.0)
 
+/-- Python time.perf_counter(): return performance counter as float seconds. -/
+partial def timePerfCounter (_args : List Value) : InterpM Value := do
+  let ms ← (IO.monoMsNow : BaseIO Nat)
+  return .float (Nat.toFloat ms / 1000.0)
+
 /-- Python time.sleep(seconds): sleep for given duration. -/
 partial def timeSleep (args : List Value) : InterpM Value := do
   let ms : UInt32 := match args with