A common seed length for the entropy grid

One polynomial bounds the input sizes of all entropy-grid entries. Padding to that common length gives each candidate exactly one bit of stretch and preserves the secure choice against uniform indexed tests. The common length is increasing and at least the security parameter plus one, preparing later reindexing by the actual seed length.

Main definitions

• PaddingBounds: shared efficiency and size contract for the padding pipeline.
• paddedGenerate: normalize an entropy-grid entry to a common input length.

Main results

• exists_common_seedLength: one increasing efficient schedule bounds every entry's seed length.
• isPolyTime_paddedGenerate, length_paddedGenerate: efficient evaluation with one-bit stretch.
• exists_secure_padded_choice: padding preserves a choice secure against every uniform test.

References

This supplies the common-length candidate family used before amplification and XOR in Thomas Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, TCC 2006, Section 5, final proof of Theorem 1, [Hol06].

Adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

theorem Cslib.Crypto.Pseudoentropy.EntropyGrid.exists_common_seedLength {sourceBits observationBound densityBound : ℕ → ℕ} (hsource : Turing.MultiTapeTM.ComputableTidilyInPolyTime sourceBits Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hobservation : Turing.MultiTapeTM.ComputableTidilyInPolyTime observationBound Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hdensity : Turing.MultiTapeTM.ComputableTidilyInPolyTime densityBound Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) : ∃ (common : ℕ → ℕ), Turing.MultiTapeTM.ComputableTidilyInPolyTime common Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary ∧ StrictMono common ∧ (∀ (n : ℕ), n + 1 ≤ common n) ∧ ∀ (n index : ℕ), index < size (sourceBits n) (densityBound n) → seedLength n (sourceBits n) (observationBound n) (densityBound n) index ≤ common n

The entire grid fits one efficient increasing seed-length schedule.

structure Cslib.Crypto.Pseudoentropy.EntropyGrid.PaddingBounds {pair : SamplablePair} (saved : pair.SeedRealization) (observationBound densityBound common : ℕ → ℕ) : Prop

Efficient observation, entropy-resolution and common seed-length bounds for padding the entropy grid. The observation bound applies only on support; the seed bound covers every grid entry. Security assumptions and the entropy gap remain separate.

• observation_isPolyTime : Turing.MultiTapeTM.ComputableTidilyInPolyTime observationBound Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary
• density_isPolyTime : Turing.MultiTapeTM.ComputableTidilyInPolyTime densityBound Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary
• common_isPolyTime : Turing.MultiTapeTM.ComputableTidilyInPolyTime common Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary
• observation_fits (n : ℕ) (observation : pair.Observation n) : observation ∈ (PMF.map Prod.fst (pair.joint n)).support → ((pair.encode n) observation).length ≤ observationBound n
• seed_fits (n index : ℕ) : index < size (saved.length n) (densityBound n) → seedLength n (saved.length n) (observationBound n) (densityBound n) index ≤ common n

def Cslib.Crypto.Pseudoentropy.EntropyGrid.paddedGenerate (n sourceBits observationBound densityBound commonBits index : ℕ) (evaluate : List Bool → List Bool × Bool) (seed : List Bool) : List Bool

Normalize every grid entry to a chosen common seed length and one bit of stretch.

theorem Cslib.Crypto.Pseudoentropy.EntropyGrid.isPolyTime_paddedGenerate {pair : SamplablePair} (saved : pair.SeedRealization) {observationBound densityBound common : ℕ → ℕ} (hobservation : Turing.MultiTapeTM.ComputableTidilyInPolyTime observationBound Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hdensity : Turing.MultiTapeTM.ComputableTidilyInPolyTime densityBound Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hcommon : Turing.MultiTapeTM.ComputableTidilyInPolyTime common Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (input : (ℕ × ℕ) × List Bool) => paddedGenerate input.1.1 (saved.length input.1.1) (observationBound input.1.1) (densityBound input.1.1) (common input.1.1) input.1.2 (saved.evaluate input.1.1) input.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits

The padded family uses the same saved sampler and ordinary word operations.

theorem Cslib.Crypto.Pseudoentropy.EntropyGrid.length_paddedGenerate {pair : SamplablePair} (saved : pair.SeedRealization) (n observationBound densityBound commonBits index : ℕ) (hfits : ∀ observation ∈ (PMF.map Prod.fst (pair.joint n)).support, ((pair.encode n) observation).length ≤ observationBound) (hcommon : seedLength n (saved.length n) observationBound densityBound index ≤ commonBits) {seed : List Bool} (hseed : seed.length = commonBits) : (paddedGenerate n (saved.length n) observationBound densityBound commonBits index (saved.evaluate n) seed).length = commonBits + 1

Correctly sized common inputs give exactly one bit of stretch.

theorem Cslib.Crypto.Pseudoentropy.EntropyGrid.exists_secure_padded_choice {pair : SamplablePair} {gap : ℕ → ℝ} (hpair : pair.HasGap gap) (saved : pair.SeedRealization) {observationBound densityBound common : ℕ → ℕ} (bounds : PaddingBounds saved observationBound densityBound common) (hgap : ∀ᶠ (n : ℕ) in Filter.atTop, 4 / ↑(Probability.dyadicSize (densityBound n)) ≤ gap n) : ∃ (choose : ℕ → ℕ), (∀ᶠ (n : ℕ) in Filter.atTop, choose n < size (saved.length n) (densityBound n)) ∧ ∀ (test : ℕ → ℕ → 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) => test input.1.1 input.1.2 input.2) → Negligible fun (n : ℕ) => Game.advantage ((PMF.map (paddedGenerate n (saved.length n) (observationBound n) (densityBound n) (common n) (choose n) (saved.evaluate n)) (BitString.uniformList (common n))).bind fun (word : List Bool) => (test n (choose n) word).eval) ((BitString.uniformList (common n + 1)).bind fun (word : List Bool) => (test n (choose n) word).eval)

Padding preserves one secure choice against every uniform indexed test.