Actual affine outputs after deterministic seed leakage #
Each call uses the same shifted source. Its seed is the XOR of a fixed seed and a deterministic observation of the source. A bad honest seed admits some shift and some collection of tampered seeds for which the honest output fails to be uniform conditioned on all tampered outputs. The witnesses may depend on the honest seed.
This is the finite bad-seed construction of Chattopadhyay--Liao, Extractors for Sum of Two Sources, Lemma 5.3: https://arxiv.org/abs/2110.12652.
noncomputable def
Algebraic.Cutwidth.Extractor.affineLeakageOutputWeight
{n d t : ℕ}
{Out : Type u_1}
(cb : (Fin n → Bool) → (Fin d → Bool) → List Bool → Out)
(p : (Fin n → Bool) → ℝ)
(leak : (Fin n → Bool) → Option (Fin t) → Fin d → Bool)
(advice : Option (Fin t) → List Bool)
(b : Fin n → Bool)
(y : Fin d → Bool)
(ys : Fin t → Fin d → Bool)
:
All actual tampered outputs and the honest output after source-dependent seed leakage.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
Algebraic.Cutwidth.Extractor.affineLeakageBadSeeds
{n d t : ℕ}
{Out : Type u_1}
[Fintype Out]
(cb : (Fin n → Bool) → (Fin d → Bool) → List Bool → Out)
(p : (Fin n → Bool) → ℝ)
(leak : (Fin n → Bool) → Option (Fin t) → Fin d → Bool)
(advice : Option (Fin t) → List Bool)
(γ : ℝ)
:
Honest seeds for which some shift and tampered seed choices exceed the requested error.
Equations
- One or more equations did not get rendered due to their size.