Fresh masks for a pseudoentropy pair

A mask coin chooses whether to replace a label by a fresh fair bit. Conditional on any deterministic observation, the resulting label has at least as much entropy as the average replacement probability. This remains true when the mask probability depends on the original input and label.

Every occurrence draws a fresh mask, including repeated inputs. The executable boosting weights provide such coins exactly, so their density is a lower bound on the masked label's conditional entropy. The sampler and its strict PPT certificate use the usual programming combinators.

The distinguishing-to-prediction reduction then samples a random coordinate and supplies a trial bit at that coordinate. Its weighted prediction bias is exactly the complete sequence gap divided by the dyadic coordinate range. The target observation is its only target-dependent input; labels and masks are computed only on fresh surrounding samples.

Main definitions

• Cslib.Crypto.Pseudoentropy.maskBit, .maskedSample: replace labels using fresh mask coins.
• Cslib.Crypto.Pseudoentropy.maskedSequencePredictor: prediction from a sequence distinguisher.

Main results

• Cslib.Crypto.Pseudoentropy.maskedSample_entropy_ge: mask density lower-bounds label entropy.
• Cslib.Crypto.Pseudoentropy.maskedSequence_prediction_gap: the exact weighted prediction gap.
• Cslib.Crypto.Pseudoentropy.isPPTOn_maskedSequencePredictor: the complete strict PPT reduction.

References

• Holenstein, Section 5, Games 3–5. The fresh soft-mask coin replaces the set indicator in that experiment; Holenstein, Section 2.1.1 discusses measures.

Adapted from Crypto/Computational/Pseudoentropy/Masking.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8. These are ingredients of the subsequent extraction and learning arguments, not a complete pseudorandomness theorem.

noncomputable def Cslib.Crypto.Pseudoentropy.maskBit (mask : ProbComp Bool) (truth : Bool) : ProbComp Bool

Replace a label by a fresh fair bit when the supplied mask accepts.

noncomputable def Cslib.Crypto.Pseudoentropy.maskedSample {α β : Type} (source : ProbComp α) (observe : α → β) (truth : α → Bool) (mask : α → ProbComp Bool) : ProbComp (β × Bool)

Sample an observation and a label with a fresh input-dependent randomization mask.

theorem Cslib.Crypto.Pseudoentropy.eval_maskBit (mask : ProbComp Bool) (truth : Bool) : (maskBit mask truth).eval = mask.eval.bind fun (replace : Bool) => if replace = true then Probability.PMF.uniformOfFintype Bool else PMF.pure truth

The mask's law is an ordinary mixture of a fair bit and the original label.

theorem Cslib.Crypto.Pseudoentropy.eval_maskBit_apply (mask : ProbComp Bool) (truth bit : Bool) : ((maskBit mask truth).eval bit).toReal = if bit = truth then 1 - (mask.eval true).toReal / 2 else (mask.eval true).toReal / 2

The original label remains with probability 1 - maskProbability / 2.

theorem Cslib.Crypto.Pseudoentropy.entropy_maskBit_ge (mask : ProbComp Bool) (truth : Bool) : (mask.eval true).toReal ≤ Probability.PMF.entropy (maskBit mask truth).eval

A fresh replacement contributes one bit of conditional randomness whenever the mask accepts.

theorem Cslib.Crypto.Pseudoentropy.eval_maskedSample {α β : Type} (source : ProbComp α) (observe : α → β) (truth : α → Bool) (mask : α → ProbComp Bool) : (maskedSample source observe truth mask).eval = source.eval.bind fun (x : α) => PMF.map (fun (x_1 : Bool) => (observe x, x_1)) (maskBit (mask x) (truth x)).eval

The masked pair reveals the original observation and averages the pointwise masked laws.

theorem Cslib.Crypto.Pseudoentropy.maskedSample_entropy_ge {α β : Type} [Fintype α] [Finite β] (source : ProbComp α) (observe : α → β) (truth : α → Bool) (mask : α → ProbComp Bool) : ∑ x : α, (source.eval x).toReal * ((mask x).eval true).toReal ≤ Probability.PMF.conditionalEntropy (maskedSample source observe truth mask).eval

Hiding all but a deterministic observation leaves at least the average mask probability in conditional label entropy. In particular, mask probabilities may depend on hidden labels.

theorem Cslib.Crypto.Pseudoentropy.maskedSample_weight_entropy_ge {α β : Type} [Fintype α] [Finite β] (source : ProbComp α) (observe : α → β) (truth : α → Bool) (votes : α → List Bool) (bound numerator threshold : ℕ) : (Boosting.density source.eval (↑numerator / ↑(Probability.dyadicSize bound)) fun (x : α) => BitString.listVoteMargin (votes x) (truth x) - ↑threshold) ≤ Probability.PMF.conditionalEntropy (maskedSample source observe truth fun (x : α) => Boosting.sampleWeight bound numerator threshold (votes x) (truth x)).eval

The entropy available from executable boosting masks is at least their exact soft density.

theorem Cslib.Crypto.Pseudoentropy.maskBit_prediction_gap (test : Bool → ProbComp Bool) (mask : ProbComp Bool) (truth : Bool) : ((test truth).eval true).toReal - ((maskBit mask truth >>= test).eval true).toReal = (mask.eval true).toReal * ((((fun (guess : Bool) => guess == truth) <$> bitPredictor test).eval true).toReal - 1 / 2)

Distinguishing a real label from its masked version gives prediction bias weighted by the mask probability. The predictor itself receives only the test, not the mask or hidden label.

theorem Cslib.Crypto.Pseudoentropy.maskedSample_prediction_gap {α β : Type} [Fintype α] (source : ProbComp α) (observe : α → β) (truth : α → Bool) (mask : α → ProbComp Bool) (test : β → Bool → ProbComp Bool) : ((do let x ← source test (observe x) (truth x)).eval true).toReal - ((do let pair ← maskedSample source observe truth mask test pair.1 pair.2).eval true).toReal = ∑ x : α, (source.eval x).toReal * ((mask x).eval true).toReal * ((((fun (guess : Bool) => guess == truth x) <$> bitPredictor (test (observe x))).eval true).toReal - 1 / 2)

The exact masked distinguishing gap is the source-averaged weighted prediction bias. Only the observation is passed to the predictor; the mask may depend on the entire source.

theorem Cslib.Crypto.Pseudoentropy.isPPTOn_maskBit {α : Type} {input : α ↪ List Bool} {mask : α → ProbComp Bool} {truth : α → Bool} (hmask : Probability.IsPPTOn input Turing.MultiTapeTM.encBool mask) (htruth : Turing.MultiTapeTM.ComputableTidilyInPolyTime truth input Turing.MultiTapeTM.encBool) : Probability.IsPPTOn input Turing.MultiTapeTM.encBool fun (a : α) => maskBit (mask a) (truth a)

A certified mask and an efficiently supplied label give a strict PPT randomized label.

theorem Cslib.Crypto.Pseudoentropy.isPPTOn_maskedSample {α β γ : Type} {input : α ↪ List Bool} {sample : β ↪ List Bool} {output : γ ↪ List Bool} {source : α → ProbComp β} {observe : α → β → γ} {truth : α → β → Bool} {mask : α → β → ProbComp Bool} (hsource : Probability.IsPPTOn input sample source) (hobserve : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : α × β) => observe pair.1 pair.2) (Turing.MultiTapeTM.encPair input sample) output) (htruth : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : α × β) => truth pair.1 pair.2) (Turing.MultiTapeTM.encPair input sample) Turing.MultiTapeTM.encBool) (hmask : Probability.IsPPTOn (Turing.MultiTapeTM.encPair input sample) Turing.MultiTapeTM.encBool fun (pair : α × β) => mask pair.1 pair.2) : Probability.IsPPTOn input (Turing.MultiTapeTM.encPair output Turing.MultiTapeTM.encBool) fun (a : α) => maskedSample (source a) (observe a) (truth a) (mask a)

Masked sampling composes a certified source, observation, label, and mask. All callbacks may capture the original input, and all intermediate encodings are charged.

noncomputable def Cslib.Crypto.Pseudoentropy.maskedSequencePredictor {α β : Type} (source : ProbComp α) (observe : α → β) (truth : α → Bool) (mask : α → ProbComp Bool) (count : ℕ) (test : List (β × Bool) → ProbComp Bool) (observation : β) : ProbComp Bool

Predict from one public observation by simulating a random-coordinate masked hybrid. Hidden labels and masks are computed only on independently generated surrounding samples.

theorem Cslib.Crypto.Pseudoentropy.maskedSequence_prediction_gap {α β : Type} [Fintype α] (source : ProbComp α) (observe : α → β) (truth : α → Bool) (mask : α → ProbComp Bool) (count : ℕ) (test : List (β × Bool) → ProbComp Bool) : ((OracleComp.replicate count ((fun (x : α) => (observe x, truth x)) <$> source) >>= test).eval true).toReal - ((OracleComp.replicate count (maskedSample source observe truth mask) >>= test).eval true).toReal = ↑(Probability.dyadicSize count) * ∑ x : α, (source.eval x).toReal * ((mask x).eval true).toReal * ((((fun (guess : Bool) => guess == truth x) <$> maskedSequencePredictor source observe truth mask count test (observe x)).eval true).toReal - 1 / 2)

A sequence distinguisher gives one predictor whose mask-weighted bias equals the complete distinguishing gap divided by the dyadic coordinate range. This allows arbitrary finite sources, arbitrary observations, hidden-label-dependent masks, and zero repetitions.

theorem Cslib.Crypto.Pseudoentropy.isPPTOn_maskedSequencePredictor {Param α β : Type} {input : Param ↪ List Bool} {sample : α ↪ List Bool} {output : β ↪ List Bool} {source : Param → ProbComp α} {observe : Param → α → β} {truth : Param → α → Bool} {mask : Param → α → ProbComp Bool} {count : Param → ℕ} {test : Param → List (β × Bool) → ProbComp Bool} {observation : Param → β} (hsource : Probability.IsPPTOn input sample source) (hobserve : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : Param × α) => observe pair.1 pair.2) (Turing.MultiTapeTM.encPair input sample) output) (htruth : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : Param × α) => truth pair.1 pair.2) (Turing.MultiTapeTM.encPair input sample) Turing.MultiTapeTM.encBool) (hmask : Probability.IsPPTOn (Turing.MultiTapeTM.encPair input sample) Turing.MultiTapeTM.encBool fun (pair : Param × α) => mask pair.1 pair.2) (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (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) (hobservation : Turing.MultiTapeTM.ComputableTidilyInPolyTime observation input output) : Probability.IsPPTOn input Turing.MultiTapeTM.encBool fun (a : Param) => maskedSequencePredictor (source a) (observe a) (truth a) (mask a) (count a) (test a) (observation a)

The complete masked-coordinate prediction reduction is strict PPT whenever its source, observation, labels, masks, test, and repetition count have certificates.