Saving the randomness of a coordinate predictor

A predictor description stores the sampled surrounding examples, a trial bit, and the test's coins. It contains no program for generating those examples, so its size does not recursively include earlier predictors used during training. The evaluator accepts arbitrary word codes; the decoder is total even when a boosting loop truncates a description. Replay is pointwise in the supplied observation; reusing a description also reuses its coins.

The saved test input is split into two encoded fragments around the missing labeled example. This avoids requiring an efficient inverse for an arbitrary observation or parameter encoding.

Main definitions

• Description, evaluate: finite saved data and a total deterministic evaluator.
• save, splice, sample: sample the context and coins before receiving an observation.
• codeBound: bound every saved description independently of the source algorithms.

Main results

• eval_sample, exists_evaluator: exact replay from one fixed efficient evaluator.
• length_sample_le, isPPTOn_sample: all-execution size and strict PPT certificates.

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]. We save the sampled context explicitly to bound descriptions in the constructive learner.

Adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

structure Cslib.Crypto.SavedPrediction.Description : Type

Finite data needed to reuse one coordinate predictor on arbitrary observations.

• active : Bool

  Padding coordinates reject the test.

• trial : Bool

  The trial label inserted with the new observation.

• front : List Bool

  Encoded test input before the inserted example.

• back : List Bool

  Encoded test input after the inserted example.

• coins : List Bool

  The test's saved random tape.

@[instance_reducible]

instance Cslib.Crypto.SavedPrediction.instDecidableEqDescription : DecidableEq Description

def Cslib.Crypto.SavedPrediction.instDecidableEqDescription.decEq (x✝ x✝¹ : Description) : Decidable (x✝ = x✝¹)

def Cslib.Crypto.SavedPrediction.Description.encoding : Description ↪ List Bool

Encode a description using the shared pair representation.

def Cslib.Crypto.SavedPrediction.Description.decode (code : List Bool) : Description

Decode any word. Missing or malformed fields use the total pair projections.

@[simp]

theorem Cslib.Crypto.SavedPrediction.Description.decode_encoding (desc : Description) : decode (encoding desc) = desc

@[simp]

theorem Cslib.Crypto.SavedPrediction.Description.length_encoding (desc : Description) : (encoding desc).length = 2 * (desc.front.length + desc.back.length) + desc.coins.length + 8

def Cslib.Crypto.SavedPrediction.Description.input (desc : Description) (observation : List Bool) : List Bool

Insert a labeled example directly into the saved encoded input.

@[simp]

theorem Cslib.Crypto.SavedPrediction.Description.length_input (desc : Description) (observation : List Bool) : (desc.input observation).length = desc.front.length + desc.back.length + 4 * observation.length + 5

def Cslib.Crypto.SavedPrediction.evaluate (test : List Bool → List Bool → List Bool) (code observation : List Bool) : Bool

Evaluate a saved predictor with a fixed total word evaluator for the original test.

theorem Cslib.Crypto.SavedPrediction.isPolyTime_evaluate {test : List Bool → List Bool → List Bool} (htest : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : List Bool × List Bool) => test pair.1 pair.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : List Bool × List Bool) => evaluate test pair.1 pair.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

Evaluation is deterministic polynomial time on every code, including truncated codes.

def Cslib.Crypto.SavedPrediction.coinBudget (c d width : ℕ) (front back : List Bool) : ℕ

A tape long enough for every observation up to the supplied width.

noncomputable def Cslib.Crypto.SavedPrediction.save (c d width : ℕ) (trial : Bool) (front back : List Bool) : ProbComp (List Bool)

Attach one random tape to an already sampled context.

theorem Cslib.Crypto.SavedPrediction.isPPTOn_save {Param : Type} {input : Param ↪ List Bool} {front back : Param → List Bool} {width : Param → ℕ} {trial : Param → Bool} (c d : ℕ) (hfront : Turing.MultiTapeTM.ComputableTidilyInPolyTime front input Turing.MultiTapeTM.encBits) (hback : Turing.MultiTapeTM.ComputableTidilyInPolyTime back input Turing.MultiTapeTM.encBits) (hwidth : Turing.MultiTapeTM.ComputableTidilyInPolyTime width input Turing.MultiTapeTM.encUnary) (htrial : Turing.MultiTapeTM.ComputableTidilyInPolyTime trial input Turing.MultiTapeTM.encBool) : Probability.IsPPTOn input Turing.MultiTapeTM.encBits fun (a : Param) => save c d (width a) (trial a) (front a) (back a)

Drawing and saving the common tape has a strict PPT certificate.

noncomputable def Cslib.Crypto.SavedPrediction.splice {α : Type} (sample : α ↪ List Bool) (base : List Bool) (replacement original : ProbComp (α × Bool)) (before after c d width : ℕ) (trial : Bool) : ProbComp (List Bool)

Sample and save the surrounding examples before any target observation is supplied.

noncomputable def Cslib.Crypto.SavedPrediction.sample {α : Type} (encoding : α ↪ List Bool) (base : List Bool) (replacement original : ProbComp (α × Bool)) (count c d width : ℕ) : ProbComp (List Bool)

Sample a reusable predictor description, including the fair trial and rejected padding.

theorem Cslib.Crypto.SavedPrediction.eval_splice {α : Type} (encoding : α ↪ List Bool) (base : List Bool) (replacement original : ProbComp (α × Bool)) (before after c d width : ℕ) (trial : Bool) (test : List (α × Bool) → ProbComp Bool) (raw : List Bool → List Bool → List Bool) (hrealize : ∀ (values : List (α × Bool)) (budget : ℕ), c * (((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encoding Turing.MultiTapeTM.encBool))) (base, values)).length + 1) ^ d ≤ budget → (test values).eval = PMF.map (fun (coins : List Bool) => (raw coins ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encoding Turing.MultiTapeTM.encBool))) (base, values))).headD false) (BitString.uniformList budget)) (observation : α) (hwidth : (encoding observation).length ≤ width) : ((fun (code : List Bool) => evaluate raw code (encoding observation)) <$> splice encoding base replacement original before after c d width trial).eval = (trialPredictor (fun (trial : Bool) => spliceTest replacement original before after test (observation, trial)) trial).eval

Replaying a saved splice has exactly the original trial predictor's distribution. Only the target observation needs a size bound; the surrounding samples choose their own coin budget.

theorem Cslib.Crypto.SavedPrediction.eval_sample {α : Type} (encoding : α ↪ List Bool) (base : List Bool) (replacement original : ProbComp (α × Bool)) (count c d width : ℕ) (test : List (α × Bool) → ProbComp Bool) (raw : List Bool → List Bool → List Bool) (hrealize : ∀ (values : List (α × Bool)) (budget : ℕ), c * (((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encoding Turing.MultiTapeTM.encBool))) (base, values)).length + 1) ^ d ≤ budget → (test values).eval = PMF.map (fun (coins : List Bool) => (raw coins ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encoding Turing.MultiTapeTM.encBool))) (base, values))).headD false) (BitString.uniformList budget)) (observation : α) (hwidth : (encoding observation).length ≤ width) : ((fun (code : List Bool) => evaluate raw code (encoding observation)) <$> sample encoding base replacement original count c d width).eval = (bitPredictor fun (trial : Bool) => sequenceTest replacement original count test (observation, trial)).eval

Sampling all predictor randomness once preserves every bounded observation's prediction law, including rejected padding coordinates.

def Cslib.Crypto.SavedPrediction.contextBound (baseSize count width : ℕ) : ℕ

Encoded surrounding examples and the public test parameter occupy this many bits.

def Cslib.Crypto.SavedPrediction.codeBound (baseSize count c d width : ℕ) : ℕ

The complete description bound depends on sample sizes and the fixed test clock, not on the program or stored state used to generate the surrounding examples.

theorem Cslib.Crypto.SavedPrediction.isPolyTime_codeBound {Param : Type} {input : Param ↪ List Bool} {baseSize count width : Param → ℕ} (c d : ℕ) (hbase : Turing.MultiTapeTM.ComputableTidilyInPolyTime baseSize input Turing.MultiTapeTM.encUnary) (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (hwidth : Turing.MultiTapeTM.ComputableTidilyInPolyTime width input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : Param) => codeBound (baseSize a) (count a) c d (width a)) input Turing.MultiTapeTM.encUnary

The saved-description budget is polynomial time in the parameter and sample sizes. The clock coefficients belong to the fixed test, so the exponent is constant.

theorem Cslib.Crypto.SavedPrediction.length_splice_le {α : Type} (encoding : α ↪ List Bool) (base : List Bool) (replacement original : ProbComp (α × Bool)) (before after c d width : ℕ) (trial : Bool) (hreplacement : ∀ value ∈ replacement.eval.support, (encoding value.1).length ≤ width) (horiginal : ∀ value ∈ original.eval.support, (encoding value.1).length ≤ width) {code : List Bool} (hcode : code ∈ (splice encoding base replacement original before after c d width trial).eval.support) : code.length ≤ codeBound base.length (before + after) c d width

Saving a fixed coordinate has a uniform description bound on every execution.

theorem Cslib.Crypto.SavedPrediction.length_sample_le {α : Type} (encoding : α ↪ List Bool) (base : List Bool) (replacement original : ProbComp (α × Bool)) (count c d width : ℕ) (hreplacement : ∀ value ∈ replacement.eval.support, (encoding value.1).length ≤ width) (horiginal : ∀ value ∈ original.eval.support, (encoding value.1).length ≤ width) {code : List Bool} (hcode : code ∈ (sample encoding base replacement original count c d width).eval.support) : code.length ≤ codeBound base.length count c d width

Every generated description fits a bound independent of the source algorithms' internal state. Padding descriptions satisfy the same bound, including when count = 0.

theorem Cslib.Crypto.SavedPrediction.exists_evaluator {α Param : Type} {input : Param ↪ List Bool} {output : α ↪ List Bool} {test : Param → List (α × Bool) → ProbComp Bool} (htest : Probability.IsPPTOn (Turing.MultiTapeTM.encPair input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair output Turing.MultiTapeTM.encBool))) Turing.MultiTapeTM.encBool fun (pair : Param × List (α × Bool)) => test pair.1 pair.2) : ∃ (c : ℕ) (d : ℕ) (predict : List Bool → List Bool → Bool), Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : List Bool × List Bool) => predict pair.1 pair.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool ∧ ∀ (a : Param) (replacement original : ProbComp (α × Bool)) (count width : ℕ) (observation : α), (output observation).length ≤ width → ((fun (code : List Bool) => predict code (output observation)) <$> sample output (input a) replacement original count c d width).eval = (bitPredictor fun (trial : Bool) => sequenceTest replacement original count (test a) (observation, trial)).eval

A PPT test supplies one fixed efficient evaluator for all saved descriptions. No decoder for either the public parameter or observation representation is required.

theorem Cslib.Crypto.SavedPrediction.isPPTOn_splice {α Param : Type} {input : Param ↪ List Bool} {output : α ↪ List Bool} {base : Param → List Bool} {replacement original : Param → ProbComp (α × Bool)} {before after width : Param → ℕ} {trial : Param → Bool} (c d : ℕ) (hbase : Turing.MultiTapeTM.ComputableTidilyInPolyTime base input Turing.MultiTapeTM.encBits) (hreplacement : Probability.IsPPTOn input (Turing.MultiTapeTM.encPair output Turing.MultiTapeTM.encBool) replacement) (horiginal : Probability.IsPPTOn input (Turing.MultiTapeTM.encPair output Turing.MultiTapeTM.encBool) original) (hbefore : Turing.MultiTapeTM.ComputableTidilyInPolyTime before input Turing.MultiTapeTM.encUnary) (hafter : Turing.MultiTapeTM.ComputableTidilyInPolyTime after input Turing.MultiTapeTM.encUnary) (hwidth : Turing.MultiTapeTM.ComputableTidilyInPolyTime width input Turing.MultiTapeTM.encUnary) (htrial : Turing.MultiTapeTM.ComputableTidilyInPolyTime trial input Turing.MultiTapeTM.encBool) : Probability.IsPPTOn input Turing.MultiTapeTM.encBits fun (a : Param) => splice output (base a) (replacement a) (original a) (before a) (after a) c d (width a) (trial a)

Saving context and coins is strict PPT whenever the sources and numerical bounds are.

theorem Cslib.Crypto.SavedPrediction.isPPTOn_sample {α Param : Type} {input : Param ↪ List Bool} {output : α ↪ List Bool} {base : Param → List Bool} {replacement original : Param → ProbComp (α × Bool)} {count width : Param → ℕ} (c d : ℕ) (hbase : Turing.MultiTapeTM.ComputableTidilyInPolyTime base input Turing.MultiTapeTM.encBits) (hreplacement : Probability.IsPPTOn input (Turing.MultiTapeTM.encPair output Turing.MultiTapeTM.encBool) replacement) (horiginal : Probability.IsPPTOn input (Turing.MultiTapeTM.encPair output Turing.MultiTapeTM.encBool) original) (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (hwidth : Turing.MultiTapeTM.ComputableTidilyInPolyTime width input Turing.MultiTapeTM.encUnary) : Probability.IsPPTOn input Turing.MultiTapeTM.encBits fun (a : Param) => sample output (base a) (replacement a) (original a) (count a) c d (width a)

The random-coordinate description sampler is a uniform strict PPT program.