Planned NTTFast multiplication

This file adds a reusable NTTFast plan that caches domain-derived data for repeated NTT-based multiplication.

structure CompPoly.CPolynomial.NTTFast.Plan (R : Type u_2) [Field R] : Type u_2

Cached domain data for repeated NTTFast multiplications.

• domain : NTT.Domain R
• inverseDomain : NTT.Domain R
• nInv : R
• twiddles : Array (Array R)
• inverseTwiddles : Array (Array R)

def CompPoly.CPolynomial.NTTFast.Plan.twiddlePowers {R : Type u_1} [Field R] (D : NTT.Domain R) (stage : ℕ) : Array R

Precompute the twiddle powers used by one radix-2 stage.

def CompPoly.CPolynomial.NTTFast.Plan.twiddleTable {R : Type u_1} [Field R] (D : NTT.Domain R) : Array (Array R)

Precompute the per-stage twiddle table for a domain.

def CompPoly.CPolynomial.NTTFast.Plan.ofDomain {R : Type u_1} [Field R] (D : NTT.Domain R) : Plan R

Build a reusable plan from an NTT domain.

@[irreducible]

def CompPoly.CPolynomial.NTTFast.Plan.butterflyDITInner {R : Type u_1} [Field R] (twiddles : Array R) (limit j i0 i1 : ℕ) (acc : Array R) : Array R

Inner DIT butterfly loop for one block.

@[irreducible]

def CompPoly.CPolynomial.NTTFast.Plan.butterflyDITBlocks {R : Type u_1} [Field R] (twiddles : Array R) (blockSize half blocks block : ℕ) (acc : Array R) : Array R

Outer DIT butterfly loop over blocks.

def CompPoly.CPolynomial.NTTFast.Plan.butterflyStageWithTwiddles {R : Type u_1} [Field R] (D : NTT.Domain R) (stage : ℕ) (twiddles a : Array R) : Array R

One butterfly stage using precomputed twiddle powers for that stage.

def CompPoly.CPolynomial.NTTFast.Plan.runStagesWithTwiddles {R : Type u_1} [Field R] (D : NTT.Domain R) (twiddles : Array (Array R)) (a : Array R) : Array R

Run all radix-2 stages using a precomputed per-stage twiddle table.

@[irreducible]

def CompPoly.CPolynomial.NTTFast.Plan.butterflyDITRadix4Inner {R : Type u_1} [Field R] (twiddlesLow twiddlesHigh : Array R) (limit j i0 i1 i2 i3 : ℕ) (acc : Array R) : Array R

Inner fused DIT loop for two adjacent radix-2 stages.

@[irreducible]

def CompPoly.CPolynomial.NTTFast.Plan.butterflyDITRadix4Blocks {R : Type u_1} [Field R] (twiddlesLow twiddlesHigh : Array R) (blockSize quarter blocks block : ℕ) (acc : Array R) : Array R

Outer fused DIT loop over radix-4 blocks.

def CompPoly.CPolynomial.NTTFast.Plan.butterflyRadix4StageWithTwiddles {R : Type u_1} [Field R] (D : NTT.Domain R) (lowStage : ℕ) (twiddlesLow twiddlesHigh a : Array R) : Array R

Run two adjacent DIT radix-2 stages as one radix-4 pass.

def CompPoly.CPolynomial.NTTFast.Plan.runStagesRadix4WithTwiddles {R : Type u_1} [Field R] (D : NTT.Domain R) (twiddles : Array (Array R)) (a : Array R) : Array R

Run DIT stages using fused radix-4 passes where possible.

@[irreducible]

def CompPoly.CPolynomial.NTTFast.Plan.butterflyDIFInner {R : Type u_1} [Field R] (twiddles : Array R) (limit j i0 i1 : ℕ) (acc : Array R) : Array R

Inner DIF butterfly loop for one block.

@[irreducible]

def CompPoly.CPolynomial.NTTFast.Plan.butterflyDIFBlocks {R : Type u_1} [Field R] (twiddles : Array R) (blockSize half blocks block : ℕ) (acc : Array R) : Array R

Outer DIF butterfly loop over blocks.

def CompPoly.CPolynomial.NTTFast.Plan.butterflyStageDIFWithTwiddles {R : Type u_1} [Field R] (D : NTT.Domain R) (stage : ℕ) (twiddles a : Array R) : Array R

One decimation-in-frequency butterfly stage using precomputed twiddle powers.

This accepts natural-order data and, when run from large stages down to small stages, produces bit-reversed evaluation order.

def CompPoly.CPolynomial.NTTFast.Plan.runStagesDIFWithTwiddles {R : Type u_1} [Field R] (D : NTT.Domain R) (twiddles : Array (Array R)) (a : Array R) : Array R

Run decimation-in-frequency stages, producing bit-reversed evaluation order.

@[irreducible]

def CompPoly.CPolynomial.NTTFast.Plan.butterflyDIFPairInner {R : Type u_1} [Field R] (twiddles : Array R) (limit j i0 i1 : ℕ) (accA accB : Array R) : Array R × Array R

Inner paired DIF butterfly loop for one block.

@[irreducible]

def CompPoly.CPolynomial.NTTFast.Plan.butterflyDIFPairBlocks {R : Type u_1} [Field R] (twiddles : Array R) (blockSize half blocks block : ℕ) (accA accB : Array R) : Array R × Array R

Outer paired DIF butterfly loop over blocks.

def CompPoly.CPolynomial.NTTFast.Plan.butterflyStageDIFPairWithTwiddles {R : Type u_1} [Field R] (D : NTT.Domain R) (stage : ℕ) (twiddles a b : Array R) : Array R × Array R

One paired DIF butterfly stage using precomputed twiddle powers.

@[irreducible]

def CompPoly.CPolynomial.NTTFast.Plan.butterflyDIFRadix4Inner {R : Type u_1} [Field R] (twiddlesHigh twiddlesLow : Array R) (limit j i0 i1 i2 i3 : ℕ) (acc : Array R) : Array R

Inner fused DIF loop for two adjacent radix-2 stages.

@[irreducible]

def CompPoly.CPolynomial.NTTFast.Plan.butterflyDIFRadix4Blocks {R : Type u_1} [Field R] (twiddlesHigh twiddlesLow : Array R) (blockSize quarter blocks block : ℕ) (acc : Array R) : Array R

Outer fused DIF loop over radix-4 blocks.

def CompPoly.CPolynomial.NTTFast.Plan.butterflyRadix4StageDIFWithTwiddles {R : Type u_1} [Field R] (D : NTT.Domain R) (lowStage : ℕ) (twiddlesHigh twiddlesLow a : Array R) : Array R

Run two adjacent DIF radix-2 stages as one radix-4 pass.

def CompPoly.CPolynomial.NTTFast.Plan.runStagesDIFRadix4WithTwiddles {R : Type u_1} [Field R] (D : NTT.Domain R) (twiddles : Array (Array R)) (a : Array R) : Array R

Run DIF stages using fused radix-4 passes where possible.

@[irreducible]

def CompPoly.CPolynomial.NTTFast.Plan.butterflyDIFRadix4PairInner {R : Type u_1} [Field R] (twiddlesHigh twiddlesLow : Array R) (limit j i0 i1 i2 i3 : ℕ) (accA accB : Array R) : Array R × Array R

Inner paired fused DIF loop for two adjacent radix-2 stages.

@[irreducible]

def CompPoly.CPolynomial.NTTFast.Plan.butterflyDIFRadix4PairBlocks {R : Type u_1} [Field R] (twiddlesHigh twiddlesLow : Array R) (blockSize quarter blocks block : ℕ) (accA accB : Array R) : Array R × Array R

Outer paired fused DIF loop over radix-4 blocks.

def CompPoly.CPolynomial.NTTFast.Plan.butterflyRadix4StageDIFPairWithTwiddles {R : Type u_1} [Field R] (D : NTT.Domain R) (lowStage : ℕ) (twiddlesHigh twiddlesLow a b : Array R) : Array R × Array R

Run two adjacent paired DIF radix-2 stages as one radix-4 pass.

def CompPoly.CPolynomial.NTTFast.Plan.runStagesDIFRadix4PairWithTwiddles {R : Type u_1} [Field R] (D : NTT.Domain R) (twiddles : Array (Array R)) (a b : Array R) : Array R × Array R

Run paired DIF stages using fused radix-4 passes where possible.

@[inline]

def CompPoly.CPolynomial.NTTFast.Plan.forwardImpl {R : Type u_1} [Field R] (P : Plan R) (p : Raw R) : Array R

Forward transform through a reusable plan.

@[inline]

def CompPoly.CPolynomial.NTTFast.Plan.forwardPairImpl {R : Type u_1} [Field R] (P : Plan R) (p q : Raw R) : Array R × Array R

Forward-transform two multiplication inputs through the same stage loops.

@[inline]

def CompPoly.CPolynomial.NTTFast.Plan.normalize {R : Type u_1} [Field R] (P : Plan R) (a : Array R) : Array R

Apply the cached inverse-domain normalization factor.

@[inline]

def CompPoly.CPolynomial.NTTFast.Plan.inverseImpl {R : Type u_1} [Field R] (P : Plan R) (v : Array R) : Raw R

Inverse transform through a reusable plan.

@[inline]

def CompPoly.CPolynomial.NTTFast.Plan.Raw.fastMulImpl {R : Type u_1} [Field R] [BEq R] (P : Plan R) (p q : Raw R) : Raw R

Raw planned pipeline for NTT-based multiplication.

@[inline]

def CompPoly.CPolynomial.NTTFast.Plan.fastMulImpl {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (P : Plan R) (p q : CPolynomial R) : CPolynomial R

Planned pipeline for NTT-based multiplication as a canonical polynomial.