Expanding candidates from a pseudoentropy pair

Each entropy-grid entry defines a deterministic polynomial-time expander with its exact seed length. One entry is secure against every uniform indexed test; its index may vary arbitrarily with the security parameter. The family is indexed by the whole finite grid and never computes entropy.

These raw candidates have different seed lengths. ThreeSource.Padding gives them a common seed length and one bit of stretch. Amplification and XOR combination are still needed to turn them into one generator.

Main definitions

• seedLength, outputLength, generate: exact lengths and evaluation of one entropy guess.

Main results

• isPolyTime_generate_of_realization: one efficient evaluator for the whole indexed family.
• seedLength_lt_outputLength, length_generate: strict expansion and exact output length.
• exists_secure_choice: a single proof-only choice works for every uniform indexed test.

References

• 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.

def Cslib.Crypto.Pseudoentropy.EntropyGrid.seedLength (n sourceBits observationBound densityBound index : ℕ) : ℕ

The exact seed length of a candidate, including all three public matrix keys.

def Cslib.Crypto.Pseudoentropy.EntropyGrid.outputLength (n sourceBits observationBound densityBound index : ℕ) : ℕ

The candidate's output keeps every matrix key and the three digests.

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

A candidate is the deterministic three-source extractor at one entropy guess.

theorem Cslib.Crypto.Pseudoentropy.EntropyGrid.isPolyTime_seedLength {α : Type} {input : α ↪ List Bool} {n sourceBits observationBound densityBound index : α → ℕ} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hsource : Turing.MultiTapeTM.ComputableTidilyInPolyTime sourceBits input Turing.MultiTapeTM.encUnary) (hobservation : Turing.MultiTapeTM.ComputableTidilyInPolyTime observationBound input Turing.MultiTapeTM.encUnary) (hdensity : Turing.MultiTapeTM.ComputableTidilyInPolyTime densityBound input Turing.MultiTapeTM.encUnary) (hindex : Turing.MultiTapeTM.ComputableTidilyInPolyTime index input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => seedLength (n a) (sourceBits a) (observationBound a) (densityBound a) (index a)) input Turing.MultiTapeTM.encUnary

The exact input size is uniformly available in unary.

theorem Cslib.Crypto.Pseudoentropy.EntropyGrid.isPolyTime_outputLength {α : Type} {input : α ↪ List Bool} {n sourceBits observationBound densityBound index : α → ℕ} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hsource : Turing.MultiTapeTM.ComputableTidilyInPolyTime sourceBits input Turing.MultiTapeTM.encUnary) (hobservation : Turing.MultiTapeTM.ComputableTidilyInPolyTime observationBound input Turing.MultiTapeTM.encUnary) (hdensity : Turing.MultiTapeTM.ComputableTidilyInPolyTime densityBound input Turing.MultiTapeTM.encUnary) (hindex : Turing.MultiTapeTM.ComputableTidilyInPolyTime index input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => outputLength (n a) (sourceBits a) (observationBound a) (densityBound a) (index a)) input Turing.MultiTapeTM.encUnary

The exact output size is uniformly available in unary.

theorem Cslib.Crypto.Pseudoentropy.EntropyGrid.isPolyTime_generate {α : Type} {input : α ↪ List Bool} {n sourceBits observationBound densityBound index : α → ℕ} {evaluate : α → List Bool → List Bool × Bool} {seed : α → List Bool} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hsource : Turing.MultiTapeTM.ComputableTidilyInPolyTime sourceBits input Turing.MultiTapeTM.encUnary) (hobservation : Turing.MultiTapeTM.ComputableTidilyInPolyTime observationBound input Turing.MultiTapeTM.encUnary) (hdensity : Turing.MultiTapeTM.ComputableTidilyInPolyTime densityBound input Turing.MultiTapeTM.encUnary) (hindex : Turing.MultiTapeTM.ComputableTidilyInPolyTime index input Turing.MultiTapeTM.encUnary) (hevaluate : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α × List Bool) => evaluate a.1 a.2) (Turing.MultiTapeTM.encPair input Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool)) (hseed : Turing.MultiTapeTM.ComputableTidilyInPolyTime seed input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => generate (n a) (sourceBits a) (observationBound a) (densityBound a) (index a) (evaluate a) (seed a)) input Turing.MultiTapeTM.encBits

Candidate evaluation is uniformly polynomial time, with an ordinary captured callback.

theorem Cslib.Crypto.Pseudoentropy.EntropyGrid.isPolyTime_generate_of_realization {pair : SamplablePair} (saved : pair.SeedRealization) {observationBound densityBound : ℕ → ℕ} (hobservation : Turing.MultiTapeTM.ComputableTidilyInPolyTime observationBound Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hdensity : Turing.MultiTapeTM.ComputableTidilyInPolyTime densityBound Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (input : (ℕ × ℕ) × List Bool) => generate input.1.1 (saved.length input.1.1) (observationBound input.1.1) (densityBound 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

A saved sampler gives one efficient evaluator for the entire indexed family.

theorem Cslib.Crypto.Pseudoentropy.EntropyGrid.seedLength_lt_outputLength (n sourceBits observationBound densityBound index : ℕ) : seedLength n sourceBits observationBound densityBound index < outputLength n sourceBits observationBound densityBound index

The advertised lengths give strict expansion for every entry, even an inaccurate guess.

theorem Cslib.Crypto.Pseudoentropy.EntropyGrid.length_generate {pair : SamplablePair} (saved : pair.SeedRealization) (n observationBound densityBound index : ℕ) (hbound : ∀ observation ∈ (PMF.map Prod.fst (pair.joint n)).support, ((pair.encode n) observation).length ≤ observationBound) {seed : List Bool} (hseed : seed.length = seedLength n (saved.length n) observationBound densityBound index) : (generate n (saved.length n) observationBound densityBound index (saved.evaluate n) seed).length = outputLength n (saved.length n) observationBound densityBound index

Every correctly sized input has exactly the advertised output length.

theorem Cslib.Crypto.Pseudoentropy.EntropyGrid.exists_valid_choice {pair : SamplablePair} {gap : ℕ → ℝ} (hpair : pair.HasGap gap) (saved : pair.SeedRealization) {densityBound : ℕ → ℕ} (hgap : ∀ᶠ (n : ℕ) in Filter.atTop, 4 / ↑(Probability.dyadicSize (densityBound n)) ≤ gap n) : ∃ (choose : ℕ → ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, Valid n (saved.length n) (densityBound n) (choose n) (Probability.PMF.entropy (PMF.map Prod.fst (pair.joint n))) (Probability.PMF.conditionalEntropy (pair.joint n)) (gap n)

Every sufficiently fine grid contains a valid entry, with no entropy estimation required.

theorem Cslib.Crypto.Pseudoentropy.EntropyGrid.exists_secure_choice {pair : SamplablePair} {gap : ℕ → ℝ} (hpair : pair.HasGap gap) (saved : pair.SeedRealization) {observationBound densityBound : ℕ → ℕ} (hobservation : Turing.MultiTapeTM.ComputableTidilyInPolyTime observationBound Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hdensity : Turing.MultiTapeTM.ComputableTidilyInPolyTime densityBound Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hfits : ∀ (n : ℕ), ∀ observation ∈ (PMF.map Prod.fst (pair.joint n)).support, ((pair.encode n) observation).length ≤ observationBound n) (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 (generate n (saved.length n) (observationBound n) (densityBound n) (choose n) (saved.evaluate n)) (BitString.uniformList (seedLength n (saved.length n) (observationBound n) (densityBound n) (choose n)))).bind fun (word : List Bool) => (test n (choose n) word).eval) ((BitString.uniformList (outputLength n (saved.length n) (observationBound n) (densityBound n) (choose n))).bind fun (word : List Bool) => (test n (choose n) word).eval)

A single varying candidate is secure against every uniform indexed test. The choice is made before the test is quantified and is used only in the proof, never by generate.

theorem Cslib.Crypto.Pseudoentropy.EntropyGrid.four_steps_le_owf_gap (n : ℕ) : 4 / ↑(Probability.dyadicSize (16 * (n + 7))) ≤ 1 / (2 * (↑n + 7))

A linear grid precision suffices for the gap already obtained from a general one-way function. This is a numerical consequence of rounding the denominator up to a power of two.