Documentation

Complexitylib.Classes.Randomized.Hashing.Affine.Internal

Affine pairwise-independent hashing -- proof internals #

source
@[simp]
theorem Complexity.PairwiseIndependentHash.affineRows_affineSeedOfRows_internal {domainWidth rangeWidth : ℕ} (rows : Fin rangeWidth → BitString (domainWidth + 1)) :
affineRows (affineSeedOfRows rows) = rows
source
@[simp]
theorem Complexity.PairwiseIndependentHash.affineAugment_castSucc_internal {domainWidth : ℕ} (input : BitString domainWidth) (column : Fin domainWidth) :
affineAugment input column.castSucc = input column
source
@[simp]
theorem Complexity.PairwiseIndependentHash.affineAugment_last_internal {domainWidth : ℕ} (input : BitString domainWidth) :
affineAugment input (Fin.last domainWidth) = true
source
def Complexity.PairwiseIndependentHash.affineEvalHom {domainWidth rangeWidth : ℕ} (input : BitString domainWidth) :
BitString (affineSeedWidth domainWidth rangeWidth) →+ BitString rangeWidth

Affine evaluation is additive in the seed.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Complexity.PairwiseIndependentHash.affinePairEvalHom {domainWidth rangeWidth : ℕ} (first second : BitString domainWidth) :
    BitString (affineSeedWidth domainWidth rangeWidth) →+ BitString rangeWidth × BitString rangeWidth

    The joint outputs on two inputs form an additive map of the seed.

    Equations
    Instances For
      source
      theorem Complexity.PairwiseIndependentHash.affineEvalHom_surjective_internal {domainWidth rangeWidth : ℕ} (input : BitString domainWidth) :
      Function.Surjective ⇑(affineEvalHom input)
      source
      theorem Complexity.PairwiseIndependentHash.affinePairEvalHom_surjective_internal {domainWidth rangeWidth : ℕ} {first second : BitString domainWidth} (hne : first ≠ second) :
      Function.Surjective ⇑(affinePairEvalHom first second)
      source
      theorem Complexity.PairwiseIndependentHash.affine_uniform_internal {domainWidth rangeWidth : ℕ} (input : BitString domainWidth) (output : BitString rangeWidth) :
      eventProb {seed : Fin (affineSeedWidth domainWidth rangeWidth) → Bool | affineEval seed input = output} = 1 / 2 ^ rangeWidth
      source
      theorem Complexity.PairwiseIndependentHash.affine_pairwise_internal {domainWidth rangeWidth : ℕ} {first second : BitString domainWidth} (hne : first ≠ second) (firstOutput secondOutput : BitString rangeWidth) :
      eventProb {seed : Fin (affineSeedWidth domainWidth rangeWidth) → Bool | affineEval seed first = firstOutput ∧ affineEval seed second = secondOutput} = 1 / 2 ^ (2 * rangeWidth)