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

[johnchandlerburnham]

This PR implements the aggregate-first path for Aiur Multi-STARK proofs. It
lifts independently-proven IxVM shards into one recursion system, folds their
CheckEnv statements along the manifest's bisection tree, and persists one
recursive root proof.

The fold has two join modes:

• join_two performs a canonical set union/difference and is efficient for
  small lower nodes.
• join_two_structural commits to nodeHash(leftRoot, rightRoot) in one hash
  and discharges assumptions with Merkle inclusion paths. Its 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
    │
    ├── verify_multi_stark_proof (lift)
    ▼
recursive proofs carrying per-shard CheckEnv statements
    │
    ├── join_two below the configured subject threshold
    │     subjects    := canonical(subjectsL ∪ subjectsR)
    │     assumptions := (assumptionsL ∪ assumptionsR) ∖ subjects
    │
    └── join_two_structural 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
}

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.

What lands

• Three production recursion entrypoints under one verifying key:
  verify_multi_stark_proof, join_two, and join_two_structural.
• Recursive validation of lift, flat-join, and structural-join children with
  transitive verifying-key, function-index, and allowed-system binding.
• 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.
• A version-2 96-byte protocol identity containing all three recursion
  entrypoint indices.
• Strict .ixes aggregation-tree parsing and post-order lowering, with a
  balanced fallback for legacy manifests.
• A monotone leaf-count scheduler controlled by --structural-above.
• Native seven-channel advice construction and Lean/Rust execute/prove FFI for
  both join modes.
• ix aggregate --ixe E --ixes M [--structural-above N] <proof>..., including
  a cheap --plan-only mode.
• Aggregate verification with cryptographic-only, all-flat environment-bound,
  and manifest-bound hybrid-root modes.
• Positive, transitive-recursion, scheduler, interpreter/codegen parity,
  malformed-input, and semantic-tampering tests.

Protocol design

One recursion system, three entrypoints

MultiStark.multiStark prunes the combined call closures of:

• verify_multi_stark_proof: the existing lift, which verifies one proof
  from an arbitrary digest-bound Multi-STARK system;
• join_two: the flat join, which opens canonical subject trees and folds
  their sorted sets; and
• join_two_structural: the structural join, which treats child subject
  roots as opaque Merkle roots and combines them with one node hash.

All three share one recursion verifying key. Every child outer claim identifies
its entrypoint by function index, and both join entrypoints constrain that index
to one of these three allowed forms. Verifying under the same key is therefore
not enough to admit an unrelated recursion function.

Public statement and pinned protocol identity

Both joins expose the same public-input shape:

join_two(allowed_digest: [G; 8], out_claim_digest: [G; 8])
join_two_structural(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 version-2 96-byte allowed-system blob; and
2. the serialized output CheckEnv claim.

The allowed blob is:

blake3(ixvm_vk)
  || verify_claim_idx:u64le
  || blake3(recursion_vk)
  || lift_idx:u64le
  || flat_join_idx:u64le
  || structural_join_idx:u64le

The circuit requires exactly 96 bytes and rejects the old 88-byte layout. 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 any function in those systems; binding
all four relevant 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.

Child-proof validation and transitive pinning

Each join reads the recursion verifying key once, checks its Blake3 digest
against the allowed blob, deserializes it strictly, and uses it for both
children. For each child it:

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 function index.

The accepted forms are:

• Lift child: its system digest must equal blake3(ixvm_vk). Its claims
  digest opens to exactly one IxVM claim at the pinned verify_claim_idx, whose
  digest opens to a strict serialized CheckEnv claim.
• Flat or structural join child: its first public digest must equal the
  current allowed_digest, transitively pinning the same systems and all
  entrypoints. Its second digest opens to its output CheckEnv claim.

Any other index, shape, digest, trailing byte, or failed proof check rejects.
This keeps lift→join, flat→join, and structural→structural composition on the
same statement format.

Flat canonical folding

For child statements (S_L, A_L) and (S_R, A_R), join_two enforces:

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

join_two_structural performs the same allowed-blob binding, recursion-key
binding, two child-proof verifications, child decoding, and output-claim
binding as the flat entrypoint. It then replaces 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

Both joins use the same seven-channel IO layout. Digest/root bindings are
checked before the corresponding bytes are decoded.

Channel	Key	Value
0	[0], [1]	left and right recursive proof bytes
1	[0]	recursion verifying-key bytes
2	[0], [1], [2]	left/right outer claims and output CheckEnv claim
3	[0]	96-byte allowed-system blob
4	packed Blake3 digest	nested claim preimages
5	raw 32-byte address	serialized canonical trees keyed by root
6	raw candidate address	carried/discharged choice and optional Merkle path

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.

Flat joins receive full subject/assumption tree advice and an empty path blob.
Structural joins 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 a
stable basis for future parallel/cache execution.

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 join 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.

The proving loop checks reconstructed subject counts against the schedule
before starting expensive work.

ix aggregate

ix aggregate --ixe ENV.ixe --ixes SHARDS.ixes \
  [--structural-above N] SHARD_PROOF_ADDR...

The command:

1. deserializes the environment and manifest and verifies a disjoint exact
   shard cover;
2. rejects empty shards and manifests with fewer than two shards;
3. reconstructs every shard's exact CheckEnv claim and canonical trees;
4. matches proof arguments to shards in any order by bundled claim digest,
   then requires exact claim equality and one proof per shard;
5. natively verifies every IxVM shard proof before an expensive lift;
6. builds the IxVM and combined recursion systems and the pinned 96-byte
   allowed blob;
7. lifts leaves and proves flat/structural joins in manifest post-order;
8. canonicalizes all leaves under the final free-form subject tree and checks
   that they reproduce the environment's canonical root;
9. requires no remaining assumptions and natively verifies the actual outer
   proof at its scheduled root entrypoint; and
10. persists an Ixon.Proof containing the output CheckEnv claim and proof.

--plan-only stops after coverage validation and scheduling. It needs no proof
arguments and does not compile recursion systems or begin proving:

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

ix verify --aggregate

Aggregate roots reuse Ixon.Proof, so verification is selected explicitly:

# Cryptographically verify either root entrypoint against the bundled claim.
ix verify --aggregate ROOT_PROOF_ADDR

# Bind an all-flat root to the environment's canonical CheckEnv(root, none).
ix verify --aggregate --ixe ENV.ixe ROOT_PROOF_ADDR

# Reproduce and bind the exact hybrid manifest-relative root.
ix verify --aggregate --ixe ENV.ixe --ixes SHARDS.ixes \
  [--structural-above N] ROOT_PROOF_ADDR

Without environment inputs, the verifier tries the flat and structural root
entrypoints and reports which one verified. --ixe alone retains the all-flat
canonical-root behavior. With both --ixe and --ixes, it rechecks shard
coverage, reconstructs every leaf statement, reruns the same threshold
schedule, folds the exact hybrid root, requires no assumptions, and verifies
under the scheduled root entrypoint. The threshold must match the proving run.

Existing non-aggregate proof and shard-composition verification paths are
unchanged.

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; and
• the matching rs_aiur_multi_stark_join_execute and
  rs_aiur_multi_stark_join_prove externs.

The generated executor is parity-checked against the bytecode interpreter on
both output and every circuit's unique-row/total-hit counts. The combined
production verifier now contains 247 Aiur functions; the regenerated Rust file
is 2,221,559 bytes. 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.

Test coverage

The 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
production lift. Those proofs are consumed by the production join circuits, so
proof validation, statement decoding, set/path folding, native advice, and
transitive recursion are exercised end-to-end at execution time.

The 29 passing 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; and
• tampered child proofs.

The primitive Multi-STARK and recursive-verifier suites were also rerun to
guard the shared verifier and lift paths.

Validation run

All of the following pass on this branch:

nix develop --command lake exe IxTests aggregate-first       # 29/29
nix develop --command lake exe IxTests multi-stark            # 12/12
nix develop --command lake exe IxTests recursive-verifier      # 6/6
nix develop --command lake build IxTests
nix develop --command lake build Ix.Cli.AggregateCmd Ix.Cli.VerifyCmd Tests.MultiStark
nix develop --command cargo test -p ixvm-codegen aiur_multi_stark_runner
nix develop --command cargo check -p ixvm-codegen -p ix-ffi
nix develop --command cargo clippy -p ixvm-codegen -p ix-ffi --tests -- -D warnings
nix develop --command cargo fmt --all -- --check
nix develop --command lake exe ix codegen --check
git diff --check

A real two-shard manifest from the 5,986-constant tc-parity.ixe environment
also passes coverage and structural scheduling with threshold zero:

[aggregate] plan: 2 lifts + 1 binary joins (1 structural; threshold > 0 subject leaves)
  slot 0: lift shard 0 (2493 subjects)
  slot 1: lift shard 1 (3493 subjects)
  slot 2: structural join slots 0, 1 (5986 subjects)

Soundness summary

• Both children are fully verified under the digest-bound recursion key.
• Child function indices are constrained to lift, flat join, or structural
  join, and nested protocol identity is pinned 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.
• The host checks extensional environment coverage, and manifest-aware
  verification independently reconstructs the scheduled hybrid claim.

Review map

Area	Primary files	What to review
Circuit protocol	Ix/MultiStark/Aggregate.lean, Ix/MultiStark.lean	96-byte identity, child pinning, canonical fold, structural path checks
Host statement model	Ix/MultiStark/Host.lean	free-form subject roots, canonical assumptions, path extraction
Manifest scheduling	Ix/Cli/CheckCmd.lean, Ix/Cli/AggregateCmd.lean	owned-constant counts, monotone threshold, runtime invariants
Root verification	Ix/Cli/VerifyCmd.lean	root-kind selection and manifest-relative hybrid reconstruction
Lean/Rust boundary	Ix/Aiur/Protocol.lean, Ix/Aiur/Semantics/BytecodeFfi.lean, crates/ffi/src/aiur/protocol.rs	path blob APIs and error propagation
Native advice	crates/ixvm-codegen/src/aiur_multi_stark_runner.rs	strict framing and seven-channel key layout
Generated executor	crates/ixvm-codegen/src/aiur_multi_stark.rs	generated artifact; verify with ix codegen --check
Tests	Tests/MultiStark.lean	flat/structural positives, parity, transitivity, scheduler, negatives

Current limits and non-goals

• No production q=100 lift/join campaign was run on this machine. Existing
  measurements project roughly 195 GiB peak RAM for even the small production
  lift, while the development host has 124 GB. The real end-to-end gate needs a
  host with at least 256 GiB RAM.
• The real-env run above validates coverage and scheduling only; it does not
  measure structural path totals, prove time, peak RSS, or proof size.
• Structural roots are manifest-relative. Environment-only verification is
  therefore restricted to all-flat roots; hybrid roots should be verified with
  both --ixe and --ixes and the same threshold used during proving.
• The first host driver is intentionally serial and cache-free. Slot inputs are
  content-addressed, but resumable caching and level-parallel joins are
  follow-ups.
• The CLI requires at least two nonempty shards. Single-shard lift packaging
  and empty-leaf pruning need an explicit persisted root-kind/system format.
• Aggregate wrappers reuse Ixon.Proof and do not encode the proof system;
  callers must pass ix verify --aggregate.
• Input-independent activation of every verifier circuit has not been audited
  or padded with dummy calls. This matters before a future static terminal
  circuit consumes the verifier.
• This PR does not tune recursion FRI parameters, adopt pruned FRI
  multiproofs/cold-circuit grouping, add production benchmark rows, or
  implement a terminal KZG/SP1 wrapper.

Follow-ups

1. Run a real two-shard production pipeline on a ≥256 GiB host and record lift
   and both join modes' time, peak RSS, proof size, and native verification.
2. Measure aggregate frontier counts and structural Merkle-path hashing at
   Mathlib scale.
3. Add versioned content-addressed lift/join cache entries and resume support.
4. Schedule independent lifts and same-level joins in parallel under an
   explicit RAM budget.
5. Add single-shard root packaging and prune empty manifest leaves.
6. Audit activation sets across child shapes and add dummy calls where needed.
7. Apply the proof-size/RAM work from W2, then connect the one root proof to the
   selected terminal compression path.