Uniform seeds for samplable pseudoentropy pairs

Every strict PPT sampler admits one polynomial-time deterministic evaluator driven by a uniform polynomial-length seed. SeedRealization exposes this algorithm while preserving the pair's exact finite joint law. Its output is the finite mathematical view used for entropy accounting.

The entropy chain rule accounts for every seed bit, including coins unused by the sampler: H(observation) + H(bit | observation) + H(seed | observation, bit) = seed length. Thus the third source in the later extraction argument retains the unused randomness too. The seed also bounds the information in a single outcome, giving an explicit exponential concentration bound for independent repetitions of the pair.

Main definitions

• Cslib.Crypto.Pseudoentropy.SamplablePair.SeedRealization: a uniformly efficient evaluator with the exact joint law on uniform seeds.
• Cslib.Crypto.Pseudoentropy.SamplablePair.SeedRealization.sampleWithSeed: return the evaluated pair together with every seed bit, including unused coins.
• Cslib.Crypto.Pseudoentropy.SamplablePair.SeedRealization.latentSampleWithSeed: the exact finite mathematical view, with no claim that observation decoding is efficient.

Main results

• Cslib.Crypto.Pseudoentropy.SamplablePair.exists_seedRealization: the sampler's existing strict PPT certificate supplies its deterministic evaluator.
• Cslib.Crypto.Pseudoentropy.SamplablePair.SeedRealization.entropy_chain_rule: account for the entire seed's entropy.

References

• T. Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, Definition 4 and Section 5. Shared machine replay supplies the uniform-seed presentation; the bounded-information concentration estimate depends on the complete seed length.

Adapted from Crypto/Computational/Pseudoentropy/Seed.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the existing typed saved-coin evaluator and tidy machine certificates. Positive pseudoentropy gaps and extraction remain separate developments.

theorem Cslib.Crypto.Pseudoentropy.SamplablePair.exists_observationBound (pair : SamplablePair) : ∃ (bound : ℕ → ℕ), Turing.MultiTapeTM.ComputableTidilyInPolyTime bound Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary ∧ ∀ (n : ℕ), ∀ observation ∈ (PMF.map Prod.fst (pair.joint n)).support, ((pair.encode n) observation).length ≤ bound n

A sampler's PPT certificate supplies an efficiently computed bound on every possible public observation. Impossible values in its finite observation type need no size bound.

structure Cslib.Crypto.Pseudoentropy.SamplablePair.SeedRealization (pair : SamplablePair) : Type

A plain polynomial-time evaluator from a uniform seed, with all input bits counted.

• length : ℕ → ℕ

  The complete number of seed bits at this parameter.

• length_isPolyTime : Turing.MultiTapeTM.ComputableInPolyTime self.length Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary

  The seed length is efficiently available in unary.

• evaluate : ℕ → List Bool → List Bool × Bool

  Evaluate the public observation and hidden bit from a saved seed.

• efficient : Turing.MultiTapeTM.ComputableInPolyTime (fun (input : ℕ × List Bool) => self.evaluate input.1 input.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool)

  Evaluation is one polynomial-time word program, also on malformed seeds.

• distribution (n : ℕ) : PMF.map (self.evaluate n) (BitString.uniformList (self.length n)) = PMF.map (fun (output : pair.Observation n × Bool) => ((pair.encode n) output.1, output.2)) (pair.joint n)

  Uniform seeds realize exactly the original finite joint law.

theorem Cslib.Crypto.Pseudoentropy.SamplablePair.SeedRealization.length_isPolyTime_tidy {pair : SamplablePair} (h : pair.SeedRealization) : Turing.MultiTapeTM.ComputableTidilyInPolyTime h.length Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary

The equivalent tidy contract used internally by compositional proofs.

theorem Cslib.Crypto.Pseudoentropy.SamplablePair.SeedRealization.efficient_tidy {pair : SamplablePair} (h : pair.SeedRealization) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (input : ℕ × List Bool) => h.evaluate input.1 input.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool)

The equivalent tidy contract used internally by compositional proofs.

theorem Cslib.Crypto.Pseudoentropy.SamplablePair.exists_seedRealization (pair : SamplablePair) : Nonempty pair.SeedRealization

A strict PPT sampler supplies an efficient uniform-seed realization with no additional computability or sampling assumption.

theorem Cslib.Crypto.Pseudoentropy.SamplablePair.SeedRealization.exists_supported_output {pair : SamplablePair} (seed : pair.SeedRealization) (n : ℕ) {word : List Bool} (hlength : word.length = seed.length n) : ∃ output ∈ (pair.joint n).support, ((pair.encode n) output.1, output.2) = seed.evaluate n word

Every well-formed seed produces an outcome in the support of the original finite law.

theorem Cslib.Crypto.Pseudoentropy.SamplablePair.SeedRealization.exists_output {pair : SamplablePair} (seed : pair.SeedRealization) (n : ℕ) (bits : Fin (seed.length n) → Bool) : ∃ (output : pair.Observation n × Bool), ((pair.encode n) output.1, output.2) = seed.evaluate n (List.ofFn bits)

Every well-formed seed produces an encoded observation and bit in the original finite law.

theorem Cslib.Crypto.Pseudoentropy.SamplablePair.SeedRealization.observation_length_le {pair : SamplablePair} (seed : pair.SeedRealization) (n bound : ℕ) (hbound : ∀ observation ∈ (PMF.map Prod.fst (pair.joint n)).support, ((pair.encode n) observation).length ≤ bound) {word : List Bool} (hlength : word.length = seed.length n) : (seed.evaluate n word).1.length ≤ bound

A bound on supported observations also bounds the evaluator on every correctly sized seed.

noncomputable def Cslib.Crypto.Pseudoentropy.SamplablePair.SeedRealization.output {pair : SamplablePair} (seed : pair.SeedRealization) (n : ℕ) (bits : Fin (seed.length n) → Bool) : pair.Observation n × Bool

The evaluator's finite mathematical output on a well-formed seed. No search over observations is run: its word representation is exactly the efficient evaluator's output.

theorem Cslib.Crypto.Pseudoentropy.SamplablePair.SeedRealization.encode_output {pair : SamplablePair} (seed : pair.SeedRealization) (n : ℕ) (bits : Fin (seed.length n) → Bool) : ((pair.encode n) (seed.output n bits).1, (seed.output n bits).2) = seed.evaluate n (List.ofFn bits)

The finite view preserves the evaluator's complete output, including the hidden bit.

theorem Cslib.Crypto.Pseudoentropy.SamplablePair.SeedRealization.output_distribution {pair : SamplablePair} (seed : pair.SeedRealization) (n : ℕ) : PMF.map (seed.output n) (Probability.PMF.uniformOfFintype (Fin (seed.length n) → Bool)) = pair.joint n

The uniform finite-seed presentation has the original joint law.

noncomputable def Cslib.Crypto.Pseudoentropy.SamplablePair.SeedRealization.jointWithSeed {pair : SamplablePair} (seed : pair.SeedRealization) (n : ℕ) : PMF ((pair.Observation n × Bool) × (Fin (seed.length n) → Bool))

Retain the complete sampler seed together with its finite output.

noncomputable def Cslib.Crypto.Pseudoentropy.SamplablePair.SeedRealization.latentSampleWithSeed {pair : SamplablePair} (seed : pair.SeedRealization) (n : ℕ) : ProbComp ((pair.Observation n × Bool) × (Fin (seed.length n) → Bool))

Sample the finite mathematical view and retain every original seed bit. This relabelling has no efficiency claim; sampleWithSeed below is its efficient encoded realization.

theorem Cslib.Crypto.Pseudoentropy.SamplablePair.SeedRealization.eval_latentSampleWithSeed {pair : SamplablePair} (seed : pair.SeedRealization) (n : ℕ) : (seed.latentSampleWithSeed n).eval = seed.jointWithSeed n

Finite uniform sampling realizes the complete latent output/seed law.

@[simp]

theorem Cslib.Crypto.Pseudoentropy.SamplablePair.SeedRealization.jointWithSeed_map_fst {pair : SamplablePair} (seed : pair.SeedRealization) (n : ℕ) : PMF.map Prod.fst (seed.jointWithSeed n) = pair.joint n

Forgetting the retained seed recovers the pair's original joint law.

theorem Cslib.Crypto.Pseudoentropy.SamplablePair.SeedRealization.jointWithSeed_mass_ge {pair : SamplablePair} (seed : pair.SeedRealization) (n : ℕ) (result : (pair.Observation n × Bool) × (Fin (seed.length n) → Bool)) (hresult : result ∈ (seed.jointWithSeed n).support) : 2 ^ (-↑(seed.length n)) ≤ ((seed.jointWithSeed n) result).toReal

Keeping the seed retains its full pointwise information bound.

noncomputable def Cslib.Crypto.Pseudoentropy.SamplablePair.SeedRealization.sampleWithSeed {pair : SamplablePair} (seed : pair.SeedRealization) (n : ℕ) : ProbComp ((List Bool × Bool) × List Bool)

An ordinary program returns the observation, label, and complete seed, including unused coins. The evaluator is the same deterministic program supplied by the sampler's certificate.

theorem Cslib.Crypto.Pseudoentropy.SamplablePair.SeedRealization.isPPTOn_sampleWithSeed {pair : SamplablePair} (seed : pair.SeedRealization) : Probability.IsPPTOn Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool) Turing.MultiTapeTM.encBits) seed.sampleWithSeed

Retaining the seed preserves strict PPT; no conditional sampling is performed.

theorem Cslib.Crypto.Pseudoentropy.SamplablePair.SeedRealization.eval_sampleWithSeed {pair : SamplablePair} (seed : pair.SeedRealization) (n : ℕ) : (seed.sampleWithSeed n).eval = PMF.map (fun (result : (pair.Observation n × Bool) × (Fin (seed.length n) → Bool)) => (((pair.encode n) result.1.1, result.1.2), List.ofFn result.2)) (seed.jointWithSeed n)

The efficient program exactly realizes the finite joint experiment with its retained seed.

theorem Cslib.Crypto.Pseudoentropy.SamplablePair.SeedRealization.mass_ge {pair : SamplablePair} (seed : pair.SeedRealization) (n : ℕ) (result : pair.Observation n × Bool) (hresult : result ∈ (pair.joint n).support) : 2 ^ (-↑(seed.length n)) ≤ ((pair.joint n) result).toReal

Every possible output has at least the probability of one complete seed.

theorem Cslib.Crypto.Pseudoentropy.SamplablePair.SeedRealization.conditionalSurprisal_concentration {pair : SamplablePair} (seed : pair.SeedRealization) (n repetitions : ℕ) {ε : ℝ} (hε : 0 ≤ ε) : ((Probability.PMF.pi fun (x : Fin repetitions) => pair.joint n).toOuterMeasure {outcomes : Fin repetitions → pair.Observation n × Bool | ∑ i : Fin repetitions, Probability.PMF.surprisal (Probability.PMF.conditionalSnd (pair.joint n) (outcomes i).1) (outcomes i).2 ≤ ↑repetitions * Probability.PMF.conditionalEntropy (pair.joint n) - ε}).toReal ≤ Real.exp (-2 * ε ^ 2 / (↑repetitions * ↑(seed.length n) ^ 2))

Independent repetitions concentrate their conditional information around the Shannon entropy of the pair. The loss accounts for the sampler's full saved seed length.

theorem Cslib.Crypto.Pseudoentropy.SamplablePair.SeedRealization.entropy_chain_rule {pair : SamplablePair} (seed : pair.SeedRealization) (n : ℕ) : Probability.PMF.entropy (PMF.map Prod.fst (pair.joint n)) + Probability.PMF.conditionalEntropy (pair.joint n) + Probability.PMF.conditionalEntropy (seed.jointWithSeed n) = ↑(seed.length n)

Revealing the observation and hidden bit leaves exactly the remaining seed entropy. This identity also counts coins that the sampler never inspected.