Samplable pseudoentropy pairs

A pair consists of a public observation and a hidden bit. The observation has a finite type at each parameter and an injective word encoding, so its conditional entropy is unambiguous. A strict PPT sampler realizes the joint law exactly.

SamplablePair.HasGap says that every uniform PPT predictor eventually has signed correlation at most 1 - H(hidden | observation) - gap. This is the entropy threshold used in the OWF-to-PRG construction; merely being hard to predict is not sufficient.

This interface records the joint law and its sampler. The shared saved-coin interface exposes a strict PPT sampler's fair-bit tape as a uniform seed, including unused randomness.

Main definitions

• Cslib.Crypto.Pseudoentropy.predictionGame: predict a sampled hidden bit from its observation.
• Cslib.Crypto.Pseudoentropy.SamplablePair: a finite joint law with a uniform strict PPT sampler.
• Cslib.Crypto.Pseudoentropy.SamplablePair.HasGap: the conditional-entropy prediction threshold.

Main results

• Cslib.Crypto.Pseudoentropy.SamplablePair.eval_latentSample: recover the exact latent joint law.
• Cslib.Crypto.Pseudoentropy.SamplablePair.HasGap.eventually_error_ge: prediction error bound.
• Cslib.Crypto.Pseudoentropy.SamplablePair.HasGap.eventually_entropy_add_gap_le_one: the threshold forced by an independent fair-bit predictor.

References

• T. Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, Definitions 3 and 4. We use a sampler presentation and uniform strict PPT predictors. Signed correlation is twice success probability minus one.

Adapted from Crypto/Computational/Pseudoentropy/Basic.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the shared nonnegative game API and tidy machine certificates. Existence of a pair with a positive gap is a separate security theorem.

def Cslib.Crypto.Pseudoentropy.predictionGame (sample : ℕ → ProbComp (List Bool × Bool)) (adversary : Distinguisher) (n : ℕ) : ProbComp Bool

Predict the hidden bit from the public component of a sampled pair.

theorem Cslib.Crypto.Pseudoentropy.isPPTOn_predictionGame {sample : ℕ → ProbComp (List Bool × Bool)} (hsample : Probability.IsPPTOn Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool) sample) {adversary : Distinguisher} (hadversary : Probability.IsPPT Turing.MultiTapeTM.encBool adversary) : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool (predictionGame sample adversary)

The complete prediction experiment is strict PPT whenever the sampler and predictor are.

structure Cslib.Crypto.Pseudoentropy.SamplablePair : Type 1

A finite joint law together with its exact strict PPT word sampler.

• Observation : ℕ → Type

  The public information available at each parameter.

• finite (n : ℕ) : Finite (self.Observation n)

  Its alphabet is finite, without requiring a computable enumeration.

• encode (n : ℕ) : self.Observation n ↪ List Bool

  Encoding preserves all the public information.

• joint (n : ℕ) : PMF (self.Observation n × Bool)

  The public observation and hidden bit.

• sample : ℕ → ProbComp (List Bool × Bool)

  A word-level sampler with the strict fair-coin realization certified below.

• efficient : Probability.IsPPTOn Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool) self.sample

  Its complete running time is bounded by one polynomial.

• eval_sample (n : ℕ) : (self.sample n).eval = PMF.map (fun (pair : self.Observation n × Bool) => ((self.encode n) pair.1, pair.2)) (self.joint n)

  The sampler realizes the finite joint law exactly.

noncomputable def Cslib.Crypto.Pseudoentropy.SamplablePair.latentSample (pair : SamplablePair) (n : ℕ) : ProbComp (pair.Observation n × Bool)

Recover the latent draw by relabelling the existing sampler. This is a mathematical program, with no efficiency claim for decoding arbitrary observation encodings.

theorem Cslib.Crypto.Pseudoentropy.SamplablePair.eval_latentSample (pair : SamplablePair) (n : ℕ) : (pair.latentSample n).eval = pair.joint n

The recovered sample has exactly the joint law, including its hidden label.

def Cslib.Crypto.Pseudoentropy.SamplablePair.HasGap (pair : SamplablePair) (gap : ℕ → ℝ) : Prop

Every uniform PPT predictor stays below the conditional-entropy threshold by this gap. The threshold beyond which the inequality holds may depend on the predictor.

theorem Cslib.Crypto.Pseudoentropy.SamplablePair.HasGap.eventually_error_ge {pair : SamplablePair} {gap : ℕ → ℝ} (hgap : pair.HasGap gap) (adversary : Distinguisher) (hefficient : Probability.IsPPT Turing.MultiTapeTM.encBool adversary) : ∀ᶠ (n : ℕ) in Filter.atTop, (Probability.PMF.conditionalEntropy (pair.joint n) + gap n) / 2 ≤ ((predictionGame pair.sample adversary n).eval false).toReal

The pseudoentropy threshold equivalently lower-bounds each efficient predictor's error.

theorem Cslib.Crypto.Pseudoentropy.SamplablePair.HasGap.eventually_entropy_add_gap_le_one {pair : SamplablePair} {gap : ℕ → ℝ} (hgap : pair.HasGap gap) : ∀ᶠ (n : ℕ) in Filter.atTop, Probability.PMF.conditionalEntropy (pair.joint n) + gap n ≤ 1

A fair-bit predictor has zero correlation, so entropy plus the prediction gap cannot eventually exceed one.

theorem Cslib.Crypto.Pseudoentropy.SamplablePair.HasGap.mono {pair : SamplablePair} {gap smaller : ℕ → ℝ} (h : pair.HasGap gap) (hle : ∀ (n : ℕ), smaller n ≤ gap n) : pair.HasGap smaller

A smaller requested gap follows from any larger proved gap.