Complete Phase 9b, begin Phase 9c: consensus containers with math.isqrt

Add math.isqrt builtin (Newton's method integer square root) for
Slot.is_justifiable_after(). Implement Phase 9c consensus container
tests: Slot/ValidatorIndex with custom methods, nested Containers
(Checkpoint, Config, BlockHeader, BlockBody, Block), model_copy on
nested containers, default field values, SSZList with Container
elements composite hash_tree_root, and State.generate_genesis
classmethod factory. All hash_tree_root results verified byte-for-byte
against CPython.

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

Author: pirapira

LeanPython/Interpreter/Eval.lean

@@ -2914,6 +2914,7 @@ partial def getBuiltinModule (name : String) : InterpM (Option Value) := do
     ns := ns.insert "fabs"  (.builtin "math.fabs")
     ns := ns.insert "isnan" (.builtin "math.isnan")
     ns := ns.insert "isinf" (.builtin "math.isinf")
+    ns := ns.insert "isqrt" (.builtin "math.isqrt")
     ns := ns.insert "inf"   (.float (1.0 / 0.0))
     ns := ns.insert "nan"   (.float (0.0 / 0.0))
     ns := ns.insert "pi"    (.float 3.141592653589793)

LeanPython/Runtime/Builtins.lean

@@ -835,6 +835,7 @@ partial def callBuiltin (name : String) (args : List Value)
   | "math.ceil"  => mathCeil args
   | "math.floor" => mathFloor args
   | "math.sqrt"  => mathSqrt args
+  | "math.isqrt" => mathIsqrt args
   | "math.log"   => mathLog args
   | "math.log2"  => mathLog2 args
   | "math.fabs"  => mathFabs args

LeanPython/Stdlib/Math.lean

@@ -95,4 +95,23 @@ partial def mathIsinf (args : List Value) : InterpM Value := do
   | [.int _] => return .bool false
   | _ => throwTypeError "math.isinf() requires a numeric argument"
 
+/-- Newton step for integer square root. -/
+private partial def isqrtLoop (n x : Nat) : Nat :=
+  let y := (x + n / x) / 2
+  if y < x then isqrtLoop n y else x
+
+/-- Integer square root: largest k such that k*k <= n. -/
+private def natIsqrt (n : Nat) : Nat :=
+  if n == 0 then 0
+  else isqrtLoop n n
+
+/-- Python math.isqrt: return integer square root of non-negative integer -/
+partial def mathIsqrt (args : List Value) : InterpM Value := do
+  match args with
+  | [.int n] =>
+    if n < 0 then throwValueError "isqrt() argument must be nonnegative"
+    else return .int (Int.ofNat (natIsqrt n.toNat))
+  | [.bool b] => return .int (if b then 1 else 0)
+  | _ => throwTypeError "math.isqrt() requires an integer argument"
+
 end LeanPython.Stdlib.Math