Deterministic three-source extraction

The input contains exactly the original sampler seeds and three independent matrix seeds. Ordinary word operations split this tape and evaluate the same hashes as the probabilistic program. The implementation uses the shared row parser and polynomial-time combinators.

Main definitions

• hashSamples: evaluate the three hashes with supplied keys, retaining each key.
• generate: parse one input seed and run the deterministic construction.

Main results

• isPolyTime_generate: runtime dimensions and a captured evaluator compose efficiently.
• eval_generate, eval_generate_of_realization: equality with the sampled extractor.
• length_generate: every correctly sized seed produces the declared number of output bits.

References

• Thomas Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, TCC 2006, Section 5, Lemma 5. [Hol06]. The matrix seeds are retained in full, so their lengths cancel from the expansion budget.

Adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using typed certificates and the shared list-row parser.

def Cslib.Crypto.Pseudoentropy.ThreeSource.hashSamples (count seedBits bound observationBits labelBits remainingBits : ℕ) (samples : List ((List Bool × Bool) × List Bool)) (firstKey middleKey lastKey : List Bool) : List Bool

Evaluate the three hashes using supplied matrix seeds, preserving all three seeds.

theorem Cslib.Crypto.Pseudoentropy.ThreeSource.isPolyTime_hashSamples {α : Type} {input : α ↪ List Bool} {count seedBits bound observationBits labelBits remainingBits : α → ℕ} {samples : α → List ((List Bool × Bool) × List Bool)} {firstKey middleKey lastKey : α → List Bool} (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (hseed : Turing.MultiTapeTM.ComputableTidilyInPolyTime seedBits input Turing.MultiTapeTM.encUnary) (hbound : Turing.MultiTapeTM.ComputableTidilyInPolyTime bound input Turing.MultiTapeTM.encUnary) (hobservation : Turing.MultiTapeTM.ComputableTidilyInPolyTime observationBits input Turing.MultiTapeTM.encUnary) (hlabel : Turing.MultiTapeTM.ComputableTidilyInPolyTime labelBits input Turing.MultiTapeTM.encUnary) (hremaining : Turing.MultiTapeTM.ComputableTidilyInPolyTime remainingBits input Turing.MultiTapeTM.encUnary) (hsamples : Turing.MultiTapeTM.ComputableTidilyInPolyTime samples input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool) Turing.MultiTapeTM.encBits))) (hfirst : Turing.MultiTapeTM.ComputableTidilyInPolyTime firstKey input Turing.MultiTapeTM.encBits) (hmiddle : Turing.MultiTapeTM.ComputableTidilyInPolyTime middleKey input Turing.MultiTapeTM.encBits) (hlast : Turing.MultiTapeTM.ComputableTidilyInPolyTime lastKey input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => hashSamples (count a) (seedBits a) (bound a) (observationBits a) (labelBits a) (remainingBits a) (samples a) (firstKey a) (middleKey a) (lastKey a)) input Turing.MultiTapeTM.encBits

Deterministic hashing composes the same efficient word operations as the sampled program.

def Cslib.Crypto.Pseudoentropy.ThreeSource.generate (count seedBits bound observationBits labelBits remainingBits : ℕ) (evaluate : List Bool → List Bool × Bool) (tape : List Bool) : List Bool

Evaluate from one seed: sampler coins, remaining-seed matrix, label matrix, observation matrix. Parsing is total even on short input tapes; exact sampling laws use seedLength input bits.

theorem Cslib.Crypto.Pseudoentropy.ThreeSource.isPolyTime_generate {α : Type} {input : α ↪ List Bool} {count seedBits bound observationBits labelBits remainingBits : α → ℕ} {evaluate : α → List Bool → List Bool × Bool} {tape : α → List Bool} (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (hseed : Turing.MultiTapeTM.ComputableTidilyInPolyTime seedBits input Turing.MultiTapeTM.encUnary) (hbound : Turing.MultiTapeTM.ComputableTidilyInPolyTime bound input Turing.MultiTapeTM.encUnary) (hobservation : Turing.MultiTapeTM.ComputableTidilyInPolyTime observationBits input Turing.MultiTapeTM.encUnary) (hlabel : Turing.MultiTapeTM.ComputableTidilyInPolyTime labelBits input Turing.MultiTapeTM.encUnary) (hremaining : Turing.MultiTapeTM.ComputableTidilyInPolyTime remainingBits input Turing.MultiTapeTM.encUnary) (hevaluate : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α × List Bool) => evaluate a.1 a.2) (Turing.MultiTapeTM.encPair input Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool)) (htape : Turing.MultiTapeTM.ComputableTidilyInPolyTime tape input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => generate (count a) (seedBits a) (bound a) (observationBits a) (labelBits a) (remainingBits a) (evaluate a) (tape a)) input Turing.MultiTapeTM.encBits

Runtime dimensions, parsing, and every evaluator call are charged through ordinary polynomial-time combinators. The callback may capture the original input.

theorem Cslib.Crypto.Pseudoentropy.ThreeSource.generate_distribution (count seedBits bound observationBits labelBits remainingBits : ℕ) (evaluate : List Bool → List Bool × Bool) : PMF.map (generate count seedBits bound observationBits labelBits remainingBits evaluate) (BitString.uniformList (seedLength count seedBits bound observationBits labelBits remainingBits)) = do let coins ← BitString.uniformList (count * seedBits) let lastKey ← BitString.uniformList (remainingBits * (count * seedBits)) let middleKey ← BitString.uniformList (labelBits * count) PMF.map (fun (firstKey : List Bool) => hashSamples count seedBits bound observationBits labelBits remainingBits (List.map (fun (seed : List Bool) => (evaluate seed, seed)) (BitString.listRows count seedBits coins)) firstKey middleKey lastKey) (BitString.uniformList (observationBits * (count * (2 * bound + 1))))

Uniform input bits supply independent sampler coins and matrix seeds, with no padding coins added by an execution clock.

theorem Cslib.Crypto.Pseudoentropy.ThreeSource.eval_hashSamples (count seedBits bound observationBits labelBits remainingBits : ℕ) (samples : List ((List Bool × Bool) × List Bool)) (hcount : samples.length = count) (hbound : ∀ sample ∈ samples, sample.1.1.length ≤ bound) : (do let third ← extractWordSeeds count seedBits remainingBits samples let middle ← extractWordLabels count labelBits third.1 let front ← finish bound observationBits middle pure (front ++ (third.2.1 ++ third.2.2))).eval = do let lastKey ← BitString.uniformList (remainingBits * (count * seedBits)) let middleKey ← BitString.uniformList (labelBits * count) PMF.map (fun (firstKey : List Bool) => hashSamples count seedBits bound observationBits labelBits remainingBits samples firstKey middleKey lastKey) (BitString.uniformList (observationBits * (count * (2 * bound + 1))))

Supplying independent uniform keys to the deterministic hash core realizes the three probabilistic hashing calls exactly. Only the observation padding requires a size bound.

theorem Cslib.Crypto.Pseudoentropy.ThreeSource.eval_generate (count seedBits bound observationBits labelBits remainingBits : ℕ) (evaluate : List Bool → List Bool × Bool) (hbound : ∀ (seed : List Bool), seed.length = seedBits → (evaluate seed).1.length ≤ bound) : PMF.map (generate count seedBits bound observationBits labelBits remainingBits evaluate) (BitString.uniformList (seedLength count seedBits bound observationBits labelBits remainingBits)) = (extract count seedBits bound observationBits labelBits remainingBits do let seed ← BitString.sampleList seedBits pure (evaluate seed, seed)).eval

A uniform seed of exactly seedLength bits realizes the complete sampled extractor. The only size premise is the observation bound on correctly sized sampler seeds.

theorem Cslib.Crypto.Pseudoentropy.ThreeSource.length_generate (count seedBits bound observationBits labelBits remainingBits : ℕ) (evaluate : List Bool → List Bool × Bool) (hbound : ∀ (seed : List Bool), seed.length = seedBits → (evaluate seed).1.length ≤ bound) {tape : List Bool} (htape : tape.length = seedLength count seedBits bound observationBits labelBits remainingBits) : (generate count seedBits bound observationBits labelBits remainingBits evaluate tape).length = outputLength count seedBits bound observationBits labelBits remainingBits

Every correctly sized seed produces the advertised fixed output length.

theorem Cslib.Crypto.Pseudoentropy.ThreeSource.eval_generate_of_realization {pair : SamplablePair} (saved : pair.SeedRealization) (n count bound observationBits labelBits remainingBits : ℕ) (hbound : ∀ observation ∈ (PMF.map Prod.fst (pair.joint n)).support, ((pair.encode n) observation).length ≤ bound) : PMF.map (generate count (saved.length n) bound observationBits labelBits remainingBits (saved.evaluate n)) (BitString.uniformList (seedLength count (saved.length n) bound observationBits labelBits remainingBits)) = (extract count (saved.length n) bound observationBits labelBits remainingBits (saved.sampleWithSeed n)).eval

The sampler's saved-seed evaluator implements the exact ensemble in the security theorem. The observation bound only concerns outcomes in the support of the finite pair.