Checked mask-and-multiply compression

The multiplier is supplied as three precomputed half-word digits. The query arrives as one physical word: masking and conversion to digits are part of the charged execution. The retained window fits inside the third product digit, including at odd physical widths.

Main definitions

• CompressProgram.code: a fixed standard-basis compression program.

Main results

• CompressProgram.exec: checked execution of mask-and-multiply compression.
• CompressProgram.exec_approximateSketch: execution of the arithmetic fusion sketch.

Node preprocessing and loading the constants are separate from query execution.

References

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

def Cslib.Algorithms.WordRAM.FusionTree.CompressProgram.embed (i : Fin 16) : Fin 21

Embed the multiplication workspace in the first sixteen registers.

theorem Cslib.Algorithms.WordRAM.FusionTree.CompressProgram.embed_injective : Function.Injective embed

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.CompressProgram.query : Fin 21

Query word, preserved.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.CompressProgram.positions : Fin 21

Input position mask, preserved.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.CompressProgram.retained : Fin 21

Retained output mask, preserved.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.CompressProgram.offset : Fin 21

Offset w - 2 * (w / 2), supplied by the caller and preserved.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.CompressProgram.out : Fin 21

Conversion scratch and final compressed result.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.CompressProgram.base : Fin 21

Half-word radix workspace.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.CompressProgram.a₀ : Fin 21

Lowest query digit.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.CompressProgram.a₁ : Fin 21

Middle query digit.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.CompressProgram.a₂ : Fin 21

Highest query digit.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.CompressProgram.productDigit : Fin 21

Third product digit, containing the retained window.

def Cslib.Algorithms.WordRAM.FusionTree.CompressProgram.split : WordRAM.Code WordRAM.Basis.standard 21

Mask the query and split it using division and remainder by the half-word radix. No squared radix is ever installed in a physical register.

def Cslib.Algorithms.WordRAM.FusionTree.CompressProgram.splitResult (w : ℕ) (x : WordRAM.Data 21) : WordRAM.Data 21

The exact data after query conversion, with an already initialized radix.

theorem Cslib.Algorithms.WordRAM.FusionTree.CompressProgram.exec_split {w : ℕ} (x : WordRAM.Data 21) (hx : WordRAM.Fits w (x.regs query)) (hbase : x.regs 2 = WordRAM.Multiword.radix w) : WordRAM.Exec w split x (splitResult w x) 6

theorem Cslib.Algorithms.WordRAM.FusionTree.CompressProgram.window_eq {w L p D : ℕ} (hL : L + (w - 2 * (w / 2)) ≤ w / 2) (hD : D < 2 ^ L) : (p / WordRAM.Multiword.radix w ^ 2 % WordRAM.Multiword.radix w) >>> (w - 2 * (w / 2)) &&& D = p >>> w &&& D

A masked window inside the third half-word digit depends only on that digit.

theorem Cslib.Algorithms.WordRAM.FusionTree.CompressProgram.exists_multiplier_digits {w L M : ℕ} (hL : L + (w - 2 * (w / 2)) ≤ w / 2) (hM : M < 2 ^ (w + L)) : ∃ (digits : Fin 3 → ℕ), (∀ (i : Fin 3), digits i < WordRAM.Multiword.radix w) ∧ Nat.ofDigits (WordRAM.Multiword.radix w) (List.ofFn digits) = M

A multiplier of at most w + L bits has three bounded half-word digits whenever the retained window fits. This is a preprocessing representation theorem; loading is separate.

def Cslib.Algorithms.WordRAM.FusionTree.CompressProgram.code : WordRAM.Code WordRAM.Basis.standard 21

Initialize the radix, convert the query, multiply three digits by three digits, and extract the retained window. Registers 7--9 contain the precomputed multiplier digits.

theorem Cslib.Algorithms.WordRAM.FusionTree.CompressProgram.size_code : code.size = 94

theorem Cslib.Algorithms.WordRAM.FusionTree.CompressProgram.exec {w L M : ℕ} (hw : 2 ≤ w) (x : WordRAM.Data 21) (hx : WordRAM.Fits w (x.regs query)) (hb : WordRAM.Multiword.Bounded (WordRAM.Multiword.radix w) (WordRAM.Data.comap embed x) (WordRAM.Multiword.Schoolbook.rightRegs 3 3)) (hM : WordRAM.Multiword.value (WordRAM.Multiword.radix w) (WordRAM.Data.comap embed x) (WordRAM.Multiword.Schoolbook.rightRegs 3 3) = M) (ho : x.regs offset = w - 2 * (w / 2)) (hD : x.regs retained < 2 ^ L) (hL : L + (w - 2 * (w / 2)) ≤ w / 2) : ∃ (y : WordRAM.Data 21), WordRAM.Exec w code x y 94 ∧ y.regs out = ((x.regs query &&& x.regs positions) * M) >>> w &&& x.regs retained ∧ y.mem = x.mem ∧ ∀ (i : Fin 21), 7 ≤ ↑i ∧ ↑i < 10 ∨ 16 ≤ ↑i ∧ ↑i < 20 → y.regs i = x.regs i

In 94 checked standard instructions, compute the masked product window. The query and all node parameters are preserved, as is memory. Only registers 0--6, 10--15 and 20 may change. Multiplier digits in registers 7--9 must be preloaded; conversion of the physical query word is charged. The retained mask occupies L bits and satisfies the stated half-word window condition.

theorem Cslib.Algorithms.WordRAM.FusionTree.CompressProgram.exec_approximateSketch {w L r : ℕ} (hw : 2 ≤ w) (b m : Fin r → ℕ) (x : WordRAM.Data 21) (hx : WordRAM.Fits w (x.regs query)) (hb : WordRAM.Multiword.Bounded (WordRAM.Multiword.radix w) (WordRAM.Data.comap embed x) (WordRAM.Multiword.Schoolbook.rightRegs 3 3)) (hM : WordRAM.Multiword.value (WordRAM.Multiword.radix w) (WordRAM.Data.comap embed x) (WordRAM.Multiword.Schoolbook.rightRegs 3 3) = Lean.FusionTree.positionMask m) (hC : x.regs positions = Lean.FusionTree.positionMask b) (hD : x.regs retained = Lean.FusionTree.positionMask fun (i : Fin r) => b i + m i - w) (ho : x.regs offset = w - 2 * (w / 2)) (hwidth : (Lean.FusionTree.positionMask fun (i : Fin r) => b i + m i - w) < 2 ^ L) (hL : L + (w - 2 * (w / 2)) ≤ w / 2) : ∃ (y : WordRAM.Data 21), WordRAM.Exec w code x y 94 ∧ y.regs out = Lean.FusionTree.approximateSketch w b m (x.regs query) ∧ y.mem = x.mem ∧ ∀ (i : Fin 21), 7 ≤ ↑i ∧ ↑i < 10 ∨ 16 ≤ ↑i ∧ ↑i < 20 → y.regs i = x.regs i

Specialize the actual execution to the arithmetic approximate sketch. The collision-free parameter construction and comparison theorem are independent of this execution theorem. The caller supplies the position and retained masks and three multiplier digits.