Documentation

CompPoly.Univariate.NTTFast.Correctness.Radix4DIT

Radix-4 DIT NTTFast correctness #

Correctness proofs for the mixed radix-4 decimation-in-time stage loop used by NTTFast.

source
def CompPoly.CPolynomial.NTTFast.Plan.radix4Cell {R : Type u_1} [Field R] (wLow wHigh0 wHigh1 : R) (i0 i1 i2 i3 : ℕ) (acc : Array R) :
Array R
Instances For
    source
    @[simp]
    theorem CompPoly.CPolynomial.NTTFast.Plan.size_radix4Cell {R : Type u_1} [Field R] (wLow wHigh0 wHigh1 : R) (i0 i1 i2 i3 : ℕ) (acc : Array R) :
    (radix4Cell wLow wHigh0 wHigh1 i0 i1 i2 i3 acc).size = acc.size
    source
    theorem CompPoly.CPolynomial.NTTFast.Plan.butterflyStageWithTwiddles_eq_ntt {R : Type u_1} [Field R] (D : NTT.Domain R) (stage : ℕ) (twiddles a : Array R) (htwiddles : ∀ j < 2 ^ stage, twiddles.getD j 0 = (D.omega ^ (D.n / 2 ^ (stage + 1))) ^ j) :
    butterflyStageWithTwiddles D stage twiddles a = NTT.Transform.butterflyStage D stage a

    A DIT butterfly stage with matching cached twiddles agrees with the NTT stage.

    source
    theorem CompPoly.CPolynomial.NTTFast.Plan.runStagesWithTwiddles_eq_ntt {R : Type u_1} [Field R] (D : NTT.Domain R) (a : Array R) :
    runStagesWithTwiddles D (twiddleTable D) a = NTT.Transform.runStages D a

    The DIT radix-2 stage loop with the full twiddle table agrees with NTT.

    source
    theorem CompPoly.CPolynomial.NTTFast.Plan.runStagesRadix4WithTwiddles_eq_ntt {R : Type u_1} [Field R] (D : NTT.Domain R) (a : Array R) (ha : a.size = D.n) :
    runStagesRadix4WithTwiddles D (twiddleTable D) a = NTT.Transform.runStages D a

    The mixed radix-4 DIT stage loop agrees with the radix-2 NTT stage loop on domain-sized arrays.