A polynomial repetition schedule for label extraction

The information bound is the sampler's seed length plus n + 2. Repeating 32 * (n + 1) * informationBits^2 * (inverseSlack + 1)^2 times makes the concentration error exponentially small. Reserving two entropy slacks also pays for leftover hashing. Neither choice depends on the distinguisher's polynomial degree.

Main definitions

• count, slack: polynomially computable repetition and entropy budgets.
• error: one negligible bound for concentration and leftover hashing.

Main results

• error_le: the entropy budget implies the common extraction-error bound.
• error_negligible: that bound decays faster than every inverse polynomial.

References

• Thomas Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, TCC 2006, Sections 3.3 and 5. [Hol06]. These explicit constants instantiate our seed-information concentration bound; they are not the optimized seed-length parameters in the write-up.

Adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using typed certificates and nonnegative errors.

def Cslib.Crypto.Pseudoentropy.ExtractionSchedule.count (n sourceBits inverseSlack : ℕ) : ℕ

A polynomial number of copies, fixed independently of the sequence distinguisher.

def Cslib.Crypto.Pseudoentropy.ExtractionSchedule.slack (n sourceBits inverseSlack : ℕ) : ℕ

Integer entropy slack for concentration; extraction reserves twice this amount.

theorem Cslib.Crypto.Pseudoentropy.ExtractionSchedule.isPolyTime_count {α : Type} {input : α ↪ List Bool} {n sourceBits inverseSlack : α → ℕ} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hsource : Turing.MultiTapeTM.ComputableTidilyInPolyTime sourceBits input Turing.MultiTapeTM.encUnary) (hslack : Turing.MultiTapeTM.ComputableTidilyInPolyTime inverseSlack input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => count (n a) (sourceBits a) (inverseSlack a)) input Turing.MultiTapeTM.encUnary

The repetition count is available in unary with polynomial cost.

theorem Cslib.Crypto.Pseudoentropy.ExtractionSchedule.isPolyTime_slack {α : Type} {input : α ↪ List Bool} {n sourceBits inverseSlack : α → ℕ} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hsource : Turing.MultiTapeTM.ComputableTidilyInPolyTime sourceBits input Turing.MultiTapeTM.encUnary) (hslack : Turing.MultiTapeTM.ComputableTidilyInPolyTime inverseSlack input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => slack (n a) (sourceBits a) (inverseSlack a)) input Turing.MultiTapeTM.encUnary

The integer slack is available in unary with polynomial cost.

theorem Cslib.Crypto.Pseudoentropy.ExtractionSchedule.two_slack_eq (n sourceBits inverseSlack : ℕ) : 2 * ↑(slack n sourceBits inverseSlack) = ↑(count n sourceBits inverseSlack) / (2 * (↑inverseSlack + 1))

Reserving two slacks costs exactly 1 / (2 * (inverseSlack + 1)) bits per sample.

noncomputable def Cslib.Crypto.Pseudoentropy.ExtractionSchedule.error (n : ℕ) : NNReal

One common exponential bound covers concentration and leftover hashing.

theorem Cslib.Crypto.Pseudoentropy.ExtractionSchedule.error_negligible : Negligible error

The explicit extraction error is negligible.

theorem Cslib.Crypto.Pseudoentropy.ExtractionSchedule.error_le (n sourceBits inverseSlack outputBits : ℕ) (density : ℝ) (hlength : ↑outputBits + 2 * ↑(slack n sourceBits inverseSlack) ≤ ↑(count n sourceBits inverseSlack) * density) : 2 * Real.exp (-2 * ↑(slack n sourceBits inverseSlack) ^ 2 / (↑(count n sourceBits inverseSlack) * ↑(sourceBits + n + 2) ^ 2)) + √(2 ^ outputBits * (2 * 2 ^ (-(↑(count n sourceBits inverseSlack) * density - ↑(slack n sourceBits inverseSlack))))) / 2 ≤ ↑(error n)

This schedule extracts below the density by two slacks with negligible error. The output length is an ordinary natural number; the density occurs only in the correctness premise.