Documentation

Complexity.Crypto.Computational.GoldreichLevin.HardCore

The Goldreich–Levin hard-core predicate #

Split a seed into two equal halves and an optional spare bit. Apply the one-way function to the first half and retain the rest. The inner product of the two halves is a hard-core predicate. Keeping the spare bit extends the construction to every seed length.

OneWayPermutation.pseudorandomGenerator completes the one-bit PRG construction, including deterministic polynomial time and security against uniform PPT adversaries.

Main definitions #

Main results #

References #

Adapted from Crypto/Computational/GoldreichLevin/HardCore.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the shared game API and tidy TM calculus.

source
def Cslib.Crypto.GoldreichLevin.paddedFunction (f : List Bool → List Bool) (seed : List Bool) :
List Bool

Apply a function to the first half of a word and retain the remaining bits.

Instances For
    source
    def Cslib.Crypto.GoldreichLevin.paddedPredicate (seed : List Bool) :
    Bool

    The inner product of the first two equal halves, ignoring an optional final bit.

    Instances For
      source
      theorem Cslib.Crypto.GoldreichLevin.polyTime_paddedFunction {f : List Bool → List Bool} (hf : Turing.MultiTapeTM.ComputableTidilyInPolyTime f Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) :
      Turing.MultiTapeTM.ComputableTidilyInPolyTime (paddedFunction f) Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits

      The padded function uses ordinary slicing and one call to the supplied function.

      source
      theorem Cslib.Crypto.GoldreichLevin.polyTime_paddedPredicate :
      Turing.MultiTapeTM.ComputableTidilyInPolyTime paddedPredicate Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool

      The hard-core predicate is an efficient dot product of the two halves.

      source
      theorem Cslib.Crypto.GoldreichLevin.paddedFunction_chunks (f : List Bool → List Bool) {n : ℕ} (x r : BitString n) (extra : List Bool) (hextra : extra.length ≤ 1) :
      paddedFunction f (List.ofFn x ++ List.ofFn r ++ extra) = f (List.ofFn x) ++ List.ofFn r ++ extra

      On two equal chunks and at most one spare bit, only the first chunk is transformed.

      source
      theorem Cslib.Crypto.GoldreichLevin.paddedPredicate_chunks {n : ℕ} (x r : BitString n) (extra : List Bool) (hextra : extra.length ≤ 1) :
      paddedPredicate (List.ofFn x ++ List.ofFn r ++ extra) = x ⬝ᵥ r

      The spare bit is retained by the function but does not enter the parity.

      source
      theorem Cslib.Crypto.GoldreichLevin.paddedFunction_length {f : List Bool → List Bool} (hlen : ∀ (word : List Bool), (f word).length = word.length) (seed : List Bool) :
      (paddedFunction f seed).length = seed.length

      A length-preserving function leaves the complete padded seed length unchanged.

      source
      theorem Cslib.Crypto.GoldreichLevin.paddedFunction_uniform {f : List Bool → List Bool} (hf : ∀ (n : ℕ), PMF.map f (BitString.uniformList n) = BitString.uniformList n) (n : ℕ) :
      PMF.map (paddedFunction f) (BitString.uniformList n) = BitString.uniformList n

      Permuting the first half preserves uniform seeds of every length.

      source
      noncomputable def Cslib.Crypto.GoldreichLevin.paddedPredictor (adversary : Distinguisher) (spare : ℕ) :
      Distinguisher

      Translate a predictor for a padded seed to a parity predictor, sampling its spare bits.

      Instances For
        source
        theorem Cslib.Crypto.GoldreichLevin.isPPT_paddedPredictor {adversary : Distinguisher} (hPPT : Probability.IsPPT Turing.MultiTapeTM.encBool adversary) (spare : ℕ) :
        Probability.IsPPT Turing.MultiTapeTM.encBool (paddedPredictor adversary spare)

        Parameter rescaling, sampling, and captured adversary calls have a uniform PPT certificate.

        source
        theorem Cslib.Crypto.GoldreichLevin.eval_paddedPrediction (f : List Bool → List Bool) (adversary : Distinguisher) (n spare : ℕ) (hspare : spare ≤ 1) :
        (predictionGame (paddedFunction f) paddedPredicate adversary (2 * n + spare)).eval = (parityPredictionGame f (paddedPredictor adversary spare) n).eval

        The padded prediction experiment is the parity experiment, for either possible spare length.

        source
        theorem Cslib.Crypto.GoldreichLevin.padded_hardCore {f : List Bool → List Bool} (hf : OneWay f) :
        HardCore (paddedFunction f) paddedPredicate

        Goldreich–Levin supplies an efficient hard-core predicate for the padded function. Two fixed PPT reductions handle even and odd seed lengths; no length-dependent adversary is chosen.

        source
        def Cslib.Crypto.GoldreichLevin.generator (f : List Bool → List Bool) (seed : List Bool) :
        List Bool

        The one-bit generator: permute the first half, retain the rest, and append the parity.

        Instances For
          source
          theorem Cslib.Crypto.OneWayPermutation.pseudorandomGenerator {f : List Bool → List Bool} (hf : OneWayPermutation f) :
          PseudorandomGenerator (GoldreichLevin.generator f) fun (n : ℕ) => n + 1

          One-way permutations imply uniform polynomial-time pseudorandom generators with one-bit stretch. Goldreich–Levin supplies the hard-core predicate; uniformity supplies the ideal hybrid.