Affine hashing of bit strings

The affine maps x ↦ A x + b of bit strings, with a Boolean matrix A of k rows given by its rows and an offset b (Cslib.BitString.LinearHash.affineHash), form a pairwise independent hash family (Cslib.BitString.LinearHash.isPairwiseIndependentHash_affineHash): masking the two-universal linear family Cslib.BitString.LinearHash.hash with a uniformly random offset satisfies the shift criterion Cslib.Probability.isPairwiseIndependentHash_add_of_surjective. This is the family of the set lower bound protocol of Goldwasser and Sipser [GS86] Arora and Barak, Section 8.2 and of the lemma of Valiant and Vazirani [VV86]. It is the affine hash Cslib.Probability.affineHash over Bool (Cslib.BitString.LinearHash.affineHash_eq_affineHash), whose pairwise independence is proved over fields; Mathlib has no Field Bool instance, so it is proved here separately.

Main definitions

• Cslib.BitString.LinearHash.affineHash: the affine map x ↦ A x + b of bit strings.

Main results

• Cslib.BitString.LinearHash.affineHash_eq_affineHash: it is the affine hash over Bool.
• Cslib.BitString.LinearHash.isPairwiseIndependentHash_affineHash: affine hashing of bit strings is pairwise independent.

References

• S. Goldwasser, M. Sipser, Private coins versus public coins in interactive proof systems
• L. G. Valiant, V. V. Vazirani, NP is as easy as detecting unique solutions
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

def Cslib.BitString.LinearHash.affineHash {k n : ℕ} (seed : (Fin k → BitString n) × BitString k) (x : BitString n) : BitString k

The affine map x ↦ A x + b of bit strings, with seed the k rows of the matrix A and the offset b.

theorem Cslib.BitString.LinearHash.affineHash_eq_affineHash {k n : ℕ} (seed : (Fin k → BitString n) × BitString k) (x : BitString n) : affineHash seed x = Probability.affineHash seed x

Affine hashing of bit strings is the affine hash Cslib.Probability.affineHash over Bool, with the rows as bit strings.

theorem Cslib.BitString.LinearHash.isPairwiseIndependentHash_affineHash (k n : ℕ) : Probability.IsPairwiseIndependentHash affineHash

Affine hashing of bit strings is pairwise independent: for distinct inputs, the difference of the linear hashes is the linear hash of a nonzero difference, which takes every value.