Most-significant-bit arithmetic for fusion trees

The arithmetic expressions use multiplication, subtraction, Boolean operations and shifts. Their correctness is distinct from execution on a bounded-word RAM: the intermediate products need multiple physical words. The construction follows pages 7–8 of the MIT 6.851 Spring 2021 lecture 12 notes, https://courses.csail.mit.edu/6.851/spring21/lectures/L12.pdf.

Main definitions

• powerFlags: parallel comparisons against consecutive powers of two.
• smallMSB: count the successful comparisons and subtract one.
• clusterSummary: compress the nonzero-cluster markers by multiplication.
• widthMSB: two comparison/count stages for arbitrary input widths.

Main results

• smallMSB_eq_log2: correctness without a most-significant-bit primitive.
• clusterMarkers_guard: exact nonzero detection, without intercluster borrowing.
• widthMSB_eq_log2: full arithmetic correctness, including zero and nonsquare widths.
• widthMSB_virtual_bounds: all recorded arithmetic intermediates fit in 6w bits.

References

• Fredman and Willard, Surpassing the information theoretic bound with fusion trees.

def Cslib.Algorithms.WordRAM.FusionTree.MSB.ones (s : ℕ) : ℕ

One at the low bit of each of s fields of width s + 1.

def Cslib.Algorithms.WordRAM.FusionTree.MSB.powers (s : ℕ) : ℕ

Field i contains the comparison threshold 2 ^ i.

def Cslib.Algorithms.WordRAM.FusionTree.MSB.guards (s : ℕ) : ℕ

A guard bit at the top of every field.

def Cslib.Algorithms.WordRAM.FusionTree.MSB.powerFlags (s z : ℕ) : ℕ

Simultaneously compare z with every 2 ^ i, for i < s. The output has a zero-or-one digit in every radix-2^(s+1) field.

def Cslib.Algorithms.WordRAM.FusionTree.MSB.powerCount (s z : ℕ) : ℕ

Multiplication counts the successful power-of-two comparisons.

def Cslib.Algorithms.WordRAM.FusionTree.MSB.smallMSB (s z : ℕ) : ℕ

Most-significant set bit for a positive input of at most s bits. The expression contains no logarithm or bit-search operation; constants depend only on s.

theorem Cslib.Algorithms.WordRAM.FusionTree.MSB.powerFlags_eq {s z : ℕ} (hz : z < 2 ^ s) : powerFlags s z = BitString.packRadix (2 ^ (s + 1)) s fun (i : ℕ) => (decide (2 ^ i ≤ z)).toNat

The comparison expression has exactly the promised Boolean digits; subtraction does not borrow between fields and no correctness oracle is a hypothesis.

theorem Cslib.Algorithms.WordRAM.FusionTree.MSB.powerCount_eq {s z : ℕ} (hs : 0 < s) (hz : z < 2 ^ s) : powerCount s z = ∑ i ∈ Finset.range s, (decide (2 ^ i ≤ z)).toNat

Counting the packed flags gives the number of powers of two at most the input.

theorem Cslib.Algorithms.WordRAM.FusionTree.MSB.smallMSB_eq_log2 {s z : ℕ} (hz0 : 0 < z) (hz : z < 2 ^ s) : smallMSB s z = z.log2

For nonzero inputs, the comparison/count arithmetic returns the highest set-bit index. Nat.log2 occurs only in the specification and proof.

def Cslib.Algorithms.WordRAM.FusionTree.MSB.clusterMask (s : ℕ) : ℕ

The most significant bit of each of s clusters, each s bits wide.

def Cslib.Algorithms.WordRAM.FusionTree.MSB.clusterMarkers (s x : ℕ) : ℕ

Set a cluster's marker exactly when the cluster is nonempty. The original high bits are separated before subtraction, preventing borrows between clusters.

def Cslib.Algorithms.WordRAM.FusionTree.MSB.compressionShift (s j : ℕ) : ℕ

Shifts moving diagonal marker products to positions s² + i.

def Cslib.Algorithms.WordRAM.FusionTree.MSB.compressionMultiplier (s : ℕ) : ℕ

Precomputed multiplier for the cluster markers.

def Cslib.Algorithms.WordRAM.FusionTree.MSB.clusterSummary (s x : ℕ) : ℕ

One bit per nonempty cluster, computed by multiply, shift, and mask. The final mask removes the off-diagonal multiplication terms.

theorem Cslib.Algorithms.WordRAM.FusionTree.MSB.clusterMarkers_guard {s x i : ℕ} (hs : 0 < s) (hx : x < 2 ^ (s * s)) (hi : i < s) : (clusterMarkers s x).testBit (s - 1 + s * i) = decide (x / 2 ^ (s * i) % 2 ^ s ≠ 0)

Every marker is set precisely when its original cluster is nonzero. This includes clusters whose only set bit was already at the marker position.

theorem Cslib.Algorithms.WordRAM.FusionTree.MSB.clusterSummary_eq {s : ℕ} (hs : 0 < s) (x : ℕ) : clusterSummary s x = ∑ i : Fin s, ((clusterMarkers s x).testBit (s - 1 + ↑i * s)).toNat * 2 ^ ↑i

The masked product compresses exactly the original cluster-marker bits. Cross terms are collision-free everywhere, including outside the final retained interval.

theorem Cslib.Algorithms.WordRAM.FusionTree.MSB.clusterSummary_lt (s x : ℕ) : clusterSummary s x < 2 ^ s

The compressed summary fits in s bits, including for an empty input.

theorem Cslib.Algorithms.WordRAM.FusionTree.MSB.clusterSummary_testBit {s x i : ℕ} (hs : 0 < s) (hx : x < 2 ^ (s * s)) (hi : i < s) : (clusterSummary s x).testBit i = decide (x / 2 ^ (s * i) % 2 ^ s ≠ 0)

A summary bit is set exactly when the corresponding original cluster is nonzero.

theorem Cslib.Algorithms.WordRAM.FusionTree.MSB.clusterSummary_log2 {s x : ℕ} (hs : 0 < s) (hx0 : 0 < x) (hx : x < 2 ^ (s * s)) : 0 < clusterSummary s x ∧ (clusterSummary s x).log2 = x.log2 / s

The first comparison/count stage identifies the highest nonempty cluster.

def Cslib.Algorithms.WordRAM.FusionTree.MSB.msb (s x : ℕ) : ℕ

Two parallel power-comparison/count stages, with extraction of the selected cluster. The value for zero is explicitly zero. All constants depend only on s.

theorem Cslib.Algorithms.WordRAM.FusionTree.MSB.msb_eq_log2 {s x : ℕ} (hs : 0 < s) (hx : x < 2 ^ (s * s)) : msb s x = x.log2

Full arithmetic correctness for s clusters of s bits. This theorem assumes only the input bound and positive cluster width, not correctness of any algorithmic stage.

def Cslib.Algorithms.WordRAM.FusionTree.MSB.clusterSize (w : ℕ) : ℕ

Ceiling of the square root, with zero width assigned zero clusters. This is a width-dependent preprocessing constant, not a run-time square-root instruction.

theorem Cslib.Algorithms.WordRAM.FusionTree.MSB.clusterSize_bounds {w : ℕ} (hw : 0 < w) : 0 < clusterSize w ∧ w ≤ clusterSize w * clusterSize w ∧ clusterSize w * clusterSize w ≤ 2 * w ∧ clusterSize w ≤ w

The cluster capacity covers nonsquare widths and uses at most twice the input width.

def Cslib.Algorithms.WordRAM.FusionTree.MSB.widthMSB (w x : ℕ) : ℕ

Width-specific MSB arithmetic, including zero and nonsquare widths.

theorem Cslib.Algorithms.WordRAM.FusionTree.MSB.widthMSB_eq_log2 {w x : ℕ} (hx : x < 2 ^ w) : widthMSB w x = x.log2

For every fitting input, the expression computes the most-significant-set-bit index; zero returns zero. No wider physical word or RAM execution is asserted here.

def Cslib.Algorithms.WordRAM.FusionTree.MSB.powerStageValues (s z : ℕ) : List ℕ

Every arithmetic value in one powers-of-two comparison/count stage. This records intermediates before masking or shifting, so oversized products cannot be hidden.

theorem Cslib.Algorithms.WordRAM.FusionTree.MSB.powerStageValues_lt {s z : ℕ} (hs : 0 < s) (hz : z < 2 ^ s) (a : ℕ) : a ∈ powerStageValues s z → a < 2 ^ (2 * (s + 1) * s)

The largest power-stage intermediate needs at most twice the packed field width. This is a bound in bits, not permission to use a larger physical RAM word.

def Cslib.Algorithms.WordRAM.FusionTree.MSB.clusterStageValues (s x : ℕ) : List ℕ

Every arithmetic value in marking and compressing the clusters, including the full product before shifting and masking.

theorem Cslib.Algorithms.WordRAM.FusionTree.MSB.clusterStageValues_lt {s x : ℕ} (hs : 0 < s) (hx : x < 2 ^ (s * s)) (a : ℕ) : a ∈ clusterStageValues s x → a < 2 ^ (2 * (s * s) + s)

The marking/compression stage needs at most 2s² + s bits for every value, including its full multiplication intermediate.

theorem Cslib.Algorithms.WordRAM.FusionTree.MSB.smallMSB_lt {s z : ℕ} (hs : 0 < s) (hz : z < 2 ^ s) : smallMSB s z < s

The small-input arithmetic returns an index below the supplied bit width, even for zero (where its saturating subtraction returns zero).

theorem Cslib.Algorithms.WordRAM.FusionTree.MSB.widthMSB_virtual_bounds {w x : ℕ} (hw : 0 < w) (hx : x < 2 ^ w) : have s := clusterSize w; have z := clusterSummary s x; have c := smallMSB s z; have v := x >>> (c * s) &&& 2 ^ s - 1; (∀ a ∈ clusterStageValues s x, a < 2 ^ (6 * w)) ∧ (∀ a ∈ powerStageValues s z, a < 2 ^ (6 * w)) ∧ (∀ a ∈ powerStageValues s v, a < 2 ^ (6 * w)) ∧ c * s < 2 ^ (6 * w) ∧ widthMSB w x < 2 ^ (6 * w)

Every value in both comparison/count stages and the marking/compression stage fits in 6w virtual bits. These bounds support a future multiword implementation; they do not claim execution with a 6w-bit physical word.