Correctness and polynomial time of the complete affine program #
The explicit runtime composes the checked first phase and bounded round iteration. The selected runtime discharges every component guard using the same boosted chooser as the statistical construction. The whole program has one unconditional FP certificate, including parameter computation and malformed encoded inputs.
theorem
Algebraic.Cutwidth.Extractor.Internal.affineCorrelationBreakerRuntime_eq
(n d t L₀ e₀ L₁ e₁ er rounds : ℕ)
(first : MatchedBlockRuntimeValid n 64 L₀ e₀)
(adviceGuard : FlipFlopSizeGuard d (matchedBlockOutputBits 64 L₀) L₁ e₁)
(right : MatchedBlockRuntimeValid d 24 L₁ er)
(rowGuard : MatchedBlockRuntimeValid (matchedBlockOutputBits (growingMatchedBlockDepth t) L₁) 24 L₁ er)
(last : GrowingMatchedBlockRuntimeValid n t L₁ er)
(x : Fin n → Bool)
(y : Fin d → Bool)
(advice : List Bool)
:
affineCorrelationBreakerRuntime t L₀ e₀ L₁ e₁ er rounds (List.ofFn x) (List.ofFn y) advice = List.ofFn (affineCorrelationBreaker n d (growingMatchedBlockDepth t) L₀ e₀ L₁ e₁ er rounds x y advice)
theorem
Algebraic.Cutwidth.Extractor.Internal.affineCorrelationBreakerRuntime_length
(t L₀ e₀ L₁ e₁ er rounds : ℕ)
(x y advice : List Bool)
:
(affineCorrelationBreakerRuntime t L₀ e₀ L₁ e₁ er rounds x y advice).length = if GrowingMatchedBlockRuntimeValid x.length t L₁ er then 2 ^ growingMatchedBlockDepth t * L₁ else 0
theorem
Algebraic.Cutwidth.Extractor.Internal.affineCorrelationBreakerRuntime_mem_FP
{t L₀ e₀ L₁ e₁ er rounds : List Bool → ℕ}
{x y advice : List Bool → List Bool}
(ht : Complexity.UnaryFn t)
(hL₀ : Complexity.UnaryFn L₀)
(he₀ : Complexity.UnaryFn e₀)
(hL₁ : Complexity.UnaryFn L₁)
(he₁ : Complexity.UnaryFn e₁)
(her : Complexity.UnaryFn er)
(hrounds : Complexity.UnaryFn rounds)
(hx : x ∈ Complexity.FP)
(hy : y ∈ Complexity.FP)
(hadvice : advice ∈ Complexity.FP)
:
(fun (z : List Bool) =>
affineCorrelationBreakerRuntime (t z) (L₀ z) (e₀ z) (L₁ z) (e₁ z) (er z) (rounds z) (x z) (y z) (advice z)) ∈ Complexity.FP
theorem
Algebraic.Cutwidth.Extractor.Internal.affineCorrelationBreakerSelectedRuntime_length
(t target : ℕ)
(x y advice : List Bool)
:
(affineCorrelationBreakerSelectedRuntime t target x y advice).length = 2 ^ growingMatchedBlockDepth t * affinePhaseOneScale x.length t advice.length (affineIterationTarget t target)
theorem
Algebraic.Cutwidth.Extractor.Internal.affineCorrelationBreakerSelectedRuntime_length_le
(t target : ℕ)
(x y advice : List Bool)
:
(affineCorrelationBreakerSelectedRuntime t target x y advice).length ≤ 2 ^ 65 * (t + 1) * affinePhaseOneScale x.length t advice.length (affineIterationTarget t target)
theorem
Algebraic.Cutwidth.Extractor.Internal.affineCorrelationBreakerSelectedRuntime_eq
(n t target : ℕ)
(advice : List Bool)
(x : Fin n → Bool)
(y : Fin (affinePhaseOneRightBits n t advice.length (affineIterationTarget t target)) → Bool)
:
affineCorrelationBreakerSelectedRuntime t target (List.ofFn x) (List.ofFn y) advice = List.ofFn (affineCorrelationBreakerSelected n t target advice x y)
theorem
Algebraic.Cutwidth.Extractor.Internal.affineCorrelationBreakerSelectedRuntime_mem_FP
{t target : List Bool → ℕ}
{x y advice : List Bool → List Bool}
(ht : Complexity.UnaryFn t)
(htarget : Complexity.UnaryFn target)
(hx : x ∈ Complexity.FP)
(hy : y ∈ Complexity.FP)
(hadvice : advice ∈ Complexity.FP)
:
(fun (z : List Bool) => affineCorrelationBreakerSelectedRuntime (t z) (target z) (x z) (y z) (advice z)) ∈ Complexity.FP
theorem
Algebraic.Cutwidth.Extractor.Internal.affineCorrelationBreakerSelectedEval_pair
(x y advice parameter targetWord : List Bool)
:
affineCorrelationBreakerSelectedEval
(Complexity.pair (Complexity.pair x (Complexity.pair y advice)) (Complexity.pair parameter targetWord)) = affineCorrelationBreakerSelectedRuntime parameter.length targetWord.length x y advice
theorem
Algebraic.Cutwidth.Extractor.Internal.affineCorrelationBreakerSelectedEval_eq
(n t target : ℕ)
(advice : List Bool)
(x : Fin n → Bool)
(y : Fin (affinePhaseOneRightBits n t advice.length (affineIterationTarget t target)) → Bool)
:
affineCorrelationBreakerSelectedEval
(Complexity.pair (Complexity.pair (List.ofFn x) (Complexity.pair (List.ofFn y) advice))
(Complexity.pair (List.replicate t true) (List.replicate target true))) = List.ofFn (affineCorrelationBreakerSelected n t target advice x y)