Amplifying the entropy-grid candidates

Each padded candidate is iterated until its output is one bit longer than all the candidates' independent seeds together. The uniformly randomized stretching reduction preserves the secure choice, with polynomial loss. This prepares XOR combination without computing that choice.

Main definitions

• amplifiedGenerate: iterate a candidate to cover the full grid's independent seed cost.

Main results

• isPolyTime_amplifiedGenerate: a uniform certificate for the indexed family.
• length_amplifiedGenerate: exact output length, one bit beyond the total seed cost.
• exists_secure_amplified_choice: amplification preserves the proof-only secure choice.

References

We follow 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.amplifiedGenerate (n sourceBits observationBound densityBound commonBits index : ℕ) (evaluate : List Bool → List Bool × Bool) (seed : List Bool) : List Bool

Amplify one candidate enough to pay for all candidates' independent seeds.

theorem Cslib.Crypto.Pseudoentropy.EntropyGrid.isPolyTime_amplifiedGenerate {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) => amplifiedGenerate 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 entire amplified family is uniformly efficient, including on malformed seed inputs.

theorem Cslib.Crypto.Pseudoentropy.EntropyGrid.length_amplifiedGenerate {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) : (amplifiedGenerate n (saved.length n) observationBound densityBound commonBits index (saved.evaluate n) seed).length = size (saved.length n) densityBound * commonBits + 1

Every enumerated candidate outputs one more bit than the total seed cost of the grid.

theorem Cslib.Crypto.Pseudoentropy.EntropyGrid.exists_secure_amplified_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 (amplifiedGenerate 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 (size (saved.length n) (densityBound n) * common n + 1)).bind fun (word : List Bool) => (test n (choose n) word).eval)

Amplification preserves one choice secure against every uniform indexed test.