Binary-matrix hashes for Count-Min tables

The existing binary linear hash family sends an n-bit item to m bits. Numbering that output with BitString.equivFin m gives a concrete universal family into Fin (2 ^ m), suitable for the stored counters of a Count-Min table. The numbering is injective, so it does not change any collision event or require a stronger randomness assumption.

A row seed consists of m * n bits. Sampling a tuple of these seeds uniformly gives the independent row seeds used by the Count-Min accuracy theorem. The seed-size statement below counts the seed space; hash evaluation and machine running times are separate obligations.

Main definitions

• Cslib.CountMin.indexedHash: binary linear hashing with a finite bucket index as output.

Main results

• Cslib.CountMin.isTwoUniversal_indexedHash: the concrete family is universal.
• Cslib.CountMin.card_indexedHash_seed: a row has 2 ^ (m * n) possible seeds.

References

• G. Cormode, S. Muthukrishnan, An Improved Data Stream Summary: The Count-Min Sketch and its Applications, Sections 3 and 4.1
• I. Haitner, S. Vadhan, The Many Entropies in One-Way Functions, Section 2.4.1, the Boolean-matrix example following Definition 4.

def Cslib.CountMin.indexedHash {n m : ℕ} (rows : Fin m → BitString n) (input : BitString n) : Fin (2 ^ m)

Hash an n-bit item to one of 2 ^ m numbered buckets using a binary m × n matrix.

@[simp]

theorem Cslib.CountMin.indexedHash_eq_iff {n m : ℕ} (rows : Fin m → BitString n) (x y : BitString n) : indexedHash rows x = indexedHash rows y ↔ BitString.LinearHash.hash rows x = BitString.LinearHash.hash rows y

Numbering the output bits leaves every collision event unchanged.

theorem Cslib.CountMin.isTwoUniversal_indexedHash (n m : ℕ) : Probability.IsTwoUniversal (Probability.PMF.uniformOfFintype (Fin m → BitString n)) indexedHash

Uniform binary matrices give a universal family of Count-Min bucket indices.

theorem Cslib.CountMin.card_indexedHash_seed (n m : ℕ) : Fintype.card (Fin m → BitString n) = 2 ^ (m * n)

A binary-matrix row seed has m * n Boolean coordinates.