Packed sketch ranks

Guard extraction and multiplication count all simultaneous comparisons. Complementing the sketches reverses the comparison to obtain inclusive ranks. None of these operations assumes a most-significant-bit primitive. Node constants must be precomputed and loaded separately.

Main definitions

• guardMask, guardFlags: extract one zero-or-one digit from each guarded comparison.
• upperRankExpr: inclusive rank using complemented sketches.

Main results

• guardFlags_eq: exact packed Boolean comparison digits.
• upperRankExpr_eq_card: the resulting inclusive rank.
• RankProgram.exec: eight actual checked instructions return the inclusive rank.

References

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

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

One guard bit per field, with all other bits zero.

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

theorem Cslib.Algorithms.WordRAM.FusionTree.guardMask_testBit (b n k : ℕ) : (guardMask b n).testBit k = true ↔ ∃ i ∈ Finset.range n, b + (b + 1) * i = k

The guard mask has no other set bits.

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

Move each comparison's guard to the lowest bit of its radix field.

theorem Cslib.Algorithms.WordRAM.FusionTree.guardFlags_eq {b n q : ℕ} (s : ℕ → ℕ) (hs : ∀ i < n, s i < 2 ^ b) (hq : q < 2 ^ b) : guardFlags b n s q = BitString.packRadix (2 ^ (b + 1)) n fun (i : ℕ) => (decide (q ≤ s i)).toNat

Guard extraction returns exactly the packed zero-or-one comparison digits.

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

Count all set comparison guards through the middle field of one product.

theorem Cslib.Algorithms.WordRAM.FusionTree.countGuards_eq {b n q : ℕ} (s : ℕ → ℕ) (hn : 0 < n) (hb : n < 2 ^ (b + 1)) (hs : ∀ i < n, s i < 2 ^ b) (hq : q < 2 ^ b) : countGuards b n s q = ∑ i ∈ Finset.range n, (decide (q ≤ s i)).toNat

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

An inclusive sketch rank, obtained by complementing both sides of each comparison.

theorem Cslib.Algorithms.WordRAM.FusionTree.upperRankExpr_eq_card {b n q : ℕ} (s : ℕ → ℕ) (hn : 0 < n) (hb : n < 2 ^ (b + 1)) (hs : ∀ i < n, s i < 2 ^ b) (hq : q < 2 ^ b) : upperRankExpr b n s q = {i ∈ Finset.range n | s i ≤ q}.card

The expression returns the number of sketches at or below the query. Sortedness is unnecessary for the arithmetic identity; a tree uses sorted sketches to interpret the rank.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.RankProgram.query : Fin 10

Query sketch.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.RankProgram.node : Fin 10

Packed guarded complements of the stored sketches.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.RankProgram.copies : Fin 10

Replication multiplier.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.RankProgram.guards : Fin 10

Mask selecting all guard bits.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.RankProgram.bits : Fin 10

Number of payload bits per field.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.RankProgram.middle : Fin 10

Power selecting the count product's middle digit.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.RankProgram.base : Fin 10

Field radix.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.RankProgram.maximum : Fin 10

Largest possible payload.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.RankProgram.temp : Fin 10

Replicated complemented query.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.RankProgram.out : Fin 10

Scratch register and final inclusive rank.

def Cslib.Algorithms.WordRAM.FusionTree.RankProgram.code : WordRAM.Code WordRAM.Basis.standard 10

Eight standard instructions compute the complete inclusive sketch rank. All eight input registers and all memory are preserved. The precomputed constants are supplied by the caller.

def Cslib.Algorithms.WordRAM.FusionTree.RankProgram.result (x : WordRAM.Data 10) (b n : ℕ) (s : ℕ → ℕ) (q : ℕ) : WordRAM.Data 10

The exact final data, retaining the intermediate temporary register.

theorem Cslib.Algorithms.WordRAM.FusionTree.RankProgram.exec {w b n q : ℕ} (s : ℕ → ℕ) (x : WordRAM.Data 10) (hn : 0 < n) (hb : n < 2 ^ (b + 1)) (hs : ∀ i < n, s i < 2 ^ b) (hq : q < 2 ^ b) (hw : 2 * ((b + 1) * n) ≤ w) (hxq : x.regs query = q) (hxn : x.regs node = packedNode b n fun (i : ℕ) => 2 ^ b - 1 - s i) (hxc : x.regs copies = queryMultiplier b n) (hxg : x.regs guards = guardMask b n) (hxb : x.regs bits = b) (hxm : x.regs middle = 2 ^ ((b + 1) * (n - 1))) (hxr : x.regs base = 2 ^ (b + 1)) (hxmax : x.regs maximum = 2 ^ b - 1) : WordRAM.Exec w code x (result x b n s q) 8 ∧ (result x b n s q).regs out = {i ∈ Finset.range n | s i ≤ q}.card ∧ (result x b n s q).mem = x.mem

Checked execution of the full inclusive rank in eight instructions. The packed word occupies at most half the physical width, making the count multiplication legal too. Construction/loading of the node constants and compressed query remain separate.