An expanding grid of entropy guesses

A dyadic grid guesses the observation entropy and the conditional label entropy. Every guess assigns enough total digest bits to expand, including incorrect guesses. Rounding the true entropies down gives a candidate satisfying all three extraction budgets whenever the prediction gap covers four grid steps. The entropy-dependent choice appears only in the existence proof.

The grid and its output lengths use ordinary unary arithmetic. Their polynomial-time certificates apply to arbitrary captured inputs, so later reductions can enumerate the family.

Main definitions

• size, observationBits, labelBits, remainingBits: the executable grid and digest lengths.
• Valid: the entropy budgets required of a successful candidate.

Main results

• expands: every candidate expands, including inaccurate guesses.
• exists_valid: a sufficiently large prediction gap guarantees a valid grid entry.

References

• Thomas Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, TCC 2006, Section 5, final proof of Theorem 1. [Hol06]. The constants below accommodate our repetition schedule and binary-matrix extractors.

Adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using typed polynomial-time certificates.

def Cslib.Crypto.Pseudoentropy.EntropyGrid.size (sourceBits bound : ℕ) : ℕ

Enumerate an observation guess up to the seed entropy and a label guess below one.

@[simp]

theorem Cslib.Crypto.Pseudoentropy.EntropyGrid.size_pos (sourceBits bound : ℕ) : 0 < size sourceBits bound

The grid is nonempty, including when the source has no seed bits.

def Cslib.Crypto.Pseudoentropy.EntropyGrid.scale (n sourceBits bound : ℕ) : ℕ

One unit is the two-slack reserve in the extraction schedule.

def Cslib.Crypto.Pseudoentropy.EntropyGrid.observationBits (n sourceBits bound index : ℕ) : ℕ

Digest length for the observation source, with a zero floor.

def Cslib.Crypto.Pseudoentropy.EntropyGrid.labelBits (n sourceBits bound index : ℕ) : ℕ

Digest length for the hidden labels, using part of the pseudoentropy surplus.

def Cslib.Crypto.Pseudoentropy.EntropyGrid.remainingBits (n sourceBits bound index : ℕ) : ℕ

Digest length for the saved seed after revealing both components.

def Cslib.Crypto.Pseudoentropy.EntropyGrid.numerator (bound index : ℕ) : ℕ

The soft-mask density numerator, four grid steps above the label guess.

theorem Cslib.Crypto.Pseudoentropy.EntropyGrid.isPolyTime_size {α : Type} {input : α ↪ List Bool} {sourceBits bound : α → ℕ} (hsource : Turing.MultiTapeTM.ComputableTidilyInPolyTime sourceBits input Turing.MultiTapeTM.encUnary) (hbound : Turing.MultiTapeTM.ComputableTidilyInPolyTime bound input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => size (sourceBits a) (bound a)) input Turing.MultiTapeTM.encUnary

The grid has polynomially many entries.

theorem Cslib.Crypto.Pseudoentropy.EntropyGrid.isPolyTime_scale {α : Type} {input : α ↪ List Bool} {n sourceBits bound : α → ℕ} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hsource : Turing.MultiTapeTM.ComputableTidilyInPolyTime sourceBits input Turing.MultiTapeTM.encUnary) (hbound : Turing.MultiTapeTM.ComputableTidilyInPolyTime bound input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => scale (n a) (sourceBits a) (bound a)) input Turing.MultiTapeTM.encUnary

The common slack unit is uniformly efficient.

theorem Cslib.Crypto.Pseudoentropy.EntropyGrid.isPolyTime_observationBits {α : Type} {input : α ↪ List Bool} {n sourceBits bound index : α → ℕ} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hsource : Turing.MultiTapeTM.ComputableTidilyInPolyTime sourceBits input Turing.MultiTapeTM.encUnary) (hbound : Turing.MultiTapeTM.ComputableTidilyInPolyTime bound input Turing.MultiTapeTM.encUnary) (hindex : Turing.MultiTapeTM.ComputableTidilyInPolyTime index input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => observationBits (n a) (sourceBits a) (bound a) (index a)) input Turing.MultiTapeTM.encUnary

The observation digest length is uniformly efficient in the candidate index.

theorem Cslib.Crypto.Pseudoentropy.EntropyGrid.isPolyTime_labelBits {α : Type} {input : α ↪ List Bool} {n sourceBits bound index : α → ℕ} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hsource : Turing.MultiTapeTM.ComputableTidilyInPolyTime sourceBits input Turing.MultiTapeTM.encUnary) (hbound : Turing.MultiTapeTM.ComputableTidilyInPolyTime bound input Turing.MultiTapeTM.encUnary) (hindex : Turing.MultiTapeTM.ComputableTidilyInPolyTime index input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => labelBits (n a) (sourceBits a) (bound a) (index a)) input Turing.MultiTapeTM.encUnary

The label digest length is uniformly efficient in the candidate index.

theorem Cslib.Crypto.Pseudoentropy.EntropyGrid.isPolyTime_remainingBits {α : Type} {input : α ↪ List Bool} {n sourceBits bound index : α → ℕ} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hsource : Turing.MultiTapeTM.ComputableTidilyInPolyTime sourceBits input Turing.MultiTapeTM.encUnary) (hbound : Turing.MultiTapeTM.ComputableTidilyInPolyTime bound input Turing.MultiTapeTM.encUnary) (hindex : Turing.MultiTapeTM.ComputableTidilyInPolyTime index input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => remainingBits (n a) (sourceBits a) (bound a) (index a)) input Turing.MultiTapeTM.encUnary

The retained-seed digest length is uniformly efficient in the candidate index.

theorem Cslib.Crypto.Pseudoentropy.EntropyGrid.isPolyTime_numerator {α : Type} {input : α ↪ List Bool} {bound index : α → ℕ} (hbound : Turing.MultiTapeTM.ComputableTidilyInPolyTime bound input Turing.MultiTapeTM.encUnary) (hindex : Turing.MultiTapeTM.ComputableTidilyInPolyTime index input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => numerator (bound a) (index a)) input Turing.MultiTapeTM.encUnary

The requested density is uniformly efficient in the candidate index.

theorem Cslib.Crypto.Pseudoentropy.EntropyGrid.numerator_pos (bound index : ℕ) : 0 < numerator bound index

No candidate asks for zero soft-mask mass.

theorem Cslib.Crypto.Pseudoentropy.EntropyGrid.scale_pos (n sourceBits bound : ℕ) : 0 < scale n sourceBits bound

The integer unit is positive even at security parameter zero.

theorem Cslib.Crypto.Pseudoentropy.EntropyGrid.count_eq (n sourceBits bound : ℕ) : ExtractionSchedule.count n sourceBits (Probability.dyadicSize bound - 1) = 2 * scale n sourceBits bound * Probability.dyadicSize bound

The repetition count is exactly two units per grid step.

theorem Cslib.Crypto.Pseudoentropy.EntropyGrid.expands (n sourceBits bound index : ℕ) : ExtractionSchedule.count n sourceBits (Probability.dyadicSize bound - 1) * sourceBits < observationBits n sourceBits bound index + labelBits n sourceBits bound index + remainingBits n sourceBits bound index

All candidates expand, whether or not their entropy guesses are accurate.

theorem Cslib.Crypto.Pseudoentropy.EntropyGrid.label_budget (n sourceBits bound index : ℕ) : ↑(labelBits n sourceBits bound index) + ↑(scale n sourceBits bound) = ↑(ExtractionSchedule.count n sourceBits (Probability.dyadicSize bound - 1)) * (↑(numerator bound index) / ↑(Probability.dyadicSize bound))

The label budget holds exactly for every candidate, independent of entropy assumptions.

structure Cslib.Crypto.Pseudoentropy.EntropyGrid.Valid (n sourceBits bound index : ℕ) (observationEntropy labelEntropy gap : ℝ) : Prop

The entropy assumptions required of a useful entry. Indexing and expansion are separate from security: inaccurate entries are still total expanding programs.

• index_lt : index < size sourceBits bound

  The entry lies in the enumerated grid.

• numerator_le : numerator bound index ≤ Probability.dyadicSize bound

  The requested mask density is at most one.

• density_le : ↑(numerator bound index) / ↑(Probability.dyadicSize bound) ≤ labelEntropy + gap

  The prediction gap pays for the increased label density.

• observation_budget : observationBits n sourceBits bound index = 0 ∨ ↑(observationBits n sourceBits bound index) + ↑(scale n sourceBits bound) ≤ ↑(ExtractionSchedule.count n sourceBits (Probability.dyadicSize bound - 1)) * observationEntropy

  The first extractor respects the observation entropy.

• remaining_budget : remainingBits n sourceBits bound index = 0 ∨ ↑(remainingBits n sourceBits bound index) + ↑(scale n sourceBits bound) ≤ ↑(ExtractionSchedule.count n sourceBits (Probability.dyadicSize bound - 1)) * (↑sourceBits - observationEntropy - labelEntropy)

  The last extractor respects the entropy left in the saved sampler seed.

theorem Cslib.Crypto.Pseudoentropy.EntropyGrid.exists_valid (n sourceBits bound : ℕ) {observationEntropy labelEntropy gap : ℝ} (hobservation : 0 ≤ observationEntropy) (hlabel : 0 ≤ labelEntropy) (htotal : observationEntropy + labelEntropy ≤ ↑sourceBits) (hgap : 4 / ↑(Probability.dyadicSize bound) ≤ gap) (hone : labelEntropy + gap ≤ 1) : ∃ (index : ℕ), Valid n sourceBits bound index observationEntropy labelEntropy gap

Rounding both true entropies down supplies a valid candidate. Four grid steps of pseudoentropy suffice; no algorithm for computing either entropy is assumed.