Documentation

CompPoly.Univariate.Raw.Context

Raw Univariate Algorithm Contexts #

Array-level execution dictionaries for reusable raw univariate polynomial kernels.

source
structure CompPoly.CPolynomial.Raw.MulContext (R : Type u_2) [Semiring R] [BEq R] [LawfulBEq R] :
Type u_2

Internal raw multiplication backend for array-level polynomial kernels.

  • mul : Raw R → Raw R → Raw R

    Multiply two raw polynomials, returning the trimmed raw product.

  • mul_eq_mul (p q : Raw R) : self.mul p q = p * q

    The backend agrees with raw polynomial multiplication.

Instances For
    source
    structure CompPoly.CPolynomial.Raw.ModContext (R : Type u_2) [Field R] [BEq R] [LawfulBEq R] :
    Type u_2

    Internal raw monic-remainder backend for array-level polynomial kernels.

    • modByMonic : Raw R → Raw R → Raw R

      Reduce the first raw polynomial modulo the second raw monic divisor.

    • modByMonic_eq_modByMonic (p q : Raw R) : p.trim = p → q.trim = q → self.modByMonic p q = p.modByMonic q

      The backend agrees with raw monic remainders for canonical raw inputs.

    Instances For
      source
      def CompPoly.CPolynomial.Raw.MulContext.naive {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] :
      MulContext R

      The default raw multiplication context, backed by raw polynomial multiplication.

      Instances For
        source
        def CompPoly.CPolynomial.Raw.MulContext.ntt {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (bestDomainForLength? : (requiredLen : ℕ) → Option (NTT.FittingDomain R requiredLen)) :
        MulContext R

        NTT-backed raw multiplication context with raw multiplication for unsupported lengths.

        Instances For
          source
          def CompPoly.CPolynomial.Raw.MulContext.nttFast {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (bestDomainForLength? : (requiredLen : ℕ) → Option (NTT.FittingDomain R requiredLen)) :
          MulContext R

          NTTFast-backed raw multiplication context with raw multiplication for unsupported lengths.

          Instances For
            source
            def CompPoly.CPolynomial.Raw.ModContext.naive {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] :
            ModContext R

            The default raw monic-remainder context, backed by raw modByMonic.

            Instances For
              source
              def CompPoly.CPolynomial.Raw.ModContext.remainderOnly {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] :
              ModContext R

              Raw remainder-only monic-remainder context.

              Instances For
                source
                def CompPoly.CPolynomial.Raw.ModContext.reversal {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (M : MulLowContext R) :
                ModContext R

                Raw reversal-based monic-remainder context parameterized by low-product multiplication.

                Instances For
                  source
                  def CompPoly.CPolynomial.Raw.ModContext.reversalNtt {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (bestDomainForLength? : (requiredLen : ℕ) → Option (NTT.FittingDomain R requiredLen)) :
                  ModContext R

                  Raw monic remainders by reversal, using an NTT low-product backend.

                  Instances For
                    source
                    def CompPoly.CPolynomial.Raw.ModContext.reversalNttFast {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (bestDomainForLength? : (requiredLen : ℕ) → Option (NTT.FittingDomain R requiredLen)) :
                    ModContext R

                    Raw monic remainders by reversal, using an NTTFast low-product backend.

                    Instances For