From sequence distinguishers to a learned predictor

Saved coordinate predictors turn a sequence distinguishing gap into the average bias of a weighted validation trial. The explicit learner then samples descriptions, chooses an orientation, and estimates their validation rates. Its output has positive weighted correlation with high probability. All target predictions receive only the public observation.

The replay law and the masked source's extraction bound are explicit hypotheses. SequenceLearner constructs saved descriptions and obtains replay from a certified sequence test. Choosing uniform asymptotic parameters remains a separate step in the final cryptographic reduction.

Main results

• maskedSequence_validation_gap: exact transfer from a sequence gap to weighted validation bias.
• maskedSequence_learn_error_pow: sample a correlated predictor from that gap.
• extractedSequence_learn_error_pow: pay the supplied test's extraction error before learning.

References

• Thomas Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, TCC 2006, Section 5, Games 3--5 and the following prediction reduction. [Hol06]. This combines the fresh-mask adaptation with explicit sampling and empirical selection.

Adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

theorem Cslib.Crypto.Pseudoentropy.maskedSequence_validation_gap {α β : Type} [Finite α] (source : ProbComp α) (observe : α → β) (truth : α → Bool) (mask : α → ProbComp Bool) (count : ℕ) (test : List (β × Bool) → ProbComp Bool) (candidates : ProbComp (List Bool)) (predict : List Bool → β → Bool) (hrealize : ∀ value ∈ source.eval.support, ((fun (code : List Bool) => predict code (observe value)) <$> candidates).eval = (maskedSequencePredictor source observe truth mask count test (observe value)).eval) : ((OracleComp.replicate count ((fun (value : α) => (observe value, truth value)) <$> source) >>= test).eval true).toReal - ((OracleComp.replicate count (maskedSample source observe truth mask) >>= test).eval true).toReal = ↑(Probability.dyadicSize count) * (((do let code ← candidates Boosting.weightedTrial source mask fun (value : α) => pure (predict code (observe value) == truth value)).eval true).toReal - 1 / 2)

The complete sequence gap is the dyadic coordinate count times the average weighted validation bias of saved descriptions. The replay law is needed only at actual observations.

theorem Cslib.Crypto.Pseudoentropy.maskedSequence_learn_error_pow {α β : Type} [Fintype α] (source : ProbComp α) (observe : α → β) (truth : α → Bool) (mask : α → ProbComp Bool) (count : ℕ) (test : List (β × Bool) → ProbComp Bool) (candidates : ProbComp (List Bool)) (predict : List Bool → β → Bool) (hrealize : ∀ value ∈ source.eval.support, ((fun (code : List Bool) => predict code (observe value)) <$> candidates).eval = (maskedSequencePredictor source observe truth mask count test (observe value)).eval) (confidence inverseGap : ℕ) (hgap : 0 < inverseGap) (hdistinguish : ↑(Probability.dyadicSize count) / ↑inverseGap ≤ |((OracleComp.replicate count ((fun (value : α) => (observe value, truth value)) <$> source) >>= test).eval true).toReal - ((OracleComp.replicate count (maskedSample source observe truth mask) >>= test).eval true).toReal|) : ((Boosting.learn candidates (fun (code : List Bool) => Boosting.weightedTrial source mask fun (value : α) => pure (predict code (observe value) == truth value)) confidence inverseGap).eval.toOuterMeasure {code : List Bool | ¬1 / (2 * ↑inverseGap) ≤ ∑ value : α, (source.eval value).toReal * (((mask value).eval true).toReal * BitString.signedVote (Boosting.signedPredict predict code (observe value)) (truth value))}).toReal ≤ (↑((confidence + 1) * (4 * inverseGap) ^ 2) + 1) * (1 / 2) ^ confidence

A noticeable sequence gap of either sign gives an explicitly sampled predictor with positive weighted correlation. Its failure probability includes discovery and estimation.

theorem Cslib.Crypto.Pseudoentropy.extractedSequence_learn_error_pow {α β Seed Output : Type} [Fintype α] (source : ProbComp α) (observe : α → β) (truth : α → Bool) (mask : α → ProbComp Bool) (count : ℕ) (seed : ProbComp Seed) (hash : Seed → List Bool → Output) (test : List β × Seed × Output → ProbComp Bool) (ideal : PMF (List β × Seed × Output)) {ε : ℝ} (hclose : ↑(Game.advantage ((OracleComp.replicate count (maskedSample source observe truth mask) >>= extractLabels seed hash).eval.bind fun (output : List β × Seed × Output) => (test output).eval) (ideal.bind fun (output : List β × Seed × Output) => (test output).eval)) ≤ ε) (candidates : ProbComp (List Bool)) (predict : List Bool → β → Bool) (hrealize : ∀ value ∈ source.eval.support, ((fun (code : List Bool) => predict code (observe value)) <$> candidates).eval = (maskedSequencePredictor source observe truth mask count (fun (samples : List (β × Bool)) => extractLabels seed hash samples >>= test) (observe value)).eval) (confidence inverseGap : ℕ) (hgap : 0 < inverseGap) (hdistinguish : ↑(Probability.dyadicSize count) / ↑inverseGap + ε ≤ ↑(Game.advantage (do let samples ← OracleComp.replicate count ((fun (value : α) => (observe value, truth value)) <$> source) let result ← extractLabels seed hash samples test result).eval (ideal.bind fun (output : List β × Seed × Output) => (test output).eval))) : ((Boosting.learn candidates (fun (code : List Bool) => Boosting.weightedTrial source mask fun (value : α) => pure (predict code (observe value) == truth value)) confidence inverseGap).eval.toOuterMeasure {code : List Bool | ¬1 / (2 * ↑inverseGap) ≤ ∑ value : α, (source.eval value).toReal * (((mask value).eval true).toReal * BitString.signedVote (Boosting.signedPredict predict code (observe value)) (truth value))}).toReal ≤ (↑((confidence + 1) * (4 * inverseGap) ^ 2) + 1) * (1 / 2) ^ confidence

A distinguisher of extracted labels supplies a weak learner once its advantage exceeds the masked-source extraction error for that test. The statistical premise concerns the complete public observations, hash seed, and output.