Counting packed flags on the word RAM

Three checked instructions count packed zero-or-one fields, using a replication constant, middle-field divisor, and radix supplied in registers. Keeping the packed input below half the physical word width makes the entire multiplication legal. Loading and constructing these constants is separate from the fragment.

Main definitions

• Cslib.WordRAM.PackedCount.code: multiplication, division, and remainder.

Main results

• Cslib.WordRAM.PackedCount.exec: the actual instruction count and exact answer.

References

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

@[reducible, inline]

abbrev Cslib.WordRAM.PackedCount.flags : Fin 5

Packed input flags.

@[reducible, inline]

abbrev Cslib.WordRAM.PackedCount.ones : Fin 5

The all-ones radix word.

@[reducible, inline]

abbrev Cslib.WordRAM.PackedCount.divisor : Fin 5

The power selecting the middle field.

@[reducible, inline]

abbrev Cslib.WordRAM.PackedCount.base : Fin 5

Field radix.

@[reducible, inline]

abbrev Cslib.WordRAM.PackedCount.out : Fin 5

Product workspace and final count.

def Cslib.WordRAM.PackedCount.code : Code Basis.standard 5

Count packed flags with three standard word operations.

def Cslib.WordRAM.PackedCount.result (x : Data 5) : Data 5

The full final data, including the overwritten workspace register.

theorem Cslib.WordRAM.PackedCount.exec {w e n : ℕ} (f : ℕ → Bool) (x : Data 5) (hn : 0 < n) (hb : n < 2 ^ e) (hw : 2 * e * n ≤ w) (hf : x.regs flags = BitString.packRadix (2 ^ e) n fun (i : ℕ) => (f i).toNat) (ho : x.regs ones = BitString.packRadix (2 ^ e) n fun (x : ℕ) => 1) (hd : x.regs divisor = (2 ^ e) ^ (n - 1)) (hbase : x.regs base = 2 ^ e) : Exec w code x (result x) 3 ∧ (result x).regs out = ∑ i ∈ Finset.range n, (f i).toNat ∧ (result x).mem = x.mem

A fully charged count, preserving memory and all input registers. The width bound covers the product, and n < 2^e prevents carry between fields in the arithmetic identity.