Aggregate-first follow-up: package single-shard roots and prune empty leaves

[johnchandlerburnham]

Summary

This stacked PR implements WP-C from the aggregate-first follow-up plan. It
makes a one-nonempty-shard manifest a valid aggregate deliverable and removes
empty manifest leaves without changing the environment statement being proved.

The resulting pipeline now has a root for every nonempty manifest shape:

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

ix verify --aggregate also learns how to reconstruct and verify the exact
outer claim of a lift root. No self-join or padding proof is introduced.

Why

The aggregate-first implementation previously rejected both:

• manifests with fewer than two shards; and
• legacy manifests containing a shard that owns no environment constants.

That made small environments and over-partitioned manifests unusable even
though the recursion schedule already represents a leaf as a lift. Padding a
single lift with a self-join would add work and manufacture a different claim
shape. The natural root of a singleton fold is the lift itself.

Empty leaves are similarly an artifact of partitioning, not part of the
CheckEnv statement. Once raw manifest coverage proves that an empty leaf owns
no constant, removing it and contracting its parent cannot remove a checked
subject.

What changes

Validate first, then prune empty manifest leaves

IxesManifestView now 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

Persist the lift for a single retained shard

ix aggregate no longer imposes a two-shard minimum. The existing fold plan
for one retained leaf contains one lift slot and zero joins. That lift proof and
its CheckEnv claim are persisted directly as the aggregate wrapper.

Consequences:

• exactly one proof is required per nonempty shard;
• --plan-only reports 1 lifts + 0 binary joins for a singleton;
• multi-shard flat/structural scheduling is unchanged; and
• the final unconditional-root check applies equally to lift and join roots.

Reconstruct lift roots during aggregate verification

Aggregate verification now treats the root kind as one of lift, flat, or
structural. For a bundled CheckEnv claim, the verifier reconstructs the
single-shard lift statement rather than trusting metadata from the wrapper:

claim_bytes := serialize(CheckEnv(...))
inner_input := pack(blake3(claim_bytes))
inner_claim := IxVM.verify_claim(verify_claim_idx, inner_input)
lift_input  := verifierPubInput(ixvm_vk, serializeClaims([inner_claim]))
outer_claim := recursion.lift(lift_idx, lift_input)

The proof must verify against this exact outer claim under the locally rebuilt
recursion system. This binds the root to the pinned IxVM verifying key,
verify_claim index, lift index, and bundled CheckEnv statement.

Verification modes are now:

Invocation	Accepted root kinds	Expected statement
ix verify --aggregate <proof>	lift, flat, structural	cryptographic proof only
ix verify --aggregate --ixe E <proof>	lift or flat	canonical environment root, unconditional
ix verify --aggregate --ixe E --ixes M <proof>	exact lift/flat/structural kind	pruned manifest fold, unconditional

The environment-only mode cannot reconstruct a manifest-relative structural
root, so it remains limited to the two roots whose statement is the canonical
environment root. Manifest-aware verification reproduces pruning and the fold
schedule, then checks exactly the resulting root kind.

Stop writing block-empty shards

The Rust .ixes writer now normalizes new manifests before serialization:

• block-empty shard records are omitted;
• retained shard ids are rewritten densely;
• the aggregation tree is pruned, contracted, and remapped;
• total cross-ingress is recomputed over retained shards; and
• the normalized shard list and tree are serialized together.

The Lean-side pass remains necessary for legacy manifests and for the stronger
environment-relative condition: a shard may contain blocks yet own zero
constants after the environment is examined.

Audit structural-root acceptance

The small structural-root audit from §13 is folded into this change. There is
no Rust claim validator that requires a canonical CheckEnv.root; the field is
already an opaque address. Stale comments now state that both canonical roots
and free-form merkle_join roots are valid protocol commitments, while
env-derived builders continue to emit canonical roots.

A Rust round-trip test uses a genuinely noncanonical structural root and
asserts that it remains accepted by the claim codec.

CLI examples

A real one-shard manifest for tc-parity.ixe now plans successfully:

$ ix shard tc-parity.ixe --shards 1 --out /tmp/tc-parity-single.ixes
[shard] wrote 1 shards (5986 consts, 5506 blocks) ...

$ ix aggregate --ixe tc-parity.ixe \
    --ixes /tmp/tc-parity-single.ixes --plan-only
[shards] 1 shards, 5986 consts
  shard 0: 5506 blocks, 5986 consts
[shards] OK: every env constant is owned by exactly one shard
[aggregate] plan: 1 lifts + 0 binary joins (0 structural; threshold > 4096 subject leaves)
  slot 0: lift shard 0 (5986 subjects)

For a legacy manifest with empty leaves, aggregation reports the normalization
before printing the plan:

[aggregate] pruned N zero-constant manifest shard(s)

Soundness notes

• 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.
• Tree contraction preserves the relative order and shape of all retained
  leaves; dense remapping changes identifiers, not statements.
• A singleton root is the already-verified lift proof, not an unverified wrapper
  shortcut.
• Verification derives the nested IxVM claim and lift public input from the
  wrapper's CheckEnv claim and locally compiled protocol identities.
• Manifest-aware verification independently repeats pruning and root-kind
  selection instead of accepting a claimed proof kind.
• New Rust manifests avoid block-empty leaves at the producer, while the Lean
  consumer remains defensive for older or environment-empty records.
• Free-form structural roots are serialized as opaque commitments; canonical
  tree openings are required only by protocol paths that explicitly need them.

Tests and validation

The aggregate-first suite grows from 29 to 34 tests. New coverage includes:

• a synthetic three-leaf manifest whose outer leaves are empty;
• raw coverage validation before pruning;
• empty-leaf contraction and dense remapping to the original middle shard;
• one retained shard being classified as a lift root;
• exact verifier reconstruction of a lift outer claim;
• native verification using that reconstructed claim;
• Rust writer normalization of shard ids and aggregation-tree leaves; and
• round-tripping a genuinely noncanonical structural CheckEnv root.

The following pass on this branch:

nix develop --command lake exe IxTests aggregate-first       # 34/34
nix develop --command lake build IxTests                      # 1079 jobs
nix develop --command cargo test -p ix-kernel shard::tests    # 23/23
nix develop --command cargo test -p ixon test_check_env_claim_accepts_structural_root
nix develop --command cargo clippy -p ix-kernel -p ixon --tests -- -D warnings
nix develop --command cargo fmt --all -- --check
nix develop --command lake exe ix codegen --check
git diff --check

Code generation remains current:

ixvm:       5,807,375 bytes / 780 functions
multi-stark: 2,221,559 bytes / 247 functions

The production-shaped one-shard tc-parity.ixe CLI run above also passes raw
coverage, pruning, scheduling, and proof-count planning.

Review map

Area	Primary files	What to review
Manifest pruning	Ix/Cli/CheckCmd.lean	validate-before-prune contract, unary contraction, dense remap, original ids
Aggregate driver	Ix/Cli/AggregateCmd.lean	singleton schedule, proof count, persisted lift root, diagnostics
Root verification	Ix/Cli/VerifyCmd.lean	exact lift-claim reconstruction and root-kind policy
Lean tests	Tests/MultiStark.lean	synthetic empty leaves and reconstructed lift verification
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

Scope and limits

• This is a stacked follow-up to the aggregate-first/structural-join PR and
  should be reviewed against jcb/aggregate-first.
• The change does not alter lift, flat-join, or structural-join circuits,
  allowed-system encoding, FRI parameters, or generated bytecode.
• It does not add cache/resume, parallel scheduling, activation padding,
  terminal compression, or benchmark instrumentation; those remain separate
  §13 work packages.
• A full production q=100 lift was not run on this 124 GB host. Existing
  measurements project roughly 195 GiB peak memory for that proof. The real
  manifest path was therefore exercised through --plan-only; native lift
  reconstruction and proof verification are covered at smoke scale.