Binary linear hashing

A uniformly random Boolean matrix is a two-universal family: hashing a nonzero input gives a uniform output. Prefixes of one public matrix supply every shorter hash length, including zero. The list implementation reads fixed-width rows, pads missing seed bits with false, and takes an AND/XOR fold. It reuses the existing block representation and ordinary list operations.

Main definitions

• Cslib.BitString.LinearHash.hash: matrix hashing on finite bit strings.
• Cslib.BitString.LinearHash.wordHash: its total list implementation.

Main results

• Cslib.BitString.LinearHash.isDeltaUniversalHash, Cslib.BitString.LinearHash.isTwoUniversal: the uniform matrix family is 2⁻ᵐ-XOR-universal, hence universal.
• Cslib.BitString.LinearHash.isTwoUniversal_prefix: universality with unused public rows.
• Cslib.BitString.LinearHash.wordHash_eq_ofFn: exact agreement of the two representations.

References

• I. Haitner, S. Vadhan, The Many Entropies in One-Way Functions, Section 2.4.1, the Boolean-matrix example following Definition 4.
• T. Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, Section 3.3, Lemma 1. Matrix hashing uses more seed bits than the cited field-multiplication family, while retaining polynomial seed length.

Adapted from Probability/LinearHash.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, in the shared bit-string namespace.

def Cslib.BitString.LinearHash.hash {n m : ℕ} (rows : Fin m → BitString n) (input : BitString n) : BitString m

Hash an n-bit input to m bits using the m rows of a Boolean matrix.

theorem Cslib.BitString.LinearHash.uniform_hash_nonzero {n m : ℕ} (input : BitString n) (hinput : input ≠ 0) : PMF.map (fun (rows : Fin m → BitString n) => hash rows input) (Probability.PMF.uniformOfFintype (Fin m → BitString n)) = Probability.PMF.uniformOfFintype (BitString m)

Hashing any nonzero input by a uniform matrix gives a uniform output.

theorem Cslib.BitString.LinearHash.uniform_hash_sub {n m : ℕ} (x y : BitString n) (hxy : x ≠ y) : PMF.map (fun (rows : Fin m → BitString n) => hash rows x - hash rows y) (Probability.PMF.uniformOfFintype (Fin m → BitString n)) = Probability.PMF.uniformOfFintype (BitString m)

The difference of the hashes of distinct inputs is uniform.

theorem Cslib.BitString.LinearHash.isDeltaUniversalHash (n m : ℕ) : Probability.IsDeltaUniversalHash (Probability.PMF.uniformOfFintype (Fin m → BitString n)) hash (↑(Fintype.card (BitString m)))⁻¹

Uniform Boolean matrices are a 2⁻ᵐ-Δ-universal hash family: the bitwise XOR of two hashes of distinct inputs is uniform.

theorem Cslib.BitString.LinearHash.isTwoUniversal (n m : ℕ) : Probability.IsTwoUniversal (Probability.PMF.uniformOfFintype (Fin m → BitString n)) hash

Uniform Boolean matrices are a universal hash family, including zero-width outputs.

theorem Cslib.BitString.LinearHash.isTwoUniversal_prefix {n m count : ℕ} (h : m ≤ count) : Probability.IsTwoUniversal (Probability.PMF.uniformOfFintype (Fin count → BitString n)) fun (rows : Fin count → BitString n) => hash (rows ∘ Fin.castLE h)

Prefixes of one public matrix give universal hashes at every shorter output length.

theorem Cslib.BitString.LinearHash.isTwoUniversal_flat (inputBits outputBits : ℕ) : Probability.IsTwoUniversal (Probability.PMF.uniformOfFintype (BitString (outputBits * inputBits))) fun (seed : BitString (outputBits * inputBits)) => hash (blocksEquiv seed)

A uniformly sampled flat matrix gives the usual two-universal family.

def Cslib.BitString.LinearHash.wordHash (count : ℕ) (seed input : List Bool) : List Bool

A word implementation of binary matrix hashing. Missing seed bits are zero.

@[simp]

theorem Cslib.BitString.LinearHash.length_wordHash (count : ℕ) (seed input : List Bool) : (wordHash count seed input).length = count

Every row contributes one output bit, including when the input has length zero.

theorem Cslib.BitString.LinearHash.wordHash_eq_ofFn {n m : ℕ} (seed : List Bool) (input : BitString n) : wordHash m seed (List.ofFn input) = List.ofFn (hash (ofList (m * n) seed).block input)

On a fixed-length source word, the executable hash is exactly the finite matrix hash.