A sequence learner for the boosting loop

Each boosting state defines a fresh soft mask. The learner samples saved coordinate predictors using that mask, then validates them on fresh labeled examples. Stored descriptions contain the sampled data and test coins; they do not recursively contain the state that generated them. Their uniform size bound therefore justifies the loop's truncation on every execution.

The evaluator is obtained from the sequence test's strict PPT certificate. Its signed version interprets the learner's orientation bit, and is also the evaluator used by subsequent rounds.

Main definitions

• parameters: configure the loop from the density and distinguishing gap.
• candidates, learn, predict: save coordinate predictors, learn, and predict.
• failureBound: the common negligible sampling-error budget.

Main results

• isPPTOn_predict: certify the complete adaptive reduction.
• exists_evaluator: discharge the replay law from one sequence-test certificate.
• predict_extracted_error: turn a gap against every dense masked source into prediction bias.

References

• Thomas Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, TCC 2006, Section 5, Games 3--5 and the prediction reduction. [Hol06].
• Thomas Holenstein, Key Agreement from Weak Bit Agreement, STOC 2005, Section 2.2. [Hol05]. We use fresh soft masks and the clocked boosting implementation.

Adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

def Cslib.Crypto.Pseudoentropy.SequenceLearner.parameters (confidence numerator densityBound inverseGap codeBound : ℕ) : Boosting.Parameters

Configure the loop at the learner's required correlation. The density denominator and inverse distinguishing gap determine the rate; the supplied bound covers signed descriptions.

theorem Cslib.Crypto.Pseudoentropy.SequenceLearner.isPolyTime_parameters {α : Type} {input : α ↪ List Bool} {confidence numerator densityBound inverseGap codeBound : α → ℕ} (hconfidence : Turing.MultiTapeTM.ComputableTidilyInPolyTime confidence input Turing.MultiTapeTM.encUnary) (hnumerator : Turing.MultiTapeTM.ComputableTidilyInPolyTime numerator input Turing.MultiTapeTM.encUnary) (hdensity : Turing.MultiTapeTM.ComputableTidilyInPolyTime densityBound input Turing.MultiTapeTM.encUnary) (hgap : Turing.MultiTapeTM.ComputableTidilyInPolyTime inverseGap input Turing.MultiTapeTM.encUnary) (hbound : Turing.MultiTapeTM.ComputableTidilyInPolyTime codeBound input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => parameters (confidence a) (numerator a) (densityBound a) (inverseGap a) (codeBound a)) input Boosting.Parameters.encoding

Polynomial-time numerical inputs construct the complete encoded loop parameters.

theorem Cslib.Crypto.Pseudoentropy.SequenceLearner.parameters_gamma_le (confidence numerator densityBound inverseGap codeBound : ℕ) (hvalid : (parameters confidence numerator densityBound inverseGap codeBound).Valid) (hgap : 0 < inverseGap) : (parameters confidence numerator densityBound inverseGap codeBound).gamma ≤ 1 / (2 * ↑inverseGap)

A positive density numerator and the configured rate meet the learner's correlation budget.

noncomputable def Cslib.Crypto.Pseudoentropy.SequenceLearner.mask (evaluate : List Bool → List Bool → Bool) (params : Boosting.Parameters) (state : Boosting.State) (sample : List Bool × Bool) : ProbComp Bool

Sample the current soft weight on a fresh labeled observation.

noncomputable def Cslib.Crypto.Pseudoentropy.SequenceLearner.candidates (evaluate : List Bool → List Bool → Bool) (source : ProbComp (List Bool × Bool)) (base : List Bool) (count c d width : ℕ) (params : Boosting.Parameters) (state : Boosting.State) : ProbComp (List Bool)

Draw saved coordinate descriptions before receiving any challenge observation.

noncomputable def Cslib.Crypto.Pseudoentropy.SequenceLearner.learn (evaluate : List Bool → List Bool → Bool) (source : ProbComp (List Bool × Bool)) (base : List Bool) (count c d width inverseGap : ℕ) (params : Boosting.Parameters) (state : Boosting.State) : ProbComp (List Bool)

Learn a signed coordinate predictor against the state's soft mask. The evaluator supplied here interprets unsigned descriptions; the loop uses signedPredict evaluate.

noncomputable def Cslib.Crypto.Pseudoentropy.SequenceLearner.predict (evaluate : List Bool → List Bool → Bool) (source : ProbComp (List Bool × Bool)) (base : List Bool) (count c d width inverseGap : ℕ) (params : Boosting.Parameters) (observation : List Bool) : ProbComp Bool

Train with the sequence learner, then predict from the challenge's public observation.

theorem Cslib.Crypto.Pseudoentropy.SequenceLearner.isPPTOn_mask {α : Type} {input : α ↪ List Bool} {evaluate : List Bool → List Bool → Bool} {params : α → Boosting.Parameters} {state : α → Boosting.State} {sample : α → List Bool × Bool} (hevaluate : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : List Bool × List Bool) => evaluate pair.1 pair.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (hparams : Turing.MultiTapeTM.ComputableTidilyInPolyTime params input Boosting.Parameters.encoding) (hstate : Turing.MultiTapeTM.ComputableTidilyInPolyTime state input Boosting.State.encoding) (hsample : Turing.MultiTapeTM.ComputableTidilyInPolyTime sample input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool)) : Probability.IsPPTOn input Turing.MultiTapeTM.encBool fun (a : α) => mask evaluate (params a) (state a) (sample a)

Masks compose the efficient evaluator with the stored state and a labeled sample.

theorem Cslib.Crypto.Pseudoentropy.SequenceLearner.isPPTOn_candidates {α : Type} {input : α ↪ List Bool} {evaluate : List Bool → List Bool → Bool} {params : α → Boosting.Parameters} {state : α → Boosting.State} {source : α → ProbComp (List Bool × Bool)} {base : α → List Bool} {count width : α → ℕ} (c d : ℕ) (hevaluate : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : List Bool × List Bool) => evaluate pair.1 pair.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (hsource : Probability.IsPPTOn input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool) source) (hbase : Turing.MultiTapeTM.ComputableTidilyInPolyTime base input Turing.MultiTapeTM.encBits) (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (hwidth : Turing.MultiTapeTM.ComputableTidilyInPolyTime width input Turing.MultiTapeTM.encUnary) (hparams : Turing.MultiTapeTM.ComputableTidilyInPolyTime params input Boosting.Parameters.encoding) (hstate : Turing.MultiTapeTM.ComputableTidilyInPolyTime state input Boosting.State.encoding) : Probability.IsPPTOn input Turing.MultiTapeTM.encBits fun (a : α) => candidates evaluate (source a) (base a) (count a) c d (width a) (params a) (state a)

Drawing descriptions is strict PPT even on executions with inaccurate guards or learners.

theorem Cslib.Crypto.Pseudoentropy.SequenceLearner.isPPTOn_learn {α : Type} {input : α ↪ List Bool} {evaluate : List Bool → List Bool → Bool} {params : α → Boosting.Parameters} {state : α → Boosting.State} {source : α → ProbComp (List Bool × Bool)} {base : α → List Bool} {count width inverseGap : α → ℕ} (c d : ℕ) (hevaluate : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : List Bool × List Bool) => evaluate pair.1 pair.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (hsource : Probability.IsPPTOn input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool) source) (hbase : Turing.MultiTapeTM.ComputableTidilyInPolyTime base input Turing.MultiTapeTM.encBits) (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (hwidth : Turing.MultiTapeTM.ComputableTidilyInPolyTime width input Turing.MultiTapeTM.encUnary) (hgap : Turing.MultiTapeTM.ComputableTidilyInPolyTime inverseGap input Turing.MultiTapeTM.encUnary) (hparams : Turing.MultiTapeTM.ComputableTidilyInPolyTime params input Boosting.Parameters.encoding) (hstate : Turing.MultiTapeTM.ComputableTidilyInPolyTime state input Boosting.State.encoding) : Probability.IsPPTOn input Turing.MultiTapeTM.encBits fun (a : α) => learn evaluate (source a) (base a) (count a) c d (width a) (inverseGap a) (params a) (state a)

The adaptive sequence learner is strict PPT in the complete stored state and source input.

theorem Cslib.Crypto.Pseudoentropy.SequenceLearner.isPPTOn_predict {α : Type} {input : α ↪ List Bool} {evaluate : List Bool → List Bool → Bool} {params : α → Boosting.Parameters} {source : α → ProbComp (List Bool × Bool)} {base observation : α → List Bool} {count width inverseGap : α → ℕ} (c d : ℕ) (hevaluate : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : List Bool × List Bool) => evaluate pair.1 pair.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (hsource : Probability.IsPPTOn input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool) source) (hbase : Turing.MultiTapeTM.ComputableTidilyInPolyTime base input Turing.MultiTapeTM.encBits) (hobservation : Turing.MultiTapeTM.ComputableTidilyInPolyTime observation input Turing.MultiTapeTM.encBits) (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (hwidth : Turing.MultiTapeTM.ComputableTidilyInPolyTime width input Turing.MultiTapeTM.encUnary) (hgap : Turing.MultiTapeTM.ComputableTidilyInPolyTime inverseGap input Turing.MultiTapeTM.encUnary) (hparams : Turing.MultiTapeTM.ComputableTidilyInPolyTime params input Boosting.Parameters.encoding) : Probability.IsPPTOn input Turing.MultiTapeTM.encBool fun (a : α) => predict evaluate (source a) (base a) (count a) c d (width a) (inverseGap a) (params a) (observation a)

The complete reduction has one uniform strict PPT implementation. The client supplies source and evaluator certificates and polynomial-time numerical parameters, not machine data.

theorem Cslib.Crypto.Pseudoentropy.SequenceLearner.mask_probability (evaluate : List Bool → List Bool → Bool) (params : Boosting.Parameters) (state : Boosting.State) (sample : List Bool × Bool) : ((mask evaluate params state sample).eval true).toReal = Boosting.weight params.rate (BitString.listVoteMargin (Boosting.State.votes evaluate state sample.1) sample.2 - ↑state.threshold)

The mask used by the executable learner is exactly the analytic soft weight.

theorem Cslib.Crypto.Pseudoentropy.SequenceLearner.candidates_length_le (evaluate : List Bool → List Bool → Bool) (source : ProbComp (List Bool × Bool)) (base : List Bool) (count c d width : ℕ) (params : Boosting.Parameters) (state : Boosting.State) (hwidth : ∀ sample ∈ source.eval.support, sample.1.length ≤ width) {code : List Bool} (hcode : code ∈ (candidates evaluate source base count c d width params state).eval.support) : code.length ≤ SavedPrediction.codeBound base.length count c d width

The code bound depends on the source's output width, not the current state's size.

theorem Cslib.Crypto.Pseudoentropy.SequenceLearner.learn_length_le (evaluate : List Bool → List Bool → Bool) (source : ProbComp (List Bool × Bool)) (base : List Bool) (count c d width inverseGap : ℕ) (params : Boosting.Parameters) (state : Boosting.State) (hwidth : ∀ sample ∈ source.eval.support, sample.1.length ≤ width) {code : List Bool} (hcode : code ∈ (learn evaluate source base count c d width inverseGap params state).eval.support) : code.length ≤ SavedPrediction.codeBound base.length count c d width + 1

Orientation and empirical selection add at most one bit to a sampled description.

theorem Cslib.Crypto.Pseudoentropy.SequenceLearner.exists_evaluator {Param : Type} {input : Param ↪ List Bool} {test : Param → List (List Bool × Bool) → ProbComp Bool} (htest : Probability.IsPPTOn (Turing.MultiTapeTM.encPair input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool))) Turing.MultiTapeTM.encBool fun (pair : Param × List (List Bool × Bool)) => test pair.1 pair.2) : ∃ (c : ℕ) (d : ℕ) (evaluate : List Bool → List Bool → Bool), Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : List Bool × List Bool) => evaluate pair.1 pair.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool ∧ ∀ (a : Param) {α : Type} (source : ProbComp α) (observe : α → List Bool) (truth : α → Bool) (count width : ℕ) (params : Boosting.Parameters) (state : Boosting.State) (observation : List Bool), observation.length ≤ width → ((fun (code : List Bool) => evaluate code observation) <$> candidates (Boosting.signedPredict evaluate) ((fun (x : α) => (observe x, truth x)) <$> source) (input a) count c d width params state).eval = (maskedSequencePredictor source observe truth (fun (x : α) => mask (Boosting.signedPredict evaluate) params state (observe x, truth x)) count (test a) observation).eval

One certified sequence test gives a fixed evaluator for every parameter, source, and boosting state. The challenge observation is supplied only after the description is sampled.

noncomputable def Cslib.Crypto.Pseudoentropy.SequenceLearner.failureBound (params : Boosting.Parameters) (inverseGap : ℕ) : NNReal

A common bound for all sampled guards, candidate discovery, validation, and slope selection.

theorem Cslib.Crypto.Pseudoentropy.SequenceLearner.failureBound_negligible {params : ℕ → Boosting.Parameters} {inverseGap : ℕ → ℕ} (hconfidence : PolynomiallyBounded fun (n : ℕ) => (params n).confidence) (hdensity : PolynomiallyBounded fun (n : ℕ) => (params n).densityBound) (hrate : PolynomiallyBounded fun (n : ℕ) => (params n).rateBound) (hgap : PolynomiallyBounded inverseGap) (hbudget : ∀ (n : ℕ), n ≤ (params n).confidence) : Negligible fun (n : ℕ) => failureBound (params n) (inverseGap n)

Polynomial parameters and at least n confidence bits make the complete failure bound negligible. The polynomial degree may depend on the fixed sequence distinguisher.

theorem Cslib.Crypto.Pseudoentropy.SequenceLearner.failureBound_eventually_le {params : ℕ → Boosting.Parameters} {inverseGap : ℕ → ℕ} (hconfidence : PolynomiallyBounded fun (n : ℕ) => (params n).confidence) (hdensity : PolynomiallyBounded fun (n : ℕ) => (params n).densityBound) (hrate : PolynomiallyBounded fun (n : ℕ) => (params n).rateBound) (hgap : PolynomiallyBounded inverseGap) (hbudget : ∀ (n : ℕ), n ≤ (params n).confidence) : ∀ᶠ (n : ℕ) in Filter.atTop, ↑(failureBound (params n) (inverseGap n)) ≤ 1 / (2 * ↑(params n).predictionInverseTolerance)

Eventually all sampling failures consume at most half the inverse-polynomial prediction advantage. The threshold may depend on the fixed distinguisher and its polynomial parameters.

theorem Cslib.Crypto.Pseudoentropy.SequenceLearner.learn_goodPredictor_error {α : Type} [Fintype α] (source : ProbComp α) (observe : α → List Bool) (truth : α → Bool) (evaluate : List Bool → List Bool → Bool) (base : List Bool) (count c d width inverseGap : ℕ) (params : Boosting.Parameters) (state : Boosting.State) (test : List (List Bool × Bool) → ProbComp Bool) (hparams : params.Valid) (hgap : 0 < inverseGap) (hgamma : params.gamma ≤ 1 / (2 * ↑inverseGap)) (hwidth : ∀ value ∈ source.eval.support, (observe value).length ≤ width) (hbound : SavedPrediction.codeBound base.length count c d width + 1 ≤ params.codeBound) (hrealize : ∀ value ∈ source.eval.support, ((fun (code : List Bool) => evaluate code (observe value)) <$> candidates (Boosting.signedPredict evaluate) ((fun (x : α) => (observe x, truth x)) <$> source) base count c d width params state).eval = (maskedSequencePredictor source observe truth (fun (x : α) => mask (Boosting.signedPredict evaluate) params state (observe x, truth x)) count test (observe value)).eval) (hdistinguish : ↑(Probability.dyadicSize count) / ↑inverseGap ≤ |((OracleComp.replicate count ((fun (x : α) => (observe x, truth x)) <$> source) >>= test).eval true).toReal - ((OracleComp.replicate count (maskedSample source observe truth fun (x : α) => mask (Boosting.signedPredict evaluate) params state (observe x, truth x)) >>= test).eval true).toReal|) : ((learn evaluate ((fun (x : α) => (observe x, truth x)) <$> source) base count c d width inverseGap params state).eval.toOuterMeasure {code : List Bool | ¬Boosting.State.GoodPredictor source.eval (fun (code : List Bool) (x : α) => Boosting.signedPredict evaluate code (observe x)) truth params state code}).toReal ≤ (↑((params.confidence + 1) * (4 * inverseGap) ^ 2) + 1) * (1 / 2) ^ params.confidence

A noticeable sequence gap supplies the actual loop contract. Both the sampled descriptions and their orientations fit the declared code bound, so truncation preserves their predictions.

theorem Cslib.Crypto.Pseudoentropy.SequenceLearner.predict_error {α : Type} [Fintype α] (source : ProbComp α) (observe : α → List Bool) (truth : α → Bool) (evaluate : List Bool → List Bool → Bool) (base : List Bool) (count c d width inverseGap : ℕ) (params : Boosting.Parameters) (test : List (List Bool × Bool) → ProbComp Bool) (hparams : params.Valid) (hgap : 0 < inverseGap) (hgamma : params.gamma ≤ 1 / (2 * ↑inverseGap)) (hwidth : ∀ value ∈ source.eval.support, (observe value).length ≤ width) (hbound : SavedPrediction.codeBound base.length count c d width + 1 ≤ params.codeBound) (hrealize : ∀ (state : Boosting.State), ∀ value ∈ source.eval.support, ((fun (code : List Bool) => evaluate code (observe value)) <$> candidates (Boosting.signedPredict evaluate) ((fun (x : α) => (observe x, truth x)) <$> source) base count c d width params state).eval = (maskedSequencePredictor source observe truth (fun (x : α) => mask (Boosting.signedPredict evaluate) params state (observe x, truth x)) count test (observe value)).eval) (hdistinguish : ∀ (state : Boosting.State), (params.delta ≤ Boosting.density source.eval params.rate fun (x : α) => state.margin (fun (code : List Bool) (x : α) => Boosting.signedPredict evaluate code (observe x)) truth x - ↑state.threshold) → ↑(Probability.dyadicSize count) / ↑inverseGap ≤ |((OracleComp.replicate count ((fun (x : α) => (observe x, truth x)) <$> source) >>= test).eval true).toReal - ((OracleComp.replicate count (maskedSample source observe truth fun (x : α) => mask (Boosting.signedPredict evaluate) params state (observe x, truth x)) >>= test).eval true).toReal|) : ((do let x ← source (fun (answer : Bool) => answer == truth x) <$> predict evaluate ((fun (x : α) => (observe x, truth x)) <$> source) base count c d width inverseGap params (observe x)).eval false).toReal ≤ params.delta / 2 - 1 / ↑params.predictionInverseTolerance + ↑(failureBound params inverseGap)

Distinguishing every dense masked sequence yields a predictor beating delta / 2, up to the single explicit failure bound. The learner here is the executable saved-description program.

theorem Cslib.Crypto.Pseudoentropy.SequenceLearner.predict_extracted_error {α : Type} [Fintype α] {Seed Output : Type} (source : ProbComp α) (observe : α → List Bool) (truth : α → Bool) (evaluate : List Bool → List Bool → Bool) (base : List Bool) (count c d width inverseGap : ℕ) (params : Boosting.Parameters) (seed : ProbComp Seed) (hash : Seed → List Bool → Output) (test : List (List Bool) × Seed × Output → ProbComp Bool) (ideal : PMF (List (List Bool) × Seed × Output)) {ε : ℝ} (hparams : params.Valid) (hgap : 0 < inverseGap) (hgamma : params.gamma ≤ 1 / (2 * ↑inverseGap)) (hwidth : ∀ value ∈ source.eval.support, (observe value).length ≤ width) (hbound : SavedPrediction.codeBound base.length count c d width + 1 ≤ params.codeBound) (hrealize : ∀ (state : Boosting.State), ∀ value ∈ source.eval.support, ((fun (code : List Bool) => evaluate code (observe value)) <$> candidates (Boosting.signedPredict evaluate) ((fun (x : α) => (observe x, truth x)) <$> source) base count c d width params state).eval = (maskedSequencePredictor source observe truth (fun (x : α) => mask (Boosting.signedPredict evaluate) params state (observe x, truth x)) count (fun (samples : List (List Bool × Bool)) => extractLabels seed hash samples >>= test) (observe value)).eval) (hclose : ∀ (state : Boosting.State), (params.delta ≤ Boosting.density source.eval params.rate fun (x : α) => state.margin (fun (code : List Bool) (x : α) => Boosting.signedPredict evaluate code (observe x)) truth x - ↑state.threshold) → ↑(Game.advantage ((OracleComp.replicate count (maskedSample source observe truth fun (x : α) => mask (Boosting.signedPredict evaluate) params state (observe x, truth x)) >>= extractLabels seed hash).eval.bind fun (output : List (List Bool) × Seed × Output) => (test output).eval) (ideal.bind fun (output : List (List Bool) × Seed × Output) => (test output).eval)) ≤ ε) (hdistinguish : ↑(Probability.dyadicSize count) / ↑inverseGap + ε ≤ ↑(Game.advantage (do let samples ← OracleComp.replicate count ((fun (x : α) => (observe x, truth x)) <$> source) let result ← extractLabels seed hash samples test result).eval (ideal.bind fun (output : List (List Bool) × Seed × Output) => (test output).eval))) : ((do let x ← source (fun (answer : Bool) => answer == truth x) <$> predict evaluate ((fun (x : α) => (observe x, truth x)) <$> source) base count c d width inverseGap params (observe x)).eval false).toReal ≤ params.delta / 2 - 1 / ↑params.predictionInverseTolerance + ↑(failureBound params inverseGap)

Extraction error is the only additional loss when the complete reduction starts from a test of hashed labels. The statistical premise is needed only at dense boosting states.