Computational extraction of a pseudoentropy pair's labels

The dense-mask theorem supplies a comparison experiment for each efficient sequence test. Extraction makes that experiment statistically uniform. Its information budget is the sampler's seed length plus n + 2, independently of the test's polynomial running-time degree.

The theorem retains all observations and the hash seed. HasGap.extract_indexed_labels instantiates a polynomial repetition schedule and proves its error negligible, leaving only the entropy budget and admissible density conditions. A valid index may be chosen arbitrarily at each parameter; the efficient reduction handles all indices. The generator must still combine the candidates.

Main results

• HasGap.indexed_extracted_advantage_negligible: dense masks give negligible extraction advantage for any valid choices from a uniformly efficient indexed family.
• HasGap.extract_indexed_labels: the fixed polynomial schedule pays the full statistical loss.

References

• Thomas Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, TCC 2006, Section 5, the transition from Game 2 through Game 5. [Hol06]. We use fresh soft masks and the checked strict PPT sequence learner.

Adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

theorem Cslib.Crypto.Pseudoentropy.SamplablePair.HasGap.indexed_extracted_advantage_negligible {pair : SamplablePair} {gap : ℕ → ℝ} (hpair : pair.HasGap gap) (realization : pair.SeedRealization) (choose : ℕ → ℕ) {Seed Output : ℕ → ℕ → Type} [(n i : ℕ) → Fintype (Seed n i)] [(n i : ℕ) → Fintype (Output n i)] [∀ (n i : ℕ), Nonempty (Output n i)] (seed : (n i : ℕ) → ProbComp (Seed n i)) (hash : (n i : ℕ) → Seed n i → List Bool → Output n i) (test : (n i : ℕ) → List (List Bool) × Seed n i × Output n i → ProbComp Bool) (htest : Probability.IsPPTOn (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool))) Turing.MultiTapeTM.encBool fun (input : (ℕ × ℕ) × List (List Bool × Bool)) => extractLabels (seed input.1.1 input.1.2) (hash input.1.1 input.1.2) input.2 >>= test input.1.1 input.1.2) {candidates count densityBound : ℕ → ℕ} {numerator : ℕ → ℕ → ℕ} {slack : ℕ → ℝ} (hcandidates : Turing.MultiTapeTM.ComputableTidilyInPolyTime candidates Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hnumerator : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (input : ℕ × ℕ) => numerator input.1 input.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encUnary) (hdensity : Turing.MultiTapeTM.ComputableTidilyInPolyTime densityBound Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hchoose : ∀ᶠ (n : ℕ) in Filter.atTop, choose n < candidates n) (hvalid : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < numerator n (choose n) ∧ numerator n (choose n) ≤ Probability.dyadicSize (densityBound n) ∧ ↑(numerator n (choose n)) / ↑(Probability.dyadicSize (densityBound n)) ≤ Probability.PMF.conditionalEntropy (pair.joint n) + gap n) (hhash : ∀ (n i : ℕ), Probability.IsTwoUniversal (seed n i).eval fun (s : Seed n i) (bits : BitString (count n)) => hash n i s (List.ofFn bits)) (hslack : ∀ (n : ℕ), 0 ≤ slack n) (herror : Negligible fun (n : ℕ) => (2 * Real.exp (-2 * slack n ^ 2 / (↑(count n) * ↑(realization.length n + n + 2) ^ 2)) + √(↑(Fintype.card (Output n (choose n))) * (2 * 2 ^ (-(↑(count n) * (↑(numerator n (choose n)) / ↑(Probability.dyadicSize (densityBound n))) - slack n)))) / 2).toNNReal) : Negligible fun (n : ℕ) => Game.advantage (do let samples ← OracleComp.replicate (count n) (pair.sample n) let result ← extractLabels (seed n (choose n)) (hash n (choose n)) samples test n (choose n) result).eval ((extractLabelsIdeal ((fun (value : pair.Observation n × Bool) => (pair.encode n) value.1) <$> pair.latentSample n) (count n) (seed n (choose n))).bind fun (output : List (List Bool) × Seed n (choose n) × Output n (choose n)) => (test n (choose n) output).eval)

Label extraction is computationally uniform along any valid choices from an efficient polynomial-size family. The choices need not be computable: the reduction handles all indices uniformly, and only the proof uses the chosen index. Observations and hash seeds stay public.

theorem Cslib.Crypto.Pseudoentropy.SamplablePair.HasGap.extract_indexed_labels {pair : SamplablePair} {gap : ℕ → ℝ} (hpair : pair.HasGap gap) (realization : pair.SeedRealization) (choose : ℕ → ℕ) {Seed : ℕ → ℕ → Type} [(n i : ℕ) → Fintype (Seed n i)] {outputBits : ℕ → ℕ → ℕ} {candidates inverseSlack : ℕ → ℕ} (seed : (n i : ℕ) → ProbComp (Seed n i)) (hash : (n i : ℕ) → Seed n i → List Bool → BitString (outputBits n i)) (test : (n i : ℕ) → List (List Bool) × Seed n i × BitString (outputBits n i) → ProbComp Bool) (htest : Probability.IsPPTOn (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool))) Turing.MultiTapeTM.encBool fun (input : (ℕ × ℕ) × List (List Bool × Bool)) => extractLabels (seed input.1.1 input.1.2) (hash input.1.1 input.1.2) input.2 >>= test input.1.1 input.1.2) (hcandidates : Turing.MultiTapeTM.ComputableTidilyInPolyTime candidates Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hslack : Turing.MultiTapeTM.ComputableTidilyInPolyTime inverseSlack Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) {numerator : ℕ → ℕ → ℕ} {densityBound : ℕ → ℕ} (hnumerator : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (input : ℕ × ℕ) => numerator input.1 input.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encUnary) (hdensity : Turing.MultiTapeTM.ComputableTidilyInPolyTime densityBound Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hchoose : ∀ᶠ (n : ℕ) in Filter.atTop, choose n < candidates n) (hvalid : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < numerator n (choose n) ∧ numerator n (choose n) ≤ Probability.dyadicSize (densityBound n) ∧ ↑(numerator n (choose n)) / ↑(Probability.dyadicSize (densityBound n)) ≤ Probability.PMF.conditionalEntropy (pair.joint n) + gap n) (hhash : ∀ (n i : ℕ), Probability.IsTwoUniversal (seed n i).eval fun (s : Seed n i) (bits : BitString (ExtractionSchedule.count n (realization.length n) (inverseSlack n))) => hash n i s (List.ofFn bits)) (hbudget : ∀ᶠ (n : ℕ) in Filter.atTop, ↑(outputBits n (choose n)) + 2 * ↑(ExtractionSchedule.slack n (realization.length n) (inverseSlack n)) ≤ ↑(ExtractionSchedule.count n (realization.length n) (inverseSlack n)) * (↑(numerator n (choose n)) / ↑(Probability.dyadicSize (densityBound n)))) : Negligible fun (n : ℕ) => Game.advantage (do let samples ← OracleComp.replicate (ExtractionSchedule.count n (realization.length n) (inverseSlack n)) (pair.sample n) let result ← extractLabels (seed n (choose n)) (hash n (choose n)) samples test n (choose n) result).eval ((extractLabelsIdeal ((fun (value : pair.Observation n × Bool) => (pair.encode n) value.1) <$> pair.latentSample n) (ExtractionSchedule.count n (realization.length n) (inverseSlack n)) (seed n (choose n))).bind fun (output : List (List Bool) × Seed n (choose n) × BitString (outputBits n (choose n))) => (test n (choose n) output).eval)

The explicit repetition schedule makes any valid indexed label extractor computationally uniform. Only the proof uses the chosen indices; the sampler, hash, and test form one uniformly efficient family. The entropy budget discharges the complete statistical error.