Extracting fresh masked labels

A dyadic mask gives a lower bound on every nonzero masked sample probability. The bound depends on the source and mask precision, independently of the cost of computing the mask's votes. Independent masked labels can therefore be extracted at almost their total soft density, while revealing every observation and the complete hash seed.

Main results

• maskedSample_map_fst: preserve the full public marginal.
• maskedSample_weight_mass_ge: bound positive masses independently of stored votes.
• maskedSample_weight_mass_ge_eventually: one eventual bound for every vote mask.
• maskedSample_extract_dist_bind_le: extraction against every finite-output test of the observations, seed, and output, including infinite observation types.

References

• Thomas Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, TCC 2006, Section 3.3, Lemma 2, and Section 5, Game 3. [Hol06]. These bounds support our fresh soft-mask adaptation of the set-masking experiment. We retain the explicit concentration loss from the source mass and dyadic mask precision.

Adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

theorem Cslib.Crypto.Pseudoentropy.maskedSample_map_fst {α β : Type} (source : ProbComp α) (observe : α → β) (truth : α → Bool) (mask : α → ProbComp Bool) : PMF.map Prod.fst (maskedSample source observe truth mask).eval = PMF.map observe source.eval

Fresh masking preserves the complete public marginal.

theorem Cslib.Crypto.Pseudoentropy.maskBit_mass_ge (mask : ProbComp Bool) (truth bit : Bool) {mass : ℝ} (hmass : mass ≤ 1) (hmask : 0 < (mask.eval true).toReal → mass ≤ (mask.eval true).toReal) (hbit : bit ∈ (maskBit mask truth).eval.support) : mass / 2 ≤ ((maskBit mask truth).eval bit).toReal

A mask with positive acceptance probability at least mass assigns each possible label probability at least mass / 2. Keeping the original label always has probability at least half.

theorem Cslib.Crypto.Pseudoentropy.maskedSample_mass_ge {α β : Type} (source : ProbComp α) (observe : α → β) (truth : α → Bool) (mask : α → ProbComp Bool) {sourceMass maskMass : ℝ} (hmaskMass : maskMass ∈ Set.Icc 0 1) (hsource : ∀ value ∈ source.eval.support, sourceMass ≤ (source.eval value).toReal) (hmask : ∀ value ∈ source.eval.support, 0 < ((mask value).eval true).toReal → maskMass ≤ ((mask value).eval true).toReal) (pair : β × Bool) (hpair : pair ∈ (maskedSample source observe truth mask).eval.support) : sourceMass * (maskMass / 2) ≤ ((maskedSample source observe truth mask).eval pair).toReal

Revealing only an observation cannot decrease the contribution of any one source outcome. The mask need not be determined by the observation or be independent of the true label.

theorem Cslib.Crypto.Pseudoentropy.maskedSample_dyadic_mass_ge {α β : Type} (source : ProbComp α) (observe : α → β) (truth : α → Bool) (mask : α → ProbComp Bool) (sourceBits bound : ℕ) (hsource : ∀ value ∈ source.eval.support, 2 ^ (-↑sourceBits) ≤ (source.eval value).toReal) (hmask : ∀ value ∈ source.eval.support, 0 < ((mask value).eval true).toReal → 1 / ↑(Probability.dyadicSize bound) ≤ ((mask value).eval true).toReal) (pair : β × Bool) (hpair : pair ∈ (maskedSample source observe truth mask).eval.support) : 2 ^ (-↑(sourceBits + Nat.log 2 bound + 2)) ≤ ((maskedSample source observe truth mask).eval pair).toReal

A dyadic lower bound on positive mask probabilities bounds the extra information carried by a masked label, independently of how the mask was obtained.

theorem Cslib.Crypto.Pseudoentropy.maskedSample_weight_mass_ge {α β : Type} (source : ProbComp α) (observe : α → β) (truth : α → Bool) (votes : α → List Bool) (sourceBits bound numerator threshold : ℕ) (hsource : ∀ value ∈ source.eval.support, 2 ^ (-↑sourceBits) ≤ (source.eval value).toReal) (pair : β × Bool) (hpair : pair ∈ (maskedSample source observe truth fun (value : α) => Boosting.sampleWeight bound numerator threshold (votes value) (truth value)).eval.support) : 2 ^ (-↑(sourceBits + Nat.log 2 bound + 2)) ≤ ((maskedSample source observe truth fun (value : α) => Boosting.sampleWeight bound numerator threshold (votes value) (truth value)).eval pair).toReal

A source with sourceBits bits of pointwise information gains at most log₂ bound + 2 bits from its dyadic mask and fresh label coin. The votes and threshold do not enter this bound.

theorem Cslib.Crypto.Pseudoentropy.maskedSample_dyadic_mass_ge_eventually {α β : ℕ → Type} (source : (n : ℕ) → ProbComp (α n)) (observe : (n : ℕ) → α n → β n) (truth : (n : ℕ) → α n → Bool) (sourceBits bound : ℕ → ℕ) (hbound : PolynomiallyBounded bound) (hsource : ∀ (n : ℕ), ∀ value ∈ (source n).eval.support, 2 ^ (-↑(sourceBits n)) ≤ ((source n).eval value).toReal) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (mask : α n → ProbComp Bool), (∀ value ∈ (source n).eval.support, 0 < ((mask value).eval true).toReal → 1 / ↑(Probability.dyadicSize (bound n)) ≤ ((mask value).eval true).toReal) → ∀ pair ∈ (maskedSample (source n) (observe n) (truth n) mask).eval.support, 2 ^ (-↑(sourceBits n + n + 2)) ≤ ((maskedSample (source n) (observe n) (truth n) mask).eval pair).toReal

For every polynomial mask precision, eventually the extra information is at most n + 2 bits, simultaneously for every mask with the given pointwise bound. Only the starting index depends on the polynomial's degree, so the extraction schedule can be fixed in advance.

theorem Cslib.Crypto.Pseudoentropy.maskedSample_weight_mass_ge_eventually {α β : ℕ → Type} (source : (n : ℕ) → ProbComp (α n)) (observe : (n : ℕ) → α n → β n) (truth : (n : ℕ) → α n → Bool) (sourceBits bound : ℕ → ℕ) (hbound : PolynomiallyBounded bound) (hsource : ∀ (n : ℕ), ∀ value ∈ (source n).eval.support, 2 ^ (-↑(sourceBits n)) ≤ ((source n).eval value).toReal) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (votes : α n → List Bool) (numerator threshold : ℕ), ∀ pair ∈ (maskedSample (source n) (observe n) (truth n) fun (value : α n) => Boosting.sampleWeight (bound n) numerator threshold (votes value) (truth n value)).eval.support, 2 ^ (-↑(sourceBits n + n + 2)) ≤ ((maskedSample (source n) (observe n) (truth n) fun (value : α n) => Boosting.sampleWeight (bound n) numerator threshold (votes value) (truth n value)).eval pair).toReal

The same eventual information bound holds uniformly over all executable vote masks.

theorem Cslib.Crypto.Pseudoentropy.maskedSample_extract_dist_bind_le {α β Seed Output : Type} [Finite α] [Fintype Seed] [Fintype Output] [Nonempty Output] (source : ProbComp α) (observe : α → β) (truth : α → Bool) (mask : α → ProbComp Bool) (count informationBits : ℕ) (hmass : ∀ pair ∈ (maskedSample source id truth mask).eval.support, 2 ^ (-↑informationBits) ≤ ((maskedSample source id truth mask).eval pair).toReal) (seed : ProbComp Seed) (hash : Seed → List Bool → Output) (hhash : Probability.IsTwoUniversal seed.eval fun (s : Seed) (bits : Fin count → Bool) => hash s (List.ofFn bits)) {δ slack : ℝ} (hdensity : δ ≤ ((source >>= mask).eval true).toReal) (hslack : 0 ≤ slack) {Result : Type u_1} [Fintype Result] (test : List β × Seed × Output → PMF Result) : dist ((OracleComp.replicate count (maskedSample source observe truth mask) >>= extractLabels seed hash).eval.bind test) ((extractLabelsIdeal (observe <$> source) count seed).bind test) ≤ 2 * Real.exp (-2 * slack ^ 2 / (↑count * ↑informationBits ^ 2)) + √(↑(Fintype.card Output) * (2 * 2 ^ (-(↑count * δ - slack)))) / 2

Any sufficiently dense mask supplies the repeated-label extractor. Every randomized finite-output test receives all observations, the seed and the extracted value. The finite latent draw supplies the information bound; the public observation type may be infinite.

theorem Cslib.Crypto.Pseudoentropy.maskedSample_weight_extract_dist_bind_le {α β Seed Output : Type} [Fintype α] [Fintype Seed] [Fintype Output] [Nonempty Output] (source : ProbComp α) (observe : α → β) (truth : α → Bool) (votes : α → List Bool) (count sourceBits bound numerator threshold : ℕ) (hsource : ∀ value ∈ source.eval.support, 2 ^ (-↑sourceBits) ≤ (source.eval value).toReal) (seed : ProbComp Seed) (hash : Seed → List Bool → Output) (hhash : Probability.IsTwoUniversal seed.eval fun (s : Seed) (bits : Fin count → Bool) => hash s (List.ofFn bits)) {δ slack : ℝ} (hdensity : δ ≤ Boosting.density source.eval (↑numerator / ↑(Probability.dyadicSize bound)) fun (value : α) => BitString.listVoteMargin (votes value) (truth value) - ↑threshold) (hslack : 0 ≤ slack) {Result : Type u_1} [Fintype Result] (test : List β × Seed × Output → PMF Result) : dist ((OracleComp.replicate count (maskedSample source observe truth fun (value : α) => Boosting.sampleWeight bound numerator threshold (votes value) (truth value)) >>= extractLabels seed hash).eval.bind test) ((extractLabelsIdeal (observe <$> source) count seed).bind test) ≤ 2 * Real.exp (-2 * slack ^ 2 / (↑count * ↑(sourceBits + Nat.log 2 bound + 2) ^ 2)) + √(↑(Fintype.card Output) * (2 * 2 ^ (-(↑count * δ - slack)))) / 2

Independent vote-masked labels provide at least their soft density per sample for extraction. The bound is uniform over all vote lists and thresholds of that density; the test retains every public observation and the complete independent hash seed.