A linearly packed tree of bit sums

A balanced addition tree counts a block of bits. Its level j contains counts of blocks of 2^j bits, and each such count fits in j+1 bits. The bit planes of every level fit together in fewer than four times the number of leaves. Their addresses use only shifts and additions.

Main definitions

• Cslib.BitString.sumTree: the sum at a node of the balanced tree.
• Cslib.BitString.sumTreeAddress: a bit-plane address within the packed tree.
• Cslib.BitString.sumTreeBits: the packed bit planes of the tree, read by address.
• Cslib.BitString.sumTreeWords: the packed bit planes stored in eight words of h bits.

Main results

• Cslib.BitString.sumTree_eq_sum: the tree counts its specified block.
• Cslib.BitString.sumTree_testBit: the root counts the set bits of a natural number.
• Cslib.BitString.sumTreeAddress_injective: distinct valid node bits have distinct addresses.

References

• N. Immerman, Descriptive Complexity, Lemma 1.18 (Bit Sum Lemma). This balanced-tree packing is a variant of the packed running-sum construction there.

def Cslib.BitString.sumTree (f : ℕ → Bool) : ℕ → ℕ → ℕ

The number of true bits in the block at level j, node q.

theorem Cslib.BitString.sumTree_le (f : ℕ → Bool) (j q : ℕ) : sumTree f j q ≤ 2 ^ j

A level-j node counts at most 2^j bits.

theorem Cslib.BitString.sumTree_lt (f : ℕ → Bool) (j q : ℕ) : sumTree f j q < 2 ^ (j + 1)

Each count occupies at most j+1 bits, including the all-one block.

theorem Cslib.BitString.sumTree_eq_sum (f : ℕ → Bool) (j q : ℕ) : sumTree f j q = ∑ i ∈ Finset.range (2 ^ j), (f (q * 2 ^ j + i)).toNat

The balanced tree counts its contiguous block, in increasing position order.

theorem Cslib.BitString.sum_testBit_eq_length_bitIndices {x k : ℕ} (hx : x < 2 ^ k) : ∑ i ∈ Finset.range k, (x.testBit i).toNat = x.bitIndices.length

Counting all the bit positions containing a numeral gives its number of set bits.

theorem Cslib.BitString.sumTree_testBit {x m : ℕ} (hx : x < 2 ^ 2 ^ m) : sumTree x.testBit m 0 = x.bitIndices.length

The root of a sufficiently deep tree counts every set bit of a natural number.

def Cslib.BitString.sumTreeAddress (m j b q : ℕ) : ℕ

Bit b of node q at level j in a tree with 2^m leaves.

theorem Cslib.BitString.sumTreeAddress_lt {m j b q : ℕ} (hj : j ≤ m) (hb : b ≤ j) (hq : q < 2 ^ (m - j)) : sumTreeAddress m j b q < 4 * 2 ^ m

All valid node bits fit in four times the number of leaves.

theorem Cslib.BitString.sumTreeAddress_injective {m j b q j' b' q' : ℕ} (hj : j ≤ m) (hb : b ≤ j) (hq : q < 2 ^ (m - j)) (hj' : j' ≤ m) (hb' : b' ≤ j') (hq' : q' < 2 ^ (m - j')) (he : sumTreeAddress m j b q = sumTreeAddress m j' b' q') : j = j' ∧ b = b' ∧ q = q'

Valid bits at different levels, nodes or bit positions never share an address.

def Cslib.BitString.sumTreeBits (f : ℕ → Bool) (m a : ℕ) : Bool

The packed bit planes of the actual addition tree, with unused positions set to zero.

theorem Cslib.BitString.sumTreeBits_address (f : ℕ → Bool) {m j b q : ℕ} (hj : j ≤ m) (hb : b ≤ j) (hq : q < 2 ^ (m - j)) : sumTreeBits f m (sumTreeAddress m j b q) = (sumTree f j q).testBit b

Reading a valid tree address returns exactly the specified node bit.

def Cslib.BitString.sumTreeWords (f : ℕ → Bool) (m h : ℕ) (r : Fin 8) : ℕ

A fixed tuple of eight h-bit words stores the tree's bit planes.

theorem Cslib.BitString.sumTreeWords_lt (f : ℕ → Bool) (m h : ℕ) (r : Fin 8) : sumTreeWords f m h r < 2 ^ h

Every packed witness is strictly less than 2^h, independently of the tree contents.

theorem Cslib.BitString.sumTreeWords_testBit (f : ℕ → Bool) (m h : ℕ) (r : Fin 8) {b : ℕ} (hb : b < h) : (sumTreeWords f m h r).testBit b = sumTreeBits f m (↑r * h + b)

Bits within a packed word have the specified global addresses.

theorem Cslib.BitString.exists_sumTreeWords_address {h a : ℕ} (ha : a < 8 * h) : ∃ (r : Fin 8) (b : Fin h), ↑r * h + ↑b = a

The eight words collectively contain every address below 8h.