Balanced MIP-8 page commitments

This file defines a variant of the MIP-8 page commitment model from commitment.v. The public input, slot normalization, pair leaves, bitmap seal, and collision statement are the same. The only algorithmic change is the merge schedule for nonempty pair leaves. In commitment.v, the compact value tree is the induced subtree of the 64-pair complete page tree: empty complete-tree regions disappear, and the surviving unary stretches do not create merge hashes. Here, after the same pair-leaf extraction step, we forget the empty regions for scheduling and recursively split the ordered active leaves at the median. Every internal node therefore combines two nonempty sublists whose lengths differ by at most one along each split. For example, with active pair indices 0, 1, 8, and 32:

induced schedule from commitment.v:

                 Node
                /    \
            Node      Leaf 32
           /    \
       Node      Leaf 8
      /    \
  Leaf 0  Leaf 1

balanced schedule in this file:

              Node
             /    \
         Node      Node
        /   \      /   \
  Leaf 0 Leaf 1 Leaf 8 Leaf 32

With an odd number of active leaves, the left side gets length / 2 leaves and the right side gets the rest:

active pair indices [0], [8], [32]:

              Node
             /    \
        Leaf 0     Node
                  /    \
             Leaf 8   Leaf 32

As in commitment.v, an empty page is sealed directly with the 128-bit slot bitmap. A nonempty page hashes each active pair leaf, hashes the balanced merge tree, and seals the tree root together with the same bitmap. The correctness property is the same binding statement, specialized to the balanced trace. If two normalized slot lists differ but their balanced roots are equal, then the two traced executions contain an aligned hash collision. The only difference is what "aligned" means for internal merge nodes: merge locations are positions in the balanced median-split tree, while leaf locations remain the original pair indices and the seal location is unchanged.

Extract the nonempty pair leaves together with their original 0-based pair positions. The positions are not used to choose the balanced merge shape; they are retained so leaf hash calls can still be aligned with the original page geometry.

Split by median. For odd lengths, the right side has one more element.

Build a balanced located tree from the ordered active pair entries. fuel is just structural recursion fuel; the exported builder below supplies length entries. Internal node locations are balanced-tree coordinates: depth counts median-split levels from the root, and index is the horizontal index at that depth.

The active leaves are pair indices 0, 1, 8, and 32. Unlike the induced tree in commitment.v, the balanced schedule merges (0,1) and (8,32) in parallel before the final root merge.

active leaves:
  pair 0  = (v0, 0)
  pair 1  = (v1, 0)
  pair 8  = (v8, 0)
  pair 32 = (v32, v32')

balanced located tree:

                    LocatedTreeNode 0 0
                   /                   \
       LocatedTreeNode 1 0       LocatedTreeNode 1 1
          /             \           /              \
 LocatedTreeLeaf   LocatedTreeLeaf LocatedTreeLeaf LocatedTreeLeaf
    0 (v0, 0)       1 (v1, 0)      8 (v8, 0)      32 (v32, v32')

The example lemma balanced_located_tree_four_leaf_demo proves that the algorithm returns exactly this balanced located tree.

With three leaves, the median split puts one leaf on the left and two on the right.

active leaves:
  pair 0  = (v0, 0)
  pair 8  = (v8, 0)
  pair 32 = (v32, v32')

balanced located tree:

                    LocatedTreeNode 0 0
                   /                   \
          LocatedTreeLeaf         LocatedTreeNode 1 1
             0 (v0, 0)              /              \
                            LocatedTreeLeaf  LocatedTreeLeaf
                               8 (v8, 0)     32 (v32, v32')

The example lemma balanced_located_tree_three_leaf_demo proves that the odd-size median split is reflected in the returned tree.

Final seal step. Empty pages are sealed by bitmap alone; nonempty pages seal the same bitmap with the balanced merge-tree root.

Trace-producing version used by the binding theorem.

Correctness

The proof follows the same strategy as commitment.v. If the seal inputs differ, root equality exposes a seal collision. If the seal inputs agree, the bitmap agrees, so both executions have the same active pair indices and hence the same balanced tree shape. The proof then compares corresponding leaves and merge nodes at their balanced locations.