Composing compression and packed ranks

All transfers into the two fixed workspaces are charged. Only the actual loaded header values supply node-dependent constants. The caller's registers and all memory are framed.

Main definitions

• NodeProgram.compressionInputs, NodeProgram.compress: workspace transfers and multiplier compression routine.
• NodeProgram.rankInputs, NodeProgram.rank, NodeProgram.sketchCut, NodeProgram.sketchQuery: workspace transfers, packed-rank routine, mathematical sketch cut, and combined compression-plus-rank query.

Main results

• NodeProgram.exec_compress: a bounded word is compressed in 102 instructions.
• NodeProgram.exec_rank: a compressed query is ranked in 17 instructions.

References

• [FW93]

def Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.compressionInputs : List (Fin registers × Fin registers)

Seven charged transfers into the compression workspace.

def Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.compress : WordRAM.Code WordRAM.Basis.standard registers

Prepare the compression workspace and run the actual multiplier program.

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.exec_compress {w n q : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) (hw : 2 ≤ w) (hn : 0 < n) (hnB : n ≤ Lean.FusionTree.branching w) (hlarge : 9 ≤ Nat.log 2 w) (x : WordRAM.Data registers) (hx : Prepared p x) (hq : WordRAM.Fits w q) (hxq : x.regs argument = q) : ∃ (y : WordRAM.Data registers), WordRAM.Exec w compress x y 102 ∧ y.regs (compressBank 20) = p.compressed q ∧ Frame x y

Seven transfers plus the terminal self-copy and 94 arithmetic instructions.

def Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.rankInputs (strict : Bool) : List (Fin registers × Fin registers)

Transfer a compressed query and seven stored constants to a packed-rank workspace. The Boolean selects strict rank (original packed sketches) or inclusive rank (complements).

def Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.rank (strict : Bool) : WordRAM.Code WordRAM.Basis.standard registers

Eight charged transfers followed by the chosen eight-instruction rank program.

def Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.sketchCut {n : ℕ} (strict : Bool) (w : ℕ) (keys : Fin n → ℕ) (q : ℕ) : ℕ

Perfect-sketch comparison count with the chosen convention.

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.exec_rank {w n q : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) (strict : Bool) (hn : 0 < n) (hs : StrictMono keys) (hk : ∀ (i : Fin n), keys i < 2 ^ w) (hnB : n ≤ Lean.FusionTree.branching w) (hlarge : 9 ≤ Nat.log 2 w) (x : WordRAM.Data registers) (hx : Prepared p x) (hxq : x.regs (compressBank 20) = p.compressed q) : ∃ (y : WordRAM.Data registers), WordRAM.Exec w (rank strict) x y 17 ∧ y.regs (rankBank 9) = sketchCut strict w keys q ∧ Frame x y

The rank call includes every transfer and preserves the caller and memory.

def Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.sketchQuery (strict : Bool) : WordRAM.Code WordRAM.Basis.standard registers

Compression followed by the requested sketch-rank convention.

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.exec_sketchQuery {w n q : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) (strict : Bool) (hw : 2 ≤ w) (hn : 0 < n) (hs : StrictMono keys) (hk : ∀ (i : Fin n), keys i < 2 ^ w) (hnB : n ≤ Lean.FusionTree.branching w) (hlarge : 9 ≤ Nat.log 2 w) (x : WordRAM.Data registers) (hx : Prepared p x) (hq : WordRAM.Fits w q) (hxq : x.regs argument = q) : ∃ (y : WordRAM.Data registers), WordRAM.Exec w (sketchQuery strict) x y 119 ∧ y.regs (rankBank 9) = sketchCut strict w keys q ∧ Frame x y

A complete sketch query, including all register transfers, takes 119 instructions.