Uh oh!
There was an error while loading. Please reload this page.
Aggregate-first recursion: lift shard proofs, fold CheckEnv claims, and verify one root - #598
Aggregate-first recursion: lift shard proofs, fold CheckEnv claims, and verify one root#598johnchandlerburnham wants to merge 24 commits into
CheckEnv claims, and verify one root#598Conversation
Add the deterministic lift/flat/structural activation matrix and keep dummy calls deferred. Split aggregate recursion commitment/FRI configuration from IxVM defaults, share it between proving and verification, and pin the future cache encoding without changing active protocol parameters.
Precompute versioned per-slot cache keys, persist lift and join wrappers in the content-addressed store, and reuse entries only after exact claim and native outer-proof verification. Add safe proof decoding, corruption recovery, and --no-cache.
Execute ready lift and join slots as a dependency DAG under explicit job and RAM admission. Add calibration-pending slot weights, failure draining, CLI controls, and serial/parallel scheduler and proof-equivalence gates.
Add an opt-in two-child benchmark that proves singleton CheckEnv shards, lifts both proofs, and measures a verified flat join. Wire join metrics through reporting and dashboards, and record the current pre-E2 lift-size baseline.
- rust-toolchain.toml channel: 1.92 → 1.98, with the matching fenix toolchain hash in flake.nix. The pinned fenix already carries the 1.98 release manifest, so flake.lock needs no change (fenix's nixpkgs stays pinned via its lean4-nix follows, so the Lean toolchain is untouched). - Drop clippy::from_iter_instead_of_collect from the workspace lints: removed in clippy 1.98 and now warns as unknown. - Fix the warnings new clippy 1.98 lints surface across the workspace: chunks_exact(N) → as_chunks::<N>() where the chunk size is constant, descending sort_by → sort_by_key(Reverse(..)), iteration over map values via .values(), map().unwrap_or() → map_or(), a checked division, an unwrap-after-is_some restructured into if-let, and assorted redundant-reference/pattern cleanups (mostly cargo clippy --fix). The two byte-gadget files keep their chunks_exact warnings until the next commit, which rewrites those regions anyway. CI derives its Rust version from rust-toolchain.toml, so no workflow changes are needed.
Companion to multi-stark's update-p3 branch (c72d321 → 249b740), which carries four soundness/robustness fixes and the Plonky3 v0.6.0 bump (pruned FRI Merkle multiproofs: ~2x faster verification, 40-70% smaller proofs; canonical Goldilocks serde removes proof-byte malleability). Proofs and verifying keys are not compatible with the previous pin. Integration: - Lookup gained max_multiplicity, a declared per-row bound on the multiplicity's integer magnitude feeding the newly enforced logUp height bound Σ wᵢ·hᵢ + |claims| < p. Function-circuit slots accumulate mutually-exclusive branch selectors, so they declare 1; committed count columns (function return slots, the memory circuit, the byte gadget tables) declare the new COUNT_COLUMN_BUDGET (2^32 queries per entry). - The VK wire format carries the bound: u64 LE max_multiplicity per lookup, between the multiplicity node id and the arg count. The in-circuit VK deserializer (Ix/MultiStark/SystemDeserialize.lean) parses past it; the value is bound through the vk digest but the height bound itself is not yet enforced in-circuit (the native verifier enforces it). - Message fingerprints are width-bound by default upstream (the slot width seeds the Horner fold), which is incompatible with aiur's branch-shared lookup slots: mutually exclusive branches superpose messages of different natural widths into one slot at the maximum width, so a narrow call is sent zero-padded to a width its callee's return slot never provides, and proving fails with UnbalancedChannel (pinned as the prove_verify_mismatched_call_widths regression). Aiur instead declares WidthBinding::ByConstruction — the plain Horner fold, restoring zero-padding transparency — and takes on the prefix-freeness contract that makes it sound: every message's natural width is a function of its constant-constrained leading prefix (channel tag plus discriminator: fun_idx fixes 2+in+out, the memory size coordinate fixes 3+size, each gadget tag fixes its table width), so zero-extension can only equate a padded message with its own natural form. The contract is documented at the channel constants in lib.rs; the declaration is applied in AiurSystem::build and mirrored in the vk_codec decoder so decoded VKs replay the same transcript. ByConstruction is also exactly the fold the in-circuit verifier's logup_fingerprint already computes, so the recursive verifier needs no fingerprint change. - The policy is Fiat-Shamir-bound as the first observe_shape word; the in-circuit transcript replay prepends the matching limb. - aiur_multi_stark.rs regenerated (ix codegen) for the deserializer and transcript changes. - P3 v0.6.0 ships FRI query openings as pruned Merkle multiproofs, while the in-circuit verifier consumes one authentication path per query (its per-query control flow is a far smaller circuit than the amortized multiproof walk). Rather than porting the walk into the DSL, the proof advice stays in the per-query transport: multi-stark's new advice module re-encodes a natively-verified proof by running p3's own verification with a recording compression function and reading each query's path back out of the recorded digest map. The advice bytes are untrusted verifier input, never digest-bound — the transcript binds the commitments and every expanded sibling is authenticated against them per query — so pruning vs expansion is pure transport and the encoding choice is sound. AiurSystem gains proof_to_advice_bytes (FFI: AiurSystem.proofToAdviceBytes); the recursive-verifier test feeds it instead of Proof.toBytes, whose native wire format is still round-tripped separately. The Lean-side proof grammar and the codegen'd verifier are byte-identical to before — no in-circuit changes. Claim layout, the VK wire format above and aiur's public semantics are otherwise unchanged; the policy adds no prover or verifier work over the previous pin. Still open, native-verifier-only: the logUp height bound is parsed past but not yet enforced in-circuit (a wide-arithmetic check, tracked separately).
The Lean v4.33.1 update pinned both dependencies at revisions that predate their Rust 1.98 bumps; their heads now carry those bumps, which this workspace needs since rust-toolchain.toml moved to 1.98. Both revisions stay on leanprover/lean4:v4.33.1. - Blake3.lean 1b0fbd2 → e6e908b (Rust 1.98, plus a case-insensitive source-directory fix), updated in lakefile.lean, lake-manifest.json and the blake3-lean flake input. The revision keeps the `blake3_rs_shared` target the `ix_native_decide_dynlib` pin requires. The inherited entry in Benchmarks/Compile/lake-manifest.json was still on the pre-4.33.1 revision and now tracks the root pin. - lean-ffi 2a9c91e → 93c7e52 (Rust 1.98). Only bignat reaches the sp1 and zisk workspaces, so their lock files move that one package.
The !benchmark recursive phase reported n/a for every fri-verifier metric: Benchmarks/Typecheck.lean still fed Proof.toBytes — the pruned multiproof wire format — to executeMultiStark/proveMultiStark, so the in-circuit verifier rejected on parse and the harness (correctly) left the recursive fields absent rather than emit a fake datum. The in-circuit verifier consumes the per-query advice transport (AiurSystem.proofToAdviceBytes); proofBytes stays the reported proof-size metric. bench-recursion-debug had the same advice-format gap plus a stale claim recipe: it still built the public input as 32 raw digest bytes, predating the ClaimHarness.packedDigestKey packing bench-typecheck uses (its own out-of-circuit sanity check failed with InvalidPowWitness — a wrong claim diverges every challenge — and the advice re-encoder refused the proof for the same reason). Both aligned with the typecheck flow. Validated end-to-end at production parameters (numQueries 100, query PoW 20, blowup 2) on Nat.add_comm: inner prove, advice re-encoding, and the codegen'd in-circuit verifier accepting.
Keep compact proof bytes at storage and cache boundaries, expand them only for recursive lift/join advice, reject unsupported zero-query benchmarks, and decode legacy store proofs without panicking. Refresh tests, benchmark pins, and Rust 1.98 lint compatibility.
Add Ix/Aggr, a recursive aggregation system for IxVM shard proofs that keeps Ix/MultiStark untouched and Ix-agnostic. One entrypoint, ix_aggr, subsumes lifting and joining: a one-byte advice shape selects wrap or binary join over any mix of IxVM and ix_aggr children, so shard proofs enter the recursion system directly as join children and the dedicated lift stage disappears. Circuit (Ix/Aggr/Circuit.lean): every shape verifies its children in full (verify + ood_verify from the shared Multi-STARK verifier modules) against the vk its hinted kind demands. Identity is one 80-byte digest-bound blob - blake3(ixvm vk) || verify_claim idx || blake3(self vk) || ix_aggr idx - carried unchanged at every node; self children must bind the identical blob digest, pinning both vks and both entrypoint indices transitively. Claims are a uniform 18-word [0, aggr_idx, allowed(8), checkEnv(8)] at every depth, so proofs of different tree levels combine freely. Wrap shapes bind the output digest to the child CheckEnv digest directly; pair shapes open both CheckEnv preimages, re-root the canonical subject/assumption trees, and prove subjects = L ∪ R, assumptions = (asmL ∪ asmR) ∖ subjects with linear sorted merges. Toplevel (Ix/Aggr.lean): ixAggr = MultiStark.multiStarkFull + circuit, pruned to ix_aggr, so verify_multi_stark_proof and other unrelated entries no longer pad aggregate proofs. The host half of the wire contracts (allowed blob, public input packing, shape codes, keyed preimage/tree blob framing, interpreter IO assembly) lives beside the toplevel; Ix/Aggr/Host.lean folds CheckEnvTrees statements. Native path: ix codegen gains the ix-aggr target (crates/ixvm-codegen/src/aiur_ix_aggr.rs, 244 fns); its runner builds the seven-channel IO buffer natively and routes execution through the generated code. New FFI rs_aiur_ix_aggr_execute/_prove (executeIxAggr/proveIxAggr) pass proofs, vks, claims, and the compact count/key/length preimage/tree blobs without per-byte boxing, plus Proof.ofBytesChecked for store-boundary decoding. CLI: ix aggr --ixe E --ixes M <shard-proof>... reconstructs every nonempty shard statement from the env, matches wrappers by claim digest, natively pre-verifies them, folds a balanced bisection (the canonical fold makes the root claim independent of tree shape), wraps single-shard roots so the persisted root is always an ix_aggr proof, checks the root closes over the env canonical tree with no residual assumptions, and persists the wrapper. Tests (lake test -- ix-aggr, 17 cases): all five shapes accept over real Multi-STARK stand-in child proofs from two distinct-vk systems; codegen'd execution matches the interpreter on output and per-circuit query counts for wrap and pair; negatives break one binding each - lying shape hint, tampered proof, foreign identity, wrap statement drift, dropped assumption, padded subject set, and tree advice not reproducing its keyed root.
Replace the legacy lift/join entrypoints with the heterogeneous ix_aggr system across aggregate, verification, cache, and codegen paths. Preserve wrap-first and direct-join policies behind one proof identity and cache namespace. Add the converged 91-check semantic suite and a deterministic 132-case activation audit covering shapes 0 through 9 twice, with no unobserved circuits.
Replace the legacy two-shard three-entrypoint benchmark with a four-shard manifest-subtree harness for production ix_aggr wrap-first and direct policies. Enforce the q=100 serialized no-cache profile, natively verify every input and recursive output, persist ordinary aggregate wrappers, and emit resumable per-slot JSON metrics. Port bench-typecheck --join to ix_aggr direct shape 2 while preserving the stable join metric schema. Remove the final legacy slot-spec/preimage shim and pin both M1-f four-shard plans in the focused suite.
Update the multi-stark dependency and Rust toolchain for Plonky3 0.6, along with the Rust 1.98 lint migrations required to keep the workspace warning-free. Refresh the Rust-compatible Blake3.lean pin in both root and compile-package manifests. Adapt recursive Aiur verification to Plonky3's pruned FRI multiproofs. Native proofs retain their compact serialized representation and native verification path; the FFI expands authenticated Merkle frontiers into per-query advice only when entering the existing recursive verifier circuit. Preserve the packed claim-digest convention in the recursion diagnostic and exercise the advice boundary in the end-to-end test and benchmark paths. CPU and CUDA recursive q1 runs produce identical 823,485-byte inner proofs and 331,273-byte outer proofs. The q50 Vector.extract_append workload retains identical CPU/CUDA proof sizes. Inner plus outer STARK proving measures 65.87s on CPU and 8.81s with CUDA on the RTX PRO 6000, a 7.48x speedup.
PR benchmark runs execute trusted workflow YAML from the default branch while loading composite actions from the PR checkout. When Bencher data and binary caches are unavailable, the workflow checks out main under base/ and asks Lake to rebuild it without first installing the Rust channel pinned by that checkout. Teach the existing CPU provenance action to install the base checkout's validated Rust channel and profile immediately before an uncached base build. The step is a no-op when the toolchain is already available and leaves cached benchmark comparisons unchanged.
Consume the Plonky3 0.6 batch-opening layout directly in Aiur instead of expanding every pruned Merkle frontier into one authentication path per FRI query. Sample all query indices from the unchanged transcript, sort and deduplicate them with an O(q log q) merge sort, authenticate each input and commit-phase commitment once, then retain the existing per-query reduced-opening and FRI arithmetic. Bind every frontier to transcript-derived indices, consume boundary digests in Plonky3's level/parent/child order, reject trailing frontier elements and inconsistent duplicate leaves, and assert all native opening dimensions and sibling counts. Explicitly constrain the digest-bound protocol specialization to cap height 0, binary FRI, and a constant final polynomial. Move memo_u32_less_than into IxVM Core so both substitution and multiproof sorting share its constrained rows. Strengthen the recursive negative test to mutate a structurally valid stage-1 commitment. Regenerate both checked-in Aiur Rust executors and retain interpreter/codegen query-count parity. On Vector.extract_append q50, recursive-verifier FFT cost falls from 204.073B to 201.166B. CPU outer proving improves from 50.09s to 45.03s and the full CPU pipeline from 90.64s to 82.90s. GPU outer proving improves from 15.85s to 13.72s and the full GPU pipeline from 28.86s to 26.69s. The outer proof grows from 3.92 MB to 4.17 MB. Validated with the MultiStark primitive suite, recursive honest/tamper/parity tests, codegen --check, release workspace clippy, release CUDA clippy, rustfmt, and diff checks.
johnchandlerburnham
commented
Sep 1, 2026
Init full proving reportRevision: Compilation and sharding
The 1.876-second compile measurement is the Ix compiler itself; it excludes the initial one-time dependency download and Lake build. Stage 1: base shard proofsAll 16 shard proofs were persisted and individually verified against their corresponding manifest claims.
Two-way concurrency gave a 1.53× wall-time speedup despite increasing total prover-seconds by about 33% from CPU/memory contention. Stage 2: recursive aggregationPolicy:
Plan:
Results:
Final proofRoot address:
Final claim:
Both validations passed:
End-to-end measured timeUsing the two-way Stage 1 run:
This total excludes the one-time dependency build/download and a few seconds of manifest and final-root verification overhead. Using serial Stage 1 instead would make the measured core pipeline approximately 1h 09m 28.35s. |
Use the PR77 lean-ffi and multi-stark pins, remove the stale width-binding and multiplicity-bound protocol fields, and regenerate the recursive and aggregate verifier sources.
Expose an opt-in x86_64-linux cuda shell with NVCC 13.2, sm_120 code generation, and safe host libcuda discovery while leaving the default development shell unchanged.
Summary
This PR implements the aggregate-first path for Aiur Multi-STARK proofs. The
production path now runs through one
ix_aggrrecursion entrypoint: it wrapsindependently-proven IxVM shards, folds their
CheckEnvstatements along themanifest's bisection tree, and persists one recursive root proof with a
uniform 18-word outer claim. Every completed recursive slot is persisted in a
verified, content-addressed version-2 resume cache, and ready slots are proven
in parallel under explicit job and RAM limits.
The entrypoint has two pair-fold modes:
small lower nodes.
nodeHash(leftRoot, rightRoot)in one hash anddischarge assumptions with Merkle inclusion paths. Their subject work is
independent of subtree size, avoiding the top-of-tree re-rooting blowup.
The CLI selects the modes monotonically with
--structural-above N(default4096 subject leaves): flat below the threshold, structural above it.
A manifest with one retained (nonempty) shard is also a valid deliverable: its
root is one shape-0 wrapper, with no self-join padding (including under
--direct-joins). Zero-constant manifest leaves are pruned after raw coveragevalidation:
This is the stage-2 aggregation layer from
plans/aggregate-first-pipeline.md: shard proofs are aggregated before anyterminal KZG/SP1 compression, so a later wrapper only needs to consume one root
proof. Terminal compression remains outside this PR.
Section 14 implementation is complete through M1-f in this branch. The
ap/ix-aggrsingle-entrypoint base is reconciled with WP-E2's compact storedproof / expanded recursive-advice boundary, and its one
ix_aggrentrypointsupports wraps, flat pairs, and structural pairs across both IxVM and recursive
children.
ix aggregatenow uses that backend for planning, proving, cacheresume, and final verification;
ix verify --aggregatederives one uniformouter claim and performs value-based environment/manifest checks. The old
ix aggrcommand and all three-entrypoint production wiring are retired. Theolder Multi-STARK aggregate implementation remains as an Ix-agnostic regression
surface, not as a CLI backend. Production semantics, activation coverage, and
benchmarking now live entirely against
ix_aggr. M1-f lands the pinnedfour-shard
bench-aggregate-policyhandoff and ports the stable typecheck joinmetric to direct shape 2; only execution of the policy comparison on the large
box remains. Operationally this is one future handoff: Arthur will check out
b70042d6d1a029bb8e1d541da7aef5e0613d67e6once, run the inherited M1-ecorrectness suite as untimed preflight, and then benchmark both policies. There
is no separate M1-e box run.
Measured performance (2026-08-29)
Arthur Paulino ran the pre-convergence pipeline end-to-end on four real Init
shard proofs (shards 8–11 of a 16-way partition, 12,493 constants; base shard
proving excluded; native verification of each output included; ~512 GB box).
These are the standing M1-f comparison baseline; the converged wrap-first and
direct policies have not yet been rerun on that box. The recursion used the
conservative q=100 / PoW 20 defaults this PR keeps:
Notes: lift cost is shard-content-independent (four lifts within ±2%, tracking
the ~constant 20–23 MB shard-proof shape); the measured lift peak brackets the
scheduler's 195 GiB weight placeholder exactly; and an unserialized run of all
four lifts OOM'd at ~492 GiB — precisely the behavior the WP-B admission gate
prevents (on a 512 GB box its weights admit two lifts). Because shards 8–11
are a strict partition subset, the root carries a real frontier assumption
set, so the joins exercised genuine discharge work. Full analysis, including
the comparison against direct (unlifted) IxVM joins, is in
plans/aggregate-first-pipeline.md§3.4 and the Zulip thread.What lands
Protocol / circuit layer:
ix_aggr, under one verifying key.Shapes 0–1 wrap one IxVM/recursive child, shapes 2–5 fold flat pairs, and
shapes 6–9 fold structural pairs for every child-kind combination.
transitive verifying-key, function-index, and allowed-system binding. A
shape hint selects the verified form but cannot weaken its checks.
CheckEnvdecoding and canonical flat set folding.keeping output assumption sets canonical and deduplicated.
digests and their two accepted entrypoint indices; every recursive node has
the same 18-word outer-claim layout regardless of shape.
nodeHash(leftRoot, rightRoot)and account for eachunique assumption candidate through a strict Merkle-path-or-carry choice.
6 carries both the one-byte shape at key
[0]and candidate path payloads atraw 32-byte address keys; the key shapes are disjoint.
framing is decoded strictly before the circuit independently validates
payload semantics.
ix_aggrexecutor is regenerated at 2,061,361 bytes / 248Aiur functions and parity-tested against the interpreter.
Host driver and operations:
.ixesaggregation-tree parsing and post-order lowering, with abalanced fallback for legacy manifests; validate-then-prune removal of
zero-constant leaves with unary tree contraction (and a Rust writer that
stops emitting them).
shape-0
ix_aggrwrapper, including under--direct-joins.--structural-above, with adefault wrap-first plan (shapes 0 then 5/9) and an explicit
--direct-joinsplan that derives heterogeneous shapes from actual childkinds.
binds the uniform outer claim, and reuse occurs only after content-digest,
claim, decode, and native verification all pass;
--no-cachebypasses.--jobsand
--max-ram(default 92% of MemTotal), heaviest-first, with failuredraining (WP-B). Admission weights are shape-aware: 4 GiB for a retained
raw IxVM leaf, 195 GiB for wraps/self pairs, 390 GiB for IxVM/IxVM pairs,
and 340 GiB for mixed pairs.
explicit
RecursionParametersvalue, defaulting to today's q=100 values;the q=50+PoW policy decision is deliberately deferred.
two controlled child trace heights, both wraps, every flat/structural
child-kind pair, optional assumptions per side, and discharge/carry. The
complete matrix runs twice with a stable signature and observes every
catalogued circuit; dummy-call padding remains intentionally deferred.
with a one-pass multi-root witness closure for proving.
ix aggregate --ixe E --ixes M [--structural-above N] [--direct-joins] [--jobs N] [--max-ram G] [--no-cache] [--plan-only] <proof>...andsingle-entrypoint aggregate verification with cryptographic-only,
environment-bound, and manifest-bound value checks. The duplicate
ix aggrcommand is removed.a flat-join bench (singleton
CheckEnvshards → two lifts → verified flatjoin), with join metrics wired into reporting/dashboards, the pre-E2 lift
proof size pinned at 7,986,166 bytes, and the post-E2 delta measured.
malformed-input, and semantic-tampering tests: the
aggregate-firstsuitehas 58 cases, plus the separate activation matrix.
Protocol design
One recursion system, one entrypoint
Production builds
Aggr.ixAggr, the shared Multi-STARK verifier closure prunedto one
ix_aggrentrypoint. A one-byte advice hint selects the exact verifiedshape:
ix_aggrix_aggrpair (2 + 2·left + right)ix_aggrpair (6 + 2·left + right)The hint is advice, not authority: each arm verifies the child proof(s) under
the key required by the encoded child kinds, then requires that kind's exact
claim layout. A wrong shape therefore fails proof verification, function-index
binding, or claim decoding.
Uniform public statement and pinned protocol identity
Every wrap and pair exposes the same public-input shape:
Each value is a 32-byte Blake3 digest packed injectively into eight
little-endian four-byte Goldilocks values. The 16-element public input commits
to:
CheckEnvclaim.The allowed blob is:
The circuit requires exactly 80 bytes. The entrypoint indices must be explicit
because Source DSL programs cannot materialize their compiler-assigned
function indices. Binding the verifying keys alone would permit a claim about
another function in those systems; binding the two accepted indices pins the
complete recursive protocol identity.
The host and root verifier independently compile both systems and reconstruct
this blob. No identity is accepted from the persisted proof wrapper on trust.
Every persisted aggregate outer claim is consequently the same 18-word form:
the
ix_aggrfunction selector followed by the packed identity and outputclaim digests. Shapes are witness choices and do not become root-kind metadata.
Child-proof validation and transitive pinning
Each pair reads the verifying key required by each child kind, checks its
Blake3 digest against the allowed blob, and deserializes it strictly. Wraps do
the same for their one child. For every child the selected arm:
ood_verify, including Fiat-Shamir replay, lookup accumulators,quotient/OOD checks, Merkle openings, and FRI verification; and
index.
The accepted forms are:
blake3(ixvm_vk). Its claimsdigest opens to exactly one 10-word IxVM claim at the pinned
verify_claim_idx, whose digest opens to a strict serializedCheckEnvclaim.
ix_aggrchild: its 18-word claim must use the pinnedix_aggr_idx; itsfirst public digest must equal the current
allowed_digest, transitivelypinning both systems and both entrypoints; and its second digest opens to its
output
CheckEnvclaim.Any other index, shape, digest, trailing byte, or failed proof check rejects.
This keeps wrap→pair, flat→pair, and structural→structural composition on one
statement format.
Flat canonical folding
For child statements
(S_L, A_L)and(S_R, A_R), flat shapes 2–5 enforce:Every present tree is strictly parsed and fully consumed. Its real leaves must
be nonempty and strictly byte-lexicographically increasing, simultaneously
enforcing sorting and deduplication. The circuit recomputes the canonical
Blake3 Merkle root, including zero-address padding for odd levels, then checks
the union and difference equations with linear sorted merges.
Address order is constrained over eight big-endian
u32words using thefull-domain
u32_less_thanprimitive. The implementation never uses Aiurpointer identity as address equality: distinct pointers imply distinct
allocations, not distinct stored byte strings.
A flat parent does not trust a structural child's opaque root. It can consume
that child only if advice opens the root as a valid canonical sorted tree. A
genuinely free-form structural root therefore rejects. In the harmless
shape-coincident case where a structural root also has a canonical opening,
the circuit proves that opening rather than relying on its provenance. The
monotone host scheduler avoids needing such openings in normal operation.
Structural root and assumption discharge
Structural shapes 6–9 perform the same allowed-blob binding, child-key
binding, two child-proof verifications, child decoding, and output-claim
binding as the flat shapes. They replace all subject-tree loading and set
re-rooting with:
Input and output assumption trees remain canonical because they represent a
small sorted frontier. The circuit walks the sorted, deduplicated union of the
two input assumption lists. For every candidate, channel 6 supplies exactly
one choice:
0): no bytes may follow, and the candidate must be the nextvalue in the output assumption list; or
1): a bounded Merkle path fromleafHash(candidate)toS_out.rootmust verify.Path payloads are strict:
countis limited to 64.side = 0hashesnodeHash(sibling, current)andside = 1hashesnodeHash(current, sibling); any other side rejects. Thepayload must be fully consumed and the folded root must equal the output root.
The candidate walk prevents dropping an assumption without proving discharge,
and it requires the output list to be exhausted, preventing extra assumptions.
Survivors do not need non-membership proofs: carrying a candidate that is also
present in subjects only weakens the statement and prevents the desired
unconditional root. Duplicate subject leaves in a structural forest are also
safe because discharge needs only one valid membership path.
Advice and FFI contract
All
ix_aggrshapes use the same seven-channel IO layout. Digest/root bindingsare checked before the corresponding bytes are decoded.
[0],[1][kind]0= IxVM,1=ix_aggr)[0],[1],[2]CheckEnvclaim[0][0]/ raw candidate addressLean passes channels 4–6 across FFI as compact framed blobs:
The Rust decoder borrows payloads rather than cloning them. It rejects
truncation, offset overflow, impossible entry counts before allocation,
declared-length overruns, and trailing bytes before circuit execution.
Wraps receive no tree or path advice. Flat pairs receive full
subject/assumption tree advice and an empty path blob. Structural pairs receive
only the input/output assumption trees plus one path choice for every
deduplicated candidate; subject trees are never opened.
Manifest and host pipeline
.ixesaggregation treeparseIxesManifestexposes both shard block lists and the optional binaryaggregation tree stored at the manifest tail. It:
tree tail or with an explicit absent-tree tag.
The tree lowers to post-order
FoldOpslots. Every join refers only to earlierslots and the last slot is the root, providing a direct serial schedule and the
basis for cache keys and parallel execution.
Validate first, then prune empty manifest leaves
IxesManifestViewretains the original shard id for every dense shard slot.pruneEmpty:The aggregate and manifest-aware verifier paths deliberately call
shardsCoveron the raw manifest before this transformation. Coveragestill establishes that every environment constant is owned exactly once. The
subsequent zero count is therefore evidence that a removed leaf contributes no
subject; pruning is not allowed to hide a missing or duplicated constant.
Original shard ids are preserved separately from dense scheduling ids, so CLI
plans and proof-binding errors continue to identify the source manifest shard.
An all-empty manifest is rejected because it cannot produce a root.
For a tree node
node(left, right), pruning follows:The Rust
.ixeswriter (crates/kernel/src/shard.rs) also normalizes newmanifests before serialization — block-empty shard records are omitted, ids
rewritten densely, the tree pruned/contracted/remapped, and cross-ingress
recomputed. The Lean-side pass remains necessary for legacy manifests and for
the stronger environment-relative condition (a shard may contain blocks yet
own zero constants).
Monotone structural scheduling
The host counts actual owned constants for each shard after the disjoint-cover
check.
schedulePlanannotates every slot with its cumulative subject count andchooses a structural pair exactly when:
The default threshold is 4096;
--structural-above 0makes every joinstructural for testing. Nonempty children make counts strictly increase toward
the root, so once a structural node appears, all ancestors are structural.
This prevents a flat parent from needing to open a free-form structural child.
By default, every leaf is an
ix_aggrshape-0 wrap, so binary slots are shape5 below the threshold and shape 9 above it. With
--direct-joins, amulti-shard plan keeps leaves as raw IxVM children and derives each pair shape
from its actual child kinds: 2–5 for flat pairs or 6–9 for structural pairs.
The monotone threshold rule is unchanged.
The proving loop checks reconstructed subject counts against the schedule
before starting expensive work.
Singleton roots
ix aggregateimposes no two-shard minimum. The fold plan for one retainedleaf contains one shape-0 wrap and zero pairs; that wrapper and its
CheckEnvclaim are persisted as the aggregate root. Even
--direct-joinswraps asingleton because the deliverable must verify under the one production
entrypoint. A self-pair would add work and manufacture a different statement.
Consequences:
--plan-onlyreports one wrap and zero binary pairs for a singleton;ix_aggrroot.ix aggregateThe command:
shard cover on the raw manifest, then prunes zero-constant leaves;
CheckEnvclaim and canonicaltrees (claim-only preparation — no dependency-byte closure);
then requires exact claim equality and one proof per nonempty shard;
ix_aggrrecursion systems and the pinned 80-byteallowed blob;
version-2 cache key up front;
DAG, resuming verified cached slots and persisting each completed wrapper
(raw direct-policy leaves are verified inputs, not cache slots);
reproduce the environment's canonical root;
the one
ix_aggrroot entrypoint; andIxon.Proofcontaining the outputCheckEnvclaim and proof.--plan-onlystops after coverage validation and scheduling, resolving andprinting the scheduler policy without loading proofs or compiling recursion
systems:
ix verify --aggregateAggregate roots reuse
Ixon.Proof, so verification is selected explicitly.The verifier never accepts root-kind metadata. It serializes the bundled
CheckEnvvalue and reconstructs the only valid outer claim:ix verify --aggregate <proof>ix_aggrix verify --aggregate --ixe E <proof>ix_aggrix verify --aggregate --ixe E --ixes M <proof>ix_aggrEnvironment-only mode compares the bundled value to the canonical environment
root; a manifest-relative structural value therefore rejects naturally, with
no root-kind branch. Manifest-aware verification repeats pruning and the fold
schedule (the threshold must match the proving run), reconstructs every leaf
statement, folds the exact hybrid value, requires no assumptions, and verifies
the same
ix_aggrouter claim. Existing non-aggregate proof andshard-composition verification paths are unchanged.
Claim-only shard preparation
shardCheckEnvClaimTreesconstructs only theCheckEnvclaim and itscanonical subject/assumption trees. Aggregate planning, shard-digest
reconstruction, and aggregate verification use this path because none of them
consumes dependency bytes.
shardCheckEnvClaimremains the witness-buildingentry point; it reuses the same claim/tree result and computes the byte
closure once from the union of the owned and available primitive roots.
Reachability distributes over that root union, so this preserves the old
closure while avoiding repeated traversal of shared subgraphs.
Recursion parameters (WP-E1)
Aggregation and aggregate verification consume one shared
MultiStark.RecursionParametersvalue containing the recursion commitment andFRI configurations, carried through
runAggregateCmdWith/runVerifyCmdWithinto the shared
MultiStark.buildRecursionSystem. The CLI entrypoints passdefaultRecursionParameters, whose fields are exactly today's canonical Aiurdefaults. This is a mechanism split, not a policy change:
configuration;
follow-up decision.
The recursion verifying key serializes and binds both parameter sets, and its
digest is included in every aggregate node's allowed-system blob, so any parameter
change changes the recursive protocol identity without a public-input or
allowed-blob format change.
RecursionParameters.cacheFriBytespins the40-byte
fri_params_sercache-key component:Commitment parameters need no second cache component: changing them changes
the recursion-vk digest already present in the key.
Pruned FRI multiproofs (WP-E2)
The four-commit
origin/update-multi-starkseries is transplanted onto thisstack: Rust 1.98, the
249b7405multi-stark revision on P3 v0.6, the matchingBlake3/Lean-FFI pins, and recursive proof-advice encoding. The new proof wire
format deduplicates shared Merkle siblings across sampled FRI queries. Width
and trace-height binding and the vk's checked
max_multiplicitytravel withthe dependency update; no aggregate claim or public-input format changes.
There are now deliberately two proof encodings.
Proof.toBytesis the compactwire form used by wrappers, native verification, the store, and WP-A cache
entries. Recursive execution still expects one path per query, so callers use
AiurSystem.proofToAdviceBytesimmediately before a wrap or pair. The CLI,pair/typecheck benchmarks, semantic tests, and activation audit all enforce
that boundary. Cached proofs stay compact at rest and are expanded only when
consumed as a parent pair's child.
The dependency's compact format is not backward-decodable. Store-facing CLI
verification therefore uses
Proof.ofBytesCheckedand reports a normal errorfor legacy or corrupt proofs instead of crossing the unchecked decoder and
aborting. P3 v0.6 also requires a positive FRI query count; benchmark CLIs
reject
--queries 0, and the old q=0 join smoke gate is replaced by q=1.The Rust 1.98 migration also applies its new strict-Clippy equivalents for
fixed-size digest chunking and fallible metadata-size lookup; these are
mechanical, semantics-preserving rewrites.
Verified cache and resume (WP-A)
Before the first proof, the driver derives every fold slot's
CheckEnvstatement, exact outer Aiur claim, and cache key, using the same
flat/structural fold policy as proving — so a manifest rebudget or statement
change invalidates only the changed subtree. The key:
The uniform outer claim already includes the
ix_aggrentrypoint index andpublic input, hence the allowed-system blob, output
CheckEnv, bothverifying-key identities, and both accepted entrypoint indices. Each completed
recursive slot is stored as an
Ixon.Proofwrapper in the content-addressed~/.ix/store; a raw--direct-joinsleaf is only an input and is not cached.The wipeable index
~/.ix/cache/aggregate/<key>holds only the wrapper's storeaddress and is updated via temp-file + atomic rename. M1-d bumps
aggregateCacheVersionfrom 1 to 2, so old outer-claim entries miss cleanly.A hit is an untrusted hint, not authority. Reuse requires all of: a
well-formed index address; store bytes whose Blake3 digest equals it; a
decodable wrapper; a bundled claim exactly equal to the precomputed slot
CheckEnv; a safely decoded Aiur proof (Aiur.Proof.ofBytesChecked— theformer trusted-byte constructor panicked on truncated bincode, and malformed
cache bytes must never abort the command); and native verification under the
exact precomputed outer claim and local recursion system. Any failure logs a
miss and re-proves. Cache write failures are warnings. On a valid hit the
host reconstructs the slot's preimages from the manifest statement, so
parents need no trusted metadata from the cache.
--no-cachebypasses indexreads and intermediate writes while still persisting the final root wrapper.
RAM-gated parallel scheduling (WP-B)
The post-order fold executes as a dependency DAG: leaves are ready
immediately; a join becomes ready when both child slots have completed. The
controller sorts ready work by descending RAM weight (slot number breaks
ties) and starts one dedicated
IO.asTaskper admitted slot around theexisting proof FFI. Two independent limits govern admission:
--jobs Ncaps active slots; absent or0means every ready slot may runif it fits the budget;
--max-ram Gcaps total reserved GiB in flight, defaulting to 92% of LinuxMemTotal.As in the existing Rust
RamGate, a slot whose estimate exceeds the entirebudget is admitted only while nothing else runs — a conservative estimate
serializes work rather than deadlocking. The calibration-pending per-shape
weights are:
The 195 GiB wrap reserve carries forward the recorded q=100 lift upper bound —
the measured peaks above (186.8–195.8 GiB) bracket it exactly. The 390/340 GiB
direct and mixed estimates deliberately keep the non-default policy out of the
256 GiB fleet tier pending M1-f calibration; measured self-pair peaks
(102.5–156.9 GiB) make their weights conservative in the safe direction. Real
calibration on a known-core box will tighten them without changing scheduler
semantics.
Results are installed by slot index, never arrival order; each worker gets an
immutable snapshot of its completed children, so parallel timing cannot
change parent advice. On failure the controller stops admitting, drains every
running proof, and reports the lowest failed slot; successful independent
tasks may finish publishing valid cache entries. Concurrent proofs share
Aiur's rayon global pool, so throughput can sub-scale even when memory
permits multiple slots; process-per-slot execution is a measurement-driven
follow-up.
Converged activation audit (WP-D + M1-e)
lake exe IxTests aggregate-activationis a dedicated diagnostic kept out ofthe default suite. It executes the generated production
ix_aggrpath across4 wraps and 128 pairs: two controlled child trace heights, shapes 0–9,
optional assumptions independently per side, complete discharge versus
explicit carry, and all four child-kind combinations in both flat and
structural modes. Every execution returns per-circuit
(uniqueRows, totalHits); the runner performs the full 132-case matrix twice and rejects anydifference before rendering a deterministic per-shape Markdown report.
Current signature:
Result: 183 audited circuits — 154 active in every case, 29 input-dependent,
zero never observed. The variable set concentrates in the expected paths:
wrap dispatch, canonical set folding, structural Merkle discharge, and
child-kind decoding. Fixed-height
Bytes1/Bytes2circuits areoutside the execute FFI's query-count array and are called out explicitly.
The audit records information only; dummy calls would add cost for the
currently planned SP1 terminal and should be chosen only if a future static
terminal requires input-independent activation.
Native execution, proving, and generated code
Large advice values remain raw byte blobs across the Lean/Rust boundary. This
PR adds or extends:
Bytecode.Toplevel.executeMultiStarkJoinfor generated or interpreted flatand structural join execution;
AiurSystem.proveMultiStarkJoinfor witness generation and proving;JoinAdvice,JoinPreimage,JoinTree,JoinPath, strict framed decoders,and the seven-channel
join_io_buffer;rs_aiur_multi_stark_join_executeandrs_aiur_multi_stark_join_proveexterns; andAiur.Proof.ofBytesCheckedfor panic-free store-boundary proof decoding.The retained three-entrypoint executor is parity-checked against the bytecode
interpreter on both output and every circuit's unique-row/total-hit counts. The
combined verifier contains 247 Aiur functions; the regenerated Rust file is
2,239,894 bytes (
ixvm: 5,807,375 bytes / 780 functions). Most line churn isgenerated code. The protocol source of truth is
Ix/MultiStark/Aggregate.lean; the native advice contract lives inaiur_multi_stark_runner.rs. It is now an Ix-agnostic regression/reference backend,not the production CLI backend.
The production
ix_aggrexecutor is independently parity-checked for wrap,flat, and structural shapes. It contains 248 Aiur functions and its generated
Rust file is 2,061,361 bytes. Its source of truth is
Ix/Aggr/Circuit.lean, with native advice construction inaiur_ix_aggr_runner.rs; all three generated artifacts are checked withix codegen --check.Benchmarks
M1-f replaces the legacy two-shard/three-entrypoint runner with
bench-aggregate-policy, a productionix_aggrbenchmark for one exactfour-shard fixture. It selects the four retained leaves from a validated and
pruned manifest, contracts the surrounding tree without changing orientation,
and independently reconstructs the expected host root. Wrap-first uses shape 0
leaves; direct mode keeps IxVM leaves raw. Both policies then select their flat
or structural heterogeneous shapes from the production plan. Measured runs
require q=100, jobs=1,
--no-cache, and JSON output; the harness nativelyverifies all four inputs and every recursive output, persists every completed
slot as an ordinary
Ixon.Proof, and writes resumable per-slot and whole-runtiming/RSS/proof metadata.
The existing
bench-typecheck --recursive --joinrow keeps its stablejoin-*reporting/dashboard schema, but its join phase now exercises directix_aggrshape 2 instead of the retiredjoin_twocircuit. Historical sizebaselines remain recorded: 7,986,166 bytes (7,986,204 with the
Ixon.Proofwrapper) for a one-constant q=100 lift under the pre-E2 247-function system,
versus 7,443,023 bytes (7,443,061-byte wrapper) after WP-E2, a 543,143-byte /
6.80% reduction. Pruned multiproof length depends on sampled query-path
overlap, so a positive-PoW output is now a sample rather than an exact
byte-length pin. The deterministic q=100/PoW-0 regression signal is 7,447,279
bytes and 38,850,942,825 recursive-verifier FFT cost. The target-box policy
comparison is the remaining measurement, not remaining harness work.
Test coverage
The legacy
aggregate-firstsuite uses a small stand-in child system so it cancreate real Multi-STARK child proofs without the tens to hundreds of GiB
required by a full recursion proof. Those proofs are consumed by the retained
join circuits, so proof validation, statement decoding, set/path folding,
native advice, and transitive recursion are exercised end-to-end at execution
time.
The 57 passing legacy aggregate-first cases cover:
post-order lowering;
a carried assumption;
carrying a different allowed digest;
is flat below and structural above monotonically;
path choice; a carried candidate omitted from the output; the obsolete
88-byte allowed blob; a flat join fed a genuinely free-form structural
child root; omitted/extra assumptions or subjects; noncanonical unsorted
trees; tampered child proofs;
pruning, contraction, dense remapping, and singleton-lift classification;
with the one-pass witness closure matching the legacy per-owned-root union;
verification under it;
former direct construction; the exact 40-byte FRI cache encoding;
independent recursion-vk identity changes for FRI and commitment overrides;
outer claim; whole-plan statement/claim/key derivation before proving;
atomic index creation, corrupt-index detection and repair; a
content-addressed, claim-bound, natively verified resume hit; mismatched
claim rejection; corrupt store-content fallback; checked rejection of
malformed proof bytes without a Rust panic;
ceilings; dependency release; admit-alone oversize handling; the flat-join
affine weight and
MemTotalparser; jobs=1/jobs=2 payload equality;failure draining without admitting a dependent join; jobs=1/jobs=2
byte-identical recursive wrappers under canonical zero-PoW grinding, with
each scheduled child decoded and verified; and
structural
CheckEnvroot.The wrapper-byte scheduler gate uses zero PoW deliberately: with the pinned
positive-PoW implementation, rayon's
find_anyselects any passing grindwitness, so two valid serial proofs already differ in bytes. Production
jobs=1/jobs=2 correctness is the stronger protocol invariant — exact claims
and native verification under the same recursion system. The primitive
Multi-STARK and recursive-verifier suites were rerun to guard the shared
verifier and lift paths, and the separate activation gate covers 132 accepted
shape/input cases twice.
The focused
ix-aggrcommand now runs 93 passing checks. Its 42circuit/shape/plan checks cover both wraps, all flat and structural child-kind
pairs, a nested structural self child, generated/interpreter parity, strict
tree and native keyed-blob framing, identity/shape closure, wrong or tampered
paths, omitted carries, unsorted trees, flat↔structural hint confusion, a flat
parent fed a free-form structural root, and exact four-shard wrap-first/direct
plans. Its 51 converged semantic checks cover uniform claims, cache v2 key
invalidation and verified resume, recursion parameters, manifest
validation/pruning, singleton/canonical/hybrid value reconstruction,
shard-preparation closure sharing, wrap-first/direct planning, per-shape RAM
admission, dependency/failure behavior, and jobs=1/jobs=2 determinism including
concurrent zero-PoW proving. Rust unit tests separately pin channel-6 key layout
and strict path-blob framing.
Validation run
All of the following pass on the current stack:
Both benchmark entrypoints also reject
--queries 0with a usage error beforebuilding or proving, and a stored pre-E2 proof now reports a checked decode
error rather than aborting. The fresh post-E2 aggregate fixture verifies
against both its
.ixeand.ixesinputs.A q=1 live smoke of the converged typecheck join also executed, proved, and
verified direct shape 2 successfully: 1.221742 s execution, 26,738,665,748 FFT
cost, 52.380108 s proving, 21,565,714,432-byte peak RSS, 401,340-byte proof,
and 0.002616 s verification. The M1-f policy harness passed plan-only smoke for
both policies and emitted the expected resumable JSON schema.
Pre-convergence real-environment gates on the 124 GB development host (kept
as WP-A/WP-B baselines for the M1-f rerun):
tc-parity.ixeenvironmentpasses coverage and structural scheduling with threshold zero
(
2 lifts + 1 binary joins (1 structural)), and its one-shard variantplans
1 lifts + 0 binary joins.cache and scheduler, establishing WP-A's invalidation/repair baseline:
090bea6f…ca1535--jobs 2 --max-ram 400At scale, the measured pre-E2 4-shard Init run in Measured performance
above exercised the former backend with real shard proofs, four q=100 lifts,
two lower joins, and a root join with genuine assumption discharge. The pinned
M1-f harness will repeat this fixture under both converged policies.
Soundness summary
its shape-constrained kind.
verify_claimorix_aggr,and every recursive child must carry the same allowed digest, pinning the
two verifying keys and two entrypoints transitively.
bytes.
structural mode proves the exact root-of-roots relation and accounts for
every unique input assumption through either inclusion or explicit carry.
noncanonical assumption tree rejects. Over-carrying and duplicate subject
leaves can only weaken the output claim; the CLI requires an unconditional
final root.
hole or overlap; only leaves with an environment-derived owned-constant
count of zero are removed, and contraction preserves the order and shape of
retained leaves.
the circuit binds its output digest directly to the pinned IxVM child's
CheckEnvdigest.value folding, then verifies the one derived
ix_aggrouter claim. Noclaimed proof kind or shape is accepted from wrapper metadata.
parameter object; any parameter change necessarily changes the recursion vk,
allowed-system identity, and cache key.
outer claim, all derived before proving; hits re-hash store content, bind
the claim, decode without panicking, and verify natively. Corrupt, missing,
or stale entries are misses, never trusted successes or command failures.
snapshots and indexed installation make arrival order irrelevant. The
controller owns all reservations; failures drain running work before exit.
(
crates/kernel/src/claim.rs); canonical openings are required only byprotocol paths that explicitly need them.
Review map
Commit-by-commit review is recommended — each commit is feature-scoped with
its own tests (map in the first comment / commit list).
Ix/MultiStark/Aggregate.lean,Ix/MultiStark.leanIx/Aggr/Circuit.lean,Ix/Aggr.leanIx/Aggr/Host.leanIx/MultiStark/Host.leanIx/Cli/CheckCmd.leanIx/Cli/AggregateCmd.leanIx/Cli/VerifyCmd.leanix_aggrouter claim, value-based environment comparison, manifest-relative hybrid reconstructionIx/MultiStark.lean,Ix/Aggr.lean,Ix/Cli/{Aggregate,Verify}Cmd.leanIx/Aiur/{Protocol,Semantics/BytecodeFfi}.lean,Ix/Cli/{Aggregate,Verify}Cmd.lean,crates/ffi/src/aiur/protocol.rsIx/Store.lean,Ix/Aiur/Protocol.lean,crates/ffi/src/aiur/protocol.rsIx/IxVM/ClaimHarness.lean,Ix/Cli/{Aggregate,Check,Verify}Cmd.leancrates/ixvm-codegen/src/aiur_multi_stark_runner.rscrates/ixvm-codegen/src/aiur_ix_aggr_runner.rs,crates/ffi/src/aiur/protocol.rscrates/ixvm-codegen/src/aiur_multi_stark.rsix codegen --checkcrates/ixvm-codegen/src/aiur_ix_aggr.rsix codegen --checkcrates/kernel/src/shard.rscrates/kernel/src/claim.rs,crates/ixon/src/proof.rsTests/Aggr.lean,Tests/AggrSemantics.lean,Tests/AggrActivation.lean,Tests/MultiStark.leanBenchmarks/AggregatePolicy.lean,Benchmarks/Typecheck.lean, bench registry/dashboardsCurrent limits and non-goals
PoW policy is an explicit follow-up decision (the measured costs above are
therefore the conservative end).
accepts only a bundled value equal to the canonical environment root;
hybrid roots should be verified with both
--ixeand--ixesand theproving threshold.
the safe direction by the measured run); concurrent proves share the rayon
global pool, so throughput can sub-scale — process-per-slot is a
measurement-driven follow-up.
never a soundness issue.
circuit is selected; under the SP1 terminal it is pure cost.
Ixon.Proofand do not encode the proof system;callers must pass
ix verify --aggregate.cache, scheduler, value-based verifier, semantic union, widened activation
audit, and policy benchmark harness. The only remaining M1 work is executing
the wrap-first/direct comparison on the target box. The pinned M1-f revision,
inherited M1-e preflight, and both measured policies are one checkout/session;
its handoff is documented in
plans/aggregate-first-m1f-large-box-runbook.md.terminal KZG/SP1 wrapper.
Follow-ups
flat-vs-structural attribution, and measure frontier/discharge-path counts
at Mathlib scale (plan §11.4.1).
exists.
single-recursion-proof SP1 guest +
ix compress-root).was only 6.80%, so grouping may still be material.
b70042d6d1a029bb8e1d541da7aef5e0613d67e6for the combined M1-e preflightand wrap-first/direct policy benchmark session in the large-box handoff
runbook.