Carter–Wegman-style universal hash family.

h_{a,b}(x) = a * x + b (mod p),

Main result: linearHashFamily.universal2

@[reducible, inline]

abbrev LinearIndex (p : ℕ) : Type

Index type: pairs (a, b) in (ZMod p)² with a ≠ 0.

Equations

• LinearIndex p = { ab : ZMod p × ZMod p // ab.1 ≠ 0 }

def linearHashFamily (p : ℕ) : HashFamily (LinearIndex p) (ZMod p) (ZMod p)

Linear family over ZMod p:

h_{a,b}(x) = a * x + b (mod p),

This is a special case of family H_1 in Wegman, Carter 1979).

where:

• p is prime,
• a ≠ 0 in ZMod p,
• (a, b) is chosen uniformly from (ZMod p)² with a ≠ 0.

Equations

• linearHashFamily p i x = (↑i).1 * x + (↑i).2

def generalLinearHashFamily (p : ℕ) [Fact (Nat.Prime p)] (a : ℕ) : HashFamily (LinearIndex p) (Fin a) (ZMod p)

Hash family H_1 in Wegman, Carter 1979).

``h_{a,b}(x) = a * x + b  (mod p),``

where:

• p is prime,
• a ≠ 0 in ZMod p,
• (a, b) is chosen uniformly from (ZMod p)² with a ≠ 0.
• x < a

Note that x is automatically cast to ℕ and then to ZMod p, which involves a modulo operation. The family is universal-2 for a < p.

Equations

• generalLinearHashFamily p a i x = (↑i).1 * ↑↑x + (↑i).2

theorem linearHashFamily.universal2 (p : ℕ) [Fact (Nat.Prime p)] : (linearHashFamily p).universal2

theorem generalLinearHashFamily.universal2 (p : ℕ) [Fact (Nat.Prime p)] {a : ℕ} (alep : a ≤ p) : (generalLinearHashFamily p a).universal2

Universality of the generalLinearHashFamily, where inputs can be restricted.