Predicting a bit from a distinguishing test

The predictor supplies a trial bit to a test and returns that bit on acceptance, or its complement on rejection. Averaging over an independent fair trial turns the test's signed distinguishing gap into prediction bias. The hidden bit is not an input to the predictor.

Pr[p] is the scoped notation of Cslib.Probability for the probability, in the reals, that p returns true, so gaps and biases are signed differences.

Main definitions

• Cslib.Crypto.trialPredictor: prediction using a fixed trial bit.
• Cslib.Crypto.bitPredictor: prediction using an independent fair trial.
• Cslib.Crypto.calibratedTest: orient a test with a fresh real-or-ideal reference.

Main results

• Cslib.Crypto.trialPredictor_gap: the gap is the average of two signed prediction biases.
• Cslib.Crypto.bitPredictor_bias: a randomized trial realizes that average.
• Cslib.Crypto.calibratedTest_gap: calibration squares the distinguishing advantage.

References

• L. Trevisan, CS276 Lecture 13: Pseudorandom Generators, scribed by Siu-On Chan, the prediction reduction in Theorem 2.

Adapted from Crypto/Computational/Prediction.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the shared nonnegative game API.

def Cslib.Crypto.trialPredictor (test : Bool → ProbComp Bool) (trial : Bool) : ProbComp Bool

Predict a trial bit on acceptance and its complement on rejection.

noncomputable def Cslib.Crypto.bitPredictor (test : Bool → ProbComp Bool) : ProbComp Bool

A fresh fair trial gives one uniform predictor from a bit test.

theorem Cslib.Crypto.trialPredictor_gap (test : Bool → ProbComp Bool) (truth : Bool) : ((test truth).eval true).toReal - (((test false).eval true).toReal + ((test true).eval true).toReal) / 2 = ((((fun (guess : Bool) => guess == truth) <$> trialPredictor test false).eval true).toReal + (((fun (guess : Bool) => guess == truth) <$> trialPredictor test true).eval true).toReal - 1) / 2

The two fixed trials recover the test's signed distinguishing gap.

theorem Cslib.Crypto.probability_bitPredictor (test : Bool → ProbComp Bool) (truth : Bool) : (((fun (guess : Bool) => guess == truth) <$> bitPredictor test).eval true).toReal = ((((fun (guess : Bool) => guess == truth) <$> trialPredictor test false).eval true).toReal + (((fun (guess : Bool) => guess == truth) <$> trialPredictor test true).eval true).toReal) / 2

Randomizing the trial averages the two fixed predictors' correctness probabilities.

theorem Cslib.Crypto.bitPredictor_bias (test : Bool → ProbComp Bool) (truth : Bool) : (((fun (guess : Bool) => guess == truth) <$> bitPredictor test).eval true).toReal - 1 / 2 = ((test truth).eval true).toReal - (((test false).eval true).toReal + ((test true).eval true).toReal) / 2

The randomized predictor's bias equals the gap between the real label and a fair label.

theorem Cslib.Crypto.isPPTOn_trialPredictor {α : Type} {input : α ↪ List Bool} {test : α → Bool → ProbComp Bool} {trial : α → Bool} (htest : Probability.IsPPTOn (Turing.MultiTapeTM.encPair input Turing.MultiTapeTM.encBool) Turing.MultiTapeTM.encBool fun (pair : α × Bool) => test pair.1 pair.2) (htrial : Turing.MultiTapeTM.ComputableTidilyInPolyTime trial input Turing.MultiTapeTM.encBool) : Probability.IsPPTOn input Turing.MultiTapeTM.encBool fun (a : α) => trialPredictor (test a) (trial a)

Trial prediction charges for both the supplied bit and the complete test.

theorem Cslib.Crypto.isPPTOn_bitPredictor {α : Type} {input : α ↪ List Bool} {test : α → Bool → ProbComp Bool} (htest : Probability.IsPPTOn (Turing.MultiTapeTM.encPair input Turing.MultiTapeTM.encBool) Turing.MultiTapeTM.encBool fun (pair : α × Bool) => test pair.1 pair.2) : Probability.IsPPTOn input Turing.MultiTapeTM.encBool fun (a : α) => bitPredictor (test a)

A certified test gives a strict PPT predictor without a length-dependent choice of trial.

noncomputable def Cslib.Crypto.calibratedTest (real ideal challenge : ProbComp Bool) : ProbComp Bool

Use a fresh real-or-ideal trial to orient a challenge test without knowing its gap's sign.

theorem Cslib.Crypto.probability_calibratedTest (real ideal challenge : ProbComp Bool) : ((calibratedTest real ideal challenge).eval true).toReal = 1 / 2 + ((real.eval true).toReal - (ideal.eval true).toReal) * ((challenge.eval true).toReal - 1 / 2)

Calibration multiplies the challenge's bias by the signed gap of the reference games.

theorem Cslib.Crypto.calibratedTest_gap (real ideal : ProbComp Bool) : ((calibratedTest real ideal real).eval true).toReal - ((calibratedTest real ideal ideal).eval true).toReal = ↑(Game.advantage real.eval ideal.eval) ^ 2

The same calibration on both sides turns a possibly negative gap into its square.

theorem Cslib.Crypto.isPPTOn_calibratedTest {α : Type} {input : α ↪ List Bool} {real ideal challenge : α → ProbComp Bool} (hreal : Probability.IsPPTOn input Turing.MultiTapeTM.encBool real) (hideal : Probability.IsPPTOn input Turing.MultiTapeTM.encBool ideal) (hchallenge : Probability.IsPPTOn input Turing.MultiTapeTM.encBool challenge) : Probability.IsPPTOn input Turing.MultiTapeTM.encBool fun (a : α) => calibratedTest (real a) (ideal a) (challenge a)

Calibration is an ordinary PPT composition of its three supplied experiments.