The affine hash family

For a finite field F and finite types m and n, the affine maps x ↦ A x + b from n → F to m → F, with seed a matrix A and a vector b (Cslib.Probability.affineHash), form a pairwise independent hash family (Cslib.Probability.isPairwiseIndependentHash_affineHash): the map A ↦ A x₁ - A x₂ is onto for x₁ ≠ x₂, so the shift criterion Cslib.Probability.isPairwiseIndependentHash_add_of_surjective applies. Over F = ZMod 2 these are the affine maps of bit vectors used for the set lower bound protocol and in the lemma of Valiant and Vazirani; the linear maps x ↦ A x over ZMod 2 form one of the universal classes of Carter and Wegman [CW79].

Main definitions

• Cslib.Probability.affineHash: the affine map x ↦ A x + b with seed (A, b).

Main results

• Cslib.Probability.isPairwiseIndependentHash_affineHash: the affine maps over a finite field form a pairwise independent hash family.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 8.2
• J. L. Carter, M. N. Wegman, Universal classes of hash functions

def Cslib.Probability.affineHash {F : Type u_1} {m : Type u_2} {n : Type u_3} [NonUnitalNonAssocSemiring F] [Fintype n] (p : Matrix m n F × (m → F)) (x : n → F) : m → F

The affine map x ↦ A x + b from n → F to m → F, with seed (A, b).

@[simp]

theorem Cslib.Probability.affineHash_apply {F : Type u_1} {m : Type u_2} {n : Type u_3} [NonUnitalNonAssocSemiring F] [Fintype n] (A : Matrix m n F) (b : m → F) (x : n → F) : affineHash (A, b) x = A.mulVec x + b

The affine map with seed (A, b) sends x to A x + b.

theorem Cslib.Probability.isPairwiseIndependentHash_affineHash {F : Type u_1} {m : Type u_2} {n : Type u_3} [Field F] [Fintype F] [DecidableEq F] [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] : IsPairwiseIndependentHash affineHash

The affine hash family is pairwise independent: over a finite field F, the affine maps x ↦ A x + b from n → F to m → F, for a uniformly random matrix A and vector b, form a pairwise independent hash family. By the shift criterion it suffices that for x₁ ≠ x₂ the matrices A reach every difference A x₁ - A x₂.