Quantitative certificates for polynomial PRG stretch

Keep a seed of the original length at the front of a word. Each iteration expands that seed by one bit and retains the previously emitted suffix. Efficiency (polyTime_iterate, polyTime_stretch) only needs a bounded seed prefix; the one-bit length promise is used separately to prove output lengths.

Under the genuine one-bit length invariant ((generator s).length = s.length + 1), iterate and stretch also admit cumulative quantitative certificates (ComputableTidilyInTimeAndSpace) that stream the emitted bits in forward generation order followed by the reversed final seed (forwardIterate), charging O(n + k + ∑_{i < k} (tGen(seed_i) + n + 1)) time and O(Q + n + 1) workspace during the streaming loop, and then apply one linear-time zero-workspace reversal (Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.reverse_bits) whose composition charges the (n + k)-bit reversal buffer to restore the exact original output order.

Main definitions

• Cslib.Crypto.PRGStretch.step, Cslib.Crypto.PRGStretch.iterate, Cslib.Crypto.PRGStretch.stretch: repeatedly expand a fixed-width seed prefix and retain emitted bits.
• Cslib.Crypto.PRGStretch.seedStep, Cslib.Crypto.PRGStretch.emitBit, Cslib.Crypto.PRGStretch.seedAt, Cslib.Crypto.PRGStretch.forwardIterate: seed trajectory and forward-streamed intermediate representation before final reversal.

Main results

• Cslib.Crypto.PRGStretch.polyTime_iterate, Cslib.Crypto.PRGStretch.polyTime_stretch: captured functional iteration and stretch have uniform polynomial-time TM certificates without a length promise on the generator.
• Cslib.Crypto.PRGStretch.forwardIterate_eq: the forward representation emits each round's bit in generation order, then the reversed final seed.
• Cslib.Crypto.PRGStretch.computableTidilyInTimeAndSpace_forwardIterate, Cslib.Crypto.PRGStretch.computableTidilyInTimeAndSpace_forwardIterate_captured: streaming k expansions in forward order with cumulative time and k-independent workspace O(Q + n + 1), both clients of Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.iterate_unary_stream_sum.
• Cslib.Crypto.PRGStretch.computableTidilyInTimeAndSpace_iterate_pair, Cslib.Crypto.PRGStretch.computableTidilyInTimeAndSpace_iterate_captured, Cslib.Crypto.PRGStretch.computableTidilyInTimeAndSpace_stretch, Cslib.Crypto.PRGStretch.computableTidilyInDegree_stretch, Cslib.Crypto.PRGStretch.polyTime_stretch_of_length_eq: quantitative cumulative-time, workspace and degree certificates for iterate (unparameterized and with captured parameters) and stretch, preserving the exact reverse-generation output order and recovering ComputableTidilyInPolyTime.

References

• B. Barak, Pseudorandomness, CS 127, length extension for PRGs. We retain the final seed and reverse the order of the emitted bits.

def Cslib.Crypto.PRGStretch.step (generator : List Bool → List Bool) (n : ℕ) (word : List Bool) : List Bool

Expand the first n bits, preserving the previously emitted suffix.

def Cslib.Crypto.PRGStretch.iterate (generator : List Bool → List Bool) (n count : ℕ) (word : List Bool) : List Bool

Repeat seed expansion a specified number of times.

def Cslib.Crypto.PRGStretch.stretch (generator : List Bool → List Bool) (count : ℕ → ℕ) (seed : List Bool) : List Bool

A one-bit generator yields count n additional bits from an n-bit seed.

theorem Cslib.Crypto.PRGStretch.length_step {generator : List Bool → List Bool} (hlen : ∀ (seed : List Bool), (generator seed).length = seed.length + 1) (n : ℕ) (word : List Bool) : (step generator n word).length = word.length + 1

Each call increases the whole word's length by one, even on short intermediate words.

theorem Cslib.Crypto.PRGStretch.length_iterate {generator : List Bool → List Bool} (hlen : ∀ (seed : List Bool), (generator seed).length = seed.length + 1) (n count : ℕ) (word : List Bool) : (iterate generator n count word).length = word.length + count

The loop's length invariant.

theorem Cslib.Crypto.PRGStretch.length_iterate_of_le {generator : List Bool → List Bool} {seedBits : ℕ} (hlen : ∀ (seed : List Bool), seed.length = seedBits → (generator seed).length = seedBits + 1) (count : ℕ) (word : List Bool) (hword : seedBits ≤ word.length) : (iterate generator seedBits count word).length = word.length + count

A generator need only expand seeds at the specified length. Longer input words carry a saved suffix, and every subsequent iteration again uses a correctly sized seed prefix.

theorem Cslib.Crypto.PRGStretch.step_append (generator : List Bool → List Bool) {n : ℕ} (seed suffix : List Bool) (hlen : seed.length = n) : step generator n (seed ++ suffix) = generator seed ++ suffix

A valid seed prefix is expanded independently of the saved suffix.

theorem Cslib.Crypto.PRGStretch.polyTime_iterate {α : Type} {input : α ↪ List Bool} {generator : α → List Bool → List Bool} {seedBits count : α → ℕ} {word : α → List Bool} (hgenerator : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : α × List Bool) => generator pair.1 pair.2) (Turing.MultiTapeTM.encPair input Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hseedBits : Turing.MultiTapeTM.ComputableTidilyInPolyTime seedBits input Turing.MultiTapeTM.encUnary) (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (hword : Turing.MultiTapeTM.ComputableTidilyInPolyTime word input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => iterate (generator a) (seedBits a) (count a) (word a)) input Turing.MultiTapeTM.encBits

Iteration may capture an arbitrary encoded input. Every call reads only a bounded seed prefix, so polynomial time follows without a length promise on the generator.

theorem Cslib.Crypto.PRGStretch.polyTime_stretch {generator : List Bool → List Bool} {count : ℕ → ℕ} (hgenerator : Turing.MultiTapeTM.ComputableTidilyInPolyTime generator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (stretch generator count) Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits

Any efficiently computed iteration count gives an efficient generator.

Quantitative cumulative-time and workspace certificates

def Cslib.Crypto.PRGStretch.seedStep (generator : List Bool → List Bool) (seed : List Bool) : List Bool

The next seed produced by one expansion: all but the last bit of generator seed.

def Cslib.Crypto.PRGStretch.emitBit (generator : List Bool → List Bool) (seed : List Bool) : List Bool

The single output bit emitted by one expansion, as a 0-or-1-element list.

def Cslib.Crypto.PRGStretch.seedAt (generator : List Bool → List Bool) (seed : List Bool) (i : ℕ) : List Bool

The seed at round i of one-bit expansion starting from seed.

def Cslib.Crypto.PRGStretch.forwardIterate (generator : List Bool → List Bool) (count : ℕ) (seed : List Bool) : List Bool

Forward streaming representation of count PRG expansions from seed: emits each round's bit in forward generation order, followed by the reversed final seed (seedAt generator seed count).reverse. Reversing this word once yields iterate generator seed.length count seed.

@[simp]

theorem Cslib.Crypto.PRGStretch.seedAt_zero (generator : List Bool → List Bool) (seed : List Bool) : seedAt generator seed 0 = seed

theorem Cslib.Crypto.PRGStretch.seedAt_succ (generator : List Bool → List Bool) (seed : List Bool) (i : ℕ) : seedAt generator seed (i + 1) = seedStep generator (seedAt generator seed i)

theorem Cslib.Crypto.PRGStretch.seedStep_append_emitBit (generator : List Bool → List Bool) (seed : List Bool) (hne : generator seed ≠ []) : seedStep generator seed ++ emitBit generator seed = generator seed

A non-empty generator output splits into its next-seed prefix and its emitted bit.

theorem Cslib.Crypto.PRGStretch.length_seedStep_of_eq {generator : List Bool → List Bool} {n : ℕ} (hlen : ∀ (s : List Bool), s.length = n → (generator s).length = n + 1) {s : List Bool} (hs : s.length = n) : (seedStep generator s).length = n

Under the one-bit length promise at width n, seedStep preserves width n.

theorem Cslib.Crypto.PRGStretch.length_emitBit_of_eq {generator : List Bool → List Bool} {n : ℕ} (hlen : ∀ (s : List Bool), s.length = n → (generator s).length = n + 1) {s : List Bool} (hs : s.length = n) : (emitBit generator s).length = 1

Under the one-bit length promise at width n, emitBit has length 1.

@[simp]

theorem Cslib.Crypto.PRGStretch.reverse_emitBit (generator : List Bool → List Bool) (s : List Bool) : (emitBit generator s).reverse = emitBit generator s

emitBit has at most one element, so reversing it is the identity.

theorem Cslib.Crypto.PRGStretch.length_seedAt {generator : List Bool → List Bool} {seed : List Bool} (hlen : ∀ (s : List Bool), s.length = seed.length → (generator s).length = seed.length + 1) (i : ℕ) : (seedAt generator seed i).length = seed.length

Under the one-bit length promise at seed.length, every round seed seedAt generator seed i has length seed.length.

theorem Cslib.Crypto.PRGStretch.streamState_replicate_eq_seedAt (generator : List Bool → List Bool) (seed : List Bool) (count j : ℕ) (hj : j ≤ count) : Turing.MultiTapeTM.streamState seed (fun (p : List Bool × Bool) => seedStep generator p.1) (List.replicate count true) j = seedAt generator seed j

The streaming fold state after j ≤ count unary tokens equals seedAt generator seed j.

theorem Cslib.Crypto.PRGStretch.iterate_append_eq_seedAt_append_streamEmit_reverse {generator : List Bool → List Bool} {n : ℕ} (hlen : ∀ (s : List Bool), s.length = n → (generator s).length = n + 1) (count : ℕ) {seed : List Bool} (hseed : seed.length = n) (suffix : List Bool) : iterate generator n count (seed ++ suffix) = seedAt generator seed count ++ (Turing.MultiTapeTM.streamEmit (fun (p : List Bool × Bool) => seedStep generator p.1) (fun (p : List Bool × Bool) => emitBit generator p.1) seed (List.replicate count true)).reverse ++ suffix

Expanding seed ++ suffix for count rounds produces seedAt generator seed count, followed by the emitted bits in reverse generation order, followed by suffix.

theorem Cslib.Crypto.PRGStretch.reverse_forwardIterate_eq_iterate {generator : List Bool → List Bool} {seed : List Bool} (hlen : ∀ (s : List Bool), s.length = seed.length → (generator s).length = seed.length + 1) (count : ℕ) : (forwardIterate generator count seed).reverse = iterate generator seed.length count seed

Reversing forwardIterate generator count seed recovers the exact output of iterate generator seed.length count seed (final seed followed by emitted bits in reverse generation order).

theorem Cslib.Crypto.PRGStretch.length_forwardIterate {generator : List Bool → List Bool} {seed : List Bool} (hlen : ∀ (s : List Bool), s.length = seed.length → (generator s).length = seed.length + 1) (count : ℕ) : (forwardIterate generator count seed).length = seed.length + count

forwardIterate generator count seed has length seed.length + count.

theorem Cslib.Crypto.PRGStretch.length_seedAt_of_forall {generator : List Bool → List Bool} (hlen : ∀ (s : List Bool), (generator s).length = s.length + 1) (seed : List Bool) (i : ℕ) : (seedAt generator seed i).length = seed.length

theorem Cslib.Crypto.PRGStretch.reverse_forwardIterate_eq_iterate_of_forall {generator : List Bool → List Bool} (hlen : ∀ (s : List Bool), (generator s).length = s.length + 1) (seed : List Bool) (count : ℕ) : (forwardIterate generator count seed).reverse = iterate generator seed.length count seed

theorem Cslib.Crypto.PRGStretch.length_forwardIterate_of_forall {generator : List Bool → List Bool} (hlen : ∀ (s : List Bool), (generator s).length = s.length + 1) (seed : List Bool) (count : ℕ) : (forwardIterate generator count seed).length = seed.length + count

theorem Cslib.Crypto.PRGStretch.forwardIterate_eq (generator : List Bool → List Bool) (count : ℕ) (seed : List Bool) : forwardIterate generator count seed = (List.map (fun (i : ℕ) => emitBit generator (seedAt generator seed i)) (List.range count)).flatten ++ (seedAt generator seed count).reverse

forwardIterate emits the bits of the rounds in generation order, then the reversed final seed.

theorem Cslib.Crypto.PRGStretch.computableTidilyInTimeAndSpace_forwardIterate {generator : List Bool → List Bool} {tGen sGen : List Bool → ℕ} (hlen : ∀ (s : List Bool), (generator s).length = s.length + 1) (hgen : Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace generator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits tGen sGen) {Q : List Bool × ℕ → ℕ} (hspace : ∀ (p : List Bool × ℕ), ∀ i < p.2, sGen (seedAt generator p.1 i) ≤ Q p) : ∃ (c : ℕ), Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace (fun (p : List Bool × ℕ) => forwardIterate generator p.2 p.1) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBits (fun (p : List Bool × ℕ) => c * (p.1.length + p.2 + ∑ i ∈ Finset.range p.2, (tGen (seedAt generator p.1 i) + p.1.length + 1) + 1)) fun (p : List Bool × ℕ) => c * (Q p + p.1.length + 1)

Quantitative streaming certificate for forwardIterate. On input (seed, count) encoded with encPair encBits encUnary, forwardIterate streams count rounds directly from the unary suffix on the input tape, emitting each round's bit in generation order and finishing with the reversed final seed. Each round runs the generator twice, once for the next seed and once for the emitted bit, and both runs are charged; workspace is O(Q + seed.length + 1), independent of the round count count.

theorem Cslib.Crypto.PRGStretch.computableTidilyInTimeAndSpace_iterate_pair {generator : List Bool → List Bool} {tGen sGen : List Bool → ℕ} (hlen : ∀ (s : List Bool), (generator s).length = s.length + 1) (hgen : Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace generator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits tGen sGen) {Q : List Bool × ℕ → ℕ} (hspace : ∀ (p : List Bool × ℕ), ∀ i < p.2, sGen (seedAt generator p.1 i) ≤ Q p) : ∃ (c : ℕ), Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace (fun (p : List Bool × ℕ) => iterate generator p.1.length p.2 p.1) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBits (fun (p : List Bool × ℕ) => c * (p.1.length + p.2 + ∑ i ∈ Finset.range p.2, (tGen (seedAt generator p.1 i) + p.1.length + 1) + 1)) fun (p : List Bool × ℕ) => c * (Q p + p.1.length + p.2 + 1)

Quantitative cumulative-time and workspace certificate for PRGStretch.iterate. Composing forwardIterate with the linear-time zero-workspace reversal primitive ComputableTidilyInTimeAndSpace.reverse_bits produces the exact output of iterate generator p.1.length p.2 p.1. The time bound remains O(n + k + ∑_{i < k} (tGen(seed_i) + n + 1)), while the workspace bound O(Q + n + k + 1) explicitly includes the (n + k)-bit intermediate reversal buffer.

theorem Cslib.Crypto.PRGStretch.computableTidilyInTimeAndSpace_stretch {generator : List Bool → List Bool} {count : ℕ → ℕ} {tGen sGen : List Bool → ℕ} {tCount sCount : ℕ → ℕ} (hlen : ∀ (s : List Bool), (generator s).length = s.length + 1) (hgen : Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace generator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits tGen sGen) (hcount : Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace count Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary tCount sCount) {Q : List Bool → ℕ} (hspace : ∀ (seed : List Bool), ∀ i < count seed.length, sGen (seedAt generator seed i) ≤ Q seed) : ∃ (c : ℕ), Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace (stretch generator count) Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits (fun (seed : List Bool) => c * (tCount seed.length + seed.length + count seed.length + ∑ i ∈ Finset.range (count seed.length), (tGen (seedAt generator seed i) + seed.length + 1) + 1)) fun (seed : List Bool) => c * (sCount seed.length + Q seed + seed.length + count seed.length + 1)

Quantitative cumulative-time and workspace certificate for PRGStretch.stretch. On input seed : List Bool of length n with k = count n, stretch generator count runs in time O(tCount n + n + k + ∑_{i < k} (tGen(seed_i) + n + 1)) and workspace O(sCount n + Q seed + n + k + 1), charging count, pair assembly, every round's generator callbacks and seed copying, and the (n + k)-bit reversal buffer.

theorem Cslib.Crypto.PRGStretch.computableTidilyInDegree_stretch {generator : List Bool → List Bool} {count : ℕ → ℕ} {dGen eGen dCount eCount : ℕ} (hlen : ∀ (s : List Bool), (generator s).length = s.length + 1) (hgen : Turing.MultiTapeTM.ComputableTidilyInDegree generator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits dGen eGen) (hcount : Turing.MultiTapeTM.ComputableTidilyInDegree count Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary dCount eCount) : Turing.MultiTapeTM.ComputableTidilyInDegree (stretch generator count) Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits (max dCount (eCount + max dGen 1)) (max 1 eCount)

Degree-level quantitative certificate for PRGStretch.stretch. If generator is computable in degree (dGen, eGen) and count is computable in degree (dCount, eCount), then under the one-bit length promise (generator s).length = s.length + 1, stretch generator count is computable in time/space degree max dCount (eCount + max dGen 1) and output-size degree max 1 eCount.

theorem Cslib.Crypto.PRGStretch.polyTime_stretch_of_length_eq {generator : List Bool → List Bool} {count : ℕ → ℕ} (hlen : ∀ (s : List Bool), (generator s).length = s.length + 1) (hgenerator : Turing.MultiTapeTM.ComputableTidilyInPolyTime generator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (stretch generator count) Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits

Recover ComputableTidilyInPolyTime (stretch generator count) directly as a corollary of the quantitative streaming theorem computableTidilyInTimeAndSpace_stretch (via computableTidilyInDegree_stretch).

theorem Cslib.Crypto.PRGStretch.computableTidilyInTimeAndSpace_forwardIterate_captured {α : Type} {encParam : α ↪ List Bool} {generator : α → List Bool → List Bool} {tGen sGen : α × List Bool → ℕ} (hlen : ∀ (a : α) (s : List Bool), (generator a s).length = s.length + 1) (hgen : Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace (fun (p : α × List Bool) => generator p.1 p.2) (Turing.MultiTapeTM.encPair encParam Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits tGen sGen) {Q : (α × List Bool) × ℕ → ℕ} (hspace : ∀ (x : (α × List Bool) × ℕ), ∀ i < x.2, sGen (x.1.1, seedAt (generator x.1.1) x.1.2 i) ≤ Q x) : ∃ (c : ℕ), Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace (fun (x : (α × List Bool) × ℕ) => forwardIterate (generator x.1.1) x.2 x.1.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair encParam Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBits (fun (x : (α × List Bool) × ℕ) => c * ((encParam x.1.1).length + x.1.2.length + x.2 + ∑ i ∈ Finset.range x.2, (tGen (x.1.1, seedAt (generator x.1.1) x.1.2 i) + (encParam x.1.1).length + x.1.2.length + 1) + 1)) fun (x : (α × List Bool) × ℕ) => c * (Q x + (encParam x.1.1).length + x.1.2.length + 1)

Quantitative streaming certificate for forwardIterate with a captured parameter. On input ((a, seed), count) encoded with encPair (encPair encParam encBits) encUnary, the streaming state holds (a, seed_i) on encPair encParam encBits, so the captured parameter length (encParam a).length is charged alongside seed.length in each round's copying cost and in the workspace bound, which stays independent of count.

theorem Cslib.Crypto.PRGStretch.computableTidilyInTimeAndSpace_iterate_captured {α : Type} {encParam : α ↪ List Bool} {generator : α → List Bool → List Bool} {tGen sGen : α × List Bool → ℕ} (hlen : ∀ (a : α) (s : List Bool), (generator a s).length = s.length + 1) (hgen : Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace (fun (p : α × List Bool) => generator p.1 p.2) (Turing.MultiTapeTM.encPair encParam Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits tGen sGen) {Q : (α × List Bool) × ℕ → ℕ} (hspace : ∀ (x : (α × List Bool) × ℕ), ∀ i < x.2, sGen (x.1.1, seedAt (generator x.1.1) x.1.2 i) ≤ Q x) : ∃ (c : ℕ), Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace (fun (x : (α × List Bool) × ℕ) => iterate (generator x.1.1) x.1.2.length x.2 x.1.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair encParam Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBits (fun (x : (α × List Bool) × ℕ) => c * ((encParam x.1.1).length + x.1.2.length + x.2 + ∑ i ∈ Finset.range x.2, (tGen (x.1.1, seedAt (generator x.1.1) x.1.2 i) + (encParam x.1.1).length + x.1.2.length + 1) + 1)) fun (x : (α × List Bool) × ℕ) => c * (Q x + (encParam x.1.1).length + x.1.2.length + x.2 + 1)

Quantitative cumulative-time and workspace certificate for PRGStretch.iterate with a captured parameter. On input ((a, seed), count) encoded with encPair (encPair encParam encBits) encUnary, the streaming state holds (a, seed_i) on encPair encParam encBits, so the captured parameter length (encParam a).length is charged alongside seed.length in each round's copying cost and in the workspace bound.