This module defines a universal-2 hash by vector matrix multiplication with Toeplitz matrices.

Toeplitz matrices are defined in ToeplitzGeneral.lean.

Main result: binToeplitz_mulVec_isUniversal2 shows that matrix-vector multiplication with (binary) Toeplitz matrices is universal-2.

theorem toeplitzModp_mulVec_isUniversal2 (m n p : ℕ) [NeZero m] [NeZero n] [hp : Fact (Nat.Prime p)] : HashFamily.universal2 fun (M : ToeplitzMatrix m n (ZMod p)) (v : Fin n → ZMod p) => (↑M).mulVec v

Main result: Multiplication (mod p) by a random Toeplitz matrix is a universal-2 hash family.

def toeplitzHash (m n : ℕ) : HashFamily (Fin (m + n - 1) → ZMod 2) (Fin n → ZMod 2) (Fin m → ZMod 2)

Toeplitz hash, expressed using only bit vectors.

Equations

• toeplitzHash m n param v = (↑(ToeplitzMatrix.from_params param)).mulVec v

theorem toeplitzHash.universal2 (m n : ℕ) [NeZero m] [NeZero n] : (toeplitzHash m n).universal2

theorem Nat.ne_rat_ge1_of_lt1 (n : ℕ) (q : ℚ) (nne0 : n > 0) (qlt1 : q < 1) : ↑n ≠ q