Jcb/kernel sharding (#436)

* Sharding: out-of-circuit kernel profiler + balanced env partitioner

Add the measure -> partition -> manifest pipeline for splitting a compiled
`.ixe` environment into balanced, low-overhead shards, so large environments
(mathlib is ~631k blocks) can be proven in zero-knowledge as independent
conditional proofs rather than one infeasible monolith.

Two new CLI verbs; the kernel runs once to profile, then sharding is cheap to
re-tune for any shard count:

  ix profile <env.ixe>   ->  env.ixesp   (per-block heartbeats + delta graph)
  ix shard   <env.ixesp> ->  env.ixes    (N-shard manifest + what-if metrics)

Phase A -- out-of-circuit kernel profiler (gated; zero overhead when off):
- Record, per checked constant, its heartbeats (recursive fuel) and the set of
  constants whose definition bodies it delta-unfolds. The *delta-unfold* graph,
  not the static reference graph, is the real cross-shard cost: a shard must
  ingress the body of any foreign block its members unfold.
- KEnv gains an optional ProfileSink (per-worker accumulator). Capture sites are
  the delta-unfold commit points in whnf.rs and per-constant fuel accounting in
  tc.rs; begin_const markers in check.rs/inductive.rs attribute work to the
  right constant. Per-constant cache isolation makes recording sound (no unfolds
  skipped by cross-constant memo) and faithful to in-circuit, un-memoized cost.
- src/ix/profile.rs: the `.ixesp` block-profile model (heartbeats + serialized
  size + CSR delta graph), the ProfileSink accumulator, and explicit
  little-endian (de)serialization (no serde dependency).

Phase B -- partitioner (src/ix/shard.rs, pure):
- Weighted hypergraph partitioning under the connectivity-1 (km1) metric:
  vertices = blocks weighted by heartbeats (balance), nets = blocks weighted by
  serialized size (ingress cost); objective = total cross-shard ingress bytes.
- Recursive bisection via greedy graph-growing + Fiduccia-Mattheyses refinement,
  with cut-net splitting on recursion and a hub-net cap. Leaf-count allocation
  distributes the N-shard budget by heartbeat mass clamped to [1, side size], so
  any N works (not only powers of two) and every shard is non-empty when
  #blocks >= N. A balance-weight cap (heartbeats capped at total/N) keeps splits
  even while accepting the unavoidable imbalance from atomic mutual blocks.
- Parallelized with rayon across independent subtrees (deterministic: identical
  result to serial), with live progress output so a slow run is never mistaken
  for a stuck one.

Phase C -- manifest (src/ix/shard.rs):
- `.ixes` per-shard manifest: member blocks, heartbeat/own-size sums, foreign
  (delta-dependency) block sets, delta-based assumption-tree roots
  (merkle_root_canonical), and a what-if summary (balance, total cross-shard
  ingress, atomic-block floor).

FFI + CLI:
- src/ffi/kernel.rs: profile_anon_ixe (runs the anon kernel over a `.ixe` with
  recording, maps constants to home blocks, writes `.ixesp`) and shard_esp
  (partition + manifest); rs_kernel_profile_anon / rs_shard_esp FFI.
- Ix/Cli/{ProfileCmd,ShardCmd}.lean, Ix/KernelCheck.lean externs, Main wiring.

No external graph-library dependency; the partitioner is self-contained. Kernel
changes are gated behind KEnv::profile_sink, so production checking is
unaffected. Validated end-to-end on initstd/lean/mathlib (64/128/256 shards,
0 empty shards). Follow-up: multilevel coarsening to make mathlib-scale
partitions run in seconds and recover cut quality.

* Sharding: multilevel coarsening for the env partitioner

Replace the flat greedy+FM body of `bisect()` with a multilevel V-cycle
(coarsen → partition the tiny coarsest graph → uncoarsen + refine), so large
environments partition in a fraction of the time *and* at markedly lower
cross-shard ingress. Self-contained to `src/ix/shard.rs`; recursion, leaf-count
allocation, cut-net splitting, rayon parallelism, and the balance-weight cap are
unchanged.

Each bisection now:
- coarsens the sub-hypergraph by heavy-edge matching (merge blocks that co-occur
  in small, heavy delta-nets) under a cluster-weight cap, down to ~256
  supervertices;
- decides the global cut once on that tiny graph (greedy graph-growing + FM to
  convergence, from several diverse seeds, keeping the lowest balanced cut);
- uncoarsens, projecting the cut down and boundary-refining with FM at each
  level.

Deciding global structure on the small graph and only ever refining locally on
the big ones is what improves both axes at once.

Benchmarks (profiled `.ixe` → partition; balance ±5%; flat baseline → multilevel;
0 empty shards, deterministic in every case):

  env       n     partition time     cross-shard ingress
  init      64     5.0s →  2.7s        8.77M →  6.52M   (-26%)
  init      128    6.0s →  2.7s       12.44M →  9.83M   (-21%)
  init      256    6.0s →  3.0s       17.71M → 15.03M   (-15%)
  lean      64     8.0s →  3.4s        9.59M →  7.42M   (-23%)
  lean      128    8.0s →  3.5s       12.59M → 10.48M   (-17%)
  lean      256    7.0s →  3.6s       18.73M → 15.49M   (-17%)
  mathlib   64      99s → 30.8s      185.63M → 93.60M   (-50%)
  mathlib   128     101s → 31.4s     233.58M →131.84M   (-44%)
  mathlib   256     104s → 33.8s     294.85M →184.32M   (-37%)

mathlib (631k blocks, 12.4M delta edges) partitions ~3.2x faster with roughly
half the cross-shard ingress; its heartbeat imbalance also drops (1.66x → 1.53x
at n=64). The non-empty-shard guarantee and determinism hold throughout.

Implementation notes — what real-env validation required beyond the textbook
scheme:

- Fallback pairing in matching: a vertex with no heavy-edge partner (delta-sparse
  or only in hub nets) is merged with the next unmatched vertex. They share no
  tracked net, so the merge is cut-neutral, but it keeps coarsening shrinking
  ~2x/pass instead of stalling far above the target (which had left an expensive
  initial partition on a ~51k-vertex graph).
- Incremental FM gains: a move updates only the changed net's contribution to
  each co-pin (O(Σ pins of the moved vertex's nets)) instead of recomputing
  neighbour gains from scratch (O(Σ neighbour degrees)). Dominant speedup —
  refining the finest level dropped from ~11s to ~0.9s on init.
- Degenerate-split rejection: graph-growing seeded at a light vertex can sweep an
  entire sub onto one side (cut 0) when one atomic block holds more than half the
  balance weight; the initial-partition selector now rejects empty-sided
  candidates and prefers balanced-then-min-cut, so no shard is left empty.
- One boundary-refinement pass per uncoarsen level (measured 1.6–1.8x faster than
  two for only ~3–6% more ingress — a clear win given the margin).

Removes the FM-skip heuristic (`FM_SKIP_VERTICES` / `FM_FULL_VERTICES`): full
refinement is now affordable at every size because it only ever runs on
already-good partitions. Adds unit tests for one-level contraction, cluster-cap
matching, large-cluster separation through the full V-cycle, determinism, and
the non-empty guarantee under a dominant block.

* clippy & fmt

Author: johnchandlerburnham

Ix/Cli/ProfileCmd.lean

@@ -0,0 +1,67 @@
+/-
+  `ix profile <path.ixe>`: run the Ix kernel out of circuit over a serialized
+  `.ixe` environment, recording per-block heartbeats and the delta-unfold graph
+  into a `.ixesp` sidecar. This is the cost model consumed by `ix shard`
+  (see `plans/sharding.md`).
+
+  Recording defaults to *cache-isolated* mode: the kernel clears its
+  cross-constant reduction-memo caches between constants so every delta-unfold
+  re-executes (sound recording) and recorded heartbeats reflect the in-circuit
+  (un-memoized) cost. `--keep-caches` trades fidelity for speed.
+-/
+module
+public import Cli
+public import Ix.Common
+public import Ix.KernelCheck
+public import Std.Internal.UV.System
+
+public section
+
+open Ix.KernelCheck
+
+namespace Ix.Cli.ProfileCmd
+
+def runProfileCmd (p : Cli.Parsed) : IO UInt32 := do
+  let some pathArg := p.positionalArg? "path"
+    | p.printError "error: must specify <path> to a .ixe file"
+      return 1
+  let envPath := pathArg.as! String
+  let outPath : String :=
+    match p.flag? "out" with
+    | some flag => flag.as! String
+    | none      => envPath ++ ".ixesp"
+  let isolate := !(p.flag? "keep-caches" |>.isSome)
+  let quiet   := !(p.flag? "verbose" |>.isSome)
+
+  if let some flag := p.flag? "workers" then
+    let n := flag.as! Nat
+    if n == 0 then
+      p.printError "error: --workers must be > 0"
+      return 1
+    Std.Internal.UV.System.osSetenv "IX_KERNEL_CHECK_WORKERS" (toString n)
+
+  IO.println s!"Profiling {envPath} → {outPath} (isolate={isolate})"
+  let start ← IO.monoMsNow
+  rsProfileAnonFFI envPath outPath isolate quiet
+  let elapsed := (← IO.monoMsNow) - start
+  IO.println s!"[profile] wrote {outPath} in {elapsed.formatMs}"
+  return 0
+
+end Ix.Cli.ProfileCmd
+
+open Ix.Cli.ProfileCmd in
+def profileCmd : Cli.Cmd := `[Cli|
+  "profile" VIA runProfileCmd;
+  "Profile a `.ixe` out of circuit → `.ixesp` (sharding cost + delta graph)"
+
+  FLAGS:
+    out           : String; "Output .ixesp path (default: <path>.ixesp)"
+    "keep-caches";          "Keep cross-constant caches: faster, lower-fidelity, may under-record"
+    workers       : Nat;    "Parallel kernel workers (default: available_parallelism). Plumbs IX_KERNEL_CHECK_WORKERS."
+    verbose;                "Log every constant (default: quiet)"
+
+  ARGS:
+    path : String; "Path to a serialized .ixe environment"
+]
+
+end

Ix/Cli/ShardCmd.lean

@@ -0,0 +1,62 @@
+/-
+  `ix shard <path.ixesp> --shards N`: partition a profiled environment into `N`
+  shards via recursive balanced min-cut bisection, minimizing cross-shard
+  delta-unfold ingress (see `plans/sharding.md`).
+
+  Reads the `.ixesp` produced by `ix profile` (pure offline graph work, so `N`
+  is cheap to re-tune without re-running the kernel). Writes a `.ixes` manifest
+  and prints a what-if report (per-shard heartbeat balance + total cross-shard
+  ingress). The partitioner is self-contained — no external graph-library
+  dependency.
+-/
+module
+public import Cli
+public import Ix.KernelCheck
+
+public section
+
+open Ix.KernelCheck
+
+namespace Ix.Cli.ShardCmd
+
+def runShardCmd (p : Cli.Parsed) : IO UInt32 := do
+  let some pathArg := p.positionalArg? "path"
+    | p.printError "error: must specify <path> to a .ixesp file"
+      return 1
+  let espPath := pathArg.as! String
+  let numShards : Nat :=
+    match p.flag? "shards" with
+    | some flag => flag.as! Nat
+    | none      => 1
+  let balancePct : Nat :=
+    match p.flag? "balance" with
+    | some flag => flag.as! Nat
+    | none      => 5
+  let outPath : String :=
+    match p.flag? "out" with
+    | some flag => flag.as! String
+    | none      => espPath ++ ".ixes"
+
+  IO.println s!"Sharding {espPath} into {numShards} shards (balance ±{balancePct}%)"
+  rsShardEspFFI espPath (toString numShards) (toString balancePct) outPath
+  if !outPath.isEmpty then
+    IO.println s!"[shard] wrote {outPath}"
+  return 0
+
+end Ix.Cli.ShardCmd
+
+open Ix.Cli.ShardCmd in
+def shardCmd : Cli.Cmd := `[Cli|
+  "shard" VIA runShardCmd;
+  "Partition a `.ixesp` into N balanced shards minimizing cross-shard delta"
+
+  FLAGS:
+    shards  : Nat;    "Number of shards N (default 1 = a single shard)"
+    balance : Nat;    "Per-bisection balance tolerance, percent (default 5)"
+    out     : String; "Output .ixes manifest path (default: <path>.ixes)"
+
+  ARGS:
+    path : String; "Path to a .ixesp produced by `ix profile`"
+]
+
+end

Ix/KernelCheck.lean

@@ -142,6 +142,30 @@ opaque rsCheckAnonFFI :
     @& String →                          -- fail-out path ("" = none)
     IO (Array (String × Option CheckError))
 
+/-- FFI: profile a `.ixe` out of circuit, writing a `.ixesp` sidecar with
+    per-block heartbeats + the delta-unfold graph (the sharding cost model,
+    see `plans/sharding.md`). Runs the anon kernel over every checkable target.
+    `isolate` clears the kernel's reduction-memo caches between constants for
+    sound/faithful recording; `quiet` suppresses per-constant progress. -/
+@[extern "rs_kernel_profile_anon"]
+opaque rsProfileAnonFFI :
+    @& String →                          -- .ixe path
+    @& String →                          -- .ixesp output path
+    @& Bool →                            -- isolate caches
+    @& Bool →                            -- quiet
+    IO Unit
+
+/-- FFI: partition a `.ixesp` into `numShards` shards, writing a `.ixes`
+    manifest. `numShards` and `balancePct` are decimal strings (kept ABI-simple).
+    Empty `outPath` skips the manifest. Prints a what-if report to stderr. -/
+@[extern "rs_shard_esp"]
+opaque rsShardEspFFI :
+    @& String →                          -- .ixesp path
+    @& String →                          -- num_shards (N)
+    @& String →                          -- balance percent
+    @& String →                          -- .ixes output path ("" = skip)
+    IO Unit
+
 end Ix.KernelCheck
 
 end

Main.lean

@@ -5,7 +5,9 @@ import Ix.Cli.CheckRsCmd
 import Ix.Cli.ClaimCmd
 import Ix.Cli.CompileCmd
 import Ix.Cli.IngressCmd
+import Ix.Cli.ProfileCmd
 import Ix.Cli.ProveCmd
+import Ix.Cli.ShardCmd
 import Ix.Cli.TreeCmd
 import Ix.Cli.ValidateCmd
 import Ix.Cli.VerifyCmd
@@ -27,7 +29,9 @@ def ixCmd : Cli.Cmd := `[Cli|
     checkRsCmd;
     claimCmd;
     treeCmd;
+    profileCmd;
     proveCmd;
+    shardCmd;
     verifyCmd;
     addrOfCmd;
     ingressCmd;