The concrete two-round look-ahead and advice-bit step

These are the deterministic programs in Algorithm 1 of Chattopadhyay, Goyal, and Li, Non-Malleable Extractors and Codes, with their Many Tampered Extensions, Section 6.3: https://arxiv.org/abs/1505.00107. Every extractor call uses the actual scheduled Boolean program.

The shared seed width is 2^24 * L; the right state has 2^64 * L bits. Both refresh calls read the original right source y. The intermediate right state is used only by the middle call of each look-ahead. Each step therefore makes eight extractor calls, with the advice bit choosing opposite look-ahead outputs at the two refreshes. The definitions are total for all parameters. Opposite.False and Opposite.True prove the one-step guarantee, and Advice.Extraction proves the complete advice-chain guarantee (adviceCorrelationBreaker_dist_le).

def Algebraic.Cutwidth.Extractor.flipFlopSeedPrefix (L : ℕ) (q : Fin (matchedBlockOutputBits 64 L) → Bool) : Fin (matchedBlockSeedBits L) → Bool

Read the common seed-width prefix of a right state.

Equations

• Algebraic.Cutwidth.Extractor.flipFlopSeedPrefix L q = Algebraic.Cutwidth.Extractor.blockPrefix ⋯ q

def Algebraic.Cutwidth.Extractor.flipFlopLookAhead (n L e : ℕ) (x : Fin n → Bool) (q : Fin (matchedBlockOutputBits 64 L) → Bool) : (Fin (matchedBlockSeedBits L) → Bool) × (Fin (matchedBlockSeedBits L) → Bool)

Two rounds of alternating extraction, using three actual scheduled calls.

Equations

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

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

The advice-bit step, refreshing twice from the original full right source.

Equations

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