Documentation

Complexitylib.Algebraic.LowerBound.Cutwidth.Extractor.CorrelationBreaker.Affine.Defs

The complete actual affine correlation-breaker construction #

Run the first affine phase, then repeatedly execute the four-call merging round with the same original source words. The selected construction uses enough rounds to cover all tamperings, and boosts the first-phase target to pay the accumulated error. These are deterministic programs; their source and advice hypotheses belong to the extraction theorems.

The construction follows Chattopadhyay--Liao, Extractors for Sum of Two Sources, Theorem 6.1, printed pp.23--25: https://arxiv.org/abs/2110.12652.

source
def Algebraic.Cutwidth.Extractor.affineCorrelationBreaker (n d h L₀ e₀ L₁ e₁ er rounds : ℕ) (x : Fin n → Bool) (y : Fin d → Bool) (advice : List Bool) :
Fin (matchedBlockOutputBits h L₁) → Bool

The first affine phase followed by actual rounds on the unchanged original sources.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Algebraic.Cutwidth.Extractor.affineCorrelationBreakerSelected (n t target : ℕ) (advice : List Bool) (x : Fin n → Bool) (y : Fin (affinePhaseOneRightBits n t advice.length (affineIterationTarget t target)) → Bool) :
    Fin (matchedBlockOutputBits (growingMatchedBlockDepth t) (affinePhaseOneScale n t advice.length (affineIterationTarget t target))) → Bool

    Select every scale, local error, and round count from the original input dimensions.

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