feat(prover): batch_splitter — split sealed batches into two Airbender pieces

[deniallugo-claude]

Why

Boojum can prove heavier batches than Airbender's geometry allows. To migrate such batches to Airbender we want to: prove the whole batch, and on failure split it into two pieces and prove each — recursively, until each piece fits Airbender's geometry.

This PR adds a batch_splitter binary (core/bin/batch_splitter) that splits a sealed L1 batch N into two independently-provable AirbenderVerifierInput pieces.

What it does

For batch N spanning L2 blocks [first, last], it cuts at the midpoint (even by block count, whole blocks only) into piece A [first, mid) and piece B [mid, last], such that old_root_N →(A) root_A →(B) new_root_N.

• Witness-input level, not a slice. A witness input is one bootloader program; the per-op arrays can't be cut at a block boundary. So each half is re-executed over its block range (mirroring BasicWitnessInputProducer / AirbenderVerifierInput::verify), seeded from the in-witness storage snapshot (piece B overlaid with A's writes).
• Non-invasive. Reads only Postgres (MVCC) and immutable object-store blobs; never writes the canonical chain, re-commits to L1, re-numbers batches, or touches the Merkle-tree RocksDB.
• Merkle paths from N's own multiproof. Sibling hashes come from batch N's immutable WitnessInputMerklePaths blob — the only non-invasive source. A sparse binary Merkle tree is reconstructed from it (N-1 leaf values from each key's first occurrence; off-trie siblings are invariant during N), then A's and B's writes are re-applied to regenerate each piece's paths + root_A. Hashing reuses Blake2Hasher's hash_leaf/hash_branch/empty_subtree_hash, so roots/paths match exactly.
• Output. Two self-contained AirbenderVerifierInput CBOR blobs (airbender_split_input_{N}_a.cbor / _b.cbor).

Correctness self-checks

Two root checks bracket the reconstruction and fail loudly rather than emitting a bad witness:

1. reconstructed N-1 root == N's previous_batch_hash;
2. post-B root == N's committed root hash.

Scope / follow-ups

• Commitment chaining for piece B (computing piece A's synthetic Airbender commitment) is gated behind --commitment-chaining. Off by default, B is emitted with commitment_input = None, which is enough to verify each half fits Airbender's geometry — the immediate goal. The full L1BatchCommitment assembly for the intermediate batch is the one piece left for a follow-up (clearly isolated in commitment.rs).
• Validation: the binary builds and is type-checked; the next step is a run on a real heavy batch to exercise the root self-checks (empirical proof the reconstruction is exact). Not yet run against live data.

See core/bin/batch_splitter/README.md for the full design.

Usage

batch_splitter --l1-batch <N> --database-url <pg> --artifacts-path <object-store> --l2-chain-id <id> [--commitment-chaining]

🤖 Generated with Claude Code