Jcb/kernel sharding

[johnchandlerburnham]

Sharding: measure → partition → manifest for proving .ixe environments

What & why

A compiled Lean environment is infeasible to prove in zero-knowledge as one
monolith (mathlib is ~631k blocks, 12.4M delta-unfold edges). This PR adds the
measure → partition → manifest pipeline that splits an environment into N
balanced, low-overhead shards, each provable as an independent conditional proof.

Two new CLI verbs. The kernel runs once to profile; sharding is then pure,
cheap graph work, re-tunable for any N without re-running the kernel:

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

Scope is measure + partition + manifest — it stops before proof generation.
No external graph-library dependency; the partitioner is self-contained.

How it works

Phase A — out-of-circuit profiler (src/ix/profile.rs, kernel instrumentation).
Runs the Ix kernel over the .ixe, recording per checked constant its heartbeats
(recursive fuel) and the set of constants whose 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.
Capture is gated behind an optional KEnv::profile_sink (zero overhead when off);
per-constant cache isolation makes recording sound (no unfold skipped by a
cross-constant memo) and faithful to in-circuit, un-memoized cost. Output is the
.ixesp block-profile (heartbeats + serialized size + CSR delta graph), with
explicit little-endian (de)serialization (no serde dep).

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. Solved by
recursive balanced bisection with cut-net splitting and rayon parallelism across
subtrees. Each bisection is a multilevel V-cycle: coarsen the sub-hypergraph
by heavy-edge matching down to ~256 supervertices, decide the global cut there
(greedy graph-growing + FM, several seeds), then uncoarsen, boundary-refining
with incremental-gain FM at each level. Leaf-count allocation guarantees every
shard is non-empty (any N, not just powers of two); a balance-weight cap keeps
splits even while accepting the unavoidable imbalance of atomic mutual blocks.

Phase C — manifest (src/ix/shard.rs).
The .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).

Benchmarks

Profiling (one-time kernel run, isolated caches):

  init      87,844 blocks,  1.0M edges    18s
  lean     152,596 blocks,  1.2M edges    22s
  mathlib  631,006 blocks, 12.4M edges   318s

Partitioning (ix shard, balance ±5%; 0 empty shards, deterministic):

  env       n     time     imbalance   cross-shard ingress
  init      64    2.7s      5.8x         6.52M
  init      128   2.7s     11.5x         9.83M
  init      256   3.0s     23.0x        15.03M
  lean      64    3.4s      5.0x         7.42M
  lean      128   3.5s     10.0x        10.48M
  lean      256   3.6s     19.9x        15.49M
  mathlib   64   30.8s      1.5x        93.60M
  mathlib   128  31.4s      1.6x       131.84M
  mathlib   256  33.8s      2.0x       184.32M

The bigger the library, the better it shards: mathlib reaches 1.5–2.0x
heartbeat imbalance, while init/lean are floored by a single 592k-heartbeat
atomic block they're too small to dilute (the .ixes report flags this).

Multilevel coarsening (the second commit) makes mathlib partition ~3.2x
faster (99s → 31s at n=64) with ~half the cross-shard ingress
(185.6M → 93.6M) vs the initial flat greedy+FM bisection, and improves init/lean
by ~2x on both axes — global cut decisions are made once on a tiny coarse graph,
and only local boundary refinement ever touches the big graphs.

Testing

• Unit tests in shard.rs (synthetic fixtures): cluster separation through the
  full V-cycle, one-level contraction, cluster-cap matching, determinism, and the
  non-empty guarantee under a dominant block. Recorder smoke tests in the kernel
  (profile_sink_records_delta_edge_and_fuel). Full suite green (1045 lib tests).
• End-to-end on init / lean / mathlib × {64, 128, 256}: 0 empty shards,
  byte-for-byte reproducible manifests.