feat(aiur): Measured-ingress sharding - #524
Draft
samuelburnham wants to merge 30 commits into
Draft
Conversation
The summary previously printed only whole-env aggregates, so finding expensive blocks meant hand-parsing the .ixprof. Print top-N block leaderboards — heartbeats first (Aiur-relevant ordering), then substitution nodes, ingress bytes, and the predicted-Zisk-steps sharding cost last — with display names: the anon env carries no names (get_anon_mmap stops before section 4), so the section-5 entries are re-read via the lazy index — cheap, bodies skipped — and each block gets its lexicographically-smallest member name (projections resolve through profile_block_of; a name-map failure falls back to raw addresses rather than failing the profile). --top 0 disables; the flag crosses the FFI as a decimal string like rs_shard_esp's numeric params. Aiur's memoized query execution collapses repeated work, so raw substitution volume overweights repetitive blocks; of the recorded counters, heartbeats (already downstream of the kernel's memo tables) track measured fft-cost closest, hence the ordering. TODO: a calibrated Aiur prove-time/RAM model — measured fft-cost from bench-typecheck is ground truth until then.
Count each substitution-node visit deduplicated by its work identity — (expression hash, binder depth, substitution context) mixed through a splitmix64 finalizer — alongside the raw visit count. A memoizing executor (Aiur proves each unique query once; repeats are memo-table lookups) pays only for distinct work, so the raw count overweights repetitive blocks; the deduplicated counter is the candidate feature for that regime. The substitution context is a fold of the fvar identities set once per top-level instantiate_rev (its recursion never re-enters subst, so a single thread-local slot suffices). The seen-set clears per constant in take_op_counts, the same scope as every other counter. Both bumps compile out on the zkvm target. Persisted per block: BlockEntry.subst_unique, .ixprof VERSION 1 -> 2 (record 56 -> 64 bytes), ProfileBuilder::block gains the sixth column, readers reject v1 files (regenerate any local .ixprof).
Direct model from kernel profile counters to Aiur prove time and peak host RAM — no Aiur execution or FFT-cost intermediate. Features are run-level aggregates in nlogn(x) = x*log2(x+2) form (Aiur's prover work is a sum of width*h*log2(h) FFTs whose dominant circuit heights track one counter each): prove_s = 1.43 + 2.38e-7*nlogn(bytes) + 9.06e-7*nlogn(subst) ram_gib = 3.67 + 1.18e-6*nlogn(bytes) + 1.57e-5*nlogn(hb) Calibration: n=13 bench-suite closures — features from ix shard extract + ix profile per closure, targets from the bencher.dev ix project's aiur-check-prove-x64-32x report on main @ 3312c3f (2026-07-23, the blowup-4 + 20-bit-grinding soundness regime of #513). prove MAPE 12% (LOO 16%), RAM MAPE 15% (LOO 19%). Tail cross-check: the BVDecide goCache_Inv_of_Inv._mutual closure (5x past the largest fitted point) predicts 530 GiB vs 536 GiB from the independent fft-linear extrapolation. Known blind spot: limb-arithmetic/append-proof-heavy closures under-predict to ~0.55x (no native counter tracks the klimbs gadget family), absorbed by AIUR_RAM_USABLE_FRAC = 0.7. bytes must stay a model feature regardless of fit scores: cross-shard foreign ingress is pure bytes work, and a bytes-free model would price duplication at zero. Datasets: fresh_calibration.csv, bencher_prove_main.csv. ix profile --backend all|aiur|zisk selects which models the summary prints; the Aiur section replaces the former TODO and adds a top-N board by marginal per-block prove-ms. ix shard --backend aiur packs to a RAM budget via partition_for_aiur_ram — same cut-coherent-order + greedy next-fit structure as the Zisk cap packer (the ordering stage is factored into cut_coherent_order), with the cap test evaluating the monotone nonlinear RAM model over running shard aggregates. Manifest format unchanged. Validated on InitStd (87,847 blocks): --backend aiur --max-ram 64 packs 117 shards, heaviest exactly at the 44.8 GiB cap, largest atomic block 39.1 GiB, cross-ingress duplication 9.0% of own bytes; whole-env predictions correctly rank the real Aiur OOM constant first.
Answers the discovery question the per-closure flow could not: which constants can Aiur execute/prove at a given RAM budget, and which small closures isolate which cost bottleneck. One whole-env profile amortizes over every query — the sweep walks each named constant's full reference closure over the env's constant graph (projections and mutual members fold into home blocks, so Constant.refs alone carries every cross-block edge), sums the .ixprof per-block counters over the members, and applies the Aiur models. No extraction, no re-checking: 87,847 InitStd closures sweep in ~0.3 s after ~4 s of graph setup. The delta-unfold graph is NOT used for membership — it under-approximates the reference closure (referenced-but-never-unfolded constants). Summing whole-env per-block counters over reference membership matches a fresh per-closure profile because isolate-mode counters are context-free; validated against four independently profiled closures (exact byte totals, counters within single-digit percent). Per-root CSV plus three reports: feasibility at --budget (with the cheapest prove-infeasible closures — minimal bottleneck reproducers), the cheapest closure containing each of the --top-blocks most expensive blocks, and --reps feature-mix-diverse prove-feasible representatives (farthest-point sampling seeded on nat-arith share, the model's blind spot). Execute-side models calibrated like the prove pair, against the aiur-check-execute suite at main @ 3312c3f (n=14 incl. the 205 B-fft BVDecide mutual): exec_s from nlogn(bytes)+nlogn(subst) (MAPE 18%, LOO 22%), exec RAM from nlogn(bytes) alone (MAPE 6%, LOO 8%; the only non-negative fit — BVDecide holdout 1.08x). BlockEntry gains whnf/def_eq/nat_arith (per-block, .ixprof v2 record 64 -> 88 bytes; v2 is unreleased so no compat bump), and ProfileBuilder::block takes a BlockCounters struct. Block display names now prefer human names over compiler-generated Ix.<hash>. aux aliases.
First real shard proves falsified the Aiur packer's byte accounting: shards predicted at 16.6-33.6 GiB OOM-killed a 50 GB cgroup. The shard claim (shardCheckEnvClaim) builds its env tree over the owned blocks' FULL reference closure — frontier constants are assumptions (not re-checked), but every closure byte is ingressed and hashed — while the packer charged own_size + delta-frontier cross-ingress, the Zisk closure-injected-leaf accounting, undercutting Aiur bytes several-fold. The fix threads the reference graph end-to-end: - .ixprof gains a trailing reference-graph CSR (every cross-block Constant.refs edge, projections/mutual members folded into home blocks), written at profile time; readers treat its absence as an old recording and the Aiur sharder rejects such files. - partition_for_aiur_ram packs against closure-UNION bytes: per-shard membership is epoch-marked, a candidate's delta is a BFS that stops at union members (each closure walked at most twice), and hb/subst stay owned-only. The per-block RAM floor is now its closure bytes — the quantity the runtime actually enforces — and shard_esp_aiur writes a <out>.costs.csv sidecar with each shard's accounting and predictions for measured-vs-predicted comparison. - profile sweep reads the stored graph instead of rebuilding it. Acceptance (Init, ix prove --ixes --shard K under a 50 GB watchdog, measured via VmHWM): three shards predicted 21.3/21.6/21.5 GiB proved successfully at 20.9/31.7/19.3 GiB peak — 0.98x/1.46x/0.90x, the one overshoot inside the documented limb-arithmetic blind-spot band. The same partition under the old accounting OOM-killed all three. Init's honest floor: the String.Slice ForwardSliceSearcher model stack's 6.4 MB closure predicts ~175 GiB for any shard containing it — infeasibility the planner now reports instead of emitting doomed plans.
An Aiur shard's CheckEnv claim ingresses its owned blocks' entire transitive reference closure, and the packer priced it that way. Measured over four environments, that accounting is what does not scale: the same bytes are re-ingressed and re-hashed by shard after shard, 56x over for Init, 509x for InitStd, 1778x for Lean, 1667x for Mathlib. Lean alone reaches 325.80 GB of union bytes for a 183 MB environment. Price instead the ingress a frontier-trusted kernel demands, in two states. Owned blocks are ingressed FULL, as is everything they delta-unfold (an unfolded body's references must resolve) and any block whose body reduction can consume. A frontier block is ingressed as a type-only AXIOM: trusted rather than re-checked, never unfolded, so the walk continues through its TYPE references only. Both states pay the block's serialized bytes once; only the recursion differs. `.ixprof` gains the two facts that walk needs (v3, no compatibility with v2): a type-reference sub-graph, and per-block kind flags marking blocks reduction can consume — inductives, constructors, recursors, quotients, projections — which cannot stand in as axioms. Type-reference collection resolves Expr::Share through the constant's sharing table; without that a type built from shared subexpressions silently under-reports its closure. At a 250 GiB budget, against the previous accounting: Init 699 -> 34 shards, floor 174.8 -> 14.6 GiB InitStd 11749 -> 62 shards, floor 482.9 -> 64.2 GiB Lean 56293 -> 90 shards, floor 538.2 -> 64.2 GiB Mathlib 227150 -> 1433 shards, floor 3829.7 -> 359.9 GiB InitStd and Lean are infeasible at any box size under the old accounting (floors needing 690 and 769 GiB budgets); both now fit this 250 GiB host. Mathlib still does not: one block carrying ~12 MB of direct references holds its floor at 359.9 GiB. The kernel does not yet implement frontier-trusted ingress, so these predictions describe the kernel this branch is building, not the one on main. Shard proving against main's kernel would under-provision.
`augment_with_blob_refs` classifies any ref absent from the const-position map as a BLOB via the sentinel, `build_ref_idxs_and_blobs` emits ref index 0 for it, and `convert_expr` turns Expr::Ref into Const(0, levels). Absence is read as "blob", never as "missing", so the reference rebinds to whatever constant occupies kernel position 0. `load_verified_blob` is no barrier: it applies the same check as `load_verified_constant` — blake3 of the served bytes against the address — so a constant's own bytes verify on the blob channel. Driving that path as an adversarial prover would (flip the channel-4 discriminator to "blob", serve the constant's real bytes on channel 5) produces no false accept: over Nat.add's 17-constant closure, all 16 victims are rejected, because Const(0) is type-incompatible and the kernel fails downstream. The defence is incidental — a type error — not a check that a ref resolves to the constant it names. These tests pin the rejection so a change that starts accepting an erased constant fails. A second assertion pins the reason: the corrupted-bytes control must fail DIFFERENTLY from the real-bytes case (hash comparison vs a later assertion), which is what shows the real bytes cleared blob verification and reached the rebinding. 13 of 16 victims get that far; the rest fail before the blob channel is consulted. Without it the per-victim pins would keep passing while silently covering nothing. The documented channel-4 argument (ClaimHarness) reaches the right outcome by the wrong mechanism: refs do not dangle, they rebind.
`augment_with_blob_refs` classified any ref absent from the const-position map as a BLOB. Absence says nothing, though: a blob is legitimately absent, and so is a constant the witness declined to ingress. The second case resolved to ref index 0, so `convert_expr` turned Expr::Ref into Const(0, levels) and the reference silently rebound to whatever constant occupied kernel position 0. Nothing downstream caught that by construction. `load_verified_blob` applies the same check as `load_verified_constant` — blake3 of the served bytes against the address — and a constant's own bytes hash to its own address, so the blob channel accepts them and cannot tell the two apart. Rejection came only from the rebound expression failing to typecheck, which is incidental rather than a check that a ref resolves to the constant it names. Classify from the ch-4 discriminator instead. 0 = blob, whose bytes arrive on ch 5; anything else = a constant that was never ingressed, which poisons the ref. An address with no ch-4 entry fails at the read. The poison is carried into `ref_idxs` rather than rejected at classification time, so only a ref an expression actually dereferences fails — a constant may carry ref-table entries nothing uses. `Expr::Ref` and `Expr::Prj` assert on it at the use site; `lookup_addr_pos`, which has no expression to blame, rejects outright. This is a prerequisite for frontier-trusted ingress, where a shard stops ingressing its frontier's references: absence is exactly how that kernel represents "not ingressed", and every honest frontier ref would otherwise rebind to position 0 and fail to check. Costs +0.05-0.08% FFT across the pinned kernel-check fixtures; pins bumped. Interpreter/codegen parity holds. Still open: a host that LIES on channel 4, declaring a real constant to be a blob, keeps the old blob path and the position-0 rebinding. Closing that needs blob and constant addresses domain-separated in the hash preimage so a constant's bytes cannot verify as a blob.
`run_check_env` ingressed its owned blocks' entire transitive reference closure and then had `check_all_skipping` skip the frontier constants it had just paid full price to load: the trust boundary existed at checking but not at ingress. Load the assumption tree before ingress so the frontier is known while walking, and rewrite each frontier constant into an Axiom carrying its type alone. Its value is dropped, so its references are never followed and the shard stops ingressing its frontier's transitive closure — which is where the duplication lives. The rewrite happens in `load_with_deps`, right after blake3 verification and before layout, pos_map and conversion, so the rest of the pipeline is untouched: `sharing`, `refs` and `univs` are preserved so the type's Expr::Ref indices still resolve, and an Axio occupies the same single kernel position a Defn would. The constant is still verified against its address, so the type the stub carries stays bound to the address the claim's assumption tree names. Axioms are never delta-unfolded (Whnf unfolds only Defn; DefEq only Defn and Thm), so "trusted, not re-checked, never unfolded" needs no new reduction guard — it is what an Axiom already means, matching the Lean kernel's Opaque declaration kind. Only standalone Defn and Axio may sit on a frontier. Inductives, constructors, recursors, quotients, projections and mutual blocks have bodies that reduction consumes, so a type-only stub would silently lose the reductions that need them; reaching one on a frontier asserts instead. The packer marks those blocks NOT_AXIOMATIZABLE so the host does not place them there. Costs +0.25% FFT median (+0.32% max) on the pinned fixtures, which run with an empty frontier; pins bumped. Interpreter/codegen parity holds. Sharded checking does not work yet: `shardCheckEnvClaim` still derives the frontier as closure-minus-owned, which includes the kinds this rejects, and does not close shards under delta. The host change is next.
samuelburnham
changed the title
`CheckEnv` carried one assumption root and the kernel used it for two different jobs: `check_all_skipping` skipped those constants, and `axiomatize_frontier` rewrote them to type-only stubs. Those are different sets, so one root cannot express both. A shard skips checking everything it does not own. But it must still ingress in FULL anything it reduces through — a definition it unfolds, an inductive whose recursor rules it applies — even though another shard is responsible for checking that constant. Stubbing such a block loses exactly the reductions that need it, which is why sharded checking broke when the kernel started stubbing the whole assumption set. Folding those blocks into the owned set instead is not available: owned sets partition the environment so each constant is checked exactly once, and two shards may reduce through the same constant. So `CheckEnv` gains a second root, `stubbed`, naming the subset of `assumptions` whose bodies were withheld. Breaking wire change: the variant now serializes a third optional address, and `run_check_env` stubs from `stubbed` while skipping from `assumptions`. Hosts pass `stubbed: none` for now, which ingresses every constant in full and restores the pre-stubbing behaviour end to end — a shard check over Init passes again. The per-shard stub set has to come from the partition, which knows which blocks a shard reduces through; it is not derivable from the environment alone. Wiring it through the manifest is next, and is what actually collects the win.
Two instrumentation changes that paid for themselves while investigating why sharded checking with frontier stubs fails. `ExecError::InvalidIOKey` reported "invalid IO key" and nothing else, which is indistinguishable from any other missing witness entry. It now carries the channel and the key, and the key identifies the constant or blob whose bytes the host failed to seed — that turned three rounds of hypothesising into one measurement. `TypeChecker::touched` records every constant CONSULTED while checking one constant, whether its body was unfolded or only its type read, dumped with IX_TOUCH_STATS=1 and gated on the profile sink otherwise. Lazy fault-in pays for exactly that set, so its size against the constant's reference closure decides whether faulting in is worth doing. Over a 400-block sample of Init: 19 constants touched at the median against a 273-block closure, means 37 and 631 — about 9%. docs/lazy-fault-in.md records the design that measurement gates, and why the frontier-stub approach it replaces cannot work: the set a shard may only mention versus must compute with is not predictable, because stubbing a definition removes its definitional height and so changes lazy-delta's unfold-order decisions. The measurement perturbs what it measures.
Carrying both a position and an address on KExprNode.Const, keeping the position authoritative and migrating consumers module by module, does not work: the address participates in structural identity. Aiur's store dedupes by content and def-eq compares nodes structurally, so the same constant with a real address and with a placeholder are different nodes. Measured on the pinned fixtures: mixed filled/placeholder addresses fail 40 checks, all recursors; uniformly placeholder addresses fail none. So the position-to-address change must land atomically. Also recorded: lake build does not validate the Aiur DSL (ix codegen is the real compiler), the dual field costs ~1% FFT for nothing, and the prerequisite for the atomic switch is synthesizing mutual-block member addresses for Expr.Rec — cprj_content_addr is the precedent, the Defn/Indc/Recr cases do not exist yet. docs: a transitional address index costs more than it saves An address-keyed Const with an eager driver still needs address -> position, which the position-aligned addrs list answers only by linear scan. Carrying a reverse index alongside it was implemented and measured: all 64 pinned fixtures regressed — median +5.78% FFT, worst +55.32% on a small closure where the eager map build dominates, aggregate +1.08%. Nothing improved, because real primitives already sit early in addrs so the replaced scans are short. The destination has no global position table: Const(addr) resolves through get_const(addr) against the witness, memoized by Aiur's call cache, and both top and addrs disappear. So the index solves a problem only the transitional design has, and Steps 1 and 2 must land as one change. Also records what get_const must do for projections: load the member's block and convert that member alone, so a Muts block yields one KConstantInfo per member address rather than a positional expansion.
Address-keyed constants resolve a reference through the constant's own
`refs` table, which works for `Expr.Ref(i)` but not for `Expr.Rec(i)`: a
mutual-block member is named by index within its block and has no entry
there. Its address is a synthesized projection address, and only the
constructor case (`cprj_content_addr`) existed.
Adds the Defn, Indc and Recr cases plus a `member_content_addr` dispatch on
the member's kind, built the same way: construct the projection `Constant`
the compiler would have built — empty sharing/refs/univs — serialize it
in-Aiur and hash. Mirrors `Constant::new(ConstantInfo::XPrj{..}).commit()`.
Both sides are pinned to one fixture: `member_addr_tests` in the
test-only `kernel_unit_tests` entrypoint asserts the in-circuit results
against hexes that `proj_addr_fixture` asserts on the Rust side, so a drift
in the projection encoding fails loudly instead of silently rebinding a
mutual-block reference.
Production circuit cost is unchanged — these are unused until the
position-to-address switch, so codegen prunes them.
This is the prerequisite identified in docs/lazy-fault-in.md for making
that switch atomic, which it must be: the address participates in
structural identity, so a dual-field migration is not available.
The .ixprof (v4) now carries a touch CSR: per block, every block the kernel CONSULTED while checking it — type and height reads included, not just unfolds. Unlike the delta and reference graphs this is a measurement of the ingress a lazy checker demands, recorded by the already-lazy native kernel under cache isolation. The Aiur packer seeds each owned block's touched set as FULL ingress, so every constant whose content steered the recording run's decisions ships whole (heights intact) and lazy-delta replays identically; only blocks the check never consulted are left to the type-only stub expansion. Measured on Init at the 250 GiB budget: 60 shards, 24.1 GiB atomic floor (full-closure: 699 / 174.8; the delta-predicted stub model claimed 34 / 14.6 but fails every shard at k_check). Optional .ixprof sections gain one-byte presence flags instead of end-of-input inference, so any subset can be absent unambiguously.
Revives the frontier-stub machinery (owned/foreign/stubbed through the .ixes manifest, both hosts, both FFI paths) with its set source swapped from delta-graph prediction to the profile's measured touch graph: every block the owned checks consulted ships whole, and only never-consulted blocks become type-only stubs. The prediction-only producer cascade is off in measured mode — a consulted body's unfolds were consulted too, and recorded against the owned consumer directly. Init at the 250 GiB budget: 60 shards, 25.6 GiB atomic floor, 53/60 green on first pass — against 35/35 failures under prediction. The remaining divergence (the Aiur kernel's caches are not the Rust kernel's, so it occasionally reduces where the recording short-circuited) gets an escalation ladder: IX_STUB_PROMOTE_ROUNDS=N promotes every stub to full N times, pushing the frontier N reference hops out. Includes the four fixes found running the wiring: the LIFO stub/full mark split, blob pull-in, host/kernel axiomatizability parity, and primitive blocks pinned non-axiomatizable via PrimAddrs.
A global promotion round fixed all seven divergent Init shards and broke a previously-green one: ingress-set changes shift kernel positions, and the position-consistency asserts can flip either way with the layout. So the escalation is per shard — IX_STUB_PROMOTE="2:1,43:2" gives each failing shard its own radius while every other shard keeps the set that already passed (a bare N still applies to all). The costs sidecar and cap report are re-priced from the emitted sets rather than the pack walk's round-0 estimate, so they describe the manifest that ships. The flip also shows the position mismatches (c_induct vs ind_pos scale) are a latent witness/kernel disagreement about duplicate-wrapper canonicalization, set-dependent rather than replay divergence; tracked for a real diagnosis separately.
The bytecode interpreter's assert_eq failure now reports the function it fired in plus the caller chain and locals map — with these, a shard-43 'assert_eq mismatch: 5716 != 5704' resolved to k_infer_only_core's Proj arm jamming whnf on a stubbed type-alias Defn, via def-eq's struct-eta → proof-irrelevance path. That closed the 'class B' investigation: the position-scale mismatches are the same replay divergence as the def-eq failures, not a canonicalization bug (see benchdata classB-diagnosis.md). diag_duplicate_wrappers (ignored, env-var driven) scans one shard's ingress set for duplicate Muts wrappers, absent-const refs (silent Const(0) rebinding candidates), stub types referencing absent constants, and per-address identity/referrer breakdowns.
ix check --repair packs the manifest from the profile, checks every shard, escalates exactly what failed, repacks, and rechecks only the escalated shards until green. Init at --max-ram 170: 93/93 green after one escalation iteration, 15.6 min wall. Escalation has two rungs, tracked per shard because any ingress-set change moves the replay's execution paths: - targeted: the IxVM kernel now REPORTS the stub it jammed on when a Proj head mismatches (report_wanted_stub aborts through empty channel 98, so the error names the address; +0.0002% FFT on passing shards). The driver ships that one block whole — measured +0.00% shard RAM. 4 of Init's 8 divergent shards resolved this way, all wanting the same type-alias Defn. - frontier round: promote every stub one ref hop (the def-eq divergence path has no report yet). +35-51% shard RAM — the rung that forces the conservative pack budget. The per-shard spec (K:N rounds, K:+HEX named blocks) replaces the IX_STUB_PROMOTE env var: parse_promote_spec in shard.rs, an explicit FFI argument, and ix shard --promote for manual use. A repeated want on the same shard falls back to a frontier round, so the precise rung cannot stall the loop; the ladder's top is full closure, the original semantics, so repair always terminates. lake test green; 624 kernel-crate tests green; clippy clean.
Stubs are now tagged: axiomatize_frontier marks its synthesized axiom with flag 2 (is_unsafe_ci treats only exact 1 as unsafe, so the tag stays out of the safety product). Wherever reduction jams on a tagged stub — whnf_const_head's stuck exit, the general chokepoint every silent consumer inherits, plus lazy delta's ineligible exits — the kernel appends the stub's address to IO channel 97 (want_if_stub, non-aborting: a stuck head is usually benign and a false def-eq verdict is legitimate mid-search; Aiur's call memoization dedupes the log per head). On shard failure the FFI appends the logged addresses to the error, and the repair driver ships exactly those blocks whole. Wants are discovered one failure point at a time (execution aborts at the first assert), so the driver's default iteration budget rises to 8 and each failure ships its full pre-abort want list. Init validation, both budgets, zero frontier rounds: - --max-ram 170: 93/93 green, 8 shards escalated by 2-17 named blocks; - --max-ram 250: 60/60 green, 7 shards escalated by 2-34 named blocks, every escalated shard still at its packed RAM (172.9-175.7 GiB predicted) — the full-cap packing no longer sacrifices headroom to escalation, so Init's deliverable drops from 93 shards to 60. Reporting cost on a passing shard: +0.0003% FFT. lake test green.
prove --ixes with no --shard now proves the whole partition as one resumable run: env handle, compiled toplevel, and AiurSystem built once; progress persisted to <manifest>.proofs.csv, where a row is appended only after the shard's proof VERIFIES and binds to the shard's reconstructed CheckEnv claim digest. A crash or OOM costs the in-flight shard; re-running resumes. Rows whose digest no longer matches the manifest (a repair escalation changed the sets) are discarded and re-proven. --jobs proves several shards concurrently for boxes that fit them. Ends with the composed verdict: disjoint cover + every shard bound to a verified proof. The digest binding immediately caught a real bug: the Lean claim reconstruction (shardCheckEnvClaim, which ix verify's composition path also uses) omitted the referenced-blob pull-in the Rust witness builder does, so every Rust-proved shard claim diverged from its reconstruction and composition verification could never bind a shard proof. The reconstruction now mirrors the Rust closure exactly. Validated on a 4-shard fixture: prove+verify+bind green, resume skips proven shards, a re-packed manifest invalidates its rows, and the composed verdict prints. lake test green. prove: batch heaviest-predicted shard first The RAM model carries a content residual it cannot see (the klimbs blind spot: two shards with equal bytes+heartbeats can differ ~1.5x in trace RAM by circuit mix). If any shard of a manifest is going to breach the watchdog, it is one of the heaviest — so the batch proves in descending predicted-RAM order, read from the packer's costs sidecar. A model miss then surfaces in the opening minutes instead of hours in, and every shard after the heavy head is strictly safer than what already passed. Without a costs sidecar, manifest order stands. Fixture-verified: prove order follows pred_ram_gib descending; resume and the composed verdict unchanged.
Port of the Zisk deferred-verification insight (never-forced constants are never hashed) to Aiur witnesses: every stub now ships as a GHOST — a ch-4 kind-2 discriminator and nothing else. The kernel fabricates a fail-closed node at the ghost's position (ixon flag-3 axiom; convert_axiom emits an unmatchable universe-arity sentinel + reporting flag 2), so refs to it resolve instead of dangling, and any semantic access fails the arity assert closed while NAMING the address on channel 98 (report_wanted_ghost) — the repair driver ships wanted ghosts whole. Blob pull-in and outside-ref discriminators now come from non-ghost members only, mirrored exactly in the Lean claim reconstruction (digest parity) and the Lean witness path. Lying on the kind-2 discriminator only withholds an assumption's content: it can turn passes into failures, never failures into passes. Batch-prove resume now RE-VERIFIES surviving sidecar rows instead of trusting the digest match alone — a digest match can pair with a proof made under a different circuit version (any kernel edit regenerates the codegen and the verifying key); such rows are discarded and re-proven. Caught live on the fixture after this very change. Status: fixture green end-to-end (check, batch prove, resume, composed verdict); lake test + clippy green. Init-scale finding, run in flight: ghosting widens the replay-divergence tripwire from value reads (unfolds, 7/60 shards) to any type/arity read — most shards escalate a handful of named blocks, converging via the driver. Net bytes accounting and whether the type-only stub tier should return as the middle escalation rung: pending that run. ghosts v2: classify stub consults Aiur-side, ghost only in the prove path v1 (ghost every stub, discover needs by execution) could not converge: type-reads surface one failure point per run. v2 classifies with the kernel itself: checks and the repair loop keep type-only stub witnesses (the fast-converging regime), and the prove path executes once with stubs while const_num_lvls_logged records every stub whose type infer consults on IO channel 96 — a width-neutral swap in the Const arms, one narrow circuit added. The prove FFI then rebuilds the witness ghosting the unconsulted stubs and proves that; a misclassification aborts naming the address (arity sentinel), and the classification is deterministic for the same witness, so the ghosted run cannot diverge from the run that produced it. The claim digest is classification-independent (blob pull-in restored to cover all members' referenced blobs — unread blob leaves cost nothing, the kernel loads blob bytes on demand), verified live: the ghosted shard-43 proof verifies the same claim as its pre-ghost proof. Measured on Init (baselines from this morning's runs): - shard 43: 142.7 -> 128.9 GiB (-9.7%), 2174/2177 stubs ghosted - shard 57: 189.0 -> 178.8 GiB (-5.4%), 1811/1815 stubs ghosted - wall ~flat: the classification execute (~10-20 s) roughly cancels the hashing savings; persisting classifications per manifest would recover it. This corrects the ~40% prediction and the model reading behind it: the RAM model's byte coefficient is correlational, not causal — the causal per-byte slice (blake3 + deserialize + convert) is ~21% of the fitted slope. The packer is unaffected (it predicts totals); the remaining ~90% of prove RAM is reduction-trace, where the env-machine WHNF line is the lever. Fixture green end to end; lake test, 624 kernel tests, clippy green.
The costs sidecar now carries the three per-block content counters summed over owned blocks, alongside hb/subst — the accumulating input for an eventual multi-feature RAM-model refit. Exploratory read on the 7 comparable measured rows: the model's residual correlates with nat_arith and def_eq (+0.46 each) and negatively with bytes (-0.79, the over-weighted correlational coefficient again). Far too few rows to refit — the point is that every future pack+prove now accumulates the dataset for free.
Classification persistence: the shard prove FFI takes a cache path (<manifest>.ghosts.csv, digest-keyed rows, digest,- marker for classified-empty); a hit skips the ~10-20 s classification execute. Staleness handling is the proofs-sidecar's: a changed claim digest simply never matches. Fixture-verified: first run classifies and writes, second run hits on every shard. Tests/Ix/Kernel/ShardPipeline.lean: the measured-ingress pipeline's first in-repo end-to-end regression — Lean env → .ixe → v4 profile → measured packing → all-shards check on stub witnesses → batched prove (classify, ghost, prove, verify, bind) → composed verdict → resume. Runs in the gated ixvm suite (lake test -- ixvm --ignored). Refreshed the 64 FFT pins the reporting instrumentation had shifted (+0.01-0.07% each — the want/consult hooks' cost, previously measured at +0.0003% aggregate). The gated suite is where the pins live, which plain lake test skips — earlier all-green claims covered only the default suites; the full gated suite is now green too: 685 passed, 0 failed, parity included.
…ess-only CSV files should carry benchmark vectors or analysis data, not mutable cache state. Both prove-path caches are keyed by claim digest, so the filename can BE the index: <ns>/<claim_digest> under ~/.ix/cache, with staleness by construction (a repacked shard has a new digest, which never names an old entry) and atomic temp+rename writes. - shard-proofs/<digest> holds the verified proof's store address (replaces <manifest>.proofs.csv). Resume becomes manifest-independent: two manifests sharing a shard share its proof. - stub-consults/<digest> holds the concatenated 32-byte consulted addresses, empty file = classified-empty (replaces <manifest>.ghosts.csv and its marker rows). - Store.cacheDir resolves ~/.ix/cache/<ns>; runShardProveAllNative takes an optional cacheRoot so the pipeline test stays hermetic. - costs.csv stays: per-shard analysis data, the CSV-appropriate case. Rename: the witness tiers are now self-describing — a constant ships FULL, as a TYPE-ONLY stub, or ADDRESS-ONLY (position and address, no bytes); "ghost" said nothing. Touches the kernel DSL (addr_only_arity, report_wanted_addr_only), the Rust witness builder, and comments. Codegen output is byte-identical; gated ixvm suite green (685).
The rebase onto main (flat quotient commitment, kernel formalization changes) replayed the branch's stale codegen snapshot and pin table; regenerate aiur_ixvm.rs from the merged kernel DSL and re-pin the 61 kernel-check FFT costs at their measured values. String.trim -> trimAscii.toString for main's toolchain deprecation (--wfail). Full gated set green: aiur aiur-hashes ixvm multi-stark recursive-verifier, 1356 tests.
The per-constant aiur rows never enter the sharded regime (a full-closure single-constant witness ships no stubs), so shard-pipeline wins and regressions were invisible to !benchmark. New perEnv backend, joining !benchmark and bench-main through the registry-driven matrix: - plan: ix profile (touch graph) + ix shard at a PINNED 250 GiB budget (machine-independent so PR and baseline describe the same partition problem). Plan wall time is logged, not uploaded. - execute: the three heaviest-predicted GREEN shards, one process per shard; ix check --shard gains --json/--json-name and reports execute-time (env parse excluded from the window) + peak-rss. A stub-witness replay divergence records a 'diverged' row (not 'rejected' — nothing failed to typecheck) and the walk takes the next-heaviest, so the aggregates compare green-vs-green; the divergence count is logged, not uploaded. Uploads five measures: shards / pred-floor-ram / union-bytes on tight 5% upper bands (profile worker interleaving wobbles touch sets ~±2 shards, so no exact pins), heavy-execute-time (MEAN over the green sample) and heavy-peak-rss (max) on 10% — count-neutral slugs and count-robust semantics, so tuning the sample size never orphans the bencher trend lines. pred-floor-ram is tracked as the cap-overflow tripwire but not plotted (the heavy execution charts the real RAM): four dashboard plots. BenchPlots titles/units/group order and the bencher-thresholds-reset workload list synced. Validated on Init (59 shards, 0 divergent heads, ~10 GB peak per execute) and InitStd (119 shards, 3 divergent heads walked past, aggregate still built from greens).
Init is the Aiur shard pipeline's deliverable env — the partition the full-Init proof runs over — so its planner trend (shards, union-bytes) matters on its own; InitStd's does not subsume it. Joins the perEnv fan-outs (compile, decompile, aiur-shard) in both bench-main scheduling and !benchmark via the registry-driven matrix; aiur-recursive's matrix label moves to the new head env but stays env-independent. Validated: aiur-shard-Init-execute = 59 shards, 0 divergent heads, heavy executes green at ~10 GB peak.
samuelburnham
force-pushed
the
sb/measured-ingress
branch
from
July 30, 2026 03:31
dfa1175 to
60b9457
Compare
One-shot diagnostic from the class-B position-mismatch investigation; the divergence mechanism is diagnosed and documented, and the kernel now names its wanted stubs directly (ch 97/98), so the probe has no remaining job. It also failed under CI's nextest --run-ignored all, which runs ignored tests without the IX_DIAG_* env artifacts it expected.
Member
Author
|
!benchmark |
Member
Author
|
!benchmark aiur-shard |
|
| constant | prove-time (main) | prove-time (PR) | Δ% | throughput (const/s) (main) | throughput (const/s) (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | execute-time (main) | execute-time (PR) | Δ% | verify-time (main) | verify-time (PR) | Δ% | proof-size (main) | proof-size (PR) | Δ% | fft-cost (main) | fft-cost (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Array.extract_append |
51.166 s | 51.180 s | +0.0% | 33.340 | 33.330 | -0.0% | 96.36 GiB | 96.57 GiB | +0.2% | 10.837 s | 10.861 s | +0.2% | 192.0 ms | 164.1 ms | -14.5% (1.17× faster) 🟢 | 25.88 MiB | 26.22 MiB | +1.3% | 36.21B | 36.26B | +0.1% |
ByteArray.utf8DecodeChar?_utf8EncodeChar_append |
50.444 s | 49.683 s | -1.5% | 57.290 | 58.170 | +1.5% | 102.09 GiB | 102.37 GiB | +0.3% | 9.424 s | 9.544 s | +1.3% | 168.1 ms | 168.9 ms | +0.4% | 25.96 MiB | 26.30 MiB | +1.3% | 38.11B | 38.24B | +0.3% |
Char.ofOrdinal_le_of_le |
39.747 s | 39.948 s | +0.5% | 72 | 71.640 | -0.5% | 79.88 GiB | 80.15 GiB | +0.3% | 7.038 s | 6.992 s | -0.7% | 167.3 ms | 166.4 ms | -0.5% | 25.90 MiB | 26.24 MiB | +1.3% | 29.15B | 29.25B | +0.3% |
Vector.extract_append._proof_2 |
29.500 s | 28.971 s | -1.8% | 48.850 | 49.740 | +1.8% | 53.14 GiB | 53.20 GiB | +0.1% | 6.054 s | 5.928 s | -2.1% | 162.4 ms | 167.2 ms | +3.0% | 25.55 MiB | 25.89 MiB | +1.3% | 21.18B | 21.22B | +0.2% |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
24.931 s | 24.127 s | -3.2% 🟢 | 79.140 | 81.780 | +3.3% 🟢 | 50.05 GiB | 50.20 GiB | +0.3% | 3.530 s | 3.543 s | +0.4% | 172.3 ms | 165.3 ms | -4.1% 🟢 | 25.72 MiB | 26.06 MiB | +1.3% | 15.71B | 15.76B | +0.4% |
String.split |
23.297 s | 23.037 s | -1.1% | 83.660 | 84.600 | +1.1% | 48.12 GiB | 48.16 GiB | +0.1% | 3.214 s | 3.263 s | +1.5% | 181.3 ms | 170.0 ms | -6.2% (1.07× faster) 🟢 | 25.92 MiB | 26.25 MiB | +1.3% | 14.22B | 14.27B | +0.4% |
List.mergeSort |
16.017 s | 16.486 s | +2.9% | 99.770 | 96.930 | -2.8% | 31.73 GiB | 31.89 GiB | +0.5% | 2.333 s | 2.318 s | -0.6% | 164.9 ms | 167.1 ms | +1.3% | 25.77 MiB | 26.11 MiB | +1.3% | 10.46B | 10.49B | +0.4% |
Vector.append |
5.204 s | 5.346 s | +2.7% | 108.770 | 105.870 | -2.7% | 8.32 GiB | 8.38 GiB | +0.8% | 615.2 ms | 615.6 ms | +0.1% | 154.9 ms | 161.7 ms | +4.3% |
24.38 MiB | 24.72 MiB | +1.4% | 2.21B | 2.22B | +0.4% |
Nat.gcd_comm |
4.361 s | 4.420 s | +1.4% | 95.170 | 93.880 | -1.4% | 7.64 GiB | 7.92 GiB | +3.6% |
474.5 ms | 486.1 ms | +2.4% | 159.4 ms | 161.5 ms | +1.3% | 23.99 MiB | 24.33 MiB | +1.4% | 1.56B | 1.57B | +0.5% |
String.append |
3.207 s | 3.253 s | +1.5% | 110.090 | 108.500 | -1.4% | 5.64 GiB | 6.05 GiB | +7.2% (1.07× larger) |
361.8 ms | 363.2 ms | +0.4% | 140.5 ms | 160.9 ms | +14.5% (1.15× slower) |
23.30 MiB | 23.63 MiB | +1.4% | 869.46M | 873.31M | +0.4% |
Int.gcd |
2.617 s | 2.671 s | +2.1% | 87.510 | 85.750 | -2.0% | 4.79 GiB | 4.84 GiB | +1.1% | 296.0 ms | 298.4 ms | +0.8% | 153.4 ms | 147.8 ms | -3.6% 🟢 | 22.92 MiB | 23.25 MiB | +1.5% | 539.56M | 541.99M | +0.4% |
Nat.sub_le_of_le_add |
2.434 s | 2.481 s | +1.9% | 78.060 | 76.580 | -1.9% | 4.88 GiB | 4.81 GiB | -1.4% | 284.8 ms | 291.4 ms | +2.3% | 142.5 ms | 144.8 ms | +1.6% | 23.39 MiB | 23.72 MiB | +1.4% | 451.92M | 453.84M | +0.4% |
Nat.add_comm |
1.317 s | 1.356 s | +3.0% | 38.710 | 37.600 | -2.9% | 4.59 GiB | 4.61 GiB | +0.5% | 200.9 ms | 200.5 ms | -0.2% | 134.3 ms | 142.6 ms | +6.2% (1.06× slower) |
21.85 MiB | 22.19 MiB | +1.5% | 48.99M | 49.19M | +0.4% |
13 constants · 4 with regressions · 4 with improvements (|Δ| > 3.0% on any metric).
|
| constant | shards (main) | shards (PR) | Δ% | pred-floor-ram (main) | pred-floor-ram (PR) | Δ% | union-bytes (main) | union-bytes (PR) | Δ% | heavy-execute-time (main) | heavy-execute-time (PR) | Δ% | heavy-peak-ram (main) | heavy-peak-ram (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
FLT |
n/a | 1,403 | n/a | n/a | 187.390 | n/a | n/a | 7,731,490,354 | n/a | n/a | 60.980 | n/a | n/a | 16,382,435,328 | n/a |
FLT/shard-7 |
n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a |
FLT/shard-713 |
n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a |
FLT/shard-85 |
n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a |
4 constants · 0 with regressions · 0 with improvements (|Δ| > 3.0% on any metric).
aiur-shard · Init — main from: base run @ 7ff054b (not on bencher)
| constant | shards (main) | shards (PR) | Δ% | pred-floor-ram (main) | pred-floor-ram (PR) | Δ% | union-bytes (main) | union-bytes (PR) | Δ% | heavy-execute-time (main) | heavy-execute-time (PR) | Δ% | heavy-peak-ram (main) | heavy-peak-ram (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Init |
n/a | 59 | n/a | n/a | 175 | n/a | n/a | 342,213,592 | n/a | n/a | 19.089 | n/a | n/a | 13,951,025,152 | n/a |
Init/shard-11 |
n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a |
Init/shard-23 |
n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a |
Init/shard-24 |
n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a |
Init/shard-40 |
n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a |
5 constants · 0 with regressions · 0 with improvements (|Δ| > 3.0% on any metric).
aiur-shard · InitStd — main from: base run @ 7ff054b (not on bencher)
| constant | shards (main) | shards (PR) | Δ% | pred-floor-ram (main) | pred-floor-ram (PR) | Δ% | union-bytes (main) | union-bytes (PR) | Δ% | heavy-execute-time (main) | heavy-execute-time (PR) | Δ% | heavy-peak-ram (main) | heavy-peak-ram (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
InitStd |
n/a | 118 | n/a | n/a | 175 | n/a | n/a | 699,270,546 | n/a | n/a | 25.316 | n/a | n/a | 15,259,164,672 | n/a |
InitStd/shard-12 |
n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a |
InitStd/shard-74 |
n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a |
InitStd/shard-94 |
n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a |
InitStd/shard-96 |
n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a |
5 constants · 0 with regressions · 0 with improvements (|Δ| > 3.0% on any metric).
aiur-shard · Lean — main from: base run @ 7ff054b (not on bencher)
| constant | shards (main) | shards (PR) | Δ% | pred-floor-ram (main) | pred-floor-ram (PR) | Δ% | union-bytes (main) | union-bytes (PR) | Δ% | heavy-execute-time (main) | heavy-execute-time (PR) | Δ% | heavy-peak-ram (main) | heavy-peak-ram (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Lean |
n/a | 174 | n/a | n/a | 175 | n/a | n/a | 1,047,229,426 | n/a | n/a | 26.614 | n/a | n/a | 16,163,889,152 | n/a |
Lean/shard-126 |
n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a |
Lean/shard-22 |
n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a |
Lean/shard-40 |
n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a |
Lean/shard-62 |
n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a |
Lean/shard-82 |
n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a |
6 constants · 0 with regressions · 0 with improvements (|Δ| > 3.0% on any metric).
aiur-shard · Mathlib — main from: base run @ 7ff054b (not on bencher)
| constant | shards (main) | shards (PR) | Δ% | pred-floor-ram (main) | pred-floor-ram (PR) | Δ% | union-bytes (main) | union-bytes (PR) | Δ% | heavy-execute-time (main) | heavy-execute-time (PR) | Δ% | heavy-peak-ram (main) | heavy-peak-ram (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Mathlib |
n/a | 2,668 | n/a | n/a | 357.900 | n/a | n/a | 14,652,331,887 | n/a | n/a | 105.570 | n/a | n/a | 16,036,937,728 | n/a |
Mathlib/shard-142 |
n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a |
Mathlib/shard-1818 |
n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a |
Mathlib/shard-895 |
n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a |
4 constants · 0 with regressions · 0 with improvements (|Δ| > 3.0% on any metric).
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.
Measured-ingress sharding for Aiur checking and proving
What this does
Until now, each shard shipped the full transitive dependency closure of its constants: everything reachable by following references, and the references of those, and so on. That closure is a huge over-approximation, because reachable is not read. The kernel always needs a referenced constant's type, but it only opens a constant's body when definitional equality actually forces an unfold — and most of a closure is only reachable through bodies that are never opened. Example: checking a theorem references lemmas; each lemma's proof mentions thousands more constants; the kernel checks the theorem without ever looking inside those proofs — it only needs the lemmas' statements. In practice the kernel reads a small portion of the closure, but the closure was what every shard carried.
This PR improves performance by making
ix profilerun the out-of-circuit Rust kernel over the whole env, and for each typechecked constant it records the set of constants the kernel actually consulted during that check — read a type, or unfolded a body. This "touch graph" is stored in the.ixproffile for use by the Aiur shard planner. The planner then gives each shard the full bytes of exactly the constants its checks consulted, plus small type-only stubs for everything referenced but never consulted. Soundness never rests on the measurement: if a shard turns out to need something the recording missed, its check fails closed, naming the missing constant — and the repair driver ships that one constant and retries.Performance win
Same 250 GiB per-shard budget, before → after:
* sequential on one 256 GB box: the packer's per-shard prove predictions, calibrated by the ~1.5× ratio observed on measured shard proves.
† Mathlib needs a >365 GiB box for its one oversized block anyway, and the batch prover parallelizes across shards with
--jobsgiven the RAM.All 60 Init shards check green and spot-checked shards prove and verify on a 256 GB box (heaviest measured 189 GiB, ~2 min per shard). Cost: the kernel hooks add +0.32% mean / +0.47% max FFT to ordinary per-constant checking.
Major pieces
ix profile,.ixprofv4) — zero cost outside profiling; the guest kernels are unaffected. The summary now prints per-metric leaderboards (--top N: heaviest blocks by heartbeats, substitutions, ingress bytes, and predicted cost, priced by--backend aiur/zisk/all), andix profile sweeppredicts the full-closure cost of every named constant in the env.ix check --repair) — the Aiur kernel replays slightly differently than the recording kernel, so a few shards need more than they measured. The kernel now names the constant it is missing, and the driver escalates exactly that block. Init converges 60/60 green with no RAM growth.ix prove --ixe E.ixe --ixes M.ixes) — one setup shared across all shards, heaviest first, resumable: a proof is recorded (in~/.ix/cache/shard-proofs/, keyed by claim digest) only after it verifies and binds to the shard's reconstructed claim.aiur-shardbenchmark backend — tracks predicted shards, ingress bytes, and real execution time/RAM of the heaviest shards per env in bencher; Init added as a registry env.!benchmark aiur-shardworks per-PR.ixvmsuite (~15 s).Reproduce
The E2E test runs in
lake test -- ixvm --ignored(also in PR CI).