feat(aiur): Accurate whole-env sharding based on execution measurements - #537
Draft
samuelburnham wants to merge 20 commits into
Draft
feat(aiur): Accurate whole-env sharding based on execution measurements#537samuelburnham wants to merge 20 commits into
samuelburnham wants to merge 20 commits into
Conversation
samuelburnham
force-pushed
the
sb/aiur-planner
branch
from
August 4, 2026 23:55
e61a9c8 to
005d9c9
Compare
…acking Port of sb/measured-ingress's planning layer onto the addr-first kernel (#529), reworked for its lazy fault-in semantics. Profiling (.ixprof v3): the recording kernel's try_get_const consults are drained per constant into a touch graph — the measured set a lazy checker faults in — persisted as a presence-flagged CSR section alongside a new block-level reference graph and a subst_unique counter (splitmix64-keyed dedup of substitution work items: the post-memoization volume a memoizing executor pays). Both graph sections are optional, so older readers' formats stay decodable by version gate alone. Planner: partition_for_aiur_ram bin-packs to a host-RAM cap with faulted-set byte accounting — under #529 the witness always ships the full closure, but only faulted bytes cost ingress trace rows, so a shard's byte feature is owned ∪ touched(owned) (full reference closure as the over-approximating fallback when no touch graph was recorded). The stub/promotion machinery of the original branch is dropped entirely: lazy fault-in computes at run time exactly the set the stubs predicted, with no replay divergence and no repair ladder, and the manifest format stays byte-identical with main (owned-only). Cost models: nlogn(x) = x·log2(x+2) feature form matching Aiur's width·height·log2(height) FFT structure; prove/execute time and RAM coefficients carried over from the pre-#529 aiur bench-suite fits. They are placeholders pending a refit against this kernel — the circuit shrank (deleted positional machinery), the byte feature narrowed to the faulted set, and the recording counters moved under #442 — with provenance noted at the definitions. The costs sidecar (<out>.costs.csv) persists per-shard features incl. subst_unique and nat_arith so the refit has its corpus. CLI: ix shard --backend aiur --max-ram G; ix profile --backend/--top (per-metric block leaderboards with display names) and ix profile sweep (env-wide closure cost sweep: per-root feature CSV + feasibility, min-root-per-hot-block, and diversity reports).
prove --ixe --ixes with no --shard now runs the whole partition through one EnvHandle + one AiurSystem instead of a fire-and-forget loop. Progress persists in the keyed cache ~/.ix/cache/shard-proofs/ (one entry per claim digest, holding the proof's store address): an entry is written only after the proof VERIFIES and binds to the shard's reconstructed CheckEnv claim digest, so a crash or OOM costs only the in-flight shard and re-running the same command resumes. Cached entries are re-verified on resume — the digest pins the claim, not the circuit version. The digest is manifest-independent, so manifests sharing a shard share its proof. Pending shards prove heaviest-predicted-RAM first (from the packer's costs sidecar): if the RAM model's blind spot is going to breach a box it is one of the heaviest shards, and proving those first surfaces the failure in the opening minutes instead of hours in. --jobs N proves shards concurrently (default 1 — each prove peaks at the shard's full predicted RAM). aiur: ExecError::InvalidIOKey now names the channel and key, so a witness that under-ships identifies the constant whose bytes are missing instead of failing generically.
aiur-shard bench backend: profile the env's touch graph, pack at a pinned machine-independent budget (aiurShardBudgetGb = 250, the deliverable prove box — a PR row and its baseline must describe the same partition problem), upload planner metrics (shards, pred-floor-ram, union-bytes) on tight 5% upper bands (profile worker interleaving wobbles touch sets ±2 shards, so no exact pins), then execute the three heaviest-predicted shards through the native kernel and aggregate count-neutral heavy-execute-time / heavy-peak-rss. ix check gains --json/--json-name so a shard check self-reports its bench row with the env parse excluded from the timed window. Init is registered as a benchmark env — it is the shard pipeline's deliverable partition, so its planner trend line matters on its own. Tests/Ix/Kernel/ShardPipeline.lean: end-to-end regression over a small multi-shard env — profile → pack (disjoint cover) → every shard checks → batched prove reaches the composed verdict → second run resumes from the shard-proofs cache with zero pending. Runs under a scratch cache root, never the global ~/.ix/cache; wired into the ixvm suite.
…s preserved ix shard --rebudget K --manifest M.ixes --max-ram G --backend aiur packs only shard K's blocks at the child budget (in the original cut-coherent order); every other shard's block list is reproduced verbatim — asserted, because ShardManifest::build is deterministic in (profile, assignment) and that identity is exactly what keeps the untouched shards' claim digests, and therefore their ~/.ix/cache/shard-proofs entries, valid. The first child keeps id K, the rest append; the aggregation tree's leaf K becomes a left-leaning chain over the children. The costs sidecar is recomputed for every row (identical for untouched shards — the faulted-set union is a function of the owned set alone), so heaviest- first prove ordering picks up the children's predictions. This is the recourse when the RAM model's blind spot packs an outlier shard past what the box can prove: a global repack at a lower budget shifts boundaries from early in the pack order and forfeits most of the proof cache, while a rebudget costs exactly the split shard. Ported from the sb/sp1-shard-agg experiment (where a 148-predicted shard measured ~248 GiB); simplified for the owned-only manifest — the promotion-inheritance step is gone because the witness ships the full closure and a child can never miss an IO key.
…resources fit
Replaces the placeholder coefficients (fit on the pre-addr-first eager
kernel) with a model fit entirely on this kernel, restructured around the
prover's actual work unit.
Stage 1 predicts a run's total FFT cost from profile features:
fft = 2.599e9 + 188.6*nlogn(faulted_bytes) + 71.27*nlogn(subst)
+ 6548*nlogn(def_eq)
def_eq is load-bearing: it appears in every acceptable-tail fit, pricing
the definitional-equality-dense shards that under the old model measured
up to 25% over predicted RAM (reproduced on this kernel before the
refit: the nat-heaviest Init shard proved at 219 GiB against a 175
prediction). nat_arith adds no explanatory power at shard scale on this
corpus and stays a persisted-but-unmodeled feature; the exact path below
covers its tail.
Stage 2 maps FFT cost linearly to resources — physically grounded
(committed LDE volume is proportional to FFT work):
prove_secs = 6.18 + 2.0425 * BFFT RSS_gib = 13.59 + 2.3507 * BFFT
exposed both composed (plan-time, from features) and as *_for_fft
accessors, so a measured FFT cost from an execute-mode stats dump gives
an exact-height prediction — the cheap pre-prove gate for any residual
outlier, which can then be `--rebudget` before burning a prove.
Corpus and fit quality (2026-08-03, this box):
- stage 1: exact FFT of all 34 Init shards at a 250 GiB pack (execute
stats dumps). MAPE 5.0%, worst under -18.5%.
- stage 2: 13 measured Init shard proves spanning 21-81 BFFT. RSS
max|err| 9.9%, wall 12.2%. Composed end-to-end on the proved set:
RAM within 12.4%.
- generalization: 60 InitStd shards the fit never saw. Stage-1 MAPE
5.7%, worst under -15.9% — inside the tail bound.
- execute models refit on the same sweep (wall tracks def_eq alone,
MAPE 9.6%; RSS bytes+def_eq, 3.7%).
AIUR_RAM_USABLE_FRAC rises 0.70 -> 0.75: the composed worst-case
under-prediction (stage-1 tail x stage-2 tail ~ -25%) inverts to 0.797,
leaving the difference as OS/variance margin — headroom that is now
derived from measurement instead of absorbing an unpriced blind spot.
Validation, end to end: repacking Init at 250 GiB yields 32 shards
(stale model: 34, one of which measured unprovable at a projected ~277
GiB); under the new pack no shard's exact-FFT-mapped RAM exceeds the
budget, and the heaviest (88.2 BFFT) proved green at 227.2 GiB measured
vs 220.9 mapped (+2.9%).
Also fixed: both greedy pack loops' tentative cap-test cost accumulated
only bytes+hb before testing — harmless when RAM ignored subst/def_eq,
an under-test under any model with reduction terms. The ShardPipeline
E2E now cuts its tiny env with the fixed-count min-cut partitioner: the
composed model base (~19.7 GiB) exceeds anything a ~200-constant env can
fill, so a RAM budget either degenerates to singletons or one shard;
the claim layer is partition-agnostic and the RAM packer keeps its own
unit coverage.
The witness IOBuffer materialized a shard's full bfs_closure eagerly, 8x-expanded (one G per byte), before the kernel executed a single query — ~2.5 GiB per Init shard buffer, ~30 GiB at Mathlib scale, per in-flight shard. The kernel's laziness was circuit-side only: shipped- but-unfaulted bytes cost zero rows, but the host always paid for the whole closure. IOBuffer gains an optional IOFaultSource backing consulted on a get_info miss: EnvFaultSource resolves ch 2/3/4 keys against the shared mmap'd env and materializes entries on first fault, so host witness RAM scales with the FAULTED set — what the check actually touches — instead of the shipped closure. Soundness-neutral: faulted bytes are blake3-verified against their content-addressed key exactly like eagerly-seeded ones, and the idx/len wires are unconstrained witness either way. Trace generation reads through a frozen lookup (get_info_frozen): it runs circuits in parallel over a shared buffer and never needs to fault — execution already materialized every entry it read. EnvHandle holds Arc<Env> so a backing outlives any handle borrow. The claim-channel seeding (ch 0/1) is factored into seed_shard_check_env_claim, shared by the eager and lazy builders, and all four with-env check/prove FFI paths now use the lazy variants.
Shard boundaries come from executing the env's check schedule through the codegen'd Aiur kernel — thin-frontier CheckEnv claims, the exact unit a prover pays for — with a running cost readout, replacing the counter-prediction path for Aiur. `ix shard env.ixe` runs the scan by default; `--backend zisk` chains profile + guest-cost pack; the .ixprof packer is unchanged for Zisk. - Two-term cut: a shard ends when RAM-per-fft * fft + record bytes reaches the budget's usable headroom — both resources a prove consumes. - One RAM mechanism: a per-worker record-byte cap ((0.70*box - 10)/workers, 8 GiB autoscale floor; --workers 1 grants the whole allowance), enforced inside execution via thread-local accounting in QueryMap::insert and codegen'd record_budget_exceeded() polls (ExecError::RecordBudgetExceeded). A trip mid-segment is an early cut; a block over the cap alone is skipped and named. Fleet RAM is workers x cap by construction — no reactive control. - True costs: every shard is re-priced with one cold CheckEnv — the claim its prove executes — and the merge pass consolidates on true costs to a fixpoint. - Manifest v2: tagged per-shard cost (Unknown / ProfileHeartbeats / ZiskCostUnits / AiurFft, raw fft units), version-checked in both the Rust and Lean parsers; ix prove orders heaviest-first from the manifest; the costs CSV sidecar is report-only. - Parallel scan over chunked schedule with work stealing; --fail-fast (default) / --no-fail-fast uniform across ix shard / check / prove, skipped blocks inventoried in failed.csv; IX_SCAN_LIMIT_BLOCKS slice knob for reproducers. - aiur-shard bench backend gains whole-env rows: scan-time, peak-rss, shards, max-shard-fft, and fft-cost in raw fft units so env totals join the existing per-constant plot. Validated at 250 GiB: Init 40 shards / 1,719 BFFT total (152 s, peak 91 GiB); InitStd 76 / 3,330 (255 s, 127 GiB); Lean 108 / 5,086 (383 s, 123 GiB); zero skipped blocks; deterministic partitions; prove spot check 74.8 GiB real vs 76.1 predicted.
The claim layer's per-claim costs (in-circuit assumption-tree hashing, env_walk frames never memo-shared across claims, members assumed by one claim then checked by the next) inflated the incremental readout ~25% per-block, which forced a blanket re-price pass doubling scan wall. Batching divides that overhead by the batch size and removes intra-batch frontier edges entirely; measured drift of the running readout vs one-cold-claim re-priced costs on Init: K=16 +11.6%, K=64 +3.7%, K=128 +0.9% — within the cut's ε margin, so the readout serves directly as the manifest cost and the blanket re-price reverts to merged-only. Any batch-level event needing per-block attribution — the segment's first claim crossing the cut, a kernel reject, a record-cap trip with nothing banked — ends the segment at the last clean checkpoint and re-enters that batch through a NARROW window, one block per claim, where the single-block semantics apply verbatim: a lone block over the cut is emitted alone with its measured cost, a rejected or over-cap block is named and skipped. A remainder re-queued mid-window rediscovers the event deterministically, so partitions stay scheduling-independent. IX_SCAN_BATCH_BLOCKS overrides the batch size (1 restores per-block claims). Validated at 250 GiB (vs the re-priced pipeline): Init 40 shards / 1,734 BFFT in 86 s (was 40 / 1,719 / 152 s); InitStd 76 / 3,269 / 130 s (was 76 / 3,330 / 255 s); Lean 90 / 5,171 / 206 s (was 108 / 5,086 / 383 s) — ~45% less wall, and Lean packs 17% fewer shards because cut placement now sees near-true running costs instead of inflated ones. ixvm suite green.
Aiur execution carries no RAM instrumentation again: the thread-local record-byte budget, its charge in QueryMap::insert, the RecordBudgetExceeded variant, the interpreter polls, and the 3,538 codegen-emitted checks are all removed (kernels regenerated). The scanner's per-worker record share becomes a PLAN — worker-count arithmetic and logging, not an enforced cap: a worker's record is bounded at claim boundaries only, and the recourse for pathologically dense content is fewer workers. The narrow window remains solely for kernel-reject attribution. Scan partitions are unchanged (Init byte-identical pre/post). New: ix check --ixe env.ixe --execute — execute-only whole-env check through the codegen'd Aiur kernel, in parallel, with no partition, manifest, or prove concerns. Segments exist only to drop records (bytes-only cut at the planned share); the report is the check verdict: blocks checked, kernel rejects named, total measured FFT. --jobs bounds workers, --no-fail-fast inventories every reject. This is the Aiur-kernel counterpart of the Rust kernel's whole-env check, for wall-clock comparison and divergence hunting. Validated: Init 51,003/51,003 blocks in 68 s (peak 82.6 GiB); InitStd 87,847/87,847 in 116 s (145 GiB); Lean 152,596/152,596 in 210 s (164.5 GiB — exactly the 20-worker x 8.2 GiB plan line). ixvm suite green.
AiurSystem::peak_prove_bytes(record): predicted peak prover RSS as the max of the schedule's three phase peaks — witness (QueryRecord + padded main traces + base-field lookup witness, all parallel-alive), stage-2 transition (stage-1 LDEs + tree + lookup witness + logUp messages with their batch-inverse copy + extension traces), and FRI open (all committed LDEs at 8·blowup bytes per cell + three Merkle trees + retained fold layers + open buffers) — plus preprocessed-gadget residency. Heights are next_power_of_two of the record's unique queries; widths, lookups, slot argument widths, and quotient degrees come from the compiled circuits; blowup and folding arity from the system parameters. Zero fitted constants. Mirrors multi-stark rev be1755e's allocation schedule. IX_AIUR_PRED_RAM=1 prints the prediction with per-phase breakdown at prove time. Validated against /usr/bin/time MaxRSS on five stratified Init shards (19.1-66.5 BFFT): residuals -0.4% to +3.0%, uniformly the expected allocator/decode-cache overhead above live bytes, and the open phase dominates in every case as the schedule analysis predicts. The empirical line needed a 25% usable-fraction absorber for its blind spots; this needs ~5%.
The scanner's cut and sidecar move from the fitted resource line to the analytic peak-prove-RSS model (AiurSystem::peak_prove_bytes) at budget x 0.95 x (1-eps), eps default 2% — the margin is the measured predicted-vs-MaxRSS residual (+0.6..+3.0% across six stratified proves on three envs), not a blind-spot absorber. Production STARK parameters consolidate in Protocol.lean (were triplicated across prove/verify); the scan FFI takes the compiled system and drops its per-call toplevel decode. Workers become 'ix shard-worker' child processes under user-delegated cgroup memory.max (oom.group=1), speaking a two-verb line protocol (SCAN in; SEG/SKIP/END out; a unit range degenerates to a single-block claim, so narrowing needs no verb). A worker that outgrows its cap is OOM-killed ALONE and recovered: respawn (fresh decode cache), retry once, then unit-narrow the dying batch; a block too dense for its slot's share retries on the BIG lane (whole-pool cap, serialized) and only a block that dies even there is named resource-infeasible in failed.csv. Fleet RAM is the sum of kernel-enforced caps, independent of content. Thread pool remains for in-process callers (tests). Sizing is width-first and uniform — full-core width, cap = measured pool / width, additive soft record cut below the cap (segments end gracefully at claim boundaries; the kill is reserved for mid-claim growth) — so planning wall time never depends on the prove budget: segments scan at RAM-optimal size and shards are assembled by the merge pass summing adjacent segments to the cut (sums are conservative for every cost in play: shared deps derive once, padded heights are subadditive). The refine re-measure pass is deleted with the coupling that motivated it. ix check --execute gains the same pool (execute-only whole-env check: no partition, record-drop segments, named rejects, measured totals). Jettisoned: the legacy Aiur counter-model packer (shard_esp_aiur, partition_for_aiur_ram, rebudget_manifest_shard + FFI/CLI/extern, -889 lines), fleet_plan and its planning constants, the blanket re-price. Surviving counter-model constants are profile-sweep advisory only and say so. Entry-overhead accounting corrected (13 -> 21 B: stored hash, multiplicity element, table slot); parent overhead is the measured post-schedule baseline instead of a guess. Validated: kill-recovery smoke (two live SIGKILLs mid-scan, 30000/30000 blocks covered, zero skips, cgroups cleaned); six-prove model validation ±2.3% worst; ixvm suite green throughout. ix prove --ixes batch mode replaces chunked --jobs barriers with RAM-aware admission: heaviest-first, the next shard's prove is admitted whenever the in-flight sum of sidecar pred_ram plus its own fits 0.92 x box; shards without predictions degrade to serial and --jobs remains as an optional ceiling.
Worker memory caps move from hand-managed cgroup dirs to systemd-run --user --scope -p MemoryMax (MemorySwapMax=0): a session-scoped parent cannot migrate children into the user-service subtree itself (common-ancestor rule), so the manual cgroup.procs attach never actually took effect and workers ran silently uncapped — the 3 GiB-free incident on the FLT fleet. The user manager performs the migration over D-Bus and garbage-collects the scopes; the manual CgroupBase machinery is deleted. Availability is probed once per pool and its absence is a loud UNCAPPED warning. Verified with a starved-cap run: kernel SIGKILLs at every over-cap batch, per-block narrowing recovers, full coverage. Children read the parent's derived schedule from an order file (IX_SCAN_ORDER_FILE env; addresses + min-cut order; deleted when the pool drops) instead of each re-deriving it — 30 workers re-running the FLT bisection concurrently was minutes of pure startup. The pool plan gains honest slack: fraction 0.72 with a 12 GiB OS reserve on top of the measured parent baseline, and a 6 GiB cap floor that bounds the auto worker count, so every child brushing its cap simultaneously still leaves tens of GiB free.
A big-lane retry capped at the whole pool could overcommit the box while the regular fleet sits at its caps (observed: a monster measurement at 34 GiB atop a 151 GiB fleet drove used memory to 245 GiB). The big cap is now the derived remainder — ram minus the fleet pool minus the measured baseline and OS reserve (~70 GiB here) — which still measures every provable-at-budget block; only content beyond that headroom is named infeasible.
A capped worker's death is self-caused and deterministic (measured 244/246 same-index re-deaths on FLT): retrying the range re-executes exactly the batch that proved too big, paying the most expensive claim in the pipeline to learn nothing. Death now narrows the dying batch immediately, deleting the retry state. The cap floor rises 6 -> 9 GiB, sized for the real constraint the FLT run measured: a fresh segment's opening claim re-derives its shared dependencies cold, a ~4-7 GiB working set on dense content. Below that, kill-and-narrow was the common case — 490 deaths and ~39% of all execution spent re-measuring narrowed units — instead of the rare one. Fewer, fatter workers (pool/9) with cold batches that fit.
The QueryRecord is the only structure that grows during a scan (env caches parse without storing), so memory control anchors on it exactly: QueryMap::heap_bytes() counts arena fill, stored hashes, and the hash table's allocation, and record_heap_bytes() is the worker's segment-cut threshold. record_retained_bytes stays as the analytic prove-RAM model's record term — the two intentionally differ (the model is calibrated end-to-end against measured proves). Worker sizing derives from the box in one pass: pool = RAM - parent baseline - OS reserve - a reserved big-lane budget; width = cores - 2 while each even slice clears a 5 GiB floor; the slice is the systemd cap and the record cut is the slice minus the worker baseline and one claim's worst-case growth. Claims shrink 128 -> 32 blocks so that mid-claim growth (~4 GiB per 128 dense blocks, scaling with K) fits the headroom; the measurement drift sits between the measured +3.7% (K=64) and +11.6% (K=16), and drift only overstates costs. Death handling loses the span ladder: a kill is record growth, not claim width, so the fresh worker continues full-width from the committed index (replaying a range from its start re-accumulates the same record and dies at the same index; narrowed claims poisoned the tail by killing every warm worker that touched them). A block with two zero-progress attempts is measured once on the serialized big lane or named resource-infeasible. RSS reads survive only in heartbeats and the parent's one-time baseline measurement — never in control flow. Arena accounting counts fill, never reserved capacity: rounding open segments to hugepage granules put ~3.4 GiB of phantom bytes on the threshold across a few hundred touched maps and fragmented Init into 2423 segments (2.8x wall regression) before the fill-only fix. Init @ 250: 82.1 s wall, 30 workers x 6.3 GiB slices, record cut 3.3 GiB, 0 deaths, 111 raw segments -> 64 shards, max predicted prove RSS 231.1 GiB vs the 232.8 cut.
…ing, opt-in cold re-price, exec-only workers
…nd; addr-of owning-shard lookup
…d re-price A shard's true cold cost is the cost of the union of its segments' records (per-query cost is context-free), so each segment ships a per-circuit membership sketch built from the record's stored entry hashes — exact lists up to 1024 uniques, 8 KB HyperLogLog registers above — and the merge unions sketches, feeds the estimated union heights to the analytic cost/RAM model, and cuts directly at the budget. Manifest fft moves to the 539-grounded formula (AiurSystem::fft_cost_from_raws, the Rust mirror of Statistics.lean). The cold re-price pass, PACK_OVERSHOOT, the PRICE worker verb, price files, and --reprice are deleted. Validated on recompiled Init/InitStd/Lean @500 GiB: 11/18/28 shards (re-priced baselines cut 9/19/27) at unchanged scan walls; heaviest shards prove green. Known follow-up: the union keeps per-claim assumption/boundary entries the prove's single claim never pays (measured 1.26x on an InitStd shard), so estimates run ~25% high — counts still land at re-price level because 541+539 shrank true content by a similar factor.
samuelburnham
force-pushed
the
sb/aiur-planner
branch
from
August 8, 2026 01:46
005d9c9 to
e1a6f27
Compare
…zero compute cost A standalone claim re-derives its whole dependency spine (no frontier): bitblast's closure proved at 473.5 GiB — more than the entire InitStd env shard that contains it plus 6655 neighbors (348 GiB). The fix is to make the closure its own env and partition it: extract → measured union-pricing scan → prove every shard, with thin frontiers internal to the closure, composing to the same unconditional verdict at per-shard RAM. Measured on bitblast (5659-const closure, 495 GB box): standalone 5:43 / 341.8 s compute / 473.5 GiB; 2 shards @480 budget 4:46 / 284.0 s / 325.8 GiB; 9 shards @108 budget 5:40 / 333.5 s / 83.2 GiB — the frontier tax and next_power_of_two padding savings cancel, so splitting is free in wall and total compute while RAM tracks the budget. The 9-shard shape fits the 128 GB CI runner class with margin, and shards prove concurrently (--jobs / a fleet), collapsing wall toward the slowest shard — a RAM-bound serial job becomes parallelizable units. Plumbing: ix prove --ixes --shard grows --json/--json-name (prove-time windowing the FFI trip, peak-rss, proof-size — the rows contract); ix bench run --backend aiur routes heavy-tier Vectors.csv constants through cutAiurClosureShards (extract + scan at the watchdog ceiling, one spawn per shard, <name>/shard-K sub-rows, aggregate parent row that lands only when every shard is green); light tier keeps the single leaf. Strategy, measurements, and caveats in docs/heavy-constant-sharding.md.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Aiur sharding: measured scan-and-cut
What this does
Shard boundaries for Aiur proving are now measured, not predicted.
ix shard env.ixeexecutes the env's check schedule through the codegen'd Aiur kernel — the same thin-frontierCheckEnvclaims a prover pays for — with a running cost readout, and cuts a shard wherever the measured cost reaches the RAM budget. The previous counter-based cost model (fit on ingress bytes / substitutions / def-eq counts) mispredicted real content by up to 16× in both directions and OOM'd shards it called safe; execution is the mandatory prefix of proving, so measuring it prices the prove exactly.Design
RAM-per-fft · measured fft + measured record bytesreaches the budget's usable headroom — both resources the prove actually consumes.0.70·box RAM / workers), enforced inside kernel execution. Fleet RAM isworkers × capby construction. A block that outgrows the cap alone is skipped and named infailed.csv, same as a kernel-rejected block — pathological content is excluded by name, not engineered around.CheckEnv— exactly the claim its prove executes — so manifest costs carry no scan-side inflation. The.ixesmanifest (format v2) stores them per shard;ix proveorders heaviest-first from it.IOBufferfaults env bytes on demand, so witness RAM tracks the touched set, not the shipped closure — for scan and prove alike.--fail-fast(default) /--no-fail-fastuniform acrossix shard/check/prove; whole-env rows in theaiur-shardbench backend (scan time, peak RSS, shards, fft totals).Validation (250 GiB budget, 32-core / 250 GB box)
All blocks covered (zero skips), partitions deterministic, every predicted prove RSS under budget. Scan cost is ~2% of the pack's prove cost. Measured prove check: shard predicted 76.1 GiB / 60.5 s proved at 74.8 GiB / 59.4 s.
Usage
The shard-pipeline E2E runs in
lake test -- --ignored ixvm(also in PR CI).Known limits