Extending an expanding family to every seed length

Choose the largest parameter whose seed fits the input, run that family member on a prefix, and retain the unused suffix. A finite initial range uses a trivial one-bit extension. The schedule need not be monotone. Bounded search is efficient, and adjacent parameters give the polynomial relation needed to preserve negligible decay.

Security uses ComputationallyIndistinguishable.uniform_bound: the padding test receives the prospective input length as an ordinary index, and one negligible bound covers all relevant lengths. No nonuniform choice of a bad length is supplied to the reduction.

Main definitions

• Cslib.Crypto.GeneratorReindex.parameter: bounded search for the greatest fitting parameter.
• Cslib.Crypto.GeneratorReindex.generate: prefix generation with the unused suffix preserved.

Main results

• Cslib.Crypto.GeneratorReindex.isPolyTime_generate: uniform machine-backed efficiency.
• Cslib.Crypto.GeneratorReindex.pseudorandomGenerator: one-bit stretch at every seed length.

References

This completes the seed-length convention for the construction in T. Holenstein, Pseudorandom Generators from One-Way Functions, Section 5.

Adapted from Crypto/Computational/GeneratorReindex.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using typed machine certificates and the nonnegative game API.

def Cslib.Crypto.GeneratorReindex.parameter (length : ℕ → ℕ) (size : ℕ) : ℕ

The greatest parameter at most size whose prescribed seed fits, or zero when none fits.

theorem Cslib.Crypto.GeneratorReindex.isPolyTime_parameter {α : Type} {input : α ↪ List Bool} {length : ℕ → ℕ} {size : α → ℕ} (hlength : Turing.MultiTapeTM.ComputableTidilyInPolyTime length Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hsize : Turing.MultiTapeTM.ComputableTidilyInPolyTime size input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => parameter length (size a)) input Turing.MultiTapeTM.encUnary

Searching an efficient schedule up to an efficient unary input size is polynomial-time.

theorem Cslib.Crypto.GeneratorReindex.parameter_le (length : ℕ → ℕ) (size : ℕ) : parameter length size ≤ size

The bounded search never returns a parameter above its input size.

theorem Cslib.Crypto.GeneratorReindex.parameter_fits {length : ℕ → ℕ} {size : ℕ} (hsize : length 0 ≤ size) : length (parameter length size) ≤ size

Once the zeroth seed fits, the selected seed fits too.

theorem Cslib.Crypto.GeneratorReindex.lt_length_succ_parameter {length : ℕ → ℕ} (hge : ∀ (n : ℕ), n + 1 ≤ length n) (size : ℕ) : size < length (parameter length size + 1)

The next parameter's seed is too large, even when the schedule is not monotone.

theorem Cslib.Crypto.GeneratorReindex.parameter_tendsto (length : ℕ → ℕ) : Filter.Tendsto (parameter length) Filter.atTop Filter.atTop

Every fixed parameter eventually fits, so the selected parameter tends to infinity.

def Cslib.Crypto.GeneratorReindex.generate (length : ℕ → ℕ) (generator : ℕ → List Bool → List Bool) (seed : List Bool) : List Bool

Search for a family member that fits, then preserve the remaining seed bits as padding.

theorem Cslib.Crypto.GeneratorReindex.isPolyTime_generate {length : ℕ → ℕ} {generator : ℕ → List Bool → List Bool} (hlength : Turing.MultiTapeTM.ComputableTidilyInPolyTime length Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hgenerator : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : ℕ × List Bool) => generator a.1 a.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (generate length generator) Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits

Generation composes bounded search, the supplied family, and padding.

theorem Cslib.Crypto.GeneratorReindex.length_generate {length : ℕ → ℕ} {generator : ℕ → List Bool → List Bool} (houtput : ∀ (n : ℕ) (seed : List Bool), seed.length = length n → (generator n seed).length = length n + 1) (seed : List Bool) : (generate length generator seed).length = seed.length + 1

Every input is expanded by exactly one bit, including the finite initial range.

theorem Cslib.Crypto.GeneratorReindex.generate_distribution (length : ℕ → ℕ) (generator : ℕ → List Bool → List Bool) {size : ℕ} (hsize : length 0 ≤ size) : generatorEnsemble (generate length generator) size = PMF.map (GeneratorPadding.generate (length (parameter length size)) size (generator (parameter length size))) (BitString.uniformList size)

At a fixed seed length, the reindexed ensemble is exactly the corresponding padded family.

theorem Cslib.Crypto.GeneratorReindex.indistinguishable {length : ℕ → ℕ} {generator : ℕ → List Bool → List Bool} (hlength : Turing.MultiTapeTM.ComputableTidilyInPolyTime length Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hge : ∀ (n : ℕ), n + 1 ≤ length n) (hgenerator : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : ℕ × List Bool) => generator a.1 a.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hsecure : ComputationallyIndistinguishable (fun (n : ℕ) => PMF.map (generator n) (BitString.uniformList (length n))) fun (n : ℕ) => BitString.uniformList (length n + 1)) : ComputationallyIndistinguishable (generatorEnsemble (generate length generator)) fun (n : ℕ) => BitString.uniformList (n + 1)

Extending a uniformly efficient secure family preserves uniform security at every seed length. A single calibrated reduction controls every padding length in the polynomial range.

theorem Cslib.Crypto.GeneratorReindex.pseudorandomGenerator {length : ℕ → ℕ} {generator : ℕ → List Bool → List Bool} (hlength : Turing.MultiTapeTM.ComputableTidilyInPolyTime length Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hge : ∀ (n : ℕ), n + 1 ≤ length n) (hgenerator : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : ℕ × List Bool) => generator a.1 a.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (houtput : ∀ (n : ℕ) (seed : List Bool), seed.length = length n → (generator n seed).length = length n + 1) (hsecure : ComputationallyIndistinguishable (fun (n : ℕ) => PMF.map (generator n) (BitString.uniformList (length n))) fun (n : ℕ) => BitString.uniformList (length n + 1)) : PseudorandomGenerator (generate length generator) fun (n : ℕ) => n + 1

A uniformly efficient one-bit expanding family on a polynomial schedule gives a PRG stretching every input by one bit.