The concrete advice chain and its final extraction

The initial state and left-to-right advice fold are Algorithm 2 of Chattopadhyay, Goyal, and Li, Non-Malleable Extractors and Codes, with their Many Tampered Extensions, Section 6.3: https://arxiv.org/abs/1505.00107. The original sources remain fixed throughout the fold. Short right sources are completed by false bits when forming the initial state.

The final map additionally extracts from the original left source using the seed-width prefix of the final state. Every call is the actual scheduled Boolean extractor. These definitions assert no statistical guarantee for the advice chain; that requires a separate invariant and entropy argument.

def Algebraic.Cutwidth.Extractor.adviceInitialState (m L : ℕ) (y : Fin m → Bool) : Fin (matchedBlockOutputBits 64 L) → Bool

The initial right state is a prefix of the right source, completed by false bits.

Equations

• Algebraic.Cutwidth.Extractor.adviceInitialState m L y i = (List.ofFn y)[↑i]?.getD false

def Algebraic.Cutwidth.Extractor.adviceFold (n m L e : ℕ) (x : Fin n → Bool) (y : Fin m → Bool) (q : Fin (matchedBlockOutputBits 64 L) → Bool) (advice : List Bool) : Fin (matchedBlockOutputBits 64 L) → Bool

Process advice from its first bit to its last, keeping both original sources.

Equations

• Algebraic.Cutwidth.Extractor.adviceFold n m L e x y q advice = List.foldl (Algebraic.Cutwidth.Extractor.flipFlopStep n m L e x y) q advice

def Algebraic.Cutwidth.Extractor.adviceCorrelationBreaker (n m L e : ℕ) (x : Fin n → Bool) (y : Fin m → Bool) (advice : List Bool) : Fin (matchedBlockSeedBits L) → Bool

The actual advice chain followed by extraction from the original left source.

Equations

• One or more equations did not get rendered due to their size.