Affine pairwise-independent hashing -- definitions #
The seed encodes one affine linear form over the Boolean ring for each output
bit. Each row has domainWidth coefficients and one constant coefficient.
Number of random bits in the affine family from domainWidth bits to
rangeWidth bits.
Equations
- Complexity.PairwiseIndependentHash.affineSeedWidth domainWidth rangeWidth = rangeWidth * (domainWidth + 1)
Instances For
Row-major equivalence between affine coefficient rows and the flat seed.
Equations
- Complexity.PairwiseIndependentHash.affineSeedEquiv domainWidth rangeWidth = (Equiv.curry (Fin rangeWidth) (Fin (domainWidth + 1)) Bool).symm.trans (finProdFinEquiv.arrowCongr (Equiv.refl Bool))
Instances For
def
Complexity.PairwiseIndependentHash.affineRows
{domainWidth rangeWidth : ℕ}
(seed : BitString (affineSeedWidth domainWidth rangeWidth))
:
Coefficient rows decoded from a flat affine-family seed.
Equations
- Complexity.PairwiseIndependentHash.affineRows seed row column = seed (finProdFinEquiv (row, column))
Instances For
def
Complexity.PairwiseIndependentHash.affineSeedOfRows
{domainWidth rangeWidth : ℕ}
(rows : Fin rangeWidth → BitString (domainWidth + 1))
:
BitString (affineSeedWidth domainWidth rangeWidth)
Flatten coefficient rows into the affine family's row-major seed.
Equations
- Complexity.PairwiseIndependentHash.affineSeedOfRows rows = (Complexity.PairwiseIndependentHash.affineSeedEquiv domainWidth rangeWidth) rows
Instances For
def
Complexity.PairwiseIndependentHash.affineAugment
{domainWidth : ℕ}
(input : BitString domainWidth)
:
Append a constant 1 coordinate to an input.
Equations
Instances For
def
Complexity.PairwiseIndependentHash.affineEval
{domainWidth rangeWidth : ℕ}
(seed : BitString (affineSeedWidth domainWidth rangeWidth))
(input : BitString domainWidth)
:
BitString rangeWidth
Evaluate the affine coefficient matrix on an augmented input. Addition in the Boolean ring is XOR and multiplication is AND.
Equations
- One or more equations did not get rendered due to their size.