bench: one shared constant set, runtime zisk sharding, stage-scoped aiur measures

[samuelburnham]

The benchmark suite ran different constants per backend, curated through Benchmarks/Vectors.csv's tier/shard_target/primary columns plus a fixed aiur selection, and the aiur pipeline's stage measures collided with the plain Phase-1 names via a mode-scoping convention. This consolidates all of it.

Shared constant set. Ix/BenchConstants.lean (a plain importable array of (name, env)) replaces Vectors.csv as the single selection: every per-constant backend (aiur, zisk, ooc, lean4lean) runs the same constants, now including Std.HashMap, Lean.Json, and Multiset.sort at the heavy end. The tier/shard_target/primary columns, fixedSelections, --full/--tier/--shard-only/--csv flags, and the BENCH_FULL/BENCH_SHARD tokens are gone with the CSV. benchExclusions shrinks to hard infeasibility only: bitblast on the zkVMs, whose ~18B-step atomic mutual block crashes the ZisK executor and cannot be split by the shard cutter. bitblast itself is commented out of the set with a re-add note — its Aiur prove exceeds any current host, so a scheduled run could only re-document the same OOM; --consts/BENCH_CONSTS still run it on demand.

Runtime zisk sharding. With the tier column gone, every zisk constant goes through extract → profile → ix shard --max-ram <ceiling> at bench time: the planner's RAM budget sizes the partition from the closure's predicted cost, so a closure that fits gets a one-shard plan and runs as a single leaf. Artifacts still pre-cut in bench-main's compile job and ride the zkshards cache; a failed cut falls back to the whole closure under the watchdog. Formerly-light constants now measure from their extracted sub-env (host peak-rss tightens once; guest cycles unchanged).

Stage-scoped aiur measures. The pipeline's measures rename from the plain/recursive- split to a uniform stage- prefix (stage1-prove-time, stage2-fft-cost, …) so the KZG stages join as stage3-/stage4- without renames. stagePrefixOf/dropStagePrefix move to the registry and parse the prefix generically; formatting kinds, units, improvement direction, and stage-table labels all derive from the base name. The execute mode keeps plain Phase-1 names on its own testbed, so the modes no longer share measure names at all. Throughput returns as a column in every stage table plus the ledger (stage1-/stage2-throughput, and pipeline-throughput = constants / total-time), emitted by bench-typecheck; none carry thresholds — constants is pinned exactly, so each is the pure inverse of an already-bounded time. bench-recursive-verifier adopts the same stage1-/stage2- keys.

Dashboard. New plots now that #567 merged: Aiur Total Throughput, Aiur Total Peak RAM Usage (which stage sets the ceiling can shift as stages are added), and Aiur Stage 1 Proof Size (it sizes stage 2's in-circuit workload). The input-constants overlay renames to Kernel Input Constants and sources from the zisk testbed — sharded execution keeps every closure feasible, so its rows upload even where the aiur prove OOMs and the row is dropped. Zisk Shards becomes a regular full-set plot (runtime-planned counts, flat at 1 for closures that fit). The sync now warn-skips a measure bencher hasn't seen yet, like benchmarks and testbeds, so it can run at any point mid-migration.

CI hardening. bench-main's upload step no longer fails on a cell whose every row OOM'd — the new single-constant aiur cells (Lean, Mathlib) may have that as their steady state — the empty bmf result skips the upload and the run step stays the failure authority. A bench-measures unit suite pins the stage-prefix parsing edge cases.

Migration: the renamed measures start fresh bencher series (the old recursive-* measures orphan; other testbeds keep the plain names). After this lands on main, let bench-main finish, then dispatch the plots sync. A !benchmark aiur run before that first bench-main completes shows n/a base columns for the stage measures; no threshold reset is needed.