The pseudoentropy prediction gap from one-wayness

The executable hashed parity reduction has polynomial loss. One-wayness therefore makes its inversion term negligible, leaving an inverse-polynomial gap between feasible prediction and the entropy threshold. Each predictor supplies one inverter with a fixed precision degree; neither its code nor its choice of saved randomness depends on a nonuniform advice string.

Main results

• Cslib.Crypto.Pseudoentropy.HashPair.pair_hasGap: prediction gap for normalized word functions.
• Cslib.Crypto.OneWay.exists_pseudoentropyPair: every uniform OWF gives an exactly samplable pair with an inverse-linear prediction gap, including variable-length original images.

References

• T. Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, Definition 4 and Section 4, Lemmas 3 and 4. We use the public matrix and dyadic-range variant proved in HashReduction. This module discharges the inversion hypothesis using uniform strict PPT one-wayness.

Adapted from Crypto/Computational/Pseudoentropy/OneWay.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using typed saved seeds and nonnegative security games.

theorem Cslib.Crypto.Pseudoentropy.HashPair.precision_three_ge {n : ℕ} (hn : 8 ≤ n) : 8 * hashCount n ≤ GoldreichLevin.precision 3 n

A single cubic precision suffices for all sufficiently large dimensions.

theorem Cslib.Crypto.Pseudoentropy.HashPair.eventually_prediction_entropy_le {f : List Bool → List Bool} (hf : OneWay f) {Image : ℕ → Type} [∀ (n : ℕ), Finite (Image n)] (finiteFunction : (n : ℕ) → BitString n → Image n) (encodeImage : (n : ℕ) → Image n ↪ List Bool) (hencode : ∀ (n : ℕ) (x : Fin n → Bool), f (List.ofFn x) = (encodeImage n) (finiteFunction n x)) (imageLength : ℕ → ℕ) (hlength : ∀ (n : ℕ) (image : Image n), ((encodeImage n) image).length = imageLength n) (adversary : Distinguisher) (hPPT : Probability.IsPPT Turing.MultiTapeTM.encBool adversary) : ∀ᶠ (n : ℕ) in Filter.atTop, 2 * ((predictionGame (sample f) adversary n).eval true).toReal - 1 ≤ 1 - Probability.PMF.conditionalEntropy (joint (finiteFunction n)) - 1 / ↑(hashCount n)

The finite entropy threshold holds eventually against every uniform PPT word predictor. The image may have any fixed width at each parameter; it need not be a permutation or regular.

theorem Cslib.Crypto.Pseudoentropy.HashPair.pair_hasGap {f : List Bool → List Bool} (hf : OneWay f) {Image : ℕ → Type} [∀ (n : ℕ), Finite (Image n)] (finiteFunction : (n : ℕ) → BitString n → Image n) (encodeImage : (n : ℕ) → Image n ↪ List Bool) (hencode : ∀ (n : ℕ) (x : Fin n → Bool), f (List.ofFn x) = (encodeImage n) (finiteFunction n x)) (imageLength : ℕ → ℕ) (hlength : ∀ (n : ℕ) (image : Image n), ((encodeImage n) image).length = imageLength n) : (pair f ⋯ finiteFunction encodeImage hencode).HasGap fun (n : ℕ) => 1 / ↑(hashCount n)

A one-way function with a fixed image width at each parameter gives a samplable pseudoentropy pair. The gap is inverse-linear in the original input length.

theorem Cslib.Crypto.OneWay.exists_pseudoentropyPair {f : List Bool → List Bool} (hf : OneWay f) : ∃ (pair : Pseudoentropy.SamplablePair), pair.HasGap fun (n : ℕ) => 1 / (2 * (↑n + 7))

Every one-way word function yields an exactly samplable pseudoentropy pair with an explicit inverse-polynomial prediction gap. Normalization handles arbitrary original output lengths.