Aggregate-first recursion: lift shard proofs, fold CheckEnv claims, and verify one root

[johnchandlerburnham]

Summary

This PR implements the aggregate-first path for Aiur Multi-STARK proofs. The
production path now runs through one ix_aggr recursion entrypoint: it wraps
independently-proven IxVM shards, folds their CheckEnv statements along the
manifest'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. All data-dependent Stage 2 work
after the two Lean-authored Aiur systems are built—manifest/environment
binding, statement construction, cache validation, scheduling, advice,
proving, persistence, replay, and manifest-bound verification—is orchestrated
in Rust.

The entrypoint has two pair-fold modes:

• Flat shapes perform a canonical set union/difference and are efficient for
  small lower nodes.
• Structural shapes commit to nodeHash(leftRoot, rightRoot) in one hash and
  discharge 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 (default
4096 subject leaves): flat below the threshold, structural above it.

IxVM shard proofs
    │
    ├── ix_aggr shape 0 (default wrap-first policy)
    │     or remain raw with --direct-joins
    ▼
ix_aggr proofs carrying uniform CheckEnv statements
    │
    ├── flat ix_aggr shapes 2–5 below the configured subject threshold
    │     subjects    := canonical(subjectsL ∪ subjectsR)
    │     assumptions := (assumptionsL ∪ assumptionsR) ∖ subjects
    │
    └── structural ix_aggr shapes 6–9 above the threshold
          subjects    := nodeHash(subjectRootL, subjectRootR)
          assumptions := candidates carried or discharged by inclusion path
    ▼
Ixon.Proof {
  claim := CheckEnv(manifest-relative subject root, none),
  proof := one recursive Multi-STARK root proof
}

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 coverage
validation:

raw manifest
    |
    | validate exact environment coverage before pruning
    v
drop zero-constant leaves + contract unary tree nodes + remap retained ids
    |
    +-- one retained leaf  --> wrap once and persist the ix_aggr root
    |
    `-- multiple leaves    --> fold flat/structural joins as above

This is the stage-2 aggregation layer from
plans/aggregate-first-pipeline.md: shard proofs are aggregated before any
terminal KZG/SP1 compression, so a later wrapper only needs to consume one root
proof. Terminal compression remains outside this PR.

Section 14 implementation and its production-scale completion gate are both
complete in this branch. The
ap/ix-aggr single-entrypoint base is reconciled with WP-E2's compact stored
proof / expanded recursive-advice boundary, and its one ix_aggr entrypoint
supports wraps, flat pairs, and structural pairs across both IxVM and recursive
children. ix aggregate now uses that backend for planning, proving, cache
resume, and final verification; ix verify --aggregate derives one uniform
outer claim and performs exact environment/manifest checks. The old
ix aggr command and all three-entrypoint production wiring are retired. The
older 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. The recovery path reused 168
existing Mathlib shard proofs, refined the oversized remainder without
invalidating proven leaves, completed all 239 Stage 1 proofs, and then proved
and fully validated the 477-slot Stage 2 root. The resulting 9.36 MiB wrapper is
checked in as a dated production regression fixture.

Measured performance

Whole-Mathlib production completion (2026-09-02–03)

The full production pipeline completed on a 64-vCPU CPU prover with
approximately 495 GiB usable RAM. The environment contains 679,499 constants;
the refined manifest retained 239 shards.

Stage 1 reused and independently verified 168 earlier successful proofs, then
produced the remaining 71 proofs with ix prove --skip-proven. The successful
original proofs sum to 10:18:29 and the recovery run took 3:11:52, for 13:30:21
(13.5 box-hours) observed proof time. Excluding the failed original shard-168
attempt and correcting the two earlier memory-pressure outliers (shards 124 and
147) gives approximately 12.7 box-hours expected with the refined leaves.
The recovery run peaked at 402.0 GiB RSS with zero swapping and finished with
239/239 proofs indexed and independently verified.

Stage 2 ran the default wrap-first policy at q=100 with --jobs 2,
--max-ram 450, and the default structural threshold:

Work	Result	Wall	Peak RSS	Artifact
Stage 1 total	239/239 shard proofs	13:30:21 observed	402.0 GiB recovery peak	~5.4 GB inputs
Stage 2	239 wraps + 238 joins (477 slots)	14:46:26	491.2 GiB	9,813,583 B root
Root validation	679,499/679,499 constants, zero assumptions	3.23 s	4.0 GiB	valid

Stage 2 exited 0 without swapping and persisted root
c2fdce660eb66899efa303b41d4ca1611a62a688ef20684fdc327739d38bd67f,
proving
CheckEnv(3211abb340539c10220990fb095f8763cb3a364e111ebe57fb518992d42d7382, none). Manifest-bound validation re-hashed and decoded the wrapper, rebuilt
the exact statement from the original .ixe and .ixes, established that all
679,499 constants occur exactly once with no missing/foreign/duplicate leaves,
required zero undischarged assumptions, and cryptographically verified the
Aiur proof.

Moving startup and verification orchestration to Rust also removed the former
Lean task bottleneck. On the same inputs, Stage 2 env/claims preparation fell
from 39.687 s to 1.064 s (37.3×); the verification manifest audit fell from
42.731 s to 2.939 s (14.5×), and end-to-end verification from 43.01 s to
3.23 s (13.3×). The dated wrapper and complete reproduction metadata live in
Tests/Fixtures/Aggregate/mathlib-2026-09-03/.

Four-shard baseline (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 remain the historical M1-f comparison baseline; the converged
direct-vs-wrap harness was not run during that session. The recursion used the
conservative q=100 / PoW 20 defaults this PR keeps:

Stage	Time	Peak RAM	Output proof
Lift × 4	98.8–103.0 s (mean ≈ 101 s)	186.8–195.8 GiB	8,162,462 B each
Join 8+9, 10+11	48.9 / 48.5 s	~102.5 GiB	9,502,843 B
Root join	85.8 s	156.9 GiB	9,455,498 B
Total (serialized)	10:23 wall	195.8 GiB	9,455,498 B

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:

• One production recursion entrypoint, 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.
• Recursive validation of wrap, flat-pair, and structural-pair children with
  transitive verifying-key, function-index, and allowed-system binding. A
  shape hint selects the verified form but cannot weaken its checks.
• Strict in-circuit CheckEnv decoding and canonical flat set folding.
• Structural subject folding with per-candidate Merkle discharge paths while
  keeping output assumption sets canonical and deduplicated.
• One 80-byte protocol identity containing the IxVM/self verifying-key
  digests and their two accepted entrypoint indices; every recursive node has
  the same 18-word outer-claim layout regardless of shape.
• Structural outputs bind nodeHash(leftRoot, rightRoot) and account for each
  unique assumption candidate through a strict Merkle-path-or-carry choice.
• Host helpers construct structural roots, survivors, and path advice. Channel
  6 carries both the one-byte shape at key [0] and candidate path payloads at
  raw 32-byte address keys; the key shapes are disjoint.
• Lean/Rust execute and prove FFI accept a compact keyed path blob, whose
  framing is decoded strictly before the circuit independently validates
  payload semantics.
• The generated ix_aggr executor is regenerated at 2,061,361 bytes / 248
  Aiur functions and parity-tested against the interpreter.

Host driver and operations:

• Strict .ixes aggregation-tree parsing and post-order lowering, with a
  balanced fallback for legacy manifests; validate-then-prune removal of
  zero-constant leaves with unary tree contraction (and a Rust writer that
  stops emitting them).
• Manifest-v2 measured-peak records, tree-preserving selective refinement,
  claim-addressed proof indexing, ix verify --record, and
  ix prove --skip-proven recover oversized or interrupted Stage 1 runs while
  retaining every already-proven leaf.
• Single-shard roots: a one-retained-shard manifest always produces one
  shape-0 ix_aggr wrapper, including under --direct-joins.
• A monotone leaf-count scheduler controlled by --structural-above, with a
  default wrap-first plan (shapes 0 then 5/9) and an explicit
  --direct-joins plan that derives heterogeneous shapes from actual child
  kinds.
• Versioned, content-addressed aggregate cache and resume (WP-A): version 2
  binds the uniform outer claim, and reuse occurs only after content-digest,
  claim, decode, and native verification all pass; --no-cache bypasses.
• Parallel execution of ready wraps/pairs as a dependency DAG under --jobs
  and --max-ram (default 92% of MemTotal), heaviest-first, with failure
  draining (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.
• Native Stage 2 orchestration in crates/ffi/src/aiur/aggregate.rs: one Rust
  controller owns deterministic manifest preparation, statement folding,
  cache admission, the RAM-gated dependency scheduler, recursive advice,
  proving, persistence, and final verification. Constant parsing/ownership and
  per-shard frontier/tree construction use deterministic Rayon parallelism.
• Targeted --reprove-slot N --no-write replay reconstructs the exact slot
  statement and verifies cached immediate children before recomputing one
  suspect wrap/join, without replaying the full Stage 2 DAG.
• A recursion-parameter split (WP-E1): aggregate proving/verification share an
  explicit RecursionParameters value, defaulting to today's q=100 values;
  the q=50+PoW policy decision is deliberately deferred.
• A deterministic 132-case production activation audit across shapes 0–9:
  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.
• Claim-only shard preparation (no discarded dependency-byte closure walks)
  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] [--reprove-slot N --no-write] <proof>... and
  single-entrypoint aggregate verification with cryptographic-only,
  environment-bound, and manifest-bound exact-coverage checks. The verifier
  re-hashes store content and uses the same native Rust statement builder as
  proving. The duplicate ix aggr command is removed.
• Opt-in aggregate benchmarks: a tiny two-shard Init pair end-to-end bench and
  a flat-join bench (singleton CheckEnv shards → two lifts → verified flat
  join), 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.
• Positive, transitive-recursion, scheduler, cache, pruning, parity,
  malformed-input, semantic-tampering, and targeted-replay tests, plus a real
  9.36 MiB q=100 Mathlib root fixture verified through the production backend
  and the separate activation matrix.

Protocol design

One recursion system, one entrypoint

Production builds Aggr.ixAggr, the shared Multi-STARK verifier closure pruned
to one ix_aggr entrypoint. A one-byte advice hint selects the exact verified
shape:

Shape	Children	Fold
0	IxVM	pass-through wrap
1	ix_aggr	pass-through wrap
2–5	IxVM/ix_aggr pair (2 + 2·left + right)	canonical flat fold
6–9	IxVM/ix_aggr pair (6 + 2·left + right)	structural fold

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:

ix_aggr(allowed_digest: [G; 8], out_claim_digest: [G; 8])

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:

1. the 80-byte allowed-system blob; and
2. the serialized output CheckEnv claim.

The allowed blob is:

blake3(ixvm_vk)
  || verify_claim_idx:u64le
  || blake3(ix_aggr_vk)
  || ix_aggr_idx:u64le

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_aggr function selector followed by the packed identity and output
claim 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:

1. reads and fully consumes one proof and exactly one outer claim;
2. runs the Multi-STARK structural verifier;
3. runs ood_verify, including Fiat-Shamir replay, lookup accumulators,
   quotient/OOD checks, Merkle openings, and FRI verification; and
4. decodes the statement according to the constrained child kind and function
   index.

The accepted forms are:

• IxVM child: its system digest must equal blake3(ixvm_vk). Its claims
  digest opens to exactly one 10-word IxVM claim at the pinned
  verify_claim_idx, whose digest opens to a strict serialized CheckEnv
  claim.
• ix_aggr child: its 18-word claim must use the pinned ix_aggr_idx; its
  first public digest must equal the current allowed_digest, transitively
  pinning both systems and both entrypoints; and its second digest opens to its
  output CheckEnv claim.

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:

S_out = S_L ∪ S_R
A_out = (A_L ∪ A_R) ∖ S_out

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 u32 words using the
full-domain u32_less_than primitive. The implementation never uses Aiur
pointer 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:

S_out.root = nodeHash(S_L.root, S_R.root)

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:

• carried (0): no bytes may follow, and the candidate must be the next
  value in the output assumption list; or
• discharged (1): a bounded Merkle path from
  leafHash(candidate) to S_out.root must verify.

Path payloads are strict:

0

1 || count:u8 || repeated(side:u8 || sibling[32])

count is limited to 64. side = 0 hashes nodeHash(sibling, current) and
side = 1 hashes nodeHash(current, sibling); any other side rejects. The
payload 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_aggr shapes use the same seven-channel IO layout. Digest/root bindings
are checked before the corresponding bytes are decoded.

Channel	Key	Value
0	[0], [1]	first and optional second child proof advice bytes
1	[kind]	verifying-key bytes (0 = IxVM, 1 = ix_aggr)
2	[0], [1], [2]	left/right outer claims and output CheckEnv claim
3	[0]	80-byte allowed-system blob
4	packed Blake3 digest	nested claim preimages
5	raw 32-byte address	serialized canonical trees keyed by root
6	[0] / raw candidate address	shape byte / carried-or-discharged path choice

Lean passes channels 4–6 across FFI as compact framed blobs:

count:u32le || repeated(key[32] || payload_len:u32le || payload)

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

.ixes aggregation tree

parseIxesManifest exposes both shard block lists and the optional binary
aggregation tree stored at the manifest tail. It:

• requires nonzero, contiguous shard IDs;
• validates option and tree tags;
• requires tree leaves to be exactly the manifest shard set;
• rejects duplicate/out-of-range leaves and trailing bytes; and
• synthesizes a balanced ascending-ID tree for legacy manifests without a
  tree tail or with an explicit absent-tree tag.

The tree lowers to post-order FoldOp slots. Every join refers only to earlier
slots 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

IxesManifestView retains the original shard id for every dense shard slot.
pruneEmpty:

1. counts the environment constants owned by every raw shard;
2. drops only shards with a count of zero;
3. contracts aggregation-tree nodes with a removed child;
4. densely remaps retained leaf indices; and
5. returns the retained per-shard subject counts with the pruned view.

The aggregate and manifest-aware verifier paths deliberately call
shardsCover on the raw manifest before this transformation. Coverage
still 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:

both retained       -> node(left', right')
only left retained  -> left'
only right retained -> right'
neither retained    -> removed

The Rust .ixes writer (crates/kernel/src/shard.rs) also normalizes new
manifests before serialization — block-empty shard records are omitted, ids
rewritten densely, the tree pruned/contracted/remapped, and cross-ingress
recomputed. The production native controller also performs the stronger
environment-relative pass (a shard may contain blocks yet own zero constants);
the Lean mirror remains a reference and supports non-aggregate check paths.

Monotone structural scheduling

The host counts actual owned constants for each shard after the disjoint-cover
check. schedulePlan annotates every slot with its cumulative subject count and
chooses a structural pair exactly when:

left.subjectCount + right.subjectCount > structuralAbove

The default threshold is 4096; --structural-above 0 makes every join
structural 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_aggr shape-0 wrap, so binary slots are shape
5 below the threshold and shape 9 above it. With --direct-joins, a
multi-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 aggregate imposes no two-shard minimum. The fold plan for one retained
leaf contains one shape-0 wrap and zero pairs; that wrapper and its CheckEnv
claim are persisted as the aggregate root. Even --direct-joins wraps a
singleton because the deliverable must verify under the one production
entrypoint. A self-pair would add work and manufacture a different statement.
Consequences:

• exactly one proof is required per nonempty shard;
• --plan-only reports one wrap and zero binary pairs for a singleton;
• multi-shard flat/structural scheduling is unchanged; and
• the final unconditional-root check always applies to an ix_aggr root.

ix aggregate

ix aggregate --ixe ENV.ixe --ixes SHARDS.ixes \
  [--structural-above N] [--direct-joins] [--jobs N] [--max-ram G] \
  [--no-cache] [--no-write] [--reprove-slot N] \
  SHARD_PROOF_ADDR...

Lean concurrently builds the two Lean-authored Aiur systems and mmap-loads the
environment. One FFI call then hands the complete data-dependent pipeline to
the native controller; the retained Lean implementation is a protocol
reference and unit-test seam, not the CLI path. The Rust controller:

1. parses the manifest, classifies every environment constant to exactly one
   raw shard, validates coverage, then prunes zero-constant leaves;
2. reconstructs every retained shard's exact CheckEnv statement and
   canonical trees in parallel, extracting walk edges in the same constant
   parse that determines ownership;
3. matches proof arguments to shards in any order by bundled claim digest,
   then requires exact claim equality and one proof per nonempty shard;
4. natively verifies every IxVM shard proof before expensive recursion work;
5. derives the pinned 80-byte allowed blob from the supplied IxVM and
   ix_aggr systems;
6. derives every slot's statement, child kind, shape, uniform outer claim, and
   version-2 cache key up front;
7. executes ready wraps and flat/structural pairs as a RAM-gated dependency
   DAG, resuming verified cached slots and persisting each completed wrapper
   (raw direct-policy leaves are verified inputs, not cache slots);
8. canonicalizes all leaves under the final subject tree and checks that they
   reproduce the environment's canonical root;
9. requires no remaining assumptions and natively verifies the outer proof at
   the one ix_aggr root entrypoint; and
10. persists an Ixon.Proof containing the output CheckEnv claim and proof.

--plan-only stops after coverage validation and scheduling, resolving and
printing the scheduler policy without loading or proving shard proofs:

ix aggregate --ixe ENV.ixe --ixes SHARDS.ixes \
  --structural-above 0 --plan-only

--reprove-slot N is the post-run diagnostic path. It bypasses slot N's cache
entry, verifies and loads only its cached immediate children (and raw shard
inputs when needed), recomputes that one exact wrap/join, and compares it under
the ordinary native verifier. --no-write makes this a read-only spot check.

ix verify --aggregate

Aggregate roots reuse Ixon.Proof, so verification is selected explicitly.
The verifier never accepts root-kind metadata. It serializes the bundled
CheckEnv value and reconstructs the only valid outer claim:

claim_bytes := serialize(CheckEnv(...))
outer_claim := ix_aggr(
  blake3(allowed_blob),
  blake3(claim_bytes))

Invocation	Cryptographic entrypoint	Expected statement value
ix verify --aggregate <proof>	ix_aggr	bundled claim; cryptographic proof only
ix verify --aggregate --ixe E <proof>	ix_aggr	canonical environment root, unconditional
ix verify --aggregate --ixe E --ixes M <proof>	ix_aggr	pruned manifest fold, unconditional

Environment-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 calls the same native Rust
statement builder used by proving: it classifies all environment constants,
reconstructs every retained leaf statement, repeats pruning and the threshold
fold, verifies exact cardinality and retained-shard coverage, canonicalizes the
root leaves back to the environment root, rejects missing/foreign/duplicate
subjects and residual assumptions, and verifies the same ix_aggr outer
claim. Store bytes are re-hashed before decoding. Existing non-aggregate proof
and shard-composition verification paths are unchanged.

Claim-only shard preparation

shardCheckEnvClaimTrees remains the Lean reference for constructing only the
CheckEnv claim and its canonical subject/assumption trees.
shardCheckEnvClaim remains the Stage 1 witness-building entry 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.

Production Stage 2 preparation now lives in Rust. It sorts the unordered
environment address map, parses/classifies constants and extracts their kernel
walk edges in one indexed Rayon pass, performs a deterministic ownership
remap, and constructs each retained shard's thin frontier and Merkle trees in
parallel. This both preserves byte/claim determinism and avoids the old second
parse of every lazy constant. The same function serves proving and
manifest-bound verification, preventing their statement semantics from
drifting.

Recursion parameters (WP-E1)

Aggregation and aggregate verification consume one shared
MultiStark.RecursionParameters value containing the recursion commitment and
FRI configurations, carried through runAggregateCmdWith/runVerifyCmdWith
into the shared MultiStark.buildRecursionSystem. The CLI entrypoints pass
defaultRecursionParameters, whose fields are exactly today's canonical Aiur
defaults. This is a mechanism split, not a policy change:

• ordinary IxVM proving and verification remain on the canonical q=100
  configuration;
• recursion proofs also remain q=100 with the same commitment and PoW values;
• no new CLI flag selects security parameters; and
• choosing q=50 plus a compensating PoW policy remains the explicit §9.5
  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.cacheFriBytes pins the
40-byte fri_params_ser cache-key component:

logFinalPolyLen:u64-le || maxLogArity:u64-le || numQueries:u64-le ||
commitProofOfWorkBits:u64-le || queryProofOfWorkBits:u64-le

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-stark series is transplanted onto this
stack: Rust 1.98, the 249b7405 multi-stark revision on P3 v0.6, the matching
Blake3/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_multiplicity travel with
the dependency update; no aggregate claim or public-input format changes.

There are now deliberately two proof encodings. Proof.toBytes is the compact
wire 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.proofToAdviceBytes immediately 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.ofBytesChecked and reports a normal error
for 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 CheckEnv
statement, 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:

blake3(
  aggregateCacheVersion:u64-le ||
  blake3(recursion_vk) ||
  recursion_fri_params:40-bytes ||
  serializeClaims([outer_claim])
)

The uniform outer claim already includes the ix_aggr entrypoint index and
public input, hence the allowed-system blob, output CheckEnv, both
verifying-key identities, and both accepted entrypoint indices. Each completed
recursive slot is stored as an Ixon.Proof wrapper in the content-addressed
~/.ix/store; a raw --direct-joins leaf is only an input and is not cached.
The wipeable index ~/.ix/cache/aggregate/<key> holds only the wrapper's store
address and is updated via temp-file + atomic rename. M1-d bumps
aggregateCacheVersion from 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 — the
former 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-cache bypasses index
reads and intermediate writes while still persisting the final root wrapper.

RAM-gated parallel scheduling (WP-B)

The post-order fold executes in the Rust controller 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 scoped Rust worker per admitted slot. Two
independent limits govern admission:

• --jobs N caps active slots; absent or 0 means every ready slot may run
  if it fits the budget;
• --max-ram G caps total reserved GiB in flight, defaulting to 92% of Linux
  MemTotal.

As in the existing Rust RamGate, a slot whose estimate exceeds the entire
budget is admitted only while nothing else runs — a conservative estimate
serializes work rather than deadlocking. The current per-shape admission
weights are:

raw IxVM leaf              =   4 GiB
shape 0/1 wrap             = 195 GiB
shape 2/6 IxVM + IxVM      = 390 GiB
shape 3/4/7/8 mixed pair   = 340 GiB
shape 5 self + self flat   = 195 GiB + 1 MiB × subject leaves
shape 9 self + self struct = 195 GiB

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. The whole-Mathlib --jobs 2 --max-ram 450 run completed
without swapping but peaked at 491.2 GiB process RSS; slot reservations govern
proof admission rather than promising a hard process-RSS ceiling, so operators
must retain environment/backend/headroom above the selected budget.

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-activation is a dedicated diagnostic kept out of
the default suite. It executes the generated production ix_aggr path across
4 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 any
difference before rendering a deterministic per-shape Markdown report.
Current signature:

52a9c44304c486bd649ddbf7531d0223dbfdb0feb705b5a96b8e2f3a4615cb16

Result: 200 audited circuits — 168 active in every case, 32 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/Bytes2 circuits are
outside 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.executeMultiStarkJoin for generated or interpreted flat
  and structural join execution;
• AiurSystem.proveMultiStarkJoin for witness generation and proving;
• JoinAdvice, JoinPreimage, JoinTree, JoinPath, strict framed decoders,
  and the seven-channel join_io_buffer;
• the matching rs_aiur_multi_stark_join_execute and
  rs_aiur_multi_stark_join_prove externs; and
• Aiur.Proof.ofBytesChecked for 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 is
generated code. The protocol source of truth is
Ix/MultiStark/Aggregate.lean; the native advice contract lives in
aiur_multi_stark_runner.rs. It is now an Ix-agnostic regression/reference backend,
not the production CLI backend.

The production ix_aggr executor 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 in
aiur_ix_aggr_runner.rs; all three generated artifacts are checked with
ix codegen --check.

crates/ffi/src/aiur/aggregate.rs is the production host controller. It owns
the manifest-relative statement model, cached canonical/structural subject
trees, deterministic slot specification, proof/cache/store validation,
RAM-gated dependency scheduling, targeted replay, recursive advice assembly,
and final root audit. Ix/Cli/AggregateCmd.lean concurrently builds the two
systems and crosses the FFI boundary once; its older controller is retained
only as a semantic reference. Ix/Cli/VerifyCmd.lean likewise delegates
manifest-bound expected-root construction to this same native implementation.

Benchmarks

M1-f replaces the legacy two-shard/three-entrypoint runner with
bench-aggregate-policy, a production ix_aggr benchmark for one exact
four-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 natively
verifies all four inputs and every recursive output, persists every completed
slot as an ordinary Ixon.Proof, and writes resumable per-slot and whole-run
timing/RSS/proof metadata.

The existing bench-typecheck --recursive --join row keeps its stable
join-* reporting/dashboard schema, but its join phase now exercises direct
ix_aggr shape 2 instead of the retired join_two circuit. Historical size
baselines remain recorded: 7,986,166 bytes (7,986,204 with the Ixon.Proof
wrapper) 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 completed
whole-Mathlib wrap-first run is now the production-scale acceptance result;
the four-shard direct-vs-wrap policy comparison remains an optional tuning
experiment rather than a merge gate.

Test coverage

The legacy aggregate-first suite uses a small stand-in child system so it can
create 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:

• canonical flat and structural host folds; manifest parsing, validation, and
  post-order lowering;
• distinct lift/flat/structural compiled entrypoint identities;
• honest flat union and cross-child discharge; structural path discharge plus
  a carried assumption;
• flat-join and structural-join outer claim layout and native verification;
• transitively pinned flat and structural children; rejection of a child
  carrying a different allowed digest;
• generated/interpreter parity for both join modes; threshold scheduling that
  is flat below and structural above monotonically;
• strict keyed-blob framing; wrong-root and tampered-sibling paths; a missing
  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;
• a synthetic three-leaf manifest with empty outer leaves: raw coverage before
  pruning, contraction, dense remapping, and singleton-lift classification;
• claim-only shard preparation preserving exact subject/assumption trees,
  with the one-pass witness closure matching the legacy per-owned-root union;
• exact legacy verifier reconstruction of a lift outer claim and native
  verification under it;
• byte-for-byte equality of the shared default recursion builder with the
  former direct construction; the exact 40-byte FRI cache encoding;
  independent recursion-vk identity changes for FRI and commitment overrides;
• cache-key invalidation across version, recursion vk, FRI parameters, and
  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;
• heaviest-first admission with deterministic tie-breaking; job and byte
  ceilings; dependency release; admit-alone oversize handling; the flat-join
  affine weight and MemTotal parser; 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
• Rust writer normalization plus round-tripping a genuinely noncanonical
  structural CheckEnv root.

The wrapper-byte scheduler gate uses zero PoW deliberately: with the pinned
positive-PoW implementation, rayon's find_any selects any passing grind
witness, 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-aggr command now runs 94 passing checks. Its 42
circuit/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 52 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. The additional production fixture gate re-hashes,
decodes, claim-checks, and cryptographically verifies the real 9.36 MiB q=100
Mathlib root through ix verify --aggregate in an isolated store. Rust unit
tests separately pin channel-6 key layout, strict path-blob framing, native
statement folding, and deterministic parallel preparation.

Validation run

All of the following pass on the current stack:

nix develop --command lake exe IxTests aggregate-first       # 57/57
nix develop --command lake exe IxTests ix-aggr                # 94/94, including real Mathlib root
nix develop --command lake exe IxTests aggregate-activation  # 132 cases × 2 stable passes
nix develop --command lake exe IxTests multi-stark           # 12/12
nix develop --command lake exe IxTests recursive-verifier    # 6/6
nix develop --command lake exe IxTests ixes-manifest         # 14/14
nix develop --command lake build IxTests bench-typecheck bench-recursion-debug bench-aggregate-policy ix
nix develop --command cargo test -p ixvm-codegen -p ix-ffi -p ix-kernel -p ixon # 1,033 passed, 3 ignored
nix develop --command cargo clippy -p ixvm-codegen -p ix-ffi -p ix-kernel -p ixon --all-targets -- -D warnings
nix develop --command cargo fmt --all -- --check
nix develop --command lake exe ix codegen --check
git diff --check

Both benchmark entrypoints also reject --queries 0 with a usage error before
building or proving, and a stored pre-E2 proof now reports a checked decode
error rather than aborting. The dated whole-Mathlib fixture verifies under the
current production backend; its provenance record pins the original .ixe
and .ixes hashes and the successful 679,499-constant manifest-bound audit.

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.

Earlier real-environment gates on the 124 GB development host are retained as
WP-A/WP-B historical baselines:

• A two-shard manifest from the 5,986-constant tc-parity.ixe environment
  passes coverage and structural scheduling with threshold zero
  (2 lifts + 1 binary joins (1 structural)), and its one-shard variant
  plans 1 lifts + 0 binary joins.
• Before E2, a one-constant q=100 production lift ran end-to-end through the
  cache and scheduler, establishing WP-A's invalidation/repair baseline:

Pass	Result	Wall
Initial	proved and cached root 090bea6f…ca1535	~64 s
Identical rerun	verified cache hit, same root	1.66 s
Truncated index	clean miss, re-proof, atomic repair, same root	~38 s
Post-repair rerun	verified cache hit, same root	1.79 s
--jobs 2 --max-ram 400	195 GiB reserved, verified hit, same root	1.45 s

At scale, the earlier 4-shard Init run in Measured performance exercised
the former backend with real shard proofs, four q=100 lifts, two lower joins,
and a root join with genuine assumption discharge. The completed 239-shard
Mathlib run now supersedes it as the production completion gate.

Soundness summary

• Every present child is fully verified under the verifying key selected by
  its shape-constrained kind.
• Child function indices are constrained to IxVM verify_claim or ix_aggr,
  and every recursive child must carry the same allowed digest, pinning the
  two verifying keys and two entrypoints transitively.
• Claims and allowed data are Blake3-bound and strictly parsed with no trailing
  bytes.
• Flat mode reopens canonical roots and proves exact union/difference;
  structural mode proves the exact root-of-roots relation and accounts for
  every unique input assumption through either inclusion or explicit carry.
• A bogus path, dropped candidate, extra survivor, malformed choice, or
  noncanonical assumption tree rejects. Over-carrying and duplicate subject
  leaves can only weaken the output claim; the CLI requires an unconditional
  final root.
• Coverage is checked on the unmodified manifest, so pruning cannot conceal a
  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.
• A singleton root is a verified shape-0 wrapper, never a raw-proof shortcut;
  the circuit binds its output digest directly to the pinned IxVM child's
  CheckEnv digest.
• Manifest-aware verification uses the same native statement semantics as
  proving but independently rebuilds them from the supplied environment and
  manifest. It re-hashes the store object, proves exact one-time coverage of
  every environment constant, repeats pruning/scheduling/value folding,
  requires zero assumptions, and verifies the one derived ix_aggr outer
  claim. No claimed proof kind or shape is accepted from wrapper metadata.
• Proving and verification build the recursion system from the same explicit
  parameter object; any parameter change necessarily changes the recursion vk,
  allowed-system identity, and cache key.
• Cache keys bind version, recursion-vk digest, explicit FRI bytes, and exact
  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.
• A pair is admitted only after both child slots complete; immutable
  snapshots and indexed installation make arrival order irrelevant. The Rust
  controller owns all reservations; failures drain running work before exit.
• Targeted replay accepts only a plan-derived slot, verifies the exact cached
  children it consumes, and uses the ordinary statement/claim/proof checks;
  bypassing one cache entry does not bypass protocol validation.
• Free-form structural roots are serialized as opaque commitments
  (crates/kernel/src/claim.rs); canonical openings are required only by
  protocol 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).

Area	Primary files	What to review
Legacy regression protocol	Ix/MultiStark/Aggregate.lean, Ix/MultiStark.lean	pre-convergence 96-byte identity and semantic/audit reference surface
Production circuit	Ix/Aggr/Circuit.lean, Ix/Aggr.lean	80-byte identity, uniform claims, shapes 0–9, heterogeneous child pinning, structural path checks
Converged host model	Ix/Aggr/Host.lean	free-form structural roots, canonical survivors, path extraction
Host statement model	Ix/MultiStark/Host.lean	free-form subject roots, canonical assumptions, path extraction
Manifest parsing + pruning	crates/kernel/src/shard.rs, crates/ffi/src/aiur/aggregate.rs, Ix/Cli/CheckCmd.lean	strict tree parsing, validate-before-prune, unary contraction, dense remap, exact native ownership
Stage 1 recovery	crates/kernel/src/shard.rs, crates/ffi/src/kernel.rs, Ix/Cli/{Shard,Prove,Verify}Cmd.lean	peak-bearing manifest v2, tree-preserving refine, proof index, proven-leaf guard, skip/resume
Aggregate driver	crates/ffi/src/aiur/aggregate.rs, Ix/Cli/AggregateCmd.lean, Ix/Aiur/Protocol.lean	native statement model, wrap-first/direct policy, singleton wrap, cache v2, RAM-gated Rust DAG, deterministic parallel prep, replay; Lean system-build/FFI boundary and reference model
Root verification	crates/ffi/src/aiur/aggregate.rs, Ix/Cli/VerifyCmd.lean	shared native expected-root builder, content re-hash, exact constant audit, one ix_aggr outer claim
Recursion parameters	Ix/MultiStark.lean, Ix/Aggr.lean, Ix/Cli/{Aggregate,Verify}Cmd.lean	shared config plumbing, deterministic systems, stable FRI cache encoding
Pruned FRI multiproofs	Ix/Aiur/{Protocol,Semantics/BytecodeFfi}.lean, Ix/Cli/{Aggregate,Verify}Cmd.lean, crates/ffi/src/aiur/protocol.rs	compact persisted proof vs expanded recursive advice boundary, checked legacy-proof failure
Cache/store boundary	Ix/Store.lean, Ix/Aiur/Protocol.lean, crates/ffi/src/aiur/protocol.rs	wipeable namespace, checked proof decoding, corrupt-data fallthrough
Shard preparation	crates/ffi/src/aiur/aggregate.rs, crates/ixon/src/shard_claim.rs, Ix/IxVM/ClaimHarness.lean	parallel one-parse ownership/edge extraction, thin frontiers, deterministic trees, one-pass Stage 1 witness closure
Native advice	crates/ixvm-codegen/src/aiur_multi_stark_runner.rs	strict framing and seven-channel key layout
Converged native advice	crates/ixvm-codegen/src/aiur_ix_aggr_runner.rs, crates/ffi/src/aiur/protocol.rs	strict path framing, shared channel-6 key layout, execute/prove passthrough
Generated executor	crates/ixvm-codegen/src/aiur_multi_stark.rs	generated artifact; verify with ix codegen --check
Converged generated executor	crates/ixvm-codegen/src/aiur_ix_aggr.rs	generated artifact; verify with ix codegen --check
Manifest writer	crates/kernel/src/shard.rs	producer-side omission, tree remap, aggregate metadata
Claim semantics	crates/kernel/src/claim.rs, crates/ixon/src/proof.rs	free-form root contract and codec regression test
Tests + production fixture	Tests/Aggr.lean, Tests/AggrSemantics.lean, Tests/AggrActivation.lean, Tests/Fixtures/Aggregate/mathlib-2026-09-03/, Tests/MultiStark.lean	94 production shape/semantic/plan/real-root checks, 132-case activation audit, retained Ix-agnostic regressions
Benchmarks	Benchmarks/AggregatePolicy.lean, Benchmarks/Typecheck.lean, bench registry/dashboards	pinned four-shard wrap-first/direct handoff, resumable JSON, converged direct-shape-2 join metrics, historical lift-size pins

Current limits and non-goals

• Recursion FRI parameters stay at the q=100 defaults; the q=50 + compensating
  PoW policy is an explicit follow-up decision (the measured costs above are
  therefore the conservative end).
• Structural roots are manifest-relative. Environment-only verification
  accepts only a bundled value equal to the canonical environment root;
  hybrid roots should be verified with both --ixe and --ixes and the
  proving threshold.
• Scheduler weights are admission estimates, not hard process-RSS limits. The
  Mathlib --jobs 2 --max-ram 450 run reached 491.2 GiB RSS without swapping;
  comparable hosts need equivalent headroom. Concurrent proves share the
  Rayon global pool, so throughput can sub-scale.
• The Rust scheduler is single-host. Cross-host Stage 1 assignment is already
  operationally trivial, but distributed Stage 2 needs an external shared
  proof/cache store or explicit subtree assignment and proof transfer.
• Same-key cross-process cache writes degrade to a warning and recomputation,
  never a soundness issue.
• Dummy-call activation padding is deferred until/unless a static terminal
  circuit is selected; under the SP1 terminal it is pure cost.
• Aggregate wrappers reuse Ixon.Proof and do not encode the proof system;
  callers must pass ix verify --aggregate.
• M1-a–f plus the Mathlib completion work land the converged production
  circuit, native host controller, recovery path, cache, scheduler, exact
  verifier, targeted replay, semantic/activation coverage, and a fully
  validated production fixture. Direct-vs-wrap policy comparison is optional
  tuning, not unfinished correctness work.
• This PR does not adopt cold-circuit grouping and does not implement a
  terminal KZG/SP1 wrapper.

[johnchandlerburnham]

Init full proving report

Revision: 82dcc9dba36d0cfd6c753c6878ab649643a52026
Host: 64 vCPU, 495 GiB RAM, 256 GiB swap
Final result: one verified ix_aggr FRI proof with no remaining assumptions.

Compilation and sharding

Step	Result
Compile source	Benchmarks/Compile/CompileInit.lean
Ix compiler time	1.876s
Constants compiled	65,994
init.ixe size	194,296,853 bytes (185.3 MiB)
Static sharding time	3.1s
Manifest	16 nonempty shards
Retained/owned constants	56,621
Manifest size	2,619,404 bytes (2.50 MiB)
Predicted FFT per shard	4.160e11–4.197e11
Predicted FFT spread	1.01×

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 proofs

All 16 shard proofs were persisted and individually verified against their corresponding manifest claims.

Metric	Serial baseline	Two-way run used for aggregation
Concurrency	1	2
End-to-end wall time	24m 16.76s	15m 53.93s
Sum of shard prover times	22m 43.23s	30m 08.14s
Per-shard time range	74.08–113.97s	98.94–142.29s
Median shard time	82.66s	108.75s
Highest individual RSS	219.8 GiB	219.8 GiB
Combined process-tree peak	—	358.2 GiB
Proof count	16	16
Total proof-wrapper size	—	369,995,038 bytes
Mean proof-wrapper size	—	23,124,690 bytes
Proof-wrapper range	—	22,714,520–23,998,692 bytes

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 aggregation

Policy:

• Wrap-first
• --structural-above 4096
• --jobs 2
• --max-ram 450
• Default q=100 recursion parameters
• Aggregate cache enabled

Plan:

Operation	Count
Shard wraps	16
Binary joins	15
Structural joins	14
Flat joins	1
Total recursive slots	31

Results:

Metric	Result
Wall time	45m 06.61s
Peak resident memory	379.9 GiB
Average CPU utilization	4,192% (~42 cores)
Cache hits	0
Freshly proved/cached slots	31
Swap used	0 bytes
Exit status	0
Final proof-wrapper size	9,596,044 bytes (9.15 MiB)

Final proof

Root address:

80f6844f968920abaef8d8c750a1a1dc1ebe32657a3cfb824e1810bcd65c8814

Final claim:

CheckEnv(6dc8f821a989c6f7b9d520b053ef8edbd582d2408d7b6a6ff72b908666e03b6f, none)

Both validations passed:

• Cryptographic-only aggregate verification
• Manifest-aware verification against init.ixe, init-16.ixes, and structural threshold 4096

End-to-end measured time

Using the two-way Stage 1 run:

Component	Time
Ix compilation	1.876s
Sharding	3.1s
Stage 1 proofs	15m 53.932s
Stage 2 aggregation	45m 06.61s
Measured core pipeline	1h 01m 05.52s

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.

[johnchandlerburnham]

Whole-Mathlib Aiur Stage 1 + Stage 2 production run

We completed the first whole-Mathlib run of this pipeline and validated the
final recursive root against every constant in the original environment. This
was the pipeline this PR is about: Stage 1 is IxVM-on-Aiur and Stage 2 is
recursive aggregation on Aiur-FRI. There is no Zisk, Flock, or terminal SNARK
in these measurements.

Result at a glance

Phase	Result	Measured time	Peak process RSS	Output
Stage 1, original run	168 verified shard proofs	10:18:28.93 summed proof time	490.8 GiB successful max	retained for recovery
Stage 1, recovery	reused 168 and proved 71 new leaves	3:11:52 wall	402.0 GiB	239/239 proofs
Stage 1 total	239/239 independently verified	13:30:20.93 observed proof work	—	5,433,397,399 bytes
Stage 2	239 wraps + 238 joins, all produced fresh	14:46:26 wall	491.2 GiB	9,813,583-byte root
Final root validation	exact audit of all 679,499 constants + Aiur verification	3.25 s wall	3.91 GiB	valid, zero assumptions

The combined successful proving work was therefore 28:16:47 on this one
64-vCPU box. That deliberately excludes the failed original shard-168 attempt,
the stopped Stage 2 startup experiments, builds, preflight/refinement, and final
verification. The Stage 1 number is conservative: normalizing the two successful
but clearly memory-thrashing historical leaves gives about 12.6–12.7 box-hours
instead of 13.5, or roughly 27.4 hours for the two proving stages as run.

Machine, inputs, and proof parameters

The prover was one EC2 CPU host with an Intel Xeon 6975P-C, 32 physical cores / 64
logical CPUs, one NUMA node, approximately 495 GiB RAM, and 255 GiB safety swap.
The successful recovery and aggregation processes both reported zero swaps.

The immutable input environment was:

• mathlib.ixe: 3,326,434,731 bytes;
  SHA-256 1044785de558aa99f93bca19d1e03b239289485d54cc458168b86851f4734609
• 679,499 unique anonymous constants, zero ungrounded constants
• environment root
  07412eac7193311e450e8e4c745c4334eb432c5d2b3405dbe5c6e8fcdb740a91
• Lean 4.33.1

The original 233-leaf manifest was 52,069,567 bytes with SHA-256
fb3e02f4ffb5bd983bd43df47569e11bd188439d2e5376f9c691fba38f408599.
It covered all 679,499 constants exactly once across 663,254 mutual blocks. Its
static FFT-work spread was only 1.01x, which turned out not to predict the large
differences in padded prover memory.

Both stages used the canonical Aiur parameters: log blowup 2, q=100 FRI queries,
0-bit commitment PoW, and 20-bit query PoW. Stage 2 used the default wrap-first
policy and switched from flat to structural joins above 4,096 subject leaves.

Stage 1: recoverable adaptive sharding

What happened in the original run

The original Stage 1 run was serial at revision
82dcc9dba36d0cfd6c753c6878ab649643a52026. It proved and verified leaves
0–167 before original leaf 168 crossed the machine's physical-memory envelope.
That attempt was stopped after about 1h51m at roughly 489–491 GiB RSS plus
123–126 GiB swap, with about 53–55% I/O wait. It produced no proof and is not
included anywhere in the successful-work totals above.

The 168 successful proofs sum to 10:18:28.93. Their median was 3m16s. Two
successful leaves were obvious pressure outliers:

Original leaf	Time	Peak RSS
124	32:01.72	490.2 GiB
147	30:12.32	490.8 GiB

Every other successful historical leaf completed in at most 4m53.56s. This is
why 13.5 box-hours is the literal observed total while 12.6–12.7 box-hours is a
better forward estimate for correctly bounded leaves.

Refinement and reuse

We added a claim-addressed proof index, ix verify --record, tree-preserving
ix shard refine, the post-execution analytic RAM gate, and
ix prove --skip-proven. At recovery revision
54da708f12a7d1e07d19716e9000cb78cb5df553, all 168 existing proofs were
re-hashed, decoded, checked against their exact claims, verified natively, and
kept unsplit.

The whole-partition preflight then executed only the 65 unproved original
leaves. It found three over budget:

Original leaf	Unsplit projected peak	Final refinement
168	768.434 GiB	four leaves: 296.058, 333.688, 283.460, 337.211 GiB
212	575.979 GiB	two leaves: 400.830 and 403.053 GiB
222	577.580 GiB	three leaves: 338.867, 278.066, and 178.817 GiB

Leaf 168 needed two split waves: its first two halves were still projected at
438.623 and 426.965 GiB. Leaf 222's second half was still 420.983 GiB and was
split once more. Replacing three leaves by nine grew the manifest from 233 to
239 leaves, while preserving the other 230 leaves and the original
aggregation-tree structure. There were zero refinement failures.

The refinement itself took 11m19.82s, peaked at 362.8 GiB, and did not swap.
The measured-versus-model calibration over the 168 historical leaves was
accepted: mean ratio 0.990964, median 0.993306, and no underprediction over 10%.
The final manifest has heartbeats from 1,661,840 to 9,270,112 (1.53x imbalance)
and measured projected peaks from 173.6 to 403.1 GiB for the 71 new leaves.

The refined manifest is 52,548,538 bytes with SHA-256
c889f696272a865fed43ba1690c0795ac7c3d4d58c7ff386149cfbaff5778ee4.
The manifest written after proving is byte-identical: no further leaf split was
needed.

Recovery proof run

The successful recovery command was:

ix prove \
  --ixe mathlib.ixe \
  --ixes mathlib-233r.ixes \
  --skip-proven \
  --texray \
  --out-ixes mathlib-233r-proved.ixes

It immediately reused the 168 verified claim-addressed proofs and produced the
remaining 71. Those new proofs sum to 3:06:12 of proof time; total command wall
was 3:11:52, including setup, reuse checks, verification, persistence, and
the final manifest write. New-leaf proof times ranged from 1m31.2s to 3m40.2s
(median 2m36s), and their projected peaks ranged from 173.637 to 403.053 GiB.
The command peaked at 421,525,716 KiB (402.0 GiB), performed zero swaps, exited
0, and reported 239 shard(s) proven, partition unchanged.

As a separate integrity pass, we verified all 239 persisted proofs with 32
verification processes. It completed in 6m08.53s with 239 successes and zero
failures. A second manifest audit completed in 40.17s and confirmed that the
partition remained disjoint and covered all 679,499 constants. The 239 Stage 1
wrappers occupy 5,433,397,399 bytes total (5.43 GB / 5.06 GiB), ranging from
19,974,189 to 25,587,632 bytes each.

Stage 2: recursive Aiur-FRI aggregation

Startup work discovered during the run

The first attempt made clear that Stage 2's host orchestration, not proving,
still had a Lean scalability problem. The revision-54da Lean baseline was
stopped after 21m16.70s while it was still constructing/printing the 477-slot
plan. Follow-up Lean-task versions got reported setup down to about 224–227s,
but brought Lean task/runtime constraints into the scheduler and were stopped
without producing cached Stage 2 proofs. None of those diagnostic attempts is
included in the production timing.

We then moved the data-dependent controller to Rust: manifest/environment
binding, claim preparation, statement construction, cache validation,
dependency scheduling, advice construction, proving, and persistence. At the
production revision, Rust --plan-only completed in 41.62s wall (40.191s
internal: 20ms manifest, 39.687s environment/claims, 483ms plan/statements).
The later parallel one-parse preparation in e92a44f5 reduced that same plan to
3.01s process wall / 1.571s internal, with environment/claims preparation at
1.064s. The proof below was produced by the first Rust controller, before that
last startup optimization.

Final production run

The production command at
77d132d80c65efd9d7d65136a7f4e3466e36ab9a was:

xargs -a proof-addresses-r.txt -n 239 -x ix aggregate \
  --ixe mathlib.ixe \
  --ixes mathlib-233r-proved.ixes \
  --jobs 2 \
  --max-ram 450

The plan contains:

• 239 shape-0 wrappers, one for every Stage 1 IxVM proof;
• 38 flat shape-5 joins below the 4,096-subject threshold; and
• 200 structural shape-9 joins above the threshold.

This also answers why Stage 2 reports 477 nodes for 239 shards: there are
still only 238 binary joins, but every Stage 1 proof first needs its own
proof-producing wrap into the uniform ix_aggr recursion system, so the Stage
2 DAG has 239 wraps + 238 joins = 477 slots.

The scheduler admitted at most two proofs and reserved 450 GiB total. Normal
wrap and structural slots reserve 195 GiB each; lower flat reservations add 1
MiB per subject. These are admission weights rather than a hard process-RSS
limit, which is why the process could peak above 450 GiB after shared
environment/backend/runtime overhead.

All 477 slots were cache misses and were proved fresh. The command:

• ran from 2026-09-02 19:01:35 UTC to 2026-09-03 09:48 UTC;
• completed in 14:46:26;
• averaged 3,386% CPU, or about 33.9 logical cores;
• peaked at 515,028,732 KiB (491.2 GiB) RSS;
• reported zero swaps and exit status 0; and
• persisted 4,353,382,440 bytes (4.35 GB / 4.05 GiB) of Stage 2 proof wrappers,
  of which only the final root is the deliverable.

Stage 2 timing diagnostics

The production log did not yet emit explicit per-slot durations, so these
numbers are reconstructed to roughly one-second accuracy from scheduler
admission order and the content-store publication mtime of each resulting
wrapper. They are useful diagnostics, but should not be mistaken for an
instrumented profile.

Across all 477 slots:

• median: 2m28.5s;
• p90: 2m45.2s;
• p95: 3m13.6s;
• median wrap / flat / structural: 2m30.6s / 2m24.5s / 2m27.0s;
• 465/477 slots completed within ten minutes, averaging 2m31.9s; and
• approximate two-worker occupancy through root publication was 98.9%.

The 12 slots over ten minutes consumed 9.50 worker-hours—32.6% of the run's
29.11 total worker-hours. The clearest anomalies were:

Slot	Kind	Subjects	Approx. duration
261	wrap	4,253	165m16s
254	structural	321,172	142m03s
382	wrap	3,731	33m16s
322	wrap	2,647	32m55s
375	structural	176,499	31m41s
253	structural	131,862	30m25s

Slots 261 and 254 overlapped and published only twelve seconds apart after both
had been slow for well over two hours. Other slow slots also occurred in paired
windows. Conversely, the 679,499-subject root itself took only about 4m26s, and
the final seven-slot serial dependency tail took about 19m17s. Together with the
28,985,662 major page faults and near-capacity RSS reported by time, that
pattern is consistent with host-level memory/page-cache contention, rather
than structural subject count being intrinsically expensive. It is not yet a
proof of cause. This PR now has --reprove-slot N --no-write, so slots 254,
261, 322, 375, and 382 can be replayed one at a time against their verified
cached children to separate per-slot cost from two-worker interference.

For scale: replacing only the >10-minute anomalies by the median for their
respective shapes would put this two-worker run near 10.1 hours. That is a
diagnostic normalization, not a claimed benchmark result; the literal measured
Stage 2 wall remains 14:46:26.

Final root and independent validation

The persisted root wrapper is:

• content address (BLAKE3):
  c2fdce660eb66899efa303b41d4ca1611a62a688ef20684fdc327739d38bd67f
• SHA-256:
  1a3cc584d5ab8cfba51fb5457aca13b643020b3684281d49472f9d0a21df1df1
• size: 9,813,583 bytes (9.36 MiB)
• claim:
  CheckEnv(3211abb340539c10220990fb095f8763cb3a364e111ebe57fb518992d42d7382, none)

At e92a44f518addd31e77a68b06ec8f9841c553b83, we reran the production,
manifest-bound verifier:

ix verify --aggregate \
  --ixe mathlib.ixe \
  --ixes mathlib-233r-proved.ixes \
  c2fdce660eb66899efa303b41d4ca1611a62a688ef20684fdc327739d38bd67f

It re-hashed and decoded the store object, independently rebuilt the exact
manifest-relative statement from the 3.33 GB environment and refined manifest,
checked every leaf, and verified the Aiur proof. The rerun reported:

[verify] native manifest audit: 679499 constants in 2955ms
[verify] aggregate backend setup: 179ms
[verify] aggregate Aiur proof: 51ms
ok: aggregate proof c2fdce66…d38bd67f verifies
    CheckEnv(3211abb3…d7382, none)
[verify] aggregate coverage: 679499/679499 environment constants committed exactly once
[verify] all 679499 included constants certified well-typed; 0 undischarged assumptions

Total verifier wall was 3.25s, peak RSS was 4,099,200 KiB (3.91 GiB), and exit
status was 0. The earlier Lean audit baseline was stopped after 35m11s; the
first native Rust audit finished in 43.01s, and parallel one-parse preparation
reduced that to the 3.25s result above.

The exact wrapper is now a dated repository fixture at
Tests/Fixtures/Aggregate/mathlib-2026-09-03/, committed in d9751983. Its
provenance record pins both input hashes, producer and validator revisions,
parameters, timing, RSS, root, and full-validation result. The regression test
re-hashes and decodes the wrapper, pins the unconditional claim, and runs it
through the production native verifier. We intentionally do not check the
3.33 GB environment or 52.5 MB manifest into Git; their hashes above make the
full audit reproducible from retained inputs.

What this says about multi-box proving

The measurements support the earlier estimate that this can be brought into
the low-single-digit-hour range with a cluster, but they sharpen the operating
assumptions:

1. Stage 1 is embarrassingly parallel after preflight. The 239 independent
   proofs represent 13.5 observed box-hours, or about 12.6–12.7 healthy
   box-hours. One proof at a time per 495 GiB host is the safe policy. Sixteen
   comparable hosts therefore put Stage 1 around 48–51 minutes plus dispatch
   and the 5.43 GB proof collection.
2. Stage 2 is a ready-node DAG. This run accumulated 29.11 slot-worker-hours
   with two workers, but about one third was in twelve likely contention
   outliers. With one slot per host, 16 hosts give a measured-work lower-order
   estimate around 1.8 hours plus the approximately 19-minute final dependency
   tail. If isolated replay confirms that the outliers disappear without
   same-host interference, the normalized work is closer to 20.1 worker-hours.
3. The data plane is modest. Stage 1 produced 5.43 GB and all 477 Stage 2
   wrappers total 4.35 GB. A shared content-addressed store, or explicit
   immediate-child transfers, is sufficient; each parent needs only its two
   child wrappers and the common environment/manifest.
4. The missing piece is orchestration, not proof semantics. The current Rust
   controller is single-host. A distributed controller must atomically claim
   ready slots, verify cached children, publish content-addressed results, and
   make parents ready. Slot identity, deterministic statements, verified cache
   entries, and targeted replay already provide most of the protocol boundary.

A reasonable planning number from this run is therefore about 2–3 hours on
16 equivalent boxes for both stages, with Stage 1 using one large proof per
box and Stage 2 spreading ready nodes across the fleet. The range is more honest
than the idealized 1.8-hour number until the anomalous Stage 2 slots have been
replayed in isolation and cross-host scheduling overhead has been measured.

The main completion result is independent of that projection: all 239 Stage 1
proofs verified, all 477 Stage 2 slots completed, and the final Aiur-FRI proof
cryptographically certifies the typing of each of the 679,499 included Mathlib
constants exactly once, with no residual assumptions.

[arthurpaulino]

Is this necessary?

[arthurpaulino]

I think the content of the Ix/Aggr folder already superseded by Ix/MultiStark/Aggregate.lean and Ix/MultiStark/Host.lean