The uniform Goldreich–Levin inverter

One functional program samples a sign, a saved predictor seed and independent mask bits, then runs the certified word decoder. Its saved evaluator is typed: it receives the parameter and auxiliary word directly and returns a Boolean. No raw output decoding is exposed to the caller.

The same seed is reused for every query at a given image. Its length accounts for the actual pair encoding: an n-bit query appended to the image has encoded input length 3 * n + image.length + 1. Images may have arbitrary lengths. Every fixed precision degree selects one uniform PPT inverter across all security parameters.

Main definitions

• coinBudget: the predictor tape length for an arbitrary image and an n-bit query.
• parityPredictionGame: predict a uniform inner product given an image and a mask.
• wordInverter: the functional randomized inversion program.

Main results

• isPPT_wordInverter: the complete inverter is uniformly PPT.
• wordInverter_eval, eval_parityPredictionGame: exact finite-game correspondences.
• word_prediction_advantage_le: the concrete reduction loss.
• negligible_parityPrediction: one-wayness implies negligible prediction bias.

References

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

Adapted from Crypto/Computational/GoldreichLevin/WordReduction.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using typed saved seeds and the tidy TM calculus.

def Cslib.Crypto.GoldreichLevin.coinBudget (c d n imageLength : ℕ) : ℕ

The saved tape covers the unary parameter, the whole image and an n-bit query.

def Cslib.Crypto.GoldreichLevin.fixedPredictor (evaluate : ℕ × List Bool → List Bool → Bool) (c d n : ℕ) (image : List Bool) (coins : BitString (coinBudget c d n image.length)) (query : BitString n) : Bool

Evaluate a parity query with the same saved private seed throughout the reduction.

noncomputable def Cslib.Crypto.GoldreichLevin.parityPredictionGame (f : List Bool → List Bool) (adversary : Distinguisher) (n : ℕ) : ProbComp Bool

Predict a uniform inner product from an image and an independent uniform query.

theorem Cslib.Crypto.GoldreichLevin.isPPTOn_parityPredictionGame {f : List Bool → List Bool} {adversary : Distinguisher} (hf : Turing.MultiTapeTM.ComputableTidilyInPolyTime f Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (ha : Probability.IsPPT Turing.MultiTapeTM.encBool adversary) : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool (parityPredictionGame f adversary)

The prediction experiment composes sampling, the adversary and Boolean word operations.

noncomputable def Cslib.Crypto.GoldreichLevin.wordInverter (f : List Bool → List Bool) (evaluate : ℕ × List Bool → List Bool → Bool) (c d degree : ℕ) : Inverter

Sample one sign, one predictor seed and independent masks, then decode and check candidates.

theorem Cslib.Crypto.GoldreichLevin.isPPT_wordInverter {f : List Bool → List Bool} {evaluate : ℕ × List Bool → List Bool → Bool} (hf : Turing.MultiTapeTM.ComputableTidilyInPolyTime f Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (hevaluate : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : (ℕ × List Bool) × List Bool) => evaluate p.1 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (c d degree : ℕ) : Probability.IsPPT Turing.MultiTapeTM.encBits (wordInverter f evaluate c d degree)

Every fixed degree gives one strict PPT inverter for all parameters and images.

theorem Cslib.Crypto.GoldreichLevin.wordInverter_eval (f : List Bool → List Bool) (evaluate : ℕ × List Bool → List Bool → Bool) (c d degree n : ℕ) (image : List Bool) : (wordInverter f evaluate c d degree n image).eval = PMF.map List.ofFn (invertSigned (fun (bits : BitString n) => f (List.ofFn bits)) (fixedPredictor evaluate c d n) (fun (image : List Bool) => Probability.PMF.uniformOfFintype (BitString (coinBudget c d n image.length))) (maskCount n (precision degree n)) image)

At every image length, the program realizes exactly the finite seeded inverter.

theorem Cslib.Crypto.GoldreichLevin.fixedPredictor_distribution (adversary : Distinguisher) (evaluate : ℕ × List Bool → List Bool → Bool) (c d : ℕ) (hrealize : ∀ (n : ℕ) (input : List Bool), (adversary n input).eval = PMF.map (evaluate (n, input)) (BitString.uniformList (c * (((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (n, input)).length + 1) ^ d))) (n : ℕ) (image : List Bool) (query : BitString n) : PMF.map (fun (coins : BitString (coinBudget c d n image.length)) => fixedPredictor evaluate c d n image coins query) (Probability.PMF.uniformOfFintype (BitString (coinBudget c d n image.length))) = (adversary n (image ++ List.ofFn query)).eval

Saved-seed evaluation has the right prediction law for images of any length.

theorem Cslib.Crypto.GoldreichLevin.eval_parityPredictionGame (f : List Bool → List Bool) (adversary : Distinguisher) (evaluate : ℕ × List Bool → List Bool → Bool) (c d : ℕ) (hrealize : ∀ (n : ℕ) (input : List Bool), (adversary n input).eval = PMF.map (evaluate (n, input)) (BitString.uniformList (c * (((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (n, input)).length + 1) ^ d))) (n : ℕ) : (parityPredictionGame f adversary n).eval = predictionExperiment (fun (bits : BitString n) => f (List.ofFn bits)) (fixedPredictor evaluate c d n) fun (image : List Bool) => Probability.PMF.uniformOfFintype (BitString (coinBudget c d n image.length))

The prediction game is exactly the finite experiment with an image-dependent saved seed.

theorem Cslib.Crypto.GoldreichLevin.eval_wordInversionGame (f : List Bool → List Bool) (evaluate : ℕ × List Bool → List Bool → Bool) (c d degree n : ℕ) : (inversionGame f (wordInverter f evaluate c d degree) n).eval = inversionExperiment (fun (bits : BitString n) => f (List.ofFn bits)) (invertSigned (fun (bits : BitString n) => f (List.ofFn bits)) (fixedPredictor evaluate c d n) (fun (image : List Bool) => Probability.PMF.uniformOfFintype (BitString (coinBudget c d n image.length))) (maskCount n (precision degree n)))

The standard any-preimage game agrees with the finite inversion experiment.

theorem Cslib.Crypto.GoldreichLevin.word_prediction_advantage_le (f : List Bool → List Bool) (adversary : Distinguisher) (evaluate : ℕ × List Bool → List Bool → Bool) (c d : ℕ) (hrealize : ∀ (n : ℕ) (input : List Bool), (adversary n input).eval = PMF.map (evaluate (n, input)) (BitString.uniformList (c * (((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (n, input)).length + 1) ^ d))) (degree n : ℕ) : |((parityPredictionGame f adversary n).eval true).toReal - 1 / 2| ≤ 1 / ↑(precision degree n) + 8 * ((inversionGame f (wordInverter f evaluate c d degree) n).eval true).toReal

Prediction bias is at most the precision error plus eight times inversion success.

theorem Cslib.Crypto.GoldreichLevin.negligible_parityPrediction {f : List Bool → List Bool} (hf : OneWay f) (adversary : Distinguisher) (hPPT : Probability.IsPPT Turing.MultiTapeTM.encBool adversary) : Negligible fun (n : ℕ) => Game.guessingAdvantage (parityPredictionGame f adversary n).eval

No uniform PPT adversary predicts a masked inner product of a one-way input with nonnegligible bias. Each precision degree selects one inverter for all lengths.

theorem Cslib.Crypto.GoldreichLevin.exists_word_reduction (f : List Bool → List Bool) (adversary : Distinguisher) (hPPT : Probability.IsPPT Turing.MultiTapeTM.encBool adversary) : ∃ (c : ℕ) (d : ℕ) (evaluate : ℕ × List Bool → List Bool → Bool), Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : (ℕ × List Bool) × List Bool) => evaluate p.1 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool ∧ ∀ (degree n : ℕ), |((parityPredictionGame f adversary n).eval true).toReal - 1 / 2| ≤ 1 / ↑(precision degree n) + 8 * ((inversionGame f (wordInverter f evaluate c d degree) n).eval true).toReal

One efficient typed evaluator witnesses the concrete reduction at every precision degree. When f is efficient, isPPT_wordInverter certifies each resulting inverter.