Documentation

CompPoly.Univariate.NTTFast.FastMul

Fast multiplication via NTT #

This file exposes the one-shot NTTFast multiplication entry point. It builds an NTTFast.Plan for the given domain and runs the planned multiplication pipeline.

source
@[inline]
def CompPoly.CPolynomial.NTTFast.Raw.fastMulImpl {R : Type u_1} [Field R] [BEq R] (D : NTT.Domain R) (p q : Raw R) :
Raw R

Raw pipeline for NTT-based multiplication.

Correctness as ordinary polynomial multiplication requires NTT.Domain.fits D p q. This raw API deliberately does not trim.

Instances For
    source
    @[inline]
    def CompPoly.CPolynomial.NTTFast.fastMulImpl {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (D : NTT.Domain R) (p q : CPolynomial R) :
    CPolynomial R

    Pipeline for NTT-based multiplication as a canonical polynomial.

    Instances For
      source
      @[inline]
      def CompPoly.CPolynomial.NTTFast.safeFastMul {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (D : NTT.Domain R) (p q : CPolynomial R) (_hfit : D.fits ↑p ↑q) :
      CPolynomial R

      Safe NTT-based multiplication wrapper.

      The domain-fit proof requires the caller to show that the domain covers the convolution length.

      Instances For
        source
        @[inline]
        def CompPoly.CPolynomial.NTTFast.withFallback {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (bestDomainForLength? : (requiredLen : ℕ) → Option (NTT.FittingDomain R requiredLen)) (p q : CPolynomial R) :
        CPolynomial R

        NTTFast-backed multiplication with canonical multiplication as a fallback.

        The selector should return a domain fitting the required convolution length. When it does, this uses fastMulImpl; otherwise it falls back to canonical CPolynomial multiplication.

        Instances For