ix shard: static profile-free strategy (walk-edge min-cut + predicted-cost rebalance)

[arthurpaulino]

ix shard <path.ixe> --shards N now partitions an environment without an out-of-circuit profiling run. The previous pipeline (unchanged, now behind --profile <path.ixprof>) partitions the delta-unfold graph recorded by ix profile and balances on Rust-kernel heartbeats; both of those signals turn out to mis-model what the Aiur kernel actually pays, and the static strategy beats it on every measured axis.

Quality metric

Partition an env into N shards, typecheck every shard with the native IxVM (real blake3), and read Total FFT cost from ix check --ixe <env> --ixes <manifest> --shard K --stats-out F. Lower mean = cheaper overall; lower stddev = better balance; the max shard is the parallel wall-clock. All numbers below are from this harness on Init (60,599 consts, 8 shards) and Init+Std (105,492 consts, 24 shards).

What the Aiur kernel actually ingresses

The kernel's constant resolver (get_ci) is a memoized Aiur function that fault-loads and blake3-verifies each constant at its first use, so its distinct-key set IS the in-circuit ingress set. Enumerating it during shard runs and comparing against (a) the shard's owned set, (b) the static thin frontier (ixon::shard_claim::walk_edges), and (c) a journal of the Rust kernel's delta-unfold targets showed, on two probes (one binder-heavy, one with ~35k delta unfolds):

• owned and thin frontier are loaded completely, always;
• the blocks behind frontier projection wrappers are loaded always (block granularity absorbs this term: wrappers share their block's vertex);
• genuine below-frontier reduction read-through is 0.5-1.5% of loads;
• every cross-shard Rust delta-unfold target was loaded by Aiur, but ~90% of them were already thin-frontier members.

So Aiur ingress is ~99% determined by the static reference structure: cutting reference edges is what costs, and the profiled delta graph is nearly redundant with it. Under the baseline partition of Init the delta objective saw 1.1 MB of cross-shard ingress while the realized static frontier was 71 MB — the old min-cut was optimizing a shadow of the real cost.

Cost model

Least-squares fit of measured per-shard FFT cost over static features, trained on 56 shards from 7 differently-shaped partitions of Init:

cost(S) ~ 28201 * owned_bytes(S)
+ 681 * sum_{b in S} size(b)^1.5
+ 38000 * frontier_bytes(S)

(sizes = serialized block bytes; mean |err| 4.7% on shards >= 3e11). A frontier byte pays ingress only (blake3 + parse); an owned byte additionally pays typechecking, which concentrates superlinearly in large proof bodies — hence the per-block ^1.5 term. It is per-block, not (sum size)^1.5: how bytes are packaged into constants is exactly what it measures (ten 1 KB lemmas cost ~3x less than one 10 KB proof at equal byte count), and per-block additivity is what makes it usable as a movable weight. Applied unchanged to Init+Std at 24 shards the model predicted per-shard cost with 4.5% aggregate bias — the constants are Aiur-kernel physics, not env-specific.

Why min-cut + rebalance, not min-cut alone

Byte-balanced static min-cut already dominates the baseline on mean (cut the real frontier), but its realized stddev stalls at ~15%, and two refinements measured WORSE:

• tightening the per-bisection tolerance 5% -> 2%: stddev 18.1% — the residual is model error (bytes can't see the superlinear term), not loose balance;
• using the fitted weight as the bisection balance weight: stddev 19.6% — per-cut tolerance compounds across log2(N) levels of integer budget splits into 1.6-1.9x max/min drift regardless of the weight's quality.

The fix is a global post-pass: greedily move blocks from the most to the least expensive shard under the fitted model (frontier deltas updated exactly per move; the model is additive so each move is O(deg)) until predicted costs are within 1% of the mean. It converges in tens of moves from a byte-balanced start and is idempotent at the fixed point. No per-bisection mechanism can do this job: the frontier term each shard pays depends on the cut itself, which vertex-weight balancing cannot see.

Measured results

Init, 8 shards (mean / stddev / max shard, FFT cost units):
profiled baseline 1.020e12 / 17.7% / 1.391e12
static + rebalance 0.729e12 / 7.2% / 0.777e12 (-29% / -/ -44%)

Init+Std, 24 shards:
profiled baseline 6.317e11 / 30.6% / 1.019e12
static + rebalance 4.305e11 / 8.9% / 5.005e11 (-32% / - / -51%)

The baseline degrades with shard count (more shards = relatively more frontier, which its objective can't see, and deeper bisection drift); the static strategy holds.

Implementation

• ix_kernel::shard: shard_static (byte-balanced min-cut over the static profile through the existing multilevel partitioner, then rebalance_static, then the usual .ixes manifest), model constants documented at STATIC_OWNED_PER_BYTE. Rebalance bookkeeping exactness is tested via second-pass idempotence.
• crates/ffi: static_block_profile builds a BlockProfile from a .ixe alone — vertices are ingress units (Muts block / standalone constant) with real serialized sizes, edges are block-level walk_edges, and the byte balance weight rides the subst counter (the partitioner's vertex weight is linear in op counters, so vweight is exactly proportional to size). rs_shard_env_static is the FFI entry; rs_shard_static_graph (ix shard graph) now shares the same builder.
• CLI: the positional argument is the .ixe; --profile <path.ixprof> selects the previous pipeline verbatim (verified byte-identical output); a .ixprof passed positionally errors with a migration hint; --max-cycles/--max-ram budgeting still requires --profile (its cycle/RAM model is calibrated on profiled op counters — a static cap mode is future work).