Combining the entropy-grid candidates

Run every amplified candidate on a separate seed block and XOR the outputs. The result expands their total seed length by one bit. The secure choice from the entropy argument proves security; the program itself never chooses or estimates an entropy.

Main definitions

• combinedGenerate: run and XOR every amplified entropy-grid candidate.

Main results

• isPolyTime_combinedGenerate: one uniform implementation of the complete grid.
• length_combinedGenerate: output length is one bit beyond the grid's total seed cost.
• combinedGenerate_indistinguishable: security against every efficient test of the full output.

References

This completes the indexed construction of Thomas Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, TCC 2006, Section 5, final proof of Theorem 1, [Hol06]. The security parameter determines the seed length here. Extending this construction to every input length requires a separate reindexing argument.

Adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

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

Use one independent seed block per candidate and XOR the amplified outputs.

theorem Cslib.Crypto.Pseudoentropy.EntropyGrid.isPolyTime_combinedGenerate {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) => combinedGenerate input.1 (saved.length input.1) (observationBound input.1) (densityBound input.1) (common input.1) (saved.evaluate input.1) input.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits

The complete grid construction has one uniform polynomial-time implementation.

theorem Cslib.Crypto.Pseudoentropy.EntropyGrid.length_combinedGenerate (n sourceBits observationBound densityBound commonBits : ℕ) (evaluate : List Bool → List Bool × Bool) (seed : List Bool) : (combinedGenerate n sourceBits observationBound densityBound commonBits evaluate seed).length = size sourceBits densityBound * commonBits + 1

The output is one bit longer than the total cost of all the independent seed blocks.

theorem Cslib.Crypto.Pseudoentropy.EntropyGrid.combinedGenerate_indistinguishable {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) : ComputationallyIndistinguishable (fun (n : ℕ) => PMF.map (combinedGenerate n (saved.length n) (observationBound n) (densityBound n) (common n) (saved.evaluate n)) (BitString.uniformList (size (saved.length n) (densityBound n) * common n))) fun (n : ℕ) => BitString.uniformList (size (saved.length n) (densityBound n) * common n + 1)

One entropy-valid choice suffices for security of the complete, explicitly computed grid.