Affine pairwise-independent hashing

This module constructs the standard affine family over the Boolean ring. A hash from domainWidth bits to rangeWidth bits uses exactly rangeWidth * (domainWidth + 1) random bits.

def Complexity.PairwiseIndependentHash.affine (domainWidth rangeWidth : ℕ) : PairwiseIndependentHash domainWidth rangeWidth (affineSeedWidth domainWidth rangeWidth)

The standard affine pairwise-independent hash family over the Boolean ring, represented by a row-major flat bit-string seed.

Equations

• Complexity.PairwiseIndependentHash.affine domainWidth rangeWidth = { eval := Complexity.PairwiseIndependentHash.affineEval, uniform := ⋯, pairwise := ⋯ }

@[simp]

theorem Complexity.PairwiseIndependentHash.affine_eval (domainWidth rangeWidth : ℕ) : (affine domainWidth rangeWidth).eval = affineEval

Evaluation of the affine family is the concrete Boolean-ring matrix map.