Goldreich–Levin parameters and the asymptotic reduction

The decoder uses maskCount n p = log₂ (2 * n * p² + 1) + 1 base masks at precision 1 / p. For p > 0 this satisfies the finite recovery bound. At every precision it enumerates at most 4 * n * p² + 2 guesses. For the fixed-degree precision (n + 1)^degree, both the list size and random-mask length are polynomially bounded. These are explicit size bounds, not machine-runtime certificates.

The prediction advantage is at most 1 / p + 8 * inversion_success. Consequently, if the inverter at each fixed precision degree has negligible success, prediction bias is negligible. Each degree defines one inverter for all lengths. No length-dependent choice of adversary or sign of the bias is used. One-wayness can discharge these success hypotheses once the word-based game correspondence and uniform PPT certificates for the inverters are proved. Adapted from the cslib crypto branch at 5ff69ca.

Main definitions

• maskCount: the logarithmic number of base masks.
• precision: a fixed inverse-polynomial accuracy denominator.

Main results

• guessCount_maskCount_le, maskCount_sufficient: output-size and recovery bounds.
• guessCount_polynomial, randomMaskBits_polynomial: polynomially bounded enumeration and coins.
• negligible_prediction_of_negligible_inversion: each fixed-precision inverter's negligible success implies negligible prediction bias, in the shared nonnegative game API.

References

• O. Goldreich, L. Levin, A Hard-Core Predicate for All One-Way Functions
• L. Trevisan, CS276 Lecture 12: Goldreich–Levin

def Cslib.Crypto.GoldreichLevin.maskCount (n precision : ℕ) : ℕ

A computable number of base masks sufficient for prediction bias at least 1 / precision.

theorem Cslib.Crypto.GoldreichLevin.maskCount_pos (n precision : ℕ) : 0 < maskCount n precision

At least one base mask is used, including at dimension zero.

theorem Cslib.Crypto.GoldreichLevin.subsetCount_maskCount_ge (n precision : ℕ) : 2 * n * precision ^ 2 ≤ 2 ^ maskCount n precision - 1

The subset masks meet the recovery theorem's required count.

theorem Cslib.Crypto.GoldreichLevin.guessCount_maskCount_le (n precision : ℕ) : 2 ^ maskCount n precision ≤ 4 * n * precision ^ 2 + 2

Rounding the mask count up costs at most a factor of two in the number of guesses.

theorem Cslib.Crypto.GoldreichLevin.maskCount_le (n precision : ℕ) : maskCount n precision ≤ 2 * n * precision ^ 2 + 1

A simple polynomial upper bound also controls the base-mask count.

theorem Cslib.Crypto.GoldreichLevin.maskCount_sufficient (n precision : ℕ) (hp : 0 < precision) : ↑n ≤ 2 * (1 / ↑precision / 2) ^ 2 * ↑(2 ^ maskCount n precision - 1)

The chosen count satisfies the exact real-valued inequality used by the finite reduction.

theorem Cslib.Crypto.GoldreichLevin.correlation_le_invertFixed {n : ℕ} {Image : Type u_1} [DecidableEq Image] (f : BitString n → Image) (predictor : BitString n → Bool) (x : BitString n) (precision : ℕ) (hp : 0 < precision) : 2 * agreement predictor x - 1 ≤ 1 / ↑precision + 2 * ((PMF.map (fun (z : BitString n) => f z == f x) (invertFixed f predictor (maskCount n precision) (f x))) true).toReal

Signed parity correlation is bounded by decoder success and its chosen accuracy. This pointwise form allows auxiliary input to be guessed in later reductions.

theorem Cslib.Crypto.GoldreichLevin.invertSigned_advantage_le {n : ℕ} {Image : Type u_1} [DecidableEq Image] {Coins : Image → Type u_2} [∀ (image : Image), Finite (Coins image)] (f : BitString n → Image) (predictor : (image : Image) → Coins image → BitString n → Bool) (coins : (image : Image) → PMF (Coins image)) (precision : ℕ) (hp : 0 < precision) : |((predictionExperiment f predictor coins) true).toReal - 1 / 2| ≤ 1 / ↑precision + 8 * ((inversionExperiment f (invertSigned f predictor coins (maskCount n precision))) true).toReal

The same inverter bounds all prediction biases, with an additive error of 1 / precision. When the actual bias exceeds that error, the recovery bound applies to the actual bias itself.

def Cslib.Crypto.GoldreichLevin.precision (degree n : ℕ) : ℕ

A fixed degree selects an inverse-polynomial accuracy for every input length.

theorem Cslib.Crypto.GoldreichLevin.precision_pos (degree n : ℕ) : 0 < precision degree n

The precision denominator never vanishes.

theorem Cslib.Crypto.GoldreichLevin.guessCount_polynomial (degree : ℕ) : PolynomiallyBounded fun (n : ℕ) => 2 ^ maskCount n (precision degree n)

Enumerating the guesses uses a polynomial-size list at any fixed precision degree.

theorem Cslib.Crypto.GoldreichLevin.maskCount_polynomial (degree : ℕ) : PolynomiallyBounded fun (n : ℕ) => maskCount n (precision degree n)

The logarithmic mask count is polynomially bounded at each fixed precision degree.

theorem Cslib.Crypto.GoldreichLevin.randomMaskBits_polynomial (degree : ℕ) : PolynomiallyBounded fun (n : ℕ) => n * maskCount n (precision degree n)

Storing all base masks uses polynomially many bits at any fixed precision degree.

theorem Cslib.Crypto.GoldreichLevin.negligible_prediction_of_negligible_inversion {Image : ℕ → Type u_1} [(n : ℕ) → DecidableEq (Image n)] {Coins : (n : ℕ) → Image n → Type u_2} [∀ (n : ℕ) (image : Image n), Finite (Coins n image)] (f : (n : ℕ) → BitString n → Image n) (predictor : (n : ℕ) → (image : Image n) → Coins n image → BitString n → Bool) (coins : (n : ℕ) → (image : Image n) → PMF (Coins n image)) (hinversion : ∀ (degree : ℕ), Negligible fun (n : ℕ) => Game.succProbability (inversionExperiment (f n) (invertSigned (f n) (predictor n) (coins n) (maskCount n (precision degree n))))) : Negligible fun (n : ℕ) => Game.guessingAdvantage (predictionExperiment (f n) (predictor n) (coins n))

If every fixed-precision inverter has negligible success, prediction bias is negligible. For each power, multiply the pointwise reduction by that power of the parameter. The precision term is at most one and the inversion term tends to zero, giving superpolynomial decay.