Finite Goldreich–Levin inversion reduction

A seeded predictor sees an image and a parity query. The inverter samples one private seed, reuses that seed for every predictor call, enumerates the decoder's candidates, and checks their images. Thus the deterministic decoding theorem applies to each fixed image and seed, even when the predictor's answers to different queries are correlated through its randomness.

If average prediction success is at least 1 / 2 + ε, invert_success_ge gives inversion success at least ε / 4. A fixed random choice between the predictor and its complement handles either sign of the bias: invertSigned_success_ge gives success at least ε / 8 from absolute bias ε. Neither inverter receives the hidden preimage or chooses a sign based on it.

The image may have any type with decidable equality, and its length need not equal the input length. The finite seed type and its distribution may depend on the image; they are fixed before the independent parity query is sampled. For a strict PPT predictor, the coin-tape representation in Cslib.Computability.Probabilistic.CoinTape supplies the appropriate seeded behavior with a polynomial-time deterministic evaluator. Connecting the encoded programs and proving the complete inverter PPT remain separate porting steps. This module contains the finite distributional argument, adapted from cslib crypto at 5ff69ca.

Main definitions

• candidateList, checkCandidates: ordered candidate generation and first valid preimage.
• invertFixed, invert, invertSigned: decoding with a fixed predictor, a saved seed, and a random sign respectively.
• predictionExperiment, inversionExperiment: the finite prediction and inversion games.

Main results

• checkCandidates_correct: any listed preimage suffices, without injectivity.
• invert_success_ge, invertSigned_success_ge: positive and absolute bias give inversion success of at least ε / 4 and ε / 8, under the stated mask-count bounds.

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.candidateList {n k : ℕ} (predictor : BitString n → Bool) (masks : Fin k → BitString n) : List (BitString n)

Generate one candidate for each parity guess, retaining duplicates.

@[simp]

theorem Cslib.Crypto.GoldreichLevin.length_candidateList {n k : ℕ} (predictor : BitString n → Bool) (masks : Fin k → BitString n) : (candidateList predictor masks).length = 2 ^ k

The list has one entry per guess, whether or not candidates coincide.

@[simp]

theorem Cslib.Crypto.GoldreichLevin.mem_candidateList {n k : ℕ} (predictor : BitString n → Bool) (masks : Fin k → BitString n) (x : BitString n) : x ∈ candidateList predictor masks ↔ x ∈ candidates predictor masks

The ordered enumeration contains exactly the candidates in the finite decoder.

def Cslib.Crypto.GoldreichLevin.checkCandidates {Image : Type u_1} [DecidableEq Image] {n : ℕ} (f : BitString n → Image) (image : Image) (list : List (BitString n)) : BitString n

Return the first candidate with the requested image, defaulting to zero if none matches.

theorem Cslib.Crypto.GoldreichLevin.checkCandidates_correct {Image : Type u_1} [DecidableEq Image] {n : ℕ} (f : BitString n → Image) (x : BitString n) (list : List (BitString n)) (hx : x ∈ list) : f (checkCandidates f (f x) list) = f x

If the original preimage is listed, checking finds a valid preimage. Injectivity is not needed.

noncomputable def Cslib.Crypto.GoldreichLevin.invertFixed {Image : Type u_1} [DecidableEq Image] {n : ℕ} (f : BitString n → Image) (predictor : BitString n → Bool) (k : ℕ) (image : Image) : PMF (BitString n)

Decode a fixed predictor and check its candidate list against the given image.

theorem Cslib.Crypto.GoldreichLevin.invertFixed_comp_injective {Image : Type u_1} [DecidableEq Image] {n : ℕ} {Encoded : Type u_2} [DecidableEq Encoded] (f : BitString n → Image) (encode : Image → Encoded) (hencode : Function.Injective encode) (predictor : BitString n → Bool) (k : ℕ) (image : Image) : invertFixed (encode ∘ f) predictor k (encode image) = invertFixed f predictor k image

An injective representation of images preserves every candidate check and the decoder's entire output distribution, including its default output.

theorem Cslib.Crypto.GoldreichLevin.invertFixed_success_ge_half {Image : Type u_1} [DecidableEq Image] {n k : ℕ} (f : BitString n → Image) (predictor : BitString n → Bool) (x : BitString n) (ε : ℝ) (hε : 0 < ε) (hk : 0 < k) (h : 1 / 2 + ε ≤ agreement predictor x) (hsize : ↑n ≤ 2 * ε ^ 2 * ↑(2 ^ k - 1)) : 1 / 2 ≤ ((PMF.map (fun (z : BitString n) => f z == f x) (invertFixed f predictor k (f x))) true).toReal

A correlated predictor yields a valid preimage with probability at least one half when there are enough masks. The algorithm receives only the image; x occurs only in the guarantee.

noncomputable def Cslib.Crypto.GoldreichLevin.invert {Image : Type u_1} [DecidableEq Image] {n : ℕ} {Coins : Image → Type u_2} (f : BitString n → Image) (predictor : (image : Image) → Coins image → BitString n → Bool) (coins : (image : Image) → PMF (Coins image)) (k : ℕ) (image : Image) : PMF (BitString n)

Sample the predictor's seed once and reuse it throughout the decoder.

noncomputable def Cslib.Crypto.GoldreichLevin.predictionExperiment {Image : Type u_1} {n : ℕ} {Coins : Image → Type u_2} (f : BitString n → Image) (predictor : (image : Image) → Coins image → BitString n → Bool) (coins : (image : Image) → PMF (Coins image)) : PMF Bool

Average parity-prediction success over a uniform preimage, the seed, and a uniform query.

noncomputable def Cslib.Crypto.GoldreichLevin.inversionExperiment {Image : Type u_1} [DecidableEq Image] {n : ℕ} (f : BitString n → Image) (inverter : Image → PMF (BitString n)) : PMF Bool

Challenge the inverter with the image of a uniform input and accept any valid preimage.

theorem Cslib.Crypto.GoldreichLevin.inversionExperiment_bind {Image : Type u_1} [DecidableEq Image] {n : ℕ} {Coins : Type u_2} (f : BitString n → Image) (coins : PMF Coins) (inverter : Coins → Image → PMF (BitString n)) : (inversionExperiment f fun (image : Image) => coins.bind fun (seed : Coins) => inverter seed image) = coins.bind fun (seed : Coins) => inversionExperiment f (inverter seed)

Independent private randomness may be sampled before or after the inversion challenge.

theorem Cslib.Crypto.GoldreichLevin.invert_success_ge {Image : Type u_1} [DecidableEq Image] {n k : ℕ} {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)) (ε : ℝ) (hε : 0 < ε) (hk : 0 < k) (h : 1 / 2 + ε ≤ ((predictionExperiment f predictor coins) true).toReal) (hsize : ↑n ≤ 2 * (ε / 2) ^ 2 * ↑(2 ^ k - 1)) : ε / 4 ≤ ((inversionExperiment f (invert f predictor coins k)) true).toReal

Positive prediction bias ε gives inversion success at least ε / 4. For each fixed input and seed, either agreement is below 1 / 2 + ε / 2, or decoding succeeds with probability at least one half. Averaging this dichotomy proves the reduction.

noncomputable def Cslib.Crypto.GoldreichLevin.invertSigned {Image : Type u_1} [DecidableEq Image] {n : ℕ} {Coins : Image → Type u_2} (f : BitString n → Image) (predictor : (image : Image) → Coins image → BitString n → Bool) (coins : (image : Image) → PMF (Coins image)) (k : ℕ) (image : Image) : PMF (BitString n)

A fixed inverter for either sign of prediction bias. One independent fair bit chooses whether to complement the predictor; no advice about its bias is required.

theorem Cslib.Crypto.GoldreichLevin.invertSigned_success_ge {Image : Type u_1} [DecidableEq Image] {n k : ℕ} {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)) (ε : ℝ) (hε : 0 < ε) (hk : 0 < k) (h : ε ≤ |((predictionExperiment f predictor coins) true).toReal - 1 / 2|) (hsize : ↑n ≤ 2 * (ε / 2) ^ 2 * ↑(2 ^ k - 1)) : ε / 8 ≤ ((inversionExperiment f (invertSigned f predictor coins k)) true).toReal

Absolute prediction bias ε gives inversion success at least ε / 8 using one fixed reduction for both signs. This is a finite probability bound, without a machine-time claim.