Actual affine extraction averaged over leaky seeds #
Conditioning on the complete source-dependent leakage gives an exact factored
law with a constant joint source envelope. Its total pays exactly the number
of leaked bits. Applying the checked actual affine construction, then forgetting
only the leakage transcript, gives the honest-base-seed average used by
Chattopadhyay--Liao, Lemma 5.3, printed pp.19--20:
https://arxiv.org/abs/2110.12652. The tampered seed is f y i XOR its leakage;
it is never replaced by the honest seed y.
theorem
Algebraic.Cutwidth.Extractor.Internal.affineLeakageOutputWeight_average_dist_le
(n t a target : ℕ)
(p : (Fin n → Bool) → ℝ)
(leak : (Fin n → Bool) → Option (Fin t) → Fin (affinePhaseOneRightBits n t a (affineIterationTarget t target)) → Bool)
(advice : Option (Fin t) → List Bool)
(g : (Fin (affinePhaseOneRightBits n t a (affineIterationTarget t target)) → Bool) → Fin n → Bool)
(f :
(Fin (affinePhaseOneRightBits n t a (affineIterationTarget t target)) → Bool) →
Fin t → Fin (affinePhaseOneRightBits n t a (affineIterationTarget t target)) → Bool)
(positive : 0 < t)
(probability : IsProbabilityWeight p)
(cap :
∀ (x : Fin n → Bool),
p x ≤ (2 ^ (affineIterationSourceEntropy n t a target + (t + 1) * affinePhaseOneRightBits n t a (affineIterationTarget t target)))⁻¹)
(honest_length : (advice none).length = a)
(tampered_length : ∀ (i : Fin t), (advice (some i)).length = a)
(different : ∀ (i : Fin t), advice none ≠ advice (some i))
:
let σ := affineIterationTarget t target;
let d := affinePhaseOneRightBits n t a σ;
have h := growingMatchedBlockDepth t;
have L₀ := affinePhaseOneInitialScale n t a σ;
have L := affinePhaseOneScale n t a σ;
have e := affinePhaseOneLocalError σ;
have cb := affineCorrelationBreaker n d h L₀ e L (adviceErrorExponent a e) e (affineIterationRounds t);
∑ y : Fin d → Bool,
uniformWeight (Fin d → Bool) y * weightDist (affineLeakageOutputWeight cb p leak advice (g y) y (f y))
(uniformSecondWeight (affineLeakageOutputWeight cb p leak advice (g y) y (f y))) ≤ (2 ^ target)⁻¹