Polynomial stretch from one-bit pseudorandom generators

Keep a seed of the original length at the front of a word. Each iteration expands that seed by one bit and retains the previously emitted suffix. The security proof replaces successive seed expansions by uniform bits, using one uniformly randomized reduction across all hops. The seed width may differ from the security parameter, and the generator may capture an index. indexed_indistinguishable preserves a secure choice in such a family.

The deterministic iteration and stretch operators (PRGStretch.step, PRGStretch.iterate, PRGStretch.stretch) and their polynomial-time and cumulative quantitative certificates live in Complexity.Crypto.Computational.Stretch.Quantitative, which this module re-exports.

Main definitions

• PRGStretch.stretch: repeatedly expand a fixed-width seed prefix and retain emitted bits (re-exported from Stretch.Quantitative).
• PRGStretch.reduction: one uniform bounded-hop security reduction.

Main results

• PRGStretch.polyTime_iterate: captured functional iteration has a uniform TM certificate (re-exported from Stretch.Quantitative).
• PRGStretch.advantage_eq: exact sampling-range loss for the uniform reduction.
• PRGStretch.indexed_indistinguishable, PRGStretch.indistinguishable, PRGStretch.pseudorandomGenerator: polynomially many one-bit expansions preserve computational indistinguishability and yield a secure PRG.
• PseudorandomGenerator.amplify, .truncate: efficient changes of output length.

References

• B. Barak, Pseudorandomness, CS 127, length extension for PRGs. We retain the final seed and reverse the order of the emitted bits. The reduction explicitly samples its hop to preserve uniformity, with dyadic padding for strict fair-coin sampling.

Adapted from Crypto/Computational/Stretch.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the tidy calculus and current upstream games.

noncomputable def Cslib.Crypto.PRGStretch.hybrid (generator : List Bool → List Bool) (n total i : ℕ) : PMF (List Bool)

Hybrid i has i genuinely random suffix bits and total - i seed expansions left.

theorem Cslib.Crypto.PRGStretch.hybrid_zero (generator : List Bool → List Bool) (count : ℕ → ℕ) (n : ℕ) : hybrid generator n (count n) 0 = generatorEnsemble (stretch generator count) n

The initial hybrid is the stretched generator's output.

@[simp]

theorem Cslib.Crypto.PRGStretch.hybrid_last (generator : List Bool → List Bool) (n total : ℕ) : hybrid generator n total total = BitString.uniformList (n + total)

The final hybrid is uniform at the expanded length.

theorem Cslib.Crypto.PRGStretch.real_hop (generator : List Bool → List Bool) (n total i : ℕ) (hi : i < total) : (do let challenge ← generatorEnsemble generator n PMF.map (fun (suffix : List Bool) => iterate generator n (total - (i + 1)) (challenge ++ suffix)) (BitString.uniformList i)) = hybrid generator n total i

Replacing the challenge by a genuine generator output gives the earlier hybrid.

theorem Cslib.Crypto.PRGStretch.ideal_hop (generator : List Bool → List Bool) (n total i : ℕ) : (do let challenge ← BitString.uniformList (n + 1) PMF.map (fun (suffix : List Bool) => iterate generator n (total - (i + 1)) (challenge ++ suffix)) (BitString.uniformList i)) = hybrid generator n total (i + 1)

Replacing the challenge by uniform bits gives the next hybrid.

noncomputable def Cslib.Crypto.PRGStretch.hop (generator : List Bool → List Bool) (count : ℕ → ℕ) (adversary : Distinguisher) (n i : ℕ) (challenge : List Bool) : ProbComp Bool

Embed one challenge at a chosen hop; out-of-range hops reject on both sides.

noncomputable def Cslib.Crypto.PRGStretch.reduction (generator : List Bool → List Bool) (count : ℕ → ℕ) (adversary : Distinguisher) : Distinguisher

One uniform reduction samples its hop using a bounded number of fair bits.

theorem Cslib.Crypto.PRGStretch.isPPT_reduction {generator : List Bool → List Bool} {count : ℕ → ℕ} {adversary : Distinguisher} (hgenerator : Turing.MultiTapeTM.ComputableTidilyInPolyTime generator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hadversary : Probability.IsPPT Turing.MultiTapeTM.encBool adversary) : Probability.IsPPT Turing.MultiTapeTM.encBool (reduction generator count adversary)

The reduction's complete efficiency proof uses the public programming interface.

noncomputable def Cslib.Crypto.PRGStretch.test (generator : List Bool → List Bool) (seedBits count : ℕ) (adversary : List Bool → ProbComp Bool) (challenge : List Bool) : ProbComp Bool

Apply the same random-hop reduction at an explicit seed length, with any captured test.

theorem Cslib.Crypto.PRGStretch.isPPT_test {α : Type} {input : α ↪ List Bool} {generator : α → List Bool → List Bool} {seedBits count : α → ℕ} {adversary : α → List Bool → ProbComp Bool} {challenge : α → List Bool} (hgenerator : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : α × List Bool) => generator pair.1 pair.2) (Turing.MultiTapeTM.encPair input Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hseedBits : Turing.MultiTapeTM.ComputableTidilyInPolyTime seedBits input Turing.MultiTapeTM.encUnary) (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (hadversary : Probability.IsPPTOn (Turing.MultiTapeTM.encPair input Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool fun (pair : α × List Bool) => adversary pair.1 pair.2) (hchallenge : Turing.MultiTapeTM.ComputableTidilyInPolyTime challenge input Turing.MultiTapeTM.encBits) : Probability.IsPPTOn input Turing.MultiTapeTM.encBool fun (a : α) => test (generator a) (seedBits a) (count a) (adversary a) (challenge a)

Captured parameters, generator code, and the adversary compose through the public tactics.

theorem Cslib.Crypto.PRGStretch.hop_min (generator : List Bool → List Bool) (count : ℕ → ℕ) (adversary : Distinguisher) (n i : ℕ) (challenge : List Bool) : hop generator count adversary n (min (count n) i) challenge = hop generator count adversary n i challenge

Capping a sampled index only merges rejecting branches.

theorem Cslib.Crypto.PRGStretch.eval_reduction (generator : List Bool → List Bool) (count : ℕ → ℕ) (adversary : Distinguisher) (n : ℕ) (challenge : List Bool) : (reduction generator count adversary n challenge).eval = (Probability.PMF.uniformOfFintype (Fin (2 ^ (Nat.log 2 (count n) + 1)))).bind fun (i : Fin (2 ^ (Nat.log 2 (count n) + 1))) => (hop generator count adversary n (↑i) challenge).eval

The randomized reduction is exactly a uniform mixture of its padded hop reductions.

theorem Cslib.Crypto.PRGStretch.eval_real_hop (generator : List Bool → List Bool) (count : ℕ → ℕ) (adversary : Distinguisher) (n i : ℕ) : ((generatorEnsemble generator n).bind fun (challenge : List Bool) => (hop generator count adversary n i challenge).eval) = if i < count n then (hybrid generator n (count n) i).bind fun (word : List Bool) => (adversary n word).eval else PMF.pure false

The real challenge at a fixed hop realizes the earlier hybrid experiment.

theorem Cslib.Crypto.PRGStretch.eval_ideal_hop (generator : List Bool → List Bool) (count : ℕ → ℕ) (adversary : Distinguisher) (n i : ℕ) : ((BitString.uniformList (n + 1)).bind fun (challenge : List Bool) => (hop generator count adversary n i challenge).eval) = if i < count n then (hybrid generator n (count n) (i + 1)).bind fun (word : List Bool) => (adversary n word).eval else PMF.pure false

The ideal challenge at a fixed hop realizes the next hybrid experiment.

theorem Cslib.Crypto.PRGStretch.advantage_eq (generator : List Bool → List Bool) (count : ℕ → ℕ) (adversary : Distinguisher) (n : ℕ) : Game.advantage (prgRealGame (stretch generator count) adversary n).eval (prgIdealGame (fun (n : ℕ) => n + count n) adversary n).eval = ↑(2 ^ (Nat.log 2 (count n) + 1)) * Game.advantage (prgRealGame generator (reduction generator count adversary) n).eval (prgIdealGame (fun (n : ℕ) => n + 1) (reduction generator count adversary) n).eval

Exact loss of the uniform reduction, including the padded sampling outcomes.

theorem Cslib.Crypto.PRGStretch.test_advantage_eq (generator : List Bool → List Bool) (seedBits count : ℕ) (adversary : List Bool → ProbComp Bool) : Game.advantage ((PMF.map (iterate generator seedBits count) (BitString.uniformList seedBits)).bind fun (word : List Bool) => (adversary word).eval) ((BitString.uniformList (seedBits + count)).bind fun (word : List Bool) => (adversary word).eval) = ↑(2 ^ (Nat.log 2 count + 1)) * Game.advantage ((PMF.map generator (BitString.uniformList seedBits)).bind fun (word : List Bool) => (test generator seedBits count adversary word).eval) ((BitString.uniformList (seedBits + 1)).bind fun (word : List Bool) => (test generator seedBits count adversary word).eval)

The same exact loss applies with the seed length independent of the security parameter. This form is convenient for indexed candidate families.

theorem Cslib.Crypto.PRGStretch.advantage_le (generator : List Bool → List Bool) (count : ℕ → ℕ) (adversary : Distinguisher) (n : ℕ) (hpositive : 0 < count n) : Game.advantage (prgRealGame (stretch generator count) adversary n).eval (prgIdealGame (fun (n : ℕ) => n + count n) adversary n).eval ≤ ↑(2 * count n) * Game.advantage (prgRealGame generator (reduction generator count adversary) n).eval (prgIdealGame (fun (n : ℕ) => n + 1) (reduction generator count adversary) n).eval

Padding the sampled hop loses at most twice the number of expansions.

theorem Cslib.Crypto.PRGStretch.loss_polynomial {count : ℕ → ℕ} (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) : PolynomiallyBounded fun (n : ℕ) => 2 ^ (Nat.log 2 (count n) + 1)

Efficient unary counts give a polynomial bound on the reduction's dyadic loss.

theorem Cslib.Crypto.PRGStretch.indexed_indistinguishable {generator : ℕ → ℕ → List Bool → List Bool} {seedBits count choose : ℕ → ℕ} (hgenerator : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (input : (ℕ × ℕ) × List Bool) => generator input.1.1 input.1.2 input.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hseedBits : Turing.MultiTapeTM.ComputableTidilyInPolyTime seedBits Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hsecure : ∀ (adversary : ℕ → ℕ → List Bool → ProbComp Bool), (Probability.IsPPTOn (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool fun (input : (ℕ × ℕ) × List Bool) => adversary input.1.1 input.1.2 input.2) → Negligible fun (n : ℕ) => Game.advantage ((PMF.map (generator n (choose n)) (BitString.uniformList (seedBits n))).bind fun (word : List Bool) => (adversary n (choose n) word).eval) ((BitString.uniformList (seedBits n + 1)).bind fun (word : List Bool) => (adversary n (choose n) word).eval)) (adversary : ℕ → ℕ → List Bool → ProbComp Bool) : (Probability.IsPPTOn (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool fun (input : (ℕ × ℕ) × List Bool) => adversary input.1.1 input.1.2 input.2) → Negligible fun (n : ℕ) => Game.advantage ((PMF.map (iterate (generator n (choose n)) (seedBits n) (count n)) (BitString.uniformList (seedBits n))).bind fun (word : List Bool) => (adversary n (choose n) word).eval) ((BitString.uniformList (seedBits n + count n)).bind fun (word : List Bool) => (adversary n (choose n) word).eval)

Polynomially many expansions preserve the secure choice in a uniformly efficient family. The choice is supplied only in the proof; each reduction receives its index as ordinary input.

theorem Cslib.Crypto.PRGStretch.indistinguishable {generator : List Bool → List Bool} {count : ℕ → ℕ} (hgenerator : PseudorandomGenerator generator fun (n : ℕ) => n + 1) (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) : ComputationallyIndistinguishable (generatorEnsemble (stretch generator count)) fun (n : ℕ) => BitString.uniformList (n + count n)

Polynomially many seed expansions preserve computational indistinguishability.

theorem Cslib.Crypto.PRGStretch.pseudorandomGenerator {generator : List Bool → List Bool} {count : ℕ → ℕ} (hgenerator : PseudorandomGenerator generator fun (n : ℕ) => n + 1) (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hpositive : ∀ (n : ℕ), 0 < count n) : PseudorandomGenerator (stretch generator count) fun (n : ℕ) => n + count n

A positive efficiently computed number of one-bit expansions is a secure PRG.

theorem Cslib.Crypto.PseudorandomGenerator.amplify {generator : List Bool → List Bool} (hgenerator : PseudorandomGenerator generator fun (n : ℕ) => n + 1) (target : ℕ → ℕ) (htarget : Turing.MultiTapeTM.ComputableTidilyInPolyTime target Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hstretch : ∀ (n : ℕ), n < target n) : PseudorandomGenerator (PRGStretch.stretch generator fun (n : ℕ) => target n - n) target

Amplify a one-bit PRG to any efficiently computed, strictly larger output length.

theorem Cslib.Crypto.PseudorandomGenerator.truncate {generator : List Bool → List Bool} {length : ℕ → ℕ} (hgenerator : PseudorandomGenerator generator length) (target : ℕ → ℕ) (htarget : Turing.MultiTapeTM.ComputableTidilyInPolyTime target Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hle : ∀ (n : ℕ), target n ≤ length n) (hstretch : ∀ (n : ℕ), n < target n) : PseudorandomGenerator (fun (seed : List Bool) => List.take (target seed.length) (generator seed)) target

Truncating a PRG to an efficiently computed, still-expanding length preserves security.