Documentation

Complexity.Probability.KWiseIndependent.Trinomial

Exact k-wise independent hashing over explicit trinomial binary fields #

By evaluating degree-< k polynomials over the explicit binary field Cslib.TrinomialField t = AdjoinRoot (X ^ (2 * 3 ^ t) + X ^ (3 ^ t) + 1) and projecting the result to its low M ≤ 2 * 3 ^ t coordinates in the power basis, we obtain an explicit, zero-bias k-wise independent hash family (Cslib.Probability.trinomialPolyHash) from Fin U onto Fin (2 ^ M) whenever U ≤ 2 ^ (2 * 3 ^ t) and M ≤ 2 * 3 ^ t (Cslib.Probability.isKWiseIndependentHash_trinomialPolyHash) Vadhan, Section 3.5.5; Wegman and Carter.

Because the coordinate map Cslib.TrinomialField.equivBits t : TrinomialField t ≃+ BitString (2 * 3 ^ t) and the bit-prefix projection BitString (2 * 3 ^ t) →+ BitString M are surjective additive group homomorphisms over 𝔽₂, every output bucket in Fin (2 ^ M) has the exact same preimage size in TrinomialField t. Consequently, projecting to the low M bits preserves exact k-wise independence without modulo bias.

We also provide Cslib.Probability.trinomialStep U M, which selects a trinomial parameter t satisfying U ≤ 2 ^ (2 * 3 ^ t), M ≤ 2 * 3 ^ t, and 2 * 3 ^ t ≤ 3 * max (Nat.clog 2 (max U 2)) (max M 1).

Main definitions #

Main results #

References #

Trinomial degree selection #

source
@[irreducible]
def Cslib.Probability.trinomialStepAux (B : ℕ) :
ℕ

Smallest exponent t : ℕ such that B ≤ 2 * 3 ^ t.

Instances For
    source
    theorem Cslib.Probability.le_two_mul_three_pow_trinomialStepAux (B : ℕ) :
    B ≤ 2 * 3 ^ trinomialStepAux B

    2 * 3 ^ trinomialStepAux B is at least B.

    source
    theorem Cslib.Probability.two_mul_three_pow_trinomialStepAux_le (B : ℕ) :
    2 * 3 ^ trinomialStepAux B ≤ 3 * max B 1

    2 * 3 ^ trinomialStepAux B is at most 3 * max B 1.

    source
    def Cslib.Probability.trinomialTargetBits (U M : ℕ) :
    ℕ

    Target bit-width needed to embed Fin U and project to M bits.

    Instances For
      source
      def Cslib.Probability.trinomialStep (U M : ℕ) :
      ℕ

      Selected trinomial parameter t for universe size U and output bit-length M.

      Instances For
        source
        def Cslib.Probability.trinomialDeg (U M : ℕ) :
        ℕ

        Selected trinomial field degree 2 * 3 ^ trinomialStep U M.

        Instances For
          source
          theorem Cslib.Probability.trinomialTargetBits_le_trinomialDeg (U M : ℕ) :
          trinomialTargetBits U M ≤ trinomialDeg U M

          The selected trinomial degree is at least trinomialTargetBits U M.

          source
          theorem Cslib.Probability.le_two_pow_trinomialDeg (U M : ℕ) :
          U ≤ 2 ^ trinomialDeg U M

          The universe size U fits inside 2 ^ trinomialDeg U M.

          source
          theorem Cslib.Probability.le_trinomialDeg (U M : ℕ) :
          M ≤ trinomialDeg U M

          The output bit-length M is at most trinomialDeg U M.

          source
          theorem Cslib.Probability.trinomialDeg_le_three_mul (U M : ℕ) :
          trinomialDeg U M ≤ 3 * max (Nat.clog 2 (max U 2)) (max M 1)

          The selected trinomial degree is within a factor of 3 of trinomialTargetBits U M.

          Trinomial polynomial hashing #

          source
          noncomputable def Cslib.Probability.trinomialPolyEval (t k U : ℕ) (c : Fin k → Fin (2 ^ (2 * 3 ^ t))) (u : Fin U) :
          Fin (2 ^ (2 * 3 ^ t))

          Evaluate the degree-< k polynomial with seed coefficients c : Fin k → Fin (2 ^ (2 * 3 ^ t)) over TrinomialField t at the key u : Fin U, returning the 2 * 3 ^ t-bit result as an element of Fin (2 ^ (2 * 3 ^ t)).

          Instances For
            source
            noncomputable def Cslib.Probability.trinomialPolyHash (t k U M : ℕ) (c : Fin k → Fin (2 ^ (2 * 3 ^ t))) (u : Fin U) :
            Fin (2 ^ M)

            The k-wise independent trinomial polynomial hash family from Fin U to Fin (2 ^ M): evaluates a degree-< k polynomial over TrinomialField t and projects to the low M bits.

            Instances For
              source
              theorem Cslib.Probability.val_trinomialPolyHash (t k U M : ℕ) (c : Fin k → Fin (2 ^ (2 * 3 ^ t))) (u : Fin U) :
              ↑(trinomialPolyHash t k U M c u) = ↑(trinomialPolyEval t k U c u) &&& 2 ^ M - 1

              The numeric output of trinomialPolyHash is the bitwise mask &&& (2 ^ M - 1) of trinomialPolyEval.

              source
              theorem Cslib.Probability.trinomialPolyHash_eq_equivFin_restrictBits {t k U M : ℕ} (hM : M ≤ 2 * 3 ^ t) (c : Fin k → Fin (2 ^ (2 * 3 ^ t))) (u : Fin U) :
              trinomialPolyHash t k U M c u = (BitString.equivFin M) ((BitString.restrictBitsAddHom hM) ((TrinomialField.equivBits t) (polynomialHash (fun (j : Fin k) => (TrinomialField.equivFin t).symm (c j)) ((AdjoinRoot.mk (trinomial t)) (polyOfCode ↑u)))))

              When M ≤ 2 * 3 ^ t, trinomialPolyHash agrees with projecting the power-basis bits of the field polynomial evaluation to the first M bits.

              source
              theorem Cslib.Probability.isKWiseIndependentHash_trinomialPolyHash {t k U M : ℕ} (hU : U ≤ 2 ^ (2 * 3 ^ t)) (hM : M ≤ 2 * 3 ^ t) :
              IsKWiseIndependentHash k (trinomialPolyHash t k U M)

              trinomialPolyHash t k U M is an exact k-wise independent hash family onto Fin (2 ^ M) whenever U ≤ 2 ^ (2 * 3 ^ t) and M ≤ 2 * 3 ^ t.