Guarded parallel comparison for fusion trees

Each sketch occupies b bits, followed by one guard bit. Multiplication replicates the query into every field, and subtraction compares all fields without borrowing between fields. This is the packed comparison step of the fusion node in [FW93], following the authoritative MIT 6.851 Spring 2021 lecture 12 notes, rather than the accompanying scribe notes: https://courses.csail.mit.edu/6.851/spring21/lectures/L12.pdf.

Main definitions

• packedNode: guarded sketches, in little-endian field order.
• queryMultiplier: replicates a query by multiplication.
• packedDifference: simultaneous guarded subtraction.

Main results

• packedDifference_field: each result field is exactly its guarded scalar difference.
• packedDifference_guard: the guard is set exactly when the query is at most the sketch.
• parallelCompare_exec: two actual standard-basis instructions produce the raw comparison.

References

• M. L. Fredman and D. E. Willard, Surpassing the information theoretic bound with fusion trees

def Cslib.Algorithms.WordRAM.FusionTree.packedNode (b n : ℕ) (s : ℕ → ℕ) : ℕ

Guarded sketches; field i has value 2 ^ b + s i and width b + 1.

def Cslib.Algorithms.WordRAM.FusionTree.queryMultiplier (b n : ℕ) : ℕ

Multiplying by this constant replicates the query into every field.

def Cslib.Algorithms.WordRAM.FusionTree.packedDifference (b n : ℕ) (s : ℕ → ℕ) (q : ℕ) : ℕ

The raw subtraction result; extracting a rank is a separate computation.

theorem Cslib.Algorithms.WordRAM.FusionTree.packedNode_eq_sum (b n : ℕ) (s : ℕ → ℕ) : packedNode b n s = ∑ i ∈ Finset.range n, (2 ^ b + s i) * 2 ^ ((b + 1) * i)

The node's fields start at bit positions (b + 1) * i.

theorem Cslib.Algorithms.WordRAM.FusionTree.queryMultiplier_eq_sum (b n : ℕ) : queryMultiplier b n = ∑ i ∈ Finset.range n, 2 ^ ((b + 1) * i)

The replication constant has one bit at the beginning of each field.

theorem Cslib.Algorithms.WordRAM.FusionTree.query_mul_multiplier (b n q : ℕ) : q * queryMultiplier b n = BitString.packRadix (2 ^ (b + 1)) n fun (x : ℕ) => q

Replication is a positional sum, not an extra word-RAM primitive.

theorem Cslib.Algorithms.WordRAM.FusionTree.query_mul_multiplier_le_packedNode {b n q : ℕ} (s : ℕ → ℕ) (hq : q < 2 ^ b) : q * queryMultiplier b n ≤ packedNode b n s

The replicated query is at most the guarded node: the subtraction never truncates.

theorem Cslib.Algorithms.WordRAM.FusionTree.packedDifference_add_query {b n q : ℕ} (s : ℕ → ℕ) (hq : q < 2 ^ b) : packedDifference b n s q + q * queryMultiplier b n = packedNode b n s

The raw subtraction is an exact natural-number difference.

theorem Cslib.Algorithms.WordRAM.FusionTree.packedDifference_eq {b n q : ℕ} (s : ℕ → ℕ) (hq : q < 2 ^ b) : packedDifference b n s q = BitString.packRadix (2 ^ (b + 1)) n fun (i : ℕ) => 2 ^ b + s i - q

Subtraction is fieldwise: guards prevent any borrow between adjacent sketches.

theorem Cslib.Algorithms.WordRAM.FusionTree.packedDifference_field {b n q i : ℕ} (s : ℕ → ℕ) (hs : ∀ j < n, s j < 2 ^ b) (hq : q < 2 ^ b) (hi : i < n) : packedDifference b n s q / 2 ^ ((b + 1) * i) % 2 ^ (b + 1) = 2 ^ b + s i - q

Each field of the simultaneous subtraction is the guarded scalar difference.

theorem Cslib.Algorithms.WordRAM.FusionTree.packedDifference_testBit {b n q i j : ℕ} (s : ℕ → ℕ) (hs : ∀ k < n, s k < 2 ^ b) (hq : q < 2 ^ b) (hi : i < n) (hj : j < b + 1) : (packedDifference b n s q).testBit (j + (b + 1) * i) = (2 ^ b + s i - q).testBit j

Every bit of a field agrees with the corresponding bit of its scalar difference.

theorem Cslib.Algorithms.WordRAM.FusionTree.packedDifference_guard {b n q i : ℕ} (s : ℕ → ℕ) (hs : ∀ j < n, s j < 2 ^ b) (hq : q < 2 ^ b) (hi : i < n) : (packedDifference b n s q).testBit (b + (b + 1) * i) = decide (q ≤ s i)

The guard of field i records q ≤ s i. Sortedness is unnecessary for this step.

theorem Cslib.Algorithms.WordRAM.FusionTree.packedNode_lt {b n : ℕ} (s : ℕ → ℕ) (hs : ∀ i < n, s i < 2 ^ b) : packedNode b n s < 2 ^ ((b + 1) * n)

The precomputed node fits the total field width.

theorem Cslib.Algorithms.WordRAM.FusionTree.queryMultiplier_lt (b n : ℕ) : queryMultiplier b n < 2 ^ ((b + 1) * n)

The multiplier fits even for zero sketches.

theorem Cslib.Algorithms.WordRAM.FusionTree.query_mul_multiplier_lt {b n q : ℕ} (hq : q < 2 ^ b) : q * queryMultiplier b n < 2 ^ ((b + 1) * n)

The actual multiplication intermediate fits the total field width.

theorem Cslib.Algorithms.WordRAM.FusionTree.packedDifference_lt {b n q : ℕ} (s : ℕ → ℕ) (hs : ∀ i < n, s i < 2 ^ b) : packedDifference b n s q < 2 ^ ((b + 1) * n)

The subtraction result fits, so checked overflow needs no modular wraparound.

def Cslib.Algorithms.WordRAM.FusionTree.parallelCompareCode : WordRAM.Code WordRAM.Basis.standard 5

Two fixed standard-basis instructions. Inputs are query in register 0, guarded node in 1, and multiplier in 2. Register 3 receives the replicated query, and 4 the raw guarded result. Precomputing/loading the node and multiplier, and converting the result to a rank, are separate. In particular, this fragment does not assume a unit-cost most-significant-bit operation.

def Cslib.Algorithms.WordRAM.FusionTree.parallelCompareResult (x : WordRAM.Data 5) (b n : ℕ) (s : ℕ → ℕ) (q : ℕ) : WordRAM.Data 5

The concrete final data, preserving memory and all three input registers.

theorem Cslib.Algorithms.WordRAM.FusionTree.parallelCompareResult_mem (x : WordRAM.Data 5) (b n : ℕ) (s : ℕ → ℕ) (q : ℕ) : (parallelCompareResult x b n s q).mem = x.mem

All memory is preserved.

theorem Cslib.Algorithms.WordRAM.FusionTree.parallelCompareResult_guard {b n q i : ℕ} (s : ℕ → ℕ) (x : WordRAM.Data 5) (hs : ∀ j < n, s j < 2 ^ b) (hq : q < 2 ^ b) (hi : i < n) : ((parallelCompareResult x b n s q).regs 4).testBit (b + (b + 1) * i) = decide (q ≤ s i)

The output register's guards are the simultaneous comparison answers.

theorem Cslib.Algorithms.WordRAM.FusionTree.parallelCompare_exec {w b n q : ℕ} (s : ℕ → ℕ) (x : WordRAM.Data 5) (hs : ∀ i < n, s i < 2 ^ b) (hq : q < 2 ^ b) (hw : (b + 1) * n ≤ w) (hxq : x.regs 0 = q) (hxn : x.regs 1 = packedNode b n s) (hxm : x.regs 2 = queryMultiplier b n) : WordRAM.Exec w parallelCompareCode x (parallelCompareResult x b n s q) 2

Actual checked-overflow execution in exactly two instructions, from arbitrary memory. The total packed width must fit a word; input delivery is the caller's responsibility.