Documentation

CompPoly.Univariate.NTTFast.Correctness.Radix4DIF

Radix-4 DIF NTTFast correctness #

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

source
def CompPoly.CPolynomial.NTTFast.Plan.radix4DIFCell {R : Type u_1} [Field R] (wHigh0 wHigh1 wLow : R) (i0 i1 i2 i3 : ℕ) (acc : Array R) :
Array R
Instances For
    source
    @[simp]
    theorem CompPoly.CPolynomial.NTTFast.Plan.size_radix4DIFCell {R : Type u_1} [Field R] (wHigh0 wHigh1 wLow : R) (i0 i1 i2 i3 : ℕ) (acc : Array R) :
    (radix4DIFCell wHigh0 wHigh1 wLow i0 i1 i2 i3 acc).size = acc.size
    source
    theorem CompPoly.CPolynomial.NTTFast.Plan.runStagesDIFRadix4WithTwiddles_correct {R : Type u_1} [Field R] (D : NTT.Domain R) (a : Array R) :
    runStagesDIFRadix4WithTwiddles D (twiddleTable D) (NTT.loadNaturalArray D a) = NTT.Transform.bitRevPermute D (NTT.Forward.forwardSpec D a)

    The mixed radix-4 DIF stage loop computes the bit-reversed forward NTT output.