This module defines notions of universality for families of hash functions.

A hash family is a family of functions Input → Output. Rather than define it as a set of functions, we put the choice of function into a type Seed.

Universal-2

A function hash : Seed → Input → Output is Universal-2 if for any distinct inputs x and y, the probability over a uniform random seed that hash s x = hash s y is at most 1 / |Output|.

This is formalized as (number of seeds causing collision) * |Output| ≤ |Seed|.

We also give an alternative definition, proven equivalent, which the AIs seem to like more. Let's see which we keep in the end...

Strongly-universal-n

A family H is strongly universal (also known as "pairwise independent") if for all x ≠ y and all a b : Output, \Pr_i [h_i(x) = a ∧ h_i(y) = b] = 1 / |Output|^2

@[reducible, inline]

abbrev HashFamily (Seed : Type u_1) (Input : Type u_2) (Output : Type u_3) : Type (max (max u_1 u_2) u_3)

A hash family is a family of functions Input → Output. Rather than define it as a set of functions, we put the choice of function into a type Seed.

Equations

• HashFamily Seed Input Output = (Seed → Input → Output)

def HashFamily.universal2 {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] (hash : HashFamily Seed Input Output) : Prop

A hash function taking a seed and an input is universal-2 if for any distinct inputs x and y, the probability (over the seed) of a collision is at most 1/|Output|.

This is expressed as: (number of seeds causing collision) * |Output| ≤ |Seed|.

Equations

• hash.universal2 = ∀ ⦃x y : Input⦄, x ≠ y → Fintype.card ↑{s : Seed | hash s x = hash s y} * Fintype.card Output ≤ Fintype.card Seed

theorem HashFamily.universal2_of_seed_empty {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] (hash : HashFamily Seed Input Output) [IsEmpty Seed] : hash.universal2

def probUniform {Seed : Type u_1} [Fintype Seed] (p : Seed → Prop) [DecidablePred p] : ℚ

The uniform probability of a predicate on Seed, modeled by counting.

Equations

• probUniform p = ↑(Fintype.card { i : Seed // p i }) / ↑(Fintype.card Seed)

theorem HashFamily.universal2_iff_probUniform {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] (H : HashFamily Seed Input Output) : H.universal2 ↔ ∀ ⦃x y : Input⦄, x ≠ y → (probUniform fun (i : Seed) => H i x = H i y) ≤ 1 / ↑(Fintype.card Output)

Alternative (equivalent) statement of universal-2 using probUniform.

A family H is universal2 if for all distinct x ≠ y, the collision probability is at most 1 / |Output|:

Pr_i [h_i(x) = h_i(y)] ≤ 1 / |Output|

def HashFamily.stronglyUniversal_n {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] (n : ℕ) (H : HashFamily Seed Input Output) : Prop

A hash family is strongly-universal-n (also called "n-wise independent") if

• given n distinct inputs a₁, a₂, ...
• and n (not necessarily distinct) outputs b₁, b₂, ..., exactly |HashFamily|/(|Output|^n) functions take a₁ to b₁ a₂ to b₂, etc.

See Wegman, Carter 1981

Equations

• One or more equations did not get rendered due to their size.

def HashFamily.stronglyUniversal2 {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] (H : HashFamily Seed Input Output) : Prop

Special case: a family H is strongly-universal-2 (also known as just "strongly universal", or "pairwise independent") if for all x ≠ y and all a b : Output, \Pr_i [h_i(x) = a ∧ h_i(y) = b] = 1 / |Output|^2.

Equations

• H.stronglyUniversal2 = ∀ ⦃x y : Input⦄, x ≠ y → ∀ (a b : Output), ↑(Fintype.card { i : Seed // H i x = a ∧ H i y = b }) = ↑(Fintype.card Seed) / ↑(Fintype.card Output) ^ 2

theorem HashFamily.stronglyUniversal2_iff_probUniform {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] [Nonempty Seed] (H : HashFamily Seed Input Output) : H.stronglyUniversal2 ↔ ∀ ⦃x y : Input⦄, x ≠ y → ∀ (a b : Output), (probUniform fun (i : Seed) => H i x = a ∧ H i y = b) = 1 / ↑(Fintype.card Output) ^ 2

Equivalent statement of strongly-universal-2 using probUniform.

A family H is stronglyUniversal2 if for all distinct x ≠ y, given two outputs a and b, the probability to map x ↦ a and y ↦ b is exactly 1 / (|Output|^2).

theorem HashFamily.stronglyUniversal2_stronglyUniversal_n_2 {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] [Inhabited Seed] (H : HashFamily Seed Input Output) : H.stronglyUniversal2 ↔ stronglyUniversal_n 2 H

stronglyUniversal2 is a special case of strongly_universal_n for n = 2.

theorem HashFamily.universal2_of_stronglyUniversal2 {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] (H : HashFamily Seed Input Output) : H.stronglyUniversal2 → H.universal2

stronglyUniversal2 implies universal2.

theorem stronglyUniversal_n_of_gt_card {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] [Fintype Input] (n : ℕ) (H : HashFamily Seed Input Output) (h : Fintype.card Input < n) : HashFamily.stronglyUniversal_n n H

If n is greater than the cardinality of the input space, then any hash family is strongly universal-n (vacuously).

theorem HashFamily.universal2_of_comp_injective_seed {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] (H : HashFamily Seed Input Output) {f : Seed → Seed} (hf : Function.Injective f) : H.universal2 ↔ universal2 (H ∘ f)

The composition of a universal2 function with an injective function is universal2.

theorem HashFamily.universal2_of_comp_bijective {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] {Seed2 : Type u_4} [Fintype Seed2] (H : HashFamily Seed Input Output) {f : Seed2 → Seed} (hf : Function.Bijective f) : H.universal2 ↔ universal2 (H ∘ f)